0 Recursion vs. Iteration at Higher Orders

1

Recursion Versus Iteration at Higher-Orders

A. J. Kfoury

Boston University, Boston, MA 02215, USA e-mail: kfoury@cs.bu.edu

Abstract. We extend the well-known analysis of recursion-removal in first-order program schemes to a higher-order language of finitely typed and polymorphically typed functional programs, the semantics of which is based on call-by-name parameter-passing. We introduce methods for recursion-removal, i.e. for translating higher-order recursive programs into higher-order iterative programs, and determine conditions under which this translation is possible. Just as finitely typed recursive programs are naturally classified by their orders, so are finitely typed iterative programs. This syntactic classification of recursive and iterative programs corresponds to a semantic (or computational) classification: the higher the order of programs, the more functions they can compute.

1 Background and Motivation

Although our analysis is entirely theoretical, as it combines methods from typed λ-calculi, from abstract recursion theory and from denotational semantics, the problems we consider have a strong practical motivation.

The translation of recursive procedures into iterative procedures, sometimes called recursion-removal, has been a standard feature of programming practice for a long time. A frequent and important use of recursion-removal is, for example, in compiler design; modern treatments of this topic are in [6, Chapter 8] and [23, Chapter 21]. Discussions about other benefits of recursion-removal can be found elsewhere in the literature, e.g. in the books [1, 13, 19], among several others. The usual implementation of a recursive procedure requires a stack, in addition to basic control mechanisms to change the order of execution in a computation, such as goto instructions. The stack in question is used to save information, the so-called activation records [2, Chapter 10], from successive recursive calls of the procedure. By contrast, the implementation of an iterative procedure does not require a stack, resulting in more efficient use of storage space.

By appropriate coding and decoding of arbitrarily long sequences of activation records, it is in principle always possible to avoid the use of a stack and directly implement recursive procedures as iterative ones. The problem is that

⋆ Partly supported by NSF grant CCR–9417382. A shorter version of this paper appears in the conference proceedings of the Foundations of Software Technology and Theoretical Computer Science, held on December 18-20, 1997, at the Indian Institute of Technology, Kharagpur, India.

such a coding and decoding mechanism is not always available, and even if it is, it often leads to just as expensive implementations by trading storage space for computational complexity. In the absence of such a coding and decoding mechanism, there are recursive procedures that can be translated into iterative ones, while there are others that cannot. A procedure in the latter case is inherently recursive, in the sense that any other procedure defining the same function cannot be iterative and requires a stack for its implementation, if we also preclude the use of a coding and decoding mechanism to simulate a stack.

Comparative Schematology. The preceding facts are well-known among computer scientists. In the early 1970’s people working in comparative schematology aimed at rigorously establishing these and other similar results. Classes of program schemes were defined, modelling different control mechanisms in conventional programming languages, such as recursion and iteration. An elegant and sometimes highly technical theory was developed to examine questions of inter-translatability between these classes. The first paper in this area, sparking an intensive research activity for many years, was by Paterson and Hewitt [22] who spelled out precise conditions under which recursion-removal is not possible. We summarize the Paterson-Hewitt result by writing ITER < REC, meaning that iteration is a strictly weaker control structure than recursion.

Pebbling vs. Counting. Paterson and Hewitt gave two very different proofs for ITER < REC. Their first proof was based on the pebble game. As it turned out in later years, the pebble game and many of its variants became a basic technique in other areas of theoretical computer science; in particular, the most numerous applications have been in complexity theory, e.g. in time-space tradeoffs [24, 25], rather than in comparative schematology or in logics of programs. The second proof by Paterson and Hewitt was a counting argument. Freely speaking, counting (rather than pebbling) is used to show that a simulating iterative procedure runs out of time (rather than space). This dichotomy between pebbling and counting pervades nearly all studies of the original question recursion vs. iteration and later variants. For the early results for example, see the survey in [10, Chapters VII and VIII].

Other Theoretical Studies. Recursion pervades the whole field of computer science. Ways of removing or simplifying recursion abound. The background reviewed above by no means exhausts the topic and only covers that part of the field directly motivating our work. There is for example an extensive literature on boundedness of database logic programs, see [12] and the references therein; a database program is bounded if the depth of recursion is a constant independent of the input, in which case the program is equivalent to a recursion-free firstorder formula. Another motivation for the study of recursion vs. iteration comes from inductive definability in abstract recursion theory; see for example [20] and [21], where a formal logic framework is defined to study the question. Another work still is [5], where the question is considered in relation to program synthesis. However interesting these and other studies are, none is directly related to this paper. Closer to our concerns is part of the literature on continuations that deals with issues of recursion removal, specifically, the use of CPS (continuationpassing style) to transform a recursive functional program into tail-recursive form. Although “iteration” and “tail-recursion” coincide in the case of firstorder programs, the two notions are not exactly the same at higher-orders. In the full version [16] of this report, we adduce several reasons for this distinction; in any case, an attractive theory and many non-trivial results emerge out of the distinction, as shown in [16].

Some Past Results and Some Questions. This history of results, starting with the Paterson-Hewitt result in 1970, is entirely concerned with the firstorder case of recursion vs. iteration. That is, recursive and iterative procedures are always activated by receiving input values of ground type, and they always return an output value, if any, of ground type.

Many modern programming languages allow their programs to use higherorder objects in their computations. The role of such objects is purely auxiliary in that, semantically, higher-order values are not mentioned in the input-output relation of the program. In our setting, only the main procedure in a program is first-order, but it can call intermediate procedures of arbitrary finite orders. It is now important to distinguish between a single procedure and a finite collection of procedures calling each other, of which only one is the main procedure. In this paper, we call such a collection a functional program. The order of a functional program is the highest order of any of its procedures. In general, a functional program is recursive, as no restriction is imposed on its syntax; under the restriction that all of its procedures are iterative, we say that the functional program is iterative. If ITER_{n} and REC_{n} are, respectively, the set of all iterative functional programs and the set of all recursive functional programs of order ⩽ n, where n is a positive integer, then:

ITER_{n} ⊂ REC_{n} (1)

i.e. every program in ITER_{n}, as a syntactic object, is a program in REC_{n}, but not vice-versa. We also have the following strict syntactic hierarchies:

ITER_{1} ⊂ ITER_{2} ⊂ ITER_{3} ⊂ ⋯ (2)

REC_{1} ⊂ REC_{2} ⊂ REC_{3} ⊂ ⋯ (3)

(ITER_{1} and REC_{1} here are ITER and REC mentioned earlier.) It is well-know there is a strict computational hierarchy (see, for example, [9] or [15] or references cited therein):

REC_{1} < REC_{2} < REC_{3} < ⋯ (4)

In words, increasing the order of functional programs results in a gain of computational power. On the other hand, so far we can only assert, by (2):

ITER_{1} ⩽ ITER_{2} ⩽ ITER_{3} ⩽ ⋯ (5) and the obvious question is whether this computational hierarchy is strict. In the presence of higher-order procedures, the question of recursion vs. iteration splits into two parts. We first ask, for n ⩾ 2:

Is ITER_{n} < REC_{n} ? (6)

If the answer to question (6) is yes, it will generalize to higher-orders the Paterson-Hewitt result in [22], namely: At every order, there are functional programs that are inherently recursive. We further ask, for n ⩾ 1:

Is REC_{n} ⩽ ITER_{n′} for some n′ > n ? If yes, what is the least such n′ ? (7)

In words, question (7) asks whether recursion-removal is always possible after all, but now at the price of increasing the order of the program. These and other related questions, to be formulated in due course, are the immediate motivation for the present work.

Organization of the Paper. The first task is to define precisely the framework of the investigation. Our choices are not the only possible ones: How we define higher-order procedures, and how we interpret and execute them, depend on choices inspired by a particular programming paradigm. This is the paradigm of strongly-typed pure functional programs, where there are no side-effects and where the only execution mechanism is call-by-name parameter-passing. This is all done in Section 2 and Section 3. Hence, equivalence between programs here means equivalence under an operational semantics based on call-by-name execution. In addition to the hierarchies {REC_{n}} and {ITER_{n}} mentioned earlier, we define the class p-REC of polymorphically typed recursive programs and the class p-ITER of polymorphically typed iterative programs.

Section 4 re-examines the recursive program used by Paterson and Hewitt [22] to show that ITER_{1} < REC_{1}. The purpose of this examination is partly to gather evidence and intuition for the systematic translation developed in Section 5 from higher-order recursion to higher-order iteration.

Our key technical lemmas are presented in Section 5 and Section 6. From these results, we draw several consequences about the hierarchies {REC_{n}} and {ITER_{n}} in Section 7.

Further details for some of the proofs here, as well as additional results relating higher-order recursion, tail-recursion and iteration, are in our forthcoming report [16]. For typesetting convenience, all figures are displaced to the very end of the report.

2 Basic Definitions: Syntax and Semantics

What we set up is the syntax of a typed λ-calculus + conditionals + recursion. We introduce recursion by means of mutually recursive functional equations, and not by application of fixpoint operators.

Definition 1 (Types). Let TVar be an infinite set of type variables. Let ∗ and bool be two type constants, which we call ground types. The atomic types are {∗, bool} ∪ TVar. The set 𝕋 of types is the least such that

