Implementing a Normalizer Using Sized Heterogeneous Types

ANDREAS ABEL∗

Institut für Informatik Ludwig-Maximilians-Universität München Oettingenstr. 67, D-80538 München, GERMANY

                           (e-mail: andreas.abel@ifi.lmu.de)

Abstract

In the simply-typed lambda-calculus, a hereditary substitution replaces a free variable in a normal form r by another normal form s of type a, removing freshly created redexes on the fly. It can be defined by lexicographic induction on a and r, thus, giving rise to a structurally recursive normalizer for the simply-typed lambda-calculus. We implement hereditary substitutions in a functional programming language with sized heterogeneous inductive types, F_{ω}, arriving at an interpreter whose termination can be tracked by the type system of its host programming language.

1 Introduction

An interpreter for a total programming language, i. e., a language in which only terminating programs can be written, will naturally terminate on all executions. However, this fact is sometimes hard to prove, as the abundant literature on normalization results shows. Often such a termination proof requires considerable insight into the semantics of the considered language. In this article, we consider a particularly easy example of a total language: the simply-typed lambda-calculus (STL). Its termination has been proven long ago and there are many different proofs. However, we will implement an interpreter for the STL whose termination can be checked automatically! As host programming language for the implementation we use F_{ω}, a polymorphic, purely functional language with sized types. Each well-typed F_{ω} -program is terminating (Abel, 2006b), hence, it is sufficient to show that the interpreter is a well-typed program. Provided the functions of the implementation are supplied with Haskell-style type signatures, well-typedness can be checked mechanically. Before we detail the structure of the interpreter, let us have a look at the idea behind F_{ω}.

Inductive types T can be expressed as the least solution of the recursive equation F X = X for some suitable monotone type function F; we write T = μF and say

∗ Research supported by the coordination action TYPES (510996) and thematic network Applied Semantics II (IST-2001-38957) of the European Union and the project Cover of the Swedish Foundation of Strategic Research (SSF).

that T is the least fixed-point of F. The least fixed point can be obtained in two ways: from above, using the theorem of Knaster and Tarski, and from below using transfinite iteration. Defining

\begin{aligned}μ^{0} & F & = & empty \\ μ^{α+1} & F & = & F (μ^{α}F) \\ μ^{λ} & F & = & ⋃_{α<λ} μ^{α}F, \end{aligned}

the least fixed-point of F is reached for some ordinal γ and we have F (μ^{γ}F) = μ^{γ}F. The construction of an inductive type from below is convenient if we want to define a function f : T → C over an inductive type; we can reason by transfinite induction that f is well-defined. This is especially the case if f defined by course-of-value recursion, i. e., refers in recursive calls only to smaller elements of the inductive type. Consider f = fix s being the fixed point of a functional s, i. e., fix s = s (fix s). Such functions can be introduced by the rule

\frac{s ∈ (μ^{α}F → C) → (μ^{α+1}F → C) for all α < β}{fix s ∈ μ^{β}F → C} .

The rule can be justified by transfinite induction up to β. Base case: since μ^{0}F is empty, fix s ∈ μ^{0}F → C trivially. For the step case, assume fix s ∈ μ^{α}F → C. By the premise of the rule, s (fix s) ∈ μ^{α+1}F → C, and by the fix-point equation, fix s ∈ μ^{α+1}F → C. Finally, for the limit case, assume fix s ∈ μ^{α}F → C for all α < λ and assume t ∈ μ^{λ}F. By definition of iteration at a limit, t ∈ μ^{α}F for some α < λ, hence fix s t ∈ C. Since t was arbitrary, fix s ∈ μ^{λ}F → C.

Up to now, we have considered the semantics of inductive types and the justification of semantical functions. Mendler (1987) first observed that by turning these semantical concepts into syntax,^{1} one gets a type system that accepts structurally recursive functions, hence, guarantees termination of well-typed programs. This idea has been taken up by Hughes, Pareto, and Sabry (1996), Giménez (1998), Amadio and Coupet-Grimal (1998), Barthe et al. (2004), Blanqui (2004) and myself (Abel, 2004a). In this article we use F_{ω}, an extension of the higher-order polymorphic lambda-calculus F_{ω} by sized inductive types and recursion on sizes. A sized inductive type μ^{a}F is the syntactic equivalent of an iteration stage μ^{α}F, only that a is now a syntactic ordinal expression and F is a syntactic type constructor whose monotonicity is established syntactically.

In this article, we give a non-trivial example of a structurally recursive function whose termination is automatically established using sized types: a β-normalizer for simply-typed λ-terms. At the heart of the normalizer are hereditary substitutions (Watkins et al., 2003): substitution of a normal form into another one, triggering new substitutions to remove freshly created redexes, until a normal form is returned. Surprisingly, this process can be formulated by a lexicographic recursion on the type of the substituted value and the normal form substituted into. We generalize them

1 Another example where semantics has been successfully turned into syntax is the monad. Invented by Moggi as a tool to reason about impure features, it has become a device to program imperatively in Haskell.

to hereditary simultaneous substitutions in order to handle de Bruijn-style λ-terms with static guarantee of well-scopedness. Such de Bruijn terms can be represented using a data structure of heterogeneous type (Bellegarde & Hook, 1994; Altenkirch & Reus, 1999; Bird & Paterson, 1999). In F_{ω}, heterogeneous types can be expressed by higher-kinded inductive types, i. e., type μ^{a}F where F is an operator on type constructors instead of just types. As a result, we obtain an implementation of a normalizer in F_{ω} whose termination and well-scopedness is ensured by type-checking in F_{ω}.

The remainder of this article is organized as follows. In Section 2, we briefly present system F_{ω}. Then, we specify and verify hereditary substitutions and normalization for simply-typed λ-terms in Section 3. In Section 4 we modify the specification to account for simultaneous hereditary substitutions. An implementation in F_{ω} is provided in Section 5. We conclude by discussing related and further work.

A preliminary version of this article has been presented at MSFP’06 (Abel, 2006a).

2 F_{ω}: A Polymorphic λ-calculus with Sized Types

In this section, we briefly introduce the most important concepts of F_{ω}. We assume some familiarity with system F_{ω} and inductive types.

Kinds. Kinds classify type constructors. In F_{ω}, one has the kind ∗ of types and function kinds κ → κ′ for type constructors. In F_{ω} we additionally have a kind ord for syntactic ordinals. Moreover, we distinguish type constructors by their variance: they can be covariant (monotonic), contravariant (antitonic), constant (both monoand antitonic) or mixed-variant (no monotonicity information). This is achieved by annotating function kinds with a polarity p.

p, q ::= ∘  mixed-variant (no monotonicity information)
| +  covariant (monotone)
| −  contravariant (antitone)
| ⊤  constant (both mono- and antitone)
κ ::= ∗  kind of types
| ord  kind of ordinals
| κ →^{p} κ′ kind of p-variant type constructors

The order on polarities is the reflexive-transitive closure of the axioms ∘ ≤ p and p ≤ ⊤. This means that the bigger a polarity, the more information it provides about the functions: just a function (∘), a mono-/antitone function (+/−), a constant function (⊤).

If one composes a function in κ_{1} →^{p} κ_{2} with a function in κ_{2} →^{q} κ_{3} one obtains a function in κ_{1} →^{pq} κ_{3}. For the associative and commutative polarity composition pq we have the laws ⊤p = ⊤, ∘p = ∘ (for p ≠ ⊤), +p = p, and −− = +. Inverse application p^{−1}q of a polarity p to a polarity q is defined as the solution of

∀q, q′. p^{−1}q ≤ q′ ⟺ q ≤ pq′.

In other words, the operations f(q) = p^{−1}q and g(q′) = pq′ form a Galois connection. It is not hard to see that the unique solution is given by the equations: +^{−1}q = q, −^{−1}q = −q, ⊤^{−1}q = ∘, ∘^{−1}∘ = ∘ and ∘^{−1}q = ⊤ (for q ≠ ∘).

Type constructors. Type constructors are expressions of a type-level λ-calculus, given by the following grammar.

A, B, F, G ::= C | X | λXF | F G

