A Predicative Analysis of Structural Recursion

ANDREAS ABEL∗

Department of Computer Science, University of Munich, 80538 Munich, Germany

                     (e-mail: abel@tcs.informatik.uni-muenchen.de)

THORSTEN ALTENKIRCH

School of Computer Science & Information Technology, University of Nottingham, Nottingham, NG8 1BB, UK

                              (e-mail: txa@cs.nott.ac.uk)

Abstract

We introduce a language based upon lambda calculus with products, coproducts and strictly positive inductive types that allows the definition of recursive terms. We present the implementation (foetus) of a syntactical check that ensures that all such terms are structurally recursive, i.e., recursive calls appear only with arguments structurally smaller than the input parameters of terms considered. To ensure the correctness of the termination checker, we show that all structurally recursive terms are normalizing with respect to a given operational semantics. To this end, we define a semantics on all types and a structural ordering on the values in this semantics and prove that all values are accessible with regard to this ordering. Finally, we point out how to do this proof predicatively using set based operators.

1 Introduction

In lambda calculi with inductive types the standard means to construct a function over an inductive type is the recursor, which corresponds to induction. This method, however, has several drawbacks, as discussed in (Coquand, 1992). One of them is that programs are hard to understand intuitively. E.g., the “division by 2”-function may be coded with recursors over natural numbers R^{N} and booleans R^{B} as follows:

R^{N} : σ → (N → σ → σ) → N → σ
R^{B} : σ → σ → B → σ
half = λn^{N}. R^{N} (λx^{B}. 0) (λx^{N}λf^{B→N}. R^{B} (f true) (1 + (f false))) n false

Alternatively, in the presence of products, it can be implemented involving an auxiliary function returning a pair. But in both cases additional constructs are unavoidable. Therefore, a concept parallel to complete resp. wellfounded induction has been investigated: recursive definitions with pattern matching, as they are common in most functional programming languages. In SML our example could be written down straightforward as follows:

∗ This work was supported by the Graduiertenkolleg Logik in der Informatik (DFG) and the Office of Technology in Education, Carnegie Mellon University.

    datatype Nat = O | S of Nat
    fun half O         = O
     |  half (S O)     = O
     |  half (S (S n)) = S (half n)

These recursive definitions with pattern matching have to satisfy two conditions to define total functions:

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 totality of the pattern is always given. For a discussion see (Coquand, 1992).

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 the arguments are smaller than the input parameters in each recursive call of that function.

How to find such termination orderings has been dealt with comprehensively in the area of termination of rewriting (Dershowitz, 1987) and functional programs (Giesl, 1995). We restrict to structural orderings and their lexicographic extensions since they are sufficient in many cases and our focus is on a theoretical foundation rather than on completeness.

1.1 Structural Ordering

Usually a value v′ is considered structurally smaller than another value v if v < v′ w.r.t. to the component resp. subterm ordering. It can be defined as the transitive closure of

w < C(…, w, …)  (1)

where C is a constructor of an inductive datatype. On this basis a structural ordering t < t′ on terms t, t′ can be defined to hold iff v < v′ where t evaluates to v and t′ to v′. An alternative, which we pursue in this paper, is to define a structural ordering on terms independently and show that evaluation maps it into the ordering on values.

The axiom (1) is motivated by term structure. We will consider another axiom, motivated by the type structure:

(f a)^{τ} ≤ f^{σ→τ}  (2)

An informal justification for this axiom can be drawn from set theory where a function is defined as the set of all argument-result-pairs. Thus one result f a can be seen as a component of f which contains all possible results.

To verify in detail that the order induced by (1) and (2) is wellfounded is a major contribution of this article. It relies crucially on the predicativity of the type system. In our case this means that all inductive types are strictly positive. Furthermore we exclude impredicative polymorphism which destroys the wellfoundedness of the structural ordering as exemplified by Coquand (1992).

Consider the following program written in Haskell with 2nd order polymorphism^{1}:

    data V = C (forall a.a -> a)
    f :: V -> V
    f (C x) = f (x (C x))

The argument of the constructor C is a polymorphic function of type ∀a. a → a, like id. Since

                      Cid > id ≥ id (Cid) = Cid

the structural ordering is no longer wellfounded, and the function f, applied to Cid, loops infinitely.

1.2 Structural Recursion

We define a structurally recursive function as

a recursively defined function which calls itself (directly or indirectly) only for structurally smaller arguments.

Consider the addition of ordinal numbers implemented in SML as follows:

    datatype Ord = O'
                 | S'  of Ord
                 | Lim of Nat -> Ord
    fun addord x O'      = x
      | addord x (S' y') = S' (addord x y')
      | addord x (Lim f) = Lim (fn z:Nat => addord x (f z))

addord is structurally recursive, since in each recursive call the second argument y is decreasing. In the first call y' < S' y' =: y following axiom (1), and in the second call f z ≤ f < Lim f =: y using both axioms.

We shall present syntactic conditions which are sufficient to ensure that a function is structurally recursive and which can be checked mechanically. We have implemented a termination checker for our language foetus that accepts structural recursive definitions. Recently this termination checker has been reimplemented by C. Coquand (1999) as part of Adga.

1.3 Lexicographic Termination Orderings

The foetus termination checker accepts also functions that are structural recursive w.r.t. a lexicographic extension of the structural ordering, e.g., the Ackermann function:

1 E.g. this is implemented in Hugs, see (Jones & Reid, 1999), section 7.2.

    fun ack O      y      = S y
      | ack (S x') O      = ack x' (S O)
      | ack (S x') (S y') = ack x' (ack (S x') y')