𝕋 ⊇ {∗, bool} ∪ TVar ∪ { (σ → τ) | σ, τ ∈ 𝕋 }

For σ ∈ 𝕋, let TVar(σ) denote the finite set of type variables occurring in σ. We partition 𝕋 into the set 𝕋_{fin} of finite types and the set 𝕋_{gen} of generic types:

𝕋_{fin} = { σ ∈ 𝕋 | TVar(σ) = ∅ }  and  𝕋_{gen} = 𝕋 − 𝕋_{fin} .

The order of a finite type σ ∈ 𝕋_{fin} is:

order(σ) = \{ \begin{matrix}0, & if σ = ∗ or bool; \\ max\{order(τ_{1}) + 1, order(τ_{2})\}, & if σ = (τ_{1} → τ_{2}). \end{matrix}

We do not define order(σ) if σ is generic. In what follows, every term M has a type τ, which we indicate by writing M : τ. If τ is a finite type and M : τ, we say that M is finitely typed. If τ is a generic type and M : τ, we say that M is polymorphically typed.

A type substitution is a map S : TVar → 𝕋 such that {α ∈ TVar|S(α) ≠ α} is finite. Every type substitution extends in a natural way to a {∗, bool, →}- homomorphism S : 𝕋 → 𝕋. For σ, τ ∈ 𝕋, we say that τ is an instance of σ, in symbols σ ≼ τ, if there is a type substitution S such that τ = S(σ).

Definition 2 (Terms). A class of functional programs is defined relative to a fixed first-order signature Σ_{A} = Σ ∪ A, where Σ is a finite set of relation and function symbols and A is a countable set of individual symbols. To avoid trivial and uninteresting situations, we require that both Σ ≠ ∅ and A ≠ ∅. Every relation (or function) symbol f ∈ Σ has a fixed arity k ⩾ 1, in which case its type is

\underbrace{∗ → ⋯ → ∗}_{k} → ρ , abbreviated as ∗^{k} → ρ ,

where ρ = bool (or ∗, resp.), i.e. a finite type of order 1. Every constant in A is of type ∗. It is convenient to use two disjoint sets of variables: object variables and function names. For every type τ there is a countably infinite set of object variables of type τ, and for every non-atomic type τ a countably infinite set of function names of type τ. The set of terms is the smallest containing

{ tt, ff } ∪ A ∪  (ground constants)
Σ ∪ { if^{τ} | τ ∈ 𝕋 } ∪  (other constants)
{ object variables } ∪ { instantiated function names } (variables)

and closed under application and λ-abstraction. The details of the definition of well-typed terms are given in Figure 1.

We omit the type subscript τ in if^{τ} and in an instantiated function name F^{τ} whenever possible, if no ambiguity is introduced. (if M then N else P) is a sugared version of (if M N P). For simplicity, we often omit the type of a λ-binding, and therefore write (λv M) instead of (λv : σ. M). If a closed term M and all its subterms are finitely typed, the order of M is:

order(M) = max { order(τ) | N ⊆ M and N : τ }

If M is not closed and N ≡ (λv M) is the closure of M, then order(M) = order(N). We do not define the order of a polymorphically typed term. By a slight abuse of terminology, we often say “M is a n-th order term” to mean that order(M) ⩽ n rather than order(M) = n.

Definition 3 (Functional Programs). Let F be a function name of type σ ∈ 𝕋. A function definition for F is an equation of the form F = M where M is an arbitrary closed term of type σ. F on the left of “=” is not instantiated, while every occurrence of F on the right of “=” is instantiated as F^{τ}, for some τ such that type(F) ≼ τ, and corresponds to a recursive call to F at type τ.

A functional program P is a finite non-empty set of function definitions, together with a distinguished function name F such that:

– The type of F is ∗^{k} → ρ for some k ⩾ 1, where ρ = ∗ or bool.

– For every function name G, P has at most one function definition for G.

– For every function name G, P has a definition for G if there is an instance G^{τ} of G appearing in P (i.e. on the right of “=”, a call to G at some type τ).

The restrictions we impose on the type of the distinguished F have to do with the fact that the inputs and output, if any, of a program are always ground values.

Let P be the functional program {F_{i} = M_{i}}_{1⩽i⩽ℓ}. In a ML-like language that supports polymorphic recursion, P can be written as:

λv_{1} ⋯ v_{k}. letrec (F_{1}, …, F_{ℓ}) = (M_{1}, …, M_{ℓ}) in F_{1}v_{1} ⋯ v_{k}

where F_{1} is the distinguished function of arity k ⩾ 1. If the types of all the terms M_{1}, …, M_{ℓ} and their subterms are finite, then P is finitely typed; otherwise, P is polymorphically typed. If P is finitely typed, then its order is

order(P) = max{order(M_{1}), …, order(M_{ℓ})}

If this order is n ⩾ 1, we also say this is an order-n functional program. We do not define the order of a polymorphically typed program. Several examples of finitely typed programs are in Sections 3, 4 and 5, and an example of a polymorphically typed program is in Section 6.

Although it does not restrict the later analysis in any way, let us assume that the right-hand side of every function definition F_{i} = M_{i} in P is in β-normal form. Under this assumption, it is easy to check that if 1 ⩽ order(F_{i}) < order(M_{i}) then there is an instantiated function name F_{j} occurring in M_{i} such that order(F_{j}) = order(M_{i}). Hence, under this assumption, we can equivalently and more simply define order(P) by: order(P) = max{order(F_{1}), …, order(F_{ℓ})} . The syntactic hierarchy of functional programs is given by:

• REC_{n} = { finitely typed functional programs of order ⩽ n }

• REC = ⋃_{n⩾1} REC_{n}

• p-REC = { polymorphically typed functional programs }

Definition 4 (Call-by-Name Semantics). A functional program computes relative to a Σ_{A}-structure A which assigns a meaning to every symbol in the signature Σ. We take the universe of A to be precisely the set A of all individual constants of type ∗. The meaning in A of the symbol f ∈ Σ of type ∗^{k} → ρ, where k ⩾ 1 and ρ = ∗ (or bool), is a total function from A^{k} to A (or to {tt,ff}). For the functional program P = {F_{i} = M_{i}}_{1⩽i⩽ℓ} we define the reduction relation ⟶_{A,P} relative to A by the rewrite rules of Figure 2.

In the δ-reduction rule, a_{1}, …, a_{k} are arbitrary elements of A, f ∈ Σ has arity k ⩾ 1, and f interpreted in A is a function that maps a_{1} ⋯ a_{k} to a_{k+1} ∈ A∪{tt,ff}. We often leave the structure A and the program P implicit, and write ⟶ instead of ⟶_{A,P}. We write ⟶ ⟶ for the reflexive transitive closure of ⟶.

A redex is one of the terms appearing on the left-hand side of ⟶ in one of the first 4 rules of Figure 2. In addition to the usual β-redexes, we also have P-redexes, if-redexes, and δ-redexes in our calculus. We often need to refer to the position of a redex occurrence Δ relative to other redex occurrences in the same term. If Δ is not a single symbol, i.e. it is not a P-redex, we agree that the position of Δ is determined by its outermost left parenthesis. For example, in the term:

( f (_{1} if tt then (_{2} (λv. F_{3} v) a_{1} ) else a_{2} ) (_{4} f a_{1} a_{2} ) )

there are four redexes labelled with 1 (an if-redex), 2 (a β-redex), 3 (a P-redex) and 4 (a δ-redex), in the order in which they occur from left to right.

The first term in a computation of program P is always (F a_{1} ⋯ a_{k}), where F is the distinguished function name of P with arity k ⩾ 1, for some a_{1}, …, a_{k} ∈ A. We call a = a_{1} ⋯ a_{k} an input vector for P. We call ⟨A, a⟩ an interpretation for P. Note that (F a_{1} ⋯ a_{k}) is a closed term of a ground type, ∗ or bool.

The next proposition is proved in [15, Sections 2 and 3]. The Church-Rosser property, the standarization property, and other concepts of the λ-calculus are defined in [4]. A term is in normal form if it does not contain any redexes, i.e. it cannot be reduced. To reduce a term in normal order means to reduce its leftmost redex at every step.

Proposition 5. Let P be a program over the signature Σ_{A}, whose distinguished function name is F : ∗^{k} → ρ where k ⩾ 1 and ρ ∈ {∗, bool}. Let ⟨A, a⟩ be an interpretation for P.

1. The above reduction system has the Church-Rosser property and the standarization property.

2. If applying the reduction rules in some arbitary order causes (F a) to terminate at a term M, i.e. M is in normal form, then M is a ground constant of type ρ.

3. If applying the reduction rules in some arbitrary order causes (F a) to terminate at ground constant b, then applying the reduction rules in normal order also causes (F a) to terminate at the same ground constant b. ⊓ ⊔

The call-by-name semantics of functional programs corresponds to carrying out their computations, viewed as reduction sequences, in normal order. Let P be a functional program over the signature Σ_{A}, whose distinguished function name is F : ∗^{k} → ρ where k ⩾ 1 and ρ = ∗ or bool. Over a Σ_{A}-structure A, the program P defines a partial function P^{A} : A^{k} → A or P^{A} : A^{k} → {tt,ff }, given by: P^{A} = { ⟨a, b⟩ | (F a) ⟶ ⟶ b } where b ∈ A or b ∈ {tt,ff }, respectively. Implicit in this definition, by the preceding proposition, is that P^{A} is the callby-name semantics of P over the structure A.

3 Iterative Form

A term M is simple if M does not mention instantiated function names. A term M is left-linear if either M is simple or M ≡ (F N_{1} ⋯ N_{k}) where F is an instantiated function name and N_{1}, …, N_{k} are simple terms.

Recall that the order of a finitely typed term M is the order of its closure. Hence, M is first-order simple iff every variable occurring in M is of ground type and M does not mention instantiated function names.

Definition 6 (Iterative Form). A function definition F = M is in iterative form (or left-linear form) if

— either M ≡ λv. N, where N is left-linear,

— or M ≡ λv. if N then P else Q, where N is first-order simple, and P and Q are left-linear.

A functional program {F_{i} = M_{i}} is in iterative form if every definition in it is in iterative form. The syntactic hierarchy of iterative programs is given by:

• ITER_{n} = { finitely typed iterative programs of order ⩽ n }

• ITER = ⋃_{n⩾1} ITER_{n}

• p-ITER = { polymorphically typed iterative programs }

It is tempting to generalize the definition of iterative form above, by relaxing the restriction on the first argument N of an outermost if on the right-hand side of a function definition. This can be done in two ways, the second being itself a generalization of the first:

1. N is a simple term in general, not restricted to first-order.

2. N is a left-linear term, not restricted to simple.

The first generalization is in fact just syntactic sugar; every program according to this generalization can be translated into an equivalent iterative program in our sense and of the same order (we do not prove this result here, but consider Definition 7 and the analysis in Section 5 for suggestions). The second generalization does introduce a powerful feature, in that the resulting class of programs of order ⩽ n, for any fixed n, cannot be translated into our class of iterative programs of order ⩽ n, as illustrated by the next example. In any case, our definition of iterative programs is not too broad and certainly within the criteria of other definitions of iterative form in the literature.

Example 1. P is the following first-order functional program:

F x = SEARCH x ε
SEARCH x y = if (eq x y) then tt else NEXT x y
NEXT x y = if LEFT x y then tt else RIGHT x y
LEFT x y = if (eq (Ly) y) then ff else SEARCH x (Ly)
RIGHT x y = if (eq (Ry) y) then ff else SEARCH x (Ry)

The signature of the program is Σ = {eq, L, R} and ε is a ground constant. The types of the symbols in Σ, the variables x and y, and the constant ε are

eq : ∗ → ∗ → bool
x, y, ε : ∗
L, R : ∗ → ∗

The types of each of the function names in {F, SEARCH, NEXT, LEFT, RIGHT} is uniquely determined by the preceding types. P is not in iterative form because of the definition for NEXT, where the first argument of the if is left-linear rather than simple. It turns out that P is not equivalent to any iterative program of the same order (first-order). This is shown next.

When interpreted in an infinite treelike structure A – with ε taken as the root of the treelike universe of A, L as the “left” operator, R as the “right” operator, and eq as the equality relation – F acquires the following meaning:

Fa = \{ \begin{matrix}tt, & if a occurs on, or to the left of, \\ & the leftmost infinite path in A; \\ undefined, & otherwise. \end{matrix}

This can be verified by considering the intuitive meaning of the function SEARCH. The computation of (SEARCH x y) searches for x in the tree rooted at y, in left-to-right depth-first fashion. If the tree rooted at y is finite, (SEARCH x y) terminates whether or not x occurs in this finite tree. (LEFT x y) searches for x in the left subtree of node y, and (RIGHT x y) searches for x in the right subtree of node y.

There are infinite treelike structures where all first-order flowchart programs are said to “unwind”, for example the structure T_{ω} in [28]. This implies that over such structures, any first-order iterative program is equivalent to one without recursion at all,^{2} and cannot therefore be equivalent to P above. ⊓ ⊔

2 Strictly speaking, a functional program without “non-trivial” recursion. A “trivial”

Definition 7 (Higher-Order Flowcharts). The translation of a recursive functional program into an iterative one, whether of the same order or of a higher order, is often easier by means of an intermediate translation to a flowchart. We only define finitely typed flowcharts; it is possible to define polymorphically typed flowcharts, but the definition is somewhat cumbersome and there is no real need for it later.

A flowchart of order n ⩾ 1 is a flowchart that may use variables of order < n (these should perhaps be called locations). Assignment instructions in a flowchart are of the form

v := M

where v is a variable, M is a simple term, and v and M have the same finite type. The execution of the instruction “v := M” produces a side-effect, namely, the normal form of M is stored in the “location” v. Test instructions are of the form

(f v_{1} ⋯ v_{k}) ?

where v_{1}, …, v_{k} are variables of ground type ∗, and f is a relation symbol in the signature Σ of type ∗^{k} → bool.

The finitely many input variables of an order-n flowchart are of ground type ∗, while its single output variable is of ground type ∗ or bool. Free variables other than input variables appearing in test instructions or to the right of “:=” in assignment instructions must be each properly initialized, i.e. assigned a term whose only free variables are among the input variables or previously initialized variables. It would be tedious for us to define higher-order flowcharts with any greater formality; we instead refer the reader to [15, Section 1] for more details, as well as to Example 2 below and to later examples in the paper.

Proposition 8. Every order-n flowchart is translatable into an equivalent ordern iterative functional program.

Proof. Use the so-called McCarthy method to translate the order-n flowchart into an order-n iterative functional program. The McCarthy method was originally devised for the translation of ordinary (first-order) flowcharts. The generalization to higher orders is immediate; consult the original [18] or any of its textbook accounts, e.g. in [11, Section 5.3]. ⊓ ⊔

Another straightforward, though somewhat tedious, translation is the following: Every order-n iterative functional program is translatable into an order-n flowchart. This is done as in the first-order case [11, Section 5.4], by “uniformizing” the functional program (not done here). Thus, the class of order-n iterative functional programs is intertranslatable with the class of order-n flowcharts.

function definition is of the form F = F or Fv = Fv, which makes the program diverge whenever the function F is called. Allowing the definition Fv = Fv in a functional program, which is otherwise recursion-free, is very much like allowing self-loops in an otherwise loop-free flowchart.

Example 2. P is the following second-order functional program:

Fx = Gfx
GF x = if px then gx(G(λy.F^{(2)}y)(F x)) else hx

where F^{(2)}y is a short-hand notation for (F (F y)). The types of the symbols in the signature Σ = {p, f, h, g} and the variables {x, y, F } are

x, y : ∗
p : ∗ → bool
f, h, F : ∗ → ∗
g : ∗ → ∗ → ∗

P is in linear but not iterative form. With a little work, we can show there is an order-2 iterative program that simulates P; actually, we construct an order-2 flowchart for the simulation and then invoke Proposition 8 to show the existence of an equivalent order-2 iterative program. This is not a syntax-directed translation and relies on our understanding of what the program computes. Consider a converging computation of F, where we leave some of the δ-redexes unevaluated:

Fx ⟶ Gfx
⟶ gx(G(λy.f^{(2)}y)(fx))
⟶ gx(g(fx)(G(λy.f^{(4)}y)(f^{(3)}x)))
⟶ ⋯
⋮
⟶ gx(g(fx)(g(f^{(3)}x) ⋯ (g(f^{(2^{n−1}−1)}x)(G(λy.f^{(2^{n})}y)(f^{(2^{n}−1)}x))) ⋯))
⟶ gx(g(fx)(g(f^{(3)}x) ⋯ (g(f^{(2^{n−1}−1)}x)(h(f^{(2^{n}−1)}x))) ⋯))

We have interrupted the reduction at the first term not containing a call to the function G. The flowchart that simulates this reduction is not concerned about the evaluation of simple terms to their normal forms, but only about the sequence of calls to the function G: How many times it is called and what are the arguments (or actual parameters) of every call. When an assignment instruction v := M in the flowchart is executed, v is bound to the normal-form term obtained after carrying out all possible β-, if-, and δ-reductions in the simple term M.

Whereas the final term is constructed in “outside-in” fashion in the above reduction sequence, the equivalent flowchart (Figure 3) constructs the same term in “inside-out” fashion. For convenience in the flowchart, we allow simultaneous assignment instructions of the form (v, w) := (M, N). This is a second-order flowchart.

We leave it to the reader to verify that the flowchart of Figure 3 simulates correctly the computation of the functional program. Observe that the flowchart has two distinct parts; the first starts with instruction labelled 1 and the second with instruction labelled 2. The first part construct the “inner” subterm (h (f^{(2^{n}−1)} x)) of the output term, and the second part constructs the rest of the output term in “inside-out” fashion. ⊓ ⊔

4 Paterson-Hewitt Revisited

The examples in this section are inspired by the Paterson-Hewitt paper [22]. They illustrate some of the evidence, as well as the difficulty, in translating a functional program into an iterative one of higher order.

Example 3. Consider the following first-order functional program:

Fxy = if px then y else g (F(fx)(Ly)) (F(fx)(Ry))

where the signature is Σ = {p, L, R, f, g}, and the types are

x, y : ∗
p : ∗ → bool
L, R, f : ∗ → ∗
F, g : ∗ → ∗ → ∗

In standard first-order notation, which makes clearer how to apply the “pebble game” (below), we can rewrite the above program as:

F(x, y) = if p(x) then y else g(F(fx, Ly), F(fx, Ry))

F is not equivalent to any first-order iterative program. To explain why this is so, consider the sequence of terms:

M_{0} ≡ y  and  M_{n+1} ≡ g(M_{n}[y := Ly], M_{n}[y := Ry])

for every n ⩾ 0. Thus, M_{1} ≡ g(Ly, Ry), M_{2} ≡ g(g(LLy, RLy), g(LRy, RRy)), etc. A straightforward application of the pebble game shows that, for every n ⩾ 1, none of the terms in {M_{k}|k ⩾ n} is accessible to the n-pebble game. Now, looking at the execution of F, it calls itself recursively twice, k times for a total of 2^{k} recursive calls, where k is the least integer ⩾ 0 such that p(f^{(k)}x) = tt. If there is no such k, then F diverges, and if there is such k, then F converges and returns the term M_{k}. Thus, {M_{k}|k ⩾ 0} is exactly the set of output terms of F.

On the other hand, F can be translated into second-order iterative form, as follows. Define the sequence of terms:

F_{0} ≡ λz.z  and  F_{n+1} ≡ λz.g(F_{n}(Lz))(F_{n}(Rz))

for every n ⩾ 0. It is easy to check that M_{n} = F_{n}y for every n ⩾ 0. We can thus write the second-order flowchart shown in Figure 4, which is equivalent to F and where the type of the variable F is ∗ → ∗. In the form of a second-order iterative program, this flowchart becomes

F_{1}xy = F_{2} (λz.z) x y
F_{2}F xy = if px then F y else F_{2} (λz.g(F (Lz))(F (Rz))) (fx) y

by a straightforward application of the McCarthy method (Proposition 8). ⊓ ⊔ Example 4. The following first-order functional program is from the Paterson-Hewitt paper [22]:

Fx = if px then x else g (F(Lx)) (F(Rx))

where the signature is Σ = {p, L, R, g}, and the types of the symbols in Σ are those given in the preceding example. Using the pebble game, Paterson and Hewitt show that this functional program cannot be simulated by a first-order iterative program. We examine some of the difficulties of simulation. Consider the stopping condition for this program: The execution of Fx converges iff every sufficiently long sequence α ∈ {L, R}^{∗} has a suffix β such that p(βx) = tt iff, more formally,

(∃n ⩾ 0) (∀α ∈ {L, R}^{n}) (∃β, γ ∈ {L, R}^{∗}) [ α = γβ and p(βx) = tt ]

If β = d_{k} ⋯ d_{2}d_{1} ∈ {L, R}^{k}, our notation βx abbreviates (d_{k}(⋯ (d_{2}(d_{1}x)) ⋯)). Given a structure A = (A, p, L, R, g) define the function φ(p, L, R) by:

φ(p, L, R) =
μn ⩾ 0 [ (∀α ∈ {L, R}^{n}) (∃β, γ ∈ {L, R}^{∗}) α = γβ and p(βx) = tt ]

It is not difficult to write a first-order flowchart augmented with counters, call it P, which can compute the value of φ(p, L, R) — if it exists, otherwise P diverges. The signature of P is also {p, L, R} (the function g is not used by P). We omit the details of how to write P. In Figure 5 we give the second-order flowchart, augmented with counters, which is equivalent to F. The type of the variable F is ∗ → ∗. The instruction labeled P in Figure 5 is a macro, whose expansion is a first-order flowchart augmented with counters. ⊓ ⊔

Example 5. Consider again the Paterson-Hewitt program in Example 4. A CPS (continuation-passing-style) transformation “by hand” produces the following program:

F′x = G′ x (λv.v)
G′xκ = if px then κx else G′ (Lx) (λv.G′ (Rx) (λw.κ(gvw)))

The resulting program is in so-called “tail form”, but not iterative in our sense. The order of the entire program is 2, as the type of G′ is ∗ → (∗ → ∗) → ∗. ⊓ ⊔

None of the techniques used in Examples 3, 4 and 5 can transform the Paterson-Hewitt program into an equivalent order-2 iterative program over the same signature Σ = {p, L, R, g}. The transformation developed in the next section, partly inspired by the translations in Examples 3 and 4, can.

5 From Recursion to Iteration

We restrict our analysis in this section to finitely typed programs, as we do not know how to extend it to polymorphically typed programs. Unless stated otherwise, all programs in this section are finitely typed. We deliberately omit details in several proofs in this section, as some of the ideas and arguments are lifted with only minor adjustments from denotational semantics and strictness analysis.

Let P = {F_{i} = M_{i}}_{1⩽i⩽ℓ} be a functional program where F_{1} is the distinguished function name. The ℓ function definitions in P are mutually recursive. Suppose F_{1} : σ_{1}, …, F_{ℓ} : σ_{ℓ} for some finite types σ_{1}, …, σ_{ℓ} ∈ 𝕋_{fin}. As F_{1} is the distinguished function name, let σ_{1} ≡ ∗^{k} → ρ for some k ⩾ 1 and some ground type ρ. We temporarily introduce a special symbol ⊥_{σ} : σ with the exhibited type for every σ ∈ 𝕋_{fin}. Intuitively, ⊥_{σ} stands for “a diverging computation at type σ”. We define a “flowchart” \overline{P} whose call-by-name semantics coincide with the call-by-name semantics of P. \overline{P} is shown in Figure 6, where x_{1}, …, x_{k} are k input variables all of type ∗ and z is a fresh variable of type ρ

The construction of \overline{P} from P is suggested by standard methods in denotational semantics. \overline{P} basically evaluates the fixed point of the equation

(F_{1}, …, F_{ℓ}) = (M_{1}(F_{1}, …, F_{ℓ}), …, M_{ℓ}(F_{1}, …, F_{ℓ}))

by evaluating successive approximations that are increasingly finer. We write M_{i}(F_{1}, …, F_{ℓ}) rather than just M_{i} to make explicit that M_{i} is a term that may mention some of the function names in {F_{1}, …, F_{ℓ}}. If on input a = a_{1} ⋯ a_{k}, the call-by-name evaluation of (F_{1}a) terminates and returns a ground value b, then \overline{P} evaluates enough of this fixed point in order to return the same output b. Note that \overline{P} is not a legal flowchart in the sense of Definition 7, because \overline{P} mentions: (1) the artificial symbols ⊥_{σ}, (2) function names F_{i} in assignment instructions, and (3) equality with ⊥_{ρ} in a test instruction — all features that are not allowed in flowcharts. But \overline{P} is a convenient description of a “parallel evaluation” of P, which we explain further below, and suggests the later transition to iterative form.

Let the signature of P and \overline{P} be Σ_{A}, and assume there is a fixed Σ_{A}-structure A over which P and \overline{P} are interpreted. It is clear how to carry out the computation of \overline{P} relative to an interpretation ⟨A, a⟩, once we introduce a reduction rule (⊥-reduction) and modify the other rules to account for the presence of the special symbols ⊥_{σ}. These are shown in Figure 8.

To explain more carefully the relationship between P and \overline{P}, we first define an operation φ on terms relative to P = {F_{i} = M_{i}}_{1⩽i⩽ℓ}. (We should perhaps identify the dependence of φ on P by writing “φ^{P}”, for example, but “φ” is more economical.) We only consider terms N where all function names are from the set {F_{1}, …, F_{ℓ}}. For every such term N, we define φ(0, N) = N. Proceeding inductively, for arbitrary n ⩾ 0, we define

φ(n + 1, N) = N[F_{1} := φ(n, M_{1}), …, F_{ℓ} := φ(n, M_{ℓ})]

Intuitively, φ(n, N) is obtained from N by “macro expanding” recursive calls to the functions F_{1}, …, F_{ℓ} in parallel and repeatedly down to depth n.^{3} For every

3 This can be called the n-th iterative (or inside-out) expansion of N and corresponds

n ⩾ 0, we define the n-th expansion of P to be the following functional program:

φ(n, P) = {F_{1} = φ(n, M_{1}), …, F_{ℓ} = φ(n, M_{ℓ})}

The 0-th expansion φ(0, P) is none other than P. We define another operation ψ on terms N containing only function names in {F_{1}, …, F_{ℓ}}, given by:

ψ(n, N) = φ(n, N)[F_{1} := ⊥_{σ_{1}}, …, F_{ℓ} := ⊥_{σ_{ℓ}}]

Note ψ(n, N) is a simple term (it does not contain any function names). Returning to the flowchart \overline{P}, the vector

(ψ(n, M_{1}), …, ψ(n, M_{ℓ}))

can be viewed as the state of \overline{P} after its n-th iteration is completed. The following lemmas explain the connection between P and \overline{P}.

Lemma 9. Let P be a functional program as defined above, and ⟨A, a⟩ an interpretation for P.

1. For every n ⩾ 0, the n-th expansion φ(n, P) is equivalent to P.

2. If the evaluation of (F_{1}a) converges, i.e. (F_{1}a) ⟶ ⟶ b for some ground constant b of type ρ, then there is n ⩾ 0 such that δ, if, β-nf(φ(n, M_{1}a)) = b.

3. If the evaluation of (F_{1}a) diverges, then δ, if, β-nf(φ(n, M_{1}a)) is not a simple term for every n ⩾ 0.

Proof. A rigorous proof of part 1 uses standard techniques of denotational semantics, omitted here. See [14, Chapter 5] or [30, Chapters 9 and 11], among other texts. Parts 2 and 3 follow from general principles on the relationship between P and its successive expansions: If the evaluation of (F_{1}a) converges to b, then for a sufficiently large expansion P′ of P, say

P′ = φ(n, P) = {F′_{1} = φ(n, M_{1}), …, F′_{ℓ} = φ(n, M_{ℓ})}

where n is very large and F_{i} is replaced by F′_{i} throughout, the evaluation of (F′_{1}a) or, equivalently, φ(n, M_{1}a) to b does not involve any P′-reduction step, in which case it suffices to use δ, if and β reduction steps only. Details omitted. ⊓ ⊔

Lemma 10. If N is a closed term of ground type ρ, then for every n ⩾ 0:

to the way \overline{P} works. We can denote it φ_{io}(n, N) to distinguish it from the n-th recursive (or outside-in) expansion of N, which is defined by: φ_{oi}(0, N) = N and φ_{oi}(n + 1, N) = φ_{oi}(n, N)[F_{1} := M_{1}, …, F_{ℓ} := M_{ℓ}] for every n ⩾ 0. A recursive expansion of N corresponds to the way reductions are carried out: Going from φ_{oi}(n, N) to φ_{oi}(n + 1, N) can be expressed as a one-step parallel reduction, because φ_{oi}(n + 1, N) is obtained by simultaneous reduction of all P-redexes in φ_{oi}(n, N). It is a non-trivial exercise, omitted here, to show that φ_{oi}(n, N) = φ_{io}(n, N) for every n ⩾ 0.

1. If δ, if, β-nf(φ(n, N)) is a simple term, then

⊥, δ_{⊥}, if_{⊥}, β-nf(ψ(n, N)) = δ, if, β-nf(ψ(n, N)) = δ, if, β-nf(φ(n, N)) = b

for some ground constant b of type ρ.

2. If δ, if, β-nf(φ(n, N)) is not a simple term, then

⊥, δ_{⊥}, if_{⊥}, β-nf(ψ(n, N)) = ⊥_{ρ}

Proof. As ⊥-reduction, δ_{⊥}-reduction and if_{⊥}-reduction do not introduce β-redexes, carry out all β-reduction steps first in both φ(n, N) and ψ(n, N). The resulting terms P and Q in β-normal form are such that

Q ≡ P [F_{1} := ⊥_{σ_{1}}, …, F_{ℓ} := ⊥_{σ_{ℓ}}]

Then carry out all δ-reduction and if-reduction steps (not δ_{⊥}-reduction and if_{⊥}- reduction steps) in both P and Q. The resulting P′ and Q′ in δ, if, β-normal form are such that:

Q′ ≡ P′[F_{1} := ⊥_{σ_{1}}, …, F_{ℓ} := ⊥_{σ_{ℓ}}]

Q′ is a simple term, possibly containing the special symbols ⊥_{σ}. The argument so far does not use the hypothesis that N is closed of ground type. With this hypothesis, Q′ can be ⊥, δ_{⊥}, if_{⊥}-reduced to ⊥_{ρ} or else to a ground constant b of type ρ. In the first case, P′ and therefore φ(n, N) are not simple terms. In the second case, it must be that P′ ≡ Q′ ≡ b. ⊓ ⊔

Lemma 11. Consider the computation of P over an interpretation ⟨A, a_{1}, …, a_{k}⟩.

1. If (F_{1}a_{1} ⋯ a_{k}) ⟶ ⟶ b where b is a ground constant of type ρ, then there is n ⩾ 0 such that ⊥, δ_{⊥}, if_{⊥}, β-nf(ψ(n, M_{1}a_{1} ⋯ a_{k})) = b.

2. If (F_{1}a_{1} ⋯ a_{k}) diverges, then ⊥, δ_{⊥}, if_{⊥}, β-nf(ψ(n, M_{1}a_{1} ⋯ a_{k})) = ⊥_{ρ} for every n ⩾ 0.

This establishes that \overline{P} simulates P correctly, because if \overline{P} is executed over the interpretation ⟨A, a_{1}, …, a_{k}⟩, then ⊥, δ_{⊥}, if_{⊥}, β-nf(ψ(n, M_{1}a_{1} ⋯ a_{k})) is exactly the value assigned to variable z at the (n + 1)-st iteration of the loop, for n ⩾ 0.

Proof. This is an immediate consequence of the two preceding lemmas. ⊓ ⊔

In the form of a functional program, again not legal in our formalism, \overline{P} can be written as

G x = H x ⊥_{ρ} ⊥_{σ_{1}} ⋯ ⊥_{σ_{ℓ}}
H x z F_{1} ⋯ F_{ℓ} = if (z ≠ ⊥_{ρ}) then (F_{1}x) else H x (F_{1}x) M_{1}^{•} ⋯ M_{ℓ}^{•}

by a straightforward application of the McCarthy method (Proposition 8), where x = x_{1} ⋯ x_{k} and M_{i}^{•} is M_{i} with F_{1}, …, F_{ℓ} replaced by F_{1}, …, F_{ℓ}, respectively, and G and H are fresh function names with the following types:

G : ∗^{k} → ρ
H : ∗^{k} → ρ → σ_{1} → ⋯ → σ_{ℓ} → ρ

The challenge here is how to turn \overline{P} into a legal functional program, in particular how to simulate the artificial symbols ⊥_{σ}. For this, we first transform P into ((P)), which incorporates an appropriate simulation of ⊥_{σ}. In a second stage, we transform ((P)) into iter(P), the final iterative form of P.

The transformation (( )) is defined in Figure 9. If P mentions object variable v (resp. function name F), then ((P)) mentions both v (resp. F) and a fresh object variable \underline{v} (resp. fresh function name \underline{F}). If P = \{F_{i} = M_{i}\}_{1⩽i⩽ℓ} then ((P)) is the program:

((P)) = \{ F_{i} = M_{i} \}_{1⩽i⩽ℓ} ∪ \{ \underline{F_{i}} = ((M_{i})) \}_{1⩽i⩽ℓ}

Note that P and ((P)) are over the same signature. It is clear what φ(n, ((N))) means for an arbitrary n ⩾ 0 and arbitrary term N containing function names only in \{F_{1}, \underline{F_{1}}, …, F_{ℓ}, \underline{F_{ℓ}}\}. We define one more operation ψ′ on such a term N:

ψ′(n, ((N))) = φ(n, ((N)))[F_{1} := c_{σ_{1}}, \underline{F_{1}} := Ω_{σ_{1}}, …, F_{ℓ} := c_{σ_{ℓ}}, \underline{F_{ℓ}} := Ω_{σ_{ℓ}}]

where Ω_{σ} is defined Figure 9, and if σ ≡ τ_{1} → ⋯ → τ_{k} → ρ with k ⩾ 1 and ρ ∈ {∗, bool}, then c_{σ} is defined as

c_{σ} ≡ (λv_{1} : τ_{1}. · · · .λv_{k} : τ_{k}. a)

where a is an arbitrary, but otherwise fixed throughout the rest of this section, ground constant of type ρ. The following lemmas relate P and ((P)).

Lemma 12. If N is a closed term of ground type ρ, then for every n ⩾ 0:

1. If δ, if, β-nf(φ(n, N)) is a simple term, then δ, if, β-nf(φ(n, ((N)))) = tt.

2. If δ, if, β-nf(φ(n, N)) is not a simple term, then neither is δ, if, β-nf(φ(n, ((N)))).

Proof. First prove that if P ⟶ Q then ((P)) ⟶ ⟶ ((Q)), by considering each kind of reduction step separately: δ, if and β. Details omitted. This implies that

δ, if, β-nf(φ(n, ((N)))) = ((δ, if, β-nf(φ(n, N))))

The two parts of the lemma now follow from the fact that if δ, if, β-nf(φ(n, N)) is simple, then it must be a ground constant b of type ρ. ⊓ ⊔

Lemma 13. If N is a closed term of ground type ρ, then for every n ⩾ 0:

1. If δ, if, β-nf(φ(n, ((N)))) is simple, then δ, if, β-nf(ψ′(n, ((N)))) = δ, if, β-nf(φ(n, ((N)))) = tt.

2. If δ, if, β-nf(φ(n, ((N)))) is not simple, then δ, if, β-nf(ψ′(n, ((N)))) = ff.

Proof. This is a consequence of the definition of ψ′(n, ((N))) from φ(n, ((N))). The details are similar to the details in the proof of Lemma 10. We only give an outline. As δ-reduction and if-reduction do not introduce β-redexes, carry out all β-reduction steps first in both φ(n, ((N))) and ψ′(n, ((N))). The resulting terms P and Q in β-normal form are such that

Q ≡ P [F_{1} := c_{σ_{1}}, \underline{F_{1}} := Ω_{σ_{1}}, …, F_{ℓ} := c_{σ_{ℓ}}, \underline{F_{ℓ}} := Ω_{σ_{ℓ}}]

treating every c_{σ}, resp. Ω_{σ}, as a formal constant of type σ, resp. ((σ)). Then carry out all δ-reduction and if-reduction steps in both P and Q. The resulting P′ and Q′ in δ, if, β-normal form are such that:

Q′ ≡ P′[F_{1} := c_{σ_{1}}, \underline{F_{1}} := Ω_{σ_{1}}, …, F_{ℓ} := c_{σ_{ℓ}}, \underline{F_{ℓ}} := Ω_{σ_{ℓ}}]

Q′ is a simple term, possibly containing the special symbols c_{σ} and Ω_{σ}. The argument so far does not use the hypothesis that N is closed of ground type. With this hypothesis, and after macro expanding each c_{σ} and each Ω_{σ}, Q′ can be δ, if, β-reduced to tt or ff. In the first case, it must be that P′ ≡ Q′ ≡ tt. In the second case, P′ and therefore φ(n, ((N))) are not simple terms. ⊓ ⊔

Lemma 14. Consider the computation of P over an interpretation ⟨A, a_{1}, …, a_{k}⟩.

1. If (F_{1}a_{1} ⋯ a_{k}) ⟶ ⟶ b where b is a ground value of type ρ, then there is n ⩾ 0 such that δ, if, β-nf(ψ′(n, ((M_{1})) tt a_{1} ⋯ tt a_{k})) = tt.

2. If (F_{1}a_{1} ⋯ a_{k}) diverges, then δ, if, β-nf(ψ′(n, ((M_{1})) tt a_{1} ⋯ tt a_{k})) = ff for every n ⩾ 0.

Proof. Immediate consequence of Lemma 9, 12 and 13. ⊓ ⊔

The earlier construction of \overline{P} from P suggests a similar construction of “flowchart” \overline{((P))} from ((P)), shown in Figure 7, the correctness of which follows from Lemma 14. Note that if \overline{((P))} is executed relative to the interpretation ⟨A, a_{1}, …, a_{k}⟩, then

δ, if, β-nf(ψ′(n, ((M_{1})) tt a_{1} ⋯ tt a_{k}))

is precisely the value assigned to variable z at the (n + 1)-st iteration of the loop of \overline{((P))}, for every n ⩾ 0.

In the form of a functional program, \overline{((P))} is basically the desired iterative form of P, denoted iter(P). The formal definition of iter(P) is given next.

Definition 15 (Transformation to Iterative Form). Let P be the finitely typed functional program {F_{i} = M_{i}}_{1⩽i⩽ℓ} where:

— F_{1} : σ_{1}, …, F_{ℓ} : σ_{ℓ} for some σ_{1}, …, σ_{ℓ} ∈ 𝕋_{fin},

— F_{1} is the distinguished function name and σ_{1} ≡ ∗^{k} → ρ for some k ⩾ 1 and ρ ∈ {∗, bool}.

The iterative form iter(P) of P is the following functional program:

G x = H x ff c_{σ_{1}} Ω_{σ_{1}} ⋯ c_{σ_{ℓ}} Ω_{σ_{ℓ}}
H x z F_{1} \underline{F_{1}} ⋯ F_{ℓ} \underline{F_{ℓ}} = if z then (F_{1} x_{1} ⋯ x_{k}) else
H x (\underline{F_{1}} tt x_{1} ⋯ tt x_{k}) M_{1}^{•} ((M_{1}))^{•} ⋯ M_{ℓ}^{•} ((M_{ℓ}))^{•}

where 1. x = x_{1} ⋯ x_{k}.

2. F_{1} : σ_{1}, \underline{F_{1}} : ((σ_{1})), …, F_{ℓ} : σ_{ℓ}, \underline{F_{ℓ}} : ((σ_{ℓ})) are fresh variables.

3. M_{i}^{•} is M_{i} with F_{1}, …, F_{ℓ} replaced by F_{1}, , …, F_{ℓ}, respectively.

4. ((M_{i}))^{•} is ((M_{i})) with F_{1}, \underline{F_{1}}, …, F_{ℓ}, \underline{F_{ℓ}} replaced by F_{1}, \underline{F_{1}}, …, F_{ℓ}, \underline{F_{ℓ}}.

5. G and H are fresh function names with the following types:

G : ∗^{k} → ρ
H : ∗^{k} → bool → σ_{1} → ((σ_{1})) → ⋯ → σ_{ℓ} → ((σ_{ℓ})) → ρ

Theorem 16. Every finitely typed functional program P of order n ⩾ 1 can be translated into an equivalent iterative program iter(P) of order n + 1.

Proof. Let P = {F_{i} = M_{i}}_{1⩽i⩽ℓ} as in Definition 15. The equivalence of P and iter(P) follows from the preceding discussion. To check that iter(P) is in iterative form is a straightforward inspection of its definition. Finally, if order(P) = n, we can take:

n = max{order(F_{1}), …, order(F_{ℓ})} = max{order(σ_{1}), …, order(σ_{ℓ})}

See Definition 3. This implies:

order(iter(P)) = order(H)
= order(∗^{k} → bool → σ_{1} → ((σ_{1})) → ⋯ → σ_{ℓ} → ((σ_{ℓ})) → ρ)
= n + 1

The last equality (to n + 1) is immediate from the definition of order. ⊓ ⊔

Example 6. Consider again the Paterson-Hewitt program P in Example 4. P consists of a single function definition {F = M}, where

M ≡ (λx.if px then x else g(F(Lx))(F(Rx)))

The functional program iter(P) is the following second-order iterative program:

Gx = H x ff (λv.x) (λ\underline{w}.λw.ff )
HxzF \underline{F} = if z then F x else H x (\underline{F} tt x) N P

where G and H are fresh function names with the following types:

G : ∗ → ∗
H : ∗ → bool → (∗ → ∗) → (bool → ∗ → bool) → ∗

and N and P are the following terms:

N ≡ λx. if px then x else g(F (Lx))(F (Rx))
P ≡ λ\underline{x}.λx. if \underline{x} then (if px then \underline{x} else (and (\underline{F} \underline{x} (Lx)) (\underline{F} \underline{x} (Rx)))) else ff

N is simply M with function name F replaced by variable F, and P is ((N)). ⊓ ⊔

Open Problem. Extend the transformation (( )) to polymorphically typed functional programs. Define the iterative form iter(P) of a polymorphically typed P based on this extension of (( )).

6 Polymorphic Iteration

We prove that there are polymorphically typed iterative programs that cannot be translated into equivalent finitely typed functional programs. We start with an example of a polymorphically typed iterative program P, which we use in the proof of Theorem 17.

Example 7. P is the following polymorphically typed functional program:

Fx = Gxfa
GxF Z = if rx then F Z else G(fx)(λv.λw.v(vw))F Z

The types of the symbols in the signature Σ = {f, r}, the ground constant a, the variables {x, v, w, F, Z}, and the function names {F, G} are

a, x : ∗
f : ∗ → ∗
r : ∗ → bool
v, F : α → α
w, Z : α
F : ∗ → ∗
G : ∗ → (α → α) → α → α

The instance of G in the definition for F has type

∗ → (∗ → ∗) → ∗ → ∗

The instance of G in the definition for G has type

∗ → ((α → α) → (α → α)) → (α → α) → (α → α)

Noting that P is in iterative form, what we have in this example is a case of polymorphic iteration. If n is the least natural number such that r(f^{(n)}x) is tt, we have the following converging computation:

Fx ⟶ ⟶ G x f a
⟶ ⟶ G (fx) 2 f a
⟶ ⟶ G (f^{(2)}x) 2 2 f a
⟶ ⟶ ⋯
⋮
⟶ ⟶ G (f^{(n)}x) \underbrace{2 ⋯ 2}_{n} f a
⟶ ⟶ \underbrace{2 ⋯ 2}_{n} f a ≡ \underbrace{f(f ⋯ (f a) ⋯)}_{e(n)} ≡ (f^{(e(n))} a)

where 2 denote the term (λv.λw.v(vw)), and the function e is given by e(0) = 1 and e(n + 1) = 2^{e(n)} for all n ⩾ 0. Each call to G in the computation is at a different type. An explicitly typed intermediate term in this computation is (types inserted as superscripts):

G^{∗→∗[k+1]→∗[k+1]} (f^{(k)}x)∗ 2^{∗[k+1]} 2^{∗[k]} ⋯ 2^{∗[2]} f^{∗[1]} a∗

where 0 ⩽ k ⩽ n and we use the following type abbreviations: ∗[0] = ∗ and ∗[k + 1] = (∗[k] → ∗[k]). Note that because the program is polymorphic, G is repeatedly applied to finitely typed arguments with increasingly complex types. This example is adapted from [15, Example 5.3]. ⊓ ⊔

Theorem 17. There is a polymorphically typed iterative program P which is not equivalent to any finitely typed functional program.

Proof. ^{4} The desired P is the program given in Example 7. It suffices to show for every finitely typed functional program Q of order n ⩾ 1, over the signature Σ of P, there is a Σ_{A}-structure A such that P^{A} ≠ Q^{A}. We choose A to be of the form ⟨{a_{1}, …, a_{u}} ∪ ℕ, r, f⟩ where u is a positive integer (to be appropriately selected depending on Q), ℕ is the set of natural numbers, r is the predicate such that (r x) = tt iff x = a_{u}, and f is the function: (f a_{i}) = a_{i+1} for 1 ⩽ i < u, (f a_{u}) = a_{u}, and (f i) = i + 1 for every i ∈ ℕ.

P mentions only one ground constant, namely a, while Q may mention a as well as several other ground constants. We choose a to be 0 in ℕ, and we can always define A so that all the other ground constants mentioned by Q are in {a_{1}, …, a_{u}}. No matter what the value of u is, the computation of P over the interpretation ⟨A, a_{1}⟩ converges and returns the value:

(f^{(e(u))} a) = (f^{(e(u))} 0) = e(u)

by the analysis in Example 7. We need to select u large enough so that the computation of Q, over the same interpretation ⟨A, a_{1}⟩, either diverges or converges and returns a value ≠ e(u). By Theorem 16, we can restrict Q to be in iterative form. We can therefore write Q in the form of an order-n flowchart consisting of, say, k ⩾ 1 instructions and ℓ ⩾ 1 variables, all of order < n. As there is no “communication” between the elements in {a_{1}, …, a_{u}} and the elements in ℕ, the behavior of Q is entirely determined by the substructure B = ⟨{a_{1}, …, a_{u}}, r, f⟩, i.e. it is not difficult to check that the computation of Q over the interpretation ⟨A, a_{1}⟩ converges iff the computation of Q over the interpretation ⟨B, a_{1}⟩ converges.

Define the function exp such that exp(0, n) = n and exp(m+1, n) = 2^{exp(m,n)}, for all m, n ∈ ℕ. It is not difficult to show there is a fixed polynomial ζ : ℕ → ℕ such that if v : σ is a variable in Q and order(σ) = m ⩾ 0, then v will be assigned at most exp(m, ζ(u)) distinct values, i.e. functions of type σ over the universe {a_{1}, …, a_{u}}, in the course of the computation of Q over the interpretation ⟨B, a_{1}⟩. If a state of this computation consists of an instruction label (k of them) in Q, together with the values assigned to the ℓ variables in Q, then k · (exp(n, ζ(u)))^{ℓ} is an upper bound on the number of distinct states

4 Joint with Paweł Urzyczyn.

that Q can visit in the course of its computation. If a state is repeated, the computation is doomed to diverge. Noting that k, ℓ and n depend on Q and are therefore fixed in this proof, let ξ(u) = k · (exp(n, ζ(u)))^{ℓ}. Suppose z : ∗ is a variable in Q which is assigned the final output, if any. The value assigned to z can be changed at most ξ(u) times in the course of a converging computation of Q, now over ⟨A, a_{1}⟩. Using the fact that a finitely-typed simple term M reduces to normal form in at most exp(|M|, |M|) steps, see [7, 8, 26], the final value assigned to z cannot exceed exp(p · ξ(u), p · ξ(u)) for some p ∈ ℕ depending on Q. The desired conclusion now follows, because e(u) > exp(p · ξ(u), p · ξ(u)) for sufficiently large u. ⊓ ⊔

7 Hierarchies

Let C_{1} and C_{2} be classes of functional programs over the same signature. Recall that the equivalence of programs is relative to their call-by-name semantics (Definition 4). We write C_{1} ⩽ C_{2} if:

(∀P_{1} ∈ C_{1}) (∃P_{2} ∈ C_{2}) [ P_{1} and P_{2} are equivalent ]

We write C_{1} < C_{2} iff C_{1} ⩽ C_{2} but C_{2} ⩽̸ C_{1}.

The results of Sections 5 and 6 do not presume that the signature Σ of programs contains a symbol eq : ∗^{2} → bool which is always interpreted as the equality relation on the universe A of a Σ_{A}-structure. To compare the hierarchies {ITER_{n}} and {REC_{n}}, and use the results of [15], we now assume the existence of such a symbol eq. It is easy to see that Theorems 16 and 17 imply the following computational hierarchy:

ITER_{1} < REC_{1} ⩽ ITER_{2} ⩽ REC_{2} ⩽ ITER_{3} ⩽ REC_{3} ⩽ ⋯ < p-ITER ⩽ p-REC

The strictness of the first level, ITER_{1} < REC_{1}, is the classical result of Paterson and Hewitt [22]. Using the already known fact that REC_{n} < REC_{n+1} for every n ⩾ 1, see [15, Theorem 3.9], we can conclude:

Theorem 18. ITER_{1} < ITER_{3} < ITER_{5} < ⋯ < ITER < p-ITER (odd orders)
Theorem 19. ITER_{2} < ITER_{4} < ITER_{6} < ⋯ < ITER < p-ITER (even orders)

Although we are not yet able to separate two consecutive levels in this hierarchy, we have thus shown that increasing the order of finitely-typed iterative programs results in a net gain of computational power, and adding polymorphic iteration results in a further gain of computational power. Based on the preceding, it is only natural to state the following.

Conjecture. ITER_{1} < ITER_{2} < ITER_{3} < ITER_{4} < ⋯ (all orders)

To settle this conjecture, we can proceed in one of two ways to prove that consecutive levels of the hierarchy {ITER_{n}} can indeed be separated. This is similar to the situation in the first-order case, where separation results can be established in two different ways, depending on whether “counting” or “pebbling” is used. The first approach is to sharpen the counting arguments we have used so far, with a view to separate consecutive levels in the hierarchy. The second approach, more problematic at this point, is to try some kind of pebbling argument.

This clearly raises the question of how to define a higher-order pebble game. We can define it with the aim to directly show that:

(1) ITER_{n} < ITER_{n+1} for every n ⩾ 1,

or, using the already established reduction REC_{n} ⩽ ITER_{n+1} of Theorem 16, the stronger result that:

(2) ITER_{n} < REC_{n} for every n ⩾ 1.

In both cases there are several technical issues to be sorted out. Any of these two results, (1) or (2), will settle the strictness of the hierarchy {ITER_{n}} for all orders. Moreover, any of these two results will also imply that the hierarchy {REC_{n}} is infinite, already shown in [15] by different techniques: If (1) is true, then the even orders and odd orders of {REC_{n}} form two infinite strict hierarchies; if (2) is true, then all orders of {REC_{n}} form a single infinite strict hierarchy.

References

1. Abelson, H., and Sussman, G., Structure And Interpretation Of Computer Progams, MIT Press/McGraw-Hill, NY, 1984.

2. Aho, A.V. and Ullman, J.D., Principles of Compiler Design, Addison-Wesley, 1979.

3. Auslander, M.A., and Strong, H.R., “Systematic recursion removal”, Communications ACM , 21, no. 2, pp 127-134, Feb 1978.

4. Barendregt, H.P., The Lambda Calculus, Its Syntax and Semantics, revised edition, North-Holland, Amsterdam, 1984.

5. Böhm, C., and Berarducci, A., “Automatic synthesis of typed lambda-programs on term algebras”, Theoretical Computer Science, 39, pp 135–154, 1985.

6. Friedman, D.P., Wand, M., and Haynes, C.T., Essentials of Programming Languages, MIT Press/McGraw-Hill, NY, 1992.

7. Gandy, R.O., “An early proof of normalization by A.M. Turing”, in To H.B. Curry: Essays on Combinatory Logic, Lambda Calculus, and Formalism, eds. Seldin and Hindley, pp 453-455, Academic Press, 1980.

8. Gandy, R.O., “Proofs of strong normalization”, in To H.B. Curry: Essays on Combinatory Logic, Lambda Calculus, and Formalism, eds. Seldin and Hindley, pp 457-477, Academic Press, 1980.

9. Goerdt, A., “On the computational power of the finitely typed lambda-terms”, in Proceedings of 13th MFCS, LNCS 324, pp 318-328, 1988.

10. Greibach, S.A., Theory of Program Structures: Schemes, Semantics, Verification, LNCS 36, Springer-Verlag, 1975.

11. Henderson, P., Functional Programming, Application and Implementation, Prentice-Hall, 1980.

12. Hillebrand, G.G., Kanellakis, P.C., Mairson, H.G., and Vardi, M.Y., “Undecidable Boundedness Problems for Datalog Programs”, Journal of Logic Programming 25:2, pp 163-190, 1995.

13. Kamin, S.N., Programming Languages: An Interpreter-Based Approach, Addison-Wesley, 1990.

14. Kfoury, A.J., Moll, R.N., and Arbib, M.A., A Programming Approach to Computability, Springer-Verlag, 1982.

15. Kfoury, A.J., Tiuryn, J., and Urzyczyn, P., “On the expressive power of finitely typed and universally polymorphic recursive procedures”, Theoretical Computer Science, 93, pp 1-41, 1992.

16. Kfoury, A.J., “Recursion, Tail-Recursion, and Iteration at Higher-Orders”. In preparation.

17. Kozen, D., and Tiuryn, J., “Logics of Programs”, in Handbook of Theoretical Computer Science, Vol. B, Formal Methods and Semantics, ed. J. van Leeuven, Elsevier Science Publ. and The MIT Press, pp 789–840, 1990.

18. McCarthy, J. , “Recursive Functions of Symbolic Expressions and Their Computation by Machine”, Comm. ACM , 3 (4), pp 184-195, 1960.

19. Mitchell, J.C., Foundations for Programming Languages, MIT Press, Cambridge, Mass, 1996.

20. Moschovakis, Y.N., Elementary Induction on Abstract Structures, North-Holland, 1974.

21. Moschovakis, Y.N., “The Formal Language of Recursion”, Journal of Symbolic Logic, 54, pp 1216-1252, 1989.

22. Paterson, M.S., and Hewitt, C., “Comparative schematology”, MIT A.I. Lab Technical Memo No. 201 (also in Proc. of Project MAC Conference on Concurrent Systems and Parallel Computation), 1970.

23. Peyton Jones, S.L., The Implementation of Functional Programming Languages, Prentice-Hall, 1987.

24. Pippenger, N., “Pebbling”, Fifth Symposium on Mathematical Foundations of Computer Science, IBM Japan, 1980.

25. Pippenger, N., “Advances in Pebbling”, Proc. of 9th ICALP, LNCS no. 140, Springer-Verlag, 1982.

26. Statman, R., “The typed λ-calculus is not elementary recursive”, Theoretical Computer Science, 9, pp 73-81, 1979.

27. Strong, H.R., “Translating recursion equations into flowcharts”, J. Computer and System Sciences, 5, pp 254-285, 1971.

28. Urzyczyn, P., “Non-trivial definability by flowchart programs”, Information and Control, 58, nos. 1-3, pp 59-87, Sept 1983.

29. Walker, S.A. and Strong, H.R., “Characterizations of flowchartable recursions”, J. Computer and System Sciences, 7, pp 404-447, 1973.

30. Winskel, G, The Formal Semantics of Programming Languages: An Introduction, The MIT Press, 1993.

Recursion vs. Iteration at Higher Orders 25

Ground constants c : ρ  type(c) = ρ
δ-terms  \frac{N_{1} : ∗ ⋯ N_{k} : ∗}{(fN_{1} ⋯ N_{k}) : ρ}  type(f) = ∗^{k} → ρ
if-terms  \frac{N_{1} : bool  N_{2} : τ  N_{3} : τ}{(if N_{1} N_{2} N_{3}) : τ}
Variables  v : τ  type(v) = τ
Function names F^{τ} : τ  type(F) = σ ≼ τ
Applications  \frac{M : σ → τ  N : σ}{(M N) : τ}
Abstractions  \frac{M : τ}{(λv : σ. M) : (σ → τ)}  type(v) = σ
Programs  \frac{M_{1} : σ_{1}  M_{2} : σ_{2}  ⋯  M_{ℓ} : σ_{ℓ}}{\{F_{1} = M_{1}, F_{2} = M_{2}, …, F_{ℓ} = M_{ℓ}\}}
M_{i} is a closed term and type(F_{i}) = σ_{i} for i ∈ {1, …, ℓ}

Fig. 1. Rules for well-typed terms and programs. Throughout, ρ ∈ {∗, bool}.

This article was processed using the L^{A}TEX macro package with LLNCS style

((λv N) P) ⟶_{A,P} N[v := P]  (β-reduction)
F_{i} ⟶_{A,P} M_{i}  (P-reduction)

(if b then N else P) ⟶_{A,P} \{ \begin{matrix}N, & if b = tt, \\ P, & if b = ff. \end{matrix} (if-reduction)
(f a_{1} ⋯ a_{k}) ⟶_{A,P} a_{k+1}  (δ-reduction)

\frac{N ⟶_{A,P} P}{(NQ) ⟶_{A,P} (P Q)}

\frac{N ⟶_{A,P} P}{(QN) ⟶_{A,P} (QP)}

\frac{N ⟶_{A,P} P}{(λv N) ⟶_{A,P} (λv P)}

Fig. 2. Reduction rules for program P = {F_{i} = M_{i}}_{1⩽i⩽ℓ} .

[figure: input x; 1:; (v, F) := (x, f); pv ?; ff; tt; (v, F) := (F v, λy.F^{(2)}y); z := hv; 2:; (v, F) := (x, f); pv ?; ff; output x; tt; (v, F) := (F v, λy.F^{(2)}y); (w_{1}, G) := (v, F); (w_{2}, H) := (x, f); pw_{1} ?; ff; tt; (w_{1}, G) := (Gw_{1}, λy.G^{(2)}y); (w_{2}, H) := (Hw_{2}, λy.H^{(2)}y); z := gw_{2}z]

Fig. 3. Flowchart for Example 2.

[figure: input x, y; F := λz.z; px ?; tt; output F y; ff; F := λz.g(F (Lz))(F (Rz)); x := fx]

Fig. 4. Flowchart for Example 3.

[figure: input x; P:; n := φ(p, L, R); k := 0; F := λz.z; k = n ?; tt; output F x; ff; F := λz.if pz then z else g(F (Lz))(F (Rz)); k := k + 1]

Fig. 5. Flowchart for Example 4.

[figure: input x_{1} ⋯ x_{k}; (F_{1}, …, F_{ℓ}) := (⊥_{σ_{1}}, …, ⊥_{σ_{ℓ}}); (F_{1}, …, F_{ℓ}) := (M_{1}, …, M_{ℓ}); z := F_{1}x_{1} ⋯ x_{k}; z ≠ ⊥_{ρ} ?; ff; tt; output z]

Fig. 6. Flowchart \overline{P}.

[figure: input x_{1} ⋯ x_{k}; (F_{1}, \underline{F_{1}}, …, F_{ℓ}, \underline{F_{ℓ}}) := (c_{σ_{1}}, Ω_{σ_{1}}, …, c_{σ_{ℓ}}, Ω_{σ_{ℓ}}); (F_{1}, \underline{F_{1}}, …, F_{ℓ}, \underline{F_{ℓ}}) := (M_{1}, ((M_{1})), …, M_{ℓ}, ((M_{ℓ}))); z := \underline{F_{1}} tt x_{1} ⋯ tt x_{k}; z ?; ff; tt; output F_{1} x_{1} ⋯ x_{k}]

Fig. 7. Flowchart \overline{((P))}.

(⊥_{σ→τ} N) ⟶_{A,P} ⊥_{τ}  (⊥-reduction)
(if^{τ} b then N else P) ⟶_{A,P} \{ \begin{matrix}N, & if b = tt, \\ P, & if b = ff. \\ ⊥_{τ} , & if b = ⊥_{bool}. \end{matrix} (if_{⊥}-reduction)
(f a_{1} ⋯ a_{k}) ⟶_{A,P} \{ \begin{matrix}a_{k+1}, & if ⊥∗ ∉ \{a_{1}, …, a_{k}\}, \\ ⊥_{ρ}, & if ⊥∗ ∈ \{a_{1}, …, a_{k}\}. \end{matrix}  (δ_{⊥}-reduction)

Fig. 8. Reduction rules in the presence of the special symbols ⊥_{σ}: Add rule (⊥-reduction), and adjust rules (if-reduction) and (δ-reduction).

Read with Figure 2.

Types  ((∗)) = bool
((bool)) = bool
((σ → τ)) = ((σ)) → σ → ((τ))

Special symbols  Ω∗ ≡ ff : bool
Ω_{bool} ≡ ff : bool
Ω_{σ→τ} ≡ (λ\underline{v} : ((σ)).λv : σ. Ω_{τ} ) : ((σ → τ))

Terms  ((c : ρ)) = tt : ((ρ))
((fN_{1} ⋯ N_{k} : ρ)) = and ((N_{1})) ⋯ ((N_{k})) : ((ρ))
((if N_{1} N_{2} N_{3} : τ)) = (if ((N_{1})) ( if N_{1} ((N_{2})) ((N_{3})) ) Ω_{τ} ) : ((τ))
((v : τ)) = \underline{v} : ((τ))
((F : τ)) = \underline{F} : ((τ))
((MN : τ)) = (((M))((N))N) : ((τ))
((λv : σ.M : σ → τ)) = (λ\underline{v} : ((σ)).λv : σ. ((M))) : ((σ → τ))

Programs \{ F_{1} = M_{1}, …, F_{ℓ} = M_{ℓ}, \underline{F_{1}} = ((M_{1})), …, \underline{F_{ℓ}} = ((M_{ℓ})) \}

Fig. 9. The transformation (( )) of finitely typed functional programs.

Read with Figure 1. Throughout, ρ ∈ {∗, bool}. The boolean operation (and P Q) is shorthand for

(if P (if Q tt ff ) (if Q ff ff )). With several arguments, (and P Q R) is shorthand for (and P (and Q R)).