Z λY λXX Y is to be read as Z ((λY (λXX))Y); we use the dot “.” as an opening parenthesis which closes as far to the right as syntactically possible, e.g. λXλY. Y X means λXλY (Y X). The constants C are drawn from a signature Σ. It contains at least the following symbols together with their kinding:

1 : ∗  unit type
+ : ∗ →^{+} ∗ →^{+} ∗  disjoint sum
× : ∗ →^{+} ∗ →^{+} ∗  cartesian product
→ : ∗ →^{−} ∗ →^{+} ∗  function space
∀_{κ} : (κ →^{∘} ∗) →^{+} ∗  quantification
μ_{κ} : ord →^{+} (κ →^{+} κ) →^{+} κ  inductive constructors
s : ord →^{+} ord  successor of ordinal
∞ : ord  infinity ordinal.

We use +, ×, and → infix and write ∀X:κ.A for ∀_{κ}(λX.A). If clear from the context or inessential, we omit the kind annotation κ in ∀X:κ.A and μ_{κ}. We also write the first argument to μ_{κ}—the size index—superscript. For instance, μ^{α}(λX. 1 + A × X) denotes the lists of length < α containing elements of type A.

Kinding. A kinding context Δ is a finite map from type constructor variables X to pairs pκ of a polarity p and a kind κ. Inverse application p^{−1}Δ of a polarity p to a context Δ is defined by (p^{−1}Δ)(X) = p^{−1}(Δ(X)) (inverse-apply p to the polarity component of Δ(X)). The judgement Δ ⊢ F : κ assigns kind κ to constructor F in context Δ. It is given inductively by the following rules:

\frac{(C : κ) ∈ Σ}{Δ ⊢ C : κ}  \frac{Δ(X) = pκ p ≤ +}{Δ ⊢ X : κ}

\frac{Δ, X:pκ ⊢ F : κ′}{Δ ⊢ λXF : κ →^{p} κ′}  \frac{Δ ⊢ F : κ →^{p} κ′  p^{−1}Δ ⊢ G : κ}{Δ ⊢ F G : κ′}

The judgement X_{1} : p_{1}κ_{1}, …, X_{n} : p_{n}κ_{n} ⊢ F : κ means that λX_{1} … λX_{n}.F is a function which is p_{i}-variant in its ith argument. Hence, one can only extract variables of polarity + or ∘ from the context; X:−κ ⊢ X : κ would state that the identity function is antitone, which is certainly wrong. The application rule forms a function H′ = λX⃗. F′ X⃗ (G X⃗) from functions F′ = λX⃗. F and G′ = λX⃗. G. The variance p′_{i} of H′ in its ith argument depends on the variance p_{i} of F′ and q_{i} of G′ in this argument and the variance p of F′ in its last argument: p′_{i} is the infimum of p_{i} and pq_{i}, thus, p′_{i} = p_{i} if p_{i} ≤ pq_{i}, which is equivalent to p^{−1}p_{i} ≤ q_{i}. So the most liberal setting for q_{i} is p^{−1}p_{i}, which is what happens in the application rule.

Example 1 Using the rules, we can derive

λF λGλX. F X → G X : (∗ →^{∘} ∗) →^{−} (∗ →^{∘} ∗) →^{+} (∗ →^{∘} ∗).

Let Δ = F : −(∗ →^{∘} ∗), G: +(∗ →^{∘} ∗), X : ∘∗. We show Δ ⊢ F X → G X : ∗ which means that F X → G X is antitone in F and monotone in G. (It is mixed-variant in X.) The type-functions F and G are assumed to be mixed-variant. Observe that +^{−1}Δ = Δ and −^{−1}Δ = −Δ = F : +(∗ →^{∘} ∗), G : −(∗ →^{∘} ∗), X : ∘∗ and

∘^{−1}Δ = ∘^{−1}(−Δ) = F:⊤(∗ →^{∘} ∗), G:⊤(∗ →^{∘} ∗), X:∘∗.

{{Δ ⊢ → : ∗ →^{∘} ∗ →^{+} ∗  −^{−1}Δ ⊢ F X : ∗ \atop Δ ⊢ (→) (F X) : ∗ →^{+} ∗}  Δ ⊢ G X : ∗ \atop Δ ⊢ (→) (F X) (G X) : ∗}

Herein, we use the subderivations

\begin{matrix}{−^{−1}Δ(F) = +(∗ →^{∘} ∗) \atop −^{−1}Δ ⊢ F : ∗ →^{∘} ∗} & {∘^{−1}(−^{−1}Δ)(X) = ∘∗ \atop ∘^{−1}(−^{−1}Δ) ⊢ X : ∗} \\ −^{−1}Δ ⊢ F X : ∗ \end{matrix}

and

\begin{matrix}{Δ(G) = +(∗ →^{∘} ∗) \atop Δ ⊢ G : ∗ →^{∘} ∗} & {∘^{−1}Δ(X) = ∘∗ \atop ∘^{−1}Δ ⊢ X : ∗} \\ Δ ⊢ G X : ∗ \end{matrix}

Observe the polarity change of F from − to + as we step into the domain part of the arrow.

Example 2 Doubly negative counts as positive: λX.(X → 1) → 1 : ∗ →^{+} ∗.

Type constructor equality. The judgement Δ ⊢ F = F′ : κ states that the two constructors F, F′ which have kind κ in context Δ, are considered equal in F_{ω}. It is the least congruence over the following axioms:

\frac{Δ, X:pκ ⊢ F : κ′ p^{−1}Δ ⊢ G : κ}{Δ ⊢ (λXF) G = [G/X]F : κ′} \frac{Δ ⊢ F : κ →^{p} κ′}{Δ ⊢ λX. F X = F : κ →^{p} κ′} X ∉ FV(F)

\frac{Δ ⊢ F : κ →^{⊤} κ′ Δ ⊢ G : κ Δ ⊢ G′ : κ}{Δ ⊢ F G = F G′ : κ′}

\overline{Δ ⊢ s ∞ = ∞ : ord}  \frac{Δ ⊢ α : ord}{Δ ⊢ μ^{sα} = λF. F (μ^{α} F) : (∗ →^{+} ∗) →^{+} ∗}

The first rule encodes β- and the second η-equality. The third rule states that a constant function has the same value for all arguments. Let us look at the remaining two rules.

The normal forms of constructors α : ord that denote ordinal expressions are essentially following the grammar

α ::= ı | ∞ | s α

where we use ı and ȷ for variables of kind ord. Not captured by this grammar are neutral expressions like X G⃗; they stem from variables X : κ⃗ →^{p⃗} ord which are not forbidden, but of no use in the type system to follow. The ordinal expression ∞ denotes an ordinal large enough such that all inductive types have reached their fixed-point, thus, we have

F (μ^{∞}F) = μ^{∞}F.  (1)

The ordinal expression s α denotes the ordinal successor of α. We also write α + n as shorthand for s (… (s α)) (n successors). The closure ordinal ∞ is the largest size we need to consider, so we set

s ∞ = ∞.  (2)

In general, we have the type equation

μ^{α+1}F = F (μ^{α}F)  (3)

for sized inductive types, which reflects the semantical construction of inductive types given in the introduction. Equations (2) and (3) are axioms of our judgmental constructor equality Δ ⊢ F = F′ : κ, the equation (1) follows from the other two.

Subtyping Δ ⊢ F ≤ F′ : κ is induced by axioms expressing relations between ordinals and equipped with congruence rules that respect polarities.

\frac{Δ ⊢ α : ord}{Δ ⊢ α ≤ s α : ord}  \frac{Δ ⊢ α : ord}{Δ ⊢ α ≤ ∞ : ord}

\frac{Δ ⊢ F ≤ F′ : κ →^{p} κ′ p^{−1}Δ ⊢ G : κ}{Δ ⊢ F G ≤ F′ G : κ′}

\frac{Δ ⊢ F : κ →^{+} κ′  Δ ⊢ G ≤ G′ : κ}{Δ ⊢ F G ≤ F G′ : κ′}  \frac{Δ ⊢ F : κ →^{−} κ′  Δ ⊢ G′ ≤ G : κ}{Δ ⊢ F G ≤ F G′ : κ′}

Additionally, we have a congruence rule for λ-abstraction and rules for reflexivity, transitivity and antisymmetry. The rules for ordinal expressions are selfexplanatory; the third rule states that functions are compared point-wise; and the last two rules generate inequalities from mono-/antitone type functions.

