Specification and Verification of a Formal System for Structurally Recursive Functions

Andreas Abel

Department of Computer Science, University of Munich

                  abel@informatik.uni-muenchen.de

Abstract. A type theoretic programming language is introduced that is based on lambda calculus with coproducts, products and inductive types, and additionally allows the definition of recursive functions in the way that is common in most functional programming languages. A formal system is presented that checks whether such a definition is structurally recursive and a soundness theorem is shown for this system. Thus all functions passing this check are ensured to terminate on all inputs. For the moment only non-mutual recursive functions are considered.

1 Introduction

In lambda calculi with inductive types the standard means to construct a function over an inductive type is the recursor. This method, however, has several drawbacks, as discussed, e.g., in [Coq92]. One of them is that it is not very intuitive: For instance it is not obvious how to code the following “division by 2”-function with recursors:

half 0 = 0 half 1 = 0 half n+2 = (half n)+1

Therefore an alternative approach has been investigated: recursive definitions with pattern matching, as they are common in nearly all functional programming languages. To define total functions, they have to satisfy two conditions:

1. The patterns have to be exhaustive and mutually exclusive. We will not focus on this point further since the foetus language we introduce in Sect. 2 uses only case expressions and thus this condition is always fulfilled. For a discussion see [Coq92].

2. The definition must be well-founded, which means that for all arguments the function value has a well-founded computation tree. This can be ensured if one can give a termination ordering for that function, i.e., a ordering with respect to which its arguments in each recursive call are smaller than the input parameters of that function.

We will restrict ourselves to structural orderings, since they can be checked automatically and still allow the definition of a large number of total functions directly. By introducing an extra wellfounded argument (which is decreased structurally in each recursive call), one can code any function that can be proven total in Martin-Löf’s Type Theory (MLTT [Mar84]) or an equivalent system.

We say an expression s is structurally smaller than an expression t if s appears in the computation tree of t. Sometimes this is called “component relation”.

In [Abe98] the implementation of the termination checker foetus has been presented. This checker, which accepts structurally recursive functions of the kind described above, has been reimplemented as part of Agda by C. Coquand [Coq00]. In [AA02] a semantics for the foetus language has been defined, and for all types the wellfoundedness wrt. the structural ordering on values has been proven. Furthermore a function has been defined to be (semantically) structurally recursive if it terminates on input value w under the condition that it terminates on all values v that are smaller than w wrt. a structural ordering on the value domain. Thus we could prove termination for all terms by assuming that all named functions are structurally recursive.

This article is meant to close a gap that has remained in [AA02]. For it to be self-contained, we repeat the definitions of the foetus language, operational and value semantics as far as we refer to them in this presentation. (Old definitions are laid out in tables.) The new contributions start with a formalization of the termination checker in the form of a predicate “sr” (syntactically structurally recursive) on terms. This extends the derivation system for structural ordering on terms. First we will show that the ordering on terms is reflected by that on the values, i.e., evaluation preserves the ordering. Second we will prove that all functions captured by the sr-predicate are indeed total, i.e., that they terminate on all inputs. Thus we establish the soundness of our system formally.

At the moment we exclude mutually recursive functions, since they require more sophisticated concepts. For non-mutual recursion—which we will treat here—the proof is beautiful in its straightforwardness. The specification consists mostly of strictly positive inductive definitions, and the proof is constructive. Also, since most details have been completely formalized, we can almost directly implement it in a system like MLTT. On the final theorem, “all closed terms evaluate to a good value”, we can apply program extraction. Thus we would obtain an interpreter for the lambda calculus with inductive types and recursive functions, for which termination is verified.

1.1 Related Work

Giménez also presents a syntactic criterion for structural recursion which he calls “guarded-by-destructors” [Gim95]. He gives, however, no proof for the soundness of his criterion. Furthermore we believe that our approach is more concise and more flexible in how functions can be defined.

Jouannaud, Okada [JO97] and later also Blanqui [BJO01] deal with inductive types, too, but in the area of extensible term rewriting systems. Since they also do not handle mutual recursion, our present approach seems to have the same expressive power than their Extended General Schema. But both approaches differ considerably in the notion of a recursive call with a smaller argument.

Telford and Turner [TT99] are investigating Strong Functional Programming, i.e., functional programming languages where only terminating functions can be defined. Technically they use abstract interpretations to ensure termination. Since they count constructors and destructors, they can handle a wider class of functions. I consider their approach as very promising but it seems that it is not yet fully formalized and verified. Maybe the ideas of my work presented here could be transferred to their approach.

Christoph Walther has invented reduction checking, which is sometimes referred to as “Walther recursion” [MA96]. Here functions are not only examined whether they are terminating, but also whether they are reducers or preservers, i.e., whether the output of the function is (strictly) smaller than the input. This information can be used to check termination of nested recursive functions or just for functions which decrease their input via a previously defined function in a recursive call. It seems that my system could be extended to reduction checking in a straightforward way, since I already use assumptions (dependencies) in my judgements (see Def. 5).

Finally, Pientka and Pfenning [PP00] have implemented termination and reduction checking for the Twelf system [PS98] based on LF [HHP93]. Although coming from the realm of logic programming, their formal system that implements the check is similar to mine. However, theirs is constructor based and mine is destructor based. They justify the stringency of their system by a cut admissibility proof, but have not shown soundness yet.

In comparision with the work discussed above, the main contribution of this article is giving a clear and straightforward soundness proof for my system, based on a semantics for the judgements of my formal system.

1.2 Notational conventions

We are using vectors to simplify our notation. If we have a family of (meta) expressions E_{1}, E_{2}, …, E_{n} we write E for the whole sequence. S_{n} denotes the set of permutations on {1, …, n}. Furthermore we use the denotations

X, Y, Z for type variables
ρ, σ, τ  for types
g, x, y, z for term variables
r, s, t, a for terms
f, u, v, w for values
c  for closures
e  for environments
p, q  for atoms (containing a relation between terms)

We use rule notation for inductive definitions, but also for propositions (cf. Lemma 1). On top of the bar we put the premises and on bottom the conclusion(s), in both cases to be read as a conjunction.

2 The foetus Language and its Semantics

In [AA02] we already introduced the term language foetus and its semantics. Here we will only briefly repeat the definitions and main results (see Tables 2 and 3). The types are constructed by type variables X, Y, Z, … and the type constructors Σ (finite sum), Π (finite product), → (function space) and μ (strictly positive inductive type).

