Theoretical Informatics and Applications Will be set by the publisher

Informatique Théorique et Applications

TERMINATION CHECKING WITH TYPES^{∗}

Andreas Abel^{1}

Abstract. The paradigm of type-based termination is explored for functional programming with recursive data types. The article introduces Λ_{μ}^{+}, a lambda-calculus with recursion, inductive types, subtyping and bounded quantification. Decorated type variables representing approximations of inductive types are used to track the size of function arguments and return values. The system is shown to be type safe and strongly normalizing. The main novelty is a bidirectional type checking algorithm whose soundness is established formally.

1991 Mathematics Subject Classification. 68N15, 68N18, 68Q42.

Introduction

In interactive theorem provers like Alfa [26], Coq [29], or LEGO [33,43], which are based on the Curry-Howard isomorphism, inductive proofs can be supplied as recursive functions. However, only functions which terminate on all inputs constitute valid proofs. In functional programming, functions are commonly defined via general recursion and pattern matching. This imposes some challenge on proof validation and, in general, it is undecidable whether a recursive program terminates.

Many termination checkers which analyze untyped program code follow methods from term rewriting and rely on term orderings. In previous work [1], we used the subterm ordering extended to higher-order functions to capture the class of structurally recursive functions over strictly positive inductive datatypes. For

\begin{matrix}c \\ ◯ \end{matrix} EDP Sciences 1999

Keywords and phrases: Type-based termination, sized types, inductive types, course-of-value

recursion, bidirectional type checking, strong normalization

∗ Research supported by the Graduiertenkolleg Logik in der Informatik (PhD Program Logic in

Computer Science) of the Deutsche Forschungsgemeinschaft, the thematic networks TYPES

(IST-1999-29001) and Applied Semantics II (IST-2001-38957) of the European Union and

the project CoVer of the Swedish Foundation of Strategic Research.

1 Department of Computer Science, Chalmers University of Technology, Rännvägen 6, 41296

Göteborg, Sweden, e-mail: abel@cs.chalmers.se

polynomial inductive types, a greater class of functions is accepted in Telford and Turner’s ESFP [46]. Their termination checker also incorporates a limited form of size-change and dataflow analysis which recognizes certain functions as reducers or preservers. Functions in these classes—first described by Walther [48]—have the property that the size of their output is bounded by the size of some input argument (strictly smaller in the case of reducers). Finally, Pientka [40] has implemented termination and reduction checking for higher-order logic programs based on the subterm ordering.

Such termination checkers, using syntactical conditions, have some drawbacks. First, for non-strictly positive inductive types it is not clear how a syntactic criterion should look like (see Section 7). Secondly, the acceptance of a program is often sensitive to small changes in the code (introduction of redexes, substitution of expressions by others of equal value).

Termination checking should abstract from the precise syntactical formulation of an algorithm; therefore Giménez [23] advocates a type-based termination method. The idea is to equip the types of recursive data structures with size information. A recursive function is only accepted if the sizes of arguments to recursive calls are bounded by the size of its inputs. Being an abstract property like type, the size information is insensitive to small reformulations of expressions. A nice feature of sized types is that function types can express whether functions are size-preserving. Hence, termination checking scales to higher-order languages which are problematic for purely syntactic methods.

Giménez was not the first to describe type-based termination; Hughes, Pareto and Sabry [28] described sized types for reactive functional programming, also in combination with region types [27, 37]. Amadio and Coupet-Grimal [7] used guarded types to ensure productivity of infinite structures like streams. Although these ideas have been around for some time, people are reluctant to pick up on them, probably because they shun changes in their type theories.

The aim of this article is to provide a gentle access to sized types for termination in order to increase their popularity. Therefore we restrict Giménez [23] proposal— sized types for the Calculus of Constructions—to a simply-typed setting, ignore coinductive types for now and confine subtyping to the necessary minimum. Once type-based termination is understood at this simple level, one can go ahead and upgrade to rich type theories with full subtyping, polymorphism or even dependent types.

For the system presented, we show type safety syntactically and termination semantically, by modeling types as set of strongly normalizing terms. Independently, Barthe et al. [9] have defined a similar restriction of Giménez original proposal and proven subject reduction and strong normalization. Relative to their work, the novel contributions of this article are:

(1) An informal introduction into type based termination, starting with its simplest form, Mendler’s rule for recursion [35], and ending with our restriction of Giménez’ system.

(2) A bidirectional type checking algorithm for our calculus. This is the main technical novelty.

(3) A motivation why the result type of a recursive function can only monotonically depend on the type of its input. This side condition was missing in Giménez original formulation [23]. We give an example of a nonterminating function which is accepted by the type system if the side condition is dropped.

The article is structured as follows. In Section 1, we introduce a core language Λ_{μ} with recursive datatypes and non-termination functions and show that it has the strong type soundness property. By restricting the type of the fixed-point combinator, one can force recursive functions to be total. In Section 2, we start with Mendler’s recursion rule [35], “the mother of type-based termination”, and refine it step by step, enlarging the class of accepted functions, until we reach Giménez’ rule. The formal presentation of the type system Λ_{μ}^{+} is given in Section 3, together with a type-checking algorithm in Section 4. A proof of strong normalization follows in Section 5. In Section 6, we first discuss the above mentioned side condition. Secondly, we show how to represent productive streams in our type system as functions over natural numbers. Thus, we motivate, form the perspective of inductive types, the rules for sized coinductive types given by Giménez [23] and Barthe et al. [9]. Several applications for type-based termination are sketched in Section 7, before we conclude with an summary of related work in Section 8.

1. A Core Language with Recursion

We consider termination in the setting of simply-typed functional programming with recursive datatypes. Table 1 shows the core language Λ_{μ}, a lambda-calculus with finite sums and products and positive recursive types. By the latter we mean recursive types μX.σ such that on each walk from the binding site to an occurrence of the variable X we choose the left component of an arrow type an even number of times (see itypes in Section 3). The particular selection of type and term formers is inspired by category theory [25].

Throughout the paper we consider α-equivalent terms or types as identical. In all contexts we consider the variable names to be unique. Both properties can be ensured by considering the variable names as just a sugar for de Bruijn indices, which we shall do for the whole of this article. We write [N/x]M resp. [ρ/Y]τ (or τ(ρ)) for capture-avoiding substitution in terms resp. types. We take the liberty to drop the dot in a binder if the expression after a binding consists of a single symbol (e.g., λxM, μXσ).^{1}

Table 1 lists the rules of the static semantics, the typing judgement Γ ⊢ M : τ, and the axioms of the dynamic semantics, the computation relation M ⟶_{β} M′. In our terminology, a β-redex, i.e., the left hand side of a reduction axiom, shall denote any elimination of a matching introduction. This notion is a generalization of β-redexes in simply-typed λ-calculus to richer type systems. The full reduction

1This goes well with the definition of “.” which denotes an “opening parenthesis which closes as far to the right as syntactically possible”.

4 TITLE WILL BE SET BY THE PUBLISHER Types:

ρ, σ, τ ::= X | 1 | σ + τ | σ × τ | σ → τ | μX.ρ (where X appears only positively in ρ) Terms:

Λ_{μ} ∋ M, N ::= x | λx.M | M_{1} M_{2} | inl M | inr M | (case M of inl x_{1} ⇒ M_{1} | inr x_{2} ⇒ M_{2})
| () | (M_{1}, M_{2}) | fst M | snd M | fold M | unfold M | fix g(x).M

Contexts (all variables distinct):

Γ ::= · | Γ, x: τ

Typing (τ and all types in Γ closed):

Γ ⊢ M : τ

Lambda-calculus:

\frac{x: τ ∈ Γ}{Γ ⊢ x : τ} \frac{Γ, x: σ ⊢ M : τ}{Γ ⊢ λx.M : σ → τ} \frac{Γ ⊢ M_{1} : σ → τ Γ ⊢ M_{2} : σ}{Γ ⊢ M_{1} M_{2} : τ}

Sum types:

\frac{Γ ⊢ M : σ}{Γ ⊢ inl M : σ + τ} \frac{Γ ⊢ M : τ}{Γ ⊢ inr M : σ + τ} \frac{Γ ⊢ M : σ + τ Γ, x_{1} : σ ⊢ M_{1} : ρ Γ, x_{2} : τ ⊢ M_{2} : ρ}{Γ ⊢ case M of inl x_{1} ⇒ M_{1} | inr x_{2} ⇒ M_{2} : ρ}

Product types:

\overline{Γ ⊢ () : 1} \frac{Γ ⊢ M_{1} : σ Γ ⊢ M_{2} : τ}{Γ ⊢ (M_{1}, M_{2}) : σ × τ} \frac{Γ ⊢ M : σ × τ}{Γ ⊢ fst M : σ} \frac{Γ ⊢ M : σ × τ}{Γ ⊢ snd M : τ}

Recursive types and terms:

\frac{Γ ⊢ M : σ(μX.σ)}{Γ ⊢ fold M : μX.σ} \frac{Γ ⊢ M : μX.σ}{Γ ⊢ unfold M : σ(μX.σ)} \frac{Γ, g: σ → τ, x: σ ⊢ M : τ}{Γ ⊢ fix g(x).M : σ → τ}

(Neutral) values:

Ne ∋ U ::= x | U V | fst U | snd U | (case U of inl x_{1} ⇒ V_{1} | inr x_{2} ⇒ V_{2}) | unfold U
Val ∋ V ::= U | λx.V | inl V | inr V | (V_{1}, V_{2}) | fold V | fix g(x).V

Reduction axioms:

(λx.M) N ⟶_{β} [N/x]M
case(inl N) of inl x_{1} ⇒ M_{1} | inr x_{2} ⇒ M_{2} ⟶_{β} [N/x_{1}]M_{1}
case(inr N) of inl x_{1} ⇒ M_{1} | inr x_{2} ⇒ M_{2} ⟶_{β} [N/x_{2}]M_{2}
fst(M_{1}, M_{2}) ⟶_{β} M_{1}
snd(M_{1}, M_{2}) ⟶_{β} M_{2}
unfold(fold M) ⟶_{β} M
(fix g(x).M) N ⟶_{β} [fix g(x).M/g][N/x]M

Reduction relations:

⟶_{β}  β-reduction (only axioms)
⟶  one-step reduction: closure of ⟶_{β} under all term constructors
⟶^{+}  transitive closure of ⟶
⟶^{∗}  reflexive-transitive closure of ⟶
⟶^{∞} ⟶^{∗} or divergence

Table 1. The Core Functional Language Λ_{μ}. relation ⟶^{∗} is obtained by closing the relation ⟶_{β} under all term constructors, reflexivity and transitivity. The proposition M ⟶^{∞} M′ shall denote that either M ⟶^{∗} M′ or M diverges, combining finite and infinite reduction sequences.

Recursive functions can be defined via the general fixed-point combinator fix. Note that fix g(x).M binds the two variables g (which stands for the recursively defined function) and x (which denotes the argument to that function) in M. The fixed-point combinator is the source of non-termination in our language, and in this work we will show a method to restrict its use by typing such that termination is regained.

Some significant subset of a functional language with recursive datatypes can be translated into Λ_{μ}. For example, consider the following Haskell program which sums up all elements in a list of natural numbers.

data Nat = Zero | Succ Nat data ListN = Nil | Cons Nat ListN

sum (Nil) = Zero sum (Cons n l) = sum′ n

where sum′ (Zero) = sum l sum′ (Succ n′) = Succ (sum′ n′)

In Λ_{μ}, the defined datatypes are represented by the type expressions Nat := μX. 1 + X and ListN := μY. 1 + Nat × Y. We simulate the Haskell constructors by the following term abbreviations.

Zero := fold(inl())  : Nat
Succ := λx. fold(inr x)  : Nat → Nat
Nil := fold(inl())  : ListN
Cons := λx.λxs. fold(inr(x, xs)) : Nat → ListN → ListN

What our representation of datatypes loses in succinctness, it gains in conceptual clarity: it separates the notion of sum (+) and product (×) from recursion (μ), which simplifies both the presentation of typing and the interpretation of types (see Section 5).

The Haskell program translates into the following Λ_{μ} code which contains two interleaving uses of fix.

sum : ListN → Nat

sum := fix f(l). case(unfold l) of inl u ⇒ Zero | inr p ⇒ (fix g(n). case(unfold n) of

inl u ⇒ f(snd p)

| inr n′ ⇒ Succ(g n′))
(fst p)

We sketch a syntactical proof of type soundness, also called type safety, following the method of Wright and Felleisen [49] which is explained in detail in Pierce [41].

The type system of Λ_{μ} guarantees that the language is free of junk terms (or faulty terms [49]) such as fst (λx.x) which would cause evaluation to get stuck. By showing that welltypedness is preserved under reduction, we ensure that junk terms never arise during evaluation, and each term M reaches a value V or diverges.

Theorem 1.1 (Type Preservation and Progress). Let Γ ⊢ M : τ be a well-typed term.

(1) Types are preserved under reduction: If M ⟶ M′ then Γ ⊢ M′ : τ.

(2) Evaluation can progress: Either M ∈ Val or M ⟶ M′ for some term M′.

Proof. Both properties can be shown by induction on Γ ⊢ M : τ. Preservation and progress are text-book results, see Pierce’s Exercise 20.2.2 [41]. □

Corollary 1.2 (Strong Type Soundness for Λ_{μ}). If Γ ⊢ M : τ then M ⟶^{∞} V for some value V with Γ ⊢ V : τ.

Proof. By coinduction. At this point, we should put forth a more precise definition of possibly infinite reductions M ⟶^{∞} V. The relation ⟶^{∞} is obtained as the greatest fixed point R of the following rules:

\overline{M R M} refl  \frac{M_{1} ⟶ M_{2}  M_{2} R M_{3}}{M_{1} R M_{3}} step

Note that if we take the least fixed point, we get ⟶^{∗}. Taking the greatest fixed point instead of the least adds infinite reduction sequences.

