Combining typing and size constraints for checking the termination of higher-order conditional rewrite systems

Frédéric Blanqui (INRIA) and Colin Riba (INPL)

LORIA^{⋆}, Campus Scientifique, BP 239 54506 Vandoeuvre-lès-Nancy Cedex, France

Abstract. In a previous work, the first author extended to higher-order rewriting and dependent types the use of size annotations in types, a termination proof technique called type or size based termination and initially developed for ML-like programs. Here, we go one step further by considering conditional rewriting and explicit quantifications and constraints on size annotations. This allows to describe more precisely how the size of the output of a function depends on the size of its inputs. Hence, we can check the termination of more functions. We first give a general type-checking algorithm based on constraint solving. Then, we give a termination criterion with constraints in Presburger arithmetic. To our knowledge, this is the first termination criterion for higher-order conditional rewriting taking into account the conditions in termination.

1 Introduction

We are interested in automatically checking the termination of the combination of β-reduction and higher-order conditional rewrite rules. There are two important approaches to higher-order rewriting: rewriting on β\overline{η}-normal forms [17], and the combination of β-reduction and term rewriting [16]. The relation between both has been studied in [20]. The second approach is more atomic since a rewrite step in the first approach can be directly encoded by a rewrite step together with β-steps in the second approach. In this paper, we consider the second approach, restricted to first-order pattern-matching (we do not allow abstractions in rule left-hand side). Following [7], our results could perhaps be extended to higher-order pattern-matching.

The combination of β-reduction and rewriting is naturally used in proof assistants implementing the proposition-as-type and proof-as-object paradigm. In these systems, two propositions equivalent modulo β-reduction and rewriting are identified (e.g. P (2 + 2) and P (4)). This is essential for enabling users to formalize large proofs with many computations, as recently shown by Gonthier and Werner’s proof of the Four Color Theorem in the Coq proof assistant. However, for the system to be able to check the correctness of user proofs, it must

⋆ UMR 7503 CNRS-INPL-INRIA-Nancy2-UHP

at least be able to check the equivalence of two terms. Hence, the necessity to have termination criteria for the combination of β-reduction and rewriting.

In Coq, rewriting is restricted to the reductions associated to inductive types like in functional programming languages with pattern-matching. Such reductions correspond to constructor-based rewriting. This is the kind of rewrite systems we are going to consider in this paper. A more general form of rewriting is studied in [9, 6] (matching on defined symbols and matching modulo).

Currently, Coq accepts only functions in the definition of which recursive calls are made on arguments that are structurally smaller. For first-order functions, this corresponds to restrict rewrite systems to simply terminating ones, that is, to the ones that can be proved terminating by an ordering containing the subterm relation. However, many interesting systems are not simply terminating. Consider for instance the following definition of division on natural numbers:

minus 0 x → 0
minus x 0 → x
minus (s x) (s y) → minus x y
div 0 y → 0
div (s x) y → s (div (minus x y) y)

Considering that minus is applied to strongly normalizing arguments and that the size of a term is the height of its normal form, one can easily prove, by induction on the size of t, that the size of v = (minus t u) is less than or equal to the size of t, hence that this definition of minus terminates:

– If v matches the first rule, then t = 0 and the normal form of v, which is 0, has the same size as t.

– If v matches the second rule, then v has the same normal form as t.

– If v matches the third rule, then t = st′, u = su′ and, by induction hypothesis, the normal form of v has a size smaller than t′, hence smaller than t. The idea of size or type based termination, initiated in [15] and developed by

various authors for ML-like definitions [11, 22, 1–4] and rewriting and dependent types [8, 5], consists in extending the underlying type system by replacing a base type B by an infinite family of base types (B^{𝔞})_{𝔞∈ℕ}, a term of type B^{𝔞} being by construction of size smaller than or equal to 𝔞 (except in [22], see later). Then, for ensuring termination, one can restrict in function definitions recursive calls to arguments whose size, by typing, is smaller.

For instance, in all these systems, one can easily (type-)check that minus has for type something similar to ∀αβN^{α} ⇒ N^{β} ⇒ N^{α}. Hence, assuming that x : N^{α} and y : N^{β}, one can easily (type-)check that minus x y : N^{α} while sx : N^{α+1}. Thus, the recursive call to div in the last rule can be allowed.

Note that higher-order inductive types, i.e. types having constructors with recursive arguments of higher-order type, require families indexed by ordinals. In the present paper, we restrict our attention to first-order inductive types since higher-order inductive types have already been studied in previous works. Note also that interpreting B^{𝔞} by the set of terms of size smaller than or equal to 𝔞 requires subtyping since t : B^{𝔟} whenever t : B^{𝔞} and 𝔞 ≤ 𝔟.

However, without explicit existential quantifications and constraints over size annotations, one cannot (type-)check that the following function has type N ⇒ ∀αL^{α} ⇒ ∃βγ(α = β + γ)L^{β} × L^{γ}:

pivot x nil → (nil , nil )
pivot x (cons y l) → let z = pivot x l in

if (le y x) then (cons y (fst z), snd z) else (fst z, cons y (snd z))

Such a type is necessary for proving that some sorting functions are size preserving, i.e. have type ∀αL^{α} ⇒ L^{α}. To the best of our knowledge, only Xi considers such explicit quantifications and constraints [22]. In this work, B^{𝔞} is interpreted as the set of terms of size 𝔞. Note that, with this interpretation, the type of terms of size smaller than 𝔞 can be represented by ∃α(α ≤ 𝔞)B^{α}. However, we cannot apply Xi’s results on the problem we are interested in for the following reasons:

– Xi considers ML-like function definitions based on letrec/match constructions while we are interested in definitions based on rewrite rules.

– Xi is interested in the termination of closed terms with call-by-value evaluation strategy while we are interested in the strong normalization of open terms.

– Xi has a two-level approach. He considers an intermediate system where not only types but also terms are annotated by size informations, and proves that terms typable in this system are terminating. Then, for proving the termination of an unannotated term, he must infer the necessary size annotations, which may not be possible. This elaboration process is described in [21]. In the present paper, we extend the simply typed part of [8] with conditional

rewriting and explicit quantifications and constraints over size annotations, without using an intermediate system. As Xi and in contrast with [8], we do not consider higher-order inductive types and interpret B^{𝔞} as the set of terms of size 𝔞. The integration of both works should not create too much difficulties. Hence, we get a powerful termination criterion for the combination of β-reduction and higher-order conditional rewriting, based on type-checking and constraint solving. To our knowledge, this is the first termination criterion for higher-order conditional rewriting taking into account the conditions in termination.

