A Simple Type System for FOF

The goal of this document is to:

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.
Summarize relatively well-known features and options of type systems, which we considered when putting this together.

The Proposal for TFF0

The initial proposal is for a simple type system that helps users write well-typed problems, and imposes very little burden on ATP system implementors. This is the core TFF language, known as TFF0 (analogous to THF0). In the future the full TFF language will be developed, including more powerful constructs, e.g., subtyping.

These ideas have been captured in the TFF syntax.
Some sample TFF0 problems.
Some sample TFF problems.

See the following sections for the options and arguments that led to this proposal.

TPTP form
A new TPTP annotated formula language is introduced, with symbol tff for "typed first order form". TPTP file names for this form will use a _ separator (in the way that ^ is used for THF, + is used for FOF and - is used for CNF - I wanted to use : to remind users of the typing (see below) but in some operating systems : cannot be used in filenames). The TPTP role type will be used for formula that declare types.
Defined atomic types
The atomic types $i (individuals), $o (Booleans), and $tType are defined. ($tType is the "type" of atomic types - it is not really a type, and in other places this is known as the "kind" of atomic types. See below for motivation for its existence and usage.) Other defined atomic types are associated with specific theories. In particular, $int, $rat, and $real are atomic types for interpreted arithmetic.
User atomic type declarations:
User atomic types can (but don't have to) be declared in advance of use, to be of "type" $tType. Example:
```
    tff(food_type,type, 
        food: $tType ).

    tff(fruit_type,type, 
        fruit: $tType ).

    tff(list_type,type, 
        list: $tType ).  
```
Declaration of atomic types is not required, i.e., atomic types can be introduced on the fly. TPTP problems will have all atomic types declared, so as to provide a typo check.
Defined functions and predicates
Defined functions and predicates have preassigned types.
- $true is of type $o
- $false is of type $o
- $distinct is ad-hoc polymorphic over all atomic types, and maybe overloaded with different arities.
- $itef has the type ($o * $o * $o) > $o
- $itett is ad-hoc polymorphic on its second and third arguments and range, which can be any atomic type other than $o. For any such atomic type α it has the type ($o * α * α) > α
- The (atomic) types of numbers are defined on the interpreted arithmetic page.
- The types of the arithmetic predicates and functions are defined on the interpreted arithmetic page.
Function and predicate type declarations
Every function and predicate symbol has maximally one declared type. Example:
```
    tff(cons_type,type, 
        cons: (fruit * list) > list   ).

    tff(is_empty_type,type, 
        isEmpty: list > $o   ).
```
The range type of a function must be an atomic type, and cannot be $o. The range type of a predicate must be $o. Note that symbols of arity greater than one use the * for a cross-product type. Currying is not possible, i.e., the first example above cannot be written
```
    tff(cons_type,type, 
        cons: fruit > list > list   ). 
```
If a symbol's type is declared more than once, and the types are not the same, that's an error.
Types of variables
Every variable can be given an atomic type at quantification time. Example:
```
tff(list_not_empty,axiom, 
    ! [X: fruit,Xs: list] : ~isEmpty(cons(X,Xs))   ).
```
Implicit typing for functions and predicates
If a symbol is used and its type has not been declared, then default types are assumed.
- All untyped predicates get type ($i * ... * $i) > $o.
- All untyped functions get type ($i * ... * $i) > $i.
- All untyped variables get type $i.
If a symbol's type is declared later to be different from the assumed type, that's an error.
Equality
Equality is ad-hoc polymorphic over atomic types. An equality between terms of different atomic types is ill-typed.
Interpetations
An interpretation has a non-empty domain for each atomic type. These domains are pairwise disjoint. It also maps function and predicate symbols to functions and predicates that respect the types of those symbols.
Type checking
It is a simple matter to check that all terms and atoms respect the types that have been declared.
Translation
A set of well-typed TFF formulae can be translated to an equisatisfiable set of FOF formulae. Each atomic type becomes a new unary predicate in the untyped world.
- All atomic types are inhabited, so a type declaration
```
tff(one_type_decl,type,
    one_type: $tType ).
```
  produces the axiom:
```
fof(one_type_inhabited,axiom,
    ? [X] : one_type(X) ).
```
  It is unnecessary to produce axioms that say the terms with different atomic types are unequal (reflecting the fact that atomic type domains are disjoint) because it is impossible to claim they are equal in a well-typed formula.
- A function type declaration of the form
```
tff(f_type,type,
    f: (t1 * ... * tn) > tf  ).
```
  is translated into:
```
fof(f_type,axiom, 
    ! [X1,...,Xn] : tf(f(X1,...,Xn)) ).
```
  It is unnecessary to have an implication with the antecedent checking the types of the arguments X1,...,Xn because it is impossible to use incorrectly typed arguments in a well-typed formula.
- Predicate type declarations are ignored (!).
- A quantification of the form
```
! [X1: t1,...,Xn: tn] : p(X1,...,Xn)
```
  is translated into:
```
! [X1,...,Xn] : 
      ( ( t1(X1) 
        & ... 
        & tn(Xn) ) 
     => p(X1,...,Xn) )
```
  Geoff thinks that for problems that do not contain equality it is unnecessary to have an implication with the antecedent checking the types of the arguments X1,...,Xn because they could never become instantiated to a term of the wrong type in a wel-typed problem. If equality is present the check is necessary because of paramodulation, either into those variables (most ATP systems won't do that), or paramodulation from a variable of another type. The latter is a case that needs to be checked in a system that deals with TFF natively.
- A quantification of the form
```
? [X1: t1,...,Xn: tn] : p(X1,...,Xn)
```
  is translated into:
```
? [X1,...,Xn] : 
      ( t1(X1) 
      & ... 
      & tn(Xn)
      & p(X1,...,Xn) )
```

The next section is a developmental idea that should be ignored
except by Geoff and other TPTP developers.

Strong Translation
A set of well-typed TFF formulae can be translated to an equisatisfiable set of FOF formulae, with the additional property that the FOF translations of all ill-typed TFF formulae are unsatisfiable in conjunction with the FOF translations of the type declarations (equivalently, their negations can be proved from from the FOF translations of the type declarations.) This translation is interesting because it maintains "order" between status in the TFF form and the FOF form.

A syntax error in the TFF is a syntax error in the FOF
An ill-typed TFF is unsatisfiable in the FOF
An unsatisfiable TFF is unsatisfiable in the FOF
A satisfiable TFF is satisfiable in the FOF
A tautologous TFF is tautologous in the FOF

With the weak translation above it is possible for an ill-typed TFF to be satisfiable or tautologous in the FOF, thus "crossing over" the unsatisfiable status. That seems less desirable, and may lead to inappropriate conclusions. For example, if a well-typed TFF axiomatization is translated to FOF for processing, a user might (foolishly) write and prove some FOF theorems that are "ill-typed". Of course the user should write TFF conjectures and check their types before converting to FOF. Those ill-typed "theorems" cannot be proved from the strong translation.

All atomic types are inhabited, so a type declaration

tff(one_type_decl,type,
    one_type: $tType ).

produces the axiom:

fof(one_type_inhabited,axiom,
    ? [X] : one_type(X) ).

All atomic types are disjoint, so that a pair of type declarations

tff(one_type_decl,type,
    one_type: $tType ).

tff(another_type_decl,type,
    another_type: $tType ).

produce the axiom:

fof(one_type_not_another_type,axiom,
    ! [X,Y] :
      ( one_type(X)
     => ~ another_type(X) )  ).

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)) )   ).

