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 gthere 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 introduced the FOOL logic, which extends TFF to allow boolean terms. 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, i.e., boolean terms are allowed. This has been achieved by conflating (with some exceptions) formulae and terms. 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.

Boolean 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,p: $o > $o ).
    tfx(me_type,type,me: $i ).
    tfx(fool_2,axiom,q((~p(me)) != q(me))).
Note that the ~p(me) needs to be ()ed AND I NEED TO SAY WHY.

Tuples
Tuples in TFF are written in [] brackets, and can contain only non-boolean terms; tuples of formulae have been removed from TFF. Tuples in TFX are also written in [] brackets, and can contain any type of term. Tuples are of type $i. For example ...

    tfx(p_type,type,p: ($i * $o * $int) > $o ).
    tfx(f_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) ).
Signatures can contain tuple types. For example ...
    tfx(t1_type,type,t1: $tType ).
    tfx(p_type,type,p: [t1,$i] > $o ).
    tfx(d_type,type,d: [$i,t1,$int] ).
    tfx(f_type,type,f: ($o * $i) > [t1,$i] ).
    tfx(tuples_2,axiom,p(f($true,d)) ).
... and ...
    tfx(a_b_type,type,[a,b]: [$int,$int] ).
    tfx(c_d_type,type,[c,d]: [$int,$int] ).
    tfx(tuples_3,axiom,[a,b] = [c,d] ).

Conditional Expressions
Conditional expressions are adhoc polymorphic, taking a formula as the first argument, then two terms (of any one type) or two formulae as the second and third arguments as the return values, 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(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)) ).
Tuples can be used 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 expression provide the type of the defined symbols, definitions for the symbols, and a formula/term (of any type) in which the let expression applies. For example ...

    tfx(p_type,type,p: $int > $o ).
    tfx(let_1,axiom,$let(c: $int,c:= 27,p(c))).
... would be equivalent to ...
    tfx(let_1,axiom,p(27) ).
The defined symbols and have scope over the formula/term in which the let expression applies, 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. Jeff wants that, but it's messy. Should we do that?

If variables are used in the definition, their values are supplied in the the defined symbol's use. Such variables do not need to be declared, 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) > $int).
    tfx(p_type,type,p: $int > $o ).
    tfx(let_2,axiom,$let(ff: ($int * $int) > $rat, ff(X,Y):= f(X,X,Y,Y), p(ff(i,j))) ).
... would be equivalent to ...
    tfx(let_2,axiom,p(f(i,i,j,j)) ).
Tuples can be used to define multiple symbols in let expressions. 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_1,axiom,
        $let([ff: ($int * $int) > $rat, gg: $int > $int],
             [ff(X,Y):= f(X,X,Y,Y), gg(Z):= f(Z,Z,Z,Z)],
             p(ff(i,gg(i)))) ).
... would be equivalent to ...
    tfx(let_tuple_1,axiom,p(f(i,i,f(i,i,i,i),f(i,i,i,i))) ).
Question: should we make it let or let*?

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_2,axiom,$let([a:$int,b:$int], [a,b]:= [27,28], p(a,b)) ).
    tfx(let_tuple_3,axiom,$let(d: [$int,$int], d:= [27,28],q(d)) ).
... would be equivalent to ...
    tfx(let_tuple_2,axiom,p(27,28)) ).
    tfx(let_tuple_3,axiom,q([27,28])) ).
An alternative equivalent version of let_tuple_2 would be ...
    tfx(let_tuple_2,axiom,$let([a,b]: [$int,$int], [a,b]:= [27,28], p(a,b)) ).
Really, should we allow that?

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

    tfx(let_ite_1,axiom,
        $let([aa: $int,bb: $$int],
             [aa,bb]:= $ite($greater(aa,bb),[aa,bb],[bb,aa]),
             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. Tuples are of type $i. For example ...

    thf(p_type,type,p: $int > $o ).
    thf(q_type,type,q: [$int,$int] > $i > $o ).
    thf(me_type,type,me: $i ).
    thf(tuples_1,axiom,p = ^ [Z: $int] : ( q @ [Z,Z] @ me ) ).
Signatures can contain tuple types. For example ...
    thf(t1_type,type,t1: $tType ).
    thf(p_type,type,p: [t1,$i] > $o ).
    thf(f_type,type,f: $o > $i > [t1,$i] ).
    thf(me_type,type,me: $i ).
    thf(tuples_2,axiom,p @ (f @ $true @ me ) ).

Conditional Expressions

Let Expressions