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.
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.
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 excerpt 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).
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.
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:
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
`examples/arith/arith.thm'.
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:
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.
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.