Types Ty(X) (over a finite list of type variables X)

τ, σ, σ ::= X_{i} | Σσ | Πσ | σ → τ | μX_{n}.σ  precedence: Π, Σ, →, μ
0 := Σ()  empty sum
1 := Π()  empty product
Ty := Ty()  closed types

Contexts

Γ = x_{1}^{σ1} , …, x_{n}^{σn} ∈ Cxt x_{i}pairwise distinct

Terms Tm^{σ}[Γ] of closed type σ in context Γ

(var) {Γ ∈ Cxt  x ∉ Γ \atop x ∈ Tm^{σ}[Γ, x^{σ}]}  (weak) {t ∈ Tm^{σ}[Γ]  x ∉ Γ \atop t ∈ Tm^{σ}[Γ, x^{τ}]}

(in)

t ∈ Tm^{σj} [Γ] σ ∈ Ty
in_{j}(t) ∈ Tm^{Σσ}[Γ]

(case)

t ∈ Tm^{Σσ}[Γ] t_{i} ∈ Tm^{ρ}[Γ, x_{i}^{σi}]
case(t, x_{1}^{σ1} .t_{1}, …, x_{n}^{σn} .t_{n}) ∈ Tm^{ρ}[Γ]
(tup) {t_{i} ∈ Tm^{σi} [Γ] for 1 ≤ i ≤ n \atop (t_{1}, …, t_{n}) ∈ Tm^{Πσ}[Γ]}  (pi) {t ∈ Tm^{Πσ}[Γ] \atop pi_{j}(t) ∈ Tm^{σj} [Γ]}

(lam)

{t ∈ Tm^{τ} [Γ, x^{σ}] \atop λx^{σ}.t ∈ Tm^{σ→τ} [Γ]}

(rec)

t ∈ Tm^{τ} [Γ, g^{Πσ→τ} , x^{Πσ}]  ⊢ g(x) sr t
fun g^{Πσ→τ} (x^{Πσ}) = t ∈ Tm^{Πσ→τ} [Γ]
(app) {t ∈ Tm^{σ→τ} [Γ]  s ∈ Tm^{σ}[Γ] \atop t s ∈ Tm^{τ} [Γ]}

(fold)

t ∈ Tm^{σ(μX.σ)}[Γ]
fold(t) ∈ Tm^{μX.σ}[Γ]

(unfold)

t ∈ Tm^{μX.σ}[Γ]
unfold(t) ∈ Tm^{σ(μX.σ)}[Γ]

Syntactic sugar for fun g(y^{Πσ}) = t[x_{1} := pi_{1}(y), …, x_{n} := pi_{n}(y)]

t ∈ Tm^{τ} [Γ, g^{Πσ→τ} , x_{1}^{σ1} , …, x_{n}^{σn}] ⊢ g(y) sr t[x_{1} := pi_{1}(y), …, x_{n} := pi_{n}(y)]

fun g(x_{1}^{σ1} , …, x_{n}^{σn}) = t ∈ Tm^{Πσ→τ} [Γ]

Table 2. The foetus Language

2.1 Recursive Terms

The terms inhabiting closed types are the terms of a lambda calculus with sums and products plus folding and unfolding for inductive types plus structurally recursive terms (see Table 2). Here fold and unfold establish the isomorphism between μX.σ and σ(μX.σ). The rule (rec) introduces a recursive term resp. named function that solves the equation g = λx.t in place of g.^{1} We require the argument of g to be of product type to simplify the handling of lexicographic termination orderings.^{2}

In the function body t the identifier g may only appear structurally recursive with respect to parameter x. This property is ensured by the judgement

Δ ⊢ g(x) sr t

Read “under the dependencies Δ the function g with parameter x is structurally recursive in t”. For example the following judgement is valid

x′ <^{Tm} x ⊢ g(x) sr g x′

which expresses that a recursive call g x′ in a function g is admissible for the function g(x) to be structurally recursive, if the argument x′ of the call is strictly smaller than the parameter x of the function. A function g is structurally recursive, if it is structurally recursive in its whole body t under no assumptions (dependencies), i.e., if all calls are decreasing.

We will present the proof rules for <^{Tm} and sr in Sect. 3. The intention is that is defined simultaneously with the terms.

2.2 Operational Semantics

We define a big step operational semantics “↓” as a relation between closures and values. The intention behind values is that they are the results of the evaluation process. Closures are (open) terms paired with a mapping of the free variables to values (environment). Closures of the form f@u (value applied to values) are convenient to define the operational semantics without casting values back to terms.

Table 3 presents the operational semantics. (For reasons of readability we leave out type and context annotations wherever possible.) Our strategy is callby-value (see rule (opapp)) and we do not evaluate under λ and recursive terms (see rules (oplam) and (oprec)). Furthermore ↓ is deterministic, i.e., c ↓ v and c ↓ v′ imply v = v′. Thus we can invert all rules for ↓. We denote the inversion of the rule (X) by (X^{−1}).

1 In the literature one often finds the notation μg.λx.t, expressing that the function is the smallest fixed-point of λx.t[Γ, g]. Our notation is inspired by the functional programming language SML.

2 Note that 1-element tuples are allowed as arguments, so this is not really a restriction.

Values Val^{σ}, environments Env[Γ] and closures Cl^{τ}

v, w, v ∈ Val ::= in_{j}(v) | (v_{1}, …, v_{n}) | fold(v) | ⟨λx.t; e⟩ | ⟨fun g(x) = t; e⟩
Env[Γ] := {x_{1} = v_{1}, …, x_{n} = v_{n} : v_{i} ∈ Val^{σi} }  Γ = x_{1}^{σ1} , …, x_{n}^{σn}
Cl^{τ} := {⟨t; e⟩ : ∃Γ ∈ Cxt. t ∈ Tm^{τ} [Γ] ∧ e ∈ Env[Γ]}
∪ {f@u : f ∈ Val^{σ→τ} , u ∈ Val^{σ}}  (“@” is a new symbol)

Notation

terms: t^{σ}[Γ] expresses t, where t ∈ Tm^{σ}[Γ] (σ, Γ optional)
values: v^{σ} expresses v, where v ∈ Val^{σ}

Operational Semantics ↓^{σ}⊆ Cl^{σ} × Val^{σ}

(opvar) ⟨x; e, x = v⟩ ↓ v (opweak) {⟨t[Γ]; e⟩ ↓ v \atop ⟨t[Γ, x]; e, x = w⟩ ↓ v} (opin) {⟨t; e⟩ ↓ v \atop ⟨in_{j}(t); e⟩ ↓ in_{j}(v)}