Here we have to check three recursive calls: In ack x' (S O) and ack x' … the first argument is decreasing and in the third (nested) call ack (S x') y' the first argument stays the same and the second is decreased w.r.t. the lexicographic ordering on ℕ × ℕ.

1.4 Mutual Recursion and Call Graphs

To handle mutual recursion as well requires some additional considerations. We shall sketch our method by the means of the following example:

    fun flat []         = []
      | flat (l::ls)    = aux l ls
    and aux  []      ls = flat ls
      | aux  (x::xs) ls = x :: aux xs ls

The function flat takes a list of lists and returns a list making use of the auxiliary function aux which processes one list. We can extract three calls and the respective behavior of the arguments and organize them in the following call graph (solid arrows):

[figure: flat; (^{<}); ^{(\begin{matrix}< \\ < \end{matrix})}; aux; (\begin{matrix}< & ? \\ ? & ≤ \end{matrix}); _{(_{? ≤})}]

Each arrow is labeled with the call matrix of the respective call where the rows represent the input parameters of the calling function and the columns the arguments of the called function. A “<” in cell (i, j) of a call matrix expresses that the j argument of the call is strictly smaller than the ith parameter of the calling function, a “≤” denotes weak decrease and a “?” stands for increase or absence of information. For example, in the call flat→aux both arguments l and ls are structurally smaller than the input parameter (l::ls) of flat. By continued combination of adjacent calls we obtain the completion of that graph which contains the direct of indirect calls of a function to itself. In our case this yields for flat (dotted arrow):

                           flat → flat : (<)

For a given function to be structural recursive, we now can apply the default demand: Each recursive call must decrease the argument structurally (which is given in the case of flat). We will treat call graphs formally in Sect. 3.

1.5 Semantic Analysis

The termination checker recognizes^{2} structurally recursive functions. We want to know whether we can rely on the checker output, i.e., we want to know whether all structurally recursive functions terminate on all inputs. This is the case if the structural ordering is well-founded, which is a fundamental assumption in (Coquand, 1992). In Sect. 4 we give an interpretation of the types of our systems as monotone operators on value sets. We further introduce a structural ordering on all values in the interpretation of closed types and prove that this ordering is wellfounded. Then we can show that all accepted terms normalize w.r.t. our operational semantics.

1.6 A Predicative Meta-Theory

In Sect. 4 we give a semantic interpretation of all types using an impredicative metatheory: We show that types which depend only strictly positively on type variables give rise to monotone operators on values. To define the interpretation of recursively defined types μX.σ(X) we use the theorem by Knaster and Tarski (1955) that every monotone operator on a complete lattice has a least fixpoint. This construction can be extended to types which depend only positively on type variables (i.e., occurring in the left hand side of the scope of an even number of arrow types) because they give rise to monotone operators semantically (Abel, 1999).

To construct the least fixpoint of a monotone operator we use the completeness of the subset lattice, i.e., we construct the fixpoint as the intersection of all prefixpoints. This construction is impredicative—we define a new subset by quantifying over all subsets of an infinite set. In contrast, in a predicative^{3} construction we only refer to concepts which have been defined previously. Thus we can construct fixpoints of strictly positive operators because they correspond to well-founded (but possibly infinitely branching) derivation trees. The induction principle can be justified because we refer to smaller (i.e., previously constructed trees) when constructing new trees. Examples of predicative theories are Martin-Löf’s Type Theory (Martin-Löf, 1984; Nordström et al., 1990) or Aczel’s Constructive Set Theory (Aczel, 1997).

In Sect. 5 we show that it is possible to interpret our predicative type system in a predicative meta-theory. We use the concept of set based operators introduced by Peter Aczel (1997) in the context of intuitionistic set theory. Here we need only the special case of deterministically set based operators. Intuitively, a set based operator can be understood as a monotone operator Φ which comes with a binary urelement relation U. In the case of simple data structures like lists and trees over

2 Note that the property structurally recursive is actually undecidable, hence we cannot hope for

a complete decision procedure. 3 Predicativity is not used in the sense of proof theory which calls theories which are stronger

than Γ_{0} impredicative. We consider all “bottom-up” theories as predicative, thus for instance also ID_{<ω}^{i}.

a type τ this relation coincides with the “element”-relation. The urelement relation U enjoys the following properties:

1. If starting from a value set V we construct a value set Φ(V) with an element w ∈ Φ(V), then all urelements v U w of w are elements of the base set V.

2. An element w ∈ Φ(True) (where True is the universal value set) can be reconstructed from its urelements, i.e., w ∈ Φ({v : v U w}).

We show that every strictly positive type can be interpreted by a set based operator and that fixpoints of set based operators can be constructed by strictly positive inductive definitions on the meta level. This idea has already been used in a predicative strong normalisation proof (Abel & Altenkirch, 2000).

1.7 Notational conventions

We are using vectors to simplify our notation. If we have a family of expressions E_{1}, E_{2}, …, E_{n} we write E⃗ for the whole sequence. We denote the length n of the sequence by |E⃗|. Given a fixed E′ we write E⃗E′ for E_{1}E′, E_{2}E′, …, E_{n}E′ and E′E⃗ for E′E_{1}, E′E_{2}, … E′E_{n}. Furthermore we use the notations

X, Y, Z for type variables
ρ, σ, τ for types
x, y, z, l for term variables
r, s, t, a for terms
u, v, w for values
f, g  for function identifiers or values
c  for closures
e  for environments

We use set notation to define predicates, i.e., we write x ∈ P for P (x) and we define new predicates by the notation for set comprehension. However, sets are not first order citizens in our meta theory, i.e., we do not quantify over sets and we do not use power sets. We write relations in infix notation, i.e., we write x R y for (x, y) ∈ R. We write projections as partial applications, i.e., R(y) = {x : x R y}.

2 The foetus Language

We introduce a term language based on the simply typed lambda calculus enriched with finite sum and products and inductive types, in the style of a functional programming language. Thus we allow the definition of recursive terms. We define normal forms explicitly as values and introduce environments avoiding to have to define substitution. The meaning of terms is defined by a big step operational semantics.

2.1 Types

The foetus type system is constructed from the base type variables X, Y, Z, … and the type constructors Σ (finite sum), Π (finite product), → (function space) and μ (inductive type). We restrict ourselves to strictly positive recursive types for two reasons: Firstly, it is not clear how to formalize structural recursion for non-strictly positive types. And secondly, it is not clear whether non-strictly positive types can be understood predicatively. Within our system the set of natural numbers may be expressed as N ≡ μX.1 + X and the set of lists over natural numbers as L^{N} ≡ μX.1 + N × X.

Type Variables. Assume a countably infinite set of type variables TyVar whose elements we denote by X, Y, Z, … A type variable X appears strictly positive within a type τ iff it appears never on the left side of some →. We enforce that all variables in a type satisfy this condition by restricting the domains of function types to closed types (see rule (Arr) below).

Definition 2.1 (Types) We inductively define the family of types Ty(X⃗) indexed over a finite list of distinct type variables X⃗ ∈ TyVar appearing only strictly positive as follows:

(Var) {X_{1}, …, X_{n} ∈ TyVar 1 ≤ i ≤ n \atop X_{i} ∈ Ty(X⃗)}

(Sum) {σ_{1}, …, σ_{n} ∈ Ty(X⃗) \atop Σσ⃗ ∈ Ty(X⃗)} (Prod) {σ_{1}, …, σ_{n} ∈ Ty(X⃗) \atop Πσ⃗ ∈ Ty(X⃗)}

(Arr) {σ ∈ Ty() τ ∈ Ty(X⃗) \atop σ → τ ∈ Ty(X⃗)} (Mu) {σ ∈ Ty(X⃗, X) \atop μX.σ ∈ Ty(X⃗)}

We can restrict the free type variables to strictly positive ones because unlike Girard’s System F (Girard, 1972), we have no polymorphic types and therefore need type variables only to construct inductive types.

Notation. In the following we write σ(X⃗) to express σ ∈ Ty(X⃗). Then σ and σ(X⃗) are synonyms. We also abbreviate the set of closed types Ty() by Ty. For binary sums Σ(σ, τ) we write σ + τ, for ternary ρ + σ + τ, etc. (same for products). The empty sum Σ() is denoted by 0 and the empty product Π() by 1.

Renaming Convention for Types. μ binds a type variable X in a type σ(X⃗, X), and we may replace all appearances of X in μX.σ(X⃗, X) by any new variable Y ∉ X⃗ without altering the actually denoted type. Thus we do not distinguish between μX.σ(X⃗, X) and μY.σ(X⃗, Y).

Our style of variable introduction and binding (see rules (Var) and (Mu) below) is very close to an implementation of variables by deBruijn-indices (see (de Bruijn, 1972)), but we have kept variable names for better readability.

Substitution. Provided a type σ(X⃗) with a list of free variables X⃗ and an equally long list of types ρ⃗ ∈ Ty(Y⃗) we define the capture avoiding substitution σ[X⃗ := ρ⃗] ∈ Ty(Y⃗) in the usual way. We write σ(ρ⃗) for σ(X⃗)[X⃗ := ρ⃗] and define substitution of a single variable Y as σ(X⃗, Y, Z⃗)[Y := ρ] = σ[X⃗ := X⃗, Y := ρ, Z⃗ := Z⃗], which we further abbreviate to σ(X⃗, ρ, Z⃗).

2.2 Terms

Now, we define the terms inhabiting the types defined above. The definitions are very similar to a typed lambda calculus enriched by sums and products, except for the recursive terms we allow. We have decided to type terms using contexts to simplify the definition of closures afterwards.

Term Variables and Contexts. Assume a countably infinite set of term variables TmVar using g, x, y, z to denote elements of this set. Given the closed types σ_{1}, … σ_{n} we can form a context Γ = x_{1}^{σ_{1}}, …, x_{n}^{σ_{n}} ∈ Cxt as a list of pairwise distinct term variables together with their types. We write x^{σ} to express the assumption that the variable is of type σ.

Definition 2.2 (Terms) We define the set of (well-typed) terms Tm^{σ}[Γ] of a closed type σ in context Γ inductively as follows:

(var)

Γ, x^{σ}, Γ′ ∈ Cxt

x ∈ Tm^{σ}[Γ, x^{σ}, Γ′]

(in)

t ∈ Tm^{σ_{j}}[Γ]

inσ⃗ ; j(t) ∈ Tm^{Σσ⃗}[Γ]

(case) t ∈ Tm^{Σσ⃗}[Γ] t_{i} ∈ Tm^{ρ}[Γ, x_{i}^{σ_{i}}] for 1 ≤ i ≤ n

case(t, x_{1}^{σ_{1}}.t_{1}, …, x_{n}^{σ_{n}}.t_{n}) ∈ Tm^{ρ}[Γ]

(tup)

t_{i} ∈ Tm^{σ_{i}}[Γ] for 1 ≤ i ≤ n
(t_{1}, …, t_{n}) ∈ Tm^{Πσ⃗}[Γ]

(pi) {t ∈ Tm^{Πσ⃗}[Γ] \atop π_{j}(t) ∈ Tm^{σ_{j}}[Γ]}

(lam)

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

(rec)

t ∈ Tm^{σ→τ} [Γ, g^{σ→τ}]
rec g^{σ→τ} . t ∈ Tm^{σ→τ} [Γ]

(app) t ∈ Tm^{σ→τ} [Γ] s ∈ Tm^{σ}[Γ]

t s ∈ Tm^{τ} [Γ]

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

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

(unfold)

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

There are two main kinds of term forming rules: Rules for introducing types (the constructors (in), (tup), (lam) and (fold)) and rules for eliminating types (the destructors (case), (pi), (app) and (unfold)). The remaining rules (var) and (rec) are structural.

Renaming Convention for Terms. In these rules case binds the variables x_{i} in the terms t_{i}, λ binds x in t and rec binds g in t. As for types we do not distinguish between terms that are equal except that the names of their bound variables differ.

Notation. Similar to the type notation σ(X⃗) we write t^{σ} to express that t is of type σ, t[Γ] that t is a term over context Γ and t^{σ}[Γ] to express both, i.e., t ∈ Tm^{σ}[Γ]. We define the set of closed terms Tm^{σ} of type σ as the set of terms over an empty context Tm^{σ}[]. We omit type annotation on in_{j}, fold, unfold and abstractions wherever we do not introduce ambiguity.

Currying. For our termination analysis it is convenient to view a function with several arguments in its uncurried form as a function with one argument of product type. To support the formulation of functions of arity ≥ 2, we introduce the construct

{t ∈ Tm^{τ} [Γ, x_{1}^{σ_{1}}, …, x_{n}^{σ_{n}}] \atop λ(x_{1}^{σ_{1}}, …, x_{n}^{σ_{n}}). t ∈ Tm^{Πσ⃗→τ} [Γ]}

From the semantic point of view it is just syntactic sugar for λy^{Πσ⃗}. t′ where t′ is the result of replacing x_{i} with π_{i}(y) for 1 ≤ i ≤ n. For instance,

λ(x^{σ}, y^{τ}). (y, x)  is interpreted as  λp^{σ×τ} . (π_{2}(p), π_{1}(p)).

2.2.1 Example: The flat Function

To clarify the different constructs of our language we give an encoding of the list flattening function in foetus. This function takes a list of lists of natural numbers and transforms it into a list of natural numbers. All required datatypes can be defined in foetus using fixpoint types:

Nat ≡ μX. 1 + X
ListN ≡ μX. 1 + Nat × X
ListL ≡ μX. 1 + ListN × X

Identifiers in bold font denote defined types or terms which are not part of the language but mere abbreviations. For convenience, we define abbreviations for the two constructors of lists:

nil ≡ fold(in_{1}())
cons(−) ≡ fold(in_{2}(−))

For a natural number x ∈ Tm^{Nat} and a list y ∈ Tm^{ListN} we can construct the extension cons(x, y) of list y by element x as follows:

x ∈ Tm^{Nat} y ∈ Tm^{ListN}

\overline{tup}

(x, y) ∈ Tm^{Nat×ListN}

\overline{in}

in_{2}(x, y) ∈ Tm^{1+Nat×ListN}

\overline{fold}

fold^{X. 1+Nat×X}(in_{2}(x, y)) ∈ Tm^{μX. 1+Nat×X}

Using the defined abbreviations the final line states cons(x, y) ∈ Tm^{ListN}. We recall the definition of the flattening function:

    fun flat []         = []
      | flat (l::ls)    = aux l ls
    and aux  []      ls = flat ls
      | aux  (x::xs) ls = x :: aux xs ls

The main function flat is recursive, taking a list of lists and returning a list of natural numbers. We will denote it with the identifier f of type ListL → ListN. The pattern matching over its one argument, which we will refer to as ll, translates into a case construct:

flat ≡ rec f^{ListL→ListN}. λll^{ListL}.

case(unfold(ll), 1. nil,

p^{ListN×ListL}. aux (π_{1}(p), π_{2}(p)))

Since ll is of fixpoint type we first have to unfold it to obtain something of sum type before we can distinguish cases. The first alternative is that unfold(ll) = in_{1}( ^{1}), which means that it is an injection of something of unit type 1. Since we are not interested in the specific inhabitant of the unit type involved here, we use the anonymous variable “ ”. In this case ll encodes the empty list, and we return the empty list nil. In the second case unfold(ll) = in_{2}(p^{ListN×ListL}) we have to deal with the injection of a pair p consisting of a list of natural numbers and a list of lists. This case is handled by the auxiliary function, denoted by the placeholder aux.

The simultaneous recursion of SML can be translated into a nested or interleaving recursion in foetus. We simply define aux via the recursion operator rec and substitute it for every occurrence of the placeholder aux in flat. In this way we realize calls from flat to aux. All calls from aux to flat can simply refer to the identifier f, since aux is within the scope of f. Omitting some type annotations the full program reads as follows:

flat ≡ rec f. λll. case(unfold(ll),
. nil,
p. (rec g. λ(l^{ListN}, ls^{ListL}). case(unfold(l),
. f ls,
q^{Nat×ListN}. cons(π_{1}(q), g(π_{2}(q), ls))))
(π_{1}(p), π_{2}(p)))

For the definition of aux—which we assigned function identifier g—we used the syntactic sugar. To obtain the unsugared version we replace

(l^{ListN}, ls^{ListL})  with  y^{ListN×ListL},
l  with  π_{1}(y)  and
ls  with  π_{2}(y).

Readers familiar with SML will know that fun is not a core construct of the programming language and can be replaced by the more primitive val rec (Harper, 2000). Replacing simultaneous recursion with interleaving recursion, we obtain a version of the original program which is very similar to its foetus encoding:

    val rec flat = fn ll =>
        let val rec aux = fn (l, ls) =>
            case l of
                [] => flat ls
              | (x::xs) => x :: aux (xs, ls)
        in
            case ll of
                [] => []
              | (l::ls) => aux (l, ls)
        end

Note that rec has to be used in conjunction with a let in SML, whereas it can appear in any position in foetus programs.

2.3 Values and Closures

We only assign a meaning to closed terms t ∈ Tm^{σ}: they evaluate to (syntactic) values of type σ. (We are going to define semantic values as well, see Sect. 4.) During the process of evaluation defined by our operational semantics we will have to handle open terms, together with environments which assign values to the free variables. This entails that we do not have to define substitution on terms. A Term and its corresponding environment form a closure which can be seen as completion of an open term.

Values. We define Val^{σ} inductively as follows. Again we write v^{σ} to express v ∈ Val^{σ}. The set of environments Val(Γ) is defined simultaneously (see the definition below).

(vlam) t ∈ Tm^{τ} [Γ, x^{σ}] e ∈ Val(Γ)

⟨λx^{σ}.t; e⟩ ∈ Val^{σ→τ}

(vrec) t ∈ Tm^{σ→τ} [Γ, g^{σ→τ}] e ∈ Val(Γ)

⟨rec g^{σ→τ} . t; e⟩ ∈ Val^{σ→τ}

(vin)

v ∈ Val^{σ_{j}}
inσ⃗ ; j(v) ∈ Val^{Σσ⃗}

(vtup) v_{i} ∈ Val^{σ_{i}} for 1 ≤ i ≤ n

(v_{1}, …, v_{n}) ∈ Val^{Πσ⃗} (vfold)

v ∈ Val^{σ(μX.σ)}
fold^{X.σ}(v) ∈ Val^{μX.σ}

These rules correspond to the introduction rules for terms. Since values represent evaluated terms, we need only constructors, no destructors.

Environments and Closures. We define the set of environments of the context Γ = x_{1}^{σ_{1}}, …, x_{n}^{σ_{n}} as

Val(Γ) := {x_{1} =v_{1}, …, x_{n} =v_{n} : v_{i} ∈ Val^{σ_{i}}}

We write e^{Γ} for an environment e ∈ Val(Γ) and “·” for the empty environment. The set of closures of type τ we define as

Cl^{τ} := {⟨t; e⟩ : Γ ∈ Cxt, t ∈ Tm^{τ} [Γ], e ∈ Val(Γ)}
∪ {f@u : f ∈ Val^{σ→τ} , u ∈ Val^{σ}}

Here @ is a syntactic function symbol Val^{σ→τ} × Val^{σ} → Cl^{τ}. Closures of the form f@u (value applied to value) are convenient to define the operational semantics without casting values back to terms, which in an implementation would be inefficient as well.

Renaming Convention for Closures. Since in a closure all variables of a term are bound, we consider two closures that differ only in variable names as equal.

2.4 Operational Semantics

In the following we present a big step operational semantics “⇓” that defines how closures are evaluated to values. Our strategy is call-by-value (see rule (opapp)) and we do not evaluate under λ and rec (see rules (oplam) and (oprec)). Furthermore it is deterministic, i.e., for every closure there is at most one computation tree.

Definition 2.3 (Operational Semantics) We inductively define a family of relations

⇓^{σ}⊆ Cl^{σ} × Val^{σ}

indexed over Ty. As the type σ can be inferred from the type of the closure or the value, we generally leave it out. For reasons of readability we leave out type and context annotations wherever possible.

(opvar) ⟨x; e, x = v, e′⟩ ⇓ 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^{τ}

⟨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 ⟨π_{j}(t); e⟩ ⇓ v_{j}}

