BRICS RS-95-35 M. Goldberg: Constructing Fixed-Point Combinators Using Application Survival

BRICS

Basic Research in Computer Science

Constructing Fixed-Point Combinators Using Application Survival

Mayer Goldberg

BRICS Report Series RS-95-35 ISSN 0909-0878 June 1995 Copyright \begin{matrix}c \\ ◯ \end{matrix} 1995, BRICS, Department of Computer Science

University of Aarhus. All rights reserved.

Reproduction of all or part of this work is permitted for educational or research use on condition that this copyright notice is included in any copy.

See back inner page for a list of recent publications in the BRICS Report Series. Copies may be obtained by contacting:

BRICS Department of Computer Science University of Aarhus Ny Munkegade, building 540 DK - 8000 Aarhus C Denmark

Telephone: +45 8942 3360
Telefax: +45 8942 3255
Internet: BRICS@daimi.aau.dk

BRICS publications are in general accessible through WWW and anonymous FTP:

http://www.brics.aau.dk/BRICS/
ftp ftp.brics.aau.dk (cd pub/BRICS)

Constructing Fixed-Point Combinators Using Application Survival ^{∗}

Mayer Goldberg Computer Science Department Indiana University ^{†} (mayer@cs.indiana.edu)

June 26, 1995

Abstract

The theory of application survival was developed in our Ph.D. thesis as an approach for reasoning about application in general and selfapplication in particular. In this paper, we show how application survival provides a uniform framework not only for for reasoning about fixed-points, fixed-point combinators, but also for deriving and comparing known and new fixed-point combinators.

1 Introduction

Fixed-points have long been studied in the λ-calculus, and numerous fixedpoint combinators are known, as well as many theorems about the existence of single and mutual fixed points. There does not seem to be, however, a single unified approach to characterise and to construct fixed points and fixedpoint combinators. On the one hand, the behaviours of fixed-point combinators are characterised by Böhm trees, but on the other hand, they give us little information as to how to go about constructing a fixed-point combinator. Böhm’s combinator [Barendregt 85, Item 6.5.4, Page 142], [Stoy 77, Problem 9, Page 77] allows us to generate an infinite sequence of distinct fixed-point combinators starting from a single fixed-point combinator. Although this approach relates Curry’s and Turing’s fixed-point combinators, it does not give us any clues as to how to construct a fixed-point combinator “from scratch.” Klop captured some intuition about constructing fixedpoint combinators, and his playful example [Barendregt 85, Problem 6.8.14, Page 149] can help in constructing a class of fixed-point combinators. As for the rest, we are on our own.

∗This work was completed while visiting BRICS (Basic Research in Computer Science, Centre of the Danish National Research Foundation).

†Bloomington, IN 47405, USA.

We wish for a unified approach that will allow us to generate various fixed-points and fixed-point combinators directly from an equational specification, as well as to explore the various fixed-point combinators and to characterise the differences between them. We believe that some progress towards a unified approach to fixed points is offered by the theory of application survival, developed in our Ph.D. thesis as a tool for reasoning about application in the λ-calculus [Goldberg 95]. It has been successful in dealing with questions that occur in untyped settings, such as questions related to self-application. The theory of application-surviving agents has been applied so far to fixed-point theory, Gödelisation in the untyped λ-calculus, and solving systems of equations.

In this paper, we show how application survival can be used to derive fixed points and fixed-point combinators from equational specifications, as well as to study the differences between various fixed-point combinators.

Section 2 provides a brief overview of application survival. In section 3 we present fixed points in light of application survival.

We shall assume a familiarity with the (untyped) λKβη-calculus, λdefinability, and Böhm trees [Church 41], [Barendregt 85].

The following notation is assumed: ⌜n⌝ is the n-th Church numeral, S^{+} is the successor, and P^{−} is the predecessor on Church numerals [Church 41, Pages 28-30]. zero? is the predicate testing for equality with ⌜0⌝. Throughout this paper we use the combinators I = λx.x and K = λxy.x [Church 41, Pages 10, 58]. We follow [Barendregt 85, Item 2.1.3 (i), Page 22] and let x⃗ = x_{1}, …, x_{n}, where n is implied by the context. Finally, 𝔵 and 𝔶 are the Gothic (Fraktur) letters x and y.