In Section 2, we define a system with constrained types. In Section 3, we give a general type-checking algorithm based on constraint solving. In Section 4, we present a general termination proof technique based on Tait’s method for proving the termination of β-reduction. In Section 5, we give a termination criterion based on type-checking with constraints in Presburger arithmetic.

2 A system with constrained types

Terms. The set T of terms is inductively defined as follows:

t ∈ T ::= x | c | f | λxt | tt | (t, t) | fst t | snd t | let x = t in t | if t then t else t where x ∈ X is a term variable, c ∈ C is a constructor symbol and f ∈ F is a function symbol. We assume that C contains true and false. As usual, terms are considered up to renaming of bound variables. By t, we denote a sequence of terms t_{1}, …, t_{n} of length |t| = n ≥ 0. Term substitutions are denoted by σ, θ, … or their explicit mappings (_{x}^{t}). By σ + θ, we denote the substitution equal to θ on dom(θ) and to σ on dom(σ) \ dom(θ). The set P of (constructor) patterns is inductively defined by p ∈ P ::= x | c p.

Size annotations. Let S = {nat, bool} be the set of size sorts. We assume given a S-sorted first-order term algebra A for size expressions a, b, … whose variables are denoted by α, β, … We assume that A at least contains the symbols 0 : nat, 1 : nat, + : nat × nat ⇒ nat, max : nat × nat ⇒ nat, t : bool and f : bool. For each sort s, we assume given a well-founded interpretation domain (D_{s}, >_{D_{s}}). For bool, we take D_{bool} = {𝔱, 𝔣}. In the following, let true^{∗} = t and false^{∗} = f; t^{∗} = 𝔱 and f^{∗} = 𝔣; 𝔱^{∗} = true and 𝔣^{∗} = false. Elements of D_{s} are denoted by 𝔞, 𝔟, … Valuations are denoted by μ, ν, … Size substitutions are denoted by φ, ψ, …

Constraints. Let a constraint be a first-order formula over A, ℂ be a class of constraints containing ⊤ and FV(C) be the variables free in C. We denote by μ ⊧ C the fact that a valuation μ satisfies C; by ⊢ C the fact that, for all valuation μ such that FV(C) ⊆ dom(μ), μ ⊧ C, and by C ≡ D the fact that ⊢ C ⇔ D. We consider constraints up to the logical equivalence ≡.

Types. We assume given a set B of type names containing bool. Let κ_{bool} = bool and, for all B ≠ bool, κ_{B} = nat (except bool that is annotated by booleans, types are annotated by natural numbers). Types are defined as follows:

types T ∈ 𝕋 ::= B^{a} | T ⇒ T | T × T | ∀αP T | ∃αP T
simple types S ∈ 𝕊 ::= ∃αB^{α} | S ⇒ S | S × S
basic types B ∈ 𝔹 ::= B^{a} | B × B
∃-basic types E ∈ 𝔼 ::= B | ∃αP E with ⊢ ∃αP

where B ∈ B is a type name, a ∈ A is a size expression of sort κ_{B} and P ∈ ℂ is a constraint. In the following, we use the following abbreviations: ∀αT = ∀α⊤T and B = ∃αB^{α}. There is a natural transformation from 𝕋 to 𝕊: let \overline{B^{a}} = ∃αB^{α}, \overline{∃αP T} = \overline{∀αP T} = \overline{T}, \overline{T ⇒ U} = \overline{T} ⇒ \overline{U} and \overline{T × U} = \overline{T} × \overline{U}.

Subtyping. We define a constraint-based subtyping relation. Let C ⊢ T ≤ U iff ⊢ C ⊃ (|T ≤ U|) where (|T ≤ U|) is inductively defined as follows:

– (|B^{a} ≤ B^{b}|) = (a = b)

– (|T ⇒ U ≤ T′ ⇒ U′|) = (|T′ ≤ T |) ∧ (|U ≤ U′|)

– (|T × U ≤ T′ × U′|) = (|T ≤ T′|) ∧ (|U ≤ U′|)

– (|T ≤ ∃αP U|) = ∃α(P ∧ (|T ≤ U|)) (α ∉ T, T ≠ ∃βQV)

– (|∃αP U ≤ T |) = ∀α(P ⊃ (|U ≤ T |)) (α ∉ T)

– (|T ≤ ∀αP U|) = ∀α(P ⊃ (|T ≤ U|)) (α ∉ T)

– (|∀αP U ≤ T |) = ∃α(P ∧ (|U ≤ T |)) (α ∉ T, T ≠ ∀βQV) Typing. An environment is a finite mapping Γ from X to 𝕋. Let Γ, x : T be

the environment Δ such that xΔ = T and yΔ = yΓ if y ≠ x. Two environments Γ_{1} and Γ_{2} are compatible if, for all x, xΓ_{1} = xΓ_{2}.

A type assignment is a function τ : C ∪ F → 𝕋 such that τ_{true} = bool^{t}, τ_{false} = bool^{f} and, for all s ∈ C ∪ F, τ_{s} is closed. To every type assignment τ, we associate a typing relation ⊢_{τ} defined in Figure 1. Note that, in contrast with [22], the typing of u and v in (if) does not depend on t. This is because we consider strong normalization instead of weak normalization. This does not reduce the expressive power of the system since we consider conditional rewriting.

A term t is typable wrt τ if there are C, Γ, T such that ⊢ C and C; Γ ⊢_{τ} t : T. Let Λ(τ) be the set of terms typable wrt τ. A term t is simply typable if there are Γ, T simple such that ⊤; Γ ⊢\overline{τ} t : T without (∃intro), (∀intro), (∃elim), (∀elim), (sub). Let \overline{Λ}(\overline{τ}) be the set of terms simply typable wrt \overline{τ}.

Fig. 1. Typing rules

(var) \frac{x ∈ dom(Γ)}{C; Γ ⊢_{τ} x : xΓ} (symb) \frac{s ∈ C ∪ F}{C; Γ ⊢_{τ} s : τ_{s}}

(abs) \frac{C; Γ, x : T ⊢_{τ} u : U x ∉ Γ}{C; Γ ⊢_{τ} λxu : T ⇒ U} (app) \frac{C; Γ ⊢_{τ} t : U ⇒ V C; Γ ⊢_{τ} u : U}{C; Γ ⊢_{τ} tu : V}