(opcase) {⟨t^{Σσ}[Γ]; e⟩ ↓ in_{j}(w^{σj})  ⟨t_{j}^{τ} [Γ, x_{j}^{σj}]; e, x_{j} = w⟩ ↓ v^{τ} \atop ⟨case(t, x.t); e⟩ ↓ v}

(optup) {⟨t_{i}; e⟩ ↓ v_{i} for 1 ≤ i ≤ n \atop ⟨(t); e⟩ ↓ (v)}  (oppi) {⟨t; e⟩ ↓ (v) \atop ⟨pi_{j}(t); e⟩ ↓ v_{j}}

(oplam) ⟨λx.t; e⟩ ↓ ⟨λx.t; e⟩  (oprec) ⟨fun g(x) = t; e⟩ ↓ ⟨fun g(x) = t; e⟩
(opapp) {⟨t; e⟩ ↓ f  ⟨s; e⟩ ↓ u  f@u ↓ v \atop ⟨t s; e⟩ ↓ v}

(opappvl) {⟨t; e, x = u⟩ ↓ v \atop ⟨λx.t; e⟩@u ↓ v}  (opappvr) {⟨t; e, g = ⟨fun g(x) = t; e⟩, x = u⟩ ↓ v \atop ⟨fun g(x) = t; e⟩@u ↓ v}

(opfold)

⟨t; e⟩ ↓ v
⟨fold(t); e⟩ ↓ fold(v)

(opunfold)

⟨t; e⟩ ↓ fold(v)
⟨unfold(t); e⟩ ↓ v

Table 3. Values and Operational Semantics

2.3 Semantics and Structural Ordering on Values

We give a semantics of the types in foetus that captures the “good” values, i.e. these values that ensure termination. In this sense f will be a good function value if it evaluates to a good result if applied to a good argument.

Definition 1 (Semantics on values). For every closed type σ ∈ Ty the semantics VAL^{σ} ⊆ Val^{σ} contains the good values of type σ. Especially for arrow types:

f ∈ VAL^{σ→τ} ⟺ ∀u ∈ VAL^{σ}. ∃v ∈ VAL^{τ} . f@u ↓ v

More details do not matter at this point. We refer the interested reader to [Abe99], where the construction of this semantics has been carried out, and to [AA02] for an even predicative construction. Note that in both papers VAL^{σ} is denoted with [[σ]].

Definition 2 (Good environment). Let Γ = x_{1}^{σ_{1}}, …, x_{n}^{σ_{n}}. Then

ENV[Γ] := {x_{1} = v_{n}, …, x_{n} = v_{n} : v_{i} ∈ VAL^{σ_{i}} for 1 ≤ i ≤ n}

Definition 3 (Strong evaluation). We say a closure c ∈ Cl^{σ} evaluates strongly to a value v ∈ Val^{σ}, if v is a good value.

c ⇓ v :⟺ c ↓ v & v ∈ VAL^{σ}

For closures of the form c ≡ ⟨t; e⟩ we additionally require that every subterm s of t evaluates strongly ⟨s; e′⟩ ⇓ in environment e′ where e′ is e, a shortening of e or the extension of e by a good value w. We refer to this requirement as the subterm property.

Structural ordering R_{σ,τ} ⊆ VAL^{σ} × VAL^{τ} (R ∈ {<, ≤})

(≤refl) v ≤_{σ,σ} v (Rin) {w R_{ρ,σj} v \atop w R_{ρ,Σσ} in_{j}(v)} (Rtup) {∃j. w R_{ρ,σj} v_{j} \atop w R_{ρ,Πσ} (v)}

(Rarr) {f@u ⇓ v  w R_{ρ,τ} v \atop w R_{ρ,σ→τ} f} (Rfold) {w ≤_{σ,τ(μX.τ)} v \atop w R_{σ,μX.τ} fold(v)}

Admissible rules (besides transitivity)

(≤<) {w <_{ρ,τ} v \atop w ≤_{ρ,τ} v} (Rin’) {in_{j}(v) R w \atop v R w} (Rtup’) {(v) R w \atop v_{j} R w}

(Rarr’) {f R w  f@u ⇓ v \atop v R w} (Rfold’) {fold(v) ≤ w \atop v R w}

Lexicographic ordering ≺_{π,σ}^{k} ⊆ VAL^{Πσ} × VAL^{Πσ} for closed types σ, a permutation π ∈ S_{n} and k ∈ IN

(lex<) {v_{π(k)} < w_{π(k)} \atop (v) ≺_{π,σ}^{k} (w)} (lex≤) {v_{π(k)} ≤ w_{π(k)}  (v) ≺_{π,σ}^{k+1} (w) \atop (v) ≺_{π,σ}^{k} (w)}

Table 4. Ordering on Values

Table 4 shows the definition of the lexicographic extension ≺_{π} of the structural ordering on values, which we obtain from ≺_{π}^{k} for k = 1. In [AA02] we proved that it is wellfounded. We will exploit this fact later in the proof of “f terminates at input v”, doing noetherian induction. Thus we have the hypothesis for all smaller v′ ≺ v at hand for the proof of termination at v.

3 A Formal System for Structural Recursion

In this section we will introduce the foetus termination calculus, but first motivate it by an example. Consider the following foetus implementation of the addition of ordinal numbers. We define two type abbreviations

Nat ≡ μ X.1 + X
Ord ≡ μ X.1 + X + (Nat → X)

The constructors of Ord and the addition function are

O ≡ fold(in_{1}())
S(v) ≡ fold(in_{2}(v))
Lim(f) ≡ fold(in_{3}(f))
add ≡ λx^{Ord}. fun add^{Π(Ord)→Ord}(y^{Ord})=

case(unfold(y), 1. x,

n^{Ord}. S(add(n)),
f^{Nat→Ord}. Lim(λz^{Nat}. add(f z)))

(The superindex 1 in the first branch of the case expression is just a type annotation, stating that the variable can only contain the empty tuple.)

In our term language we can only define add, if add is structurally recursive in its function body. For this we require that in all recursive calls the argument is structurally smaller than the input parameter of the function. In our case this gives us the proof obligations

1. n < y
2. f z < y

Our approach works as follows: We descend into the function body until we reach the recursive calls, and on our way we collect dependency information between variables. These dependencies are generated whenever we pass a case-expression. Thus for call 1 we get the dependency n ≤ unfold(y). From this we infer n < y since we require a folding step to increase the structural ordering strictly.

