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.
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".
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.
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.tff(bird_t, type, bird: $tType). tff(list_t, type, list: $tType > $tType). tff(map_t, type, map: ($tType * $tType) > $tType).
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:
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.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 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.
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.
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(bird_list_not_empty, axiom, ![B : bird, Bs : list(bird)]: ~ is_empty(bird, cons(bird, B, Bs))).
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.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).
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.
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) )).