(pair) \frac{C; Γ ⊢_{τ} u : U C; Γ ⊢_{τ} v : V}{C; Γ ⊢_{τ} (u, v) : U × V}

(fst) \frac{C; Γ ⊢_{τ} t : U × V}{C; Γ ⊢_{τ} fst t : U} (snd) \frac{C; Γ ⊢_{τ} t : U × V}{C; Γ ⊢_{τ} snd t : V}

(if) \frac{C; Γ ⊢_{τ} t : bool C; Γ ⊢_{τ} u : T C; Γ ⊢_{τ} v : T T ∃-basic}{C; Γ ⊢_{τ} if t then u else v : T}

(let) \frac{C; Γ ⊢_{τ} t : T C; Γ, x : T ⊢_{τ} u : U x ∉ Γ}{C; Γ ⊢_{τ} let x = t in u : U}

(∀intro) \frac{C ∧ P; Γ ⊢_{τ} t : T ⊢ C ⊃ ∃αP α ∉ C, Γ}{C; Γ ⊢_{τ} t : ∀αP T}

(∀elim) \frac{C; Γ ⊢_{τ} t : ∀αP T ⊢ C ⊃ P_{α}^{a}}{C; Γ ⊢_{τ} t : T_{α}^{a}}

(∃intro) \frac{C; Γ ⊢_{τ} t : T_{α}^{a} ⊢ C ⊃ P_{α}^{a}}{C; Γ ⊢_{τ} t : ∃αP T}

(∃elim) \frac{C; Γ ⊢_{τ} t : ∃αP T C ∧ P; Γ, x : T ⊢_{τ} u : U ⊢ C ⊃ ∃αP α, x ∉ C, Γ, U}{C; Γ ⊢_{τ} let x = t in u : U}

(sub) \frac{C; Γ ⊢_{τ} t : T C ⊢ T ≤ T′}{C; Γ ⊢_{τ} t : T′}

Example 1. Consider the symbols append : ∀βγL^{β} ⇒ L^{γ} ⇒ L^{β+γ} and pivot : N ⇒ ∀αL^{α} ⇒ ∃βγ(α = β + γ)L^{β} × L^{γ}. Let Γ = x : N, l : L^{α}, u = (let z = t in v), t = pivot x l and v = append (fst z)(snd z). Then, ⊤; Γ ⊢ t : ∃βγ(α = β+γ)L^{β}×L^{γ} and α = β + γ; Γ, z : L^{β} × L^{γ} ⊢ v : L^{α}. Thus, by (∃elim), Γ ⊢ u : L^{α}.

Rewriting. Let →_{β} be the smallest relation stable by context containing the head-β-reduction relation →_{βh} defined as follows:

(λxu)t →_{βh} u_{x}^{t}_{let x = t in u →_{βh} u_{x}^{t}} fst (u, v) →_{βh} u_{snd (u, v) →_{βh} v} if true then u else v →_{βh} u

if false then u else v →_{βh} v

A conditional rewrite rule is an expression of the form t = c ⊃ l → r such that l is of the form fl, l are patterns, c ∈ {true, false} and FV(r, t) ⊆ FV(l). A rule t = c ⊃ l → r defines f ∈ F if l is of the form fl. In the following, we assume given a set R of rules. The associated rewrite relation is the smallest relation →_{R} stable by context and substitution such that, for all t = c ⊃ l → r ∈ R, lσ →_{R} rσ whenever tσ →^{∗} c, where →^{∗} is the reflexive and transitive closure of →=→_{β} ∪ →_{R}.

Our goal is to prove the strong normalization of →=→_{β} ∪ →_{R} on the set of simply typable terms \overline{Λ}(\overline{τ}).

Assumption: We assume that → is locally confluent.

Hence, any strongly normalizing term t has a unique normal form t↓. Note that → is locally confluent whenever →_{R} so is. See [10] for general conditions on the confluence of β-reduction and higher-order conditional rewriting.

It should be noted that (∃elim) makes subject reduction fail. For instance, with Γ = x : ∃αN^{α}, y : ∀αN^{α} ⇒ ∃βN^{β}, we have ⊤; Γ ⊢ let z = x in yz : ∃βN^{β} while yx is not typable in ⊤; Γ. It could be fixed by replacing in (∃elim) let x = t in u by u_{x}^{t}. It does not matter since our termination proof technique does not need subject reduction. Note however that subject reduction holds on simply typed terms.

An example of higher-order conditional rule is given by the following definition of filter : (N ⇒ N) ⇒ ∀αL^{α} ⇒ ∃β(β ≤ α)L^{β}:

filter f nil → nil
f x = true ⊃ filter f(cons x l) → cons (f x) (filter f l)
f x = false ⊃ filter f(cons x l) → filter f l

3 Type-checking algorithm

Type-checking is the following problem: given τ, C, Γ, t and T, do we have C satisfiable and C; Γ ⊢_{τ} t : T ?

Because of the rules (∃elim) and (conv), type-checking does not seem to be decidable. Similarly, in [22], the elaboration process is not complete. It is however possible to give an algorithm that either succeed or fails, a failure meaning that we don’t know. To this end, we inductively define in Figure 2 two relations in the style of bi-directional type inference [12, 2]. In the type inference relation C; Γ ⊢ t ↑ T, C and T are produced according to Γ and t. In the type checking relation C; Γ ⊢ t ↓ T, C is produced according to Γ, t and T. An actual algorithm is a strategy for applying the rules defining these relations.

Let \overline{ℂ} be the closure of ℂ by conjunction, implication, existential and universal quantification. If one starts with C ∈ ℂ, then the constraints generated by such an algorithm are in ℂ too. Hence, if ℂ only contains linear inequalities, then \overline{ℂ} are formulas of Presburger arithmetic which is known to be decidable [18] and whose complexity is doubly exponential in the size of the formula [13]. This high complexity is not so important in our case since the terms we intend to consider are small (rule right-hand sides). It would be however interesting to study in more details the complexity of type-checking wrt ℂ.

For proving the correctness of the rule (↓∃intro), we need to assume that the size expression language A is complete wrt the interpretation domains D_{s}, that is, to every 𝔞 ∈ D_{s} corresponds a closed term a ∈ A whose denotation in D_{s} is 𝔞. Note that this is indeed the case when D_{s} = ℕ and A contains 0, 1 and +.

See Example 3 at the end of the paper for an example of derivation.