For call 2 we infer f z < y from f ≤ unfold(y). We justify this by f z ≤ f. The latter is valid since we regard functions as (possibly infinitely branching) trees and application as selection of one branch.

The formalization of the above informally described method consists of three relations on terms:

1. the structural ordering <^{Tm},

2. its lexicographic extension ≺^{Tm} (needed e.g. for the Ackermann function) and

3. the predicate of structural recursiveness “sr”.

3.1 Structural Ordering on Terms

In the following we will make precise the definition of the structural ordering on terms and give rules that allow us to derive a relation between two terms under a given set of dependencies.

Right hand side rules (R ∈ {<^{Tm}, ≤^{Tm}}):

(RcaseR)

Δ, x_{i} ≤^{Tm} s ⊢ s_{i} R t for i = 1, ..., n
Δ ⊢ case(s, x.s) R t

(RpiR)

{Δ ⊢ s R t \atop Δ ⊢ pi_{j}(s) R t}

(RappR)

{Δ ⊢ s R t \atop Δ ⊢ s a R t}

(RunfR)

Δ ⊢ s ≤^{Tm} t
Δ ⊢ unfold(s) R t

Left hand side rules (R ∈ {<^{Tm}, ≤^{Tm}}):

(RcaseL)

Δ, x_{i} ≤^{Tm} t, y R t_{i}, Δ′ ⊢ p for i = 1, ..., n
Δ, y R case(t, x.t), Δ′ ⊢ p

(RpiL)

{Δ, y R t, Δ′ ⊢ p \atop Δ, y R pi_{j}(t), Δ′ ⊢ p}

(RappL)

{Δ, y R s, Δ′ ⊢ p \atop Δ, y R s a, Δ′ ⊢ p}

(RunfL)

Δ, y <^{Tm} t, Δ′ ⊢ p
Δ, y R unfold(t), Δ′ ⊢ p

Reflexivity and transitivity:

(≤^{Tm}refl) Δ ⊢ t ≤^{Tm} t

(<^{Tm}transL)

Δ ⊢ s R t  y <^{Tm} s ∈ Δ  R ∈ {<^{Tm}, ≤^{Tm}}
Δ ⊢ y <^{Tm} t

(<^{Tm}transR)

Δ ⊢ s <^{Tm} t  y R s ∈ Δ  R ∈ {<^{Tm}, ≤^{Tm}}
Δ ⊢ y <^{Tm} t
(≤^{Tm}trans) {Δ ⊢ s R t  y S s ∈ Δ  R, S ∈ \{<^{Tm}, ≤^{Tm}\} \atop Δ ⊢ y ≤^{Tm} t}

Table 5. Structural ordering on Terms

Declaration 1 (Structural ordering). The structural ordering on terms <^{Tm} and its non-strict version ≤^{Tm} are defined as families of relations indexed over a pair of types: For all σ, τ ∈ Ty we define

<_{σ,τ}^{Tm} ⊆ Tm^{σ} × Tm^{τ}
≤_{σ,τ}^{Tm} ⊆ Tm^{σ} × Tm^{τ}

For purposes of readability we will generally omit the indices.

Definition 4 (Dependencies). A set of dependencies Δ consists of relations

y R t where y ∈ TmVar^{σ}, t ∈ Tm^{τ} , R ∈ {<_{σ,τ}^{Tm}, ≤_{σ,τ}^{Tm}}

Definition 5 (Derivation of structural ordering). By the rules in Table 5 we introduce the judgement

Δ ⊢ s R t R ∈ {<^{Tm}, ≤^{Tm}}

Read “under the dependencies Δ we know that s is less (or equal) than t”.

The right hand rules work on the judgements we want to derive, whereas the left hand side rules work on the dependencies, which—in backward reading— are only introduced by the treatment of case statements (rules (RcaseR) and (srcase)—see next section). Therefore the dependencies can be restricted to the form y R^{Tm} t, where y is the fresh variable introduced for one clause in the case statement. Typically t, the term that is analyzed by the case expression, will be of the form unfold(t′), hence of the left-rules (<^{Tm}unfL) will be the one mostly used in practice. To see the system “in action”, we give derivations of the proof obligations for add (omitting the superindex ^{Tm}):

\overline{≤^{Tm}refl} ; n < y ⊢ y ≤ y

\overline{<^{Tm}transL}

n < y ⊢ n < y

\overline{≤^{Tm}unfL}
n ≤ unfold(y) ⊢ n < y

\overline{≤^{Tm}refl} ; f < y ⊢ y ≤ y

\overline{<^{Tm}transL}

f < y ⊢ f < y

\overline{≤^{Tm}unfL}
f ≤ unfold(y) ⊢ f < y
\overline{<^{Tm}appR}
f ≤ unfold(y) ⊢ f z < y

The rule (<^{Tm}caseL) is needed for nested case statements, as for instance in the following curious implementation of the “half”-function:

fun half^{Nat→Nat}(n^{Nat})= case(unfold(case(unfold(n), 1. n,

n_{1}^{Nat}. n_{1})),
1. O,
n_{2}^{Nat}. S(half(n_{2})))

The obligation n_{2} <^{Tm} n is proven as follows:

\begin{matrix}… \\ ≤ unfold(n), n_{2} < n ⊢ n_{2} < n \end{matrix} \begin{matrix}… \\ n_{1} ≤ unfold(n), n_{2} < n_{1} ⊢ n_{2} < n \end{matrix}
\overline{<^{Tm}caseL}
n_{2} < case(unfold(n), .n, n_{1}.n_{1}) ⊢ n_{2} < n
\overline{≤^{Tm}unfL}
n_{2} ≤ unfold(case(unfold(n), .n, n_{1}.n_{1})) ⊢ n_{2} < n

3.2 Lexicographic Extension

To handle functions like the Ackermann function, we need extend our calculus to lexicographic orderings. This requires just two additional rules.

Declaration 2 (Lexicographic ordering). Given closed types σ = σ_{1}, …, σ_{n} and a permutation π ∈ S_{n} we define the relation

(s_{1}, ..., s_{n}) ≺_{π,σ}^{Tm} t where s_{1} ∈ Tm^{σ_{1}}, …, s_{n} ∈ Tm^{σ_{n}}, t ∈ Tm^{Πσ}

To enhance readability we will usually omit the second index σ.