To prove the corollary, we first apply Theorem 1.1(2) to the assumption Γ ⊢ M : τ. If M is a value, we are done since V ⟶^{∞} V by rule refl. Otherwise, M ⟶ M′ where Γ ⊢ M′ : τ by Theorem 1.1(1). By coinduction hypothesis, M′ ⟶^{∞} V for some value V with Γ ⊢ V : τ. Thus, M ⟶^{∞} V by rule step. The use of the coinduction hypothesis is justified by the fact that we used at least one generating rule of ⟶^{∞} to produce the goal M ⟶^{∞} V after appealing to the coinduction hypothesis. This principle is called the guardedness condition by Coquand [17]. □

Thus, well-typed Λ_{μ} programs cannot go wrong (Milner [36]). But they can diverge, like the totally undefined function fix g(x).g x. In the remainder of the paper, we develop a more restrictive set of typing rules in which only terminating programs are typable.

2. From Mendler Iteration to Size-Preserving Recursion

Starting at Mendler’s formulation of iteration [35], we stepwise motivate our principle of recursion through size-preserving functions inspired by Giménez [23]. We both give a semantical motivation as well as an interesting application: termination verification of quicksort by our type system.

2.1. Iteration à la Mendler

Let L denote the set of lists of natural numbers and L → L denote the set of all total functions from lists to lists. Let f be some (possibly partial) function over lists and n ∈ ℕ arbitrary. Assume we can prove that if f is total for lists of length less than n, then f is total for lists of length less than n + 1. By induction on n, and since there are no lists of length less than 0, if follows that f is total for all lists. More formally, let L_{n} := {l ∈ L : |l| < n} be the nth approximation to the set of all lists L. The proof principle can be expressed via the following natural deduction rule:

[n ∈ ℕ][f ∈ L_{n} → L] ; \begin{matrix}· \\ · \\ · \end{matrix} ; f ∈ L_{n+1} → L ; f ∈ L → L

Mendler [35] first turned this principle into a typing rule for recursive functions which by their typing are bound to terminate. For the case of functions from lists to lists, his rule reads as follows:

\frac{Γ, Y :type, g:Y → ListN, x:1 + Nat × Y ⊢ M : ListN}{Γ ⊢ fix g(x).M : ListN → ListN}

In the assumptions of the premise, the (fresh) type variable Y stands for some approximation L_{n}. The to-be-defined recursive function g is assumed to be element of L_{n} → L. The premise now shows that the function is in L_{n+1} → L. To this end, an argument x : 1 + Nat × Y is assumed; its type denotes L_{n+1} in unfolded form. Under these assumptions, the body M of the recursive function is shown to be well-typed. This implies that within M, recursive calls of g can only happen with arguments of type Y, which can only arise as subterms of x, since Y is a type variable. During evaluation of a function call via the reduction rule

(fix g(x).M) (fold N) ⟶ [fix g(x).M/g][N/x]M,

the type variable Y gets instantiated by ListN, g by the recursive function, and x by the unfolded argument.

A closer look on the general form of Mendler’s rule, given in the following, reveals that it types exactly the iterative programs (cf. Matthes [32], Spławski and Urzyczyn [44]):

\frac{Γ, Y :type, g:Y → τ, x:σ(Y) ⊢ M : τ}{Γ ⊢ fix g(x).M : μXσ → τ}

Above, we used an instance of this rule with μXσ = τ = ListN. Some numbertheoretic functions which have a very natural iterative implementation are addition, multiplication and exponentiation. For instance:

add : Nat → Nat → Nat
add := λy. fix add(x). case x of
inl u ⇒ y
| inr x′ ⇒ Succ(add x′)

The definition is well-typed with the following type assignments to the bound variables: y : Nat, add : Y → Nat, x : 1 + Y, u : 1 and x′ : Y.

From now, since we interpret μXσ as the least fixed-point of the type operator σ(X), and since we allow μXσ only in the domain of total functions, we speak of inductive types instead of recursive types.^{2}

2.2. Primitive Recursion à la Mendler

Mendler also gave a more expressive rule which types all primitive recursive programs [34]. The premise of the recursion rule has an additional hypothesis i : Y → μXσ which can be used to convert a predecessor r : Y of the input x into the inductive type μXσ. After conversion, it can either become part of the output or be used as argument to previously defined functions. During reduction, i gets instantiated with the identity λxx. We achieve the same gain of expressivity by making Y a subtype of μXσ in the iteration rule.

\frac{Γ, Y ≤μXσ, g:Y → τ, x:σ(Y) ⊢ M : τ}{Γ ⊢ fix g(x).M : μXσ → τ} .

The reduction rule remains unchanged—but we need to add subsumption to our typing judgement. The following axiom and rule have to be added.

\frac{(Y ≤μXσ) ∈ Γ}{Γ ⊢ Y ≤ μXσ}  \frac{Γ ⊢ M : ρ  Γ ⊢ ρ ≤ σ}{Γ ⊢ M : σ}

To equip subtyping with the standard properties of transitivity and reflexivity (in our case only for types ρ ≤ μXσ), we add the following axioms:

\frac{(Y ≤μXσ) ∈ Γ}{Γ ⊢ Y ≤ Y}  \overline{Γ ⊢ μXσ ≤ μXσ}

and Urzyczyn [44].

2There is a Curry-Howard-correspondence of—on the programming side—elimination schemes for μXσ and—on the logical side—induction axioms for inhabitants of μXσ, hence the name “inductive types”. For more details on this correspondence, the reader is referred to Spławski

Examples of number-theoretic functions which have a natural primitive recursive implementation are predecessor, subtraction and factorial. For instance,

pred : Nat → Nat
pred := fix pred(x). case x of
inl u ⇒ Zero ; | inr x′ ⇒ x′

with types pred : Y → Nat, x : 1+Y, u : 1 and x′ : Y. Observe that this definition would not have type-checked using the Mendler iteration rule, since we need to make use of subtyping to convert x′ : Y to type Nat.

2.3. Course-of-Value Recursion

In our introductory example, type variable Y denotes some approximation L_{n} of the set of number lists. The next stage of approximation L_{n+1} is only available in its unfolded version σ(Y). To make approximation stages first-class citizens, we follow Giménez [23] and extend our type language by a “next stage” operator (·)^{+}. The cumulative character L_{n} ⊆ L_{n+1} ⊆ L_{n+2} ⊆ ⋯ ⊆ L is reflected by a chain of subtyping relations Y ≤ Y^{+} ≤ Y^{++} ≤ ⋯ ≤ μXσ which can be derived using the additional rules:

\frac{Γ ⊢ ρ ≤ μXσ}{Γ ⊢ ρ^{+} ≤ μXσ} \frac{Γ ⊢ ρ ≤ μXσ}{Γ ⊢ ρ ≤ ρ^{+}} \frac{Γ ⊢ ρ ≤ μXσ}{Γ ⊢ ρ ≤ ρ} \frac{Γ ⊢ ρ ≤ σ  Γ ⊢ σ ≤ τ}{Γ ⊢ ρ ≤ τ}

Folding and unfolding now must be applicable to inhabitants of approximations of inductive types as well. We replace the original rules from Table 1 by

\frac{Γ ⊢ ρ ≤ μXσ  Γ ⊢ M : σ(ρ)}{Γ ⊢ fold M : ρ^{+}}  \frac{Γ ⊢ ρ ≤ μXσ  Γ ⊢ M : ρ^{+}}{Γ ⊢ unfold M : σ(ρ)} .

The original rules can be derived using the new ones plus the fact that subtyping admits (μXσ)^{+} ≤ μXσ. With the new notation for approximation stages the typing rule for recursion reads as follows.

\frac{Γ, Y ≤μXσ, g:Y → τ, x:Y^{+} ⊢ M : τ}{Γ ⊢ fix g(x).M : μXσ → τ} .

Since the argument x of the recursive function is no longer of the unfolded type σ(Y), but inhabits Y^{+}, we need to substitute the full fold N for x during reduction:

(fix g(x).M) (fold N) ⟶ [fix g(x).M/g][fold N/x]M,

Silently, we have turned primitive recursion into course-of-value recursion. This can be seen from the following argument: If we have computed the predecessor r : Y of input x : Y^{+} within the body M of our recursive function, we can apply the subtyping law Y ≤ Y^{+} on the type of r, unfold r, and compute its predecessor in turn. Going on like this, we can analyze x arbitrarily deep to obtain subcomponents which all qualify as arguments to recursive calls of g since they are assigned type Y. Course-of-value recursion is useful, for instance, to program division by two, or to implement the specification of the Fibonacci numbers directly:

fib : Nat → Nat
fib := fix fib(x). case (unfold x) of
inl u ⇒ Zero
| inr y ⇒ case (unfold y) of
inl u ⇒ Succ(Zero)
| inr z ⇒ add (fib y) (fib z)

In this definition, we have the following types for the bound variables: fib : Y → Nat, x : Y^{+}, u : 1, y : Y ≤ Y^{+} and z : Y. Since we can cast the type of y to Y^{+}, we can unfold it again, hence, look deeper into the recursion argument. This is the essence of course-of-value recursion. Note also that in contrast to the fixed-point rules before, the function argument x is not automatically in an unfolded state any more; we need to unfold it manually in order to analyze it.

To be precise, fib is already an instance of the weaker scheme of course-of-value iteration, a notion coined by Uustalu and Vene [47]. We obtain a rule for courseof-value iteration by replacing the hypothesis Y ≤ μXσ by Y_{X.σ} ≤ Y_{X.σ}^{+}. The subscript X.σ to the variable Y expresses that Y is an approximation type of μX.σ, an information that was implicit in the old hypothesis.

2.4. Recursion Via Size-Preserving Functions

Some functions like Euclidean division or functional quicksort have a succinct recursive implementation where the argument r to the recursive call is derived from the input argument x through another function. For example, assume a function pivot a xs which splits the input list xs into two output lists (l, r) where l contains all elements < a and r the remainder. Using pivot, we define qsapp xs ys which quick-sorts list xs and prepends it to ys.

qsapp [ ] ys = ys

qsapp (x :: xs) ys = let (l, r) = pivot x xs in qsapp l (x :: qsapp r ys)

(We use a sugared syntax for Nil and Cons in this example). This function is defined by recursion on its first argument. However, the arguments l and r of the recursive calls are not derived from the input directly, i.e., using only pattern matching. They are connected to xs, a direct subterm of the input, via the function pivot. If we know that both output lists (l, r) of the application pivot x xs are at most as long as the input xs, we can justify that qsapp is defined by course-of-value recursion on the length of its first argument and constitutes a total function. We say (a bit sloppily) that pivot x needs to be a size-preserving function.^{3} In terms of approximations, pivot x is size preserving if for every input xs ∈ L_{n} both output lists l and r are in the same approximation stage L_{n} as the input xs. More formally, we require pivot x ∈ ⋂_{n}(L_{n} → L_{n} × L_{n}). Giménez [23] observed that one can use bounded quantification

3A similar terminology is used by Walther [48] and Pientka [40].

pivot x : ∀Y ≤ListN. Y → Y × Y

to express this semantical property on the syntax level. How can we show a function to be size preserving? Semantically, we can use the following proof by induction (f = pivot x):

\frac{[f ∈ L_{n} → L_{n} × L_{n}] ; ⋮ ; f ∈ L_{n+1} → L_{n+1} × L_{n+1}}{f ∈ ⋂_{n}(L_{n} → L_{n} × L_{n})}

The difference to the proof scheme given in Section 2.1 is that the result type now also mentions approximation stages. We can carry this modification over to the syntactical level by allowing occurrences of Y in the result type τ of recursion. In this article, we restrict to positive occurrences of Y in τ (so do Barthe et al. [9]). As we will see in Section 6, negative occurrences can lead to non-termination. The recursion rule now takes the following shape:

\frac{Γ, Y ≤μXσ, g:Y → τ(Y), x:Y^{+} ⊢ M : τ(Y^{+}) Y pos. in τ(Y)}{Γ ⊢ fix g(x).M : ∀Y ≤μXσ. Y → τ(Y)}

It is crucial to keep the quantifier in the conclusion. If its type were just μXσ → τ(μXσ), we would have lost the information about size relations between the input and the outputs of the recursive function. To use functions defined with this rule, we need a means to instantiate bounded quantification:

\frac{Γ ⊢ ρ ≤ μXσ Γ ⊢ M : ∀Y ≤μXσ. Y → τ(Y)}{Γ ⊢ M : ρ → τ(ρ)}

In Giménez formulation [23], bounded quantification is not part of the type syntax and consequently, instantiation is merged with the fixed-point rule. Size relations can still be used this way, but local recursive functions can then not always be lifted to the top-level to be made available for other functions. For instance, pivot would have to be defined locally within qsapp. Since we have bounded quantification as a first-class citizen, we can even abstract the pivot function out of the qsapp function. We define a function qsapp′ such that qsapp = qsapp′ pivot and assign it the type

qsapp′ : (∀Y ≤ListN. Y → Y × Y) → ∀Y ≤ListN. Y → ListN → ListN.

In the following, we complete the quicksort example and demonstrate that our type system can verify its totality. We give the program in a Haskell-like language with type annotations, which is more readable than a direct representation in the core language. However, there is a simple one-to-one correspondence between type annotations in the clauses below and the typing rule for fix given above: The principal function argument is assumed to have type Y^{+}, recursive calls can only occur with arguments of type Y, and the result must have type τ(Y^{+}).

pivot : Nat → ∀Y ≤ListN. Y → Y × Y

pivot a [ ]^{Y^{+}} = ([ ]^{Y^{+}}, [ ]^{Y^{+}})

pivot a (x :: xs^{Y})^{Y^{+}} = let (l^{Y}, r^{Y}) = pivot a xs in

if x < a then ((x :: l)^{Y^{+}}, r^{Y ≤Y^{+}})
else (l^{Y ≤Y^{+}}, (x :: r)^{Y^{+}})

qsapp : ∀Y ≤ListN. Y → ListN → ListN

qsapp [ ]^{Y^{+}} ys = ys

qsapp (x :: xs^{Y})^{Y^{+}} ys = let (l^{Y}, r^{Y}) = pivot x xs in

qsapp l^{Y} (x :: qsapp r^{Y} ys)

quicksort : ListN → ListN

quicksort l = qsapp l [ ] All annotations in the function bodies can be inferred by the type checking algorithm presented in Section 4, once the types of the functions are given.

3. Type System