Using the application rules and the polarized kind κ of constants C : κ from the signature, we can establish interesting subtyping relations: Since μ is covariant in its first argument, the rules allow us to derive

μ^{ı}F ≤ μ^{ı+1}F ≤ ⋯ ≤ μ^{∞}F.

This reflects the fact that by definition of the semantics, ordinals are upper bounds on size. For instance List^{α} A = μ^{α}(λX. 1 + A × X) contains lists of length < α, BTree^{α} A = μ^{α}(λX. 1 + A × X × X) binary trees of height < α, and Nat^{α} = μ^{α}(λX. 1 + X) natural numbers < α. Transfinite sizes are needed for infinitely branching trees, e. g., μ^{α}(λX. 1 + Nat^{∞} × X + (Nat^{∞} → X)).

Programs (terms). F_{ω} is a purely functional language with categorical datatypes^{2} and recursion. Programs are given by the following grammar.

e, f ::= x | λxe | f e  λ-calculus
| ⟨⟩  inhabitant of type 1
| ⟨e_{1}, e_{2}⟩ | fst e | snd e  pairing and projections
| inl e | inr e | case e f_{1} f_{2}  injections into disjoint sum, case distinction
| fix f  recursion.

Typing. Wellformed typing contexts are generated by the rules

\overline{⋄ cxt}  \frac{Γ cxt}{Γ, X:∘κ cxt}  \frac{Γ cxt Γ ⊢ A : ∗}{Γ, x:A cxt}.

Typing contexts can always be viewed as kinding contexts, forgetting the bindings for the term variables. The typing rules for the λ-calculus part are inherited from Curry-style system F_{ω}.

\frac{(x:A) ∈ Γ Γ cxt}{Γ ⊢ x : A}  \frac{Γ, x:A ⊢ e : B}{Γ ⊢ λxe : A → B}  \frac{Γ ⊢ f : A → B  Γ ⊢ e : A}{Γ ⊢ f e : B}

\frac{Γ, X:∘κ ⊢ e : F X}{Γ ⊢ e : ∀_{κ}F} X ∉ FV(F)  \frac{Γ ⊢ e : ∀_{κ} F  Γ ⊢ G : κ}{Γ ⊢ e : F G}

\frac{Γ ⊢ e : A Γ ⊢ A ≤ B : ∗}{Γ ⊢ e : B}

Unit type, cartesian product and disjoint sum are introduced and eliminated using the respective terms given in the grammar (we omit the obvious typing rules). Inductive types can be introduced and eliminated using the type equations. For instance, the empty list is typed as

inl ⟨⟩ : 1 + A × List^{ı}A = List^{ı+1}A.

The central feature of F_{ω} is the type-based recursion rule which has been semantically motivated in the introduction:

\frac{Γ ⊢ α : ord Γ ⊢ G : ord →^{+} ∗ Γ ⊢ f : ∀ı:ord. (∀X⃗. μ^{ı}F X⃗ → G ı) → ∀X⃗. μ^{ı+1}F X⃗ → G (ı + 1)}{Γ ⊢ fix f : ∀X⃗. μ^{α}F X⃗ → G α}

2 Categorical datatypes do not contain names, just structure. Constructors of data structures are derived from the program primitives. This is in opposition to nominal languages where data constructors are themselves primitives (e. g., in Haskell).

In comparison with the semantic rule given in the introduction, we now allow polymorphic recursion, and the result type G α may mention the ordinal index α, but only positively (Barthe et al., 2004; Abel, 2004a; Blanqui, 2004). Note that the size index α in the conclusion can be arbitrary. (Alternatively, one could formulate the rule with conclusion fix f : ∀ı∀X⃗. μ^{ı}F X⃗ → G ı. This size-polymorphic function can then be instantiated to any size α.)

Typing is not decidable, since F_{ω} features impredicative polymorphism and polymorphic recursion, which are both undecidable by themselves already. However undecidability may not be a problem in practice, as the experience with Haskell shows. There, it is usually sufficient that the programmer provides the types of all recursive functions. Type information is then propagated using heuristics like bidirectional type-checking. In previous work (Abel, 2004a) I have described a bidirectional type-checking algorithm for a simply-typed language with sized types, and I expect that sized types can be integrated into Haskell type-checking without causing new undecidability issues.

We illustrate the potential of type-based termination à la F_{ω} with the following example.

Example 3 (Quicksort) F_{ω} accepts the usual functional quicksort as terminating. The type system can track the size of the output of filter f l (the list of elements of l for which f holds) which is at most the size of l.

filter : ∀A. (A → Bool) → ∀ı. List^{ı}A → List^{ı} A

filter f = fix λfiltλl. case l (λ_. inl⟨⟩) (λp. if f (fst p) then inr ⟨fst p, filt (snd p)⟩ else filt (snd p))

quicksort : ∀ı. List^{ı} Int → List^{∞} Int

quicksort = fix λquicksortλl. case l (λ_. inl⟨⟩) (λp. append (quicksort (filter (≤ (fst p)) (snd p))) (inr ⟨fst p, quicksort (filter (> (fst p)) (snd p))⟩))

Using the size bound on filtered lists, quicksort is well-typed, hence, terminating.

In the next section, we start developing an interpreter for an object language, in our case, the simply-typed λ-calculus, which we will later implement in our meta language, F_{ω}.

3 A Terminating Normalizer for Simply-Typed Lambda-Terms

In this section, we formally define hereditary substitution for the simply-typed λcalculus. We show its termination, soundness, and completeness.

Types and terms. The following grammars introduce our object language, the simply-typed λ-calculus. To distinguish it from our meta-language, F_{ω}, we use lower case letters for the types.

a, b, c ::= o | a → b  simple types
r, s, t ::= x | λx:a.t | r s simply-typed terms
n  ::= x | n s  neutral terms (required in Section 3.3)
Γ  ::= ⋄ | Γ, x:a  typing contexts

Ordinary (capture-avoiding) substitution [s/x]t of s for x in t, the set FV(t) of free variables of term t, and β-equality t =_{β} t′ of terms t, t′ shall be defined as usual, as well as the typing judgement Γ ⊢ t : a. We need these notions to prove correctness of the normalization algorithm which we are going to implement in F_{ω} .

Let |a| ∈ ℕ denote a measure on types with |b| < |b → c| and |c| ≤ |b → c|. There are three natural candidates for this measure:

|o|  |a → b|  measure
1  |a| + |b| + 1  tree size
1  max(|a|, |b|) + 1 tree height, or structural measure
0  max(|a| + 1, |b|) order of the type

The last two can be expressed in F_{ω}, see Section 5.

3.1 Hereditary substitution

We define a 4-ary function [s/x]^{a}t, called hereditary substitution, which returns a result r̂. A result is either just a term r or a term annotated with a type, written r^{c}. The intention is that if s and t are β-normal and well-typed terms and a is the type of s and x, then the result will also be β-normal (and well-typed). Our definition is a simplification of Watkins et al.’s (2003) hereditary substitutions for terms of the concurrent logical framework CLF. Implicitly, hereditary substitutions are present already in Joachimski and Matthes’ (2003) normalization proof for the simply-typed λ-calculus. This proof is similar to normalization proofs before Tait (1967), e. g., Gentzen (1935)^{3}, Turing, Prawitz (1965)^{4}, and others.

Let us first introduce some overloaded notation on results r̂. The operation \underline{r̂} discards the type annotation on the result if present, i. e., \underline{r^{a}} := r and \underline{r} := r. This operation is to be applied implicitly when the context demands it. For example, application of two results r̂ and ŝ implicitly discards the type annotations: r̂ŝ:= \underline{r̂}\underline{ŝ}. Similarly for abstraction: λx: a.r̂ := λx: a.\underline{r̂}. Finally, reannotation r̂^{a} := (\underline{r̂})^{a} puts a fresh type annotation a onto a result.

Using these notations, we can compactly define the process [s/x]^{a}t = r̂ of hereditarily substituting s of type a for variable x in t. The type a should be viewed as fuel which is spent on triggering new hereditary substitutions. If the result r̂ is r^{c}, then the process returns fuel c. If the result is simply a term r, no fuel is returned,

