A Simple Type System for FOF

Koen Claessen, Geoff Sutcliffe

The goal of this document is to:

Summarize the kinds of features one might want in a type system that are relatively well-known.
Propose a simple type system that is powerful enough to deal with some common type situations in current TPTP problems, and also be compatible with the type system requirements of the higher order logic extension of the TPTP.

These ideas have been implemented in the TFF syntax.

Type System

A type system consists of the following:

a definition of what types there are,
decisions about any implicit properties of the types, e.g., inhabitance, intersection.
definitions that specify the types of variables
definitions that specify the argument types and result type for function symbols
definitions that specify the argument types for predicates symbols
a type checking algorithm,
a definition of what it means to be a model of a typed theory,
a translation of typed formulae into untyped formulae.
The translation has to have the following property: For typed formulae F that pass the type checking algorithm, and their translated untyped counterpart F', F has a typed model iff F' has an (untyped) model.

Feature Summary

The following features can be discussed when talking about type systems:

Simple types: There is only a finite set of primitive types.
Examples: bool, int, animal.
Parametrized types: There are types that can take other types as arguments.
Examples: list(int), pair(bool,animal), list(pair(int,bool)).
Dependent types: There are types that can have types as well as terms as arguments. This means that the term-level and type-level conceptually collapse.
Examples: vector(3,int), set(finite), set(infinite).
Parametric polymorphism: A function or predicate symbol can be used for any given argument type.
Examples: ∀A (cons: A > list(A) > list(A)), ∀A (nil: list(A)).
Ad-hoc polymorphism: A function or predicate symbol can be used with a (limited) number of different types, determined by the context in which it is used.
Examples: on(point,line), on(line,plane).
Subtyping: A (partial) ordering « on all types is specified. If s1 « s2, and t : s1, then t can be used everywhere where something of type s2 is expected. This necessarily leads to non-disjoint types.
Disjoint vs. non-disjoint types: If types are disjoint then no term has more than one type. If types are not disjoint then a term may have more than one type. If a latttice of types is used to provide a subtyping structure, types are necessarily non-disjoint (see Future Plans below). Disjoint types give systems more information that can be used to improve performance. The effect of allowing non-disjoint types is to require runtime checking of the well-typedness of inferred formulae when equality is used, because ill-typed results are possible. This arises from equalities that are allowed between terms of different types. For example,
```
    tff(a_type,type,a:animal).
    tff(b_type,type,b:integer).
    tff(has_4_legs_type,type,has_4_legs: animal > $oType).
    tff(some_integer_animal,axiom,a = b).
    tff(a_has_4_legs,axiom,has_4_legs(a)).
    tff(b_has_4_legs,plain,has_4_legs(b),inferred(paramodulation ... 
```
To overcome this problem would require either multiple equality symbols or polymorphic equality (see below).
Inhabitance: Types (i.e., their domains in interpretation) need to be assumed to be inhabited, in order for the (normal) logical reasoning processes of first-order logic to apply. Nasty things happen if a domain is empty, e.g., ∀X p(X), ∀X ~ p(X), ∀X false are all true.

Equality

There are various options for dealing with equality:

Monomorphic equality: Equality is dealt with just like any other predicate. However, this means that equality can only be used on one type, which seems silly.
Multiple equality symbols: A separate equality symbol is introduced for each type where we want to use equality, e.g. =int and =bool. These can then be explicitly typed with their own types. This also seems silly.
Subtyping equality with a universe: Equality is allowed between all terms, even terms of different types. This introduces a mild form of subtyping, where there is one supertype and all other types are a direct subtype of this supertype. The two argument types of equality are then this supertype. Using this option leads to subtyping, which in turn leads to non-disjoint types, which leads to less gain for systems, so it has been rejected. However, see Future Plans below for ideas about subtyping. Hmmm, I'm not convinced ... this option is still viable. Here's an example that illustrates the knots that subtyping introduces ...
```
a:$iType; f:fruit; ifun: $iType -> $iType; fruitfun: fruit -> fruit;

a = f
ifun(f)
fruitfun(a)
```
Polymorphic equality: Either equality is thought of as if it had the parametric polymorphic type ∀S (=: S > S > o), or ad-hoc polymorphism is used and different versions of equality are introduced depending on its arguments. The effect is the same; equality can be used on any type, as long as both arguments have the same type.

We think ...

It is probably impossible to have a type system where all of the above is present; some features just don't mix well with each other. Here are some observations/conjectures:

Having parametrized types does not make any sense without some form of polymorphism or subtyping.
In order to have decidable type checking, and not change the current syntax of terms and atoms, parametric polymorphism and subtyping cannot be combined.
For decidable type checking, it is necessary to keep the type-level separate from the term- and predicate-level. Dependent types lead to undecidable type checking, since type checking would require computing terms, which cannot be done in general.
Given any type system, it is always possible to add some form of ad-hoc polymorphism to it without problems. (One just complains in the type checking if it cannot be derived from the context which typing is meant for a particular use of a symbol.)
Systems should be able to easily improve performance from the type information.

Proposal

TPTP form: A new TPTP annotated formula type will be introduced, with symbol tff for "typed first order form". TPTP file names for this form will use a = separator (in the way the - is used for CNF and + is used for FOF). A new TPTP role for typing will be added, type.
Defined types: The types $iType (which can be abbreviated to $i) and $oType (which can be abbreviated to $o) are defined. These are, respectively, the types of individuals and truth values.
User types: Types are not declared in advance - they can be introduced freely in type declarations and in formulae when variables are given types.
Implicit properties: All types are assumed to be inhabited. All types are disjoint, including user types being disjoint from the defined types. (However, see Future Plans below for how this will be relaxed.)

Type declarations: Every function and predicate symbol has exactly one specifically declared type. Example:

    tff(cons_type,type, 
        cons: (int * list) > list   ).

    tff(is_empty_type,type, 
        isEmpty:list > $oType   ).

Types of variables: Every variable can be typed at quantification time. Example (in the proposed TPTP style syntax):
```
tff(list_not_empty,axiom, 
    ! [X:int,Xs:list] : ~isEmpty(cons(X,Xs))   ).
```
Equality: Equality is ad-hoc polymorphic. An equality between terms of different types is ill-typed.
Typing for fof: fof annotated formulae provide (implicit) typing of the predicates, and functions in the logical formula. All non-defined predicates have type ($iType * ... * $iType) > $oType. All non-defined functions have type ($iType * ... * $iType) > $iType. All such (implicit) typing must, like explicit typing, agree with any previous typing. Variables in fof annotated formulae are implicitly of type $iType.
Type checking: It is a simple matter to check that all terms and atoms respect the typing that has been declared.
Models: A model consists of a non-empty domain for each type. These domains all have to be non-overlapping. Further, it contains an interpretation involving the appropriate domains for each function and predicate symbol.

Translation: Each type becomes a new unary predicate in the untyped world.

A function type declaration of the form

tff(f_type,type,
    f: (t1 * ... * tn) > tf  ).

is translated into:

fof(f_type,axiom, 
    ! [X1,...,Xn] : 
      ( ( t1(X1) 
        & ... 
        & t2(Xn) ) 
     => tf(f(X1,...,Xn)) )   ).

Predicate type declarations are ignored (!).

A typed quantification of the form

! [X1:t1,...,Xn:tn] : p(X1,...,Xn)

is translated into:

! [X1,...,Xn] : 
      ( ( t1(X1) 
        & ... 
        & tn(Xn) ) 
     => p(X1,...,Xn) )

A typed quantification of the form

? [X1:t1,...,Xn:tn] : p(X1,...,Xn)

is translated into:

? [X1,...,Xn] : 
      ( t1(X1) 
      & ... 
      & tn(Xn)
      & p(X1,...,Xn) )

The Effect on ATP Systems

What is the effect of typing on ATP systems?

Systems have to do type-checking on the input.
Since no polymorphism is allowed, standard unification and matching only have to be extended minimally: they have to check if variables are of the correct type.
All standard inferences and simplifications remain correct as long as substitutions are sort-preserving.

Theorem provers: TODO. Reference: SPASS and soft typing.

Model finders have an easier task to find typed models, as long as the domains of the separate types are as most as large as the domain of the untyped version of the problem. This is the case for the first proposal, but definitely not for the second.

Future Plans

Subtyping: A lattice of types provides a general subtyping structure. The lattice will have $iType as the top type. A new defined type, $eType can be defined for the bottom of the lattice, for the empty type. There will be no assumption of disjointness of types in the lattice. However, types outside the lattice remain disjoint from each other and the types in the lattice.

Predicates as types: Josef Urban is using predicates as types, which allows a flexible structure, e.g.,

    ! [X:(human & male)] : ~ has_ovary(X)
    ? [Y:(republican | democrat)] : president(Y)
    ! [M : matrix(4)] : M = M

These are translated as

    ! [X] : ((human(X) & male(X)) => ~ has_ovary(X))
    ? [Y] : ((republican(Y) | democrat(Y)) & president(Y))
    ! [M] : (matrix(X,4) => M = M)

Can/should this be integrated?

Examples taken from the current TPTP

TODO.