(oplam) ⟨λx.t; e⟩ ⇓ ⟨λx.t; e⟩  (oprec) ⟨rec g. t; e⟩ ⇓ ⟨rec g. 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 = ⟨rec g. t; e⟩⟩ ⇓ f f@u ⇓ v \atop ⟨rec g. t; e⟩@u ⇓ v}

(opfold)

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

(opunfold)

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

Proposition 2.4 ⇓ is deterministic, i.e., c ⇓ v and c ⇓ v′ implies v = v′.

Proof For all closures except ⟨case(t, x⃗.t); …⟩ there is only one computation rule. But also for closures with case analysis there will be only one computation tree, since ⟨t; …⟩ may only evaluate to in_{j}(w) for a fixed j thus only one instance of (opcase) is applicable.

3 The foetus Termination Checker

The syntactic check, whether a recursive term is structurally recursive, consists of three phases:

1. Function call extraction.

The recursive term is analyzed and all recursive calls are gathered. During the analysis dependencies of new variables are gained, i.e., information whether a new variable is structurally smaller than an already known one.

2. Call graph generation and completion. All calls which have been gathered are organized in a call graph which is completed afterwards.

3. Search for a termination ordering. From the completed graph all recursive calls of the function in consideration are extracted. Then it is searched for a lexicographic ordering on the arguments that ensures termination.

The termination checker makes use of two major data structures, dependencies and calls, and a minor data structure, the function stack.

Dependencies Δ: A set of dependencies Δ is a collection of straitened variables x ≤ s. We use these dependencies to derive that arguments decrease structurally in a recursive call. They are generated whenever we learn information about terms when stepping over a case construct. The semantics of the term

case(s, x_{1}.t_{1}, …, x_{n}.t_{n})

yields the constraints in_{j}(x_{j}) = s for 1 ≤ j ≤ n. Thus within the scope of x_{j}, i.e, within t_{j}, we may safely assume that x_{j} ≤ s.

Calls C: A call g(t_{1}, …, t_{n}) of function g with arguments t⃗ within a function f with formal parameters (x_{1}, …, x_{m}) is denoted by

f → g : (a_{ij}) where a_{ij} ∈ {<, ≤,?} for 1 ≤ i ≤ n, 1 ≤ j ≤ m

We will refer to (a_{ij}) as call matrix, since its elements indicate how the arguments t⃗ behave in a function call: a_{ij} = < if t_{i} can be shown to always be strictly structurally smaller than x_{j}, a_{ij} = ≤ if t_{i} is ensure to be less or equal than x_{j}, and a_{ij} = ? if neither of the previous alternatives holds. We denote sets of calls by C.

Function stack Φ: As we traverse a term we build up a function stack Φ which contains the name of functions together with their formal arguments. When we analyze

rec f. λ(x_{1}, …, x_{n}). s

we will push f(x_{1}, …, x_{n}) onto the stack. The topmost element denotes the function whose body we are currently inspecting.

The procedure which analyzes a term, finds all function calls and computes the call matrices will be presented in form of two judgments:

Δ, Φ ⊢ t ⊐ C  function call extraction
Δ ⊢ t R x (R ∈ {<, ≤,?})  structural ordering on terms

In the remainder of this section we will define these two judgments (Sect. 3.1 and 3.2), state some properties about call matrices (Sect. 3.3), give an algorithm that finds indirect calls via graph completion (Sect. 3.4) and show how to find a lexicographic ordering that ensures termination (Sect. 3.5).

3.1 Function Call Extraction

Given a foetus program t the termination checker first extracts the set of function calls C within t. The extraction process can be formalized as follows:

Definition 3.1 (Function Call Extraction) Let Δ be a set of dependencies, Φ a function stack, t a term and C a set of calls. Then C is extracted from t iff

Δ; Φ ⊢ t ⊐ C

Read “under the dependencies Δ and within the functions Φ the term t contains the calls C”. The judgment is established by the following rules:

Recursive functions and calls:

(⊐rec) {Δ; Φ, g(x_{1}, …, x_{n}) ⊢ s ⊐ C \atop Δ; Φ ⊢ rec g. λ(x_{1}, … x_{n}). s ⊐ C}

(⊐appvar) Δ; Φ, f(x⃗) ⊢ (t⃗) ⊐ C Δ ⊢ t_{i} a_{ij} x_{j} for all 1 ≤ i ≤ n, 1 ≤ j ≤ m

Δ; Φ, f(x_{1}, …, x_{m}) ⊢ g (t_{1}, …, t_{n}) ⊐ C, f → g : (a_{ij})

(⊐apprec)

Δ; Φ ⊢ (t⃗) ⊐ C  Δ; Φ, g(y⃗) ⊢ s ⊐ C′  Δ ⊢ t_{i} a_{ij} x_{j} for all i, j
Δ; Φ ≡ (Φ′, f(x⃗)) ⊢ (rec g. λ(y⃗). s) (t⃗) ⊐ C, C′, f → g : (a_{ij})

Dependencies:

(⊐case)

Δ; Φ ⊢ s ⊐ C Δ, x_{i} ≤ s; Φ ⊢ t_{i} ⊐ C_{i} for all i
Δ; Φ ⊢ case(s, x⃗.t) ⊐ C, C⃗

Congruences:

(⊐var) Δ; Φ ⊢ x ⊐ ·  (⊐in) {Δ; Φ ⊢ t ⊐ C \atop Δ; Φ ⊢ in_{j}(t) ⊐ C}

(⊐tup)

Δ; Φ ⊢ t_{i} ⊐ C_{i} for all i

Δ; Φ ⊢ (t⃗) ⊐ C⃗ (⊐pi)

{Δ; Φ ⊢ t ⊐ C \atop Δ; Φ ⊢ π_{j}(t) ⊐ C}

(⊐lam) {Δ; Φ ⊢ t ⊐ C \atop Δ; Φ ⊢ λx. t ⊐ C}  (⊐app) {Δ; Φ ⊢ t ⊐ C  Δ; Φ ⊢ s ⊐ C′ \atop Δ; Φ ⊢ t s ⊐ C, C′}

(⊐fold)

Δ; Φ ⊢ t ⊐ C
Δ; Φ ⊢ fold(t) ⊐ C

(⊐unfold)

Δ; Φ ⊢ t ⊐ C

Δ; Φ ⊢ unfold(t) ⊐ C

Note that only the rules (⊐appvar) and (⊐apprec) add new calls to the set C. To calculate the call matrix (a_{ij}) they rely on the judgment inferring structural ordering on terms, which we will describe in the next section.

Read upwards the given rules provide an algorithm for extracting function calls out of a well-typed term t. As stated, it is non-deterministic since several rules for application exist. In the following we stipulate that (⊐appvar) and (⊐apprec) always override (⊐app). This makes the algorithm deterministic and complete, i.e., it will return all function calls to be found in t.

Let us clarify the algorithm by an example. Recall the flattening function and its implementation in foetus (now stripped of all type annotations):

flat ≡ rec f. λll. case(unfold(ll),
. nil,
p. (rec g. λ(l, ls). case(unfold(l),
. f ls,
q. cons(π_{1}(q), g (π_{2}(q), ls))))
(π_{1}(p), π_{2}(p)))

The following table gives snapshots of the extraction algorithm in action. We display the dependencies Δ and the function stack Φ at the points where calls are detected.

Δ  Φ  t  call
Δ_{0} ≡ p ≤ unfold(ll) f(ll)  (rec g. λ(l, ls) …) (π_{1}(p), (π_{2}(p)) f → g
Δ_{0}, q ≤ unfold(l)  f(ll), g(l, ls) f ls  g → f
Δ_{0}, q ≤ unfold(l)  f(ll), g(l, ls) g (π_{2}(q), ls)  g → g

In all three cases the call matrices can be computed from Δ, Φ and the arguments of the call. How, we will present in the next section.

3.2 Structural Ordering on Terms

The second integral part of the termination checker is a calculus that allows us to determine whether from a set of dependencies Δ we can derive a relation p of the form t < x or t ≤ x. Since its use is restricted to calculate whether a function argument t is structurally smaller than a function parameter x, the right hand side will always be a variable.

Definition 3.2 (Structural Ordering on Terms) Let Δ be a set of dependencies, t a term and x a variable. The judgment

Δ ⊢ t R x R ∈ {<, ≤}

states that “under the dependencies Δ the term s is (strictly) structurally smaller than the variable x”. It is defined by the rules given after the following motivation.

As stated in the introduction, we motivate structural ordering mainly by the fact that a constructor of an inductive datatype increases the order. For example,

l < cons(x, l) ≡ fold(in_{2}(x, l))  (3)

Since every constructor of an inductive datatype involves a fold in the outermost position, it is sufficient for the other term constructors like pairing and injection to increase the order weakly. Thus we can form the chain

l ≤ (x, l) ≤ in_{2}(x, l) < fold(in_{2}(x, l))

This term constructor oriented definition is motivated by the observable values of the programming language. We will come back to it in Sect. 4.2. However, for the program analysis we perform, we have to consider the term destructors. Consider the recursive function

rec f. λx … f t …

The argument t can be shown to be structurally smaller than the parameter x if it is derived from x involving only destructors.^{4} From the perspective of destructors the inequality (3) looks as follows (l ≠ nil):

tail(l) ≡ case(l, .nil, p.π_{2}(p)) < l  (4)

This motivates the following rules (R ∈ {<, ≤}):

(≤refl) Δ ⊢ x ≤ x

(Rcase)

Δ, y_{i} ≤ s ⊢ t_{i} R x for i=1, ..., n

Δ ⊢ case(s, y⃗.t) R x (Rpi)

{Δ ⊢ t R x \atop Δ ⊢ π_{j}(t) R x}

(Rapp)

{Δ ⊢ f R x \atop Δ ⊢ f a R x}

(Runf)

Δ ⊢ t ≤ x
Δ ⊢ unfold(t) R x

During the process of function call extraction, whenever we step into a branch t of a case construct case(s, …, y.t, …) we introduce a the new variable y which is constrained by the dependency y ≤ s. In checking Δ ⊢ t R x, whenever we have reduced t to a variable y by the destructor rules above, we can use the dependency of y by transitivity (R ∈ {<, ≤}).

(Rtrans) {Δ, y ≤ t, Δ′ ⊢ t R x \atop Δ, y ≤ t, Δ′ ⊢ y R x}

The arising calculus is deterministic. The number of rule applications necessary to decide Δ ⊢ t R x is limited by the size of Δ, i.e., the sum of the sizes of all terms in Δ.

Continuing our example from the last section we show that in the call f → g the second argument to g is smaller than the parameter of f, i.e., p ≤ unfold(ll) ⊢ π_{2}(p) < ll). Furthermore we show for the call g → g that q ≤ unfold(l) ⊢ π_{2}(q) < l which means that the first argument is decreased.

\overline{≤refl} ; … ⊢ ll ≤ ll

\overline{<unf}
… ⊢ unfold(ll) < ll
\overline{<trans}
p ≤ unfold(ll) ⊢ p < ll
\overline{<pi}
p ≤ unfold(ll) ⊢ π_{2}(p) < ll

\overline{≤refl} ; … ⊢ l ≤ l

\overline{<unf}
… ⊢ unfold(l) < l
\overline{<trans}
q ≤ unfold(l) ⊢ q < l
\overline{<pi}
q ≤ unfold(l) ⊢ π_{2}(q) < l

4 For the sake of simplicity we ignore the fact that constructors might be contained in t if they are eliminated by a larger number of destructors. See Remark 3.3.

Remark 3.3 (Limitations) Since we limit the rules to destructors, the termination checker does not accept recursive calls with constructors in the arguments. A consequence of that is that we do not recognize termination of functions like the following, which computes the sum of a list:

    fun sum []         = 0
      | sum (S n :: l) = S (sum (n :: l))
      | sum (0 :: l)   = sum l

However, this program can be mechanically transformed into one that terminates by a lexicographic ordering.

Remark 3.4 (Deciding R) Given Δ, t and x the calculus can also decide whether Δ ⊢ t < x or only Δ ⊢ t ≤ x. For that purpose we construct a derivation for Δ ⊢ t R x where R is undetermined. The first time we invoke the rule for unfold we fix R = <.

Definition 3.5 We write Δ ⊢ t ? x iff not Δ ⊢ t R x for R ∈ {<, ≤}.

3.3 Call Matrices

The behavior of the arguments in a call f(x_{1}, …, x_{m}) → g(t_{1}, …, t_{n}) with dependencies Δ can be expressed by a matrix A = (a_{ij}) ∈ R^{n×m}, where R = {<, ≤,?}. We define