3 pp. 197ff 4 Thm. III.2

i. e., it has all been spent or wasted.

[s/x]^{a}x  = s^{a}
[s/x]^{a}y = y if x ≠ y
[s/x]^{a}(λy:b.r) = λy:b. [s/x]^{a}r where y fresh for s, x
[s/x]^{a}(t u)  = ([û/y]^{b}r′)^{c}  if t̂= (λy:b′.r′)^{b→c}
t̂û  otherwise
where t̂ = [s/x]^{a}t
û = [s/x]^{a}u

In lines 2, 3, and 5, all fuel is wasted. In line 1, all fuel is returned. And in line 4, the fuel (b → c) returned by the hereditary substitution into t is partially spent (b) on a new substitution, and partially returned (c).

Example 4 Let us demonstrate hereditary substitution for a few cases. We will write λxt instead of λx:a. t if the type a of the abstracted variable does not matter for our purposes.

1. Different head variable (x ≠ y):

[s/x]^{a}(y t_{1} … t_{n}) = y ([s/x]^{a}t_{1}) … ([s/x]^{a}t_{n})

Hereditarily substituting for x into a term y t_{1} … t_{n} with a different head variable behaves on the surface level like ordinary substitution. (In the subterms t_{i} something more interesting might happen, of course.)

2. Same head variable, out of fuel: creates redexes.

[λy. y λzz/x]^{o}(x λff) = (λy. y λzz) λff.

We have [λy. y λzz/x]^{o}x = (λy. y λzz)^{o}, and since o is a base type, the application of the result to λff does not trigger a new substitution.

3. Same head variable, some fuel left:

[λy. y λzz/x]^{o→o}(x λff) = (λff) λzz.

This time, executing the hereditary substitution for x in x returns o → o fuel, so a new hereditary substitution [λff/y]^{o}(y λzz) is triggered. However, now we run out of fuel, and one redex remains.

4. Same head variable, enough fuel:

[λy. y λzz/x]^{(o→o)→o}(x λff) = (λzz)^{o}.

Finally, we reach a normal form, since the hereditary substitution for y returns fuel o → o, so a third and last hereditary substitution, [λzz/f]^{o}f is triggered.

5. Substituting into redexes:

[s/x]^{a}((λyt) u) = (λy. [s/x]^{a}t)([s/x]^{a}u)

Already present redexes are preserved by hereditary substitution, only new redexes which are created by the substitution process can be eliminated. Similarly, redexes in s are kept:

[(λxr) s/y]^{a}(y z) = (λxr) s z

In the following we will prove termination of hereditary substitution and soundness, i. e., the hereditary substitution [s/x]^{a}t returns a term with the same meaning as ordinary substitution [s/x]t. A necessary condition for termination is that driving does not create fuel, which we can more formally express as:

Lemma 1 (Invariant) If [s/x]^{a}t = r^{c} then |c| ≤ |a|.

Proof By induction on t. There are only two cases which return an annotated term:

• [s/x]^{a}x = s^{a}. Trivially |a| ≤ |a|.

• [s/x]^{a}(t u) = ([û/y]^{b}r′)^{c} where [s/x]^{a}t = (λy:b′.r′)^{b→c}. By induction hypothesis, |b → c| ≤ |a|. This proves the invariant, since |c| ≤ |b → c| by definition of the measure | · |.

This entails termination, because whenever we want to execute a new hereditary substitution, we need to have b → c fuel left, from which we take b for the new substitution and keep the c for further substitutions which may arise.

Lemma 2 (Termination and soundness) [s/x]^{a}t =_{β} [s/x]t for all a, s, x, t.

Remark 1 The statement “[s/x]^{a}t =_{β} some term” entails the statement “[s/x]^{a}t is defined” (termination).

Proof By lexicographic induction on (|a|, t). In the case of application, [s/x]^{a}(t u), by induction hypothesis, t̂ = [s/x]^{a}t and û = [s/x]^{a}u are both defined. We consider the subcase t̂ = (λy : b′.r′)^{b→c}. Using the invariant, we infer |b| < |b → c| ≤ |a|. Hence, we can again apply the induction hypothesis to infer that [û/y]^{b}r′ terminates, thus, by definition, also [s/x]^{a}(t u). Soundness holds by the induction hypotheses, since (λy:b′.r′) \underline{û} =_{β} [\underline{û}/y]r′.

In Sec. 3.3 we will show that hereditary substitution is complete, i. e., returns a normal form, if run on normal forms with sufficient fuel. For well-typed terms, the type of the substituted variable provides sufficient fuel. For non-well-typed terms, no amount of fuel might be sufficient; consider [λx. x x/x]^{a}(x x), which has no normal form.

3.2 Full Normalization

We define a function [[t]] which β-normalizes term t, provided it is well-typed. Even if it is not well-typed, the normalizer terminates and returns a term which is β-equal to the input.

[[x]]  = x
[[λx:a.r]] = λx:a. [[r]]
[[r s]]  = [[[s]]/x]^{a}t if [[r]] = λx:a.t
[[r]] [[s]]  otherwise

The normalizer is structurally recursive in its argument, thus, once we have established termination of hereditary substitution, its termination is trivial.

Lemma 3 (Termination and soundness) [[t]] =_{β} t for all t.

Proof By induction on t, using termination and soundness of hereditary substitution.

Example 5 (Behavior of normalizer)

[[(λx:o → o.λy:b. x y) (λz:a.z)]] = λy:b.y

Hereditarily substituting (λz : a.z) at function type o → o for x into x y triggers another substitution of y for z in z. However, if variable x is annotated with base type o only, this second substitution is not invoked and we get a non-normal result:

[[(λx:o.λy:b. x y) (λz:a.z)]] = λy:b. (λz:a.z) y

Evaluation of terms that are diverging under β-reduction also stops, e.g.,

[[(λx:o. x x) (λx:o. x x)]] = (λx:o. x x) (λx:o. x x).

3.3 Completeness of the Normalizer

In the following we show that the normalizer actually computes normal forms for well-typed terms.

Typed normal forms. We introduce a judgement Γ ⊢ t ⇓ a which expresses that t is a β-normal form of type a in context Γ.

\frac{(x:a) ∈ Γ}{Γ ⊢ x ⇓ a}  \frac{Γ ⊢ n ⇓ a → b Γ ⊢ s ⇓ a}{Γ ⊢ n s ⇓ b} n not a λ  \frac{Γ, x:a ⊢ r ⇓ b}{Γ ⊢ λx:a.r ⇓ a → b}

Note that in the second rule, the head n of the application n s is a neutral term, in particular, not an abstraction.

Lemma 4 (Completeness of hereditary substitution) Let Γ ⊢ s ⇓ a and Γ, x:a ⊢ t ⇓ c. Then exists an r with the following properties: if t is neutral then either [s/x]^{a}t = r^{c}, or r is also neutral and [s/x]^{a}t = r. Otherwise, if t is not neutral, [s/x]^{a}t = r. In all cases, Γ ⊢ r ⇓ c.

Proof By lexicographic induction on (|a|, t). We consider the interesting case t = n u:

\frac{Γ, x:a ⊢ n ⇓ b → c Γ, x:a ⊢ u ⇓ b}{Γ, x:a ⊢ n u ⇓ c}

Let û = [s/x]^{a}u. If [s/x]^{a}n = r̂ and \underline{r̂} is neutral, then Γ ⊢ r̂û : c follows easily by induction hypothesis. Otherwise, [s/x]^{a}n = (λy : b.r′)^{b→c}. By the invariant, |b| < |b → c| ≤ a, and we can apply the induction hypothesis to infer Γ ⊢ [û/y]^{b}r′ ⇓ c, which is by definition equivalent to Γ ⊢ [s/x]^{a}(n u) ⇓ c.

Theorem 1 (Completeness of the normalizer)

If Γ ⊢ t : a then Γ ⊢ [[t]] ⇓ a.

Proof By induction on t, using the previous lemma in case of a β-redex.

4 Adaptation to Simultaneous Substitutions

Our aim is to implement the normalizer of the last section for a representation of terms using de Bruijn indices. Following Bellegarde and Hook (Bellegarde & Hook, 1994), Altenkirch and Reus (1999) and Bird and Paterson (1999), untyped λ-terms over the set of free variables A can be implemented by a heterogeneous datatype Tm A with the three constructors:

