Dependently Typed Higher-Order Logic

by Cezary Kaliszyk, Daniel Ranalter, Geoff Sutcliffe.

Dependently typed higher-order logic (DHOL) is a extension of Church's higher-order logic (HOL) introduced by Rothgang et al. [RRB23]. It takes the widely supported HOL and equips it with dependent types, i.e., types that take term arguments. As such, it is a classical and extensional type theory, as opposed to the theory used in Rocq, Lean or others which rely on an intensional type theory. Notable exceptions to this trend are PVS and F*. While the extensionality of DHOL comes at the cost of making type checking an undecidable problem in general, the gain is also significant: Having judgmental and provable equality coincide is much closer to how mathematics is usually done in the context of Automated Theorem Proving. Furthermore, the cost - which might seem steep at first glance - is mitigated by the ever increasing performance of ATP systems and the fact that in many cases the proof obligations resulting from type checking are simpler than the original conjecture. The inclusion of dependent types into the formalism allows the elegant definition of data structures like lists with fixed length, sets of a fixed finite size and others. Having constraints encoded on the level of types removes the need for lengthy and error prone guards in programming, and encodes additional, useful information for theorem proving. Types in DHOL are either fully applied base types, dependent function types, or classical booleans. A remark about the binary connectives: Due to type checking, binary connectives like AND and OR are no longer commutative. Consider as an example the statement a =A b ⇒ f a =B(a) f b. The well-formedness of the right-hand side requires the left hand side as premise, which breaks commutativity for the boolean connectives defined with ⇒. While apparently disruptive, it is common practice to sacrifice commutativity for, e.g., short-circuit evaluation of boolean terms in programming languages.

Translation of DHOL

In order to take advantage of the proving power already available for regular HOL, Rothgang et al. define a dependency-erasure and thereby a translation from DHOL into regular HOL. They also prove that this translation is sound and complete for well-typed DHOL problems. Due to this result, and the implementation of the translation in the preprocessor of the Leo-III theorem prover, there existed reasoning support for DHOL, even before native DHOL reasoning was implemented into Lash by Niederhauser et al. [NBK24]. Information lost due to the erasure of term dependencies is captured in Partial Equivalence Relations (PERs) - symmetric and transitive relations on pairs of terms - with the idea that the relation is reflexive exactly for those terms that were previously of the same dependent type. While intuitively one might think unary predicates would be sufficient to specify subtypes for type guards, a binary equality relation becomes necessary when relating higher-order functions which are equal when guarded inputs are mapped to equal outputs.

Type Checking

Due to equality reflection, type checking for DHOL is in general undecidable. Nevertheless, problems need to be well-typed, not least of all because otherwise the translation outlined previously would not necessarily be sound. As such, type checking takes up a larger role compared to other logics in the TPTP. While performing the usual type checking procedure in DHOL, one eventually encounters obligations of the form a t1 ... tn ≡ b u1 ... un, establishing equality of the dependent types a, b of arity n with t1 ... tn , u1 ... un being terms of appropriate type. At this point the type equality judgment is reflected into proving obligations, each establishing the equality of the corresponding term arguments. In cases where ti, ui are equal, the obligation can be dismissed directly by reflectivity. In general, however, this creates a number of new conjectures that need to be addressed by the theorem prover. This sometimes creates interesting situations, where problems need to include axioms not directly necessary for the conjecture itself, but for type checking the problem. The common example of fixed length lists is one such instance. Proving the associativity of append requires the inclusion of the defining equations of append as well as cons. To type check the problems it is additionally necessary to include axioms and defining equations that allow proving the associativity of addition on natural numbers.

The undecidability of type checking does incite finding compromises. One such compromise is "shallow type checking". When a problem file is shallowly checked, only the simply typed skeleton of the problem is considered, i.e., term arguments to types as well as dependent functions are ignored during the procedure. Consequently, it collapses to type checking as is done on non-dependently typed problems, and is decidable.