In the following we formally enrich the type system of Λ_{μ} by approximation types, subtyping, and bounded quantification, as we explained informally in the last section. This constitutes the language Λ_{μ}^{+}. Due to the restricted fix-rule, it types only strongly normalizing terms of Λ_{μ}.

3.1. Contexts, Types and Subtyping

Table 2 summarizes types and type-related judgements of Λ_{μ}^{+}. The set of raw types is an extension of the types of Λ_{μ} by decorations τ^{+} and bounded quantifications ∀Y ≤μXσ. Y → τ(Y). Additionally to term variables x, wellformed contexts Γ can bind constrained type variables Y ≤ μXσ. As before, all variables bound by Γ are assumed to be distinct. By two judgements, we distinguish two kinds of types:

itype: Datatypes. These are essentially the positive inductive types of Λ_{μ}. Additionally, they may contain type variables Y which are approximations Y ≤ μXσ of an inductive datatype μXσ. For example, in Section 7.1 we will see the type Y list = μX. 1 + Y × X referring to an approximation type Y. Note that the itype-formation rule for σ → τ swaps positivity and negativity of variables in σ.

Raw types:

ρ, σ, τ ::= X | 1 | σ + τ | σ × τ | σ → τ | μXσ | τ^{+} | ∀Y ≤ μXσ. Y → τ(Y)

Judgments:

Γ cxt  Γ is a wellformed context.
Γ; X⃗; X⃗′ ⊢ σ : itype σ is a datatype with free positive variables X⃗ and free negative variables X⃗′.
Γ ⊢ τ : type  τ is a wellformed decorated type.
Γ ⊢ ρ ≤ σ  ρ is a subtype of σ.

Wellformed contexts Γ cxt.

\overline{· cxt}  \frac{Γ ⊢ τ : type}{Γ, x: τ cxt}  \frac{Γ; ·; · ⊢ μXσ : itype}{Γ, Y ≤ μXσ cxt}

Datatypes Γ; X⃗; Y⃗ ⊢ σ : itype.

\frac{Γ cxt (Y ≤ μXσ) ∈ Γ}{Γ; X⃗; X⃗′ ⊢ Y : itype} \frac{Γ cxt}{Γ; X⃗; X⃗′ ⊢ 1 : itype} \frac{Γ; X⃗; X⃗′ ⊢ σ : itype Γ; X⃗; X⃗′ ⊢ τ : itype}{Γ; X⃗; X⃗′ ⊢ σ ⋆ τ : itype} ⋆ ∈ \{+, ×\}

\frac{Γ cxt}{Γ; X⃗; X⃗′ ⊢ X_{i} : itype}  \frac{Γ; X⃗′; X⃗ ⊢ σ : itype  Γ; X⃗; X⃗′ ⊢ τ : itype}{Γ; X⃗; X⃗′ ⊢ σ → τ : itype}  \frac{Γ; X⃗, X; X⃗′ ⊢ σ : itype}{Γ; X⃗; X⃗′ ⊢ μXσ : itype}

Subtyping I: Γ ⊢ ρ ≤ μXσ.

\frac{Γ; ·; · ⊢ μXσ : itype}{Γ ⊢ μXσ ≤ μXσ}  \frac{Γ cxt  (Y ≤ μXσ) ∈ Γ}{Γ ⊢ Y ≤ μXσ}  \frac{Γ ⊢ ρ ≤ μXσ}{Γ ⊢ ρ^{+} ≤ μXσ}

Wellformed types Γ ⊢ τ : type.

\frac{Γ cxt}{Γ ⊢ 1 : type}  \frac{Γ ⊢ σ : type  Γ ⊢ τ : type}{Γ ⊢ σ ⋆ τ : type} ⋆ ∈ \{+, ×, →\}
\frac{Γ ⊢ ρ ≤ μXσ}{Γ ⊢ ρ : type}  \frac{Γ, Y ≤ μXσ ⊢ τ : type}{Γ ⊢ ∀Y ≤ μXσ. τ : type}

Subtyping II: Γ ⊢ ρ ≤ σ.

\frac{(Y ≤ μXσ) ∈ Γ}{Γ ⊢ Y ≤ Y}  \frac{Γ ⊢ μXσ ≤ ρ}{Γ ⊢ μXσ ≤ ρ^{+}}  \frac{Γ ⊢ Y ≤ ρ}{Γ ⊢ Y ≤ ρ^{+}}  \frac{Γ ⊢ τ ≤ ρ}{Γ ⊢ τ^{+} ≤ ρ^{+}}

Table 2. Contexts, Types and Subtyping

type: (Decorated) types. They can contain the standard type formers 1, +, × and →, inductive types μXσ and their approximations ρ—this is handled via the judgement ρ ≤ μXσ—and bounded quantification. All free variables Y for a wellformed type Γ ⊢ τ : type are approximations of datatypes and bound in Γ.

Separation of the types in two classes simplifies the theory: First, we do not need to define positivity for bounded quantification. Secondly, it brings some stratification that simplifies the semantics given in Section 5. For instance, monotonicity is only required of itypes.

Subtyping of the form ρ ≤ μXσ (I) determines ρ to be an approximation of the inductive type μXσ. Setting ρ^{0} := ρ and ρ^{i+1} = (ρ^{i})^{+}, the approximations can only take the shape Y^{i} or (μXσ)^{i} for some natural number i. We observe that

∃σ. Γ ⊢ ρ ≤ μXσ

is decidable for all Γ and ρ. This entails that the other four judgements are also decidable (only the rule for wellformed approximations ρ is critical). Furthermore, if ρ ≤ μXσ and ρ ≤ μXσ′ then σ = σ′.

There is another set of subtyping rules ρ ≤ σ (II) for the cases where the right hand side σ is an approximation of the shape Y or ρ^{+}. These rules are never invoked by the type-judgement, but by the subsumption rule (see below). The presentation of subtyping differs from the one in the previous section, but the same types are related. The formulation now is syntax-directed; transitivity and reflexivity for approximations ρ ≤ μXσ are admissible.

The judgements have a number of technical properties. Wellformedness of the context is a byproduct of the wellformedness of a type or a subtyping relation between two types in the given context:

Lemma 3.1 (Wellformedness of contexts). If either Γ; X⃗; X⃗′ ⊢ σ : itype or Γ ⊢ τ : type or Γ ⊢ ρ ≤ σ then Γ cxt.

Proof. Simultaneously by induction on the derivation. □

All judgements allow weakening with wellformed contexts and substitution of approximation variables Y by the full inductive type μXσ:

Lemma 3.2 (Type Substitution). Let Γ ⊢ ρ ≤ μXσ. Then (1) If Γ, Y ≤μXσ, Γ′ cxt then Γ, [ρ/Y]Γ′ cxt.

(2) If Γ, Y ≤μXσ, Γ′; X⃗; X⃗′ ⊢ τ : itype then Γ, [ρ/Y]Γ′; X⃗; X⃗′ ⊢ [ρ/Y]τ : itype.

(3) If Γ, Y ≤μXσ, Γ′ ⊢ τ : type then Γ, [ρ/Y]Γ′ ⊢ [ρ/Y]τ : type.
(4) If Γ, Y ≤μXσ, Γ′ ⊢ τ_{1} ≤ τ_{2} then Γ, [ρ/Y]Γ′ ⊢ [ρ/Y]τ_{1} ≤ [ρ/Y]τ_{2}.

Proof. By simultaneous induction over the derivation. □

3.2. Terms and Type Assignment

Λ_{μ}^{+} features the same terms as Λ_{μ}, but comes with a more precise typing of inductive data (fold, unfold) and recursive functions (fix). Furthermore there are typing rules which arise from subtyping and quantification. Table 3 summarizes the changes to Λ_{μ} which have been introduced in Section 2 already. Due to the richer type grammar, not every context is automatically wellformed and we have to add the judgement Γ cxt to the two axioms of typing, var and unit. Similarly, not every type is wellformed, so we also have to refine the injection rules for sums.

Typing axioms:

\frac{Γ cxt x: τ ∈ Γ}{Γ ⊢ x : τ} var \frac{Γ cxt}{Γ ⊢ () : 1} unit

Sum types:

\frac{Γ ⊢ M : σ Γ ⊢ τ : type}{Γ ⊢ inl M : σ + τ} inl \frac{Γ ⊢ σ : type Γ ⊢ M : τ}{Γ ⊢ inr M : σ + τ} inr

Inductive types:

\frac{Γ ⊢ ρ ≤ μX.σ(X)  Γ ⊢ M : σ(ρ)}{Γ ⊢ fold M : ρ^{+}} fold  \frac{Γ ⊢ ρ ≤ μX.σ(X)  Γ ⊢ M : ρ^{+}}{Γ ⊢ unfold M : σ(ρ)} unfold

Recursive functions:

\frac{Γ, Y ≤ μXσ, g: Y → τ(Y), x: Y^{+} ⊢ M : τ(Y^{+})  Y pos. in τ}{Γ ⊢ fix g(x).M : ∀Y ≤ μXσ. Y → τ(Y)} fix

Subtyping:

\frac{Γ ⊢ ρ ≤ σ  Γ ⊢ M : ρ}{Γ ⊢ M : σ} sub  \frac{Γ ⊢ ρ ≤ μXσ  Γ ⊢ M : ∀Y ≤ μXσ. τ(Y)}{Γ ⊢ M : τ(ρ)} inst

Neutral values:

Ne ∋ U ::= … | (fix g(x).V) U

Reduction axiom:

(fix g(x).M) (fold N) ⟶_{β} [fix g(x).M/g][fold N/x]M

Table 3. Typing and Reduction Rules for Λ_{μ}^{+}.

The new typing rules for inductive data now also treat inhabitants of approximations of inductive types. Let us explain the fold-rule for the example of lists: Let Y ≤ ListN = μX. 1 + Nat × X be an approximation of the type of lists over natural numbers and x : Nat a natural number. Let y : Y a list in this approximation, i.e., a list with size < n for an unknown n. Then inr(x, y) : 1 + Nat × Y, hence, by the folding rule, the list Cons(x, y) = fold(inr(x, y)) : Y^{+} is of size < n + 1. The unfold-rule works analogously. As mentioned in Section 2, the old folding rules (of Λ_{μ}) are a special case of the new ones: set ρ = μXσ.

The reduction axioms of Λ_{μ}^{+} are the same as for Λ_{μ} with the exception of fixed-point unrolling. To ensure normalization, recursive functions fix g(x).M are now only reduced if applied to a value fold N of an inductive type. Consequently, we get a new neutral value (fix g(x).V) U for a value U which is not of the form fold V. The one-step reduction relation ⟶ and multi-step reductions ⟶^{+}, ⟶^{∗} and ⟶^{∞} are to be understood with regard to the modified axiom.

Example 3.3 (Empty Type). The empty type is definable as the least fixed-point of the identity function on the type level.

0  := μX.X
abort := fix g(x).g(unfold x) : 0 → τ

Its elimination function abort is accepted by the type system in the above form and is indeed no threat to strong normalization. Why this holds will be informally explained by the following failed counterexample. It is formally established in Section 5. Assume a free variable y : μX.X. Then we have fold y : μX.X and the following reduction sequence.

abort (fold y) = (fix g(x).g(unfold x)) (fold y)
⟶ (fix g(x).g(unfold x)) (unfold(fold y))
⟶ (fix g(x).g(unfold x)) y
= abort y

We observe that the present definition of abort in Λ_{μ}^{+} does not produce loops, in contrast to the function fix g(x).g x which would be the simplest definition of abort in Λ_{μ}.

The typing calculus enjoys the usual properties of wellformedness, restricted exchange, weakening, strengthening and substitution for term variables x. Substitution also holds for type variables Y:

Lemma 3.4 (Type Substitution). If Γ, Y ≤ μXσ, Γ′ ⊢ M : τ and Γ ⊢ ρ ≤ μXσ then Γ, [ρ/Y]Γ′ ⊢ M : [ρ/Y]τ.

Proof. By induction of the typing derivation and case distinction on the subtyping derivation. □

Important for the soundness of typing is the fact that all contexts and types appearing in the typing judgement are wellformed:

Lemma 3.5. If Γ ⊢ M : τ then Γ cxt and Γ ⊢ τ : type.

Proof. By induction on the typing derivation. □

Example 3.6 (Tree Ordinals). The second number class can be represented as the strictly positive inductive type Ord = μX. 1 + (X + (Nat → X)) with three constructors.

OZero := fold(inl())  : Ord  zero ordinal
OSucc := λa. fold(inr(inl a)) : Ord → Ord  successor ordinal
OLim := λf. fold(inr(inr f)) : (Nat → Ord) → Ord limit ordinal

Example 3.7 (Representation of ω). Assuming toOrd : Nat → Ord is defined as the function which converts a natural number Succ^{n}(Zero) into its ordinal equivalent OSucc^{n}(OZero) we obtain a representation of the least infinite ordinal ω as omega = OLim toOrd.

Example 3.8 (Addition of Tree Ordinals). In Λ_{μ}^{+}, ordinal addition can be defined as follows:

oadd : Ord → ∀Y ≤Ord. Y → Ord
oadd := λx. fix oadd(y). case(unfold y) of
inl u ⇒ x
| inr y′ ⇒ case y′ of
inl a ⇒ OSucc(oadd a)
| inr f ⇒ OLim(λn. oadd (f n))

During type checking, the bound variables receive the following types: x : Ord, oadd : Y → Ord, y : Y^{+}, u : 1, y′ : Y + (Nat → Y), a : Y, f : Nat → Y and n : Nat. Also, the positivity condition on the result type Ord of recursion is trivially satisfied, since Y is not mentioned in Ord.

Datatypes with embedded function spaces, like in Example 3.6, are explicitely excluded in the work on size types by Hughes, Pareto and Sabry [28]. The reason is that in their their approach, size annotations are interpreted as ordinals ≤ ω. But Example 3.7 needs larger ordinals, as explained in Section 5.

Translation contexts Δ tcxt.

\overline{· tcxt}  \frac{Δ tcxt  ·; ·; · ⊢ μXσ : itype}{Δ, Y ≤ μXσ tcxt} Y ∉ Δ

Approximation erasure in types Δ ⊢ τ ||⟩ τ′.

