Go to the first, previous, next, last section, table of contents.

8 Termination

Besides checking types and modes, Twelf can also verify if a given type family, when interpreted as a logic program, always terminates on well-moded goals. In many cases this means that the program implements a decision procedure. Of course, in general termination is undecidable, so we only check a simple sufficient condition.

Checking termination presupposes that the program is well-typed and guarantees termination only when the arguments involved in the termination order are ground. This will always be true for well-moded goals, since mode and termination declarations must be consistent.

Termination is different from checking types and modes in that it is not checked incrementally as the signature is read. Instead, termination of a predicate is a global property of the program once it has been read. Thus termination declarations came after the predicate has been fully defined; further extensions of the predicate are not checked and may invalidate termination.

The termination checker is rather rudimentary in that it only allows lexicographic and simultaneous extensions of the subterm ordering. Moreover, it does not take into account if a result returned by a predicate is smaller than an input argument. Nonetheless, for the style of programs written in Twelf, the termination of many decision procedures can be verified.

8.1 Termination Declaration

The termination orders we construct are lexicographic or simultaneous extensions of the subterm ordering explained in section 8.3 Subterm Ordering. The termination declaration associates the termination order with argument positions of predicates via call patterns.

The case of mutually recursive predicates is particularly complex and requires mutual call patterns and mutual arguments. Their syntax is given below; they are explained in section 8.6 Mutual Recursion.

args ::=
       | id args       % named argument
       | _ args        % anonymous argument

callpat ::= id args    % a x1 ... xn

callpats ::= 
           | (callpat) callpats
                       % mutual call patterns

ids ::=
      | id ids         % argument name

marg ::= id            % single argument
       | ( ids )       % mutual arguments

orders ::=
         | order orders % component order

order ::= marg         % subterm order
        | { orders }   % lexicographic order
        | [ orders ]   % simultaneous order

tdecl ::= order callpats    % termination order

decl ::= ...
       | %terminates tdecl. % termination declaration

All identifiers in the order specification of a termination declaration must be upper case, must occur in the call patterns, and no variable may be repeated. Furthermore, all arguments participating in the termination order must occur in the call patterns in input positions.

The most frequent form of termination declaration is

%terminates Xi (a X1 ... Xn).

which expresses that predicate a terminates because recursive calls decrease the input argument Xi according to the subterm ordering (see section 8.3 Subterm Ordering).