By this definition we mean that term (s) is lexicographically smaller than term t w.r.t. a permutation π of the components. Note that the left hand side must be a tuple syntactically, whereas the right hand side may be any term of product type.

Definition 6 (Derivation of lexicographic ordering). By the following rules we introduce an auxiliary judgement

Δ ⊢^{k} (s) ≺_{π}^{Tm} t 1 ≤ k ≤ n = |s|

In case of k = 1 we just write

Δ ⊢ (s) ≺_{π}^{Tm} t

Read “under the dependencies Δ we know that (s) is lexicographically smaller than t w.r.t. the permutation π”.

(lex<^{Tm}) {Δ ⊢ s_{π(k)} <^{Tm} pi_{π(k)}(t) \atop Δ ⊢^{k} (s) ≺_{π}^{Tm} t}

(lex≤^{Tm}) Δ ⊢ s_{π(k)} ≤^{Tm} pi_{π(k)}(t) Δ ⊢^{k+1} (s) ≺_{π}^{Tm} t

Δ ⊢^{k} (s) ≺_{π}^{Tm} t

This encodes the standard lexicographic ordering. We start in comparing the first component (k = 1) of tuple (s) with tuple t. If it is only non-strictly smaller, we have to consider the next component (k ⇝ k + 1). The terms “first” and “next” have to be seen relatively to the permuation π.

3.3 Structural Recursiveness

As a frame for the derivation system for size relations on terms, we now define the judgement “sr” that we introduced in Sect. 2. Roughly described, a function g will be structurally recursive in a term t, if it is so in all subterms of t and is called recursively only with smaller arguments (see rule (srapprec)). This is were a reference to the judgement “≺^{Tm}” is made.

Definition 7 (Derivation of structural recursiveness). We introduce the judgement

Δ ⊢ g(x) sr_{π} t where g ∈ TmVar^{σ→τ}, x ∈ TmVar^{σ}, t ∈ Tm^{τ},

read “under the dependencies Δ the function g with parameter x is structurally recursive in t w.r.t. the permutation π”, by the following rules.

(srvar) {y ≠ g \atop Δ ⊢ g(x) sr_{π} y} (srweak) {Δ ⊢ g(x) sr_{π} t[Γ] \atop Δ ⊢ g(x) sr_{π} t[Γ, x]} (srin) {Δ ⊢ g(x) sr_{π} t \atop Δ ⊢ g(x) sr_{π} in_{j}(t)}

(srcase)

Δ ⊢ g(x) sr_{π} s Δ, x_{i} ≤^{Tm} s ⊢ g(x) sr_{π} t_{i} for i=1, ..., |t|
Δ ⊢ g(x) sr_{π} case(s, x.t)
(srtup) {Δ ⊢ g(x) sr_{π} t_{i} for i=1, ..., |t| \atop Δ ⊢ g(x) sr_{π} (t)}  (srpi) {Δ ⊢ g(x) sr_{π} t \atop Δ ⊢ g(x) sr_{π} pi_{j}(t)}

(srlam) {Δ ⊢ g(x) sr_{π} t  y ∉ \{g, x\} \atop Δ ⊢ g(x) sr_{π} λy. t}  (srapp) {Δ ⊢ g(x) sr_{π} t  Δ ⊢ g(x) sr_{π} s \atop Δ ⊢ g(x) sr_{π} t s}

(srapprec) {Δ ⊢ g(x) sr_{π} (a)  Δ ⊢ (a) ≺_{π}^{Tm} x \atop Δ ⊢ g(x) sr_{π} g(a)}

(srfold)

Δ ⊢ g(x) sr_{π} t
Δ ⊢ g(x) sr_{π} fold(t)

(srunfold)

Δ ⊢ g(x) sr_{π} t
Δ ⊢ g(x) sr_{π} unfold(t)

Note that g, x and π remain fixed in all rules. Furthermore, since there is no rule for recursive terms and since “sr” is used in the term definition, in our system a nested definition of functions, and thus mutual recursion, is not possible.

Definition 8 (Syntactically structurally recursive). We define a recursive term fun g(x)=t to be syntactically structurally recursive,

Δ ⊢ g(x) sr t

if there is a permutation π s.th. Δ ⊢ g(x) sr_{π} t.

As an example we show that add is a definable term in the foetus system. Expanding the syntactic sugar and the abbreviations and omitting some type annotations the term becomes

λx. fun add(ȳ^{Π(Ord)})=case(unfold(pi_{1}(ȳ)),
. x,
n. fold(in_{2}(add(n))),
f. fold(in_{3}(λz. add(f z))))

To prove add ∈ Tm^{Ord→Π(Ord)→Ord} we have to show that

⊢ add(ȳ) sr_{π} case(…)

where π is the identical permutation on S_{1}. We infer our goal by (srcase), obtaining four subgoals:

– Head term:

ȳ ≠ add

\overline{srvar}

⊢ add(ȳ) sr_{π} ȳ

\overline{srpi}

⊢ add(ȳ) sr_{π} pi_{1}(ȳ)

\overline{srunfold}

⊢ add(ȳ) sr_{π} unfold(pi_{1}(ȳ))

– Side term 1:

x ≠ add

\overline{srvar}

≤^{Tm} unfold(pi_{1}(ȳ)) ⊢ add(ȳ) sr_{π} x

– Side terms 2 and 3: We prove them by reusing the derivations for structural ordering in Sect. 3.1, substituting pi_{1}(ȳ) for y in all occurrences.

n ≤^{Tm} unfold(pi_{1}(ȳ)) ⊢ n <^{Tm} pi_{1}(ȳ)

\overline{lex<^{Tm}}

n ≤^{Tm} unfold(pi_{1}(ȳ)) ⊢ (n) ≺_{π}^{Tm} ȳ

\overline{srapprec}

n ≤^{Tm} unfold(pi_{1}(ȳ)) ⊢ add(ȳ) sr_{π} add(n)

\overline{srin}

n ≤^{Tm} unfold(pi_{1}(ȳ)) ⊢ add(ȳ) sr_{π} in_{2}(add(n))

\overline{srfold}

n ≤^{Tm} unfold(pi_{1}(ȳ)) ⊢ add(ȳ) sr_{π} fold(in_{2}(add(n)))

f ≤^{Tm} unfold(pi_{1}(ȳ)) ⊢ f z <^{Tm} pi_{1}(ȳ)
\overline{lex<^{Tm}}
f ≤^{Tm} unfold(pi_{1}(ȳ)) ⊢ (f z) ≺_{π}^{Tm} ȳ

