Computer Science Mathematics
ComputerScience,1970-2008-Computer Science-2000.jsonl.gz.gz
Computer Science
6cba1c1e335c2741d5d26f3eb7488e1dd8ad3a2e
Proving Termination of Normalization Functions for Conditional Expressions

Boyer and Moore have discussed a recursive function that puts conditional expressions into normal form [1]. It is difficult to prove that this function terminates on all inputs. Three termination proofs are compared: (1) using a measure function, (2) in domain theory using LCF, (3) showing that its recursion relation, defined by the pattern of recursive calls, is well-founded. The last two proofs are essentially the same though conducted in markedly different logical frameworks. An obviously total variant of the normalize function is presented as the `computational meaning' of those two proofs. A related function makes nested recursive calls. The three termination proofs become more complex: termination and correctness must be proved simultaneously. The recursion relation approach seems flexible enough to handle subtle termination proofs where previously domain theory seemed essential.


A normalization function
Boyer and Moore have published a machine-assisted proof of the correctness of a tautology checker for propositional logic [1]. Propositions are represented as conditional expressions (henceforth expressions). An expression is either an atom At(a) for some symbol a, or else has the form If (x, y, z) where x, y, z are themselves expressions. An atom represents a propositional letter, while If (x, y, z) is equal to y if x is true, and equal to z otherwise.
The tautology checker includes a function for putting expressions into normal form. An expression is in normal form if it has no tested Ifs: subexpressions of the form If (If (u, v, w), y, z). Replacing this by If (u, If (v, y, z), If (w, y, z)) preserves the value of the entire expression and removes one tested If. However new tested Ifs are created whenever v or w begin with If.
The following program, written in Standard ML [6], defines the data structure exp and the normalize function norm. If its argument is a tested If then norm replaces it as above and calls itself recursively. For any other argument norm makes recursive calls on the subexpressions. The ML code should fill in the details: It is far from obvious that norm terminates. In the If-If case it calls itself with a larger expression than it was given. One way of proving termination is to find a well-founded relation under which the argument 'goes down' in every recursive call [1,5]. Classically, a relation ≺ is well-founded if and only if it has no infinite descending chains · · · ≺ x 2 ≺ x 1 ≺ x 0 . The less-than relation < on the set N of natural numbers is well-founded. Less-than is not well-founded on certain other sets: for the integers, · · · < −2 < −1 < 0, and for the rationals, · · · < .01 < .1 < 1.
A common way of defining a well-founded relation on a set A uses a measure function f :

A proof using a measure function
In Boyer and Moore's logic all functions are total. Their theorem prover only accepts a recursive definition if it can show that the function terminates on all arguments. For this purpose it uses well-founded relations consisting of lexicographic combinations of inverse images. Boyer and Moore present a well-founded relation for norm involving two measures on expressions. Boyer has also sent me a simpler proof, credited to R. Shostak, using a single measure function: To show that this measure goes down in each of norm's recursive calls is a tedious exercise of expanding and collecting terms. It is important to check the easy If-At case, because a clever measure that goes down in the hard If-If case may not go down in the easy case. Note that m(x) is positive for all x.
and the original argument has measure Cancelling common terms, this case terminates because UY + UZ > 0.

A proof in the Logic of Computable Functions
Jacek Leszczy lowski [4] has proved the termination of norm using the theorem prover Edinburgh LCF [3]. LCF's logic, a formalization of domain theory, allows reasoning about partial functions. Leszczy lowski's proof uses a lemma that the termination of norm in particular cases implies termination in other cases. Each domain contains an 'undefined' element ⊥, representing the result of a divergent computation. There is a weak equality predicate ≡ such that x ≡ y iff x and y are both undefined, or both defined and equal. Since quantifiers often range over defined values only, let ∀ D x. P (x) abbreviate ∀x. x ≡ ⊥ ⇒ P (x). The statement 'norm is total' is expressed as ∀ D x.norm(x) ≡ ⊥. The domain of expressions is flat to avoid having infinite expressions [9]. The constructor functions At and If are total: This rule is often stated with the additional premise P (⊥). Then the conclusion is ∀x. P (x).
The function norm is expressed as three equations in LCF: The termination proof involves a lemma that if norm(y) and norm(z) terminate, then norm(If (x, y, z)) terminates.
which follows because If and At are total.
The If case reduces to showing assuming that u, v, w, y, z are all defined and with induction hypotheses for u, v, and w: Instantiate the induction hypothesis for u with y → If (v, y, z) and z → If (w, y, z), Q.E.D.
Termination of norm on all inputs follows by induction in ∀ D x.norm(x) ≡ ⊥.

Proving the recursion relation is well-founded
The first termination proof defines a well-founded relation using a measure function, and shows that norm's recursive calls obey that relation. A dual approach is to define a relation ≺ in terms of norm's recursive calls, then show that ≺ is wellfounded. Define x ≺ y to be true whenever evaluating norm(x) requires a recursive call norm(y), and to be false otherwise. (It should be false whenever possible, since additional relationships between elements could prevent ≺ from being well-founded.) I call ≺ the recursion relation of norm.
Case analysis of norm defines its recursion relation: To show the termination of norm it suffices to show that the relation ≺ is wellfounded. This proof will have a remarkable similarity to the LCF proof, which was conducted in domain theory. This section uses a simple mathematical framework with no partial elements. It uses constructive mathematics because this paper is an outgrowth of my study of well-founded relations [10] in Martin-Löf's Constructive Type Theory [8].
Showing that a relation is well-founded requires showing the soundness of its rule of well-founded induction for an arbitrary predicate P : In constructive reasoning, showing that ≺ has no infinite descending chains is insufficient to verify the rule. The rule is verified directly, proving its conclusion from its premise. For the rest of this section assume the induction step: Termination follows from proving ∀x.P (x); a lemma is helpful.
which follows from (1) and the definition of ≺. Recall that If (At(a), y, z) has only two predecessors, y and z.
By (1) it is enough to show Assume P (y) and P (z). The induction hypotheses for v and w imply P (If (v, y, z)) and P (If (w, y, z)). Instantiate the induction hypothesis for u with The previous proof can be translated into this one by replacing norm(x) ≡ ⊥ by P (x). Each unfolding of norm becomes an appeal to the induction step (1). Perhaps domains and partial objects are not essential even for difficult proofs of termination.
As a sample proof in his higher-order theory of constructions, Thierry Coquand has proved the termination of normalization [2] (pages 46-48). He defines a predicate N (x) to mean 'x can be put into normal form,' and proves ∀x. N (x). Translated from his formalism, the axioms are The connection between N (x) and norm(x) ≡ ⊥ is obvious. Coquand builds a proof object resembling my Constructive Type theory one, using a similar Lemma.

An obviously total normalize function
Constructive Type Theory provides a formal interpretation of propositions as types. One consequence is that every proof by induction involves constructing a proof object by recursion. My Type Theory proof that ≺ is well-founded suggests another way of writing the normalize function: normif (v, y, z), normif (w, y, z)); fun norm 1 (At(a)) = At(a) | norm 1 (If (x, y, z)) = normif (x, norm 1 (y), norm 1 (z)); The function normif is obviously total because it is structural recursive in its first argument, a sort of 'higher type' recursion. Although normif makes nested recursive calls in its second and third arguments, these have no effect on termination. (Ackermann's function is another example where termination is obvious despite nested recursive calls.) Note the similarity between normif's recursive calls and the appeals to the induction hypotheses in the proof of the lemma.
Proving in LCF that ∀ D x. norm(x) ≡ norm 1 (x) constitutes yet another termination proof for norm. Our familiar lemma now takes the form with essentially the same proof as before.
There is a pleasing concreteness about the first termination proof. But the measure function offers little intuition. The second and third proofs convey something of what norm is actually doing, for they give us the function normif.

A normalize function with nested recursion
If we modify the If-If case of norm to make nested recursive calls, proving termination becomes trickier still. Call the new function norm 2 : fun norm 2 (At(a)) = At(a) | norm 2 (If (At(a), y, z)) = If (At(a), norm 2 (y), norm 2 (z)) | norm 2 (If (If (u, v, w), y, z)) = norm 2 (If (u, norm 2 (If (v, y, z)), norm 2 (If (w, y, z)))); I sent this function as a challenge to Boyer and Moore. The version of the theorem prover described in their book [1] cannot handle this nested recursion. It could not admit norm 2 as a function unless, for some measure m 2 (x), it could prove m 2 (If (u, norm 2 (If (v, y, z)), norm 2 (If (w, y, z)))) < m 2 (If (If (u, v, w), y, z)) .

Yet this very statement involves norm 2 .
Moore informs me that the theorem prover has since been extended. A nested recursive function definition can be admitted by showing that it is equivalent to some already accepted definition. In this case replace norm 2 by norm in the recursion equations and show that the new equations hold. Thus they have at least one solution: norm. Then show that some measure decreases for each recursive call of norm in the new equations. Thus the solution is unique: by well-founded induction on the measure, norm(x) = norm 2 (x) for all x. Reasoning about norm is possible because it is already known to be a total function. Moore describes this principle of definition in his paper on the termination of Takeuchi's function [7].
Moore's proof of norm 2 has several stages: • norm(norm(x)) = norm(x) is proved by induction on the measure m(x). The result is used in the At case of the next stage.
• ∀yz. norm(If (x, norm(y), norm(z))) = norm (If (x, y, z)) is proved, like the Lemma, by structural induction on x. The theorem prover does not allow quantified induction schemes, but any instance of one can be specified.
• Therefore norm is a solution to the equations for norm 2 .
• A function to count the number of tested Ifs in an expression is defined. This differs from the function IF.DEPTH of the original proof [1], which counts the nesting of tested Ifs.
• norm(x) is indeed normal: it contains no tested Ifs. Proved by induction on m(x).
• The measure for proving uniqueness is the lexicographic combination of the number of tested Ifs and the size of an expression.

The LCF proof revisited
In domain theory the termination of norm 2 can be proved without any mention of norm. Termination and partial correctness must be proved simultaneously. Showing termination of the If-If case requires showing that the nested calls yield normal expressions. Define the predicate ISN (x) to hold whenever x is in normal form. ISN is a recursive predicate but the recursion is trivially well-founded: (If (u, v, w), y, z)) ⇐⇒ false The element ⊥ is not in normal form under this definition; ∀ D x.ISN (norm 2 (x)) states that norm 2 is a total function whose result is always normal. This is not a complete statement of correctness; it mentions no relationship between x and norm 2 (x).
The proof resembles that of section 3, replacing each occurrence of norm(x) ≡ ⊥ by ISN (norm 2 (x)). Fact. If the argument of norm 2 is normal then so is its result: Proof. By structural induction on x. The ⊥ and At cases are easy. For If consider two cases. Since If (If (u, v, w), y, z) is not normal the result holds vacuously. The If (At(a), y, z) case is (At(a), y, z))) which simplifies to which follows from the induction hypotheses. Now we have the usual Lemma. ∀ D xyz. ISN (norm 2 (y)) ∧ ISN (norm 2 (z)) ⇒ ISN (norm 2 (If (x, y, z))) Proof. By structural induction on x. The At case reduces to the clearly true The If case reduces to showing, under induction hypotheses, ISN (norm 2 (y)) ∧ ISN (norm 2 (z)) ⇒ ISN (norm 2 (If (u, If (v, y, z), If (w, y, z)))) .
Again the overall proof for norm 2 is an easy induction using the Lemma. Proving ∀ D x.ISN (norm 2 (x)) rather than ∀ D x.norm 2 (x) ≡ ⊥ is a classic example of strengthening the goal in order to strengthen the induction hypotheses. The Lemma is essentially the inductive step. Its proof requires the Fact (2). Proving ∀ D x.norm 2 (x) ≡ ⊥ would require a Lemma of the form ∀ D xyz. norm 2 (y) ≡ ⊥ ∧ norm 2 (z) ≡ ⊥ ⇒ norm 2 (If (x, y, z)) ≡ ⊥ and a Fact of the form ∀x.x ≡ ⊥ ⇒ norm 2 (x) ≡ ⊥. We are going in circles! It would suffice to prove a weaker version of the Fact: An attempted proof of this resembles that of (2) except that the If-If case is no longer trivial.

The recursion relation proof revisited
The recursion relation proof of section 4 can similarly be adapted to norm 2 . I continue to use the predicate ISN for reasoning about normal expressions, though in this section there is no element ⊥. The recursion relation ≺ 2 is defined like ≺, except that the If-If case has three recursive calls instead of one. The outer call involves the results of the inner calls, expressed as existentially quantified variables. The results are assumed to be in normal form: ⇐⇒ false It will be necessary to show inductively that the equations for norm 2 produce normal expressions. First let us show that ≺ 2 is well-founded. Assume the induction step for an arbitrary P : Fact. The induction step (3) implies P (x) for all x in normal form. The Lemma is stated just like in section 4: Lemma. ∀xyz. P (y) ∧ P (z) ⇒ P (If (x, y, z)) Proof. By structural induction on x. The At case is proved as before. The If case is ∀yz. P (y) ∧ P (z) ⇒ P (If (If (u, v, w), y, z)) .
By (3) it is enough to show that P (y) and P (z) imply each of The induction hypotheses for v and w imply P (If (v, y, z)) and P (If (w, y, z)). It suffices to show P (If (u, v , w )) for arbitrary normal expressions v and w . The Fact (4) implies P (v ) and P (w ). Instantiate the induction hypothesis for u with y → v and z → w . Q.E.D.
The translation from the domain theory proof replaces ISN (norm 2 (x)) by P (x). The connection between the proofs is weaker that it was for norm. Domain theory allows explicit mention of norm 2 's recursive calls when instantiating u's induction hypothesis; the recursion relation hides the calls via quantifiers.
The justification of norm 2 still requires simultaneous proofs that it terminates yielding a normal expression. The proof is by well-founded induction on ≺ 2 : • Given At(a) it makes no recursive calls and returns an atom, which is always normal.
• Given If (At(a), y, z) it makes recursive calls on the predecessors y and z. By induction hypotheses these calls return normal expressions so the final result is normal.
• Given If (If (u, v, w), y, z) it makes recursive calls on predecessors If (v, y, z) and If (w, y, z). By induction hypotheses these return normal expressions v and w . So If (u, v , w ) is a predecessor, justifying the final recursive call. By induction hypothesis this returns a normal expression.
This reasoning about the various cases of norm 2 can be formalized in my setting of well-founded recursion operators in Constructive Type Theory [10]. A function application has type y∈exp ISN (y). It returns a pair of results: a normal expression y and a proof object of type ISN (y). Each recursive call on an argument z must be justified by exhibiting a proof object of type z ≺ 2 x. This is passed as an additional argument. In the If-If case, the outer call passes a proof object for If (u, v , w ) ≺ 2 If (If (u, v, w), y, z), constructed from proof objects ISN (u ) and ISN (v ) from the inner calls.
After performing this elaborate construction of a well-founded recursion, the equations for norm 2 can be proved as usual in the approach [10].

Conclusions
Domain theory allows reasoning about recursion in a most flexible way, but at a heavy cost of complexity. The ideas can be difficult to grasp and introduce theoretical and practical obstacles. LCF is the only major theorem proving project that uses domain theory; even LCF users sometimes prefer to do without domains. The recursion relation proofs of norm and norm 2 suggest that domains are not essential for reasoning about many programs. Domain theory still has a vital role to play: there is no alternative for reasoning about compilers and continuously running processes.
Constructive Type Theory is concerned with terminating computations. Domain theory cannot be patched onto it; partial functions are completely antithetical to its view of computation. Using recursion relations it can express termination proofs of norm and norm 2 , thereby deriving the function normif.
It is especially hard to prove the termination of functions involving nested recursion, since the termination of an outer recursive call may depend on a property of the results of the inner calls. The example norm 2 shows that this can be done without domains. Manna and Waldinger have studied a much more interesting nested recursive function, UNIFY, which performs unification [5]. They define a well-founded relation involving the structure of the expressions being unified and the number of distinct variables in those expressions. Under this relation, UNIFY's outer recursive call can be justified only if its inner call returns a most-general, idempotent unifier of its arguments.
I formalized their work using the theorem prover Cambridge LCF, proving the total correctness of UNIFY [12]. The proof used a predicate BEST UNIFY TRY in a role analogous to that of ISN in the proof of norm 2 : to allow the simultaneous proof of termination and correctness. It appears possible to verify UNIFY in Constructive Type Theory. Manna and Waldinger's well-founded relation is appropriate; there is no need to consider the recursion relation. UNIFY would return a substitution paired with a proof that this substitution had the necessary properties.
An axiom, previously created by struct axm, is bound to the ML identifier EXP DEFINED. The structural induction tactic is instantiated to handle expressions and bound to the ML identifier EXP TAC. The Lemma is proved by induction followed by rewriting via the equations for norm and the totality of the constructors At and If. I have tweaked the statement of the Lemma to circumvent an annoyance involving admissibility of induction [3]. The proof that norm is total resembles the proof of the Lemma.