Theorem 1. Consider the rules of Figure 2. If C; Γ ⊢^{?} t : T, then C is satisfiable and C; Γ ⊢ t : T.

Proof. First, one can easily check that, for every rule, if the constraint in the conclusion is satisfiable, then the constraints in the premises are satisfiable too. Then, we prove that, if C is satisfiable and C; Γ ⊢ t ↑ T or C; Γ ⊢ t ↓ T, then C; Γ ⊢ t : T. We only detail some cases.

(↑∃elim) Let E = C ∧ ∃αP ∧ ∀α(P ⊃ D). Since E ⊃ C and (E ∧ P) ⊃ D, by induction hypothesis and weakening, E; Γ ⊢ t : ∃αP T and E ∧ P; Γ ⊢ u : U. Since (E ∧ P) ⊃ P, by (∃intro), E ∧ P; Γ ⊢ u : ∃αP U. Since E ⊃ ∃αP and α ∉ ∃αP U, by (∃elim), E; Γ ⊢ let x = t in u : ∃αP U.

(↓∀intro) Let E = ∃αP ∧ ∀α(P ⊃ C). Since (E ∧ P) ⊃ C, by induction hypothesis and weakening, E ∧ P; Γ ⊢ t : T. Since E ⊃ ∃αP, we can conclude by (∀intro).

(↓∀elim) Let E = C ∧ P_{α}^{a}. By induction hypothesis and weakening, E; Γ ⊢ t :

∀αP T. Since E ⊃ P_{α}^{a}, we can conclude by (∀elim). (↓∃intro) Let E = ∃α(C ∧ P). Since E is satisfiable, C is satisfiable too. By

completeness, there is a such that F = C_{α}^{a} ∧ P_{α}^{a} is satisfiable. By induction hypothesis, C; Γ ⊢ t : T. By substitution and weakening, F; Γ ⊢ t : T_{α}^{a}. Since F ⊃ P_{α}^{a}, by (∃intro), F; Γ ⊢ t : ∃αP T. Since E ⊃ F, we can conclude by weakening.

(↓∃elim) Let E = C ∧ ∃αP ∧ ∀α(P ⊃ D). Since E ⊃ C and (E ∧ P) ⊃ D, by induction hypothesis and weakening, E; Γ ⊢ t : ∃αP T and E ∧ P; Γ ⊢ u : U. Since E ⊃ ∃αP and α ∉ U, by (∃elim), E; Γ ⊢ let x = t in u : U. ⊓ ⊔

Fig. 2. Rules for deciding type-checking

(type-check) \frac{D; Γ ⊢ t ↓ T ⊢ C ⊃ D C satisfiable}{C; Γ ⊢^{?} t : T}

(↑var) \frac{x ∈ dom(Γ)}{⊤; Γ ⊢ x ↑ xΓ} (↑symb) ⊤; Γ ⊢ s ↑ τ_{s}

(↑app) \frac{C; Γ ⊢ t ↑ U ⇒ V D; Γ ⊢ u ↓ U}{C ∧ D; Γ ⊢ tu ↑ V}

(↑pair) \frac{C; Γ ⊢ u ↑ U D; Γ ⊢ v ↑ V}{C ∧ D; Γ ⊢ (u, v) ↑ U × V}

(↑fst) \frac{C; Γ ⊢ t ↑ U × V}{C; Γ ⊢ fst t ↑ U} (↑snd) \frac{C; Γ ⊢ t ↑ U × V}{C; Γ ⊢ snd t ↑ V}

(↑let) \frac{C; Γ ⊢ t ↑ T D; Γ, x : T ⊢ u ↑ U}{C ∧ D; Γ ⊢ let x = t in u ↑ U}

(↑∀elim) \frac{C; Γ ⊢ t ↑ ∀αP T α ∉ C, Γ}{C ∧ P; Γ ⊢ t ↑ T}

(↑∃elim) \frac{C; Γ ⊢ t ↑ ∃αP T D; Γ, x : T ⊢ u ↑ U x ∉ Γ α ∉ C, Γ}{C ∧ ∃αP ∧ ∀α(P ⊃ D); Γ ⊢ let x = t in u ↑ ∃αP U}

(↓abs) \frac{C; Γ, x : T ⊢ u ↓ U x ∉ Γ}{C; Γ ⊢ λxu ↓ T ⇒ U}

(↓if) \frac{C; Γ ⊢ t ↓ ∃αbool^{α} D; Γ ⊢ u ↓ T E; Γ ⊢ v ↓ T T ∃-basic}{C ∧ D ∧ E; Γ ⊢ if t then u else v ↓ T}

(↓∀intro) \frac{C; Γ ⊢ t ↓ T α ∉ Γ}{∃αP ∧ ∀α(P ⊃ C); Γ ⊢ t ↓ ∀αP T}

(↓∀elim) \frac{C; Γ ⊢ t ↑ ∀αP T}{C ∧ P_{α}^{a}; Γ ⊢ t ↓ T_{α}^{a}}

(↓∃intro) \frac{C; Γ ⊢ t ↓ T α ∉ Γ}{∃α(C ∧ P); Γ ⊢ t ↓ ∃αP T}

(↓∃elim) \frac{C; Γ ⊢ t ↑ ∃αP T D; Γ, x : T ⊢ u ↓ U α ∉ C, Γ, U}{C ∧ ∃αP ∧ ∀α(P ⊃ D); Γ ⊢ let x = t in u ↓ U}

(↓sub) \frac{C; Γ ⊢ t ↑ T′}{C ∧ (|T′ ≤ T |); Γ ⊢ t ↓ T}

4 Termination proof technique

In this section, we present a general method for proving the strong normalization of β-reduction and rewriting on well-typed terms. It is based on Tait’s method for proving the strong normalization of β-reduction [19]. The idea is to interpret types by particular sets of strongly normalizing terms, called saturated, and prove that every well-typed term belongs to the interpretation of its type.

Following [2], we define the weak-head-β-reduction relation →_{βwh} as the relation such that E[t] →_{βwh} E[u] iff t →_{βh} u and E ∈ E, where the set of elimination contexts E is inductively defined as follows:

E ∈ E ::= [] | E t | fst E | snd E

Definition 1 (Saturated sets). The set SAT of saturated sets is the set of all the sets of terms S such that:

(1) If t ∈ S, then t ∈ SN.

(2) If t ∈ S and t → t′, then t′ ∈ S.

(3) If E[x] ∈ SN, then E[x] ∈ S.

