Extended Typed First-Order Form (TFX)

Changes to Typed Higher-order Form (THF)

by Geoff Sutcliffe, Evgeny Kotelnikov


Motivation

Since the inception of THF and TFF there have been some features that have received little use, and hence little attention. In particular, tuples, conditional expressions (if-then-else), and let expressions (let-defn-in) have been neglected. In TFF, conditional expressions and let expressions were horribly formulated, with variants to distinguish between their use with formulae and terms. Recently conditional expressions and let expressions have become more important because of their use in software verification applications.

In a separate development, Evgeny Kotelnikov et al. introduced the FOOL logic, which extends TFF so that (i) formulae can be used as terms with the type $o, (ii) variables of type $o can be used as formulae, (iii) tuple terms and tuple types are available as first-class citizens, and (iv) conditional and let expressions are supported. This logic can be automatically translated to first-order logic. It has is also useful in software verification applications.

This document describes a new TPTP language form - Typed First-order form eXtended (TFX), and changes to the THF language that correspond to decisions made for TFX.


Typed First-order form eXtended (TFX)

The Typed First-order form eXtended (TFX) language is a superset of the Typed First-order Form (TFF) language. TFX includes the FOOL logic. This has been achieved by conflating (with some exceptions) formulae and terms. As a result, the default typing of functions and predicates supported in TFF (functions default to ($i * ... * $i) > $i and predicates default to ($i * ... * $i) > $o) is not supported in TFX (as is the case for THF). Tuples have been simplified in TFF, and fully expressive tuples included in TFX. Conditional expressions and let expressions have been removed from TFF, and included in a more elegant form in TFX. (This more elegant form has been mirrored in THF, as described below.) Annotated formulae in TFX have tfx as their principle symbol.

Formulae as Terms
Formulae are permitted as terms. For example ...

    tfx(p_type,type,p: ($i * $o * $int) > $o ).
    tfx(q_type,type,q: ($int * $i) > $o ).
    tfx(me_type,type,me: $i ).
    tfx(fool_1,axiom,! [X: $int] : p(me,! [Y: $i] : q(X,Y),27) ).
... and ...
    tfx(p_type,type,p: $i > $o ).
    tfx(q_type,type,q: $o > $o ).
    tfx(me_type,type,me: $i ).
    tfx(fool_2,axiom,q((~p(me)) != q(me)) ).
