Discriminating coded lambda terms

Henk Barendregt

Computing Science Institute University of Nijmegen and Department of Software Technology CWI, Amsterdam

Abstract

A coding for a (type-free) lambda term M is a lambda term ⌜M⌝ in normal form such that M (and its parts) can be reconstructed from ⌜M⌝ in a lambda definable way. Kleene[1936] defined a coding ⌜M⌝^{K} and a selfinterpreter E^{K}∈Λ^{∘} such that (Kleene did it for the λI-calculus, but the result is valid also for the λK-calculus)

∀M∈Λ^{∘} E^{K}⌜M⌝^{K} = M.  (1)

In this style one can construct a discriminator Δ^{K}∈Λ^{∘} such that

∀M, N∈Λ Δ^{K}⌜M⌝^{K}⌜N⌝^{K} = \{ \begin{matrix}true & (≡ λxy.x) & if M ≡ N; \\ false & (≡ λxy.y) & else. \end{matrix} (2)

The terms E^{K} and Δ^{K} are complicated. E^{K} appears also in Church [1941] under the name form. They depend on the lambda definability of functions on the integers dealing with coded syntactic properties. Inspired by a construction of P. de Bruin (see Barendregt [1991]) a different coding ⌜M⌝ and an efficient self-interpreter E∈Λ^{∘} was constructed by Mogensen [1992] such that even

∀M∈Λ E⌜M⌝ = M.  (3)

This construction does not represent syntax via an encoding as numbers, but directly as lambda terms. This results in a much less complex E. Mogensen’s construction was simplified even further in Böhm et al. [1994]. In this paper we construct a simple discriminator Δ∈Λ^{∘} such that

∀M, N∈Λ^{∘} Δ⌜M⌝⌜N⌝ = \{ \begin{matrix}true & if M ≡_{α} N; \\ false & else. \end{matrix}  (4)

Note that in (1) and (4) the statement is only about closed lambda terms, while that in (2) and (3) is about all lambda terms. Moreover in (2) syntactic equality on terms is considered literary, while in (4) we can deal in an easy way with the better notion of equality modulo a change of names for bound variables. It will become clear why this is so.

This paper first appeared in From Universal Morphisms to Megabytes— a Baayen Space Odyssey, printed at CWI, Amsterdam.

1. Introduction

The most important notations for the type-free lambda calculus will be given here. Background can be found in Barendregt [1984].

1.1. Definition. Variables and terms of the lambda calculus are defined by the following abstract syntax.

               var = a | var′
               term = var | term term | λ var term

Notation. (i) M, N, …, P, Q, … range over λ-terms. The letters x, y, z, … range over variables. Note that the variables are {a, a′, a′′, …, a^{(n)}, …}.

(ii) Λ is the set of lambda terms. FV(M) is the set of free variables of M.The set of closed terms is Λ^{∘} = {M∈Λ | FV(M) = ∅}.

(iii) The relation ≡ denotes syntactic equality; the relation ≡_{α} denotes syntactic equality up to a change of names of the bound variables. For example

λx.x ≡_{α} λy.y ≢ λx.x.

(iv) The relation = denotes β-convertibility, axiomatized by

(λx.M)N = M[x := N].

Here [x := n] denotes substitution of N in the free occurrences of x. E.g.

(x(λx.x))[x := a] ≡ a(λx.x).

(v) IN is the set of natural numbers. For n∈IN the terms c_{n} ≡ λfx.f^{n}x, where f^{0}x ≡ x and f^{n+1}x ≡ f(f^{n}x), denote the so called Church numerals. Note that the c_{n} are distinct normal forms; hence

c_{n} = c_{m} ⇒ n = m

by the Church-Rosser theorem.

A lambda term can be seen as an executable: the redexes want to be evaluated. In this sense a normal form is not executable anymore. For a lambda term M its code ⌜M⌝ is a normal form such that M is reconstructible from M. Kleene [1936] defined a code ⌜M⌝^{K} essentially as follows.

1.2. Definition. (i) By induction on the structure of M we define #M.

#(a^{(n)}) = < 0, n >;
#(P Q) = < 1, < #(P), #(Q) >>;
#(λx.P) = < 2, < #(x), #(P) >> .

Here < −, − > denotes a recursive pairing function on IN with the recursive projections (−)_{0}, (−)_{1}:

(< n_{0}, n_{1} >)_{i} = n_{i}.

(ii) The map ⌜−⌝^{K} : Λ→Λ is defined by

⌜M⌝^{K} = c_{#M}.

Note that for all M∈Λ the term ⌜M⌝^{K} is in normal form. Moreover,

⌜M⌝^{K} = ⌜N⌝^{K} ⇒ M ≡ N.

1.3. Proposition. There is no lambda term Q such that for all M∈Λ^{(o)} one has

QM = ⌜M⌝^{K}.

Proof. Suppose Q exists. Then for I ≡ λx.x one has

Q(II) = ⌜II⌝^{K} = c_{#(II)} = c_{<1,<#I,#I>>}.

But also

Q(II) = QI = ⌜I⌝^{K} = c_{#I} = c_{<2,<#(x),#(x)>>}.

Hence < 1, < #(I), #(I) >>=< 2, < #(x), #(x) >>, a contradiction.

In spite of this fact that the ‘quote’ Q does not exists, the inverse ‘evaluation’ E can be constructed.

1.4. Theorem (Kleene [1936]). There exists an E^{K}∈Λ^{∘} such that for all M∈Λ^{∘} one has

E^{K}⌜M⌝^{K} = M.

Proof. See Kleene [1936] or Barendregt [1984], theorem 8.1.16.

The self-interpreter E can work only for closed terms M (or terms having at most a fixed finite set of free variables). The reason is that if

E^{K}⌜M⌝^{K} = M,

then

FV(M) ⊆ FV(E^{K}⌜M⌝^{K}) = FV(E^{K}).

Therefore if E^{K} is closed, then the M have to be closed as well. This causes one difficulty in the construction of E^{K}. The closed terms do not form a contextfree language. Kleene solved this problem by constructing E first for the set of combinatory terms C^{∘} built from the basis {K, S} using application only; then the real self-interpreter can be obtained by translations between Λ^{∘} and C^{∘}.

A different construction of a self-interpreter was given by a former student of mine, using ideas from denotational semantics. The equations for the selfinterpreter are those of the semantic interpretation and the F plays the role of a valuation (environment).

1.5. Theorem (P. de Bruin). There exists an E_{0}∈Λ^{∘} such that for all M∈Λ and all F ∈Λ one has

E_{0}⌜M⌝F = M[x_{1}, …, x_{n} := F ⌜x_{1}⌝, …, F ⌜x_{n}⌝]  (5)

(simultaneous substitution), where {x_{1}, …, x_{n}} = FV(M).

Proof. By the representability of computable functions and the fixedpoint theorem there is a term E_{0}∈Λ^{∘} such that

E_{0}⌜x⌝^{K}F = F ⌜x⌝^{K};
E_{0}⌜P Q⌝^{K}F = (E_{0}⌜P ⌝^{K}F)(E_{0}⌜Q⌝^{K}F);
E_{0}⌜λx.P ⌝^{K}F = λx.(E_{0}⌜P ⌝^{K}F_{[⌜x⌝↦x]}),

where F_{[⌜x⌝↦x]} = F′_{x} with

F′_{x}⌜x⌝ = x;
F′_{x}⌜y⌝ = F ⌜y⌝, if y ≢ x.

Note that F′_{x} can be written as GF x, with G closed. By induction on the structure of M∈Λ one can show that the statement holds.

1.6. Corollary. There exists an E^{dB}∈Λ^{∘} such that for all M∈Λ^{∘} one has

E⌜M⌝^{K} = M.

Proof (P. de Bruin). We can take

E^{dB} ≡ λm.E_{0}mI.

Indeed, for closed terms M it follows from (5) that

E^{dB}⌜M⌝ = E_{0}⌜M⌝I = M.

2. Representing data types

After seeing the method of P. de Bruin, an improved version of it was given by Mogensen [1992] by representing data types directly (i.e. not using the natural numbers) in lambda calculus as done in e.g. Böhm and Berarducci [1985]. This approach was improved later by Böhm et al. [1994] by constructing a new representation of data types into type-free lambda calculus. This new representation will be treated in a slightly modified form in this section.

2.1. Definition. Write

⟨M_{1}, …, M_{n}⟩ = λz.zM_{1} … M_{n};
U_{i}^{n} = λx_{1} … x_{n}.x_{i};
true = U_{1}^{2};

                        false = U_{2}^{2}.

Note that

⟨M_{1}, …, M_{n}⟩U_{i}^{n} = M_{i};
true P Q = P;

                           false P Q = Q.

In particular we have ⟨M⟩ = λz.zM and ⟨ ⟩ = λx.x = I. Now we define the notion of lists inspired by the language LISP, McCarthy et al. [1961].

2.2. Definition. (i) Write

nil = ⟨ ⟩;
cons = λxy.⟨x, y⟩;
car = ⟨U_{1}^{2}⟩;
cdr = ⟨U_{2}^{2}⟩;
null_{?} = ⟨U_{3}^{3}, U_{1}^{2}, false , true ⟩.

(ii) Define

[ ] = ⟨ ⟩;
[M_{1}, …, M_{n+1}] = cons M_{1}[M_{2}, …, M_{n+1}].

So for example

[M_{1}, M_{2}, M_{3}] = ⟨M_{1}, ⟨M_{2}, ⟨M_{3}, ⟨ ⟩⟩⟩⟩.

(In Barendregt [1984] this term is written as [M_{1}, M_{2}, M_{3}, I]. At the time of writing that book we did not yet see the usefulness of terminating a list with a special constructor.) Note that

                     car ( cons P Q) = P;
                     cdr ( cons P Q) = Q;
                         null_{?} nil = true ;
                     null_{?}( consPQ) = false .

2.3. Proposition. There exists lambda definable functions ( )_{i} such that for 1 ≤ i ≤ n one has

([M_{1}, …, M_{n}])_{i} = M_{i}.

Proof. Take

(l)_{1} = car l;
(l)_{i+1} = ( cdr l)_{i}.

2.4. Definition. An (algebraic) signature s consists of a number n∈IN (thought of as the list of symbols [f_{1}, …, f_{n}]) together with a list of numbers [s_{1}, …, s_{n}] (thought of as the arity of the respective f_{i}’s). We write s = [s_{1}, …, s_{n}].

For example a field has signature s = [2, 2, 1, 1, 0, 0] (thought of as the arities of the functionsymbols [+, ×, −,^{−1}, 0, 1]; so f_{1} = +, f_{2} = × etcetera).

2.5. Definition. If s is a signature then term_{s}, the set of terms of signature s, is defined as follows.

                      x∈var ⇒ x∈term_{s};

t_{1}, …, t_{s_{i}}∈ term_{s} ⇒ f_{i}(t_{1}, …, t_{s_{i}})∈ term_{s}.

For example in the signature of fields the term f_{1}(f_{1}(x, f_{3}(f_{2}(y, f_{4}(z))), f_{6}) is usually written as x − yz^{−1} + 1.

2.6. Definition. Let s = [s_{1}, …, s_{n}] be a signature.

(i) A lambda interpretation of s is a list of ‘constructors’ C_{1}, …, C_{n}∈Λ. (ii) Let C_{1}, …, C_{n} be a lambda interpretation of s. Then we define a map

T : term_{s}→Λ

as follows.

T_{x} = x;
T_{f_{i}(t_{1},...,t_{s_{i}})} = C_{i}[T_{t_{1}}, …, T_{t_{s_{i}}}],

where [T_{t_{1}}, …, T_{t_{s_{i}}}] is the list operation on lambda terms defined in 2.2.

Example. The signature of binary trees is [0, 2]. The term t = f_{2}(f_{2}(f_{1}, f_{1}), f_{1}) denotes a simple tree and t′ = f_{2}(f_{1}, f_{2}(f_{1}, f_{1})) its miror image. Can we find a lambda interpretation for this signature in such a way that mirroring becomes lambda definable, i.e. for some F ∈Λ^{∘} one has F T_{t} = T_{t′}? The following result, due to Böhm et al. [1994], will affirm this. We present the result in a modified form that will be useful for §4.

2.7. Theorem. For every algebraic signature s = [s_{1}, …, s_{n}] there exists a lambda interpretation C_{1}, …, C_{n} such that the following hold.

(i) ∀A_{1} … A_{n} ∃F

F T_{f_{i}(t_{1},...,t_{s_{i}})} = A_{i}[T_{t_{1}}, …, T_{t_{s_{i}}}]F,  1 ≤ i ≤ n.  (6)

(ii) The C_{1}, …, C_{n} only depend on n, not on the [s_{1}, …, s_{n}]. In (6) we can take F ≡ ⟨⟨A_{1}, …, A_{n}⟩⟩.

Proof. Define C_{f_{i}} ≡ λle.eU_{i}^{n}l⟨e⟩.

(i) Given A_{1}, …, A_{n}, we try whether F ≡ ⟨⟨A_{1}, …, A_{n}⟩⟩ works. Indeed,

F T_{f_{i}(t_{1},...,t_{s_{i}})} = ⟨⟨A_{1}, …, A_{n}⟩⟩(C_{f_{i}}[T_{t_{1}}, …, T_{t_{s_{i}}}])
= C_{f_{i}}[T_{t_{1}}, …, T_{t_{s_{i}}}]⟨A_{1}, …, A_{n}⟩
= ⟨A_{1}, …, A_{n}⟩U_{i}^{n}[T_{t_{1}}, …, T_{t_{s_{i}}}]⟨⟨A_{1}, …, A_{n}⟩⟩
= A_{i}[T_{t_{1}}, …, T_{t_{s_{i}}}]F.

(ii) By the construction.

2.8. Corollary. Let s = [s_{1}, …, s_{n}] be an algebraic signature. Let C_{1}, …, C_{n} be the lambda interpretation of s constructed in theorem 2.7. Then for all B_{1} … B_{n} there exists an F such that

F (C_{f_{i}}[x_{1}, …, x_{s_{i}}]) = B_{i}x_{1} … x_{s_{i}}F,  1 ≤ i ≤ n.  (7)

Proof. Let B_{1}, …, B_{n} be given. Define A_{i} = λl.B_{i}(l)_{1} … (l)_{s_{i}}. Then

A_{i}[x_{1}, …, x_{s_{i}}] = B_{i}x_{1}, …, x_{s_{i}}.

Then the F for the A_{i} found in theorem 2.7 is the F satisfying (7).

Now we can program the function that ‘mirrors’ trees. In the signature [0,2] for binary trees let

leaf = T_{f_{1}}  = C_{f_{1}}⟨ ⟩;
tree = λab.T_{f_{2}(a,b)} = λab.C_{f_{2}}⟨a, b⟩.

By corollary 2.8 there exists an F such that

                        F leaf = leaf;

F (tree a b) = tree(fb)(fa).

This F has the mirror effect. E.g. F (f_{2}(f_{2}(f_{1}, f_{1}), f_{1})) = f_{2}(f_{1}, f_{2}(f_{1}, f_{1})).

3. A simple self-interpreter

In Mogensen [1992] a simple coding and self-interpreter for lambda terms is defined, using the fact that data types (term algebras of a signature s) have a lambda interpretation. The method was simplified by Böhm et al. [1994] by making use of their lambda representation of algebraic signatures given in §2.

3.1. Definition. Let s be the signature [1, 2, 1]. Define

const = C_{f_{1}} ≡ λle.eU_{1}^{3}l⟨e⟩;
app = C_{f_{2}} ≡ λle.eU_{2}^{3}l⟨e⟩;
abs = C_{f_{3}} ≡ λle.eU_{3}^{3}l⟨e⟩.

3.2. Definition. For M∈Λ define ⌜M⌝ as follows.

⌜x⌝ = const [x];
⌜P Q⌝ = app [⌜P ⌝, ⌜Q⌝];
⌜λx.P ⌝ = abs [λx.⌜P ⌝].

Note that FV(⌜M⌝) = FV(M).

3.3. Theorem (Mogensen [1992]). There exists an E∈Λ^{∘} such that

∀M∈Λ E⌜M⌝ = M.

Proof (B”ohm et al. [1994]). By corollary 2.8 there exists a term E∈Λ^{∘} such that

E( const [p]) = p;
E( app [p, q]) = (Ep)(Eq);
E( abs [p]) = λx.E(px).

Then

E⌜x⌝ = x;
E⌜P Q⌝ = (E⌜P ⌝)(E⌜Q⌝);
E⌜λx.P ⌝ = λx.E⌜P ⌝.

Now the results follows by induction on the structure of M.

Using the constructions in §2 the self-interpreter becomes

E ≡ ⟨⟨λlf.(l)_{1}, λlf.f(l)_{1}(f(l)_{2}), λlfx.f((l)_{1}x)⟩⟩.

The construction in Böhm et al. [1994] is simpler. They take

const = λxe.eU_{1}^{3}xe;
app = λxye.eU_{2}^{3}xye;
abs = λxe.eU_{3}^{3}xe.

The resulting self-interpreter then becomes E^{B} = ⟨⟨K, S, C⟩⟩. Here K ≡ λxy.x, S ≡ λxyz.xz(yz) and C ≡ λxyz.x(zy). For reasons of uniformity we have given the definition of const , app and abs as in 3.1. This will be useful in §4.

4. A simple discriminator

In this section we will construct a simple term discriminating between coded closed lambda term. The discrimination is even modulo α-conversion. For open terms discrimination is possible only for the coding ⌜ ⌝^{K} of Kleene.

4.1. Lemma. (i) There exists a term δ_{IN}∈Λ^{∘} such that

δ_{IN}c_{n}c_{m} = \{ \begin{matrix}true & if n = m; \\ false & else. \end{matrix}

(ii) There exists a term and ∈Λ^{∘} such that

                      and true true = true ;
                     and true false = false ;
                     and false true = false ;
                    and false false = false .

Proof. (i) By the representability of the recursive functions.

(ii) Take and = λab.a true b.

4.2. Proposition. There exists a term δ∈Λ^{∘} such that (writing δ_{n} for δc_{n}) one has

δ_{n}⌜x⌝⌜x′⌝  = δ_{IN}xy;
δ_{n}⌜x⌝⌜P′Q′⌝  = false ;
δ_{n}⌜x⌝⌜λx′.P′⌝  = false ;
δ_{n}⌜P Q⌝⌜x′⌝  = false ;
δ_{n}⌜P Q⌝⌜P′Q′⌝  = and (δ_{n}⌜P ⌝⌜P′⌝)(δ_{n}⌜Q⌝⌜Q′⌝)
δ_{n}⌜P Q⌝⌜λx′.P′⌝ = false ;
δ_{n}⌜λx.P ⌝⌜x′⌝  = false ;
δ_{n}⌜λx.P ⌝⌜P′Q′⌝ = false ;
δ_{n}⌜λx.P ⌝⌜λx′.P′⌝ = δ_{n+1}(⌜P ⌝[x := c_{n}])(⌜P′⌝[x′ := c_{n}]).

Proof. We introduce the following ad hoc notation.

(i) Let A_{1}, …, A_{n}∈Λ. Then we write

λx⃗![A_{1}, …, A_{n}] ≡ ⟨⟨λx⃗.A_{1}, …, λx⃗.A_{n}⟩⟩.

(ii) If B_{i} ≡ [A_{i1}, …, A_{in}], then we write

λx⃗!![B_{1}, …, B_{n}] ≡ ⟨⟨λx⃗!B_{1}, …, λx⃗!B_{n}⟩⟩.

(iii) Let for 1 ≤ i ≤ n, 1 ≤ j ≤ n be given A_{ij}∈Λ. Then

[A_{ij}] ≡ [[A_{11}, …, A_{1n}],
[A_{21}, …, A_{2n}],
…
[A_{n1}, …, A_{nn}]].

If n = 3 we may write [A_{ij}] as

[ \begin{matrix}A_{11} & A_{12} & A_{13} \\ A_{21} & A_{22} & A_{23} \\ A_{31} & A_{32} & A_{33} \end{matrix} ] .

Now define δ ≡ λntt′.

(λtd!λt′d′n!![ \begin{matrix}δ_{IN}(t)_{1}(t′)_{1} & false & false \\ false & and (d(t)_{1}(t′)_{1}n)(d(t)_{2}(t′)_{2}n) & false \\ false & false & d(tn)(t′n)(S^{+}n) \end{matrix} ]) tt′n,

where S^{+} lambda defines the successor function. Then by theorem 2.7 this δ satisfies the specification.

4.3. Proposition. For all M, M′∈Λ such that FV(MM′) ⊆ {x_{1}, …, x_{n}} and for substitutions ∗ = [x_{1} := c_{k_{1}}] … [x_{n} := c_{k_{n}}] with k_{i} ≠ k_{j} (for 1 ≤ i < j ≤ n) one has for p > k_{i} (for all 1 ≤ i ≤ n) that

δ_{p}⌜M⌝⌜M′⌝∗ = \{ \begin{matrix}true & if M ≡_{α} M′; \\ false & else. \end{matrix}

Proof. By induction on the structure of M, in each case making distinctions according to the structure of M′. We treat four instructive cases.

Case M ≡ x, M′ ≡ x′. Then

δ_{p}⌜M⌝⌜M′⌝∗ = δ_{IN}c_{k_{i}}c_{k_{i′}} ,

where x ≡ x_{i}, x′ ≡ x_{i′}. This is true or false depending on whether x ≡ x′ (so i = i′) or x ≢ x′ (so i ≠ i′).

Case M ≡ x, M′ ≡ P′Q′. Then

δ_{p}⌜M⌝⌜M′⌝∗ = false .

Case M ≡ P Q, M′ ≡ P′Q′. Then

δ_{p}⌜M⌝⌜M′⌝∗ =  and (δ_{p}⌜P ⌝⌜P′⌝∗)(δ_{p}⌜Q⌝⌜Q′⌝∗)

                      =_{IH} and ( true / false )( true / false )
                      =  true / false ,

as it should (= true only if P Q ≡ P′Q′ i.e. if both P ≡ P′ and Q ≡ Q′). Case M ≡ λx.P, M′ ≡ λx′.P′. Then

δ_{p}⌜M⌝⌜M′⌝∗ = δ_{p+1}(⌜P ⌝[x := c_{p}])(⌜P′⌝[x′ := c_{p}]) ∗
= δ_{p+1}⌜P ⌝⌜P′[x′ := x]⌝[x := c_{p}] ∗
= δ_{p+1}⌜P ⌝⌜P′[x′ := x]⌝∗′,

with ∗′ = ∗[x := c_{p}] being an admissible substitution. So

δ_{p}⌜M⌝⌜M′⌝∗ =_{IH} \{ \begin{matrix}true & if P ≡_{α} P′[x′ := x]; \\ false & else. \end{matrix}

Now M ≡_{α} M′ iff λx.P ≡_{α} λx′.P′ (≡_{α} λx.P′[x′ := x]) iff P ≡_{α} P′[x′ := x]. Hence we are done.

4.4. Corollary. Write Δ ≡ δ_{0}. Then Δ∈Λ^{∘} and for all M, M′∈Λ^{∘} one has

Δ⌜M⌝⌜M′⌝ = \{ \begin{matrix}true & if M ≡_{α} M′; \\ false & else. \end{matrix}

Proof. Immediate from the proposition.

Note that this corollary cannot hold for arbitrary M, M′∈Λ. For example, it is impossible to discriminate ⌜x⌝ and ⌜x′⌝. Indeed take x ≢ x′ and make a substitution [x′ := x]:

Δ⌜x⌝⌜x′⌝ = false ⇒ Δ⌜x⌝⌜x⌝ = false ,

a contradiction.

References

Barendregt, H.P.

[1984] The Lambda Calculus, its Syntax and Semantics, revised edition, Studies in Logic and the Foundations of Mathematics, North-Holland, Amsterdam.

[1991] Theoretical pearls: Self-interpretation in lambda calculus, J. Funct. Pro-

gramming, 1(2), 229–233.

Böhm, C., and A. Berarducci

[1985] Automatic synthesis of typed λ-programs on term algebras, Theor. Comput.

Sci. 39, 135-154.

Böhm, C., A. Piperno and S. Guerrini

[1994] λ-definitions of function(al)s by normal forms, in: ESOP ’94 , (ed. D. San-

nella), LNCS 788, Springer, Berlin, 135–149

Church, A.

[1941] The calculi of lambda conversion, Princeton University Press, Princeton.

Reprinted by Kraus reprint corporation, New York, 1965.

Kleene, S.C.

[1936] λ-definability and recursiveness, Duke Math. J. 2, 340-353. McCarthy, J., P.W. Adams, D.J. Edwards, T.P. Hart and M.I. Levin

[1962] LISP 1.5 Programmer’s manual, MIT Press. Mogensen, T.Æ.

[1992] Efficient self-interpretation in lambda calculus, J. Funct. Programming, 2(3), 345–364.