var : ∀A. A → Tm A
abs : ∀A. Tm (1 + A) → Tm A
app : ∀A. Tm A → Tm A → Tm A

The second constructor, abs, expects a term with one more free variable (1 + A) and binds this variable such that the result will only have free variables in A.

In this representation of de Bruijn terms, which uses types A as indices of the family Tm A, substitution [s/x]t for a single variable x is most elegantly obtained as an instance of simultaneous substitution tρ for all free variables in t: if t has type Tm A and ρ has type A → Tm B, the result tρ of the substitution has type Tm B.^{5}

Hereditary simultaneous substitution. A valuation ρ is a function from variables to results r̂. Let the update ρ[x ↦ r̂] of valuation ρ in x by result r̂ be defined as usual:

\begin{aligned}ρ[x ↦ r̂](x) & = & r̂ \\ ρ[x ↦ r̂](y) & = & ρ(y) & if x ≠ y \end{aligned}

The singleton valuation which maps x to r̂ and all other variables to themselves shall be denoted by (x ↦ r̂). A single substitution [s/x]t can be implemented using the simultaneous substitution t(x ↦ s) with a singleton valuation.

The hereditary simultaneous substitution t!ρ returns a result r̂ and is defined by the following equations:

x!ρ = ρ(x)
(λy:b.r)!ρ = λy:b. (r!ρ[y ↦ y]) where y fresh for any ρ(x) with x ∈ FV(λyr)
(t u)!ρ = (r′!(y ↦ û^{b}))^{c}  if t̂= (λy:b′.r′)^{b→c}
t̂û  otherwise
where t̂ = t!ρ
û = u!ρ

A closer look reveals that we use only three operations on valuations: lookup, ρ(x), lifting, ρ[y ↦ y] for y fresh, and creation of a singleton valuation, (y ↦ û^{b}). In

5 The type constructor Tm forms a Kleisli triple with unit var and simultaneous substitution as the bind-operation.

particular, if t!ρ is invoked with a singleton valuation ρ, all recursive calls will also just involve a singleton valuation. We could therefore restrict ourselves to singleton valuations (see also Appendix A). However, for termination, a weaker requirement is sufficient:

In the following we consider only valuations ρ where ρ(x) = r^{a} for only finitely many variables x. For such valuations,

|ρ| := max{|a| | ρ(x) = r^{a}}

is a well-defined measure, |ρ| ∈ ℕ. Trivially, |(y ↦ s^{a})| = |a| for a singleton valuation.

Hereditary simultaneous substitutions always terminate, and the respective proof for hereditary singleton substitutions can be adopted:

Lemma 5 (Invariant) If t!ρ = r^{c}, then |c| ≤ |ρ|.

Proof By induction on t.

Lemma 6 (Termination and soundness of hereditary simultaneous substitutions) For all terms r and valuations ρ such that |ρ| exists, we have r!ρ =_{β} rρ.

Proof By lexicographic induction on (|ρ|, r). In case r = t u and t̂ = t!ρ = (λy: b′.r′)^{b→c}, use the invariant to establish |(y ↦ û^{b})| = |b| < |b → c| ≤ |ρ| and apply the induction hypothesis.

By setting [s/x]^{a}t := t!(x ↦ s^{a}) we can reuse the code for the normalization function [[r]] from the last section.

5 Implementation in F_{ω}

In this section, we implement hereditary substitutions in F_{ω}. As a result, we will get a normalizer whose termination is certified by the type system of F_{ω}.

Simple types over a single base type o can be defined as follows in F_{ω}:

Ty : ord →^{+} ∗
Ty := λı. μ_{∗}^{ı}λX. 1 + X × X
o : ∀ı. Ty^{ı+1}
o := inl ⟨⟩
arr : ∀ı. Ty^{ı} → Ty^{ı} → Ty^{ı+1}
arr := λaλb. inr ⟨a, b⟩

The definition of Ty forces the types of the constructors o and arr. The size index ı in Ty^{ı} implements the structural measure on simple types. The requirements |b| < |arr b c| and |c| ≤ |arr b c| hold since b, c : Ty^{ı} implies arr b c : Ty^{ı+1}.

Remark 2 If we choose to implement types as (naked) rose trees, Ty^{ı} = μ^{ı}λX. List^{∞}X, the constructors o and arr, defined as above, now receive the typing:

o : ∀ı. Ty^{ı+1}
arr : ∀ı. Ty^{ı} → Ty^{ı+1} → Ty^{ı+1}.

To see this, observe that Ty^{ı+1} = List^{∞}Ty^{ı} and o = nil and arr = cons. The resulting measure is an upper bound on the order of a type and fulfills the requirements as well. However, I do not see how one could code Ty^{ı} such that ı would be an upper bound on the number of arr-nodes.

5.1 De Bruijn Terms as a Sized Heterogeneous Data Type

We can express the sized type constructor Tm for de Bruijn terms by a least fixed point of kind ∗ →^{+} ∗.

Tm : ord →^{+} ∗ →^{+} ∗
Tm := λı. μ^{ı}_{∗→^{+}∗}λXλA. A + (X A × X A + Ty^{∞} × X (1 + A))
var : ∀ı∀A. A → Tm^{ı+1} A
var := λx. inl x
app : ∀ı∀A. Tm^{ı} A → Tm^{ı} A → Tm^{ı+1} A
app := λrλs. inr (inl ⟨r, s⟩)
abs : ∀ı∀A. Ty^{∞} → Tm^{ı} (1 + A) → Tm^{ı+1} A
abs := λaλr. inr (inr ⟨a, r⟩)

Note that the first argument to abs is the object-level type of the abstraction: abs a r represents λx:a. r.

Lifting the free de Bruijn indices of a term t by one is implemented as map_{Tm} inr where map_{Tm} is the functorial action of Tm.

map_{Tm}  : ∀ı∀A∀B. (A → B) → Tm^{ı}A → Tm^{ı}B
map_{Tm}  := λfλr. map′_{Tm} r f
map′_{Tm}  : ∀ı∀A. Tm^{ı}A → ∀B. (A → B) → Tm^{ı}B
map′_{Tm}  := fix λmap′λtλf. match t with
var x ↦ var (f x)
app r s ↦ app (map′ r f) (map′ s f)
abs a r ↦ abs a (map′ r (map_{Maybe} f))
map_{Maybe} : ∀A∀B. (A → B) → (1 + A → 1 + B)
map_{Maybe} := λfλt. match t with
inl ⟨⟩ ↦ inl ⟨⟩
inr x ↦ inr (f x)
lift_{Tm}  : ∀ı∀A. Tm^{ı}A → Tm^{ı}(1 + A)
lift_{Tm}  := map_{Tm} inr

The call map_{Tm} f t renames all free variables in t according to f; the structure of t remains unchanged, which is partially reflected in the type of map_{Tm}: it expresses that the output term is not larger than the input term.

5.2 Implementation of Hereditary Simultaneous Substitution

The result of a hereditary substitution of a normal term into a neutral term is either a neutral term r or a normal term r plus (its) type a, which we have written as r^{a}. We encode these alternatives in the type Res^{ı} A, where ı is an upper bound on the size of the type a and A is the set of free variables that might occur in the result term r. We define two constructors: ne_{Res} r for the first alternative, and nf_{Res} r a for the second alternative.

Res : ord →^{+} ∗ →^{+} ∗
Res := λıλA. Tm^{∞} A × (1 + Ty^{ı})
ne_{Res} : ∀ı. Tm^{∞} A → Res^{ı} A
ne_{Res} := λr. ⟨r, inl ⟨⟩⟩
nf_{Res} : ∀ı. Tm^{∞} A → Ty^{ı} → Res^{ı} A
nf_{Res} := λrλa. ⟨r, inr a⟩

The destructor tm just extracts the term component. The function lift_{Res} lifts the free variables in a result term by one.

tm  : ∀ı∀A. Res^{ı}A → Tm^{∞} A
tm  := λ⟨r, a⟩. r
lift_{Res} : ∀ı∀A. Res^{ı} A → Res^{ı} (1 + A)
lift_{Res} := λ⟨r, a⟩. ⟨lift_{Tm} r, a⟩