2 Agents

2.1 Preliminaries

2.1.1 Definition: Set of Agents. Let A be a set of λ-expressions, and let R be a set of rules of the form {⟨𝔵, f, 𝔶⟩ : ∃n, m ∈ ℕ, 𝔵 ∈ A^{n}, 𝔶 ∈ A^{m}, f ∈ Λ}.

We call A a set of agents for R, if for all ⟨𝔵 = ⟨x_{1}, …, x_{n}⟩, f, 𝔶 = ⟨y_{1}, …, y_{m}⟩⟩ ∈ R, we have (x_{1} ⋯ x_{n}) = (f (y_{1} ⋯ y_{m})).

Note that by selecting R = ∅ or choosing R such that ∀⟨𝔵, f, 𝔶⟩ ∈ R we have 𝔵 = 𝔶, etc., we can construct trivial sets of agents. This, however, does not trivialise the notion of an agent. 2.1.2 Terminology: Interaction. The application of agents in A according to a rule in R is called an interaction, to set it aside from other kinds of application. 2.1.3 Terminology: Active Agent, Passive Agent. Given an interaction (A_{1} ⋯ A_{n}), the agent A_{1} is called the active agent. An agent that is never used as an active agent is called a passive agent.

Interactions for non-trivial sets of agents are typically defined recursively, and hence some rules represent the base case of a recursion, while others represent an induction step. A rule of the form ⟨𝔵 = ⟨x_{1}, …, x_{n}⟩, f, 𝔶 = ⟨y⟩⟩, represents the base case of the recursion and corresponds to the statement that (x_{1} ⋯ x_{n}) = (f y), from which we see that the application of agents on the left-hand side do not reduce to an application of agents; the process of applications of agents reducing to other applications of agents has terminated. Alternatively, a rule of the form ⟨𝔵 = ⟨x_{1}, …, x_{n}⟩, f, 𝔶 = ⟨y_{1}, …, y_{m>1}⟩⟩ represents the induction step of the recursion, and corresponds to the statement that (x_{1} ⋯ x_{n}) = (f (y_{1} ⋯ y_{m>1})), from which we see that the application on the left-hand side has resulted in an application of agents; The process of applications of agents resulting in applications of agents has continued. The resulting application (y_{1} ⋯ y_{m}) may in turn terminate, by reducing to (f′ z), or it may continue, by reducing to (f′ (z_{1} ⋯ z_{k>1})), where f′ ∈ Λ is some λ-expression, and z, z_{1}, …, z_{k} ∈ A are agents, etc. We express the behaviour of the application on the left-hand side in the induction step by saying that application has been survived. The entire process is referred to as recursive application-survival.

2.2 Some Facts About Agents

2.2.1 Notation: The expression ⟨expression⟩_{⟨variables⟩} is meant to suggest that ⟨variables⟩ are free in ⟨expression⟩. 2.2.2 Convention: Once we use subscripts to tag a given expression with some of its free variables, we will not tag that expression with other free variables. If new variable names appear as subscripts in any future occurrence of a given expression, then that expression will be understood to have been renamed. For example, if having mentioned M_{x}, we now mention M_{y} in a similar context, then M_{y} should be taken as an abbreviation for M_{x}[x := y]. 2.2.3 Definition: [Barendregt 85, Problem 8.5.15, Page 184] A Proper Combinator. A combinator M is a proper combinator if and only if M ≡ λx⃗.Px⃗ where x⃗ = x_{1}, …, x_{n}, and Px⃗ ∈ {x⃗}^{+}.