\overline{srapprec}

z ∉ {add, ȳ} f ≤^{Tm} unfold(pi_{1}(ȳ)) ⊢ add(ȳ) sr_{π} add(f z)

\overline{srlam}

f ≤^{Tm} unfold(pi_{1}(ȳ)) ⊢ add(ȳ) sr_{π} λz. add(f z)

\overline{srin}

f ≤^{Tm} unfold(pi_{1}(ȳ)) ⊢ add(ȳ) sr_{π} in_{3}(λz. add(f z))

\overline{srfold}

f ≤^{Tm} unfold(pi_{1}(ȳ)) ⊢ add(ȳ) sr_{π} fold(in_{3}(λz. add(f z)))

4 Soundness of the Structural Ordering

In this section we show that the ordering on values corresponds to the structural ordering on terms. We accomplish this by proving that evaluation preserves the structural ordering. To this end, we give an interpretation of the judgement Δ ⊢ s R^{Tm} t:

Definition 9 (Weak and strong interpretation of the structural ordering). We define the propositions “environment e satisfies (weakly) the relation s R^{Tm} t for the terms s and t” and “e satisfies the dependencies Δ”:

\begin{aligned}e ⊨^{wk} s R^{Tm} t & :⟺ & ∀v, w. ⟨s; e⟩ ⇓ v → ⟨t; e⟩ ⇓ w → v R w \\ e ⊨ s R^{Tm} t & :⟺ & ∃v, w. ⟨s; e⟩ ⇓ v & ⟨t; e⟩ ⇓ w & v R w \\ e ⊨ Δ & :⟺ & ∀p ∈ Δ. e ⊨ p \end{aligned}

Strong satisfaction of an atom p of the form s R^{Tm} t carries evidence that s and t are strongly evaluating, whereas weak satisfaction needs proof of this. We will interpret atoms in the dependencies (left hand side) strongly and the concluded atom (right hand side) weakly. The reason for this assymetry lies in the architecture the sr-judgement. Interpreting terms t for which the judgment Δ ⊢ g(x) sr t holds as strongly terminating—which we will do in Sect. 5—we can read off the definition of sr that only strongly evaluating terms enter the dependencies.

Lemma 1 (Weakening). Extending the environment does not destroy satisfaction of dependencies.

{e ⊨^{wk} p \atop e, x = v ⊨ p}  {e ⊨ Δ \atop e, x = v ⊨ Δ}

Proof. Since by the definition of contexts and environments x must be a new variable, it does not appear in e and thus not in any of the terms in p or Δ.

Theorem 1. The structural ordering on terms and its lexicographic extension are preserved by the operational semantics.

{Δ ⊢ p \atop ∀e ⊨ Δ. e ⊨^{wk} p}

Proof. By induction on Δ ⊢ p. Right hand side rules (R ∈ {<^{Tm}, ≤^{Tm}}):

(RcaseR) We have to show

∀i, e′ ⊨(Δ, x_{i} ≤^{Tm} s). e′ ⊨^{wk} s_{i} R^{Tm} t e ⊨Δ ⟨case(s, x.s); e⟩ ⇓ v ⟨t; e⟩ ⇓ w

v R w

The assumption ⟨case(s, x.s); e⟩ ⇓ entails by (opcase^{−1}) ⟨s; e⟩ ↓ in_{j}(v′), and since s is a subterm of case(s, x.s), by definition 3 also in_{j}(v′) ∈ VAL. By an instance of the induction hypothesis using j and e′ ≡ (e, x_{j} = v′) (which is of course a good environment) we obtain e′ ⊨^{wk} s_{j} R^{Tm} t (*) leaving us four subgoals.

1. e′ ⊨ Δ: by weakening (lemma 1)

2. ⟨x_{j}; e′⟩ ⇓ v′: by (opvar)

3. ⟨s; e′⟩ ⇓ in_{j}(v′): by (opweak)

4. v′ ≤ in_{j}(v′): by (≤in)

Since by (opcase^{−1}) also ⟨s_{j}; e′⟩ ⇓ v and by (opweak) ⟨t; e′⟩ ⇓ w we can infer our goal v R w from (*).

(RpiR) Our goal is

{⟨s; e⟩ ⇓ (v) → ⟨t; e⟩ ⇓ w → (v) R w  ⟨pi_{j}(s); e⟩ ⇓ v_{j}  ⟨t; e⟩ ⇓ w \atop v_{j} R w}

Since (oppi^{−1}) entails ⟨s; e⟩ ⇓ (v) because s is a subterm of pi_{j}(s), we can use the ind.hyp. and achieve our goal using (Rtup’).

(RappR) Here we show

{⟨s; e⟩ ⇓ f → ⟨t; e⟩ ⇓ w → f R w  ⟨sa; e⟩ ⇓ v  ⟨t; e⟩ ⇓ w \atop v R w}

By (opapp^{−1}) and the subterm property ⟨s; e⟩ ⇓ f, ⟨a; e⟩ ⇓ u and f@u ⇓ v. Hence we complete using the ind.hyp. and the rule (Rarr’).

(RunfR) analogously using (opunfold^{−1}) and (Rfold’)

Left hand side rules (R ∈ {<^{Tm}, ≤^{Tm}}): All the goals we have to show are of the form

{∀e′ ⊨ (Δ, q′, Δ′). e′ ⊨^{wk} p \atop ∀e ⊨ (Δ, q, Δ′). e ⊨^{wk} p}

Hence by weakening it suffices to show e′ ⊨ q′ from e ⊨ q for each case, where e′ is e or an extension of e.

(RcaseL) Assume e ⊨ y R case(t, x.t), which expands to the three propositions ⟨y; e⟩ ⇓ v (1), ⟨case(t, x.t); e⟩ ⇓ w (2) and v R w (3). The rule (opcase^{−1}) plus subterm property entails ⟨t; e⟩ ⇓ in_{j}(v′) (2a) and ⟨t_{j}; e, x_{j} = v′⟩ ⇓ w (2b). Our two goals are:

1. e, x_{j} = v′ ⊨ x_{j} ≤^{Tm} t: We prove this by ⟨x_{j}; e, x_{j} = v′⟩ ⇓ v′ (opvar), by (2a) and by v′ ≤ in_{j}(v′) (≤in).

2. e, x_{j} = v′ ⊨ y R t_{j}: By (1), (2b) and (3) using weakening. (RpiL) We expand our goal to