\overline{Δ ⊢ 1 ||⟩ 1} \frac{X ∉ Δ}{Δ ⊢ X ||⟩ X} \frac{Δ ⊢ σ ||⟩ σ′}{Δ ⊢ μXσ ||⟩ μXσ} \frac{Δ ⊢ ρ ||⟩ ρ′ Δ ⊢ σ ||⟩ σ′}{Δ ⊢ ρ ⋆ σ ||⟩ ρ′ ⋆ σ′} ⋆ ∈ \{+, ×, →\}

\frac{Δ ⊢ ρ ≤ μXσ}{Δ ⊢ ρ ||⟩ μXσ}  \frac{Δ ⊢ σ ||⟩ σ′  Δ, Y ≤ μXσ′ ⊢ τ ||⟩ τ′}{Δ ⊢ ∀Y ≤ μXσ.τ ||⟩ τ′}

Approximation erasure in contexts Γ ||⟩ Γ′; Δ.

\overline{· ||⟩ ·; ·}  \frac{Γ ||⟩ Γ′; Δ  Δ ⊢ τ ||⟩ τ′}{Γ, x: τ ||⟩ Γ′, x: τ′; Δ}  \frac{Γ ||⟩ Γ′; Δ  Δ ⊢ σ ||⟩ σ′}{Γ, Y ≤ μXσ ||⟩ Γ′; Δ, Y ≤ μXσ′}

Table 4. Erasure of Approximation Types.

3.3. Weak Type Soundness of Λ_{μ}^{+}

In this section, we show that in the extended system Λ_{μ}^{+}, programs still cannot go wrong. Unfortunately, the type preservation property fails for the new type system, since our notion of subtyping is too weak. Consider the following typing derivation:

{M : σ(ρ_{1}) \atop fold M : ρ_{1}^{+}}  {ρ_{1} ≤ ρ_{2} \atop ρ_{1}^{+} ≤ ρ_{2}^{+}}
fold M : ρ_{2}^{+}
unfold(fold M) : σ(ρ_{2})

Since unfold(fold M) ⟶_{β} M, type preservation requires that M : σ(ρ_{2}). However, our syntactic subtyping lacks the necessary property σ(ρ_{1}) ≤ σ(ρ_{2}) for arbitrary ρ_{1} ≤ ρ_{2} and σ(X) in which X appears only positively^{4}. One way to overcome the problem would be to add the necessary closure properties to the subtyping relation, as we have done in other work [3]. Instead, we make use of the fact that we have the simpler type system Λ_{μ} which already ensures that well-typed programs cannot go wrong. We show that each typing derivation of Λ_{μ} can be turned into a typing derivation of Λ_{μ}^{+} by replacing approximation types by the full inductive types. Since the progress property—Theorem 1.1(2)—also holds for the slightly restricted reduction relation and the slightly enlarged value set of Λ_{μ}^{+}, type soundness of Λ_{μ} ensures that Λ_{μ}^{+} programs cannot get stuck as well.

Table 4 specifies how to erase approximations in both types and contexts. The judgement Δ tcxt singles out such contexts Δ—called translation contexts—which map approximation type variables Y into closed approximation-free inductive types μXσ. Given an approximation context Δ and a Λ_{μ}^{+}-type τ with Δ ⊢ τ : type, judgement Δ ⊢ τ ||⟩ τ′ outputs a wellformed Λ_{μ}-type τ′ in which all approximation types ρ ≤ μXσ have been replaced by the full inductive type μXσ. Similarly, Γ ||⟩ Γ′; Δ separates a wellformed Λ_{μ}^{+}-context Γ cxt into a approximation-free Λ_{μ}-context Γ′ and a translation context Δ tcxt.

Theorem 3.9 (Soundness of Λ_{μ}^{+}-typing with regard to Λ_{μ}-typing). If Γ ⊢ M : τ in Λ_{μ}^{+}, Γ ||⟩ Γ′; Δ and Δ ⊢ τ ||⟩ τ′, then Γ′ ⊢ M : τ′ in Λ_{μ}.

Proof. By induction on Γ ⊢ M : τ. The proof amounts to removing all applications of subsumption and instantiation from the Λ_{μ}^{+} typing derivation. □

Corollary 3.10 (Weak Type Soundness for Λ_{μ}^{+}). If Γ ⊢ M : τ in Λ_{μ}^{+}, then M ⟶^{∞} V.

Proof. By combining the last theorem with Corollary 1.2. □

Since we are lacking type preservation in Λ_{μ}^{+}, we cannot show Γ ⊢ V : τ and therefore only obtain the weak type soundness property. This is enough for our purposes; in Section 5 we show that infinite reduction sequences are excluded by the advanced type system—with the result that each well-typed term reduces to a value in Λ_{μ}^{+}.

4Semantically, this property does hold and is the content of Lemma 5.5.

TITLE WILL BE SET BY THE PUBLISHER 19

Terms.

L_{μ}^{+} ∋ M, N ::= ⋯ | λx: σ.M | (M: τ) | let x = N in M

Judgments.

Γ ⊢ τ ◁ τ′  Extended subtyping.
Γ ⊢ M ↓ τ  The type of term M is inferred as τ.
Γ ⊢ M ⇑ τ  Term M is checked against type τ.

Type inference.

\frac{x: τ ∈ Γ}{Γ ⊢ x ↓ τ} ↓var  \frac{Γ ⊢ σ : type  Γ, x: σ ⊢ M ↓ τ}{Γ ⊢ λx: σ.M ↓ σ → τ} ↓lam  \frac{Γ ⊢ M ↓ σ → τ  Γ ⊢ N ⇑ σ}{Γ ⊢ M N ↓ τ} ↓app
\overline{Γ ⊢ () ↓ 1} ↓unit  \frac{Γ ⊢ M ↓ σ  Γ ⊢ N ↓ τ}{Γ ⊢ (M, N) ↓ σ × τ} ↓pair  \frac{Γ ⊢ M ↓ σ × τ}{Γ ⊢ fst M ↓ σ} ↓ fst  \frac{Γ ⊢ M ↓ σ × τ}{Γ ⊢ snd M ↓ τ} ↓ snd
\frac{Γ ⊢ M ↓ ρ^{+}  Γ ⊢ ρ ≤ μX.σ(X)}{Γ ⊢ unfold M ↓ σ(ρ)} ↓ unfold^{+}  \frac{Γ ⊢ M ↓ ρ  Γ ⊢ ρ ≤ μX.σ(X)}{Γ ⊢ unfold M ↓ σ(ρ)} ↓ unfold
\frac{Γ ⊢ τ : type  Γ ⊢ M ⇑ τ}{Γ ⊢ (M: τ) ↓ τ} ↓ann \frac{Γ ⊢ M ↓ ∀Y ≤ μXσ. Y → τ  Y ∉ FV(τ)  Γ ⊢ N ⇑ μXσ}{Γ ⊢ M N ↓ τ} ↓appμ1
\frac{Γ ⊢ M ↓ ∀Y ≤ μXσ. Y → τ(Y)  Γ ⊢ N ↓ ρ  Γ ⊢ ρ ≤ μXσ}{Γ ⊢ M N ↓ τ(ρ)} ↓appμ2

Type checking.

\frac{Γ, x: σ ⊢ M ⇑ τ}{Γ ⊢ λx.M ⇑ σ → τ} ⇑lam  \frac{Γ ⊢ M ⇑ σ}{Γ ⊢ inl M ⇑ σ + τ} ⇑ inl  \frac{Γ ⊢ M ⇑ τ}{Γ ⊢ inr M ⇑ σ + τ} ⇑ inr
\frac{Γ ⊢ N ↓ σ_{1} + σ_{2}  Γ, x_{i}: σ_{i} ⊢ M_{i} ⇑ ρ}{Γ ⊢ case N of inl x_{1} ⇒ M_{1} | inr x_{2} ⇒ M_{2} ⇑ ρ} ⇑ case  \frac{Γ ⊢ N ↓ σ  Γ, x: σ ⊢ M ⇑ τ}{Γ ⊢ let x = N in M ⇑ τ} ⇑ let

\frac{Γ ⊢ ρ ≤ μX.σ(X) Γ ⊢ M ⇑ σ(ρ)}{Γ ⊢ fold M ⇑ ρ^{+}} ⇑ fold \frac{Γ ⊢ M ⇑ σ(μX.σ(X))}{Γ ⊢ fold M ⇑ μX.σ(X)} ⇑ foldμ

\frac{Γ ⊢ M ⇑ σ Γ ⊢ N ⇑ τ}{Γ ⊢ (M, N) ⇑ σ × τ} ⇑pair  \frac{Γ, Y ≤ μXσ, g: Y → τ, x: Y^{+} ⊢ M ⇑ τ}{Γ ⊢ fix g(x).M ⇑ μXσ → τ} ⇑ fix^{−}
\frac{Γ, Y ≤ μXσ, g: Y → τ(Y), x: Y^{+} ⊢ M ⇑ τ(Y^{+})  Y pos. in τ(Y)}{Γ ⊢ fix g(x).M ⇑ ∀Y ≤ μXσ. Y → τ(Y)} ⇑ fix

\frac{Γ ⊢ M ↓ ∀Y ≤ μXσ. Y → τ(Y) match τ′ with τ(Y) ⟹ Y = ρ Γ ⊢ ρ ≤ μXσ Γ ⊢ N ⇑ ρ}{Γ ⊢ M N ⇑ τ′} ⇑appμ

\frac{Γ ⊢ M ↓ σ → τ Γ ⊢ τ ◁ τ′ Γ ⊢ N ⇑ σ}{Γ ⊢ M N ⇑ τ′} ⇑app

Direction reversal.

\frac{Γ ⊢ M ↓ τ  Γ ⊢ τ ◁ τ′}{Γ ⊢ M ⇑ τ′} ⇑↓

Extended subtyping.

\overline{Γ ⊢ τ ◁ τ} ◁refl  \frac{Γ ⊢ ρ ≤ σ}{Γ ⊢ ρ ◁ σ} ◁≤  \frac{Γ ⊢ ρ ≤ μXσ}{Γ ⊢ ∀Y ≤ μXσ. Y → τ(Y) ◁ ρ → τ(ρ)} ◁inst

Table 5. Type Checking.

4. Type Checking

In order to use our type system as a termination checker, we need a suitable type checking algorithm. One possibility would be to extend the Hindley-Milner algorithm to bounded quantification and approximation types. This algorithm would produce a set of existential type variables together with a set of equations these variables have to satisfy. The problem with such an algorithm (as implemented in SML 1997, for instance) is that in case of unsolvable equations, the location “responsible” (from a human perspective) for the type error is hard to locate.^{5}

Pierce and Turner [42] advocate local type inference, which restricts propagation of type information to adjacent nodes of the syntax tree of the term which is to be type-checked—in contrast to Hindley-Milner which collects type equations globally. Local type inference is based on bidirectional type checking, a folklore method which is for instance used by Coquand [18] for dependent types and Davies and Pfenning [20] for intersection types. Recently, Dunfield and Pfenning [21] have extended this method to tridirectional checking.

Bidirectional type checking is incomplete, it can decide typing only for some terms—in the case of the simply-typed lambda-calculus, it is exactly the normal terms. Non-normal terms need type annotations to type-check. Hence, we extend our calculus Λ_{μ}^{+} by some means to aid the type-checker and obtain the language L_{μ}^{+}. The new constructs allow annotation of bound variables λx : σ. M and of whole terms (M : τ). Additionally, we introduce let-binding let x = N in M which has the same operational meaning as (λx.M) N, but better behavior w.r.t. type checking.

We adapt bidirectional type checking to our calculus Λ_{μ}^{+}, the rules are listed in Table 5. The checking judgement Γ ⊢ M ⇑ τ requires all of Γ, M and τ as input and its generating rules are to be read upwards as the arrow suggests. It is defined simultaneously with type inference Γ ⊢ M ↓ τ, which computes the type τ from given Γ and M—the rules for inference should be read downwards.

The general principle of bidirectional checking is that the type of variables and eliminations can be inferred: rules ↓var, ↓ fst, ↓ snd, ↓ unfold, ↓app and ↓appμ1. In contrast, the type of introductions must be checked against: rules ⇑lam, ⇑pair, ⇑ fold, ⇑ inl, ⇑ inr, ⇑ fix^{−} and ⇑ fix (annotated lambda-abstractions λx:σ.M are an exception and admit inference by rule ↓lam). The rule ⇑↓ allows one to switch from checking mode into inference mode and should be applied if no other checking rule matches. In this case, the infered type τ must be more general than the type τ′ supplied to the checking judgement. This is expressed be the extended subtyping relation τ ◁ τ′, which encompasses subtyping and instantiation. Hence, the nondeterministic character of subsumption in the typing judgement is tamed in the type checking algorithm by shifting applications of the subsumption rule to the specific point where inference and checking meet.

5Recently, type inference algorithms which give better error messages have been put forward by Haack and Wells [24] and Yang, Michaelson and Trinder [51].

A positive abnormality to the introduction/elimination dichotomy are tuples: They permit inference although they are constructors (↓unit, ↓pair). One of the negative abnormalities is sum-elimination: The type of the side clauses in the case-construct is arbitrary, and cannot be inferred in general (⇑ case). Let-binding (⇑ let) can be seen as elimination of a unary sum and is therefore treated like case. Another problem occurs with bounded quantification: In the rule ↓appμ2, the size ρ of the argument needs to be inferred to give a size-bound τ(ρ) on the result of the application. If the size of the result is known, it can be checked (rule ⇑appμ). This rule involves simple matching on the level of types: τ′ = τ(ρ) for some unknown ρ. However, since types are first-order expressions without reduction, the matching problem is decidable.

Disregarding the abnormalities, the algorithm can check the types of most normal expressions, which is the kind of expressions that dominates in practical programming. Non-normal expressions need to be annotated with their type at some sensible position (rules ↓ann and ↓lam). All top-level expressions and all recursive functions, need to be defined with their type. This is not too heavy a load for the programmer; in Haskell it is quite common.

Example 4.1 (Type-Checkable Version of sum Example). To make the function sum from Section 1 acceptable by the type checker we need to introduce one annotation. Using the let construct, we can write it as follows in L_{μ}^{+}:

sum : ListN → Nat
sum := fix f(l). case (unfold l) of
inl u ⇒ Zero
| inr p ⇒ let sum′ = (fix g(n). case (unfold n) of
inl u ⇒ f (snd p)
| inr n′ ⇒ Succ(g n′))
: Nat → Nat

in sum′(fst p)

The rules have been implemented in the higher-order logical framework Twelf [39] to yield a prototypical type checker which is available on the homepage of the author [4]. It is easy to turn the rules into a deterministic algorithm, namely into two mutually recursive functions inf and chk with the following specification.

inf (Γ, M)  = \{ \begin{matrix}τ & if Γ ⊢ M ↓ τ \\ error & otherwise \end{matrix}

chk (Γ, M, τ) = \{ \begin{matrix}ok & if Γ ⊢ M ⇑ τ \\ error & otherwise \end{matrix}

Function inf is defined by case distinction on M and function chk by cases on both M and τ. The tests and recursive calls necessary in each case can be read off the rules in Table 5. In some cases several rules seem applicable. This source of non-determinism can be resolved by fusing the respective rules into a single one:

(1) Case inf (Γ, unfold M), rules ↓ unfold^{+} and ↓ unfold: After inferring the type ρ of M, distinguish whether ρ is of shape ρ^{+} or not.

(2) Case inf (Γ, M N), rules ↓app, ↓appμ1 and ↓appμ2: Distinguish on the infered type of M.

(3) Case chk (Γ, M N, τ′), rules ⇑appμ and ⇑app: similarly.

(4) Case chk (Γ, M, τ′), rule ⇑↓: Switch to inference only if no checking rule

is applicable. The resulting function chk(Γ, M, τ) checks types in time linear in the size of the input expression M plus type τ (modulo context lookup, type matching and subtype checking).

Table 6 shows a trace of the type checker as it verifies the welltypedness of the ordinal addition function oadd. The first column displays which rules have fired, the second column lists the hypotheses which the rules have added to the context and the third column show the new state of the checker. To simplify presentation we have ignored the inl branches of the case expressions in this trace.

The algorithm is not complete, but it can check many interesting programs, for instance, all examples of this article. In the following we show soundness of the algorithm.

Definition 4.2 (Erasure). Let |M| ∈ Λ_{μ}^{+} denote the result of erasing all type annotations and let-bindings from M ∈ L_{μ}^{+}. We define | · | by

|λx:σ.M|  = λx.|M|,
|(M:τ)|  = |M|, and
|let x=N in M| = (λx.|M|) |N|,

adding congruences for all other term constructors.

Proposition 4.3 (Soundness of Type Checking). Let Γ be a wellformed context, M a term of L_{μ}^{+} and τ a type.

(1) If Γ ⊢ M ↓ τ, then Γ ⊢ τ : type and Γ ⊢ |M| : τ.
(2) If Γ ⊢ M ⇑ τ and Γ ⊢ τ : type, then Γ ⊢ |M| : τ.

Proof. Simultaneously by induction on Γ ⊢ M ↓⇑ τ. For example:

Case

\frac{Γ ⊢ M ↓ ρ  Γ ⊢ ρ ≤ μX.σ(X)}{Γ ⊢ unfold M ↓ σ(ρ)} ↓ unfold
Γ ⊢ M : ρ  by induction hypothesis
Γ ⊢ ρ ≤ ρ^{+}  from assumption by subtyping
Γ ⊢ M : ρ^{+}  by subsumption rule
Γ ⊢ unfold M : σ(ρ)  by unfolding rule

Case

\frac{Γ ⊢ M ↓ ∀Y ≤μXσ. Y → τ  Y ∉ FV(τ)  Γ ⊢ N ⇑ μXσ}{Γ ⊢ M N ↓ τ} ↓appμ1

oadd : Ord → ∀Y ≤Ord. Y → Ord
oadd := λx. fix oadd(y). case(unfold y) of
inl u ⇒ x
| inr y′ ⇒ case y′ of
inl a ⇒ OSucc(oadd a)
| inr f ⇒ OLim(λn. oadd (f n))

Γ_{0} := OZero:Ord, OSucc:Ord → Ord, OLim:(Nat → Ord) → Ord

Rule  Context ext.  Judgement
start  Γ_{0}  λx. fix … ⇑ Ord → ∀Y ≤Ord. Y → Ord
⇑lam  x : Ord  fix oadd(y) … ⇑ ∀Y ≤Ord. Y → Ord
⇑ fix  Y ≤ Ord
oadd : Y →Ord
y : Y^{+}  case(unfold y) … ⇑ Ord
↓var  y ↓ Y^{+}
↓ unfold  unfold y ↓ 1 + (Y + (Nat → Y))
⇑ case y′:Y + (Nat→Y)  case y′ … ⇑ Ord
↓var  y′ ↓ Y + (Nat → Y)
⇑ case f : Nat→Y  OLim(λn …) ⇑ Ord
⇑↓, ↓var  OLim ↓ (Nat → Ord) → Ord
↓app  λn. oadd … ⇑ Nat → Ord
⇑lam n : Nat oadd (f n) ⇑ Ord
⇑↓, ↓var  oadd ↓ Y → Ord
↓app  f n ⇑ Y
⇑↓, ↓var  f ↓ Nat → Y
↓app  n ⇑ Nat
⇑↓, ↓var  n ↓ Nat

Table 6. Example Run of Type Checker.

Γ ⊢ M : ∀Y ≤μXσ. Y → τ by induction hypothesis
Γ ⊢ M : μXσ → τ  by instantiation
Γ ⊢ μXσ → τ : type  by Lemma 3.5
Γ ⊢ N : μXσ  by induction hypothesis
Γ ⊢ M N : τ  by application rule

The other cases are similarly straightforward. □

Most of the soundness proof has been formally verified in Twelf and can be obtained from the author [4]. For the remainder of this article, we forget about the additional constructs in L_{μ}^{+} and return to our core calculus Λ_{μ}^{+}.

5. Strong Normalization

In this section, we present a semantical soundness proof for Λ_{μ}^{+}. More precisely, we assign to each wellformed type τ a set [[τ]] of strongly normalizing terms such that each term M which can be assigned type τ inhabits [[τ]]. The consequence is that such M are strongly normalizing, which in combination with the weak type soundness result of Section 3.3 guarantees that they reduce to values V in a finite number of steps.

Proofs of strong normalization have a long tradition and several methods have been developed. We use the saturated sets method based on the notion of weak head reduction as found e.g. in Luo [31] and Altenkirch [6].

5.1. Preliminaries: Saturated Sets

The set of strongly normalizing terms SN ⊆ Λ_{μ}^{+} is defined inductively by the following rule:

\frac{∀M′ ∈ Λ_{μ}^{+}. M ⟶ M′ ⇒ M′ ∈ SN}{M ∈ SN}

In other words, SN is the wellfounded part of the set of terms w. r. t. the reduction relation ⟶. All variables x are strongly normalizing as well as all subterms of strongly normalizing terms. The set SN is closed under reduction.

The notion of weak head reduction can be elegantly defined with evaluation contexts E[•], which are generated by the following grammar:

E[•] ::= • | E[•] M | fst E[•] | snd E[•]
| (case E[•] of inl x_{1} ⇒ M_{1} | inr x_{2} ⇒ M_{2})
| unfold E[•] | (fix g(x).M) E[•]

Weak head reduction is reduction of the form E[M_{0}] ⟶ E[M_{1}] where M_{0} ⟶_{β} M_{1}. In this situation, we say that E[M_{0}] has a head redex M_{0}. Terms of the form E[x] are called neutral, they possess no head redex and produce no head redex if substituted for some variable into some term. In the process of normalization, weak head redexes E[M_{0}] must be resolved, there is no way of skipping them by performing other reductions first. This is expressed by the following standardization lemma (Altenkirch [6]).

Lemma 5.1 (Weak Standardization). If M_{0} ⟶_{β} M_{1} and E[M_{0}] ⟶ N, then either N = E[M_{1}] or N = E′[M′_{0}] for some E′[•], M′_{0} and there exists an M′_{1} such that M′_{0} ⟶_{β} M′_{1} and E[M_{1}] ⟶^{∗} E′[M′_{1}].

Proof. By induction on the generation on E[•], and in the base case E[•] = • by case distinction on M_{0} ⟶ N. □

A consequence of weak standardization is that the set SN is closed under weak head expansion.

Lemma 5.2 (Weak Head Expansion). If E[M_{1}] ∈ SN then for all M_{0} ∈ SN with M_{0} ⟶_{β} M_{1} it holds that E[M_{0}] ∈ SN.

Proof. By simultaneous induction on E[•], M_{0} ∈ SN we show N ∈ SN for all N with E[M_{0}] ⟶ N, using Lemma 5.1. □

A set of terms P ⊆ Λ_{μ}^{+} is called saturated, written P ∈ SAT , if it contains only strongly normalizing terms, all strongly normalizing neutral terms, and if it is closed under weak head expansion. The saturation of a set P is defined as the closure under the following rules:

\frac{M ∈ P}{M ∈ P^{∗}}  \frac{E[x] ∈ SN}{E[x] ∈ P^{∗}}  \frac{M ∈ SN  M ⟶_{β} M′  E[M′] ∈ P^{∗}}{E[M] ∈ P^{∗}}

For sets of terms P, Q we define the function space

P → Q := {M ∈ SN : ∀N ∈ P. M N ∈ Q}.

In the following we reuse the well-known and easily verified fact that the function space constructor → operates on saturated sets, i.e., for P, Q ∈ SAT also P → Q ∈ SAT .

5.2. Type Interpretation

In this section, we give an interpretation [[τ]] for every wellformed type τ. For datatypes σ, the semantics [[σ]] is a monotone operator on saturated sets. In particular, [[μX.σ]] is the fixpoint of an operator derived from [[σ]]. In previous work [5], we obtained this fixpoint by the theorem of Knaster and Tarski, resp. by accessibility inductive definitions. This time we follow an idea of Mendler [35] (reused by Amadio and Coupet-Grimal [7]) and reach the fixpoint by transfinite iteration. This technique enables us to give an interpretation to approximation types ρ ≤ μX.σ.

Let O be some set which we call origin set and Φ a monotonic operator on sets. For an ordinal number α we define the α-iterate Φ^{α} by transfinite recursion on α:

Φ^{0} = O
Φ^{α+1} = Φ(Φ^{α})
Φ^{λ} = ⋃_{α<λ} Φ^{α}  for λ limit ordinal

If O ⊆ Φ(O), then the hierarchy (Φ^{α}) is cumulative, that is, Φ^{α} ⊆ Φ^{β} for all α < β. A cumulative hierarchy, which is also called a chain, will become stationary at some point in the iteration process, i.e., it reaches a fixed-point. Since we consider sets over a countable domain, the fixed-point will be reached latest at the least uncountable ordinal Ω and we have

Φ(Φ^{Ω}) = Φ^{Ω} = ⋃_{α<Ω} Φ^{α}.

If O is least in the considered collection of sets, then Φ^{Ω} is guaranteed to be the least fixed point. In the following, we consider operators on saturated sets and fix O = ∅^{∗} to be the least saturated set, namely the saturation of the empty set.

In order to define the interpretation [[τ]] of type τ we need a valuation θ for the free type variables occurring in τ. Since we later also interpret terms which have free term variables, we introduce valuations θ : Γ which provide a substitute for all variables bound in context Γ by the following rules:

\overline{· : ·}  \frac{θ : Γ  M ∈ Λ_{μ}^{+}}{(θ, x↦M) : (Γ, x:τ)}  \frac{θ : Γ  P ⊆ Λ_{μ}^{+}}{(θ, Y ↦P) : (Γ, Y ≤μXσ)}

For context triples, θ : (Γ; X⃗; X⃗′) holds if θ additionally provides a set of terms Q for each variable in X⃗, X⃗′.

Note that θ : Γ only expresses that dom(θ) = dom(Γ) and that each term variable is mapped to a term and each type variable to a set of terms. We do not require that the assigned terms are type-correct nor are there any conditions on the assigned term sets. We do not even require Γ to be a well-formed context. Still, this notion of valuation is sufficient to define a type interpretation and prove monotonicity of this interpretation for all itypes, which are positive by definition. In the next section, we will sharpen our requirements on valuations by an additional judgement θ ∈ [[Γ]].

Now to the semantics of types: Let τ be a type with free type variables in Δ = (Γ; X⃗; X⃗′) and θ : Δ. We define the interpretation [[τ]]θ by recursion on τ:

[[Z]]θ = θ(Z)
[[1]]θ = {()}^{∗}
[[σ + τ]]θ = {inl M : M ∈ [[σ]]θ}^{∗} ∪ {inr M : M ∈ [[τ]]θ}^{∗}
[[σ × τ]]θ = {(M_{1}, M_{2}) : M_{1} ∈ [[σ]]θ, M_{2} ∈ [[τ]]θ}^{∗}
[[σ → τ]]θ = [[σ]]θ → [[τ]]θ
[[μXσ]]θ = Φ^{Ω}  where Φ = Φ_{X.σ,θ}
[[ρ^{+}]]θ = Φ^{α+1}  if  [[ρ]]θ = Φ^{α}
[[∀Y ≤μXσ. τ]]θ = ⋂_{α<Ω}[[τ]](θ, Y ↦Φ^{α}) where Φ = Φ_{X.σ,θ}
and Φ_{X.σ,θ}(Q) = {fold M : M ∈ [[σ]](θ, X ↦Q)}^{∗}

It can be shown that for →-free inductive types the least-fixed point is reached at ordinal ω. Examples include Nat = μX. 1 + X and ListN = μX. 1 + Nat × X, but also the empty type.

Example 5.3 (Interpretation of the Empty Type). A built-in empty type 0 would be interpreted as O. In our case, 0 is defined and [[0]]θ = [[μX.X]]θ = Φ_{X.X,θ}^{ω} = (Q ↦ {fold M : M ∈ Q}^{∗})^{ω}. But we can show that [[0]] is extensionally equal to O, i.e., for all M ∈ [[0]] exists some N ∈ O such that abort M ⟶^{∗} abort N (recall that abort = fix g(x). g (unfold x)). The proof proceeds by induction on the approximations of [[0]] with a side induction on the saturation and makes use of the fact that abort (fold N) ⟶^{+} abort N.

Inductive types involving function spaces can have a closure ordinal greater than ω. One instance is the type of tree ordinals Ord introduced in Example 3.6.

Example 5.4. [Ord Requires Iteration Beyond ω] Let Φ denote the generating operator for type Ord. Then the conversion function from natural numbers to tree ordinals toOrd ∈ [[Nat]] → Φ^{α} if and only if α ≥ ω. Hence the least approximation stage that omega = OLim toOrd inhabits is ω + 1.

We continue by showing that the interpretation of a positive type is a monotone operator. But first, observe that the interpretation is preserved under substitution, that is, for types σ(X) and ρ it holds that

[[σ]](θ, (X ↦[[ρ]]θ), θ′) = [[σ(ρ)]](θ, θ′).

Lemma 5.5 (Monotonicity of itype s). Let Γ; X⃗; X⃗′ ⊢ σ : itype and θ, θ′ be valuations with θ(Y) = θ′(Y) for all Y ∈ Γ, θ(X_{i}) ⊆ θ′(X_{i}) for all 1 ≤ i ≤ |X⃗| and θ(X′_{j}) ⊇ θ′(X′_{j}) for all 1 ≤ j ≤ |X⃗′|. Then [[σ]]θ ⊆ [[σ]]θ′ and Φ_{X.σ,θ}^{α} ⊆ Φ_{X.σ,θ′}^{α} for all ordinals α.

Proof. By induction on Γ; X⃗; X⃗′ ⊢ σ : itype. □

For datatypes σ : itype, the interpretation [[σ]]θ is monotone in θ (in the sense of the previous lemma), hence also the operator Φ_{X.σ,θ}, which additionally has the property O ⊆ Φ_{X.σ,θ}(O). This entails that the fixpoints exist and the iterates (Φ_{X.σ,θ}^{α}) form a cumulative hierarchy. The following fact will be important for the proof of strong normalization: If a data value inhabits an approximation type, it is already found in a successor iterate.

Lemma 5.6. If fold M ∈ Φ^{α} then fold M ∈ Φ^{β+1} for some β < α.

Proof. By transfinite induction on α. □

5.3. Proof of Strong Normalization

To complete the proof of strong normalization, we first ensure that the interpretation of every type is a saturated set. Then we show that each well-typed term inhabits the interpretation of its type and therefore is strongly normalizing.

Wellformed contexts Γ cxt are interpreted as the set of all sound valuations. We define θ ∈ [[Γ]] inductively by the following rules.

\overline{· ∈ [[·]]}  \frac{θ ∈ [[Γ]]  M ∈ [[τ]]θ}{(θ, x↦M) ∈ [[Γ, x:τ]]}  \frac{θ ∈ [[Γ]]  Φ = Φ_{X.σ,θ}}{(θ, Y ↦Φ^{α}) ∈ [[Γ, Y ≤μXσ]]}

We now can verify that our subtyping calculus is sound:

Lemma 5.7 (Soundness of Subtyping). If Γ ⊢ ρ ≤ σ then for all θ ∈ [[Γ]] it holds that

[[ρ]]θ = Φ^{α} ⊆ Φ^{β} = [[σ]]θ

for some operator Φ and some ordinals α and β.

Proof. By induction over the derivation of Γ ⊢ ρ ≤ σ. □

Note that in the previous lemma we do not always have α ≤ β, since subtyping accepts (μXσ)^{+} ≤ μXσ, for example.

Lemma 5.8 (Saturatedness of Type Interpretations). If Γ ⊢ τ : type then for all θ ∈ [[Γ]] we have [[τ]]θ ∈ SAT .

Proof. State similar propositions for the other three type-related judgements on Table 2 and prove all propositions by simultaneous induction. □

Lemma 5.9 (Wellformed Contexts are Satisfiable). If Γ cxt then there exists some θ ∈ [[Γ]].

Proof. By induction on Γ cxt. For the empty context, we take the empty valuation. In case Γ = (Γ′, x: τ) with Γ′ ⊢ τ : type we know by Lemma 3.1 that Γ′ cxt and obtain a θ′ ∈ [[Γ′]] by induction hypothesis. Since by the last lemma [[τ]]θ′ is a saturated set, it contains x and hence θ = (θ′, x ↦ x) is the desired valuation for Γ. In the remaining case Γ = (Γ′, Y ≤ μXσ) we similarly obtain a θ′ ∈ [[Γ′]] by induction hypothesis and extend it by the mapping Y ↦[[μXσ]]θ′. □

Now we have assembled all the pieces to prove strong normalization.

Theorem 5.10 (Soundness of Typing). If Γ ⊢ M : τ then for all θ ∈ [[Γ]] we have Mθ ∈ [[τ]]θ.

Proof. By induction on Γ ⊢ M : τ. We only show the interesting cases of fold, unfold and fix.

Case

\frac{Γ ⊢ ρ ≤ μX.σ(X) Γ ⊢ M : σ(ρ)}{Γ ⊢ fold M : ρ^{+}}

From the assumption follows [[ρ]]θ = Φ^{α} for Φ(Q) = {fold N : N ∈ [[σ]](θ, X ↦Q)}^{∗} and some α. By induction hypothesis, Mθ ∈ [[σ]](θ, X ↦ Φ^{α}). Thus, fold Mθ ∈ Φ^{α+1} = [[ρ^{+}]]θ.

Case

\frac{Γ ⊢ ρ ≤ μX.σ(X) Γ ⊢ M : ρ^{+}}{Γ ⊢ unfold M : σ(ρ)}

As in the last case, [[ρ]]θ = Φ^{α}. By induction hypothesis, Mθ ∈ Φ^{α+1}. We show unfold Mθ ∈ [[σ(ρ)]]θ by side induction on the saturation of Φ^{α}.

Subcase Mθ = E[x]. Then unfold Mθ = unfold E[x] is neutral and strongly

normalizing and therefore element of [[σ(ρ)]]θ. Subcase Mθ = E[M_{0}], M_{0} ∈ SN, M_{0} ⟶_{β} M_{1} and E[M_{1}] ∈ Φ^{α}. By side

induction hypothesis, unfold E[M_{1}] ∈ [[σ(ρ)]]θ and by saturation also unfold E[M_{0}] ∈ [[σ(ρ)]]θ.

Subcase Mθ = fold N with N ∈ [[σ]](θ, X ↦ Φ^{α}) = [[σ(ρ)]]θ. Since we can reduce unfold(fold N) ⟶_{β} N, by saturatedness it follows that unfold Mθ ∈ [[σ(ρ)]]θ.

Case

\frac{Γ, Y ≤μXσ, g:∀Y → τ(Y), x:Y^{+} ⊢ M : τ(Y^{+})}{Γ ⊢ fix g(x).M : ∀Y ≤μXσ. Y → τ(Y)}

where Y appears only positively in τ. Let Φ = Φ_{X.σ,θ}. Then [[∀Y ≤ μXσ. Y → τ(Y)]]θ = ⋂_{α<Ω}(Φ^{α} → [[τ]](θ, Y ↦ Φ^{α})). We show for all ordinals α,

(fix g(x).M)θ ∈ Φ^{α} → [[τ]](θ, Y ↦Φ^{α})

by a first side induction on α. Fix the ordinal α and some term N ∈ Φ^{α}. We show

(fix g(x).M)θ N ∈ [[τ]](θ, Y ↦Φ^{α})

by a second side induction on the saturation of Φ^{α}. Subcase N = E[x]. Then (fix g(x).Mθ) E[x] is neutral and in [[τ]](θ, Y ↦Φ^{α}). Subcase N = E[N_{1}] with N_{1} ⟶_{β} N_{2} and E[N_{2}] ∈ Φ^{α}. By the second side

induction hypothesis, (fix g(x).Mθ) E[N_{2}] ∈ [[τ]](θ, Y ↦ Φ^{α}), and by saturatedness also (fix g(x).Mθ) E[N_{1}] ∈ [[τ]](θ, Y ↦Φ^{α}).

Subcase N = fold N′ ∈ Φ^{β+1} ⊆ Φ^{α} (with Lemma 5.6). By the first side induction hypothesis fix g(x).M ∈ (Φ^{β} → [[τ]](θ, Y ↦Φ^{β})). Hence,

\begin{aligned}θ′ & = & (θ, Y ↦Φ^{β}, g ↦ fix g(x).M, x↦N) \\ & ∈ & [[Γ, Y ≤μXσ, g:Y → τ(Y), x:Y^{+}]] \end{aligned}

By main induction hypothesis

\begin{aligned}Mθ′ & ∈ & [[τ(Y^{+})]]θ′ = [[τ]](θ, Y ↦Φ^{β+1}) \\ & ⊆ & [[τ]](θ, Y ↦Φ^{α}), \end{aligned}

since Y appears only positively in τ. We can conclude by saturation, since

(fix g(x).M)θ (fold N) ⟶_{β} Mθ′. □

Remark 5.11 (Transfinite Induction). The soundness proof for the fixed point rule uses a course-of-value transfinite induction on α, using the fact that new canonical inhabitants of an inductive datatype are only found at successor iterates (Lemma 5.6). It is quite instructive to consider the less economic proof by a simple transfinite induction. In this case, the base case α = 0 holds since Φ^{0} contains no canonical forms fold N, the step case α ⇝ α + 1 follows from the main induction hypothesis and the limit case α = λ needs monotonicity of [[τ(Y)]] which is ensured by the positivity condition for τ.

Corollary 5.12 (Strong Normalization). If Γ ⊢ M : τ then M ∈ SN.

Proof. By Lemma 3.5 the context Γ is wellformed. This entails that there exists a valuation θ ∈ [[Γ]], as constructed in the proof of Lemma 5.9, which maps all term variables to themselves. Hence Mθ = M, and by soundness of typing M ∈ [[τ]]θ ⊆ SN, since the interpretation of τ is saturated. □

Remark 5.13 (Type-Based Termination in DML). Xi’s [50] more sophisticated type system admits inconsistent contexts Γ. Consequently, strong normalization does not hold although he can prove soundness of typing analogously to our Theorem 5.10. But since in his case, a θ ∈ [[Γ]] as in the last proof does not always exist, he can show normalization only for closed terms (empty Γ).

Strong normalization excludes infinite reduction sequences. More directly, we can show that each possibly infinite reduction sequence is in fact finite. As a consequence, each well-typed Λ_{μ}^{+}-program reduces to a value.

Lemma 5.14 (Termination). If M ∈ SN and M ⟶^{∞} M′ then M ⟶^{∗} M′.

Proof. By induction on M ∈ SN and cases on M ⟶^{∞} M′. □

Corollary 5.15 (Reduction to Value). If Γ ⊢ M : τ then M ⟶^{∗} V.

Proof. By Corollary 1.2, M ⟶^{∞} V. Since M ∈ SN by Corollary 5.12, Lemma 5.14 implies M ⟶^{∗} V. □

6. Extensions

Two issues are briefly discussed in this section: The positivity requirement for result types in the recursion rule and approximations of coinductive types. Both topics are treated rather informally and incompletely, more systematic approaches can be found in Pareto [37], Barthe et al. [9] and Abel [3].

6.1. On Non-Monotonic Result Types of Recursion

In Section 2 we promised to motivate why we required the result type τ(Y) of recursion to be positive in Y. In his first presentation, Giménez [23] had no such requirement, it was added later [9]. Indeed, if we simply drop the side condition,

\frac{Γ, Y ≤μXσ, g:Y → τ(Y), x:Y^{+} ⊢ M : τ(Y^{+})}{Γ ⊢ fix g(x).M : ∀Y ≤μXσ. Y → τ(Y)}

we can type non-terminating functions, which we will demonstrate in the following. Recall the type Nat = μX. 1+X with the defined constructors Zero and Succ from Section 1. We introduce an abbreviation

maybe : (1 + σ) → τ → (σ → τ) → τ
maybe := λtλbλf. case t of inl ⇒ b | inr a ⇒ f a

for any types σ and τ. For ρ ≤ Nat, we define:

shift : (Nat → (1 + ρ^{+})) → Nat → (1 + ρ)
shift := λfλn. maybe (f (Succ n)) (inl()) (λz. unfold z)
inc : Nat → (1 + Nat)
inc := λn. inr (Succ n)

The function inc is a fixed-point of shift as we can show by the following reduction sequence:

shift inc ⟶^{+} λn. maybe (inr (Succ (Succ n))) (inl ()) (λz. unfold z)
⟶^{+} λn. unfold (Succ (Succ n))
⟶^{+} λn. inr (Succ n)
= inc

Using shift, we can construct a recursive function g with result type τ(Y) = (Nat → (1 + Y)) → 1 which loops on input inc.

g : ∀Y ≤Nat. Y → (Nat → (1 + Y)) → 1
g := fix g( ). λf. maybe (f Zero) ()

(λx. maybe (unfold x) () (λy. g y (shift f)))

This function is well typed, we can infer the following types for some subexpressions:

g : Y → (Nat → (1 + Y)) → 1
f : Nat → (1 + Y^{+})
x : Y^{+}
y : Y
shift f : Nat → (1 + Y)

Hence, the application of the recursive function g y (shift f) is accepted by the type system. By a simple computation,

g Zero inc ⟶^{+} g Zero (shift inc) ⟶^{+} g Zero inc

and we have created a loop.

What exactly causes non-termination? Not the mere negative occurrence of Y because the type ∀Y ≤ Nat. Y → (1 + Y) → 1 would be unproblematic for terminating recursion (cf. Abel [3]). Only through the presence of an argument f of type Nat → (1 + Y), arbitrary natural numbers n can “sneak through the back door f” being declared of type Y on the way and present themselves as safe arguments for recursion.

To be on the safe side, all arguments a : τ′(Y) (for Y ≤ μXσ) to a recursive function must be cocontinuous [3] resp. overshooting (in the terminology of Hughes, Pareto and Sabry [28]). This means that for each limit ordinal λ,

[[τ′]](Y ↦Φ^{λ}) ⊆ ⋃_{α<λ}[[τ′]](Y ↦Φ^{α}),

where Φ = Φ_{X.σ}. In our counterexample (where τ′(Y) = Nat → (1 + Y)), the argument inc violates this requirement for λ = ω. While inc clearly inhabits the set [[Nat → (1 + Nat)]] on the left hand side, it is not member of the right hand side set [[Nat → (1 + Y)]](Y ↦Φ^{α}) for any α < ω, since Φ^{α} contains only codes for the natural numbers < α.

A systematic treatment of admissible result types of recursion can be found in Pareto’s PhD thesis [37], for evaluation of closed terms, and in Abel [3], for evaluation under binders.

6.2. On Coinductive Datatypes

Approximation types have been used to check productivity of infinite structures like streams (cf. Hughes, Pareto and Sabry [28], Amadio and Coupet-Grimal [7], Giménez [23] and Barthe et al. [9]). In the following, we demonstrate how to simulate productivity checking for streams in our type system via an encoding of streams as functions over natural numbers.

Streams, being infinite sequences of elements of a fixed type, can—in finitary languages—only be defined by recursion. The dual to termination in the case of functions is productivity for streams. It means that at any time, one can unfold a stream and extract its first element, obtaining a remainder which is again productive. What the size is for inductive data is definedness for coinductive structures. If we define U to be the set of all partial streams of natural numbers,

S_{n} := {s ∈ U | s can be unfolded n times }

characterizes the streams of definedness n. While the corresponding predicate L_{n} for lists is covariant in its argument n (see Section 2), i.e., L_{n} ⊆ L_{m} for n ≤ m, definedness is contravariant: S_{n} ⊆ S_{m} for m ≤ n. The set of productive streams S = S_{ω} is the bottom element of the approximation chain (S_{n}). Productive streams can be obtained via the induction rule “if s ∈ S_{n} implies s ∈ S_{n+1} for all n, then s ∈ S”. In the following, we present rules for productive streams which could form an extension of Λ_{μ}^{+}. Later we will show that these rules are admissible in a small extension of our original calculus.

Formation.

\frac{Γ; X⃗; X⃗′ ⊢ σ : itype}{Γ; X⃗; X⃗′ ⊢ Stream(σ) : itype}  \frac{Γ, Y ≥Stream(σ) ⊢ τ(Y) : type}{Γ ⊢ ∀Y ≥Stream(σ). τ(Y) : type}

Subtyping.

Stream(σ) ≤ … ≤ Stream(σ)^{++} ≤ Stream(σ)^{+} ≤ Stream(σ)
Stream(σ) ≤ … ≤ Y^{++} ≤ Y^{+} ≤ Y (for Y ≥ Stream(σ))

Elimination.

Γ ⊢ hd : ∀Y ≥Stream(σ). Y^{+} → σ Γ ⊢ tl : ∀Y ≥Stream(σ). Y^{+} → Y

Introduction.

Γ ⊢ scons : σ → ∀Y ≥Stream(σ). Y → Y^{+}

Recursion.

\frac{Γ, Y ≥Stream(σ), g:τ(Y) → Y ⊢ M : τ(Y^{+}) → Y^{+} Y pos. in τ(Y)}{Γ ⊢ fix_{2} g.M : ∀Y ≥Stream(σ). τ(Y) → Y}

Reduction.

hd (scons M N) ⟶_{β} M
tl (scons M N) ⟶_{β} N
hd ((fix_{2} g.M) N) ⟶_{β} hd ([fix_{2} g.M/g]M N)
tl ((fix_{2} g.M) N) ⟶_{β} tl ([fix_{2} g.M/g]M N)

These rules enable us, for instance, to code the sequence of natural numbers starting at a given n, and a sorted merging of streams.

nats : ∀Y ≥Stream(Nat). Nat → Y
nats := fix_{2} nats. λn. scons n (nats (Succ n))
merge : ∀Y ≥Stream(Nat). Y × Y → Y
merge := fix_{2} merge. λp.

let x=hd (fst p) in let y =hd (snd p) in if x < y then scons x (merge (tl (fst p), snd p)

else scons y (merge (fst p), tl (snd p))

We claim that all we need to simulate streams via the definition Stream(σ) = Nat → σ in our type system, is a little more liberal handling of subtyping and bounded quantification and a new fixed-point combinator which implements recursion on the second argument. Thus, we extend Λ_{μ}^{+} by the following rules instead:

Bounded quantification and subtyping.

\frac{Γ, X≤μZσ ⊢ τ(X) : type}{Γ ⊢ ∀X≤μZσ. τ(X) : type}  \frac{Γ ⊢ σ′ ≤ σ  Γ ⊢ τ ≤ τ′}{Γ ⊢ σ → τ ≤ σ′ → τ′}  \overline{Γ ⊢ σ ≤ σ}

Recursion on the second argument.

X neg. in τ
X pos. in τ′
Γ, X≤μZσ, g : τ(X) → X → τ′(X) ⊢ M : τ(X^{+}) → X^{+} → τ′(X^{+})
Γ ⊢ fix_{2} g.M : ∀X≤μZσ. τ(X) → X → τ′(X)

Reduction.

(fix_{2} g.M) N_{1} (fold N_{2}) ⟶_{β} [fix_{2} g.M/g]M N_{1} (fold N_{2})

To encode streams in the extended Λ_{μ}^{+}, we replace all quantifications ∀Y ≥ Stream(σ) by ∀X ≤ Nat, all occurrences of Y^{i} by (X^{i} → σ) and all remaining occurrences of Stream(σ)^{i} by (Nat^{i} → σ). The formation rules for streams are immediately valid, and subtyping can be justified using the rule for arrow, for example Y^{+} ≤ Y:

\frac{X ≤ X^{+} σ ≤ σ}{(X^{+} → σ) ≤ (X → σ)}

Destructors and the constructor for streams can be defined with the correct typing:

hd  : ∀X≤Nat. (X^{+} → σ) → σ
hd  := λs. s Zero
tl  : ∀X≤Nat. (X^{+} → σ) → X → σ
tl  := λsλn. s (Succ n)
scons : σ → ∀X≤Nat. (X → σ) → X^{+} → σ
scons := λaλsλn. maybe (unfold n) a s

In the typing of scons we need the new introduction rule for bounded quantification. The fixed-point combinator for streams is a special case of recursion over the second argument, with τ′(X) = σ. The polarity conditions are satisfied, since Y positive in τ(Y) implies X negative in τ(X → σ). By calculation, we verify the computational behavior for streams:

hd (scons M N) ⟶ (λn. maybe (unfold n) M N) Zero
⟶^{+} M
tl (scons M N) ⟶ λn. (λn′. maybe (unfold n′) M N) (Succ n)
⟶^{+} λn. N n
hd ((fix_{2} g.M) N) ⟶ ((fix_{2} g.M) N) Zero
⟶ ([fix_{2} g.M/g]M N) Zero
=  hd ([fix_{2} g.M/g]M N)
tl ((fix_{2} g.M) N) ⟶ λn. ((fix_{2} g.M) N) (Succ n)
⟶ λn. ([fix_{2} g.M/g]M N) (Succ n)
⟵ tl ([fix_{2} g.M/g]M N)

Reduction is not completely simulated by the encoding since tl M is equal to a lambda-abstraction. But for each axiom M ⟶_{β} M′ for streams, M and M′ are βη-equal in the encoding. The reader is invited to check that the programs for nats and merge also inhabit the translated types.

nats : ∀X≤Nat. Nat → X → Nat
merge : ∀X≤Nat. (X → Nat) × (X → Nat) → X → Nat

Summing up, we have managed to justify the use of approximation stages also for coinductive types in the example of streams. We hope that we hereby have provided an easy access to the rules of productivity checking for infinite structures, which are—in the experience of the author—harder to communicate than the rules for termination checking.

7. Applications

After establishing soundness, we show the effectiveness of the presented approach in this section. We sketch how the explored principles can be applied in functional programming, theorem proving and, as a specific example, for resource bound certification.

7.1. Functional Programming

Throughout the article we have demonstrated type-based termination on small functional programs already. In the following we present another example which shows that our system can handle mutual recursion, interleaving inductive types, and even non-strictly positive types.

We introduce two abbreviations for certain datatypes: X list for lists over some type X and term for first-order terms with continuations.

X list = μY. 1 + X × Y
term = μX. int + int ×(X list) + ((X → 0) → 0)

The first-order terms we consider are constructed from variables, n-ary function symbols and continuations^{6}. We have three constructors:

Var : int → term
Func : int ×term list → term
Mu : ((term → 0) → 0) → term

Var(i) denotes the ith variable, Func(i, l) the ith function symbol applied to the terms of the list l and

Mu(λa^{term→0}. b^{term→0} t)

the term that stores the current continuation in a, retrieves a continuation b and throws the term t at b.

Note that term is the rare example of a non-strictly positive type, furthermore term and list are interleaving, also called nested. Nevertheless, our system accepts the following mutually recursive substitution function.

subst : (int → term) → ∀X≤term. X → term

subst f (Var(i))^{X^{+}} = f(i)

subst f (Func(i, l))^{X^{+}} = Func(i, sl(l^{X list}))

where sl : ∀Y ≤X list. Y → term list sl ([])^{Y^{+}} = []

sl (t :: ts)^{Y^{+}} = (subst f t^{X}) :: sl ts^{Y}

subst f (Mu(t))^{Y^{+}} = Mu (λa^{term→0}. t^{(Y →0)→0} (λr^{Y}.

a (subst f r^{Y})))

Recursion over interleaving inductive datatypes is most naturally expressed by mutually recursive functions. In our case it is crucial that this mutual recursion is not simultaneous but interleaving, as the approximation of the type of terms X ≤ term must be available with in the inner function sl for the approximation Y ≤ X list. Informally, X contains terms upto a certain height and X list lists of such terms. Hence, Y contains lists of restricted length which consist of terms of bounded height. The typing ensures that the call subst f t within sl terminates, no call graphs are necessary (cf. Abel and Altenkirch [5] or Lee, Jones and Ben-Amram [30]).

6The continuations we consider are modeled after the λμ-calculus (Parigot [38]), which is very well presented in Bierman [10]. The chosen representation as positive type is derived from Abel [2].

The last line encodes substitution for continuations, applying our technique for non-strictly positive types. Here, termination is not obvious at all, also not for measure-based approaches—it is not clear which measure one should use. For sure, termination cannot be checked with the usual untyped notion of the subterm ordering, since r is no subterm of t. Type-based termination succeeds since the types provide us with some data flow information which is not available in subterm calculi.

In every-day programming, some functions are not terminating on all inputs. Others may be terminating, but the termination proof may involve complicated arguments and cannot be checked automatically. For that reason, it is desirable to allow both total and partial functions in a program. This can be realized naturally in our system by simply adding the fix-rule of Λ_{μ} which does not impose any restriction on recursion. In the extended system, functions are total if their typing derivation does not use the liberal fix-rule. To keep efficiency in an implementation of the type system, functions could be tagged as total resp. possibly partial by the compiler.

7.2. Theorem Proving

As pointed out in the introduction, the typed-based approach to termination is suitable for theorem provers based on theories with inductive definitions, e.g., Agda [16], Coq [29], and LEGO [43]. However, it needs to be adapted to dependent type theories. A first proposal has been put forth by Blanqui [12]. He combines parts of the approaches of Xi [50], Giménez et al. [9,23] and Hughes et al. [28] to obtain a type-based termination criterion for the Calculus of Algebraic Constructions.

7.3. Resource Bound Certification

Crary and Weirich [19] describe a language LXres for resource bound certification. To estimate the cost of defined operations they use static cost functions. Technically these cost functions are so-called constructors in their type theory which is based on F^{ω}. For type-checking to be decidable, these constructors must be terminating. Currently they are restricted to Mendler-style primitive recursive functions (see Section 2). Our extension could be integrated into their type theory which would strictly increase the expressiveness of their language.

8. Conclusion

We have presented a method of ensuring termination by types, shown soundness, given an algorithm for type checking and discussed applications besides the intended use in theorem provers. Table 7 gives an overview over the technical results of this article. In Section 4 we have formalized a type checking algorithm which is sound for Λ_{μ}^{+}. Typing of Λ_{μ}^{+} excludes infinite reduction sequences as proven in Section 5. Each Λ_{μ}^{+}-program can also be assigned a Λ_{μ}-type which is obtained by erasure (Section 3.3) and guarantees that evaluation does not get stuck

[figure: Γ ⊢ M′ : τ (Λ_{μ}^{+}); \begin{matrix}Γ ||⟩ Γ′; Δ \\ Δ ⊢ τ ||⟩ τ′ \end{matrix}; M′ ∈ SN; Γ ⊢ M ⇑ τ; M′ = |M|; M′ ⟶^{∗} V; Γ′ ⊢ M′ : τ′ (Λ_{μ}); M′ ⟶^{∞} V]

Table 7. Summary of Technical Results.

(Section 1). Putting things together, each type-checkable Λ_{μ}^{+}-program reduces to a value in finite time.

Type based termination combines three program analyses: ordinary type checking, termination checking and what is called reduction checking (Pientka [40]) resp. size checking (Chin and Khoo [15]). We expect that this combination will make implementations of normalizing calculi more succinct, efficient and transparent to the user. However, to give substance to our claim, implementations of type based termination have to be tested in practice.

We conclude with a discussion of related work on sized types and termination.

8.1. Hughes, Pareto et al.

Hughes, Pareto [27] and Sabry [28] use sized types for termination and productivity checking of functional programs. A detailed treatment is given by Pareto in his thesis [37]. His type system refers to approximations of the type of natural numbers as Nat i where i is a size expression. The full type of natural numbers is represented as Nat ω. Instead of bounded quantification he uses quantification over size variables, and our next-stage operation (·)^{+} is simulated by a successor operation on sizes. For instance, the type Nat → ∀Y ≤ ListN. Y → Y × Y of the pivot function would be written Nat → ∀i. List i Nat → List i Nat × List i Nat in his system, where i is a size variable.

Pareto’s type language is more expressive than ours in two aspects: First, since sizes are separated from approximation stages, he can assign, for instance, the precise type ∀α. ∀i. List i α → Nat i to the length function; furthermore, this enables size information for polymorphic functions like map: ∀α∀β. (α → β) → ∀i. List i α → List i β. Secondly, size expressions can contain addition of sizes and multiplication with a constant, thus, a more precise type ∀α ∀i. List i α → ∀j. List (j + 1) α → List (i + j) α of the append function is possible. On the other hand, since sizes are bounded by ordinal ω, he can not treat inductive types with embedded function spaces like Ord (Example 3.6). Also, his semantics is denotational and based on domains, hence he only shows termination for closed programs, whereas we permit evaluation under binders.

Notwithstanding the different interpretations, the formation of recursive functions underlies the same constraints in Pareto’s and our approach. Our side condition on the fixed point rule (see Section 6.1) is a restriction of his condition to instantiate a size quantifier ∀i to the limit ordinal ω. He has another side condition on the fixed point rule, the so called bottom check. It expresses that the type ∀i. τ of a recursive function must, when i is instantiated to 0, be the universe of all terms in the semantics. In our setting, types of recursive functions are restricted to the shape Y → τ′(Y), which trivially satisfy the bottom check [37, page 148] for empty types Y such as the 0th approximation of an inductive type. Our pendant to the bottom check is the base case α = 0 of the transfinite induction over α in the soundness proof of the fixed point rule (see Remark 5.11).

8.2. Giménez et al.

Giménez [23] provided the starting point for our work. He describes typebased termination using approximation types for an extension of the Calculus of Constructions, but provides no soundness proof. Showing strong normalization for his method was the original motivation for the present article.

In Giménez later work with Barthe et al. [9], the formulation of the type system follows Hughes et al.. The set of size expressions is generated by size variables, the successor operation, and the symbol ∞, denoting the first uncountable ordinal Ω. The type system features function types and inductive datatypes, but excludes quantification over size variables, hence one cannot abstract over a size-preserving function (see qsapp′ in Section 2.4). Except for bounded quantification, our system embeds into Barthe et al., and they give both a proof of subject reduction and strong normalization. However, they do not describe a type checking algorithm. Thus, their type system is not ready to be used as a termination checker.

8.3. Xi’s Dependent ML

Xi [50] considers termination of closed functional programs in DML, a functional language with lightweight dependent types. In contrast to our approach and the approaches described above, the size of a data structure is not determined to be its height, but it can be any integer expression defined by the user. For example, one could define the size of a tree as the total number of nodes, or even the sum of its labels. Recursive functions come with a termination measure which has the form of a lexicographic product of size expressions. His size annotations are exact in contrast to our notion of size which is just an upper bound. Therefore, he does not need subtyping; to compare integer expressions he relies on a constraint solver.

On one hand, due to exact size annotations, Xi can also perform size-checking for accumulation parameters in functions, which is impossible with the approaches mentioned above. This qualifies Xi’s approach for practical termination checking of realistic functional programs. On the other hand, since Xi has no ordinal sizes, he can not handle higher-order datatypes like infinite trees which are common in proof theory. This limits the applicability of his approach in theorem provers.

8.4. Other Related Work

On termination in general, a vast amount of literature has been published, so we can only give a non-representative overview of work related to ours.

Typed functional programming. In previous work [1] with Thorsten Altenkirch [5], we have described a syntactic check for structurally recursive functions in the context of simple types. We proved termination only for closed terms (no strong normalization). Telford and Turner [45,46] check termination and productivity of recursive functions by an abstract interpretation. They track size-change on an abstract domain; the power of the approach is comparable to the one presented here. Giesl [22], also with Brauburger [14], generates termination predicates by static analysis of functional programs. Termination can be proven by some external automated theorem prover. Their approach is limited in power only by the theorem prover, hence very flexible, but also quite unpredictable.

Higher-order logic programming. Pientka [40] describes a calculus for termination and reduction checking of logic programs over a higher-order term language. Her calculus is based on the subterm ordering and used in the HOAS theorem prover Twelf [39].

Untyped functional programming. Lee, Jones and Ben-Amram [30] investigate termination of untyped first-order functional programs via size-change graphs. They show that the implicit complexity of termination-checking mutually recursive functions is PSPACE-hard.

Term rewriting. This is the classical area of investigating termination. We accentuate Giesl’s work, for example, with Arts, on dependency pairs [8]. Blanqui, Jouannaud and Okada investigate term rewriting for systems with inductive types [13]. In his thesis [11], Blanqui proves strong normalization for the Calculus of Algebraic Constructions with rewrite rules.

The author thanks Thorsten Altenkirch for more than one year of joint work on termination, Thierry Coquand for pointing to Giménez’ work, John Hughes and Lars Pareto for a conversation which eventually lead to the counterexample in Section 6, Martin Hofmann, Frank Pfenning and Brigitte Pientka for helpful discussions, and Frédéric Blanqui for encouraging feedback on this article. He is indebted to Ralph Matthes for careful reading of the draft and for conversation and advice which helped overcome unforeseen difficulties in the final preparation phase of this articles. Last but not least, thanks to the anonymous referees for critical remarks which led to a clearer presentation.

References

[1] A. Abel. Specification and verification of a formal system for structurally recursive functions. In T. Coquand, P. Dybjer, B. Nordström, and J. Smith, editors, Types for Proof and Programs, International Workshop, TYPES ’99, volume 1956 of Lecture Notes in Computer Science, pages 1–20. Springer, 2000.

[2] A. Abel. A third-order representation of the λμ-calculus. In S. Ambler, R. Crole, and A. Momigliano, editors, Electronic Notes in Theoretical Computer Science, volume 58. Elsevier Science Publishers, 2001.

[3] A. Abel. Termination and guardedness checking with continuous types. In M. Hofmann, editor, Typed Lambda Calculi and Applications (TLCA 2003), volume 2701 of Lecture Notes in Computer Science, pages 1–15, Valencia, Spain, June 2003. Springer.

[4] A. Abel. Soundness of a bidirectional typing algorithm. Twelf code, available on the author’s homepage, http://www.tcs.informatik.uni-muenchen.de/˜ abel, May 2004.

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

[6] T. Altenkirch. Constructions, Inductive Types and Strong Normalization. PhD thesis, University of Edinburgh, November 1993.

[7] R. M. Amadio and S. Coupet-Grimal. Analysis of a guard condition in type theory. In M. Nivat, editor, Foundations of Software Science and Computation Structures, First International Conference, FoSSaCS’98, volume 1378 of Lecture Notes in Computer Science. Springer, 1998.

[8] T. Arts and J. Giesl. Termination of term rewriting using dependency pairs. Theoretical Computer Science, 236:133–178, 2000.

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

[10] G. M. Bierman. A computational interpretation of the λμ-calculus. In L. Brim, J. Gruska, and J. Zlatuska, editors, Proceedings of Symposium on Mathematical Foundations of Computer Science, volume 1450 of Lecture Notes in Computer Science, pages 336–345, Brno, Czech Republic, August 1998.

[11] F. Blanqui. Type Theory and Rewriting. PhD thesis, Univeristé Paris XI, Sept. 2001.

[12] F. Blanqui. A type-based termination criterion for dependently-typed higher-order rewrite systems. In V. van Oostrom, editor, Rewriting Techniques and Applications, 15th International Conference, RTA 2004, Aachen, Germany, June 3 – 5, 2004, Proceedings, volume 3091 of Lecture Notes in Computer Science, pages 24–39. Springer, 2004.

[13] F. Blanqui, J.-P. Jouannaud, and M. Okada. Inductive data type systems. Theoretical Computer Science, 277, 2001.

[14] J. Brauburger and J. Giesl. Termination analysis for partial functions. In Proceedings of the Third International Static Analysis Symposium (SAS’96), volume 1145 of Lecture Notes in Computer Science, Aachen, Germany, 1996. Springer.

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

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

[17] T. Coquand. Infinite objects in type theory. In H. Barendregt and T. Nipkow, editors, Types for Proofs and Programs (TYPES ’93), volume 806 of Lecture Notes in Computer Science, pages 62–78. Springer, 1993.

[18] T. Coquand. An algorithm for type-checking dependent types. In Mathematics of Program Construction. Selected Papers from the Third International Conference on the Mathematics of Program Construction (July 17–21, 1995, Kloster Irsee, Germany), volume 26 of Science of Computer Programming, pages 167–177. Elsevier Science, May 1996.

[19] K. Crary and S. Weirich. Resource bound certification. In Proceedings of the 27th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 184–198, Boston, Massachusetts, USA, January 2000.

[20] R. Davies and F. Pfenning. Intersection types and computational effects. In Proceedings of the International Conference on Functional Programming (ICFP 2000), pages 198–208, Montreal, Canada, September 2000.

[21] J. Dunfield and F. Pfenning. Tridirectional typechecking. In N. D. Jones and X. Leroy, editors, 31st Annual Symposium on Principles of Programming Languages (POPL’04), Venice, Italy, pages 281–292. ACM, jan 2004.

[22] J. Giesl. Termination of nested and mutually recursive algorithms. Journal of Automated Reasoning, 19:1–29, 1997.

[23] E. Giménez. Structural recursive definitions in type theory. In Automata, Languages and Programming, 25th International Colloquium, ICALP’98, Aalborg, Denmark, July 13-17, 1998, Proceedings, volume 1443 of LNCS, pages 397–408. Springer, 1998.

[24] C. Haack and J. B. Wells. Type error slicing in implicitly typed, higher-order languages. In Programming Languages and Systems, 12th European Symp. Programming, volume 2618 of Lecture Notes in Computer Science, pages 284–301. Springer, 2003.

[25] T. Hagino. A typed lambda calculus with categorical type constructors. In D. H. Pitt, A. Poigné, and D. E. Rydeheard, editors, Category Theory and Computer Science, volume 283 of Lecture Notes in Computer Science, pages 140–157. Springer, 1987.

[26] T. Hallgren. Alfa home page. http://www.math.chalmers.se/˜ hallgren/Alfa/, 2003.

[27] J. Hughes and L. Pareto. Recursion and dynamic data-structures in bounded space: Towards embedded ML programming. In International Conference on Functional Programming (ICFP’99), pages 70–81, 1999.

[28] J. Hughes, L. Pareto, and A. Sabry. Proving the correctness of reactive systems using sized types. In Symposium on Principles of Programming Languages, pages 410–423, 1996.

[29] INRIA. The Coq Proof Assistant Reference Manual, version 8.0 edition, April 2004. http://coq.inria.fr/doc/main.html.

[30] C. S. Lee, N. D. Jones, and A. M. Ben-Amram. The size-change principle for program termination. In ACM Symposium on Principles of Programming Languages (POPL’01), London, UK, January 2001. ACM Press.

[31] Z. Luo. ECC: An Extended Calculus of Constructions. PhD thesis, University of Edinburgh, 1990.

[32] R. Matthes. Extensions of System F by Iteration and Primitive Recursion on Monotone Inductive Types. PhD thesis, Ludwig-Maximilians-University, May 1998.

[33] C. McBride. Dependently Typed Functional Programs and their Proofs. PhD thesis, University of Edinburgh, 1999.

[34] N. P. Mendler. Recursive types and type constraints in second-order lambda calculus. In Proceedings of the Second Annual IEEE Symposium on Logic in Computer Science, Ithaca, N.Y., pages 30–36. IEEE Computer Society Press, 1987.

[35] N. P. Mendler. Inductive types and type constraints in the second-order lambda calculus. Annals of Pure and Applied Logic, 51(1–2):159–172, 1991.

[36] R. Milner. A theory of type polymorphism in programming. Journal of Computer and System Sciences, 17:348–375, Aug. 1978.

[37] L. Pareto. Types for Crash Prevention. PhD thesis, Chalmers University of Technology, 2000.

[38] M. Parigot. λμ-calculus: An algorithmic interpretation of classical natural deduction. In A. Voronkov, editor, Logic Programming and Automated Reasoning: Proc. of the International Conference LPAR’92, pages 190–201. Springer, Berlin, Heidelberg, 1992.

[39] F. Pfenning and C. Schürmann. System description: Twelf - a meta-logical framework for deductive systems. In H. Ganzinger, editor, Proceedings of the 16th International Conference on Automated Deduction (CADE-16), volume 1632 of Lecture Notes in Artificial Intelligence, pages 202–206, Trento, Italy, July 1999. Springer.

[40] B. Pientka. Termination and reduction checking for higher-order logic programs. In R. Goré, A. Leitsch, and T. Nipkow, editors, Automated Reasoning, First International Joint Conference, IJCAR 2001, volume 2083 of Lecture Notes in Artificial Intelligence, pages 401–415. Springer, 2001.

[41] B. C. Pierce. Types and Programming Languages. MIT Press, 2002.

[42] B. C. Pierce and D. N. Turner. Local type inference. In POPL 98: The 25TH ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, San Diego, California, 1998.

[43] R. Pollack. The Theory of LEGO. PhD thesis, University of Edinburgh, 1994.

[44] Z. Spławski and P. Urzyczyn. Type fixpoints: Iteration vs. recursion. SIGPLAN Notices, 34(9):102–113, 1999. Proceedings of the 1999 International Conference on Functional Programming (ICFP), Paris, France.

[45] A. J. Telford and D. A. Turner. Ensuring streams flow. In Algebraic Methodology and Software Technology (AMAST ’97), volume 1349 of Lecture Notes in Computer Science, pages 509–523. Springer, 1997.

[46] A. J. Telford and D. A. Turner. Ensuring termination in ESFP. Journal of Universal Computer Science, 6(4):474–488, Apr. 2000. Proceedings of BCTCS 15 (1999).

[47] T. Uustalu and V. Vene. Primitive (co)recursion and course-of-value (co)iteration, categorically. Informatica (Lithuanian Academy of Sciences), 10(1):5–26, 1999.

[48] C. Walther. Argument-Bounded Algorithms as a Basis for Automated Termination Proofs. In E. L. Lusk and R. A. Overbeek, editors, 9th International Conference on Automated Deduction, volume 310 of Lecture Notes in Computer Science, pages 602–621. Springer, 1988.

[49] A. K. Wright and M. Felleisen. A syntactic approach to type soundness. Information and Computation, 115(1):38–94, 1994.

[50] H. Xi. Dependent types for program termination verification. Journal of Higher-Order and Symbolic Computation, 15:91–131, Oct. 2002.

[51] J. Yang, G. Michaelson, and P. Trinder. Explaining polymorphic types. Computer Journal, 45(4):436–452, 2002.

Communicated by Zoltán Ésik and Igor Walukiewicz. May 14, 2004.