Polymorphic Typed First-order Form

by Jasmin Blanchette, Andrei Paskevich, and others.

The TPTP untyped conjunctive normal form (CNF) and first-order form (FOF) are implemented in dozens of reasoning tools, and a growing number of reasoners can process the "core" typed first-order form (TFF0), which provides simple monomorphic types and interpreted arithmetic, or the corresponding higher-order form (THF0). A polymorphic version of THF0, the full THF, is in the works. Despite the variety of this offering, there is a strong desire in parts of the automated reasoning community for a polymorphic first-order format. Many applications require polymorphism, notably interactive theorem provers and program specification languages, but lacking a suitable interchange format these must communicate via monomorphic formats. Moreover, there is no entirely satisfactory way to eliminate polymorphism: Monomorphization is generally incomplete, and it is difficult to encode polymorphism in a sound, complete, and efficient manner, especially in the presence of interpreted types. Tool authors are reduced to developing their own monomorphizers and type encodings, often using suboptimal schemes. Ultimately, we contend that polymorphism belongs in provers, where it can be implemented simply and efficiently, as demonstrated by the SMT solver Alt-Ergo.

We aim to change this state of affairs by introducing the TFF1 format, an extension of TFF0 with rank-1 polymorphism. Syntactically, the types, terms, and formulas of TFF1 are analogous to those of TFF0, except that function and predicate symbols can be declared to be polymorphic, types can contain type variables, and n-ary type constructors are allowed. Type variables in type signatures and formulas are explicitly bound. Instances of polymorphic symbols are specified by explicit type arguments, rather than inferred.

Resources

Types

The types of TFF1 are built from type variables and type constructors of fixed arities. Nullary type constructors are called type constants. The usual conventions of TPTP apply: Type variables start with an uppercase letter and type constructors with a lowercase letter. A type is polymorphic if it contains type variables; otherwise, it is monomorphic.

As in TFF0, the type $i of individuals is predefined but has no peculiar semantics, whereas the arithmetic types $int, $rat, and $real are modeled by Z, Q, and R, respectively. Refer to the TFF0 specification for the semantics of the arithmetic types and their operations. It is perfectly acceptable for a TFF implementation not to support arithmetic. "TFFk with arithmetic" is sometimes called "TFAk".

Type Signatures

Each function and predicate symbol occurring in a formula must be associated with a type signature that specifies the types of the arguments and, for functions, the return type. Type signatures can take any of the following forms:
  1. a type (predefined or user-defined);
  2. the Boolean pseudotype $o;
  3. ($τ1$ * ... * $τn$) > $υ$ for n > 0, where τ1, ..., τn are types and υ is a type or $o;
  4. !>[α1 : $tType, ..., αn : $tType]: ς for n > 0, where α1, ..., αn are distinct type variables and ς has one of the previous three forms.
The parentheses in form (c) are omitted if n = 1. The binder !> in form (d) denotes universal quantification. If ς is of form (c), it must be put in parentheses.

Form (a) is used for monomorphic constants; form (b), for propositional constants, including the predefined symbols $true and $false; form (c), for monomorphic functions and predicates; and form (d), for polymorphic functions and predicates. It is often convenient to regard all forms above as instances of the general syntax

!>[α1 : $tType, ..., αm : $tType]: ((τ1 * ... * τn) > ς)
where m and n can be 0.

Type variables that are bound by !> without occurring in the type signature's body are called ghost type variables. These make it possible to specify operations and relations directly on types, providing a convenient way to encode type classes. For example, we can declare a polymorphic propositional constant is_linear with the signature !>[A : $tType]: $o and use it as a guard to restrict the axioms specifying that a binary predicate less_eq with the signature !>[A : $tType]: ((A * A) > $o) is a linear order to those types that satisfy the is_linear predicate.

Type Declarations

Type constructors, like function and predicate symbols, can optionally be declared. The following declarations introduce a type constant bird, a unary type constructor list, and a binary type constructor map: 
tff(bird_t, type, bird: $tType).
tff(list_t, type, list: $tType > $tType).
tff(map_t, type, map: ($tType * $tType) > $tType).
If a type constructor is used before being declared, its arity is determined by the first occurrence. Any later declaration must give it the same arity.

A declaration of a function or predicate symbol specifies its type signature. Every type variable occurring in a type signature must be bound by a !>-binder. The following declarations introduce a monomorphic constant pi, a polymorphic predicate is_empty, and a pair of polymorphic functions cons and lookup: 

tff(pi_t, type, pi: $real).
tff(is_empty_t, type, is_empty : !>[A : $tType]: (list(A) > $o)).
tff(cons_t, type, cons : !>[A : $tType]: ((A * list(A)) > list(A))).
tff(lookup_t, type, lookup : !>[A : $tType, B : $tType]: ((map(A, B) * A) > B)).
If a function or predicate symbol is used before being declared, a default type signature is assumed: ($i * ... * $i) > $i for functions and ($i * ... * $i) > $o for predicates. If a symbol is declared after its first use, the declared signature must agree with the assumed signature.