{⟨y; e⟩ ⇓ v  ⟨pi_{j}(t); e⟩ ⇓ w_{j}  v R w_{j} \atop ⟨y; e⟩ ⇓ v  ⟨t; e⟩ ⇓ (w)  v R (w)}

It follows from (oppi^{−1}), subterm property and (Rtup).

(RappL) The expanded goal is

{⟨y; e⟩ ⇓ v  ⟨s a; e⟩ ⇓ w  v R w \atop ⟨y; e⟩ ⇓ v  ⟨s; e⟩ ⇓ f  v R f}

By (opapp^{−1}) and subterm property ⟨s; e⟩ ⇓ f, ⟨a; e⟩ ⇓ u and f@u ⇓ w. Thus v R f follows by (Rarr).

(RunfL) analogously using (opunfold^{−1}) and (Rfold)

Reflexivity and transitivity:

(≤^{Tm}refl) e ⊨^{wk} t ≤^{Tm} t follows from (≤refl). (<^{Tm}transL) We have to show (R ∈ {<, ≤})

{e ⊨^{wk} s R^{Tm} t  e ⊨ y <^{Tm} s  ⟨y; e⟩ ⇓ u  ⟨t; e⟩ ⇓ w \atop u < w}

From e ⊨ y <^{Tm} s we obtain ⟨s; e⟩ ⇓ v and u < v and thus by the first premise v R w. Transitivity of the structural ordering on values implies u < w.

(<^{Tm}transR) analogously (≤^{Tm}trans) analogously

Lexicographic extension:

(lex<^{Tm}) We have the simplified goal

{e ⊨^{wk} s_{π(k)} <^{Tm} pi_{π(k)}(t)  ⟨(s); e⟩ ⇓ (v)  ⟨t; e⟩ ⇓ (w) \atop (v) ≺_{π}^{k} (w)}

By (optup^{−1}) ⟨s_{π(k)}; e⟩ ⇓ v_{π(k)} and by (oppi) ⟨pi_{π(k)}(t); e⟩ ⇓ w_{π(k)} hence v_{π(k)} < w_{π(k)}, and the goal (v) ≺_{π}^{k} (w) follows form (lex<).

(lex≤^{Tm}) Our simplified goal is

{e ⊨^{wk} s_{π(k)} ≤^{Tm} pi_{π(k)}(t)  (v) ≺_{π}^{k+1} (w)  ⟨(s); e⟩ ⇓ (v)  ⟨t; e⟩ ⇓ (w) \atop (v) ≺_{π}^{k} (w)}

It follows analogously to (lex<^{Tm}) using (lex≤). ⊓ ⊔

5 Soundness of Structural Recursion

We transfer the syntactic property of being structurally recursive to our semantics. Then we show that every structurally recursive term is good.

Definition 10 (Semantically structurally recursive). We say a function value f ∈ Val^{σ→τ} is semantically structurally recursive f ∈ SR^{σ→τ} if it terminates on all inputs v under the condition that it terminates on all lexicographically smaller inputs w ≺ v:

f ∈ SR^{σ→τ} :⟺ ∃π∀v ∈ VAL^{σ}. (∀w ∈ VAL^{σ}. w ≺_{π} v → f@w ⇓) → f@v ⇓

Proposition 1. SR^{σ→τ} = VAL^{σ→τ}

Proof. The domain VAL^{σ} of all function values of type σ → τ is wellfounded w.r.t. the lexicographic ordering, what we have shown in detail in [Abe99] and [AA02]. Thus the wellfounded induction principle establishes the equality between semantically structurally recursive and good functions. ⊓ ⊔

Theorem 2. Every recursive term of type σ → τ and context Γ is good in a good initial environment e_{0} ∈ VAL(Γ).

⟨fun g(x)=t_{0}; e_{0}⟩ ∈ VAL^{σ→τ}

Proof. By definition there exists a permutation π s.th. ⊢ g(x) sr_{π} t_{0}. Using the abbreviation

f_{0} ≡ ⟨fun g(x)=t_{0}; e_{0}⟩

and proposition 1 our goal becomes (∀w ∈ VAL^{σ}. w ≺ v_{0} → f_{0}@w ⇓) → f_{0}@v_{0} ⇓. If we can prove the following lemma under the global assumption

∀w ≺ v_{0}. f_{0}@w ⇓  (1)

we can finish using this lemma with empty Δ, t ≡ t_{0} and e ≡ (e_{0}, g =f_{0}, x=v_{0}).

Lemma 2. {Δ ⊢ g(x) sr_{π} t  e ⊨ Δ  ⟨g; e⟩ ↓ f_{0}  ⟨x; e⟩ ⇓ v_{0} \atop ⟨t; e⟩ ⇓}

Proof. By induction on Δ ⊢ g(x) sr_{π} t.

(srvar) ⟨y; e⟩ ⇓ since e is good except for g, but y ≠ g by assumption. (srcase) We have to show

Δ ⊢ g(x) sr_{π} s ∀i. Δ, x_{i} ≤^{Tm} s ⊢ g(x) sr_{π} t_{i} e ⊨ Δ ⟨g; e⟩ ↓ f_{0} ⟨x; e⟩ ⇓ v_{0}

⟨case(s, x.t); e⟩ ⇓

The first ind.hyp. entails ⟨s; e⟩ ⇓ in_{j}(v′). By (opcase) our goal follows from the second ind.hyp. using environment e′ ≡ e, x_{j} =v′, if we show the three premises of the ind.hyp.:

1. e′ ⊨ Δ, x_{j} ≤^{Tm} s: This follows from weakening and the three facts ⟨x_{j}; e′⟩ ⇓ v′, ⟨s; e′⟩ ⇓ in_{j}(v′) and v′ ≤ in_{j}(v′).

2. ⟨g; e′⟩ ↓ f_{0}: by (opweak)

3. ⟨x; e′⟩ ⇓ v_{0}: by (opweak)

(srlam) We have to show

{Δ ⊢ g(x) sr_{π} t  e ⊨ Δ  ⟨g; e⟩ ↓ f_{0}  ⟨x; e⟩ ⇓ v_{0} \atop ⟨λy.t; e⟩ ⇓}