Finally, we can mimic all term constructors on Res. They should all discard the type component, if present. This is why the size index ı on the result of these operations is arbitrarily small:

var_{Res} : ∀ı∀A. A → Res^{ı} A
var_{Res} := λa. ne_{Res} (var a)
abs_{Res} : ∀ı∀A. Ty^{∞} → Res^{∞}(1 + A) → Res^{ı}A
abs_{Res} := λaλr. ne_{Res} (abs a (tm r))
app_{Res} : ∀A. Res^{∞} A → Res^{∞} A → Res^{ı} A
app_{Res} := λtλu. ne_{Res} (app (tm t) (tm u))

We represent valuations ρ which map all variables in A to a result with variables in B by the sized type Val^{ı} A B. The size index ı is an upper bound for |ρ|.

Val  : ord →^{+} ∗ →^{−} ∗ →^{+} ∗
Val  := λıλAλB. A → Res^{ı}B
lookup_{Val} : ∀ı∀A∀B. Val^{ı} A B → A → Res^{ı}B
lookup_{Val} := λρλx. ρ x
sg_{Val}  : ∀ı∀A. Tm^{∞}A → Ty^{ı} → Val^{ı} (1 + A) A
sg_{Val}  := λsλaλmy. match my with
inl ⟨⟩ ↦ nf_{Res} s a
inr y ↦ var_{Res} y
lift_{Val}  : ∀ı∀A∀B. Val^{ı} A B → Val^{ı} (1 + A) (1 + B)
lift_{Val}  := λρλmx. match mx with
inl ⟨⟩ ↦ var_{Res} (inl ⟨⟩)
inr x ↦ lift_{Res} (ρ x)

The expression sg_{Val} s a : Val^{ı} (1 + A) A corresponds to the singleton valuation (x ↦ s^{a}); it generates a valuation which maps the variable x in 1 to nf_{Res} s a and the variables y in A to ne_{Res} (var y). The extension ρ[y ↦ y] of a valuation ρ is implemented by lift_{Val} ρ and lookup of variable x in ρ by lookup_{Val}. Other implementations of valuations are possible, see Appendix A.

For implementing hereditary substitutions, we have to take into account the limitations of recursion in F_{ω}. Lexicographic recursion on type and term, Ty^{ı} × Tm^{ȷ} A, needs to be split up into an outer recursion on Ty^{ı} and an inner recursion on Tm^{ȷ}.

Thus, we define hereditary substitution [s/x]^{a}r by a function subst a s r recursive in a. This outer function calls an inner function simsubst r (sg_{Val} a s) recursive in r, which performs hereditary simultaneous substitutions in r, starting with the singleton valuation (x ↦ s^{a}). In one case, the inner function calls the outer function, albeit with a smaller type b. That b is in fact smaller than a is tracked by the type system.

subst : ∀ı. Ty^{ı} → ∀A. Tm^{∞} A → Tm^{∞}(1 + A) → Tm^{∞} A
subst := fix λsubstλaλsλt. tm (simsubst t (sg_{Val} s a))

where

simsubst : ∀ȷ. ∀A∀B. Tm^{ȷ}A → Val^{ı+1} A B → Res^{ı+1}B
simsubst := fix λsimsubstλrλρ. match r with
var x ↦ lookup_{Val} ρ x
abs b t ↦ abs_{Res} b (simsubst t (lift_{Val} ρ))
app t u ↦ let t̂ = simsubst t ρ û = simsubst u ρ
in match t̂with
nf_{Res} (abs b′ r′) (arr b c) ↦ nf_{Res} (subst b (tm û) r′) c
_↦ app_{Res} t̂û

The outer function is defined by induction on size ı; we have the following important types of bound variables:

subst : Ty^{ı} → ∀A. Tm^{∞} A → Tm^{∞}(1 + A) → Tm^{∞} A
a  : Ty^{ı+1}

This explains why in the type of the inner function, we have used size index ı + 1 for Val and Res. The inner function is defined by induction on ȷ. It is important that lift_{Val} does not touch the size argument to Val. Also, abs_{Res} and app_{Res} can return results Res with any size argument, thus, ı + 1 is fine. In lookup_{Val} ρ x, the size index on Val is returned as the size of Res. Finally, when we match t̂: Res^{ı+1} B as the result of a recursive call to simsubst, the expression arr b c has sized type Ty^{ı+1}, hence, b : Ty^{ı}, and the recursive call to subst is legal. Since c : Ty^{ı} ≤ Ty^{ı+1} by subtyping, the result nf_{Res} (…) c is well-typed.

The normalizer [[−]] can now be implemented straightforwardly. Its termination is guaranteed by sized types!

norm : ∀ı∀A. Tm^{ı}A → Tm^{∞}A
norm := fix λnormλt. match t with
var x ↦ var x
abs a r ↦ abs a (norm r)
app r s ↦ let r′ = norm r s′ = norm s
in match r′ with abs a t′ ↦ subst a s′ t′ _↦ app r′ s′

6 Discussion and Related Work

We have seen an interesting example for certifying termination with sized types. One may wonder, is this normalizer extensible beyond the simply typed lambdacalculus, and are sized types strictly necessary to implement terminating hereditary substitutions? The answer to the first question is, yes, but not substantially. One can add product and sum types and probably control operators such as the μ in the λμ-calculus (David & Nour, 2005). Yet System T is clearly out of reach, since the termination orderings are well beyond lexicographic. With respect to the second question: one can obtain a structurally recursive implementation of hereditary substitutions if one uses a spine representation of λ-terms: r, s, t ::= x t⃗ | λx: a. t | r s. This was pointed out to me by one of the referees. However, as we have seen, sized types offer more flexibility and means to abstract: we can always replace a piece of code by something different with the same type and maintain termination. For instance, we have factored out the implementation of valuations from the implementation of simultaneous substitutions, so now we can choose a completely different representation.

Terminating normalizers for object languages like System T or System F (Altenkirch, 1993) can be implemented in dependently typed meta-languages of appropriate strength, like Coq (2007) which is based on a type theory called the Calculus of Inductive Constructions. There have been proposals to integrate sized types into the type theory (Barthe et al., 2006; Blanqui, 2005) to check termination of recursive definitions behind the scenes. In F_{ω}, sizes are first-class, i. e., one can speak about non-size-increasing functions like filter and pass them as parameters to other functions. Of course, dependent type theories already feature indexed types, thus, one can simulate sized types to a certain extent. E. g., sized types requiring only sizes < ω can be simulated by an inductive family indexed by a natural number, and size ω through an existential type. However, subtyping sized types is then not available, one has to insert explicit coercions instead, and the conveniences of a size ∞ are lost.^{6} A lightweight integration of sized types into dependent types is still a topic of research.

We continue with a review of some related work.

Type-based termination and sized types. Mendler (1991) first devised a typing rule for general recursive programs that would single out the ones that are iterative— like fold for lists. Mendler’s system was extended by Giménez (1998) and Barthe et al. (2004; 2005) to account for course-of-value recursion—covering functions like quicksort. I have explored how the type of a recursive function may depend on the size index (Abel, 2006c)—now functions like breadth-first traversal are recognized as terminating by the type system. In my thesis (Abel, 2006b), I cover also heterogeneous types like this article’s Tm. Blanqui (2004; 2005) extended type-based termination to dependent types and rewriting.

Independently of these “type-theoretic” developments, Hughes, Pareto, and Sabry (Hughes et al., 1996; Pareto, 2000) have explored sized types for preventing crashes of functional programs. They arrived at a similar rule for type-based terminating recursion.

De Bruijn representation by a heterogeneous type. Since the 1960s it is known that simultaneous substitution can be viewed as the bind operation of a suitable monad (Lane, 1971; Manes, 1976). For terms with binders, the idea was taken up by Bird and Paterson (1999) as a case study for heterogeneous types in Haskell. Altenkirch and Reus (1999) implement simultaneous substitutions for de Bruijn terms in a more type-theoretic setting; they carry out the renaming—performed in substitution under a binder—also by an invocation of substitution. Thus, termination of substitution becomes more complicated; they justify it by a lexicographic argument. McBride (2006) stratifies this situation by exhibiting a common scheme with substitution and renaming as special instances. This scheme is again structurally recursive. McBride considers the object language of simply-typed terms in a dependently typed meta language; this way, he even establishes that substitution and renaming are type-preserving.