If a type constructor, function symbol, or predicate symbol is declared more than once, it must be given the same type signature up to renaming of bound type variables. All symbols share the same namespace; in particular, a type constructor cannot have the same name as a function or predicate symbol.

Function and Predicate Application

To keep the required type inference to a minimum, every use of a polymorphic symbol must explicitly specify the type instance. A function or predicate symbol with a type signature !>[$α1$ : $tType, ..., $αm$ : $tType]: (($τ1$ * ... * $τn$) > υ) must be applied to m type arguments and n term arguments. Given the above signatures for is_empty, cons, and lookup, the term lookup($int, list(A), M, 2) and the atom is_empty($i, cons($i, X, nil($i))) are well-formed and contain free occurrences of the type variable A and the term variable X, respectively.

In keeping with TFF1's rank-1 polymorphic nature, type variables can only be instantiated with actual types. In particular, $o, $tType, and !>-binders cannot occur in type arguments of polymorphic symbols.

For systems that implement type inference, the following nonstandard extension of TFF1 might be useful. When a type argument of a polymorphic symbol can be inferred automatically, it may be replaced with the wildcard $_. For example:

is_empty($_, cons($_, X, nil($_)))
Although nil's type argument cannot be inferred locally from the types of its term arguments (since there are none), the Hindley–Milner type inference can deduce it. The producer of a TFF1 problem must be aware of the type inference algorithm implemented in the consumer to omit only redundant type arguments.

Type and Term Variables

Every variable in a TFF1 formula must be bound. It can be given a type at binding time: 
tff(bird_list_not_empty, axiom,
    ![B : bird, Bs : list(bird)]: ~ is_empty(bird, cons(bird, B, Bs))).
If the type and the preceding colon (:) are omitted, the variable is given type $i. Every type variable occurring in a TFF1 formula (whether in a type argument or in the type of a bound variable) must also be bound, with the pseudotype $tType: 
tff(lookup_update_same, axiom,
    ![A : $tType, B : $tType, M : map(A, B), K : A, V : B]:
        lookup(A, B, update(A, B, M, K, V), K) = V).
A single quantifier cluster can bind both type variables and term variables. Universal and existential quantifiers over type variables are allowed under the propositional connectives, including equivalence, as well as under other quantifiers over type variables, but not in the scope of a quantifier over a term variable. Rationale: A statement of the form "for every integer k, there exists a type α such that ..." effectively makes α a dependent type. On such statements, type skolemization is impossible, and there is no easy translation to ML-style polymorphic formalisms. Moreover, type handling in an automatic prover would be more difficult were such constructions allowed, since they require paramodulation into types.

On the other hand, all the notions and procedures described in the TFF1 specification—except for type skolemization—are independent of this restriction. The rules of type checking and the notion of interpretation are directly applicable to unrestricted formulas. The encoding into a monomorphic is sound and complete on unrestricted formulas, and the proofs require no adjustments. This prepares the ground for TFF2, which is expected to lift the restriction and support more elaborate forms of dependent types. Implementations of TFF1 are encouraged to support unrestricted formulas, treating them according to the semantics given here, if practicable.

Terms and Formulas

Apart from the differences described above, the terms and formulas of TFF1 are identical to those of TFF0. Refer to the TFF0 specification for further information.

Example

The following problem gives the general flavor of TFF1. It first declares and axiomatizes lookup and update operations on maps, then conjectures that update is idempotent for fixed keys and values. Its SZS status is Theorem. 
tff(map_t,type,(
    map: ( $tType * $tType ) > $tType )).

tff(lookup_t,type,(
    lookup: 
      !>[A: $tType,B: $tType] :
        ( ( map(A,B) * A ) > B ) )).

tff(update_t,type,(
    update: 
      !>[A: $tType,B: $tType] :
        ( ( map(A,B) * A * B ) > map(A,B) ) )).

tff(lookup_update_same,axiom,(
    ! [A: $tType,B: $tType,M: map(A,B),K: A,V: B] : 
      lookup(A,B,update(A,B,M,K,V),K) = V )).

tff(lookup_update_diff,axiom,(
    ! [A: $tType,B: $tType,M: map(A,B),V: B,K: A,L: A] :
      ( K != L
     => lookup(A,B,update(A,B,M,K,V),L) = lookup(A,B,M,L) ) )).

tff(map_ext,axiom,(
    ! [A: $tType,B: $tType,M: map(A,B),N: map(A,B)] :
      ( ! [K: A] : lookup(A,B,M,K) = lookup(A,B,N,K)
     => M = N ) )).

tff(update_idem,conjecture,(
    ! [A: $tType,B: $tType,M: map(A,B),K: A,V: B] : 
      update(A,B,update(A,B,M,K,V),K,V) = update(A,B,M,K,V) )).

Type Checking and Semantics

Refer to the TFF1 specification for more details on type checking and semantics, and much more.