a_{ij} = \{ \begin{matrix}< & if Δ ⊢ t_{i} < x_{j} \\ ≤ & if Δ ⊢ t_{i} ≤ x_{j}, but not Δ ⊢ t_{i} < x_{j} \\ ? & if not Δ ⊢ t_{i} ≤ x_{j} \end{matrix}

The columns of that matrix stand for the input variables of the calling function and the rows for the arguments of the call. Together with the two operations + and · defined as in the table below the set R forms a commutative semi-ring with zero ? and unit ≤.

\begin{aligned}+ & < & ≤ & ? \\ < & < & < & < \\ ≤ & < & ≤ & ≤ \\ ? & < & ≤ & ? \end{aligned}  \begin{aligned}· & < & ≤ & ? \\ < & < & < & ? \\ ≤ & < & ≤ & ? \\ ? & ? & ? & ? \end{aligned}

The operation + can be understood as “combining parallel information about a relation”. For instance, if we have a ? y and a < y we have a (? + <) y and that simplifies to a < y. The operation · however is “serial combination”, for example, a < y and y ≤ z can be combined into a (<·≤) z, simplified: a < z. The element ? is neutral regarding + because it provides no new information, whereas < is dominant because it is the strongest information. Regarding · the relation ≤ is neutral and ? is dominant because it “destroys” all information.

Since R is a semi-ring, we can define multiplication on matrices over R which allows us to compute the size change information of a combined call in the following sense: Given two calls

\begin{aligned}f(x_{1}, …, x_{l}) & → & g(y_{1}, …, y_{m}) & : & (a_{ij}) ∈ R^{m×l}, and \\ g(y_{1}, …, y_{m}) & → & h(z_{1}, …, z_{n}) & : & (b_{ij}) ∈ R^{n×m}, \end{aligned}

the argument behavior of the indirect call f → g → h is captured by the matrix product

(c_{ij}) = (b_{ij})(a_{ij}) = (∑_{k=1}^{m} b_{ik}a_{kj}) ∈ R^{n×l}.

Definition 3.6 (Call Matrix) A call matrix is a matrix over R with no more than one element different from “?” per row.

CM(n, m) := {(a_{ij}) ∈ R^{n×m} : ∀i∀j∀k ≠ j(a_{ij} = ? or a_{ik} = ?)}

Remark 3.7 The reason we define call matrices this way is these are the only ones foetus produces by function call extraction. By definition of the structural ordering on terms a call argument can only depend on one function parameter.

For the three calls in our example the call matrices are

f → g : ( \begin{matrix}< \\ < \end{matrix} )  g → g : ( \begin{matrix}< & ? \\ ? & ≤ \end{matrix} )  g → f : ( ? ≤ )

The next proposition ensures that all matrices foetus will have to deal with are call matrices.

Proposition 3.8 (Call Matrix Multiplication) Multiplication on matrices induces a multiplication on call matrices

· : CM(n, m) × CM(m, l) → CM(n, l)

This operation is well defined.

Proof Let A = (a_{ij}) ∈ CM(n, m), B = (b_{ij}) ∈ CM(m, l), AB = C = (c_{ij}) ∈ R^{n×l} and k(i) the index of the element of the ith row of A that is different from “?” (or 1, if no such element exists). Then we have with the rules in semi-ring R

c_{ij} = ∑_{k=1}^{m} a_{ik}b_{kj} = a_{i,k(i)}b_{k(i),j}

Now consider the ith row of C:

c_{i} = (c_{ij})_{1≤j≤l} = (a_{i,k(i)}b_{k(i),j})_{1≤j≤l}

Because at most one b_{k(i),j} is different from “?”, at most one element of c_{i} is different from “?”. Therefore C ∈ CM(n, l).

3.4 Call Graphs

In the following we give a formal treatment of call graphs together with a graph completion algorithm which is a central part of the termination checker.

The nodes of call graphs are function identifiers with a given arity (the names of the function parameters are no longer of relevance). For each i ∈ ℕ we assume an infinite supply F^{(i)} = {f^{(i)}, g^{(i)}, h^{(i)}, ...} of identifiers for functions of arity i. The edges of a call graph are taken from the set of calls:

Calls = {(f^{(n)}, g^{(m)}, A) : f^{(n)} ∈ F^{(n)}, g^{(m)} ∈ F^{(m)}, A ∈ CM(m, n)}.

Since calls contain (besides the call matrix A) the source (f^{(n)}) and the target (g^{(m)}) function identifier with arities, we can simply identify a call graph with its edges:

Definition 3.9 (Call Graph) A call graph is a finite set of calls C ⊆ Calls.

By the following operation, two consecutive calls can be put together.

Definition 3.10 (Call Combination) The partial operation combination of calls is given by

∘ : Calls × Calls → Calls

((g^{(m)}, h^{(l)}, B), (f^{(n)}, g^{(m)}, A)) ↦ (f^{(n)}, h^{(l)}, BA).

That is, if g calls h with call matrix B and f calls g with call matrix A, then f indirectly calls h with call matrix BA. The operation ∘ cannot be applied to calls that have no “common function” like g, therefore it is partial. Call combination can be lifted to sets of calls

∘ : P(Calls) × P(Calls) → P(Calls)

(C, C′) ↦ {c ∘_{Calls} c′ : c ∈ C, c′ ∈ C′, (c, c′) ∈ Dom(∘_{Calls})}

Here we combine each call in C with each call in C′ to which ∘_{Calls} is applicable and form a set of the combined calls. Of course, ∘_{P(Calls)} is a total and monotonic function. For n ≥ 1,

C^{n} := \underbrace{C ∘ … ∘ C}_{n}

denotes the set of calls which are combinations of exactly n calls in C.

To decide whether a call graph is good in the sense that it witnesses the termination of all involved functions, we complete it, i.e., include all indirect calls, and then check whether all reflexive calls of a function to itself are decreasing. Completeness can be defined by means of combination operation ∘:

Definition 3.11 (Complete Call Graphs) A call graph C is complete if C ∘C ⊆ C. The completion C^{∗} is the smallest supergraph of C that is complete.

The completion of a graph C can be computed by the following saturation algorithm.

Theorem 3.12 (Completion Algorithm) Let C be a call graph and (C_{n})_{n∈ℕ} the sequence of call sets defined recursively as follows:

\begin{aligned}C_{1} & := & C \\ C_{n+1} & := & C_{n} ∪ (C_{n} ∘ C) \end{aligned}

Then there exists an n ≥ 1 such that C_{n} = C^{∗}.

Proof Since C has a finite number of nodes and the number of distinct calls between these nodes is finite as well, the C_{i} cannot grow endlessly and there is an n ≥ 1 s.th. C_{i} = C_{n} for all i ≥ n. This implies C_{n} ∘ C ⊆ C_{n+1} ⊆ C_{n} which iteratively gives us C_{n} ∘ C^{i} ⊆ C_{n} for all i ≥ 1. Because

C_{n} = ⋃_{1≤i≤n} C^{i},

we can infer C_{n} ∘ C_{n} ⊆ C_{n}. Thus, C_{n} is complete, and it remains to show minimality to conclude the proof.

Let C′ be any complete supergraph of C. Then C ∘ C ⊆ C′ ∘ C′ ⊆ C′, and iterating this result, we obtain C^{i} ⊆ C′ for all i ≥ 1. Hence, by the laws of set union, C_{n} ⊆ C′ which shows that C_{n} = C^{∗}.

Below we give the completion of our example call graph. Added calls are given by dotted arrows and labelled by call matrices with square brackets.

[figure: flat; [ ^{<} ]; ^{( \begin{matrix}< \\ < \end{matrix} )}; aux; ^{( \begin{matrix}< & · \\ · & ≤ \end{matrix} )}; _{[ \begin{matrix}? & < \\ ? & < \end{matrix} ]}; ( ·  ≤ ); _{[ _{·  <} ]}]

3.5 Lexicographic Orderings

After completing the call graph, foetus checks whether each reflexive call of a function f to itself is decreasing the size of the arguments. For this, lexicographic orderings are considered and the necessary order of the arguments is computed. In the following we provide a formal description.

Definition 3.13 Given C a complete call graph and f a function of arity n. We call

C_{f} := {Δ(A) : (f, f, A) ∈ C} ⊆ R^{n}

the recursion behavior of function f. (Δ takes the diagonal of square matrices).

Each tuple in this set represents one possible recursive call of f and how the orders of all parameters are altered in this call. The diagonals of the call matrices are taken because we want to know only how a parameter relates to its old value in the last call to f.

In the following we identify lexicographic orderings on parameters with permutations π ∈ S_{n} of the arguments. We write π = [k_{0} … k_{n−1}] ∈ S_{n} for the permutation π : i ↦ k_{i}. Often not all of the parameters are relevant for termination; these are not listed in the lexicographic ordering and can appear in the permutation in any sequence. We write π = [k_{0} … k_{m−1}] (m < n) for an arbitrary representative of the subset {π | π(i) = k_{i}, i = 0, …, m − 1} ⊂ S_{n}.

For the following definition we introduce these abbreviations:

π′_{i} = [k′_{0} … k′_{i−1}k′_{i+1} … k′_{n−1}] ∈ S_{n−1}  given π = [k_{0} … k_{n−1}] ∈ S_{n}

where k′_{j} = \{ \begin{matrix}k_{j} & if k_{j} < k_{i} \\ k_{j} − 1 & else \end{matrix}

r′_{i} = (k_{0}, …, k_{i−1}, k_{i+1}, …, k_{n−1}) ∈ R^{n−1} given r = (k_{0}, …, k_{n−1}) ∈ R^{n}
B′_{i} = {r′_{i} | r ∈ B ∧ r_{i} ≠ <} ⊆ R^{n−1}  given B ⊆ R^{n}

The tuple r′_{i} is the result of removing the ith component of r. B′_{i} is the set of which results from removing all relation tuples containing “<” in the ith position and shortening the remaining tuples by the ith component.

Definition 3.14 Let B ⊆ R^{n} be a recursion behavior and π ∈ S_{n} a permutation. We define the relation “π is a lexicographic ordering on B” (π LexOrd B) inductively as follows:

π LexOrd ∅
∃r ∈ B. r_{π(0)} = < ∀r ∈ B. r_{π(0)} ≠ ? π′_{0} LexOrd B′_{π(0)}
π LexOrd B

Note that this definition gives a direct algorithm for computing a lexicographic ordering π for a recursion behavior B: First, find π(0) such that r_{π(0)} = < for one r ∈ B but r_{π(0)} ≠ ? for all r ∈ B. Then, continue with π′_{0} and B′_{π(0)}.

Definition 3.15 Let f be a function of arity n in the call graph C. We say π ∈ S_{n} is a termination ordering for f iff π is a lexicographic ordering on the recursion behavior C_{f} of f:

π TermOrd f :⟺ π LexOrd C_{f}

In our example flat has recursion behavior {(<)} and termination ordering [0] and aux has recursion behavior {(<, ≤), (?, ≤)} and termination ordering [10].

4 An Impredicative Semantic Analysis

Having presented an algorithm to check whether given terms are structurally recursive or not, we want to know whether we can rely on the output of the checker. Thus we have to show that our definition of structural recursion is sound. This involves mutually recursive functions with lexicographic extensions of the structural ordering, generalized inductive types and higher order functions. Consider the evaluation of an application of a structurally recursive function f:

f(u_{0}) ⇝ f(u_{1}) ⇝ f(u_{2}) ⇝ …

This means that during evaluation of f(u_{0}) we have to evaluate f(u_{1}), which again requires evaluation of f(u_{2}) etc. Since f is structurally recursive, we know that

u_{0} > u_{1} > u_{2} > …

where “>” is the structural ordering. Surely the evaluation of f(u_{0}) terminates, if the domain of f is wellfounded, that is, there are no infinite descending chains u_{0} > u_{1} > u_{2} > . . ..

In the following we will prove that in our system all domains are wellfounded. To this end, we first define a semantics for all types (Sect. 4.1). On this semantics we define the structural ordering and show that it is wellfounded (Sect. 4.2). We will extend this ordering lexicographically (Sect. 4.3). Finally we show the soundness of structural recursion by induction over well typed terms (Sect. 4.4).

4.1 Interpretation of the Types

We give a semantics of the types in foetus that captures the “good” values, i.e., those 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. Since we use Knaster-Tarski to define the semantics of μ-types, we must prove monotonicity along its inductive definition.

Definition 4.1 (Semantics) Given a type σ ∈ Ty(X⃗) and closed types τ_{1}, …, τ_{n} (where n = |X⃗|) we define the semantics of σ

[[σ]] : P (Val^{τ_{1}}) × … × P (Val^{τ_{n}}) → P (Val^{σ(τ⃗)})

by induction over σ and simultaneously prove monotonicity of [[σ]]: I.e., V_{i} ⊆ W_{i} for i = 1, …, n (where V_{i}, W_{i} ⊆ Val^{τ_{i}}) implies

[[σ]](V⃗) ⊆ [[σ]](W⃗)

(Var) [[X_{i}]](V⃗) := V_{i}

V_{i} ⊆ W_{i} by assumption.

(Sum) [[Σσ⃗]](V⃗) := ⋃_{j=1}^{n}{in_{j}(v) : v ∈ [[σ_{j}]](V⃗)}

By induction hypothesis {in_{j}(v) : v ∈ [[σ_{j}]](V⃗)} ⊆ {in_{j}(v) : v ∈ [[σ_{j}]](W⃗)} and thus by monotonicity of “∪”

[[Σσ⃗]](V⃗) ⊆ [[Σσ⃗]](W⃗)

(Prod) [[Πσ⃗]](V⃗) := {(v⃗) : v_{i} ∈ [[σ_{i}]](V⃗) for 1 ≤ i ≤ n}

[[Πσ⃗]](V⃗) ⊆ [[Πσ⃗]](W⃗) by ind.hyp. and monotonicity of the cartesian product.

(Arr) [[σ → τ(X⃗)]](V⃗) := { f ∈ Val^{σ→τ(τ⃗)} :
∀u ∈ [[σ]].∃v ∈ [[τ(X⃗)]](V⃗).f@u ⇓ v}

Assume f ∈ [[σ → τ]](V⃗) and u ∈ [[σ]]. By definition there is a value v ∈ [[τ]](V⃗) with f@u ⇓ v. By ind.hyp. v ∈ [[τ]](W⃗) and hence f ∈ [[σ → τ]](W⃗).

(Mu) Since we know that [[σ(X⃗, Y)]](V⃗ , −) is monotone we can use the theorem of Knaster and Tarski to define [[μY.σ(X⃗, Y)]](V⃗) as the smallest set closed under the rule

{v ∈ [[σ]](V⃗ , [[μY.σ]](V⃗)) \atop fold v ∈ [[μY.σ]](V⃗)}

For the monotonicity we must prove that [[μY.σ]](W⃗) is closed under this rule: Assume v ∈ [[σ]](V⃗ , [[μY.σ]](W⃗)). Using the ind.hyp. monotonicity of [[σ]] entails v ∈ [[σ]](W⃗ , [[μY.σ]](W⃗)), hence fold v ∈ [[μY.σ]](W⃗).

Proposition 4.2 (Substitution property)

[[σ(X⃗, Y, Z⃗)]](V⃗ , [[τ]], W⃗) = [[σ(X⃗, τ, Z⃗)]](V⃗ , W⃗)

Proof By induction on σ. The cases (Sum), (Prod) and (Arr) are immediately shown by the induction hypothesis, so let us have a look at the remaining two:

(Var) [[Y]](V⃗ , [[τ]], W⃗) = [[τ]] = [[Y [Y := τ]]](V⃗ , W⃗)

(Mu) “⊆” We must show that the fixed-point on the right side is closed under the rule defining the one on the left (we omit X⃗, Z⃗, V⃗ and W⃗):

{v ∈ [[σ(Y, Z)]]([[τ]], [[μZ.σ(τ, Z)]]) \atop fold v ∈ [[μZ.σ(τ, Z)]]}

By ind.hyp. we get from the assumption v ∈ [[σ(τ, Z)]]([[μZ.σ(τ, Z)]]) which infers the conclusion. “⊇” analogously

Corollary 4.3 (Subset property) Given V_{i} ⊆ [[τ_{i}]]. Then

[[σ(X⃗)]](V⃗) ⊆ [[σ(τ⃗)]]

Proof By iterated application of proposition 4.2 and monotonicity of [[σ]].

4.2 Wellfoundedness of the Structural Ordering on Semantic Values

We now define a transitive structural (pre-)ordering < on semantic values. ^{5} The basic idea is that a value v is structurally smaller than a value w if the representing tree of v is a subtree of w. In our approach the order of a value is only decreased

5 Note that this is different from the relations <, ≤ on terms defined in Sect 3 which formalize the behaviour of the termination checker.

(<) by the destructor (unfold), whereas case analysis, projection and application keep it on the same level (≤). This is because we need the ordering only to show that a function f ∈ Val^{σ→τ} terminates on an input v ∈ [[σ]] if it terminates on all w ∈ [[σ]] that are structurally smaller than v, i.e., w < v. Thus we only need to compare values of the same type σ. Since injection (in_{j}), pairing and building functions by λ enlarge the type and only folding shrinks the type, we need at least one folding step to obtain a greater value v of the same type σ out of a given value w. Hence it is sufficient that unfolding decreases the order strictly.

Definition 4.4 (Codomain) We define the codomain of a function f ∈ [[σ → τ(X⃗)]](V⃗) as

CoDom(f) := {v ∈ [[τ(X⃗)]](V⃗) : ∃u ∈ [[σ]]. f@u ⇓ v}

Definition 4.5 (Structural ordering) We define a pair of mutually dependent families of relations <_{σ,τ} , ≤_{σ,τ} ⊆ [[σ]] × [[τ]] inductively as follows:

(≤refl) v ≤_{σ,σ} v  (Rin) w R_{ρ,σ_{j}} v ; R ∈ {<, ≤} ; w R_{ρ,Σσ⃗} in_{j}(v)

(Rtup)

w R_{ρ,σ_{j}} v_{j} for some j ∈ {1 … n}
R ∈ {<, ≤}
w R_{ρ,Πσ⃗} (v⃗)
(Rarr)

w R_{ρ,τ} v for some v ∈ CoDom(f)
R ∈ {<, ≤}
w R_{ρ,σ→τ} f
(<fold) {w ≤_{σ,τ(μX.τ)} v \atop w <_{σ,μX.τ} fold(v)} (≤fold) {w ≤_{σ,τ(μX.τ)} v \atop w ≤_{σ,μX.τ} fold(v)}

Notation. Since the indexes σ and τ of <_{σ,τ} and ≤_{σ,τ} are determined in most expressions, we omit them for better readability.

Proposition 4.6 (Properties) The relations < and ≤ are transitive, ≤ reflexive and < is contained in ≤, i.e.,

(≤<)  {w <_{ρ,τ} v \atop w ≤_{ρ,τ} v}

Proof We show that w ≤ v is closed under the rules defining w < v: In case of (<fold) we must show w ≤ fold v from the assumption w ≤ v: immediately by (≤fold); in all other cases we can apply the respective ≤-rule on the induction hypothesis.

Only after having shown the theorem 4.8 we can verify that our relation is antisymmetric. However, we shall use the term ordering in anticipation of this fact. The relation < captures our notion of “smaller values” and allows us to prove wellfoundedness of the computation trees of all values.

We want to show that every set of semantic values is wellfounded which is given if every value is accessible. Therefore we first define the sets of accessible values w.r.t. < and then we show that each value is in the accessible set of its type.

Definition 4.7 (Accessibility) Given a family of relations

R_{σ,τ} ⊆ [[σ]] × [[τ]]

indexed over closed types σ, τ ∈ Ty we define the family of accessible sets Acc_{R}^{τ} ⊆ [[τ]] w.r.t. R inductively as follows.

(acc)  {∀σ, w ∈ [[σ]]. w R_{σ,τ} v → w ∈ Acc_{R}^{σ} \atop v ∈ Acc_{R}^{τ}}

Since there is only one introduction rule for Acc_{R}^{τ}, we can invert it and obtain the destructor

(acc^{−1})  {v ∈ Acc_{R}^{τ} w R_{σ,τ} v \atop w ∈ Acc_{R}^{σ}}

Furthermore the definition yields a wellfounded induction principle: Let P^{σ} be a family of predicates over values of type σ.

(accind)  {∀v ∈ [[σ]]. (∀ρ, w ∈ [[ρ]]. w R v → P^{ρ}(w)) → P^{σ}(v) \atop ∀v ∈ Acc_{R}^{σ}. P^{σ}(v)}

Notation. We abbreviate Acc_{<}^{τ} by Acc^{τ}. For lists ρ⃗ of types we use the abbreviation Accρ⃗ := Acc^{ρ_{1}}, …, Acc^{ρ_{n}}.

Now we can show that all semantic values are accessible. It would be sufficient to know that all semantic values of closed types [[σ]] are accessible. But to prove it for μ-types we have to show the stronger proposition that also the semantic values of open types are accessible, where we insert sets of accessible values for the free type variables.

Theorem 4.8 (All semantic values are accessible) Given a type σ ∈ Ty(X⃗) and a closed type ρ_{i} for each free variable X_{i} in σ the following relation holds

[[σ(X⃗)]](Accρ⃗) ⊆ Acc^{σ(ρ⃗)}

We prove this theorem by the fact that the generation of semantic values preserves accessibility (see lemma 4.11). But to show this property we need accessibility of less-equal values (lemma 4.10), which again follows from lemma 4.9.

Lemma 4.9 (Destructors for Acc) If a value is accessible, then component values are accessible as well:

(accout)

in_{j}(v) ∈ Acc^{Σσ⃗}
v ∈ Acc^{σ_{j}}

(accpi)

{(v⃗) ∈ Acc^{Πσ⃗} \atop v_{i} ∈ Acc^{σ_{i}}}

(accres)

f ∈ Acc^{σ→τ}
CoDom(f) ⊆ Acc^{τ}

(accunf) fold(v) ∈ Acc^{μX.σ}

v ∈ Acc^{σ(μX.σ)} Proof (accout) Under the assumption (1) in_{j}(v) ∈ Acc^{Σσ⃗} we have to show v ∈ Acc^{σ_{j}},

what by (acc) refines to w < v → w ∈ Acc^{ρ}. The assumption (2) w < v entails w < in_{j}(v) (by (<in)) and hence using (acc^{−1}) on (1) we obtain w ∈ Acc^{ρ}.

(accpi) analogously using (<tup)

(accres) We have to show v ∈ CoDom(f) → v ∈ Acc^{τ}. Assume v ∈ CoDom(f) and w < v. By (<arr) we get w < f and again (acc^{−1}) proves w ∈ Acc^{ρ},

hence v ∈ Acc^{τ}.

(accunf) To prove accessibility of v we have to show w ∈ Acc^{ρ} under the assumption w < v. By (≤<) and (<fold) we get w < fold(v), and since fold(v) is accessible by the premise, w ∈ Acc^{ρ} by (acc^{−1}).

Lemma 4.10 (Accessibility of less-equal values) The values less than or equal to an accessible value are accessible themselves.

(acc≤)  {v ∈ Acc^{τ} w ≤ v \atop w ∈ Acc^{σ}}

Proof We show that the relation w R_{τ,σ} v :⟺ v ∈ Acc^{σ} → w ∈ Acc^{τ} is closed under the rules defining w ≤ v:

(≤refl) v ∈ Acc^{σ} → v ∈ Acc^{σ} by assumption.

(≤in) From the ind.hyp. v ∈ Acc^{σ_{j}} → w ∈ Acc^{ρ} we have to show

in_{j}(v) ∈ Acc^{Σσ⃗} → w ∈ Acc^{ρ}
This follows from in_{j}(v) ∈ Acc^{Σσ⃗} → v ∈ Acc^{σ} (accout).

In the same way we treat the remaining rules (≤pi), (≤arr) and (≤fold), using the propositions (accpi), (accres) and (accunf).

Lemma 4.11 (Constructors for Acc) A value is accessible if its components are accessible.

(accin)

v ∈ Acc^{σ_{j}}
in_{j}(v) ∈ Acc^{Σσ⃗}

(acctup)

v_{i} ∈ Acc^{σ_{i}} for all 1 ≤ i ≤ n
(v⃗) ∈ Acc^{Πσ⃗}

(accarr)

f ∈ [[σ→τ]] CoDom(f) ⊆ Acc^{τ}
f ∈ Acc^{σ→τ}

(accfold)

v ∈ Acc^{σ(μX.σ)}
fold(v) ∈ Acc^{μX.σ}

Proof For all propositions our goal is of the form [−] ∈ Acc^{−}, what we refine to w < [−] → w ∈ Acc^{ρ}. This we prove by case analysis on w < [−].

(accin) w < in_{j}(v) can only be generated by (<in) from w < v. By (acc^{−1}) we get w ∈ Acc^{ρ}.

(acctup) For w < (v⃗) there must be a j ∈ {1, …, n} s.th. w < v_{j}, and since

v_{j} ∈ Acc_{j}^{σ}, w ∈ Acc^{ρ} holds.

(accarr) w < f is generated by (<arr) from w < v for a v ∈ CoDom(f). Since

by assumption v ∈ Acc^{τ}, we have w ∈ Acc^{ρ}.

(accfold) For w < fold(v) the case (<fold) matches: w ≤ v. By (acc≤) we get w ∈ Acc^{ρ}.

Proof of Theorem 4.8 We show [[σ(X⃗)]](Accρ⃗) ⊆ Acc^{σ(ρ⃗)} by induction over σ(X⃗).

(Var) [[X_{j}]](Accρ⃗) = Acc^{ρ_{j}} = Acc^{X_{j}[X⃗:=ρ⃗]} (Sum) Be v ∈ [[Σσ⃗]](Accρ⃗). Then v = in_{j}(v′) for a suitable j ∈ {1, …, n} and

v′ ∈ [[σ_{j}]](Accρ⃗). By ind.hyp. we have v′ ∈ Acc^{σ_{j}(ρ⃗)}, hence by (accin)

v ∈ Acc^{Σσ⃗(ρ⃗)}.

(Prod) Be (v⃗) ∈ [[Πσ⃗]](Accρ⃗). Since v_{i} ∈ [[σ_{i}]](Accρ⃗) for all 1 ≤ i ≤ n, by

ind.hyp. v_{i} ∈ Acc^{σ_{i}(ρ⃗)}, hence by (acctup) (v⃗) ∈ Acc^{Πσ⃗(ρ⃗)}. (Arr) We assume f ∈ [[σ → τ(X⃗)]](Accρ⃗). Since CoDom(f) ⊆ [[τ(X⃗)]](Accρ⃗)

by definition, the ind.hyp. entails CoDom(f) ⊆ Acc^{τ(ρ⃗)}. Corollary 4.3 infers f ∈ [[σ → τ(ρ⃗)]] and hence by (accarr) f ∈ Acc^{σ→τ(ρ⃗)}. (Mu) We prove that Acc^{μY.σ(ρ⃗,Y)} is closed under the rule that is defining

[[μY.σ(X⃗, Y)]](Accρ⃗), i.e., we show

v ∈ [[σ(X⃗, Y)]](Accρ⃗, Acc^{μY.σ(ρ⃗,Y)})
fold v ∈ Acc^{μY.σ(ρ⃗,Y)}

Applying the ind.hyp. on the premise entails v ∈ Acc^{σ(ρ⃗,μY.σ(ρ⃗,Y))}, and (accfold) infers the conclusion.

Corollary 4.12 The semantic values coincide with the accessible ones.

[[σ(X⃗)]](Accρ⃗) = Acc^{σ(ρ⃗)}

Proof “⊆” by the theorem, “⊇”: Since for closed types ρ from the lemma we immediately get [[ρ]] = Acc^{ρ}, we have by proposition 4.2 Acc^{σ(ρ⃗)} = [[σ(ρ⃗)]] = [[σ(X⃗)]]([[ρ⃗]]) = [[σ(X⃗)]](Accρ⃗).

4.3 Wellfoundedness of the Lexicographic Extension

Since the termination checker allows descent over lexicographic orderings in recursive functions, we have to define it on values and prove that it is wellfounded as well. When denoting tuples in vector notation, we allow ourselves to omit the enclosing parentheses, i.e., for (v⃗) ∈ [[Πσ⃗]] we write just v⃗. Furthermore we use the abbreviations for shortened vectors and permutations as defined in Sect. 3.

Definition 4.13 (Lexicographic Ordering) Given closed types σ⃗ = σ_{1}, …, σ_{n} and a permutation π ∈ S_{n} we inductively define ≺_{Πσ⃗}^{π} ⊆ [[Πσ⃗]] × [[Πσ⃗]] as follows:

(lex<) {v_{π(0)} < w_{π(0)} \atop v⃗ ≺_{Πσ⃗}^{π} w⃗} (lex≤) {v_{π(0)} ≤ w_{π(0)} v′_{π(0)} ≺_{Πσ′_{π(0)}}^{π′_{0}} w′_{π(0)} \atop v⃗ ≺_{Πσ⃗}^{π} w⃗}

Proposition 4.14 (Wellfoundedness of the Lexicographic Ordering) Given closed types σ⃗ = σ_{1}, …, σ_{n} the following relation holds:

[[Πσ⃗]] ⊆ Acc_{≺}^{Πσ⃗}

To show this proposition we need the following lemma:

Lemma 4.15

v⃗ ∈ Acc_{≺} w_{j} ≤ v_{j} w_{i} = v_{i} for all i ≠ j
w⃗ ∈ Acc_{≺}

Proof By case analysis and transitivity of the structural ordering show u⃗ ≺ w⃗ → u⃗ ≺ v⃗ for all u⃗.

Proof of Prop. 4.14 By induction on n. We make extensive use of the wellfounded induction principle.

n = 0 We have to show () ∈ Acc_{≺}^{1}, what refines to

∀w⃗ ≺ (). w⃗ ∈ Acc_{≺}

This is true since no case matches for w⃗ ≺ ().

n→n+1 Or goal is

v_{π(0)} ∈ [[σ_{π(0)}]] → v′_{π(0)} ∈ [[σ′_{π(0)}]] → v⃗ ∈ Acc_{≺^{π}}^{Πσ⃗}

Using theorem 4.8 we can replace [[σ_{π(0)}]] by Acc^{σ_{π(0)}} and apply wellfounded induction on it. This gives us the hypothesis

∀w⃗ ∈ [[Πσ]].w_{π(0)} < v_{π(0)} → w⃗ ∈ Acc_{≺}  (5)

to show v′_{π(0)} ∈ [[σ′_{π(0)}]] → v⃗ ∈ Acc_{≺}. Using the ind.hyp. we can replace

[[σ′_{π(0)}]] by Acc_{≺}^{Πσ′_{π(0)}} and apply well-founded induction, obtaining

∀w⃗ ∈ [[Πσ]].w_{π(0)} = v_{π(0)} → w′_{π(0)} ≺ v′_{π(0)} → w⃗ ∈ Acc_{≺}  (6)

to show v⃗ ∈ Acc_{≺}. For this we have to prove w⃗ ≺ v⃗ → w⃗ ∈ Acc_{≺}. Case analysis on the generation of w⃗ ≺ v⃗: Case w_{π(0)} < v_{π(0)} (lex<): According to (5) w⃗ ∈ Acc_{≺}. Case w_{π(0)} ≤ v_{π(0)}, w′_{π(0)} ≺ v′_{π(0)} (lex≤): Hypothesis (6) entails u⃗ ∈ Acc_{≺}, where u_{π(0)} = v_{π(0)} and u_{i} = w_{i} for i ≠ π(0). Following lemma 4.15 w⃗ ∈ Acc_{≺}.

Corollary 4.16 With regard to the lexicographic ordering, the good value tuples are exactly the accessible ones.

[[Πσ⃗]] = Acc_{≺}^{Πσ⃗}

4.4 Soundness of Structural Recursion

To show that our system is sound, we will prove normalization where we restrict recursive terms to structurally recursive ones. Restricting environments to good ones, i.e., to those containing only semantic values, we show that each term normalizes with regard to the operational semantics defined in Sect. 2.

To this end, we will define good terms TM, good environments [[Γ]] and good closures. After stating that structurally recursive functions terminate, we can do the normalization proof mechanically.

Definition 4.17 (Good Environments) The subset of environments of semantic values over context Γ = x_{1}^{σ_{1}}, …, x_{n}^{σ_{n}} is naturally defined as

[[Γ]] = {x_{1} = v_{1}, …, x_{n} = v_{n} : v_{i} ∈ [[σ_{i}]]} ⊆ Val(Γ)

Definition 4.18 We say a closure c ∈ Cl^{σ} terminates c ⇓ iff it evaluates to some value v ∈ [[σ]]:

c ⇓ :⟺ ∃v ∈ [[σ]]. c ⇓ v

Definition 4.19 (Structural Recursiveness) We define the set of structurally recursive terms SR^{σ→τ} [Γ] of type σ → τ over context Γ as the recursive terms that applied to any value v terminate in any good environment under the condition that they terminate for all structurally smaller values w ≺ v:

SR^{σ→τ} [Γ] := {rec g. t ∈ Tm^{σ→τ} [Γ] : ∀e ∈ [[Γ]], v ∈ [[σ]].
(∀w ∈ [[σ]]. w ≺ v → ⟨rec g. t; e⟩@w ⇓) → ⟨rec g. t; e⟩@v ⇓}

Proposition 4.20 (Structurally recursive functions terminate) Let rec g. t ∈ SR^{σ→τ} and e ∈ [[Γ]]. Then

⟨rec g. t; e⟩ ∈ [[σ → τ]].

Proof Assuming e ∈ [[Γ]] we expand the first premise to

∀v ∈ [[σ]]. (∀w ∈ [[σ]] w ≺ v → ⟨rec g. t; e⟩@w ⇓) → ⟨rec g. t; e⟩@v ⇓

Applying wellfounded induction with the family of predicates P^{ρ} ⊆ [[ρ]] (ρ ∈ Ty) defined as

P^{ρ}(v) := \{ \begin{matrix}⟨rec g. t; e⟩@v ⇓ & if ρ = σ \\ true & else \end{matrix}

yields ∀v ∈ Acc_{≺}^{σ}. ⟨rec g. t; e⟩@v ⇓, which is equivalent to our claim since all values are accessible (Acc_{≺}^{σ} = [[σ]], see corollary 4.16).

With SR^{σ→τ} we have given a semantical criterion for structural recursion. This can be replaced by syntactical criteria for certain classes of structurally recursive functions. In (Abel, 2000), we have provided a criterion that captures non-mutually recursive functions which terminate by lexicographic extensions of the structural ordering. Of course, we were required to give a proof that all such syntactically structurally recursive functions are also semantically structurally recursive.

Definition 4.21 (Good Terms) We inductively define the set of good terms TM^{σ}[Γ] ⊂ Tm^{σ}[Γ] of type σ over context Γ, i.e., the terms that ensure termination. These rules are almost identical to the original term formation rules (see Def. 2.2), we only change Tm to TM and label the rule in CAPITAL letters, e.g.

(TUP)

t_{i} ∈ TM_{i}^{σ}[Γ] for 1 ≤ i ≤ n
(t_{1}, …, t_{n}) ∈ TM^{Πσ⃗}[Γ]

Only the rule (rec) is replaced by

(REC)

t ∈ TM^{σ→τ} [Γ, g^{σ→τ}] rec g. t ∈ SR^{σ→τ} [Γ]
rec g. t ∈ TM^{σ→τ} [Γ]

Definition 4.22 (Good closures) Consequently the set of good closures CL^{τ} of type τ is defined as

CL^{τ} := {⟨t; e⟩ : Γ ∈ Cxt, t ∈ TM^{τ} [Γ], e ∈ [[Γ]]}
∪ {f@u : f ∈ [[σ → τ]], u ∈ [[σ]]}

Again CL^{τ} ⊆ Cl^{τ}, hence we can use our operational semantics ⇓ on good closures as well. Now we are ready to show normalization.

Theorem 4.23 (Normalization) Let t ∈ TM^{σ}[Γ] be a good term of type σ over context Γ and e ∈ [[Γ]] a good environment. Then there exists a v ∈ [[σ]] such that

⟨t; e⟩ ⇓ v.

Proof By induction on t ∈ TM^{σ}[Γ]. We overload the definition of e^{Γ} and now mean e ∈ [[Γ]].

(VAR) Since e^{Γ}, x^{σ} =v, d^{Γ′} ∈ [[Γ, x^{σ}, Γ′]] by (opvar) we prove

⟨x[Γ, x^{σ}Γ′]; e, x = v, d⟩ ⇓ v ∈ [[σ]]

(IN) By ind.hyp. ⟨t^{σ_{j}}; e⟩ ⇓ v ∈ [[σ_{j}]], thus by (opin)

⟨in_{j}(t)^{Σσ⃗}; e⟩ ⇓ in_{j}(v) ∈ [[Σσ⃗]]

(CASE) We must show

⟨case(u^{Σσ⃗}[Γ], x_{1}. t_{1}^{ρ}[Γ, x_{1}^{σ_{1}}], …, x_{n}. t_{n}^{ρ}[Γ, x_{n}^{σ_{n}}]); e⟩ ⇓ v ∈ [[ρ]]

By ind.hyp. we have ⟨u^{Σσ⃗}[Γ]; e⟩ ⇓ w′ ∈ [[Σσ⃗]]. Now w′ must be of form in_{j}(w^{σ_{j}}): By ind.hyp. we get ⟨t_{j}^{ρ}[Γ, x_{j}^{σ_{j}}]; e, x_{j} = w⟩ ⇓ v ∈ [[ρ]], hence by (opcase) we prove our claim.

(TUP) Here we show

⟨(t_{1}^{σ_{1}}, …, t_{n}^{σ_{n}}); e⟩ ⇓

By ind.hyp. we have ⟨t_{i}; e⟩ ⇓ v_{i} ∈ [[σ_{i}]] for all 1 ≤ i ≤ n hence by (optup) ⟨(t⃗); e⟩ ⇓ (v⃗) which is in [[Πσ⃗]] by definition.

(PI) By ind.hyp. ⟨t^{Πσ⃗}; e⟩ ⇓ (v⃗) ∈ [[Πσ⃗]], hence by (oppi)

⟨π_{j}(t); e⟩ ⇓ v_{j} ∈ [[σ]]

for any 1 ≤ j ≤ n. (LAM) By (oplam) ⟨λx^{σ}.t^{τ}; e^{Γ}⟩ ⇓ ⟨λx.t; e⟩. We have to show

⟨λx.t; e⟩ ∈ [[σ → τ]]

i.e. ⟨λx.t; e⟩@u ⇓ for all u ∈ [[σ]]. Refinement by (opappvl) reduces our goal to ⟨t; e, x = u⟩ ⇓ which we get by the induction hypothesis.

(REC) Here by (oprec) we have to show

⟨rec g. t; e⟩ ∈ [[σ → τ]]

which is true by lemma 4.20 since rec g. t ∈ SR^{σ→τ} by definition. (APP) By ind.hyp. we have ⟨t^{σ→τ}; e⟩ ⇓ f ∈ [[σ → τ]] and ⟨s; e⟩ ⇓ u ∈ [[σ]]

therefore f@u ⇓ and futhermore by (opapp)

⟨t s; e⟩ ⇓

(FOLD) By ind.hyp. ⟨t; e⟩ ⇓ v ∈ [[σ(μX.σ)]], hence by (opfold)

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

which is in [[μX.σ]] by definition. (UNF) By ind.hyp. ⟨t; e⟩ ⇓ fold(v) ∈ [[μX.σ]], hence

⟨unfold(t); e⟩ ⇓ v

by (opunfold), which is in [[σ(μX.σ)]].

Note that we have also shown normalization for mutual recursive terms (as for instance our example flat): They are handled by case (REC). Since in all terms accepted by termination checker all recursive subterms are in SR, they are “good” by Proposition 4.20.

5 A Predicative Analysis using Set Based Operators

In definition 4.1 we used the theorem of Knaster-Tarski to construct the interpretation of μ-Types. In this section we shall show that impredicative reasoning is not necessary and can be replaced by strictly positive inductive definitions.

5.1 On Inductive Definitions

A set μ ⊆ U is considered to be inductively defined if it is the fixpoint of some monotone operator Φ : P(U) → P(U). According to the Knaster-Tarski theorem every such operator has a such a least fixpoint, defined by

μ = ⋂{P ⊆ U | Φ(P) ⊆ P }

This fixpoint satisfies the following two rules

(intro) {v ∈ Φ(μ) \atop v ∈ μ}  (elim) {v ∈ μ Φ(V) ⊆ V \atop v ∈ V}

The first rule expresses that μ is a prefixpoint (Φ(μ) ⊆ μ). The second implies that μ ⊆ Φ(μ), and hence that μ is a fixpoint; but the second rule also implies that μ is least, i.e. a subset of every other fixpoint.

The definition above is said to be impredicative, since it is defining a set, μ, by reference to the totality of subsets of U, of which μ itself is a member. There is a second, predicative, way of defining the least fixpoint, from the bottom up. Define μ_{0} = ∅, μ_{α+1} = Φ(μ_{α}) and μ_{lim γ} = ⋃{μ_{α} | α ∈ γ}. Then

μ = ⋃{μ_{α} | α ∈ Ω}

where Ω is the least uncountable ordinal.

We are calling predicative those theories of inductive definitions that are based on this latter conception of the construction of μ, which is still sufficient to justify the two rules above. In such a theory, one needs a syntactic means of ensuring that the operator Φ is monotone. Classically, it is enough to ensure that Φ is positive, but constructively, it is more desirable to have a strictly positive operator. In fact, from a constructive point of view, it is desirable to have Φ take the following very simple form:

Φ(V) = {v ∈ P : ∀w. w R v → w ∈ V },

where P is a set and R some binary relation. In this case, we say that the fixpoint μ of Φ is accessibility inductively defined; it is interpreted as the accessible (or wellfounded) part of R in P. Accessibility inductive definitions are deterministic, that is, for each v ∈ μ there is a unique well-founded deduction tree which shows how v enters the inductively defined set μ. We quote a discussion on inductive definitions from (Buchholz et al., 1981), p. 8:

Accessibility inductive definitions enjoy a privileged position in our informal conception of the subject. We have a direct picture of how the members of such i.d. sets are generated, which leads us immediately to recognize the ID axioms [i.e. the fixpoint introduction and elimination rule] for them as correct. This is the picture “from below”. Furthermore, we can carry out definition by recursion on accessibility i.d. sets. However the axioms for nonaccessibility inductive definitions either need to be justified by impredicative principles “from above” (for the least set satisfying given closure conditions) or require a prior classical theory of ordinals.

In this section, we show that we can replace the positive fixpoint definition of the previous section by an accessibility definition, giving the construction a clear predicative character.

An example is the operator defining accessible sets given in Sect. 4.2 (simplified for clarity):

Φ_{Acc}^{ρ}(V) := {v ∈ [[ρ]] : ∀w < v. w ∈ V }

The fixpoint of Φ_{Acc}^{ρ} is the set Acc^{ρ} of accessible values of type ρ. The variable V appears never on the right hand side of an arrow and thus the operator is strictly positive. In contrast, the operator Φ_{[[μX.σ]]} given above is not strictly positive since the variable V appears as an argument of [[σ]]. If [[σ]](V) was just a notational definition, we could expand it and check whether V appears strictly positive, but unfortunately the interpretation [[−]] is defined by recursion on the structure of the type σ and thus we cannot know what [[σ]] “does” with its argument.

A solution to the problem is to replace Φ_{[[μX.σ]]} by a semantically equivalent operator which is strictly positive. Indeed, that can be done using Peter Aczel’s set based operators, as we show in the next section. An alternative would be to reformulate the definition of types s.th. the interpretation can be given by a strictly positive inductive definition directly. This approach has been carried out by Holger Benl (1998) using vector notation and simultaneously inductive types instead of interleaving inductive types. However, his proof could only be implemented in a predicative theorem proving system that considers vector notation as primitive.

5.2 Interpreting Strictly Positive Types

The interpretation [[σ]] of a strictly positive inductive type σ is monotone, but this does not seem to capture the fundamental property of strictly positive types. Indeed, we could show in (Abel, 1999) that a wider class of types enjoy this property: the positive types. In the following we will show that strictly positive types are interpreted as operators that are set based, which makes their definition by a predicative inductive definition possible. We consider set-basedness to be the characterizing property of strictly positive types.

We extend Def. 4.1 of the semantics by the requirement that each operator has to come with an urelement relation U. The construction follows closely the one presented in (Abel & Altenkirch, 2000). Here the verification is simpler because we do not need closure rules to achieve saturatedness.

Definition 5.1 (Semantics) For σ ∈ Ty(X⃗) and closed types τ_{1}, …, τ_{n} we define

[[σ]] : P (Val^{τ_{1}}) × … × P (Val^{τ_{n}}) → P (Val^{σ(τ⃗)})

as in definition 4.1 but we additionally require that there are relations

U_{i}^{σ} ⊆ Val^{τ_{i}} × Val^{σ(τ⃗)} for 1 ≤ i ≤ n

such that for all 1 ≤ i ≤ n, v ∈ Val^{σ(τ⃗)} and u ∈ Val^{τ_{i}}:

v ∈ [[σ]](V⃗)  u U_{i}^{σ} v ; \overline{(sb1)} ; u ∈ V_{i}  v ∈ [[σ]](Valτ⃗) ; \overline{(sb2)} ; v ∈ [[σ]](U⃗(v))

where U⃗(v) = {w⃗ | ∀_{1≤i≤n}w_{i}U_{i}^{σ}v}.

The definition of [[σ]] in the cases (Var), (Sum), (Prod), (Arr) is the same as before. The interpretation of μ-types is replaced by

{v ∈ [[σ]](V⃗ , Val^{μX.σ}) ∀u. u U_{n+1}^{σ} v → u ∈ [[μX.σ]](V⃗) \atop fold(v) ∈ [[μX.σ]](V⃗)}

Below we will define the relations U_{i}^{σ} and show that they satisfy the required properties.

The rule (sb1), which can be read as v ∈ [[σ]](V⃗) → U_{i}^{σ}(v) ⊆ V_{i}, states that the relations U_{i} “sort” the urelements of v back into the sets V_{i} they came from. More precisely, if u U_{i} v holds then u is a urelement of v that came from value set V_{i}. Rule (sb2) expresses that a value v can be reconstructed from its urelements.

Let us demonstrate the urelement-relation in the case of lists, where it actually implements an element relation. Lists of element type X can be defined as

List(X) ≡ μY. 1 + X × Y

Given a closed type τ and a set of values V ⊆ Val^{τ} lists can be introduced by the following two rules:

[] ∈ [[List]](V)

u ∈ V v ∈ [[List]](V)
u :: v ∈ [[List]](V)

For readability we use the notational definitions [] ≡ fold(in_{1}()) and u :: v ≡ fold(in_{2}(u, v)). The urelement relation can be defined by these rules:

u U^{List} u :: v  u U^{List} v ; u U^{List} w :: v

Property (sb1) for U^{List} states that for all lists v all elements u U v must have come from V. Property (sb2), which states that a list can be constructed from its elements, is non-trivial.

Proposition 5.2 (set basedness for lists) (sb1) If v ∈ [[List]](V) and u U v then u ∈ V. (sb2) If v ∈ [[List(τ)]] then v ∈ [[List]](U(v)).

Proof (sb1) By induction on u U v. (sb2) By induction on v ∈ [[List(τ)]]: The base case is trivial. For v = u :: v′ we have by induction hypothesis that v′ ∈ [[List]](U(v′)). By the definition of U for lists it holds that U(v′) ⊆ U(u :: v′). Thus we can make use of the monotonicity of [[List]] and derive v′ ∈ [[List]](U(u :: v′)) from which our goal follows.

These proofs serve as models for the proofs in the general inductive case.

The following theorem illustrates the benefit of set basedness: The interpretation of strictly positive types can be made strictly positive itself.

Theorem 5.3 (Fundamental property of strictly positive types) Assuming that (sb1) and (sb2) hold for U, Every [[σ]](V⃗) is equivalent to a predicate which is strictly positive in V⃗ - that is for v ∈ Val^{σ(τ⃗)}:

v ∈ [[σ]](V⃗) ⟺ v ∈ [[σ]](Valτ⃗) ∧ ∀i. U_{i}^{σ}(v) ⊆ V_{i}

Proof ⇒ Assuming v ∈ [[σ]](V⃗), we obtain v ∈ [[σ]](Valτ⃗) by monotonicity and U_{i}^{σ}(v) ⊆ V_{i}

for all i by (sb1).

⇐ Using (sb2), v ∈ [[σ]](Valτ⃗) entails

v ∈ [[σ]](U⃗^{σ}(v))

Since by assumption U⃗^{σ}(v) ⊆ V⃗ (component wise), we can derive v ∈ [[σ]](V⃗) by monotonicity.

We see at a glance that the new, strictly positive operator for the interpretation of inductive types given in Def. 5.1 constructs the same semantics as the old in Def. 4.1, which can be written as

{v ∈ [[σ]](V⃗ , [[μX.σ]](V⃗)) \atop fold(v) ∈ [[μX.σ]](V⃗)}

The premises of the old rule match the left hand side of the equivalence in Theorem 5.3, and the premises of the new rule the right hand side.

We now complete Def. 5.1 and give the definition of the urelement relation U^{σ} by induction over the type σ. In each case it is defined inductively by a set of strictly positive rules and we have to prove the laws of set basedness. In each case (sb1) is proven by induction over the derivation of u U v and (sb2) is shown by induction over v ∈ [[σ]](Valτ⃗), using monotonicity of the operators and the set basedness properties for the already defined types. We only give a detailed proof for the non-trivial case of μ-types. (Var)

{v ∈ V_{i} \atop v U_{i}^{X_{i}} v}

(Sum) For all 1 ≤ j ≤ |σ⃗|

{u U_{i}^{σ_{j}} v \atop u U_{i}^{Σσ⃗} in_{j}(v)}

(Prod)

{u U_{i}^{σ_{j}} v_{j} for all 1 ≤ j ≤ |σ⃗| \atop u U_{i}^{Πσ⃗} (v⃗)}

(Arr)

{v ∈ CoDom(f) u U_{i}^{τ} v \atop u U_{i}^{σ→τ} f}

(Mu) U^{μX.σ} is defined inductively by the following two rules:

(non-rec) {1 ≤ i ≤ n u U_{i}^{σ} v \atop u U_{i}^{μX.σ} fold(v)}  (rec) {v′ U_{n+1}^{σ} v u U_{i}^{μX.σ} v′ \atop u U_{i}^{μX.σ} fold(v)}

(sb1) We show that

u R_{i} v :⟺ v ∈ [[μX.σ]](V⃗) → u ∈ V_{i}

is closed under the rules defining U_{i}^{μX.σ}

(non-rec) If fold(v) ∈ [[μX.σ]](V⃗) then v ∈ [[σ]](V⃗ , [[μX.σ]](V⃗)) and hence (sb1) for σ entails that u U_{i}^{σ} v implies u ∈ V_{i}.

(rec) As before we have v ∈ [[σ]](V⃗ , [[μX.σ]](V⃗)). Hence, using (sb1) for σ, the first premise v′ U_{n+1}^{σ} v implies v′ ∈ [[μX.σ]](V⃗). Now we use the second premise u R_{i} v′ to conclude u ∈ V_{i}.

(sb2) We show that the set

Q = {v | v ∈ [[μX.σ]](U⃗^{μX.σ}(v))}

is closed under the rule defining [[μX.σ]](Valτ⃗). We assume

v ∈ [[σ]](Valτ⃗, Q)  (7)

which by using (sb2) for σ entails

v ∈ [[σ]](U⃗^{σ}(v))  (8)

To show that fold(v) ∈ Q it suffices to show

v ∈ [[σ]](U⃗^{μX.σ}(fold(v)), [[μX.σ]](U⃗^{μX.σ}(fold(v))))

We derive this from 8 using (mon), which leaves us two subgoals

1. We have to show that U_{i}^{σ}(v) ⊆ U_{i}^{μX.σ}(fold(v)) which follows from (non-rec).

2. To show U_{n+1}^{σ}(v) ⊆ [[μX.σ]](U⃗^{μX.σ}(fold(v))) assume

v′ U_{n+1}^{σ} v  (9)

Under this assumption we have that U_{i}^{μX.σ}(v′) ⊆ U_{i}^{μX.σ}(fold(v)) by (rec). Using (sb1) for σ on 7 and 9 we have that v′ ∈ Q, i.e.,

v′ ∈ [[μX.σ]](U⃗^{μX.σ}(v′))

and hence using (mon) v′ ∈ [[μX.σ]](U⃗^{μX.σ}(fold(v))).

6 Conclusions and Further Work

We have introduced a termination checker foetus for structurally recursive terms that recognizes also descent via a lexicographic ordering. We have given an interpretation of the types, transfered the ordering onto the interpretation and thus have shown that (even mutually) recursive terms accepted by foetus are sound.

In (Abel, 2000) our work is continued: We introduce a judgment that implements a syntactic check whether functions are structurally recursive. This judgment is an abstract description of the algorithm that foetus uses to decide whether functions are structurally recursive or not. We then prove that this syntactic check is sound w.r.t. to the semantics given here. This proof is restricted to non-mutual recursion, the proof for mutual recursion is in preparation.

We would like to extend our work to (predicatively) polymorphic, coinductive and dependent types. To handle corecursive functions especially the interplay between guarded and structurally recursive has to be considered. Introducing dependent types, more effort has to be done to check the totality of a pattern.

6.1 Related Work

Publications on termination are numerous since research in this area has been carried out since the very beginnings of computer science. Much work has been done in the context of term rewriting systems and we want to cite the seminal investigations of Christoph Walther (1988):

Walther has described reduction checking, which is sometimes referred to as “Walther recursion” (McAllester & Arkoudas, 1996). His estimation calculus examines whether functions are terminating and 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. More work on the estimation calculus has been done by Bundy and others (Gow et al., 1999).

Closely related to our work, though in the area of extensible term rewriting systems is the work of Blanqui, Jouannaud and Okada (2001). They define structurally recursive terms syntactically using side conditions by their Extended General Schema. Since they do not handle mutually recursive functions, their approach seems to have the same strength as the formal system we present in Sect. 3.2.

Gimenéz (1995) presents a syntactic translation of structural (and guarded) recursive definitions into (dependently typed) recursors in the context of the Coq system (Barras et al. , 2000)—based on the Calculus of Constructions (Coquand & Huet, 1988). We avoid having to introduce and analyze a type theory with recursors but consider structural recursion as a primitive principle. The consideration of predicativity does not play a role in Giminéz’ work because Coq is impredicative anyway.

More recently Gimenéz (1998) has shown how to integrate guardedness and termination checking into type-checking. He uses a tagged version of the types to indicate whether its inhabitants are guarded by a constructor. This technique yields partial reduction checking for free: The type system can capture whether a function is a preserver, but not whether it is a reducer. His type system does not contain Σ-types and thus he cannot handle lexicographic descent. An extension to Σ-types is non-trivial since it is not obvious how to incorporate lexicographic products into his subtyping calculus.

Gimenéz motivated his new technique as follows: Side-conditions in typing rules that ensure termination are undesirable since it is difficult to construct a semantics for the types, which is needed in normalization proofs. In this article we manage to construct a sound interpretation for the types and a rigid normalization proof is given by one of the authors (Abel, 2000). Altogether, we consider Gimenéz’ approach as very promising; it deserves more attention by the scientific community.

Amadio and Coupet-Grimal (1998) analyze a λ-calculus with coinductive types where the guardedness check is woven into the typing rules. They give a PER model of the types and interpret the terms in the untyped λ-calculus (in contrast to our observable values interpretation). Furthermore they give a proof of strong normalization for a restricted reduction rule for corecursively constructed data.

Codata are only unfolded in the head position of a case-construct, which corresponds to our approach to expand recursive functions only in case of an application.

Telford and Turner (1999) are investigating Elementary Strong Functional Programming, i.e., functional programming languages where only terminating functions can be defined. Technically they use abstract interpretations to ensure termination. They can handle a wider class of functions since they keep track not whether an argument is decreasing but how much it is decreasing or increasing, thus allowing temporary growth that is compensated by sufficient shrinkage later. We consider their technique as a promising alternative to our logical approach. However the focus of our work is not maximal completeness but a solid theoretical foundation.

Lee, Jones and Ben-Amram (2001) introduce a new paradigm into reasoning about termination: “a program terminates on all inputs if every infinite call sequence (...) would cause an infinite descent in some data values”. Thus they characterize terminating functions as those accepted by certain Büchi automata. An interesting result is that termination checking is PSPACE-complete. For the practical implementation of termination checking they propose an algorithm based on size-change graphs, which can be translated into our call graphs. Their algorithm performs graph completion as well as ours, thus their complexity results should apply to ours as well.

Finally, Pientka and Pfenning (2000) have implemented reduction and termination checking for the logical framework LF (Harper et al., 1993). Their algorithm does not infer termination orderings, but checks termination using an ordering the user specifies. The formulation of the algorithm is judgment-based like ours and justified by a cut admissibility argument rather than a soundness proof as in our case.

6.2 Acknowledgements

The authors like to thank Catarina and Thierry Coquand for inspiring e-mail exchange and discussions. The predicative semantics in Section 5 was inspired by Thierry Coquand’s proposal that this should be carried out using Peter Aczel’s set based operators. We thank Jeremy Avigad, Ralph Matthes, Frank Pfenning and the anonymous referee for comments on draft versions of this paper.

The first author thanks the creator of the universe who gave mankind the gift of creativity and abstract thinking.

References

Abel, Andreas. (1999). A semantic analysis of structural recursion. Diplomarbeit, Uni-

versity of Munich. Abel, Andreas. (2000). Specification and verification of a formal system for structurally

recursive functions. Types for Proof and Programs, International Workshop, TYPES ’99, Selected Papers. Lecture Notes in Computer Science, vol. 1956. Springer-Verlag.

Abel, Andreas, & Altenkirch, Thorsten. (2000). A predicative strong normalisation proof for a λ-calculus with interleaving inductive types. Types for Proof and Programs, Inter-

40 A. Abel and T. Altenkirch

national Workshop, TYPES ’99, Selected Papers. Lecture Notes in Computer Science, vol. 1956.

Aczel, Peter. (1997). Notes on constructive set theory. Published on the WWW. Amadio, Roberto M., & Coupet-Grimal, Solange. (1998). Analysis of a guard condition

in type theory. Nivat, Maurice (ed), Foundations of Software Science and Computation Structures, First International Conference, FoSSaCS’98. Lecture Notes in Computer Science, vol. 1378. Springer-Verlag.

Barras, Bruno, et al. . (2000). The Coq proof assistant reference manual. INRIA. Version

6.3.11. Benl, Holger. (1998). Konstruktive Interpretation induktiver Typen. Diplomarbeit, Uni-

versity of Munich. Blanqui, Frédéric, Jouannaud, Jean-Pierre, & Okada, Mitsuhiro. (2001). Inductive data

type systems. Theoretical Computer Science, 277. Buchholz, Wilfried, Feferman, Solomon, Pohlers, Wolfram, & Sieg, Wilfried. (1981). It-

erated inductive definitions and subsystems of analysis: Recent proof-theoretical studies. Lecture Notes in Mathematics, vol. 897. Springer-Verlag.

Coquand, Catarina. (1999). Agda home page. Coquand, Thierry. (1992). Pattern matching with dependent types. Proceedings of the

1992 Workshop on Types for Proofs and Programs. Coquand, Thierry, & Huet, Gerard. (1988). The calculus of constructions. Information

and Computation, 76, 95 – 120. de Bruijn, N. G. (1972). Lambda calculus notation with nameless dummies, a tool for

automatic formula manipulation, with application to the Church-Rosser theorem. Indagationes mathematicae, 34, 381–392.

Dershowitz, Nachum. (1987). Termination of rewriting. Journal of Symbolic Computation,

3, 69–115. Giesl, Jürgen. (1995). Termination analysis for functional programs using term orderings.

Proceedings of the Second International Static Analysis Symposium. Lecture Notes in Computer Science, vol. 983. Springer-Verlag.

Gimenéz, Eduardo. (1995). Codifying guarded definitions with recursive schemes. Pages 39–59 of: Dybjer, Peter, Nordström, Bengt, & Smith, Jan (eds), Types for Proofs and Programs, International Workshop TYPES´ 94, Bøastad, Sweden, June 6-10, 1994, Selected Papers. Lecture Notes in Computer Science, vol. 996. Springer-Verlag.

Gimenéz, Eduardo. (1998). Structural recursive definitions in type theory. Pages 397–408 of: Automata, Languages and Programming, 25th International Colloquium, ICALP’98, Aalborg, Denmark, July 13-17, 1998, Proceedings. Lecture Notes in Computer Science, vol. 1443. Springer-Verlag.

Girard, Jean-Yves. (1972). Interprétation fonctionnelle et élimination des coupures dans

l’arithmétique d’ordre supérieur. Thèse de Doctorat d’État, Université de Paris VII. Gow, Jeremy, Bundy, Alan, & Green, Ian. (1999). Extensions to the estimation calculus.

Pages 258–272 of: Ganzinger, H., McAllester, D., & Voronkov, A. (eds), Proceedings of the 6th International Conference on Logic for Programming and Automated Reasoning (LPAR’99). LNAI, no. 1705. Springer-Verlag.

Harper, Robert. (2000). Programming in Standard ML. Carnegie Mellon University. Harper, Robert, Honsell, Furio, & Plotkin, Gordon. (1993). A Framework for Defining

Logics. Journal of the Association of Computing Machinery, 40(1), 143–184. Jones, Mark P, & Reid, Alastair. (1999). The Hugs 98 user manual. The Yale

Haskell Group and the Oregon Graduate Institute of Science and Technology, http://www.haskell.org/hugs/.

Structural Recursion 41

Lee, Chin Soon, Jones, Neil D., & Ben-Amram, Amir M. (2001). The size-change principle for program termination. ACM Symposium on Principles of Programming Languages. ACM Press.

Martin-Löf, Per. (1984). Intuitionistic type theory. Bibliopolis. McAllester, David, & Arkoudas, Kostas. (1996). Walther recursion. McRobbie, M. A.,

& Slaney, J. K. (eds), 13th International Conference on Automated Deduction, New Brunswick, NJ, USA, July 30 – August 3, 1996, Proceedings. Lecture Notes in Computer Science, vol. 1104. Springer-Verlag.

Nordström, Bengt, Petersson, Kent, & Smith, Jan M. (1990). Programming in Martin-Löf

type theory: An introduction. Clarendon Press, Oxford. Pientka, Brigitte, & Pfenning, Frank. (2000). Termination and reduction checking in the

Logical Framework. Workshop on Automation of Proofs by Mathematical Induction, CADE-17, Pittsburgh, PA, USA.

Tarski, Alfred. (1955). A lattice-theoretical fixpoint theorem and its applications. Pacific

Journal of Mathematics, 5, 285 – 309. Telford, Alistair J., & Turner, David A. (1999). Ensuring termination in ESFP. 15th

British Colloquium in Theoretical Computer Science. Walther, Christoph. (1988). Argument-bounded algorithms as a basis for automated ter-

mination proofs. Pages 602–621 of: Lusk, Ewing L., & Overbeek, Ross A. (eds), 9th International Conference on Automated Deduction. Lecture Notes in Computer Science, vol. 310. Springer-Verlag.