Documentation out of dateLearn more

%terminates

A %terminates declaration checks that a program will either succeed or fail in a finite amount of time when given ground inputs.

A %total declaration uses the same syntax as a %terminates declaration.

Termination checking in STELF

Termination is in general an undecidable problem, and so STELF uses a simple strategy of requiring the user to define some termination ordering, and then checking that every recursive subgoal makes that ordering smaller.

STELF considers a term to be smaller than another term if it can inspect the two terms to see that the first is a strict subterm or if it follows from a %reduces declaration that the first is smaller. STELF also uses mode information to ensure that it is reasoning about ground terms.

A term A is only considered to be smaller than B if A is a strict subterm of B. So, for instance, (s (s z)), (s z), and z are all subterms of (f (s (s z)) (s z)), but (f z z) is not.

As usual, we will use the natural numbers as the basis for our example.

%sort nat %.
%term z nat %.
%term s %pi nat %-> nat %.

Non-ordering

The simplest termination ordering says that no termination argument is needed, because there are no recursive calls! We can write such an ordering for triv, which takes a number and can either return a number one greater or one less.

%sort triv {_ nat} {_ nat} %.
%mode triv %in %out %.
%term triv/ triv (s N) N %.
%term triv/ triv N (s N) %.

%terminates {} (triv _ _).

Simple ordering

A simple ordering says that one term always gets smaller in a subgoal, even if the other ones get larger. The first argument to a always gets smaller in this example (even though the second may get bigger). We only need to be able to reason about the first argument, but we define both to be inputs.

%sort a {_ nat} {_ nat} %.
%mode a %in %in %.
%term a0 a z z %.
%term a1 %pi (a (s N1) N) %<- (a N1 (s (s (s N)))) %.

%terminates N (a N _).

Alternatively, the second argument to b always gets smaller (even though the first may stay the same), and the termination declarations capture this information. The *A in the %mode declaration means that we do not care whether the first argument to b is an input or an output.

Notice that because we already showed a to be terminating, we can use it as a subgoal to b as long as it is only called with ground terms.

%sort b {_ nat} {_ nat} %.
%mode b %star %in %.
%term b0 b (s z) (s z) %.
%term b1 %pi (b N (s (s M))) %<- (b N M) %<- (a (s (s (s M))) M) %.

%terminates N (b _ N).

Simultaneous ordering

We can define a relation c that non-deterministically counts three numbers down to zero:

%sort c {_ nat} {_ nat} {_ nat} %.
%mode c %in %in %in %.
%term c0 c z z z %.
%term c1 %pi (c (s N1) N2 N3) %<- (c N1 N2 N3) %.
%term c2 %pi (c N1 (s N2) N3) %<- (c N1 N2 N3) %.
%term c3 %pi (c N1 N2 (s N3)) %<- (c N1 N2 N3) %.

No single term gets smaller at any one step, but some term gets smaller at every step. We can express this using a simultaneous ordering:

%terminates [N1 N2 N3] (c N1 N2 N3).

Lexicographic ordering

Lexicographic orders generalize simultaneous orders - using a lexicographic ordering we can define d in a manner similar to c, but we can allow the second and third numbers to count up whenever the first number counts down, and allow the third number to count up whenever the second number counts down. However, the first number must stay constant when the second counts down, and the first and second both must stay constant when the third counts down.

%sort d {_ nat} {_ nat} {_ nat} %.
%mode d %in %in %in %.
%term d0 d z z z %.
%term d1 %pi (d (s N1) N2 N3) %<- (d N1 (s (s (s (s N2)))) (s (s N3))) %.
%term d2 %pi (d N1 (s N2) N3) %<- (d N1 N2 (s N3)) %.
%term d3 %pi (d N1 N2 (s N3)) %<- (d N1 N2 N3) %.

%terminates {N1 N2 N3} (d N1 N2 N3).

Lexicographic ordering II

Another example that is (slightly) less contrived arises with lists of natural numbers. If we want to directly represent the sum of a natural number N and a list L, then we can define it as follows:

The sum of z and nil is z.
The sum of z and cons N L is the sum of N and L.
The sum of (s N) and L is s M, if M is the sume of N and L.

This is a lexicographic induction - either the list gets smaller, or the natural number gets smaller and the list stays the same size.

%sort list %.
%term nil list %.
%term cons %pi nat %-> list %-> list %.
%sort listsum {_ nat} {_ list} {_ nat} %.
%mode listsum %in %in %out %.
%term lsz listsum z nil z %.
%term lsl %pi (listsum z (cons N L) M) %<- (listsum N L M) %.
%term lss %pi (listsum (s N) L (s M)) %<- (listsum N L M) %.
%terminates {L N} (listsum N L M) %.

Mutual, lexicographic ordering

In this case, we have a program that is non-deterministic to illustrate more possibilities. We will describe a “big” lemma and a “small” lemma, each with two arguments. STELF decides what is “big” or “small” based on the way we order things - from small to large - in the %terminates declaration below.

%sort big {_ nat} {_ nat} {_ nat} %.
%sort small {_ nat} {_ nat} {_ nat} %.
%mode big %in %in %out %.
%mode small %in %in %out %.

We can split up the possibilities into four cases:

We “bottom out” in a base case or a call to another theorem:

%term & small z N N %.
%term & %pi (big N M P) %<- (listsum N (cons M (cons M nil)) P) %.

The second argument gets smaller (nothing else matters)

%term & %pi (small N1 (s N2) N3) %<- (big (s (s N1)) N2 N3) %.
%term & %pi (small N1 (s N2) N3) %<- (big N2 N2 N3) %.
%term & %pi (big N1 (s (s N2)) N3) %<- (big N1 N2 N3) %.

The first argument gets smaller, and the second argument gets no bigger.

%term & %pi (small (s N1) (s N2) (s N3)) %<- (big N1 N2 N3) %.
%term & %pi (big (s N1) N2 N3) %<- (big N1 N2 N3) %.

The “lemma” gets smaller and everything else gets no bigger.

%term & %pi (big N1 N2 N3) %<- (small N1 N2 N3) %.
%term & %pi (big (s N1) (s N2) N3) %<- (small N1 N2 N3) %.

These requirements are encoded in the declaration below. The ordering of the patterns declares small to be smaller than big, and either the second argument (B1 and B2) gets smaller, or else it gets no bigger and the first argument (A1 and A2) gets smaller.

%terminates {(B1 B2) (A1 A2)} (small A2 B2 _) (big A1 B1 _) %.

Troubleshooting

The simplest example of running afoul of the STELF termination checker is if the recursive call uses an argument unrelated to the original argument.

e: nat -> nat -> type.
- : e N M <- e M N.
%mode e +N +M.
%terminates N (e N M).

As the error message indicates, STELF requires that M be less than N in the recursive call in order for termination analysis to hold, but it has no way of establishing this. If, for some reason, the un-fufilled termination requirement is actually true, it can often be established with a %reduces declaration.