

8 Termination





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.


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


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


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).


%mode of +E *T.



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).


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)


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



%mode of +E *T.



(E x) < (lam E)



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




(A T) < (forall A)



8.4 Lexicographic Orders

Lexicographic orders are specified as

{O1 ... On}


v1 < w1, or
v1 = w1 and v2 < w2, or


8.5 Simultaneous Orders


Simultaneous orders are specified as

[O1 ... On]




8.6 Mutual Recursion



(X1 ... Xn)


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