The reader may have noticed by now that the kinds of applications allowed by our definition of a set of agents are of the form (w_{1} ⋯ w_{k}), i.e. flat, left-associative applications, and may have wondered whether this restriction imposes limitations on what can be expressed in terms of agents. An arbitrary application of λ-expressions from {w_{1}, …, w_{k}} is some expression Mw⃗ ∈ {w⃗}^{+}. The abstraction of w⃗ over M is the proper combinator P ≡ λw⃗.Mw⃗ and specifies an interaction pattern of w_{1}, …, w_{k}, i.e., how we would like these agents to be applied to each other. By combining P with the ordered k-tuple ⟨w_{1}, …, w_{k}⟩, we obtain the k + 1-tuple ⟨P, w_{1}, …, w_{k}⟩, where the corresponding application (P w_{1} ⋯ w_{k}) β-reduces to the desired application Mw⃗. Our definition is thus sufficiently general to allow for any application of ⟨w_{1}, …, w_{k}⟩ in {w⃗}^{+}, either on the right-hand side or the left-hand side of the defining equation for a set of agents. 2.2.4 Observation: It should now become clear why we need to wrap the function f explicitly around the resulting interaction in the definition of an agent, as opposed to choosing a proper combinator that would permute one of the agents to the position of f. The latter approach would require us always to pass f along as one of the agents, and although this is occasionally used, as in for example Turing-style fixed-point combinators, this is not always desirable in general, especially in the case where f is constant over all interactions. 2.2.5 Convention: In light of the above discussion, and in order to simplify the description of an interaction, the proper combinator specifying the pattern of an interaction will remain implicit. 2.2.6 Definition: Information Content. The information content of an agent is the number of free variables it contains. An agent with n free variables is designated as an “n-information agent.” Accordingly, if an agent is a combinator, it is a “0-information agent.” 2.2.7 Theorem: Any n-information agent, where n > 0, can be written as a 1-information agent.

Proof: Let A_{v_{1},...,v_{n}} be some n-information agent. We aggregate v_{1}, …, v_{n} into a store σ represented by the ordered n-tuple [v_{1}, …, v_{n}] with selectors π_{1}^{n}, …, π_{n}^{n}. We now define a 1-information agent A_{σ} equivalent to A_{v_{1},...,v_{n}} as follows:

A_{σ} = ((λv_{1} ⋯ v_{n}.A_{v_{1},...,v_{n}}) (π_{1}^{n} σ) ⋯ (π_{n}^{n} σ))
⟶_{β} A_{v_{1},...,v_{n}}[v_{1} := (π_{1}^{n} σ)] ⋯ [v_{n} := (π_{n}^{n} σ)]

Our theorem follows. ■

Active, 0-information agents act as permutors and associators, taking other agents as arguments in the interaction, and “rearranging” them. The behaviour of active n-information agents, on the other hand, might depend on its free variables: We regard free variables in an agent as information to be accessed and perhaps acted upon by the agent, as well as shared with other agents.

What principles guide the choice between 0-information and n-information agents? The answer depends on the information our agents need to access. We would prefer to use 0-information agents when the information changes from one interaction to another. When the information remains constant between interactions, it would be simpler to code the information into the agent (i.e., use an n-information agent), rather than to apply the agent to the same information repeatedly. In cases where an agent needs to know both variable as well as constant information, we combine the two approaches.

3 Fixed-Point Combinators

A fixed-point combinator is a combinator Φ with the property that for any λ-expression f, the following equality holds:

(Φ f) = (f (Φ f))

It is usually a simple matter to verify that an expression is indeed a fixedpoint combinator (See Theorem 3.4.1); it is not as simple to actually derive one from the above equational specification.

As we establish in 3.2.4, any fixed-point combinator can be described in terms of a non-trivial interaction of agents. We offer below the derivation and analysis of the two best known fixed-point combinators.

3.1 Curry’s and Turing’s Fixed-Point Combinators

3.1.1 Example: Curry’s Y-Combinator. Pick f. We want to find an agent u_{f} that satisfies the single rule ⟨⟨u_{f}, u_{f}⟩, f, ⟨u_{f}, u_{f}⟩⟩, which specifies that (u_{f} \underline{u_{f}}) = \underline{\underline{(f (u_{f} u_{f}))}}. So:

A = {u_{f}}
R = {⟨⟨u_{f}, u_{f}⟩, f, ⟨u_{f}, u_{f}⟩⟩}

We notice that the right-hand side of the equation can be written in terms of the argument to u_{f} by abstracting over it. We can now derive a definition for u_{f} from the underlined and double-underlined expressions: λ\underline{u}.\underline{\underline{(f (u u))}}. The application (u_{f} u_{f}) is a fixed-point of f. In order to get Curry’s fixedpoint combinator we need only abstract over f:

Y_{Curry} = λf.(u_{f} u_{f})
= λf.((λu.(f (u u)))
(λu.(f (u u))))

The approach taken in constructing Curry’s fixed-point combinator is to let u_{f} “know” about f, i.e. to let f be a free variable in the definition of u_{f}: When Y_{Curry} gets applied to f, u_{f} becomes specialised for this particular f. In order to generate a new interaction, u_{f} needs to have access to its own definition, which is then passed on to its single argument in its interaction. 3.1.2 Example: Turing’s Y-Combinator. Pick f. We start with the system

A = {u, f, P }
R = {⟨⟨u, u, f⟩, I, ⟨P, u, f⟩⟩}

where P is the proper combinator λuf.(f (u u f)), and is used to permute the agents. We have only a single rule to satisfy, so that (u \underline{u f}) = \underline{\underline{(I (P u f))}} = \underline{\underline{(P u f)}} = \underline{\underline{(f (u u f))}}. We therefore need to have P ≡ λuf.(f (u u f)). This last equation specifies, as was the case with Curry’s Y-Combinator, a definition for u:

u = λ\underline{uf}.\underline{\underline{(I (P u f))}}
= λ\underline{uf}.\underline{\underline{(P u f)}}
= λ\underline{uf}.\underline{\underline{(f (u u f))}}

Notice how the underlined and double-underlined expressions in the equation that defines the interaction correspond respectively to the underlined and double-underlined expressions in the definition of u. Now:

Y_{Turing} = λf.(u u f) =_{η} (u u)
= ((λuf.(f (u u f)))
(λuf.(f (u u f))))

In this approach, the active agent u neither knows of its own definition, nor the definition of f, and receives them both as arguments (recall Observation 2.2.4). Since f is passed to u, f is treated as an agent, and in the derivation of Y_{Turing} it is indeed included in the set of agents A. It is, however, explicitly excluded from functioning as an active agent by the one rule in R.

3.2 Various Fixed-Point Combinators

Let us begin by considering how we derived the fixed-point combinators in the previous section. The fixed-point of an expression f is an expression of the form: φ_{f} ⟶_{βη} (f (f ⋯)), and has no normal form. To generate an expression that converts to φ_{f} we came up with agents that upon interaction generated an application of f wrapped around an interaction of agents, which in turn would reduce in a similar way to the first interaction, et cetera. In order to derive Y_{Curry} and Y_{Turing}, we defined our agents to generate one application of f after each interaction. If we were merely interested in generating a fixed-point combinator, any number of applications of f would do. Both u_{f} and u need to be able to place f around some interaction, and so they both need access to f. These observations suggest how to combine the effects of Curry’s and Turing’s fixed-point combinator. 3.2.1 Example: A Curry-Turing Fixed-Point Combinator. Let us derive two variations, Φ_{1} and Φ_{2}, of a third kind of fixed-point combinator, which combines both Curry- and Turing-style agents, with their different information-content properties: The Curry-style agent will “know” of the function f, and will interact with two other agents. The Turing-style agent will not “know” of f, and will therefore interact with three other agents. Thus, the pattern of the interactions will be as follows: An application of three agents reduces to an application of four agents, with f wrapped around it; The interaction of four agents reduces to an interaction of three agents, with f wrapped around it, etc. ad infinitum.

Pick f. We want to construct a set of agents A = {u, v_{f}, f, P } for the set of rules

\begin{matrix}R = \{⟨⟨u, u, v_{f}, f⟩, I, ⟨P, u, v_{f}, f⟩, \\ ⟨⟨v_{f}, u, v_{f}⟩, f, ⟨u, u, v_{f}, f⟩⟩\} \end{matrix}

where P = λuvf.(f (v u v)) is a proper combinator we use to permute the agents in one of the interactions. We now have:

(u \underline{u v_{f} f}) = \underline{\underline{(f (v_{f} u v_{f}))}}
(v_{f} \underline{u v_{f}}) = \underline{\underline{(f (u u v_{f} f))}}

We can now define u and v_{f} accordingly, as follows:

u ≡ λ\underline{uvf}.\underline{\underline{(f (v u v))}}
v_{f} ≡ λ\underline{uv}.\underline{\underline{(f (u u v f))}}

As usual now, the underlined and double-underlined expressions in the set of equations correspond to the underlined and double-underlined expressions in the definitions of the agents u and v_{f}. Finally, we can define two fixedpoint combinators, the first initially passing control to the agent u and the

second initially passing control to the agent v_{f}: \begin{matrix}Φ_{1} ≡ λf.(u u v_{f} f) \\ ≡ λf.((λuvf.(f (v u v))) \\ (λuvf.(f (v u v))) \\ (λuv.(f (u u v f))) f) \end{matrix}  \begin{matrix}Φ_{2} ≡ λf.(v_{f} u v_{f}) \\ ≡ λf.((λuv.(f (u u v f))) \\ (λuvf.(f (v u v))) \\ (λuv.(f (u u v f)))) \end{matrix}

3.2.2 Example: Klop’s Fixed-Point Combinator. The following problem is given in [Barendregt 85, Problem 6.8.14, Page 149] and is due to Klop. Given:

£ = λabcdefghijklmnopqstuvwxyzr.r(thisisafixedpointcombinator)
$ = \underbrace{££££££££££££££££££££££££££}_{26 times}

Show that $ is a fixed-point combinator.

It is not difficult to verify that $ is indeed a fixed-point combinator, and to duplicate such an example. Let us put Klop’s problem in the light of our theory of agents.

It should be clear from the Example 3.2.1, that our interactions can be of any size, and that the active agent can interact with several copies of itself. In that case, it has some choice as to which of its arguments to use in constructing the next interaction. The $ combinator is in fact, a Turing-style fixed-point combinator, in which the active agent not only interacts with the function $ is fixing (look at the position of r in the expression of £), but also with 25 copies of itself, represented by {a, …, z}−{r}. The application thisisafixedpointcombinator is nothing more than an application of the active agent t to 25 copies of itself (look at how $ is defined) followed by the function r, which is what we would expect of a Turing-style fixed-point combinator. It is not a coincidence that r appears only in the last position of this is a fixed point combinator because otherwise we would have to guarantee that the above permutation of letters didn’t result in r becoming an active agent.

Finally, Klop was able to write $ as an application containing only £ through an η-reduction similar to what was used in Example 3.1.2. This would not be possible in Curry-style fixed-point combinators, where any one of the agents could function as an active agent.

It should be clear now how similar fixed-point combinators of either the Curry or the Turing style are possible.

Let us consider a more challenging example: 3.2.3 Example: Finding a Fixed Point of an Implicit Function. We would like to define a combinator Φ, which takes f and g and returns the fixed-point (f (g (f (g^{2} (f (g^{3} ⋯)))))). Our agent needs to know of both f and g, which both remain constant, as well as the exponent of g, which will be represented as a Church numeral (recall: (⌜n⌝ g) ⟶_{β} g^{n}), and which will be incremented from interaction to interaction. Therefore, our agent “knows” of f and g and is passed the exponent of g with each interaction. We define our interactions as follows:

A = {u_{f,g}} ∪ {⌜n⌝ : n ∈ ℕ}
R = {⟨ 𝔵_{n} = ⟨u_{f,g}, u_{f,g}, ⌜n⌝⟩,
f_{n} = λx.(f (⌜n⌝ g x)),
𝔶_{n} = ⟨u_{f,g}, u_{f,g}, ⌜n + 1⌝⟩⟩ : n ∈ ℕ}

where R implies

(u_{f,g} \underline{u_{f,g} ⌜n⌝}) = (f_{n} (u_{f,g} u_{f,g} ⌜n + 1⌝))
= \underline{\underline{(f (⌜n⌝ g (u_{f,g} u_{f,g} ⌜n + 1⌝)))}}
⟶_{β} (f (g^{n} (u_{f,g} u_{f,g} ⌜n + 1⌝)))

As usual, we derive a definition for u_{f,g} by joining the underlined and doubleunderlined expressions in the above equation:

u_{f,g} = λ\underline{un}.\underline{\underline{(f (n g (u u (S^{+} n))))}}