Immediately by (oplam) we get ⟨λy.t; e⟩ ↓, thus it remains to show ⟨λy. t; e⟩ ∈ VAL. For this we assume u ∈ VAL and show ⟨λy.t; e⟩@u ⇓. The latter follows from (opappvl) and the ind.hyp. ⟨t; e′⟩ ⇓ for e′ ≡ (e, y =u), since e′ ⊨ Δ by weakening and ⟨g; e′⟩ ↓ f_{0} and ⟨x; e′⟩ ⇓ v_{0} by (opweak).

(srapprec) Using the ind.hyp. our goal becomes

{⟨(a); e⟩ ⇓ w  Δ ⊢ (a) ≺_{π}^{Tm} x  e ⊨ Δ ⟨g; e⟩ ↓ f_{0} ⟨x; e⟩ ⇓ v_{0} w ≺_{π} v_{0} \atop ⟨g(a); e⟩ ⇓}

By (opapp) and (opappvr) this is true, if f_{0}@w ⇓. That, however, was our global assumption (1) for w ≺_{π} v_{0}, which we obtain if we apply theorem 1 on the premise Δ ⊢ (a) ≺_{π}^{Tm} x.

All other cases follow directly by ind.hyp. using the operational semantics. ⊓ ⊔

Corollary 1. All terms t terminate in a good environment e.

∀t^{σ}[Γ], e ∈ ENV[Γ]. ∃v ∈ VAL^{σ}. ⟨t; e⟩ ⇓ v

Proof. By straightforward induction on t, using the operational semantics. For the critical case t ≡ fun g(x) = s use theorem 2. The proof has been carried out in [Abe99] and [AA02].

Corollary 2. All closed terms terminate.

From this corollary we can extract an interpreter for the foetus language that always terminates. This is no surprise since the interpreter just applies the operational semantics on the input term. Additionally, it computes a witness for the goodness of the result value (v ∈ VAL), which could be eliminated, using a refined program extraction (cf. [BS93]).

6 Conclusions and Further Work

We have formally defined a syntactical check “sr” for structurally recursive functions that serves as a frame for the derivation system for size relations between terms given in [AA02]. We have shown that these two parts of the termination checker are sound w.r.t. our operational semantics.

I expect that my approach can be extended to mutual recursion (see below) and dependent types, since they only put more restrictions on the acceptable terms. By this I mean that every term typable in a lambda calculus with inductive and dependent types (λΠ) should be typable in foetus. Hence we could just strip the dependency and run the foetus termination checker. My standpoint is confirmed by the fact that implementations of a termination checker for λΠ do not make use of the typing information (cf. [PP00]).

So far the termination checking of foetus is very limited, e.g., “quicksort” cannot be proven total with our method. To capture the Walther recursive functions [MA96] like quicksort one has to define two more judgements stating that a function is reducing resp. preserving. E.g., for quicksort the filtering step has to be preserving. Implementation of this so-called reduction checking should be straightforward for the simple structural ordering on terms. However, lexicographic orderings will require a number of modifications since they are not “first class citizens” in my system so far. They may appear only on right hand sides, not within the dependencies.

In [Abe98] and [AA02] Altenkirch and myself have informally described a termination checker also for mutual recursive functions. The main extension is the construction of a call graph for the mutual recursive functions, which has to satisfy a “goodness” condition. This enables the construction of a wellfounded ordering on the function symbols which, in addition to the lexicographic ordering on the arguments, serves as a component of the termination ordering required to run through the soundness proof. Work on the details is in progress.

In contrast to the full approach with call graphs a light weight version of mutual recursion with descent in every call would be a straightforward extension of the proof in the present article.

6.1 Acknowledgements

A number of colleagues deserve my thanks for their contribution to this work: Thorsten Altenkirch, for laying the foundations and for discussions on the definitions of the judgements and their semantics; Brigitte Pientka, for discussions on the commonesses and differences of our formal systems; and Ralph Matthes, Aaron Stump and the two anonymous referees for helpful comments on the draft.

References

[AA02] Andreas Abel and Thorsten Altenkirch. A predicative analysis of structural recursion. Journal of Functional Programming, 12(1):1–41, January 2002.

[Abe98] Andreas Abel. foetus – termination checker for simple functional programs. Programming Lab Report, 1998.

[Abe99] Andreas Abel. A semantic analysis of structural recursion. Master’s thesis, Ludwig-Maximilians-University Munich, 1999.

[BJO01] Frédéric Blanqui, Jean-Pierre Jouannaud, and Mitsuhiro Okada. Inductive data type systems. Theoretical Computer Science, 277, 2001.

[BS93] Ulrich Berger and Helmut Schwichtenberg. Program Development by Proof Transformation. Talk at Marktoberdorf, draft available under http://www.mathematik.uni-muenchen.de/˜ schwicht/, 1993.

[Coq92] Thierry Coquand. Pattern matching with dependent types. WWW, 1992.

[Coq00] Catarina Coquand. Agda. WWW page, 2000. http://www.cs.chalmers.se/˜ catarina/agda/.

[Gim95] Eduardo Giménez. Codifying guarded definitions with recursive schemes. In Peter Dybjer, Bengt Nordström, and Jan Smith, editors, Types for Proofs and Programs, International Workshop TYPES´ 94, Båstad, Sweden, June 6-10, 1994, Selected Papers, volume 996 of LNCS, pages 39–59. Springer, 1995.

[HHP93] Robert Harper, Furio Honsell, and Gordon Plotkin. A Framework for Defining Logics. Journal of the Association of Computing Machinery, 40(1):143–184, January 1993.

[JO97] J. P. Jouannaud and M. Okada. Abstract data type systems. Theoretical Computer Science, 173, 1997.

[MA96] David McAllester and Kostas Arkoudas. Walther Recursion. In M. A. McRobbie and J. K. Slaney, editors, 13th International Conference on Automated Deduction, New Brunswick, NJ, USA, July 30 – August 3, 1996, Proceedings, volume 1104 of Lecture Notes in Computer Science. Springer-Verlag, 1996.

[Mar84] Per Martin-Löf. Intuitionistic Type Theory. Bibliopolis, 1984.

[PP00] Brigitte Pientka and Frank Pfenning. Termination and Reduction Checking in the Logical Framework. Workshop on Automation of Proofs by Mathematical Induction, CADE-17, Pittsburgh, PA, USA, June 2000.

[PS98] Frank Pfenning and Carsten Schürmann. Twelf user’s guide. Technical report, Carnegie Mellon University, 1998.

[TT99] Alastair J. Telford and David A. Turner. Ensuring Termination in ESFP. Journal of Universal Computer Science, 6(4):474–, 1999. Proceedings of BCTCS