(4) If t ∈ SN, t →_{βh} t′ and E[t′] ∈ S, then E[t] ∈ S. We also define the following operations on sets of terms:

– S_{1} ⇒ S_{2} = {t ∈ T | ∀u ∈ S_{1}, tu ∈ S_{2}}

– S_{1} × S_{2} = {t ∈ T | fst t ∈ S_{1} ∧ snd t ∈ S_{2}} Let N be the set of terms of the form ft, if t then u else v, fst t or snd t. A saturated set S has the neutral term property if s ∈ S whenever s ∈ N and →(s) ⊆ S.

Lemma 1. SAT is a complete lattice for inclusion with ⋃ as lub, ⋂ as glb and SN as greatest element. It is also stable by ⇒ and ×.

All this is more or less well known. See for instance [2]. The key difference with the first author work [8] is that we use saturated sets instead of reducibility candidates. See [14] for a comparison between the two kinds of sets. With reducibility candidates, (4) is replaced by the neutral term property.

Reducibility candidates are saturated but the converse does not hold since candidates are not stable by union. Hence, with candidates, ∃αP T cannot be interpreted as an union, which is essential if one wants to interpret B^{𝔞} as the set of terms of size 𝔞 in order to give precise types to function symbols.

However, reducibility candidates extend well to rewriting and polymorphism since, for proving that ft ∈ S, it suffices to prove that →(ft) ⊆ S. In Lemma 2, we prove that this property still holds with saturated sets when S is the interpretation of an existentially quantified basic type.

Definition 2 (Interpretation of types). A base type interpretation is a function I which, to every pair (B, 𝔞) with B ≠ bool, associates a set I_{B}^{𝔞} ∈ SAT. We extend I to bool by taking I_{bool}^{𝔞} = {t ∈ SN | t↓ ≠ 𝔞^{∗}}. Given such an interpretation, types are interpreted by saturated sets as follows:

– [[B^{a}]]_{μ}^{I} = I_{B}^{aμ} – [[U × V]]_{μ}^{I} = [[U]]_{μ}^{I} × [[V]]_{μ}^{I}

– [[U ⇒ V]]_{μ}^{I} = [[U]]_{μ}^{I} ⇒ [[V]]_{μ}^{I}

– [[∀αP T]]_{μ}^{I} = ⋂_{μ+_{α}^{𝔞}⊧P} [[T]]_{μ+_{α}^{𝔞}}^{I} if ⊢∃αP, [[∀αP T]]_{μ}^{I} = SN otherwise

– [[∃αP T]]_{μ}^{I} = ⋃_{μ+_{α}^{𝔞}⊧P} [[T]]_{μ+_{α}^{𝔞}}^{I} if ⊢∃αP, [[∃αP T]]_{μ}^{I} = ⋂ SAT otherwise

Let I_{B}^{ω} = [[∃αB^{α}]]. A symbol s ∈ C ∪ F is computable if s ∈ [[τ_{s}]]^{I}. A pair (μ, σ) is valid for C; Γ, written (μ, σ) ⊧ C; Γ, if μ ⊧ C and, for all x ∈ dom(Γ), xσ ∈ [[xΓ]]_{μ}^{I}. A base type interpretation I is valid if every constructor is computable and, for every ∃-basic type T, [[T]]_{μ}^{I} has the neutral term property.

Note that I_{bool}^{𝔞} ∈ SAT has the neutral term property and [[T φ]]_{μ}^{I} = [[T]]_{φμ}^{I}.

Theorem 2. Assume that I is a valid base type interpretation and every f ∈ F is computable. If C; Γ ⊢ t : T and (μ, σ) ⊧ C; Γ, then tσ ∈ [[T]]_{μ}^{I}.

Proof. By induction on C; Γ ⊢ t : T. We only detail some cases. (abs) We must prove that s = (λxu)σ ∈ [[T ⇒ U]]_{μ}^{I}. Wlog, we can assume that

x ∉ σ. Then, s = λx(uσ). Let t ∈ [[T]]_{μ}^{I}. We must prove that st ∈ [[U]]_{μ}^{I}. By induction hypothesis, uσ ∈ [[U]]_{μ}^{I}. Let now σ′ = σ+_{x}^{t}. Since (μ, σ′) ⊧ C; Γ, x : T, by induction hypothesis, uσ′ ∈ [[U]]_{μ}^{I}. Hence, st ∈ SN since, by induction on (uσ, t) with →_{lex} as well-founded ordering, →(st) ⊆ SN. Therefore, st ∈ [[U]]_{μ}^{I} since st →_{βh} uσ′ ∈ [[U]]_{μ}^{I} and st ∈ SN.

(if) Let s = (if t then u else v)σ. By induction hypothesis, tσ ∈ I_{bool}^{ω} and t_{i}σ ∈ [[T]]_{μ}^{I}. Since s ∈ N and T is an ∃-basic type, by the neutral term property, it suffices to prove that →(s) ⊆ [[T]]_{μ}^{I}. This follows by induction on (tσ, uσ, vσ) with →_{lex} as well-founded ordering.

(∃elim) We must prove that s = (let x = t in u)σ ∈ [[U]]_{μ}^{I}. Wlog, we can assume that x ∉ σ. Then, s = let x = tσ in uσ. Let σ′ = σ_{x}^{tσ}. By induction hypothesis, tσ ∈ [[∃αP T]]_{μ}^{I}. Since ⊢ C ⊃ ∃αP, there is 𝔞 such that μ+_{α}^{𝔞} ⊧ P and tσ ∈ [[T]]_{μ+_{α}^{𝔞}}^{I}. Therefore, by induction hypothesis, uσ′ ∈ [[U]]_{μ+_{α}^{a}}^{I} = [[U]]_{μ}^{I}.

(sub) By induction on T and T′, one can easily prove that [[T]]_{μ}^{I} ⊆ [[U]]_{μ}^{I} whenever μ ⊧ (|T ≤ U|). ⊓ ⊔

Corollary 1. Assume that I is a valid base type interpretation and every f ∈ F is computable. Then, → is strongly normalizing on Λ(τ).

Corollary 2. Assume that, for all s ∈ C ∪ F, τ_{s} is of the form T ⇒ ∀αB^{α} ⇒ T with T simple, B basic and T an ∃-basic type. If every symbol is computable, then → is strongly normalizing on \overline{Λ}(\overline{τ}).