Note that in TFX (as is the case for THF) negated formulae must be ()ed to accommodate their use as terms (even when they're not being used as terms).

Boolean Variables as Formulae
Variables of type $o can be used as formulae. For example ...

    tfx(implies_type,type,implies: ($o * $o) > $o).
    tfx(implies_defn,axiom, ! [X: $o,Y: $o]: (implies(X,Y) <=> ((~X) | Y)) ).

Tuple Terms
Tuples in TFF are written in [] brackets, and can contain non-boolean terms; tuples of formulae have been removed from TFF. Tuples in TFX are written in [] brackets, and can contain any type of term (including formulae and variables of type $o). Signatures can contain tuple types. For example ...

    tfx(t1_type,type,t1: $tType ).
    tfx(d_type,type,d: [$i,t1,$int] ).
    tfx(p_type,type,p: [t1,$i] > $o ).
    tfx(f_type,type,f: ($o * [$i,t1,$int]) > [t1,$i] ).
    tfx(tuples_2,axiom,p(f($true,d)) ).
Tuples can occur only as terms (not as formulae, and not on the lefthand side of a type declaration). Tuples can occur anywhere they are well-typed. For example ...
    tfx(p_type,type,p: ([$int,$i,$o] * $o * $int) > $o ).
    tfx(q_type,type,q: ($int * $i) > $o ).
    tfx(me_type,type,me: $i ).
    tfx(tuples_1,axiom,! [X: $int] : p([33,me,$true],! [Y: $i] : q(X,Y),27) ).
Tuples cannot be typed. Rather the elements must be typed separately. For example ...
    tfx(a_type,type,a: $int).
    tfx(b_type,type,b: $int).
    tfx(p_type,type,p: [$int,$int] > $o).
    tfx(p,axiom,p([a,b]).
... cannot be abbreviated to ...
    tfx(ab_type,type,[a,b]: [$int,$int]).
    tfx(p_type,type,p: [$int,$int] > $o).
    tfx(p,axiom,p([a,b]).

Conditional Expressions
Conditional expressions are parametric polymorphic, taking a formula as the first argument, then two terms or formulae of any one type as the second and third arguments, as the true and false return values respectively, i.e., the return type is the same as that of the second and third arguments. For example ...

    tfx(p_type,type,p: $int > $o).
    tfx(q_type,type,q: $int > $o).
    tfx(max_type,type,max: ($int * $int) > $int).
    tfx(ite_1,axiom,! [X:$int,Y:$int] : $ite($greater(X,Y),p(X),p(Y)) ).
    tfx(ite_2,axiom,! [X:$int,Y:$int] : q($ite($greater(X,Y),X,Y)) ).
    tfx(max_defn,axiom,! [X: $int,Y: $int]: (max(X,Y) = $ite($greatereq(X,Y),X,Y)) ).
    tfx(max_property,axiom,! [X: $int,Y: $int]: $ite(max(X,Y) = X,$greatereq(X,Y),$greatereq(Y,X)) ).
Tuples can be used usefully in conditional expressions. For example ...
    tfx(p_type,type,p: [$int,$int] > $o).
    tfx(d_type,type,d: [$int,$int]).
    tfx(ite_3,axiom,! [X:$int,Y:$int] : p($ite($greater(X,Y),[X,Y],[Y,X])) ).
    tfx(ite_4,axiom,! [X:$int,Y:$int] : (d = $ite($greater(X,Y),[X,Y],[Y,X])) ).

Let Expressions
Let expressions provide the types of defined symbols, definitions for the symbols, and a formula/term in which the definitions are applied. Each type declaration is the same as a type declaration in an annotated formula with the type role, and multiple type declarations are given in []ed tuples of declarations. Each definition defines the expansion of one of the declared symbols, and multiple definitions are given in []ed tuples of definitions. For example ...

    tfx(p_type,type,p: $int > $o ).
    tfx(let_1,axiom,$let(c: $int,c:= 27,p(c)) ).
... is equivalent to ...
    tfx(p_type,type,p: $int > $o ).
    tfx(let_1,axiom,p(27) ).
If variables are used in the lefthand side of a definition, their values are supplied in the defined symbol's use. Such variables do not need to be declared (they are implicitly declared to be of the type defined by the symbol declaration), but must be top-level arguments of the defined symbol and be pairwise distinct. For example ...
    tfx(i_type,type,i: $int).
    tfx(j_type,type,j: $int).
    tfx(f_type,type,f: ($int * $int * $int * $int) > $rat).
    tfx(p_type,type,p: $rat > $o ).
    tfx(let_2,axiom,$let(ff: ($int * $int) > $rat, ff(X,Y):= f(X,X,Y,Y), p(ff(i,j))) ).
... is equivalent to ...
    tfx(i_type,type,i: $int).
    tfx(j_type,type,j: $int).
    tfx(f_type,type,f: ($int * $int * $int * $int) > $rat).
    tfx(p_type,type,p: $rat > $o ).
    tfx(let_2,axiom,p(f(i,i,j,j)) ).
The defined symbols have scope over the formula/term in which the definitions are applied, shadowing any definition outside the let expression. The RHS of a definition can have symbols with the same name as the defined symbol, but refer to symbols defined outside the let expression. For example ...
    tfx(array_type,type,array: $int > $real).
    tfx(p_type,type,p: $real > $o).
    tfx(let_3,axiom,$let(array: $int > $real,array(I):= $ite(I = 3,5.2,array(I)),p($sum(array(2),array(3)))) ).
... is equivalent to ...
    tfx(array_type,type,array: $int > $real).
    tfx(p_type,type,p: $real > $o).
    tfx(let_3,axiom,p($sum(array(2),5.2)) ).
The occurrence of array in the a side of the definition array(I):=, and the occurrences in the formula in which the let expression is applied p($sum(array(2),array(3))), are the defined symbol. The occurrence in the righthand side of the definition $ite(I = 3,5,array(I)) is the globally defined symbol.

Tuples can be used to define multiple symbols in let expressions in parallel (not sequential, i.e., this is let, not let*). For example ...

    tfx(a_type,type,a: $int).
    tfx(b_type,type,b: $int).
    tfx(p_type,type,p: ($int * $int) > $o).
    tfx(let_tuple_1,axiom,$let([a: $int,b: $int],[a:= b,b:= a],p(a,b)) ).
... is equivalent to ...
    tfx(a_type,type,a: $int).
    tfx(b_type,type,b: $int).
    tfx(p_type,type,p: ($int * $int) > $o).
    tfx(let_tuple_1,axiom,p(b,a)).
... and ...
    tfx(i_type,type,i: $int).
    tfx(f_type,type,f: ($int * $int * $int * $int) > $int).
    tfx(p_type,type,p: $int > $o ).
    tfx(let_tuple_2,axiom,
        $let([ff: ($int * $int) > $int, gg: $int > $int],
             [ff(X,Y):= f(X,X,Y,Y), gg(Z):= f(Z,Z,Z,Z)],
             p(ff(i,gg(i)))) ).
... is equivalent to ...
    tfx(i_type,type,i: $int).
    tfx(f_type,type,f: ($int * $int * $int * $int) > $int).
    tfx(p_type,type,p: $int > $o ).
    tfx(let_tuple_2,axiom,p(f(i,i,f(i,i,i,i),f(i,i,i,i))) ).

As tuples cannot be typed ...

    tfx(p_type,type,p: ($int * $int) > $o).
    tfx(not_let_tuple,axiom,
        $let([a: $int,b: $int],[a:= b,b:= a],p(a,b)) ).
... cannot be abbreviated to ...
    tfx(p_type,type,p: ($int * $int) > $o).
    tfx(not_let_tuple,axiom,
        $let([a,b]: [$int,$int],[a:= b,b:= a],p(a,b)) ).

Sequential let expressions (let*) can be implemented by nesting. For example ...

    tfx(i_type,type,i: $int).
    tfx(f_type,type,f: ($int * $int * $int * $int) > $int).
    tfx(p_type,type,p: $int > $o ).
    tfx(let_tuple_3,axiom,
        $let(ff: ($int * $int) > $int,
             ff(X,Y):= f(X,X,Y,Y),
             $let(gg: $int > $int,gg(Z):= ff(Z,Z),p(gg(i)) ) ) ).
... is equivalent to ...
    tfx(i_type,type,i: $int).
    tfx(f_type,type,f: ($int * $int * $int * $int) > $int).
    tfx(p_type,type,p: $int > $o ).
    tfx(let_tuple_3,axiom,p(f(i,i,i,i)) ).

Tuples can be used directly in let expressions. For example ...

    tfx(p_type,type,p: ($int * $int) > $o ).
    tfx(q_type,type,q: [$int,$int] > $o ).
    tfx(let_tuple_4,axiom,$let([a:$int,b:$int], [a,b]:= [27,28], p(a,b)) ).
    tfx(let_tuple_5,axiom,$let(d: [$int,$int], d:= [27,28],q(d)) ).
... is equivalent to ...
    tfx(p_type,type,p: ($int * $int) > $o ).
    tfx(q_type,type,q: [$int,$int] > $o ).
    tfx(let_tuple_4,axiom,p(27,28)) ).
    tfx(let_tuple_5,axiom,q([27,28])) ).

Tuples, conditional expressions, and let expressions can be mixed in useful ways. For example ...

    tfx(cc_type,type,cc: $int).
    tfx(dd_type,type,dd: $int).
    tfx(let_ite_1,axiom,
        $let([aa: $int,bb: $$int],
             [aa,bb]:= $ite($greater(cc,dd),[cc,dd],[dd,cc]),
             p(aa,bb)) ).


Typed Higher-order Form (THF)

The Typed Higher-order Form (THF) has been updated with changes that correspond to the decisions made for TFX, so as to provide consistency across the TPTP languages.

Tuples
Tuples in THF are written in [] brackets, and can contain any type of expression. Signatures can contain tuple types. For example ...

    thf(t1_type,type,t1: $tType ).
    thf(d_type,type,d: [$i,t1,$int] ).
    thf(p_type,type,p: [t1,$i] > $o ).
    thf(f_type,type,f: $o > [$i,t1,$int] > [t1,$i] ).
    thf(tuples_1,axiom,p @ (f @ $true @ d ) ).
Tuples can occur anywhere they are well-typed. For example ...
    thf(p_type,type,p: [$int,$i,$o] > $o > $int > $o ).
    thf(q_type,type,q: $int > $i > $o ).
    thf(r_type,type,r: $int > $o).
    thf(me_type,type,me: $i ).
    thf(tuples_2,axiom,r = ^ [X: $int] : (p @ [33,me,$true] @ (q @ 27 @ me)) ).
Tuples cannot be typed. Rather the elements must be typed separately. For example ...
    thf(a_type,type,a: $int).
    thf(b_type,type,b: $int).
    thf(p_type,type,p: [$int,$int] > $o).
    thf(p,axiom,p([a,b]).
... cannot be abbreviated to ...
    thf(ab_type,type,[a,b]: [$int,$int]).
    thf(p_type,type,p: [$int,$int] > $o).
    thf(p,axiom,p([a,b]).

Conditional Expressions
Conditional expressions are parametric polymorphic, taking a boolean expression as the first argument, then two expressions of any one type as the second and third arguments, as the true and return values respectively, i.e., the return type is the same as that of the second and third arguments. For example ...

    thf(p_type,type,p: $int > $o).
    thf(q_type,type,q: $int > $o).
    thf(max_type,type,max: $int > $int > $int).
    thf(ite_1,axiom,! [X:$int,Y:$int] : $ite($greater @ X @ Y,p @ X,p @ Y) ).
    thf(ite_2,axiom,! [X:$int,Y:$int] : ( q @ $ite($greater @ X @ Y,X,Y)) ).
    thf(max_defn,axiom,! [X: $int,Y: $int]: ((max @ X @ Y) = $ite($greatereq @ X @ Y,X,Y)) ).
    thf(max_property,axiom,! [X: $int,Y: $int]: $ite((max @ X @ Y) = X,$greatereq @ X @ Y,$greatereq @ Y @ X)).
Tuples can be used usefully in conditional expressions. For example ...
    thf(p_type,type,p: [$int,$int] > $o).
    thf(d_type,type,d: [$int,$int]).
    thf(ite_3,axiom,! [X:$int,Y:$int] : (p @ $ite($greater @ X @ Y,[X,Y],[Y,X])) ).
    thf(ite_4,axiom,! [X:$int,Y:$int] : (d = $ite($greater @ X @ Y,[X,Y],[Y,X])) ).

Let Expressions
Let expressions provide the types of defined symbols, definitions for the symbols, and an expression in which the definitions are applied. Each type declaration is the same as a type declaration in an annotated formula with the type role, and multiple type declarations are given in []ed tuples of declarations. Each definition defines the expansion of one of the declared symbols, and multiple definitions are given in []ed tuples of definitions. For example ...

    thf(p_type,type,p: $int > $o ).
    thf(let_1,axiom,$let(c: $int,c:= 27,p @ c)).
... is equivalent to ...
    thf(p_type,type,p: $int > $o ).
    thf(let_1,axiom,p @ 27 ).
If variables are used in the a side of the definition, their values are supplied in the the defined symbol's use. Such variables do not need to be declared (they are implicitly declared to be of the type defgined by the symbol declaration), but must be top-level arguments of the defined symbol and be pairwise distinct. For example ...
    thf(i_type,type,i: $int).
    thf(j_type,type,j: $int).
    thf(f_type,type,f: $int > $int > $int > $int > $rat).
    thf(p_type,type,p: $rat > $o ).
    thf(let_2,axiom,$let(ff: $int > $int > $rat, ff @ X @ Y:= f @ X @ X @ Y @ Y, p @ (ff @ i @ j)) ).
... is equivalent to ...
    thf(i_type,type,i: $int).
    thf(j_type,type,j: $int).
    thf(f_type,type,f: $int > $int > $int > $int > $rat).
    thf(p_type,type,p: $rat > $o ).
    thf(let_2,axiom,p @ (f @ i @ i @ j @ j) ).

An alternative use is with lambda expressions. For example ...

    thf(i_type,type,i: $int).
    thf(j_type,type,j: $int).
    thf(f_type,type,f: $int > $int > $int > $int > $rat).
    thf(p_type,type,p: $rat > $o ).
    thf(let_2,axiom,$let(ff: $int > $int > $rat, ff := ^ [X: $int,Y: $int] : (f @ X @ X @ Y @ Y), p @ (ff @ i @ j)) ).
... is equivalent to ...
    thf(i_type,type,i: $int).
    thf(j_type,type,j: $int).
    thf(f_type,type,f: $int > $int > $int > $int > $rat).
    thf(p_type,type,p: $rat > $o ).
    thf(let_2,axiom,p @ (f @ i @ i @ j @ j) ).
The defined symbols have scope over the formula/term in which the definitions are applied, shadowing any definition outside the let expression. The RHS of a definition can have symbols with the same name as the defined symbol, but refer to symbols defined outside the let expression. For example ...
    thf(array_type,type,array: $int > $real).
    thf(p_type,type,p: $real > $o).
    thf(let_3,axiom,$let(array: $int > $real,array @ I:= $ite(I = 3,5.2,array @ I),p @ ($sum @ (array @ 2) @ (array @ 3))) ).
... is equivalent to ...
    thf(array_type,type,array: $int > $real).
    thf(p_type,type,p: $real > $o).
    thf(let_3,axiom,p @ ($sum @ (array @ 2) @ 5.2) ).
The occurrence of array in the lefthand side of a definition array @ I:=, and the occurrences in the formula in which the let expression is applied p @ ($sum @ (array @ 2) @ (array @ 3)), are the defined symbol. The occurrence in the righthand side of the definition $ite(I = 3,5.2,array @ I) is the globally defined symbol.

Tuples can be used to define multiple symbols in let expressions in parallel (not sequential, i.e., this is let, not let*). For example ...

    thf(a_type,type,a: $int).
    thf(b_type,type,b: $int).
    thf(p_type,type,p: $int > $int > $o).
    thf(let_tuple_1,axiom,$let([a: $int,b: $int],[a:= b,b:= a],p @ a @ b)).
... is equivalent to ...
    thf(a_type,type,a: $int).
    thf(b_type,type,b: $int).
    thf(p_type,type,p: $int > $int > $o).
    thf(let_tuple_1,axiom,p @ b @ a).
... and ...
    thf(i_type,type,i: $int).
    thf(f_type,type,f: $int > $int > $int > $int > $int).
    thf(p_type,type,p: $int > $o ).
    thf(let_tuple_2,axiom,
        $let([ff: $int > $int > $int, gg: $int > $int],
             [ff @ X @ Y:= f @ X @ X @ Y @ Y, gg @ Z:= f @ Z @ Z @ Z @ Z],
             p @ (ff @ i @ ( gg @ i))) ).
... is equivalent to ...
    thf(i_type,type,i: $int).
    thf(f_type,type,f: $int > $int > $int > $int > $int).
    thf(p_type,type,p: $int > $o ).
    thf(let_tuple_2,axiom,p @ (f @ i @ i @ (f @ i @ i @ i @ i) @ (f @ i @ i @ i @ i)) ).

As tuples cannot be typed ...

    thf(p_type,type,p: $int >  $int > $o).
    thf(not_let_tuple,axiom,
        $let([a: $int,b: $int],[a:= b,b:= a],p @ a @ b) ).
... cannot be abbreviated to ...
    thf(p_type,type,p: $int >  $int > $o).
    thf(not_let_tuple,axiom,
        $let([a,b]: [$int,$int],[a:= b,b:= a],p @ a @ b) ).
Sequential let expressions (let*) can be implemented by nesting. For example ...
    thf(i_type,type,i: $int).
    thf(f_type,type,f: $int > $int > $int > $int > $int).
    thf(p_type,type,p: $int > $o ).
    thf(let_tuple_3,axiom,
        $let(ff: $int > $int > $int,
             ff @ X @ Y:= f @ X @ X @ Y @ Y,
             $let(gg: $int > $int,gg @ Z:= ff @ Z @ Z,p @ (gg @ i)) ) ).
... is equivalent to ...
    thf(i_type,type,i: $int).
    tfh(f_type,type,f: $int > $int > $int > $int > $int).
    thf(p_type,type,p: $int > $o ).
    thf(let_tuple_3,axiom,p @ (f @ i @ i @ i @ i) ).

Tuples can be used directly in let expressions. For example ...

    thf(p_type,type,p: $int > $int > $o ).
    thf(q_type,type,q: [$int,$int] > $o ).
    thf(let_tuple_4,axiom,$let([a:$int,b:$int], [a,b]:= [27,28], p @ a @ b) ).
    thf(let_tuple_5,axiom,$let(d: [$int,$int], d:= [27,28],q @ d) ).
... is equivalent to ...
    thf(p_type,type,p: $int > $int > $o ).
    thf(q_type,type,q: [$int,$int] > $o ).
    thf(let_tuple_4,axiom,p @ 27 @ 28) ).
    thf(let_tuple_5,axiom,q @ [27,28]) ).

Tuples, conditional expressions, and let expressions can be mixed in useful ways. For example ...

    thf(cc_type,type,cc: $int).
    thf(dd_type,type,dd: $int).
    thf(let_ite_1,axiom,
        $let([aa: $int,bb: $$int],
             [aa,bb]:= $ite($greater @ cc @ dd,[cc,dd],[dd,cc]),
             p @ aa @ bb) ).