Adams (2006) has carried out metatheory of pure type systems using de Bruijn representations as a heterogeneous type. He found that he had to pass from smallstep statements, which speak about a single variable, e.g., a single substitution,

6 Implementing arr′ : Ty^{∞} → Ty^{∞} → Ty^{∞} as arr′ : (∃ı : ℕ.Ty^{ı}) → (∃ı : ℕ.Ty^{ı}) → (∃ı : ℕ.Ty^{ı}) involves computation of a maximum.

to big-step statements, that take all variables into account at the same time, like simultaneous substitution. We can only confirm his findings.

Arithmetic normalization proofs and functions. Joachimski and Matthes (2003) present strong and weak normalization proofs of the simply-typed λ-calculus using a lexicographic induction on types and derivations, similar to the one we have given in Section 3. They hand-extract a general recursive normalization algorithm which may diverge on ill-typed input. Berghofer (2006) implements the weak normalization proof in Isabelle and automatically extracts a normalizer, being much more complicated and keeping some intermediate data structures. I have implemented a similar proof in Twelf (Abel, 2004b). The termination checker of Twelf is capable to certify termination of the normalization proof, if viewed as a recursive function.

Watkins et al. (2003) define hereditary substitutions for terms of the logical framework LF, and its extensions to linearity and concurrency. These substitutions proved to be terminating by a lexicographic induction on type and term—as in this article. Hereditary substitutions enable us to specify a framework which only treats canonical forms (β-normal η-long objects), thus, simplifying its metatheory considerably; see also the tutorial on LF by Harper and Licata (2007).

7 Conclusion

We have presented F_{ω}, a pure polymorphic programming language with sized heterogeneous inductive types and type-based termination. As a non-trivial example, we have implemented a normalizer for simply-typed λ-terms in F_{ω}. The termination of the normalizer is statically ensured in F_{ω}. Additionally, the normalizer is well-scoped, by virtue of an implementation of λ-terms using a heterogeneous type.

One can go further and aim for a normalizer for statically well-typed λ-terms, “well-typed” referring here to typing in the object language of simple types. McBride (2006) has done a first step and implemented type-preserving renaming and substitution for the object language using a dependently-typed meta language. Pursuing this approach, one can modify the normalizer such that it does not any more explicitly manipulate object-level types but considers only object-level terms. The object-level types are then visible only in the meta-level typing of the normalizer. The normalizer, viewed purely operationally, has the possibility to diverge on illtyped terms, but the static well-typedness condition guarantees its termination for all actual inputs.^{7}

Acknowledgments. Thanks to the anonymous referees for their careful reading and their humorous, helpful, and encouraging comments.

7 One referee has sent me Agda code which implements the type-preserving normalizer I describe here.

A Variation

In this section, we consider an alternative representation of a single substitution for de Bruijn terms. It will turn out that the alternative is not so different to what we had already; substitution [s/i]t of a term s for a free de Bruijn index i in t is just an instance of simultaneous substitution tρ, using a special representation of the valuation ρ.

Consider λ-terms as given by the grammar Tm ∋ r, s, t ::= i | λt | r s, where i ∈ ℕ is a de Bruijn index, and λt binds index 0 in t. The set of free indices and the lifting operation ↑ t, which increases each free index by 1, shall be defined as usual.

Let ρ ∈ ℕ → Tm. Simultaneous substitution tρ is given by the three equations:

\begin{aligned}iρ & = & ρ(i) \\ (λt)ρ & = & λ. t(⇑ ρ) \\ (r s)ρ & = & (rρ) (sρ) \end{aligned}

Herein, (⇑ ρ)(0) = 0 and (⇑ ρ)(i + 1) = ↑(ρ(i)). Substitution [s/i]t for a single index i is an instance of simultaneous substitution tρ with