Proof. It suffices to prove that, for all s, s ∈ [[\overline{τ_{s}}]]^{I}. We have \overline{τ_{s}} = T ⇒ B ⇒ \overline{B}. Let t ∈ [[T]]^{I} and u ∈ I_{B}^{ω}. We must prove that ftu ∈ [[\overline{B}]]^{I}. There is αμ such that u ∈ I_{B}^{αμ}. Assume that T = ∀δP B. Since f : T ⇒ ∀αB^{α} ⇒ T is computable, ftu ∈ [[T]]_{μ}^{I} = ⋃_{μ+_{δ}^{𝔡}⊧P} [[B]]_{μ+_{δ}^{𝔡}}^{I}. Let ν = μ+_{δ}^{𝔡} ⊧ P. We are left to prove that

[[B]]_{ν}^{I} ⊆ [[\overline{B}]]^{I}. We proceed by induction on B. ⊓ ⊔

5 Termination criterion

We now provide conditions to obtain the computability of defined symbols.

A precedence is a quasi-ordering ≥ whose strict part > = ≥ \ ≤ is wellfounded. Let ≃ = ≥ ∩ ≤ be its associated equivalence relation. We assume given a precedence ≥_{B} on B and a precedence ≥_{F} on F. We are going to define some base type interpretation and prove that every function symbol is computable by induction on these precedences.

Assumption: For all c ∈ C, we assume that τ_{c} is of the form^{1} C ⇒ ∀αB^{α} ⇒ B^{a} with C <_{B} B, B ≃_{B} B, a = 0 if |α| = 0, and a = 1 + max(α) if |α| > 0.

Example 2. The type N of natural numbers has constructors 0 : N^{0} and s : ∀αN^{α} ⇒ N^{α+1}. The type L of lists has constructors nil : L^{0} and cons : N ⇒ ∀αL^{α} ⇒ L^{α+1}. The type T of binary trees has constructors leaf : N ⇒ T^{0} and node : ∀αβT^{α} ⇒ T^{β} ⇒ T^{1+max(α,β)}.

We define the base type interpretation as follows:

– I_{B}^{0} = {t ∈ SN | ∀c : C ⇒ ∀αB^{α} ⇒ B^{a}, ∀tu, |t| = |C| ∧ |u| = |α| ∧ t →^{∗} ctu ⇒ t ∈ I_{C}^{ω} ∧ |α| = a = 0}

– I_{B}^{𝔞+1} = {t ∈ SN | ∀c : C ⇒ ∀αB^{α} ⇒ B^{a}, ∀tu, |t| = |C| ∧ |u| = |α| ∧ t →^{∗} ctu ⇒ t ∈ I_{C}^{ω} ∧ a = 1 + max(α) ∧ (∃𝔟) 𝔞 = max(𝔟) ∧ u ∈ I_{B}^{𝔟}}

Lemma 2. I is a valid base type interpretation.

Proof. One can easily check that I_{b}^{𝔞} is saturated and that every constructor is computable. We now prove that [[T]]_{μ}^{I} has the neutral term property whenever T is ∃-basic.

We first remark that, if t ∈ SN and t →^{∗} t′ ∈ I_{B}^{𝔞}, then t ∈ I_{B}^{𝔞}. We prove it by induction on (B, 𝔞) with (>_{B}, >_{D_{κ_{B}}})_{lex} as well-founded ordering. Let c : C ⇒ ∀αB^{α} ⇒ B^{a}, t and u such that |t| = |C|, |u| = |α| and t →^{∗} ctu. By confluence, t′ →^{∗} ct′u′ with tu →^{∗} t′u′. We proceed by case on 𝔞.

– 𝔞 = 𝔱. Then, t′ ↛^{∗} false. Hence, t ↛^{∗} false and t ∈ I_{B}^{𝔞}.

– 𝔞 = 𝔣. Idem.

– 𝔞 = 0. Since t′ ∈ I_{B}^{𝔞}, t′ ∈ I_{C}^{ω} and |α| = a = 0. Since C <_{B} B, by induction hypothesis, t ∈ I_{C}^{ω}. Thus, t ∈ I_{B}^{𝔞}.

– 𝔞 > 0. Since t′ ∈ I_{B}^{𝔞}, t′ ∈ I_{C}^{ω}, a = 1 + max(α) and there are 𝔟 such that 𝔞 = 1+max(𝔟) and u′ ∈ I_{B}^{𝔟}. Since C <_{B} B and 𝔟 < 𝔞, by induction hypothesis, t ∈ I_{C}^{ω} and u ∈ I_{B}^{𝔟}. Thus, t ∈ I_{B}^{𝔞}.

Let now T = ∃αP B be an ∃-basic type. We have S = ⋃_{μ+_{α}^{𝔞}⊧P} [[B]]_{μ+_{α}^{𝔞}}^{I}. We first prove that there are 𝔞 such that ν = μ+_{α}^{𝔞} ⊧ P and →(s) ⊆ S′ = [[B]]_{ν}^{I}. If →(s) = ∅, this is immediate. So, assume that there is t ∈ →(s). Since t ∈ S, there are 𝔞 such that ν = μ+_{α}^{𝔞} ⊧ P and t ∈ S′ = [[B]]_{ν}^{I}. Let now u ∈ →(s). By

1 The order of types is not relevant. We take this order for the sake of simplicity.

confluence, there is v such that t, u →^{∗} v. Since t ∈ S′, we have v ∈ S′. Thus, u ∈ S′ too. Hence, →(s) ⊆ S′.

We now prove that s ∈ S′ whenever →(s) ⊆ S′ by induction on B. ⊓ ⊔

Fig. 3. Matching constraints

(1) α = ε_{x}; x : B^{ε_{x}} ⇝ x : B^{α}

(2) \frac{c : T ⇒ B^{0} B ≠ bool}{α = 0; x : T ⇝ cx : B^{α}} (2’) \frac{c : bool^{c^{∗}}}{α = c^{∗}; ∅ ⇝ c : bool^{α}}

(3) \frac{c : T ⇒ ∀αB^{α} ⇒ B^{1+max(α)} α = a; Γ ⇝ u : B^{α} α ∉ α x : T, Γ are compatible}{α = 1 + max(a); x : T, Γ ⇝ cxu : B^{α}}

Lemma 3. We assume given an injection ε from term variables to size variables. Consider the rules of Figure 3. If α = a; Γ ⇝ t : B^{α} and tσ ∈ I_{B}^{αμ}, then there is ν such that (μ + ν, σ) ⊧ α = a; Γ.