A predicate type declaration of the form

tff(p_type,type,
    p: (t1 * ... * tn) > $o  )..

is translated into:

fof(p_type,axiom,
    ! [X1,...,Xn] :
      ( ( t1(X1)
        & ...
        & t2(Xn) )
     <= p(X1,...,Xn) )   ).

A quantification of the form

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

is translated into:

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

A quantification of the form

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

is translated into:

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

Consider the following TFF types and conjectures ...

%----Type declarations
tff(australian,type,                    australian: $tType ).
tff(russian,type,                       russian: $tType ).
tff(vodka,type,                         vodka: $tType ).
tff(geoff,type,                         geoff: australian ).
tff(andrei,type,                        andrei: russian ).
tff(smirnoff,type,                      smirnoff: vodka ).
tff(rotgut,type,                        rotgut: vodka ).
tff(drink_of,type,                      drink_of: russian > vodka ).
tff(tasty,type,                         tasty: vodka > $o ).
tff(trueblue,type,                      trueblue: australian > $o ).
%----Ill-typed conjectures
tff(geoff_vodka,conjecture,             vodka(drink_of(geoff)) ).
tff(tasty_australian,conjecture,        ? [X: australian] : tasty(X) ).
tff(tasty_geoff,conjecture,             tasty(geoff) ).
tff(tasty_drink_of_geoff,conjecture,    tasty(drink_of(geoff)) ).
tff(geoff_rotgut,conjecture,            drink_of(geoff) = rotgut ).
tff(trueblue_andrei,conjecture,         trueblue(andrei) ).
tff(geoff_andrei,conjecture,            geoff = andrei ).
tff(drink_of_andrei_russian,conjecture, drink_of(andrei) = geoff ).