Finally we now define Φ in terms of u_{f,g} as follows:

Φ ≡ λfg.(u_{f,g} u_{f,g} ⌜1⌝)
≡ λfg.((λun.(f (n g (u u (S^{+} n)))))
(λun.(f (n g (u u (S^{+} n)))))
⌜1⌝)

Using a pre-existing fixed-point combinator, we would have had to begin with an explicit definition for the function being fixed and then apply to it this fixed-point combinator. Using agents, we simply capture the behaviour we are interested in, without ever bothering to have an explicit definition for the function we’re fixing.

Finally, we extend our derivation of the above fixed-point combinators to all fixed-point combinators. 3.2.4 Theorem: Any fixed-point combinator can be characterised in terms of the behaviour of application-surviving agents.

Proof: Pick a fixed-point combinator Φ. We know that for all g ∈ Λ we have (Φ g) = (g (Φ g)). From the left-hand side of the equation we know: Φ =_{βη} λf.M_{f}. Because of the Böhm tree of Φ (See [Barendregt 85, Page 217]) we know M_{g} =_{β,η} (g^{n} (P Q g)) for some integer n and some P, Q ∈ Λ. We construct our set of agents as follows: Let A = {P, Q, g}, R = {⟨𝔵 = ⟨P, Q, g⟩, f = g^{n}, 𝔶 = ⟨P, Q, g⟩⟩}. Our theorem follows. ■

3.3 Mutual Fixed-Point Combinators

3.3.1 Definition: Mutual Fixed-Point Combinators. The λ-expressions Φ_{1}, …, Φ_{n} are said to be mutual fixed-point combinators if for any λ-expressions x_{1}, …, x_{n} we have:

(Φ_{j} x_{1} ⋯ x_{n}) = (x_{j} (Φ_{1} x_{1} ⋯ x_{n}) ⋯ (Φ_{n} x_{1} ⋯ x_{n})) for all j ∈ {1, …, n}

Multiple fixed-point combinators can be used to express mutual recursion: 3.3.2 Example: Defining the Predicates even?, odd? with Mutual Fixed-Point Combinators. Let Φ_{1}, Φ_{2} be mutual fixed-point combinators. Let

E = λeon.(zero? n T (o (P^{−} n)))
O = λeon.(zero? n F (e (P^{−} n)))

We can now define

even? = (Φ_{1} E O)
odd? = (Φ_{2} E O)

Mutual, or multiple fixed-point combinators^{1} are derived in much the same way as we derived Y_{Curry} and Y_{Turing}, and similar consideration can be given to the information content of the agents involved. We can thus design agents for solving for mutual fixed-points which are of the Curry-style, the Turing-style, or any hybrid of these two approaches, as in Example 3.3.2.1. We offer below a derivation of a Curry-style multiple (n-ary) fixed-point combinator. 3.3.3 Example: Deriving n Curry-style Mutual Fixed-Point Combinators. Pick n λ-expressions x_{1}, …, x_{n}. We need to find n agents u_{x⃗,1}, …, u_{x⃗,n} that satisfy the interaction schema:

R = {⟨⟨u_{x⃗,j}, u_{x⃗,1}, …, u_{x⃗,n}⟩, I, ⟨P_{j}, u_{x⃗,1}, …, u_{x⃗,n}⟩ : j ∈ {1, …, n}}

where P_{j} is given by

P_{j} = λx_{j}u_{1} ⋯ u_{n}.(x_{j} (u_{1} u_{1} ⋯ u_{n}) ⋯ (u_{n} u_{1} ⋯ u_{n}))

so that

(u_{x⃗,j} \underline{u_{x⃗,1} ⋯ u_{x⃗,n}}) = \underline{\underline{(P_{j} u_{x⃗,1} ⋯ u_{x⃗,n})}}
= \underline{\underline{(x_{j} (u_{x⃗,1} u_{x⃗,1} ⋯ u_{x⃗,n}) ⋯ (u_{x⃗,n} u_{x⃗,1} ⋯ u_{x⃗,n}))}}

As usual, we now derive a definition for u_{x⃗,j} by joining the underlined and double-underlined parts of the previous equation:

u_{x⃗,j} = λ\underline{u_{1} ⋯ u_{n}}.\underline{\underline{(x_{j} (u_{1} u_{1} ⋯ u_{n}) ⋯ (u_{n} u_{1} ⋯ u_{n}))}}

Finally, we define the j’th mutual fixed-point combinator as follows:

Φ_{j} = λx_{1} ⋯ x_{n}.(u_{x⃗,j} u_{x⃗,1} ⋯ u_{x⃗,n})

1See [Barendregt 85, 6§5] for a complete treatment of mutual fixed-points.

3.4 Böhm-style Fixed-Point Combinators

A fixed point x of an expression M must satisfy, by definition, (M x) = x. The equality predicate is normally taken to be =_{βη} and so what the above fixed-point equation means is that there exists an expression y, and two finite ordinals m, n, such that y is m βη-reductions away from (M x) and n βη-reductions away from x:

[figure: \begin{aligned}(M x) & & x \\ & y \end{aligned}; m; βη; n; βη]

The finiteness of m and n is built into our notion of equality. This finiteness carries on to the λ-acceptability of the set of all fixed-point combinators: 3.4.1 Theorem: The set of all fixed-point combinators is λ-acceptable.

Hint of Proof: Pick a fixed-point combinator Φ. We know that for any λ-expression x we have (Φ x) = (x (Φ x)). So Φ = λx.(x (Φ x)) (by rule ξ followed by rule η). We know there exist finite ordinals m, n such that

[figure: \begin{aligned}Φ & & λx.(x (Φ x)) \\ & y \end{aligned}; m; βη; n; βη]

By enumerating all pairs of ordinals, and for each pair ⟨m_{j}, n_{j}⟩ reducing Φ and λx.(x (Φ x)) m_{j} and n_{j} β-reductions respectively, and comparing the two (possibly very large) respective sets of λ-expressions, we can arrive at the particular ⟨m, n⟩ for which syntactic equality holds. It follows that the set of all fixed-point combinators is λ-acceptable. ■

If we remove the restriction that m, n be finite, our equality predicate becomes the =_{η,Böhm} predicate which is satisfied when two expressions have the same Böhm tree modulo any number of η-reductions. What we lose by relaxing this requirement that m and n must be finite is the λ-acceptability of the set of fixed-point combinators, which is not needed for the purpose of doing general recursion.

In the following example, we construct Y_{Böhm,Curry}, a semantic but not syntactic fixed-point combinator of the Curry-style. Y_{Böhm,Curry} will not satisfy the equation (Y_{Böhm,Curry} x) = (x (Y_{Böhm,Curry} x)), however (Y_{Böhm,Curry} x) and (x (Y_{Böhm,Curry} x)) have the same Böhm tree. Y_{Böhm,Curry} is sufficient for expressing general recursion.

3.4.2 Example: The Construction of a Curry-Böhm-Style Fixed-Point Combinator. In all the previous examples of fixed-point combinators, the interaction of agents resulted in an identical interaction. One way to make sure that a Böhm-style fixed-point combinator Φ fails to satisfy (Φ M) = (M (Φ M)), i.e. that there is no λ-expression N such that (Φ M) ⟶_{βη}^{m} N and (M (Φ M)) ⟶_{βη}^{n} N, for any integers m and n, is to guarantee that the agent interactions always reduce to a different interaction. One approach is to select agents satisfying the following interaction schema:

(u u ⌜n⌝) = (⌜n⌝ f (u u ⌜n + 1⌝))

Our set of agents is defined as A = {u} ∪ {⌜n⌝ : n ∈ ℕ}, and our rule schema is defined as R = {⟨⟨u, u, ⌜n⌝⟩, f^{n}, ⟨u, u, ⌜n + 1⌝⟩⟩ : n ∈ ℕ}. We now need to define u to satisfy the above schema:

λun.(⌜n⌝ f (u u (S^{+} n)))

And accordingly:

Y_{Böhm,Curry} = λf.((λun.(⌜n⌝ f (u u (S^{+} n))))
(λun.(⌜n⌝ f (u u (S^{+} n))))
⌜1⌝)

It is clear that many other Böhm-style fixed-point combinators are obtainable through simple variations on this scheme. For example, the following is a Turing-Böhm-style fixed-point combinator:

Y_{Böhm,Turing} = ((λunf.(⌜n⌝ f (u u (S^{+} n) f)))
(λunf.(⌜n⌝ f (u u (S^{+} n) f)))
⌜1⌝)

It should also be clear that the set of all Böhm-style fixed-point combinators is not λ-acceptable.

4 Conclusion

While results on fixed points abound, little is known about how these results were obtained. It is trivial to verify that Y_{Curry} and Y_{Turing} are indeed fixedpoint combinators, but mere verification leaves one unsatisfied: How does one come up with such expressions on one’s own?

The theory of application survival [Goldberg 95] provides us with a unified approach to reasoning about fixed-points: Not only can we derive the classical, well-known fixed-point combinators, but we can also construct new ones. Application survival can be used to characterise any fixed-point combinator in terms of how it accesses the information it needs, how it sets up new interactions, and what function gets applied in the interaction. This characterisation is specified equationally. It not only allows us to study the differences between various fixed-point combinators, but also to derive any specific fixed-point combinators.

Acknowledgements

I am grateful to BRICS^{2} for hosting me this summer and for providing a stimulating environment. Thanks are also due to Olivier Danvy, Daniel P. Friedman, and Larry Moss for their comments and encouragement.

The diagrams of Section 3 were drawn with Kristoffer Rose’s XY-pic package.

References

[Barendregt 85] Hendrik P. Barendregt. The Lambda Calculus, Its Syntax and Semantics. North-Holland, 1985.

[Church 41] Alonzo Church. The Calculi of Lambda-Conversion. Princeton University Press, 1941.

[Goldberg 95] [Forthcoming] Mayer Goldberg. Recursive Application-Survival in the λ-Calculus. Ph.D. Thesis, Department of Computer Science, Indiana University, December 1995.

[Stoy 77] Joseph Stoy. Denotational Semantics: The Scott-Strachey Approach to Programming Language Theory. MIT Press, 1977.

2

Basic Research in Computer Science,

Centre of the Danish National Research Foundation.

Recent Publications in the BRICS Report Series

RS-95-35 Mayer Goldberg. Constructing Fixed-Point Combinators Using Application Survival. June 1995. 14 pp.

RS-95-34 Jens Palsberg. Type Inference with Selftype. June 1995. 22 pp.

RS-95-33 Jens Palsberg, Mitchell Wand, and Patrick O’Keefe. Type Inference with Non-structural Subtyping. June 1995. 22 pp.

RS-95-32 Jens Palsberg. Ef�cient Inference of Object Types. June 1995. 32 pp. To appear in Information and Computation. Preliminary version appears in Ninth Annual IEEE Symposium on Logic in Computer Science, LICS ’94 Proceedings, pages 186�195.

RS-95-31 Jens Palsberg and Peter �rb�k. Trust in the λ-calculus. June 1995. 32 pp. To appear in Static Analysis: 2nd International Symposium, SAS ’95 Proceedings, 1995.

RS-95-30 Franck van Breugel. From Branching to Linear Metric Domains (and back). June 1995. 30 pp. Abstract appeared in Engberg, Larsen, and Mosses, editors, 6th Nordic Workshop on Programming Theory, NWPT ’6 Proceedings, 1994, pages 444-447.

RS-95-29 Nils Klarlund. An n log n Algorithm for Online BDD Re�nement. May 1995. 20 pp.

RS-95-28 Luca Aceto and Jan Friso Groote. A Complete Equational Axiomatization for MPA with String Iteration. May 1995. 39 pp.

RS-95-27 David Janin and Igor Walukiewicz. Automata for the μcalculus and Related Results. May 1995. 11 pp. To appear in Mathematical Foundations of Computer Science: 20th Int. Symposium, MFCS ’95 Proceedings, LNCS, 1995.

RS-95-26 Faith Fich and Peter Bro Miltersen. Tables should be sorted (on random access machines). May 1995. 11 pp. To appear in Algorithms and Data Structures: 4th Workshop, WADS ’95 Proceedings, LNCS, 1995.

RS-95-25 S�ren B. Lassen. Basic Action Theory. May 1995. 47 pp.