Proof. We say that 𝔞 is minimal for t ∈ [[B]]^{ω} if t ∈ [[B]]^{𝔞} and, for all 𝔟 < 𝔞, t ∉ [[B]]^{𝔟}. We prove the lemma by induction on α = a; Γ ⇝ t : B^{α} with the additional requirement that ν is minimal whenever μ so is.

(1) It suffices to take ε_{x}ν = αμ.

(2) and (2’) It suffices to take ν = ∅.

(3) We have tσ = cxσuσ. Thus, μ is minimal, xσ ∈ [[T]] and there is μ′ minimal such that uσ ∈ I_{B}^{αμ′} and αμ = 1 + max(αμ′). Now, by induction hypothesis, there are ν minimal such that (μ′ + ν, σ) ⊧ α = a; Γ. Since ν are minimal, if xσ ∈ I_{B_{i}}^{ε_{x}ν_{i}} ∩ I_{B_{j}}^{ε_{x}ν_{j}}, then ε_{x}ν_{i} = ε_{x}ν_{j}. Thus, we can define ν = Σν. Since ν is minimal, we are left to prove that (μ + ν, σ) ⊧ α = 1 + max(a); Γ. First, we have μ + ν ⊧ α = 1 + max(a) since αμ = 1 + max(αμ′) = 1 + max(aν). Second, let x ∈ u_{i}. Then, xσ ∈ [[xΓ]]_{ν_{i}}^{I} = [[xΓ]]_{xν}^{I}. ⊓ ⊔

Theorem 3 (Termination criterion). Assume that, for every f ∈ F:

(1) τ_{f} is of the form T ⇒ ∀αB^{α} ⇒ T with T an ∃-basic type;

(2) there is a constraint (β <_{f} α) such that the ordering ≻_{f} defined by αμ ≻_{f} βμ iff μ ⊧ β <_{f} α is well-founded;

(3) for every g ≃_{F} f, τ_{g} is of the form U ⇒ ∀αB^{α} ⇒ U and <_{f}=<_{g}; and, for every rule t = c ⊃ l → r defining f:

(4) l is of the form fxl with |x| = |T | and |l| = |α|;

(5) there are Γ compatible and a such that α = a; Γ ⇝ l : B^{α};

(6) every symbol occurring in r is ≤_{F} f; (7) α = a; x : T , Γ ⊢_{τ^{<}} t : bool^{b};

(8) b = c^{∗}; α = a; x : T , Γ ⊢_{τ^{<}} r : T. where:

(9) for every g <_{F} f, τ_{g}^{<} = τ_{g};

(10) for every g ≃_{F} f, τ_{g}^{<} = U ⇒ ∀α′(α′ <_{f} α)B^{α′} ⇒ U with α′ ∉ α whenever τ_{g} = U ⇒ ∀α′B^{α′} ⇒ U.

Then, → is strongly normalizing on Λ(τ) and \overline{Λ}(\overline{τ}).

Proof. We must prove that, for all f : T ⇒ ∀αB^{α} ⇒ T, t ∈ [[T]], μ and u ∈ I_{B}^{αμ}, ftu ∈ [[T]]_{μ}^{I}. We proceed by induction on (f, αμ, tu) with (>_{F}, ≻_{f}, →_{lex})_{lex} as well-founded ordering. By Lemma 2, it suffices to prove that →(s) ⊆ S. If the reduction takes place in tu, we conclude by induction hypothesis. Assume now that there are fxl → r ∈ R and σ such that xσ = t and lσ = u. We must prove that rσ ∈ [[T]]_{μ}^{I}. After Lemma 3, since Γ are compatible, there is ν such that (μ + ν, σ) ⊧ α = a; Γ. By induction hypothesis, for all g ≤_{F} f, g ∈ [[τ_{g}^{<}]] (considering α as constants interpreted by αμ). Thus, letting η = μ + ν, by Theorem 2, we have tσ ∈ I_{bool}^{bη}. Since tσ →^{∗} c ∈ I_{bool}^{c^{∗∗}}, we have bη = c^{∗∗}. Thus, η ⊧ b = c^{∗} and, by Theorem 2 again, rσ ∈ [[T]]_{η}^{I} = [[T]]_{μ}^{I}. ⊓ ⊔

The size variables α in the type of f (1) represents the sizes of the recursive arguments of f. The user-defined predicate <_{f} in (2) expresses the measure that must decrease in recursive calls. One can for instance take lexicographic or multiset comparisons together with linear combinations of the arguments. The condition (5) provides the constraints on α when a term matches the rule left hand-side l = fxl. The condition (7) implies that the terms t are terminating whenever the arguments of the left hand-side so are. The condition (8) implies that the right hand-side is terminating whenever the arguments of the left handside so are and t →^{∗} c. The fact that t →^{∗} c is expressed by the additional constraint b = c^{∗}. Termination is ensured by doing type-checking in the system ⊢_{τ^{<}} where, by condition (10), function symbols equivalent to f can only be applied to arguments smaller than α in <_{f}. This is in contrast with [8] where a new type system (called the computability closure) restricting the use of (app) must be introduced.

Example 3. We detail the criterion with the second rule of pivot given in the introduction. Let r be the right-hand side of the rule and u (resp. v) be the first (resp. second) branch of if in r.

We take pivot : N ⇒ ∀αL^{α} ⇒ T (α) with T (α) = ∃βγ(α = β + γ)L^{β} × L^{γ}, <_{f} = <, ≻_{f} = >_{ℕ} and le : N ⇒ N ⇒ bool. Let Γ = y : N, l : L^{δ} and Δ = x : N, Γ.

Matching constraint: α = δ + 1; Γ ⇝ cons y l : L^{α} (we take ε_{l} = δ).

We must check that α = δ + 1; Δ ⊢ r : T (α) with pivot : N ⇒ ∀α′(α′ < α)L^{α′} ⇒ T (α′). Let Δ = Γ, z : L^{β} × L^{γ}.

One can easily check that δ < α; Γ ⊢ pivot x l ↑ T (δ), ⊤; Δ ⊢ le y x ↑ bool, ⊤; Δ ⊢ u ↑ L^{β+1} × L^{γ}, ⊤; Δ ⊢ v ↑ L^{β} × L^{γ+1}.

Thus, by (↓sub), β + 1 = β′ ∧ γ = γ′; Δ ⊢ u ↓ L^{β′} × L^{γ′} and β = β′ ∧ γ + 1 = γ′; Δ ⊢ u ↓ L^{β′} × L^{γ′}.