In the weak translation the first conjecture can be proved, and none of the others can be disproved (their negations proved) ...

fof(australian,axiom,                   ? [X] : australian(X) ).
fof(russian,axiom,                      ? [X] : russian(X) ).
fof(vodka,axiom,                        ? [X] : vodka(X) ).
fof(geoff_australian,axiom,             australian(geoff) ).
fof(andrei_russian,axiom,               russian(andrei) ).
fof(smirnoff_vodka,axiom,               vodka(smirnoff) ).
fof(rotgut_vodka,axiom,                 vodka(rotgut) ).
fof(drink_of_russian,axiom,             ! [X] : vodka(drink_of(X)) ).
%----Can prove this weird thing
fof(geoff_vodka,conjecture,             vodka(drink_of(geoff)) ).
%----Cannot prove (they are CSA) these negated weird things (but also cannot 
%----prove their unnegated form, like the one above).
fof(tasty_australian,conjecture,        ~ ? [X] : ( australian(X) & tasty(X) )).
fof(tasty_geoff,conjecture,             ~ tasty(geoff) ).
fof(tasty_drink_of_geoff,conjecture,    ~ tasty(drink_of(geoff)) ). 
fof(geoff_rotgut,conjecture,            drink_of(geoff) != rotgut ).
fof(trueblue_andrei,conjecture,         ~ trueblue(andrei) ).
fof(geoff_andrei,conjecture,            geoff != andrei ).
fof(drink_of_andrei_russian,conjecture, drink_of(andrei) != geoff ).

In the strong translation all of the conjectures can be disproved (their negations can be proved) ...

fof(australian,axiom,                   ? [X] : australian(X) ).
fof(russian,axiom,                      ? [X] : russian(X) ).
fof(australian_not_russian,axiom,       ! [X] : ( australian(X) => ~ russian(X) ) ).
fof(vodka,axiom,                        ? [X] : vodka(X) ).
fof(australian_not_vodka,axiom,         ! [X] : ( australian(X) => ~ vodka(X) ) ).
fof(russian_not_vodka,axiom,            ! [X] : ( russian(X) => ~ vodka(X) ) ).
fof(geoff_australian,axiom,             australian(geoff) ).
fof(andrei_russian,axiom,               russian(andrei) ).
fof(smirnoff_vodka,axiom,               vodka(smirnoff) ).
fof(rotgut_vodka,axiom,                 vodka(rotgut) ).
fof(drink_of_russian,axiom,             ! [X] : ( russian(X) <=> vodka(drink_of(X)) ) ).
fof(vodka_tasty,axiom,                  ! [X] : ( tasty(X) => vodka(X) ) ).
fof(australian_trueblue,axiom,          ! [X] : ( trueblue(X) => australian(X) ) ).
%----These can all be proved - they are the negations of ill-typed TFF
fof(geoff_vodka,conjecture,             ~ vodka(drink_of(geoff)) ).
fof(tasty_australian,conjecture,        ~ ? [X] : ( australian(X) & tasty(X) ) ).
fof(tasty_geoff,conjecture,             ~ tasty(geoff) ).
fof(tasty_drink_of_geoff,conjecture,    ~ tasty(drink_of(geoff)) ).
fof(geoff_rotgut,conjecture,            drink_of(geoff) != rotgut ).
fof(trueblue_andrei,conjecture,         ~ trueblue(andrei) ).
fof(geoff_andrei,conjecture,            geoff != andrei ).
fof(drink_of_andrei_russian,conjecture, drink_of(andrei) != geoff ).

A theorem to be proved:
For every FOF theorem proved from the strong translation of TFF type declarations and well-typed TFF axioms, there is a well-typed TFF theorem that translates to the FOF theorem.

Yikes, here's a FOF conjecture that can be proved in the strong translation, cannot be proved in the weak translation, and cannot be expressed in TFF.

fof(non_russian,conjecture,             ? [X] : ~ russian(X)).

The following sections summarize relatively well-known features and options of type systems
that we considered when putting this proposal together.

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 subtyping is used then types related by subtyping are necessarily non-disjoint. 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 > $o).
    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). If equations are permitted only between terms of the same type then a formula has a model with non-disjoint type domains iff it has a model with disjoint type domains. So, you can consider only models with disjoint type domains if you want. It makes no difference. (Thanks to Cesare Tinelli)
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. Here's an example that illustrates the knots that subtyping introduces ...
```
a: $i; f: fruit; ifun: $i -> $i; 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.

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 type-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.