ρ(j) = \{ \begin{matrix}s & if j = i \\ j & if j < i \\ j − 1 & if j > i. \end{matrix}

There is also a direct implementation of substitution [s/i]t for a single index:

\begin{aligned}[s/i]j & = & \{ \begin{matrix}s & if j = i \\ j & if j < i \\ j − 1 & if j > i \end{matrix} \\ [s/i](λt) & = & λ. [↑ s/i + 1]t \\ [s/i](t u) & = & ([s/i]t) ([s/i]u) \end{aligned}

However, this algorithm differs not much from the instance of simultaneous substitution we had before. It just uses a representation of the valuation ρ as a pair (s, i), with lookup ρ(j) and lifting ⇑ ρ defined accordingly.

We will now investigate how this implementation of a single substitution carries over to our representation of de Bruijn terms as a heterogeneous datatype. The operations <, >, and −1 cannot be implemented in F_{ω} on our type of variables, which has a shape of the form 1 + ⋯ + 1 + A; we would need advanced type-level programming features such type classes or inductive kinds. But we can massage our implementation of singleton valuations into a form which is implementable in F_{ω}.

The new representation of a singleton valuation is a pair (s, ϕ) where ϕ ∈ ℕ → (ℕ ∪ {∗}), and we define lookup and lifting as follows:

(s, ϕ)(j) = \{ \begin{matrix}s & if ϕ(j) = ∗ \\ ϕ(j) & otherwise \end{matrix}

⇑(s, ϕ) = (↑ s, ϕ′) where ϕ′(0)  = 0 ϕ′(j + 1) = \{ \begin{matrix}∗ & if ϕ(j) = ∗ \\ ϕ(j) + 1 & otherwise \end{matrix}

Substitution [s/0]t for the index 0 is then obtained by tρ with ρ = (s, ϕ), ϕ(0) = ∗ and ϕ(j + 1) = j.

This representation of singleton valuations can also be used with the representation of de Bruijn terms as a heterogeneous type in Section 5. Then, ϕ(j) = ∗ is represented as ϕ(y) = inl⟨⟩. If y is not the one variable which is assigned to ŝ in the singleton valuation, then ϕ(y) = inr y′ for some variable y′ which is either identical to y or the variable just below y (thus, we have y ∈ {y′, inr y′}). A singleton valuation is defined for at least one variable, thus, the domain of ϕ is 1 + A.

SgVal  : ord →^{+} ∗ →^{∘} ∗
SgVal  := λıλA. Tm^{∞}A × Ty^{ı} × (1 + A → 1 + A)
lookup_{Val} : ∀ı∀A. SgVal^{ı}A → 1 + A → Res^{ı}A
lookup_{Val} := λ⟨s, a, ϕ⟩λy. match ϕ y with
inl ⟨⟩ ↦ nf_{Res} s a
inr y′ ↦ ne_{Res} (var y′)
sg_{Val}  : ∀ı∀A. Tm^{∞}A → Ty^{ı} → SgVal^{ı} A
sg_{Val}  := λsλa. ⟨s, a, λy.y⟩
lift_{Val}  : ∀ı∀A. SgVal^{ı} A → SgVal^{ı} (1 + A)
lift_{Val}  := λ⟨s, a, ϕ⟩. ⟨lift_{Tm} s, a, ϕ′⟩

where

ϕ′ := λy. match y with
inl ⟨⟩ ↦ inl ⟨⟩
inr y′ ↦ map_{Maybe} inr (ϕ y′)

The code for subst can be reused, only simsubst now receives the less general type

simsubst : ∀ȷ. ∀A. Tm^{ȷ}(1 + A) → SgVal^{ı+1} A → Res^{ı+1}A.

By parametricity for the type of simsubst, SgVal needs to have a functional component with a domain that mentions A positively. Thus, no fundamentally different implementations of substitution are possible for the chosen, type-indexed representation of de Bruijn terms.

References

Abel, Andreas. (2004a). Termination checking with types. RAIRO – Theoretical Informatics and Applications, 38(4), 277–319. Special Issue: Fixed Points in Computer Science (FICS’03).

Abel, Andreas. (2004b). Weak normalization for the simply-typed lambda-calculus in Twelf. Logical Frameworks and Metalanguages (LFM 2004), IJCAR Satellite Workshop, Cork, Ireland.

Abel, Andreas. (2006a). Implementing a normalizer using sized heterogeneous types. McBride, Connor, & Uustalu, Tarmo (eds), Workshop on Mathematically Structured Functional Programming, MSFP 2006, Kuressaare, Estonia, July 2, 2006. electronic Workshop in Computing (eWiC). The British Computer Society (BCS).

Abel, Andreas. (2006b). A polymorphic lambda-calculus with sized higher-order types. Ph.D. thesis, Ludwig-Maximilians-Universität München.

A Normalizer Via Sized Types 23

Abel, Andreas. (2006c). Semi-continuous sized types and termination. Pages 72–88 of: Ésik, Zoltán (ed), Computer Science Logic, 20th International Workshop, CSL 2006, 15th Annual Conference of the EACSL, Szeged, Hungary, September 21-24, 2006, Proceedings. Lecture Notes in Computer Science, vol. 4207. Springer-Verlag.

Adams, Robin. (2006). Formalized metatheory with terms represented by an indexed family of types. Pages 1–16 of: Filliâtre, Jean-Christophe, Paulin-Mohring, Christine, & Werner, Benjamin (eds), Types for Proofs and Programs, International Workshop, TYPES 2004, Jouy-en-Josas, France, December 15-18, 2004, Revised Selected Papers. Lecture Notes in Computer Science, vol. 3839. Springer-Verlag.

Altenkirch, Thorsten. (1993). A formalization of the strong normalization proof for System F in LEGO. Pages 13–28 of: Bezem, M., & Groote, J. F. (eds), Typed Lambda Calculi and Applications, TLCA’93. Lecture Notes in Computer Science, vol. 664. Springer-Verlag.

Altenkirch, Thorsten, & Reus, Bernhard. (1999). Monadic presentations of lambda terms using generalized inductive types. Pages 453–468 of: Flum, Jörg, & Rodríguez-Artalejo, Mario (eds), Computer Science Logic, 13th International Workshop, CSL ’99, 8th Annual Conference of the EACSL, Madrid, Spain, September 20-25, 1999, Proceedings. Lecture Notes in Computer Science, vol. 1683. Springer-Verlag.

Amadio, Roberto M., & Coupet-Grimal, Solange. (1998). Analysis of a guard condition in type theory (extended abstract). Pages 48–62 of: Nivat, Maurice (ed), Foundations of Software Science and Computation Structure, First International Conference, FoS-SaCS’98, Held as Part of the European Joint Conferences on the Theory and Practice of Software, ETAPS’98, Lisbon, Portugal, March 28 - April 4, 1998, Proceedings. Lecture Notes in Computer Science, vol. 1378. Springer-Verlag.

Barthe, Gilles, Frade, Maria J., Giménez, Eduardo, Pinto, Luis, & Uustalu, Tarmo. (2004). Type-based termination of recursive definitions. Mathematical Structures in Computer Science, 14(1), 97–141.

Barthe, Gilles, Grégoire, Benjamin, & Pastawski, Fernando. (2005). Practical inference for type-based termination in a polymorphic setting. Pages 71–85 of: Urzyczyn, Pawel (ed), Typed Lambda Calculi and Applications (TLCA 2005), Nara, Japan. Lecture Notes in Computer Science, vol. 3461. Springer-Verlag.

Barthe, Gilles, Grégoire, Benjamin, & Pastawski, Fernando. (2006). CICˆ : Type-based termination of recursive definitions in the Calculus of Inductive Constructions. Pages 257–271 of: Hermann, Miki, & Voronkov, Andrei (eds), Logic for Programming, Artificial Intelligence, and Reasoning, 13th International Conference, LPAR 2006, Phnom Penh, Cambodia, November 13-17, 2006, Proceedings. Lecture Notes in Computer Science, vol. 4246. Springer-Verlag.

Bellegarde, Françoise, & Hook, James. (1994). Substitution: A formal methods case study using monads and transformations. Science of Computer Programming, 23(2-3), 287– 311.

Berghofer, Stefan. (2006). Extracting a normalization algorithm in Isabelle/HOL. Pages 50–65 of: Filliâtre, Jean-Christophe, Paulin-Mohring, Christine, & Werner, Benjamin (eds), Types for Proofs and Programs, International Workshop, TYPES 2004, Jouyen-Josas, France, December 15-18, 2004, Revised Selected Papers. Lecture Notes in Computer Science, vol. 3839. Springer-Verlag.

Bird, Richard S., & Paterson, Ross. (1999). De Bruijn notation as a nested datatype.

Journal of Functional Programming, 9(1), 77–91. Blanqui, Frédéric. (2004). A type-based termination criterion for dependently-typed

higher-order rewrite systems. Pages 24–39 of: van Oostrom, Vincent (ed), Rewriting Techniques and Applications, 15th International Conference, RTA 2004, Aachen, Ger-

24 A. Abel

many, June 3 – 5, 2004, Proceedings. Lecture Notes in Computer Science, vol. 3091. Springer-Verlag.

Blanqui, Frédéric. (2005). Decidability of type-checking in the Calculus of Algebraic Constructions with size annotations. Pages 135–150 of: Ong, C.-H. Luke (ed), Computer Science Logic, 19th International Workshop, CSL 2005, 14th Annual Conference of the EACSL, Oxford, UK, August 22-25, 2005, Proceedings. Lecture Notes in Computer Science, vol. 3634. Springer-Verlag.

David, René, & Nour, Karim. (2005). Arithmetical proofs of strong normalization results for the symmetric lambda-mu-calculus. Pages 162–178 of: Urzyczyn, Pawel (ed), Typed Lambda Calculi and Applications (TLCA 2005), Nara, Japan. Lecture Notes in Computer Science, vol. 3461. Springer-Verlag.

Gentzen, Gerhard. (1935). Untersuchungen über das logische Schließen. Mathematische Zeitschrift, 39, 176–210, 405–431. English translation in M. E. Szabo, editor, The Collected Papers of Gerhard Gentzen, pages 68–131, North-Holland, 1969.

Giménez, Eduardo. (1998). Structural recursive definitions in type theory. Pages 397–408 of: Larsen, K. G., Skyum, S., & Winskel, G. (eds), Automata, Languages and Programming, 25th International Colloquium, ICALP’98, Aalborg, Denmark, July 13-17, 1998, Proceedings. Lecture Notes in Computer Science, vol. 1443. Springer-Verlag.

Harper, Robert, & Licata, Daniel. (2007). Mechanizing metatheory in a logical framework.

Journal of Functional Programming, 17(4–5), 613–673. Hughes, John, Pareto, Lars, & Sabry, Amr. (1996). Proving the correctness of reactive

systems using sized types. Pages 410–423 of: 23rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL’96.

INRIA. (2007). The coq proof assistant, version 8.1. INRIA. http://coq.inria.fr/. Joachimski, Felix, & Matthes, Ralph. (2003). Short proofs of normalization. Archive of

Mathematical Logic, 42(1), 59–87. Lane, Saunders Mac. (1971). Categories for the working mathematician. Springer-Verlag. Manes, Ernest G. (1976). Algebraic theories. Springer-Verlag. McBride, Conor. (2006). Type-preserving renaming and substitution. Functional Pearl.

Draft. Mendler, Nax Paul. (1987). Recursive types and type constraints in second-order lambda

calculus. Pages 30–36 of: Proceedings of the Second Annual IEEE Symposium on Logic in Computer Science, Ithaca, N.Y. IEEE Computer Society Press.

Mendler, Nax Paul. (1991). Inductive types and type constraints in the second-order

lambda calculus. Annals of Pure and Applied Logic, 51(1–2), 159–172. Pareto, Lars. (2000). Types for crash prevention. Ph.D. thesis, Chalmers University of

Technology. Prawitz, Dag. (1965). Natural deduction. Almqvist & Wiksell, Stockholm. Republication

by Dover Publications Inc., Mineola, New York, 2006. Tait, William W. (1967). Intensional interpretations of functionals of finite type I. The

Journal of Symbolic Logic, 32(2), 198–212. Watkins, Kevin, Cervesato, Iliano, Pfenning, Frank, & Walker, David. (2003). A concur-

rent logical framework I: Judgements and properties. Tech. rept. School of Computer Science, Carnegie Mellon University, Pittsburgh.