This form of type checking catches careless mistakes in the formulation of problems and provides a very basic check of issues usually caught in HOL problems. Matching the number of arguments to the arity of a function, and egregious type mismatches, are examples of errors that can be avoided by shallow type checking. This provides a valuable sanity check for users, especially considering the complexity that problems in DHOL forms can reach.

Syntax of TPTP Dependently Typed Higher-order Form (DHF)

The syntax of DHF requires next to no change to the already established TPTP language BNF. The TPTP language already defines the !> binder for types. This is currently only used for polymorphism e.g., cons : !>[A: $tType]: (A > (list @ A) > (list @  A)) might be found as the type statement for a polymorphic cons operation. However, the TPTP language does not forbid to list terms in the types of such variable lists. This fact is used to unobtrusively extend TPTP with dependent types. A dependent type symbol declaration is written with m terms of n types as a: !>[x1:A1,...,xm:An] : $tType, or alternatively a: A1 > ... > An > $tType.  Instantiations of such types use the application operator @, applying the terms to the dependent type: a @ t1 @ ... @ tm. In polymorphic problems the variable list is prepended with their type variables, which may appear in the same binder.

An Example Problem in DHF

The following example formalizes the base case of the inductive proof that append on fixed-length lists is associative. 
%------------------------------------------------------------------------------
%----The theory of natural numbers. Well-established and simply typed.
thf(nat_type,type,
    nat: $tType ).

thf(zero_type,type,
    zero: nat ).

thf(suc_type,type,
    suc: nat > nat ).

thf(plus_type,type,
    plus: nat > nat > nat ).

thf(ax1,axiom,
    ! [N: nat] :
      ( ( plus @ zero @ N ) = N ) ).

%----The second defining equation for 'plus' is not necessary in the base case.
%----The associativity of plus is needed for type checking (and, in fact, only
%----for type checking)
thf(plus_assoc,axiom,
    ! [M1: nat,M2: nat,M3: nat] :
      ( ( plus @ M1 @ ( plus @ M2 @ M3 ) )
      = ( plus @ ( plus @ M1 @ M2 ) @ M3 ) ) ).

%----A type of arbitrary elements for our list.
thf(elem_type,type,
    elem: $tType ).

%----Dependent types: the list type takes a nat typed term and returns a type
thf(list_type,type,
    list: nat > $tType ).

%----'nil', the empty list, is specified to have length 0, encoding properties
%----into types that would otherwise need definitions of a length function,
%----additional axioms, etc.
thf(nil_type,type,
    nil: list @ zero ).

%----The 'cons' operator is dependently typed, taking a nat corresponding to
%----the length of the input vector. Note that this prevents any conjecture
%----from trying to establish nil' as a result of cons, as this wouldn't
%----type-check.
thf(cons_type,type,
    cons:
      !>[N: nat] : ( elem > ( list @ N ) > ( list @ ( suc @ N ) ) ) ).

%----'app' is also dependent, incorporating reasoning about plus into the type
%----checking procedure.
thf(app_type,type,
    app:
      !>[N: nat,M: nat] : 
        ( ( list @ N ) > ( list @ M ) > ( list @ ( plus @ N @ M ) ) ) ).

%----First (and for this conjecture, the only) defining equation of 'app'
thf(ax3,axiom,
    ! [N: nat,X: list @ N] :
      ( ( app @ zero @ N @ nil @ X ) = X ) ).

%----The conjecture: The base case of the induction proof. Note that this is
%----part of a larger problem, broken up to make it easier.
thf(list_app_assoc_base,conjecture,
    ! [M2: nat,L2: list @ M2,M3: nat,L3: list @ M3] :
      ( ( app @ zero @ ( plus @ M2 @ M3 ) @ nil @ ( app @ M2 @ M3 @ L2 @ L3 ) )
      = ( app @ ( plus @ zero @ M2 ) @ M3 @ ( app @ zero @ M2 @ nil @ L2 ) @ L3 ) ) ).
%------------------------------------------------------------------------------

Problems

ATP Systems and Tools