As an example, we consider a proof that simple type inference (see section 5.6 Sample Program) terminates. Recall the relevant program fragment (see `examples/guide/lam.elf').

of : exp -> tp -> type.                 %name of P.
%mode of +E *T.

tp_lam : of (lam E) (arrow T1 T2)       % |- lam x. E : T1 => T2
          <- ({x:exp}                   % if  x:T1 |- E : T2.
                of x T1 -> of (E x) T2).

tp_app : of (app E1 E2) T1              % |- E1 E2 : T1
          <- of E1 (arrow T2 T1)        % if  |- E1 : T2 => T1
          <- of E2 T2.                  % and |- E2 : T2.

The typability of an expression is always reduced to the typability of its subexpressions. Therefore any call to the of predicate with a ground expression should terminate. In general, termination can only be checked for input arguments, and all calls must be well-moded (see section 7.3 Mode Checking). Twelf verifies termination with the declaration

%terminates E (of E T).

Here, E specifies the decreasing argument, namely the first argument of the typing judgment as expressed in the call pattern (of E T).

A corresponding attempt to show that evaluation always terminates,

%terminates E (eval E V).

fails for the clause ev_app with the message

examples/guide/lam.elf:1053-1068 Error:
Termination violation:
(E1' V2) < (app E1 E2)

indicating that in a recursive call the term E1' V2 could not be shown to be smaller than app E1 E2. In our example, of course, evaluation need not terminate for precisely this reason.

Termination checking plays a crucial role in checking meta-programs. The meta-program represents a proof that some relation about programs holds. The recursive calls in the meta-program correspond to applications of the induction hypothesis in the proof. Termination checking of meta-programs corresponds to checking that the application of the induction hypothesis is valid, i.e. we apply the induction hypothesis to a smaller argument.

8.2 Reduction Declaration

A reduction predicate specifies a relation between input and output arguments of a program. The reduction checker is rather restrictive and allows only relations based on subterm ordering. For example, we cannot reason about the length of a list or term. Moreover, reduction checking presupposes that the right side of the reduction predicate corresponds to the input arguments and the left side of the predicate corresponds to the output arguments. The declaration %reduces checks if the specified reduction predicate holds for a given program. To check whether the predicate also terminates, one needs to check termination of the predicate separately. The syntax for order can be found in section 8 Termination.

pdecl ::= order < order     % strictly smaller than
        | order <= order    % smaller or equal than
        | order = order     % equal

rdecl ::= pdecl callpats    % reduction predicate

decl ::= ...
       | %reduces rdecl.    % reduction declaration

A pdecl requires that both orders specified are of the same variety. For example, if one is lexicographic, the other one must be as well.

For example,

%reduces Z <= X (minus X Y Z).

expects X to be the input and Z to be the output of the goal (minus X Y Z). The declaration checks whether the output argument Z is smaller than the input argument X, and if the program terminates in X.

As a simple example of reduction checking we consider the greatest common divisor. This is an exceprt from the signature for unary arithmetic in the file `example/guide/arith.elf'.

gcd: nat -> nat -> nat -> type.          %name gcd G. 
%mode gcd +X +Y -Z. 

gcd_z1: gcd z Y Y. 
gcd_z2: gcd X z X. 

gcd_s1: gcd (s X) (s Y) Z 
  <- less (s X) (s Y) true 
  <- rminus (s Y) (s X) Y' 
  <- gcd (s X) Y' Z. 

gcd_s1: gcd (s X) (s Y) Z 
  <- less  (s X)(s Y) false 
  <- rminus (s X) (s Y) X' 
  <- gcd X' (s Y)  Z. 

rminus: nat -> nat -> nat -> type.        %name rminus M. 
%mode rminus +X +Y -Z. 
rmin : rminus (s X) (s Y) Z 
 <- sub X Y Z. 

%reduces Z < X (rminus X Y Z). 
%terminates [X Y] (gcd X Y _). 

In order to verify that the definition of gcd terminates, we need to show that the arguments in the recursive call are decreasing, i.e. we need to show Y' < (s Y) and X' < (s X). To check that these properties hold, we need the fact that the output argument Y' of rminus (s Y) (s X) Y' is always smaller than the input argument (s Y) (i.e. rminus (s Y) (s X) Y' always satisfies the reduction predicate Y' < (s Y)). We verify that rminus (s Y) (s X) Y' always reduces its output argument by checking the declaration %reduces Z < X (rminus X Y Z). While checking termination of gcd we use this information and prove Y' < (s Y) (termination condition of gcd) under the assumption Y' < (s Y) (reduction predicate of rminus).

8.3 Subterm Ordering

On first-order terms, that is, terms not containing lambda-abstraction, the subterm ordering is familiar: M < N if M is a strict subterm of N, that is, M is a subterm N and M is different from N.

On higher-order terms, the relation is slightly more complicated because we must allow the substitution of parameters for bound variables without destroying the subterm relation. Consider, for example, the case of the typing rule

of : exp -> tp -> type.                 %name of P.
%mode of +E *T.

tp_lam : of (lam E) (arrow T1 T2)       % |- lam x. E : T1 => T2
          <- ({x:exp}                   % if  x:T1 |- E : T2.
                of x T1 -> of (E x) T2).

from the signature for type inference (see section 5.6 Sample Program) in the file `example/guide/lam.elf'. We must recognize that

(E x) < (lam E)

according to the subterm ordering. This is because E stands for a term [y:exp] E' and so E x has the same structure as E' except that y (a bound variable) has been replaced by x (a parameter). This kind of pattern arises frequently in Twelf programs.

On the other hand, the restriction to parameter arguments of functions is critical. For example, the lax rule

tp_applam : of (app (lam E1) E2) T2
             <- of (E1 E2) T2.

which applies E1 to E2 which is not a parameter, is indeed not terminating. This can be seen from the query

?- of (app (lam [x:exp] app x x) (lam [y:exp] app y y)) T.

The restriction of the arguments to parameters can be lifted when the type of the argument is not mutually recursive with the result type of the function. For example, the signature for natural deduction (see section 3.6 Sample Signature, contains no constructor which allows propositions to occur inside individual terms. Therefore

(A T) < (forall A)

where A : i -> o and T : i is an arbitrary term (not just a parameter). Intuitively, this is correct because the number of quantifiers and logical connectives is smaller on the left, since T cannot contain such quantifiers or connectives.

This kind of precise analysis is important, for example, in the proof of cut elimination or the termination of polymorphic type reconstruction.

8.4 Lexicographic Orders

Lexicographic orders are specified as

{O1 ... On}

Using vi and wi for corresponding argument structures whose order is already defined, we compare them lexicographically as follows:

{v1 ... vn} < {w1 ... wn}, if
v1 < w1, or
v1 = w1 and v2 < w2, or
v1 = w1, v2 = w2, ..., and vn < wn.

A lexicographic order is needed, for example, to show termination of Ackermann's function, defined in `examples/arith/arith.elf' with the termination declaration in

8.5 Simultaneous Orders

Simultaneous orders require that one of its elements decreases while all others remain the same. This is strictly weaker than a lexicographic ordering built from the same components. Technically speaking it is therefore is redundant for termination checking, since the corresponding lexicographic ordering could be used instead. However, for inductive theorem proving it is quite useful, since the search space for simultaneous induction is much smaller than for lexicographic induction.

Simultaneous orders are specified as

[O1 ... On]

Using vi and wi for corresponding argument structures whose order is already defined, we compare them simultaneously as follows:

[v1 ... vn] < [w1 ... wn], if
v1 < w1, v2 <= w2, ..., and vn <= wn, or
v1 <= w1, v2 < w2, ..., and vn <= wn, or
v1 <= w1, v2 <= w2, ..., and vn < wn.

A combination of simultaneous and lexicographic order is used, for example, in the admissibility of cut found in `examples/cut-elim/int.thm', where either the cut formula A gets smaller, or if A stays the same, either the derivation of the left or right premise get smaller while the other stays the same.

8.6 Mutual Recursion

Mutually recursive predicates present a challenge to termination checking, since decreasing arguments might appear in different positions. Moreover, mutually recursive predicates a and a' might be prioritized so that when a calls a' all termination arguments remain the same, but when a' calls a the arguments are smaller according to the termination order.

To handle the association of related argument in mutually recursive predicates, so-called mutual arguments can be specified in a termination order. They are given as

(X1 ... Xn)

The priority between predicates is indicated by the order of the call patterns. If we analyze call patterns

(a1 args1)
(a2 args2)
(an argsn)

then ai may call aj for i < j with equal termination arguments, but calls of ai from aj must decrease the termination order.

Mutual arguments are used, for example, in the proofs of soundness (file
`examples/lp-horn/uni-sound.thm') and completeness (file
`examples/lp-horn/uni-complete.thm') of uniform derivations for Horn logic.

Go to the first, previous, next, last section, table of contents.