By (↓∃intro), D; Δ ⊢ u ↓ T (α) where D = ∃β′γ′(β + 1 = β′ ∧ γ = γ′ ∧ α = β′ +γ′), and E; Δ ⊢ v ↓ T (α) where E = ∃β′γ′(β = β′ ∧γ +1 = γ′ ∧α = β′ +γ′). Note that D ≡ E ≡ (α = β + γ + 1).

By (↓if), α = β + γ + 1; Δ ⊢ if (le y x) then u else v : T (α).

By (↓∃elim), F; Γ ⊢ r ↓ T (α) where F = δ < α∧(∃βγ(α = β+γ))∧(∀βγ(δ = β + γ ⊃ α = β + γ + 1)).

Therefore, α = δ + 1; Δ ⊢ r : T (α) if ⊢ α = δ + 1 ⊃ F, which is true.

Example 4. Consider the following definition of Mc Carthy’s 91 function:

le x 100 = true ⊃ f x → f (f (plus x 11))
le x 100 = false ⊃ f x → minus x 10

We assume that A contains le : nat × nat ⇒ bool interpreted as expected.

We assume that le : ∀αβN^{α} ⇒ N^{β} ⇒ bool^{le(α,β)}, plus : ∀αβN^{α} ⇒ N^{β} ⇒ N^{α+β}, minus : ∀αβN^{α} ⇒ N^{β} ⇒ ∃γP N^{γ} with P = (α ≤ β ∧ γ = 0) ∨ (α > β ∧ α = β + γ), and f : ∀αN^{α} ⇒ ∃βQN^{β} with Q = (α ≤ 100 ∧ β = 91) ∨ (α > 100 ∧ α = β + 10). Taking Γ = x : N^{α}, we get that ⊤; Γ ⊢ le x 100 : bool^{le(α,100)}. The condition le(α, 100) = t is equivalent to α ≤ 100, hence the termination.

6 Conclusion and future work

We extended the simply typed part of [8] with conditional rewriting and explicit quantifications and constraints over size annotations. This allows to precisely describe the relation between the size of the output of a function and the size of its inputs. This also provides a powerful termination criterion for the combination of β-reduction and higher-order conditional rewriting, based on type-checking and constraint solving. To our knowledge, this is the first termination criterion for higher-order conditional rewriting taking into account conditions in termination. We plan to extend this work in various directions:

– As in [22], we did not consider constructors with recursive arguments of higher-order type since this is already studied in [8]. The integration of both works should not create too much difficulties. We already have preliminary results in this direction.

– The complexity of Presburger arithmetic is high. Although it is not so important in our case since the constraints we consider are small (rule right-hand sides are generally not very big terms), it would be interesting to study the complexity in more details, depending on the allowed size annotations.

– Our long term goal is to extend the present work to polymorphic and dependent type systems that serve as basis for proof assistants like Coq, e.g. the Calculus of Algebraic Constructions [9].

– We assume that constrained types of function symbols are given and check that they imply termination. It would be very interesting to infer these constraints automatically.

References

1. A. Abel. Termination and productivity checking with continuous types. In Proc. of TLCA’03, LNCS 2701.

2. A. Abel. Termination checking with types. Theoretical Informatics and Applications, 38(4):277–319, 2004.

3. G. Barthe, M. J. Frade, E. Giménez, L. Pinto, and T. Uustalu. Type-based termination of recursive definitions. Mathematical Structures in Computer Science, 14(1):97–141, 2004.

4. G. Barthe, B. Grégoire, and F. Pastawski. Practical inference for type-based termination in a polymorphic setting. In Proc. of TLCA’05, LNCS 3461.

5. F. Blanqui. Decidability of type-checking in the Calculus of Algebraic Constructions with size annotations. In Proc. of CSL’05, LNCS 3634.

6. F. Blanqui. Rewriting modulo in Deduction modulo. In Proc. of RTA’03, LNCS 2706.

7. F. Blanqui. Termination and confluence of higher-order rewrite systems. In Proc. of RTA’00, LNCS 1833.

8. F. Blanqui. A type-based termination criterion for dependently-typed higher-order rewrite systems. In Proc. of RTA’04, LNCS 3091.

9. F. Blanqui. Definitions by rewriting in the Calculus of Constructions. Mathematical Structures in Computer Science, 15(1):37–92, 2005.

10. F. Blanqui, C. Kirchner, and C. Riba. On the confluence of λ-calculus with conditional rewriting. In Proc. of FoSSaCS’06, LNCS 3921.

11. W. N. Chin and S. C. Khoo. Calculating sized types. Journal of Higher-Order and Symbolic Computation, 14(2-3):261–300, 2001.

12. R. Davies and F. Pfenning. Intersection types and computational effects. In Proc. of ICFP’00, SIGPLAN Notices35(9).

13. M. Fischer and M. Rabin. Super-exponential complexity of presburger arithmetic. In Proceedings of the SIAM-AMS Symposium in Applied Mathematics, 1974.

14. J. Gallier. On Girard’s “Candidats de Réductibilité”. In P.-G. Odifreddi, editor, Logic and Computer Science. North-Holland, 1990.

15. J. Hughes, L. Pareto, and A. Sabry. Proving the correctness of reactive systems using sized types. In Proc. of POPL’96.

16. J. W. Klop, V. van Oostrom, and F. van Raamsdonk. Combinatory reduction systems: introduction and survey. Theoretical Computer Science, 121:279–308, 1993.

17. R. Mayr and T. Nipkow. Higher-order rewrite systems and their confluence. Theoretical Computer Science, 192(2):3–29, 1998.

18. M. Presburger. ber die vollst ndigkeit eines gewissen systems der arithmetik ganzer zahlen, in welchem die addition als einzige operation hervortritt. In Sprawozdanie z I Kongresu Matematykow Krajow Slowcanskich, Warszawa, Poland, 1929.

19. W. W. Tait. A realizability interpretation of the theory of species. In R. Parikh, editor, Proceedings of the 1972 Logic Colloquium, volume 453 of Lecture Notes in Mathematics, 1975.

20. V. van Oostrom and F. van Raamsdonk. Comparing Combinatory Reduction Systems and Higher-order Rewrite Systems. In Proc. of HOA’93, LNCS 816.

21. H. Xi. Dependent types in practical programming. PhD thesis, Carnegie-Mellon, Pittsburgh, United States, 1998.

22. H. Xi. Dependent types for program termination verification. Journal of Higher-Order and Symbolic Computation, 15(1):91–131, 2002.