                        CATS 2000 Preliminary Version

Böhm’s Theorem for Berarducci Trees^{1}

Mariangiola Dezani-Ciancaglini^{a} Paula Severi^{b}

Fer-Jan de Vries^{c}

a Dipartimento di Informatica, Università degli Studi di Torino Corso Svizzera 185, 10149 Torino, Italia, Email: dezani@di.unito.it b Centro de Matemática, Facultad de Ciencias, Universidad de la República Oriental del Uruguay, Iguá 4225 CP 11400, Montevideo, Uruguay, E-mail: severi@cmat.edu.uy c Computer Science Division, Electrotechnical Laboratory, 1-1-4 Umezono, Tsukuba, Ibaraki 305 Japan, E-mail: ferjan@etl.go.jp

Abstract We propose an extension of lambda calculus which internally discriminates two lambda terms if and only if they have different Berarducci trees.

1 Introduction

The Lambda Calculus is a theory of functions that serves as a foundation for the functional programming paradigm. Lambda terms in this view are idealized programs. There are essentially two ways of characterizing the meaning of lambda terms. The first one is to run the program and to study the output. The second one is to observe the effect of the program when used as a subprogram in other programs.

With respect to the first approach, traditionally the output of a lambda term was described by its Böhm tree. But also Lévy-Longo trees and more recently Berarducci trees have been used. In this paper we will focus on Berarducci trees. These trees provide the possible output of a lambda term in greatest detail.

The idea behind all these different concepts of tree is stable information, that we can recover by reducing the terms. This is the token of information

1 This paper was made possible thanks to the hospitality ETL offered in the March 1999 to both Mariangiola Dezani and Paula Severi.

This is a preliminary version. The final version will be published in Electronic Notes in Theoretical Computer Science

                       URL: www.elsevier.nl/locate/entcs

M. Dezani-Ciancaglini, P. Severi and F.J. de Vries

which cannot be altered by further reductions but can only be added upon. (As an example the reader may think of the calculation of the \sqrt{2}. The calculation process merely adds decimals to the already calculated decimal expansion). If one organizes all the stable information that can be obtained from a computation and orders it according to the order it is produced, then it is quite natural to obtain a tree representation of the information implicitly contained in the original term. There exist many tree representations in literature, depending on the possible notions of stable relevant information [16], [17], [3]. If only head normal forms are stable, i.e., terms of the shape λx_{1} … x_{n}.yM_{1} … M_{m}, then we obtain the notion of Böhm trees [4]. If we consider stable weak head normal forms (i.e. also all abstractions) we get the notion of Lévy-Longo trees [23]. Lastly when all top normal forms (i.e. also applications MN where M never reduces to an abstraction) are viewed as stable we obtain the notion of Berarducci trees [7].

The second approach to the meaning of lambda terms puts lambda terms inside contexts and observes when they reduce to values. This leads to a notion of observational equivalence that is parametric with respect to the set of values considered. Natural choices are the sets of normal forms, head normal forms, weak head normal forms, and top normal forms.

In this paper we will consider the case that the set of values is the set of the top normal forms, that is we will consider Berarducci trees.

1.1 Berarducci Trees

Berarducci trees arise in a natural way when we look at the parsing trees of lambda terms (see for example [25]). In this representation the abstraction with respect to a given variable is an unary operator and the application (explicitly denoted by @) is a binary operator. For example the term (λx.x)(λy.y)

is represented by [figure: @; λx; λy; x; y] . As a matter of fact, (λx.x)(λy.y) reduces to

λy.y, so we can conclude that if we are looking at lambda terms modulo β-

equality a better tree representation of (λx.x)(λy.y) is \begin{matrix}λy \\ y \end{matrix} .

This suggest to draw only the nodes of the parsing tree which will never be changed by β-reduction. It is clear that when the root of a parsing tree is an abstraction or a variable (in this last case, the root is also a leaf) it is stable, i.e. it will never change by β-reducing the corresponding term. The case in which the root is an application node requires more care. But it is immediate to understand that in this case the root is stable if and only if the root of the left subtree will never become an abstraction, or equivalently if and only if the subterm in functional position will never reduce to an abstraction (i.e. to a term of the shape λx.M). The above discussion justifies the following definitions of zero terms, rootstable terms, rootactive terms and Berarducci trees.

Definition 1.1 For terms in the pure lambda calculus we define:

(i) a zero term is a term which cannot reduce to an abstraction, (ii) a rootstable term [16] is a term which cannot reduce to a redex, (iii) a rootactive term [16] is a term of which any reduct can reduce to a redex. (iv) R denotes the set of rootactive terms in the pure lambda calculus Λ.

Note that a term is rootactive if and only if it cannot reduce to a rootstable term. The term III is an example of a term which is neither rootactive nor rootstable but it is a term which can reduce to a rootstable term.

Rootstable terms have concrete forms which can not change anymore after further reduction: they reduce either to a variable, to an abstraction or to a term of the shape MN where M is a zero term. These forms are called top normal forms in [7]. In the terminology of [1] we let rootstable terms take the role of values and rootactive terms the role of divergent terms.

Definition 1.2 [7] The Berarducci tree T (M) of a lambda term M is defined by coinduction as a possible infinite term in the infinitary extension Λ_{⊥}^{∞} of the pure lambda calculus with a fresh constant ⊥:

(i) if M →_{β}^{∗} x, then T (M) = x

(ii) if M →_{β}^{∗} λx.N, then T (M) = \begin{matrix}λx \\ T (N) \end{matrix}

(iii) if M →_{β}^{∗} M_{1}M_{2}, where M_{1} is a zero term, then T (M) =

[figure: @; T (M_{1}); T (M_{2})]

(iv) otherwise, (exactly when M is rootactive) T (M) = ⊥.

This gives an equivalence relation: two lambda terms are equivalent if and only if they have the same Berarducci tree (modulo α-conversion, as defined in [16]).

1.2 Observational equivalence

A completely different way of comparing lambda terms is observational equivalence [21], in which we say that M is equivalent to N iff:

∀C[ ] ∈ Λ C[M] ∈ R ⟺ C[N] ∈ R.

Here we put M and N in various contexts and observe whether the behavior of M and N in those contexts is the same, that is whether C[M] and C[N] can both produce stable information, that is if they both reduce to rootstable terms. Berarducci tree equality implies observational equivalence [24]:

Theorem 1.3 For all M, N ∈ Λ, T (M) = T (N) implies ∀C[ ] ∈ Λ C[M] ∈ R ⟺ C[N] ∈ R.

This can be easily seen with help of the fact that

T (C[M]) = T (C[T (M)])

which directly follows from the unique normal form property of the infinitary lambda calculus extended with a rule like:

M → ⊥ if M is rootactive.

The Berarducci tree of a term is nothing else but its unique normal form in this calculus. The proof of the implication then becomes simply:

\begin{aligned}C[M] ∈ R & ⟺ T (C[M]) = ⊥ ⟺ T (C[T (M)]) = ⊥ ⟺ \\ & ⟺ T (C[T (N)]) = ⊥ ⟺ T (C[N]) = ⊥ ⟺ C[N] ∈ R. \end{aligned}

However the converse is not true: observational equivalence does not imply Berarducci tree equivalence. For example one can check that there is no context C[ ] such that C[ΩΩ] is rootactive and C[ΩΩΩ] is not, or vice versa, where Ω ≡ (λx.xx)(λx.xx). The terms ΩΩ and ΩΩΩ have different Berarducci

trees, since they are [figure: @; ⊥; ⊥] and [figure: @; @; ⊥; ⊥; ⊥].

1.3 Summary

In this paper we will define an extension Λ_{OA} of the pure lambda calculus Λ and a reduction relation →_{βOA} for which we can prove:

Theorem 1.4 For all M, N ∈ Λ it holds that

T (M) = T (N)

if and only if

C[M] ∈ R_{OA} ⟺ C[N] ∈ R_{OA} for all C[ ] ∈ Λ_{OA},

where R_{OA} is the set of rootactive terms in Λ_{OA} (with respect to →_{βOA}).

The “if” part will be proved by a variation on the Böhm out technique. For the “only if” part we adapt techniques from infinitary lambda calculus.

1.4 Background

Historically, quoting from [4](page 215), “the notion of Böhm tree is suggested by the original proof of Böhm’s theorem”. Böhm’s theorem states that given two distinct β-η-normal forms there is a context C[ ] such that C[M] = x and C[N] = y, where x, y are arbitrary distinct variables. The method used to find such a context is called the Böhm out technique [4](Section 10.3).

In [25] Wadsworth, generalizing Böhm’s theorem, shows that two lambda terms M, N have the same Böhm tree modulo infinite η-expansions iff for all contexts C[ ] the following holds:

C[M] has a head normal form ⟺ C[N] has a head normal form.

The proof technique used to obtain this result is the Böhm out technique. The same property holds even considering Böhm trees modulo finite ηexpansions and normal forms, as shown in [13]. More precisely Hyland proves, using the Böhm out technique, that two lambda terms M, N have the same Böhm tree modulo finite η-expansions iff for all contexts C[ ] the following holds:

C[M] has a normal form ⟺ C[N] has a normal form.

The results of [25] and [13] can be rephrased as follows: the lambda calculus internally discriminates as Böhm tree modulo infinite (respectively finite) η-expansions when the set of values is the set of head normal forms (respectively normal forms).

To internally discriminate terms having different Böhm trees Dezani-Intrigila-Zilli [11] add to the pure lambda calculus a non-deterministic choice operator + and an adequate numeral system (as defined in Section 6.4 of [4]). The reduction rules for + are:

M + N ⟶ M and M + N ⟶ N.

Clearly the non-deterministic choice operator allows to gain definability of combinators like Plotkin’s parallel-or [22] when one considers may convergence, under which a term converges if at least one of the possible computations (properly reductions) starting from it ends. This extension increases the power of the lambda calculus to detect convergence internally also in those cases in which a term converges as soon as at least one of its subterms does, no matter in which order they are evaluated. This amounts to have the definability of all compact points in a standard model, that is, by Milner’s theorem [20], to have a fully abstract interpretation for the language. The numerals play an essential role to discriminate between a term possessing head normal form and its η-expansion, essentially since they can never be applied to an argument, while all pure lambda terms can be seen both as functions and as arguments. This result is proved using a variation of the the Böhm out technique as well as characteristic terms and test terms [8].

Instead, Lévy-Longo trees correspond to observational equivalence with respect to weak head normal forms in suitably enriched versions of the lambda calculus, as shown in [23], [9], [12]. Now, we shortly recall such approaches.

In [23], Sangiorgi considers the embedding of lazy lambda calculus in some concurrent calculi. First, Milner’s encoding of lazy lambda calculus in πcalculus is studied. Then the lazy lambda calculus is enriched with a simple non-deterministic operator, which, when applied to an argument, either gives the argument itself or diverges. In both cases the processes are compared using bisimulation. The proof technique is the Böhm out technique.

On the other side, Boudol and Laneve [9] introduce a “resource conscious” refinement of lambda calculus, in which every argument comes with a multiplicity. The reduction process (which uses explicit substitutions in an essential way) remains deterministic, but a deadlock can appear. The terms are compared by means of the standard observational equivalence. The proof technique is again the Böhm out technique.

Dezani-Tiuryn-Urzyczyn [12] consider the behavior of pure lambda terms inside contexts of the concurrent lambda calculus as defined in [10]. This calculus is obtained from the pure lambda calculus (with call-by-value and callby-name variables) by adding the non-deterministic choice operator discussed above and a parallel operator ∥, whose main reduction rule is

M ⟶ M′ N ⟶ N′
(∥)
M∥N ⟶ M′∥N′

where ⟶ stands for one-step reduction.

The terms are compared by means of the standard observational equivalence. The proof technique is that of characteristic terms and test terms.

2 Extending λ-calculus

Besides the pure lambda calculus Λ and its extension Λ_{OA} we define the infinitary extensions Λ_{⊥}^{∞} and Λ_{OA⊥}^{∞} in which we can reason about the Berarducci trees of terms of Λ and Λ_{OA}. First we introduce the syntax of these sets and then the reduction rules.

2.1 Syntax

Let a countable set of variables V be given.

Definition 2.1 (i) The set Λ of pure lambda terms is defined by the inductive grammar:

M :=_{ind} x | λx.M | MM, where x ∈ V.

(ii) The set Λ_{⊥} of partial terms is defined by the inductive grammar:

M :=_{ind} x | ⊥ | λx.M | MM, where x ∈ V.

(iii) The infinitary extension Λ_{⊥}^{∞} of Λ_{⊥} is defined by the coinductive grammar:

M :=_{coind} x | ⊥ | λx.M | MM, where x ∈ V.

(iv) The extension Λ_{OA} of Λ with the constants O, A is defined by the inductive grammar:

X :=_{ind} M | OX | AX | λx.X | XM, where M ∈ Λ.

(v) The extension Λ_{OA⊥} of Λ_{OA} with partial terms is defined by the inductive grammar:

X :=_{ind} M | OX | AX | λx.X | XM, where M ∈ Λ_{⊥}.

(vi) The infinitary extension Λ_{OA⊥}^{∞} of Λ_{OA} is defined by the inductive grammar:

X :=_{ind} M | OX | AX | λx.X | XM, where M ∈ Λ_{⊥}^{∞}.

We will use abbreviations for some lambda terms:

I =^{Def} λx.x  K =^{Def} λxy.x Δ =^{Def} λx.xx
Δ_{M} =^{Def} λx.xxM Ω =^{Def} ΔΔ  Ω_{M} =^{Def} Δ_{M}Δ_{M}

These sets of terms play the following roles in this paper. The set Λ_{⊥}^{∞} of the finite and the infinite terms contains the Berarducci trees of terms in Λ (when we do not distinguish between terms and their parsing trees). The set Λ_{OA} is the set Λ extended with two constants O and A that allow us to discriminate Berarducci trees of pure lambda terms. The set Λ_{OA⊥}^{∞} of finite and infinite terms includes the set of Berarducci trees of terms in Λ_{OA}.

Note that the syntax of Λ_{⊥}^{∞} is given coinductively. This implies that Λ_{⊥}^{∞} includes besides finite terms only well-formed infinite terms with the property that any node has finite distance (in the parsing trees of terms) to the root. One can think of those terms as build in top down manner in contrast to the inductive bottom up manner (cf. [6]). Alternatively, we can define the set Λ_{⊥}^{∞} as the metric completion (cf. [5,16,14]) or the order completion (for example cf. [2]) of the finite set Λ_{⊥}. From either construction it follows that if all finite prefixes of two terms are the same, then the two terms themselves are equal to each other. The effect of the inductive constructions of Λ_{OA} from Λ and of Λ_{OA⊥}^{∞} from Λ_{⊥}^{∞} is that any term of Λ_{OA} and Λ_{OA⊥}^{∞} contains at most finitely many symbols O and A.

Finally note the restriction on the arguments in applications in Λ_{OA} and Λ_{OA⊥}^{∞}. These arguments have to be elements of Λ and Λ_{⊥}^{∞} respectively. This implies that all O or A symbols can occur only on the left-spines (the left-most paths in the parsing trees) of terms.

2.2 Rewrite rules

We introduce now the reduction relations of the various calculi in a concise form.

Definition 2.2 Let Λ′ be an extension of the set Λ. A binary reduction relation R on Λ′ is called compatible if

\begin{aligned}X_{1} R X_{2} & ⇒ & λx.X_{1} R λx.X_{2} \\ X_{1} R X_{2} & ⇒ & (X_{1}Y) R (X_{2}Y) \\ Y_{1}RY_{2} & ⇒ & (XY_{1})R(XY_{2}). \end{aligned}

The above notion of compatibility restricted to Λ coincides with the one defined in [4] (Definition 3.1.1).

Definition 2.3 Let →_{1} and →_{2} be reduction relations on Λ′.

(i) The reduction relation →_{12} is defined as the union of the reduction →_{1} with →_{2}.

(ii) The reduction relation →_{1}^{=} is the reflexive closure of →_{1}. (iii) The reduction relation →_{1}^{∗} is the reflexive and transitive closure of →_{1}.

Definition 2.4 Let Λ′ ⊃ Λ.

(i) We define the binary reduction relation →_{β} as the least compatible binary relation on Λ′ containing the beta rule:

(λx.X)M →_{β} X[M/x].

(ii) A β-redex is a term in Λ′ of the form (λx.X)M.

Substitution in the infinitary lambda calculus Λ_{⊥}^{∞} needs some attention. We refer to [16,18].

We generalize the notion of zero term given in Definition 1.1 and that of strong zero term [7].^{2}

Definition 2.5 Let Λ′ ⊃ Λ and →′ a reduction relation on Λ′.

2 Equivalent alternative formulations for strong zero term are unsolvable of order 0 in [19] and strongly unsolvable in [1].

(i) A term in Λ′ is called a zero term with respect to →′ if it cannot →′-reduce to an abstraction.

(ii) A term in Λ′ is called a strong zero term with respect to →′ if all its substitution instances with terms from Λ′∩Λ_{⊥}^{∞} are zero terms with respect to →′.

For example Ω and Ω_{M} for all M in Λ are strong zero terms with respect to →_{β}.

Definition 2.6 Let Λ′ ⊃ Λ_{OA}.

(i) We define the binary reduction relation →_{OA} as the least compatible relation on Λ′ closed under the two inference rules

M is strong zero with respect to →_{β}

(O)

O(MN) →_{OA} M

M is strong zero with respect to →_{β}

(A)

A(MN) →_{OA} N

where M, N range over Λ′ ∩ Λ_{⊥}^{∞}. (ii) An OA-redex is a term in Λ′ of the form O(MN) or A(MN) where M is

a strong zero term in Λ′ ∩ Λ_{⊥}^{∞} with respect to →_{β}.

We will use these new rules to discriminate between terms with different Berarducci trees. For instance, in order to discriminate the terms Ω_{K} and Ω_{I}, we choose the context A[ ]Ω. These terms reduce as follows:

AΩ_{K}Ω →_{β} A(Ω_{K}K)Ω →_{OA} KΩ →_{β} λy.Ω

and

AΩ_{I}Ω →_{β} A(Ω_{I}I)Ω →_{OA} IΩ →_{β} Ω.

Hence the context is discriminating as Ω is rootactive and λy.Ω is not.

Example 2.7 The fact that ⊥ is strong zero with respect to →_{β} in Λ_{⊥} implies in any Λ′ ⊇ Λ_{OA⊥} that:

(i) O(⊥M_{1} … M_{n}N) →_{OA} ⊥M_{1} … M_{n} (ii) A(⊥M_{1} … M_{n}N) →_{OA} N for all M_{1}, …, M_{n}, N ∈ Λ′ (n ≥ 0).

We generalize the notion of rootstable and rootactive term given in Definition 1.1.

Definition 2.8 Let Λ′ ⊃ Λ and →′ a reduction relation on Λ′.

(i) A term in Λ′ is called rootstable with respect to →′ if it cannot →′-reduce to a →′-redex.

(ii) A term in Λ′ is called rootactive with respect to →′ if all its reducts can →′-reduce to →′-redexes.

Notice that a term is rootactive with respect to →′ if and only if it can not reduce to a rootstable term with respect to →′.

The last class of terms we consider are those which block OA-reductions.

Definition 2.9 A term in Λ′ is called a OA-blocker with respect to →′ if it does not →′-reduce to MN ∈ Λ′ ∩Λ_{⊥}^{∞} with M a strong zero term with respect to →_{β}.

We can characterize the set of rootstable terms for the extended set Λ_{OA} and the reduction →_{βOA}.

Proposition 2.10 A term X in Λ_{OA} is rootstable with respect to →_{βOA} if and only if it has one of the following shapes:

• a variable,

• an abstraction,

• an application of the form XM with X a zero term with respect to →_{βOA},

• a term of the form OX or AXwith X a OA-blocker with respect to →_{βOA}.

For example O(xx)y and A(O(λx.X)Ω) are zero terms with respect to →_{βOA} and also rootstable terms with respect to →_{βOA}.

A short notation for the set of terms in Λ_{OA} which are rootactive with respect to →_{βOA} will be handy.

Definition 2.11 R_{OA} is the set of of terms in Λ_{OA} which are rootactive with respect to →_{βOA}.

Since each term in Λ_{OA⊥}^{∞} contains only a finite number of occurrences of O, A we can prove that all rootactive terms with respect to →_{βOA} reduce to rootactive terms with respect to →_{β}.

Lemma 2.12 If X ∈ Λ_{OA⊥}^{∞} is rootactive with respect to →_{βOA} then there exists a term M ∈ Λ_{⊥}^{∞} such that X →_{βOA}^{∗} M and M is rootactive with respect to →_{β}.

Proof. By Definition 2.1(vi) the more general shape of a term X which can reduce to a OA-redex is:

(λx_{1} … x_{n}.χY M_{1} … M_{m})N_{1} … N_{p}

where χ stands for O or A , Y ∈ Λ_{OA⊥}^{∞}, M_{1}, …, M_{m}, N_{1}, …, N_{p} ∈ Λ_{⊥}^{∞} and m, n, p ≥ 0.

If n > p then X reduces to an abstraction, so it is not rootactive with respect to →_{βOA}.

If n ≤ p then X reduces to χZP_{1} … P_{m}N_{p+1} … N_{p} where Z = Y [N_{1}/x_{1}, …, N_{n}/x_{n}] and P_{i} = M_{i}[N_{1}/x_{1}, …, N_{n}/x_{n}] for 1 ≤ i ≤ m. This last term is a OA-redex if and only if Z →_{βOA}^{∗} NP for some N, P ∈ Λ_{⊥}^{∞} such that N is a strong zero term with respect to →_{β}. We can conclude that X →_{βOA}^{∗} NP_{1} … P_{m}N_{p+1} … N_{p} if χ = O and X →_{βOA}^{∗} P P_{1} … P_{m}N_{p+1} … N_{p} if χ = A.

□

The last rule we introduce allows us to equate all rootactive terms.

Definition 2.13 Let Λ′ ⊃ Λ_{⊥}. We define the reduction relation →_{⊥} as the least compatible binary relation on Λ′ closed under the inference rule:

M is rootactive with respect to →_{β}

(⊥)
M →_{β⊥} ⊥

where M, N range over Λ′.

Note that the set of rootactive terms with respect to →_{β⊥} is empty, since each rootactive term with respect to →_{β} reduces to ⊥ using rule (⊥).

Notation 2.1 Let us summarize the most used reduction relations in this paper.

• The reduction →_{β} on Λ,

• The reduction →_{βOA} on Λ_{OA},

• The reduction →_{β⊥} on Λ_{⊥}^{∞},

• The reduction →_{β⊥OA} on Λ_{OA⊥}^{∞}.

2.3 Confluence of the reductions →_{βOA} and →_{β⊥OA}

We use the Hindley-Rosen Lemma (Proposition 3.3.5 of [4]) to prove that the reduction relations →_{βOA} on Λ_{OA} and →_{β⊥OA} on Λ_{OA⊥} are confluent. We need a few auxiliary lemmas.

Lemma 2.14 (i) The relation →_{OA} commutes with the relation →_{β} in Λ_{OA}: (ii) The relation →_{OA} commutes with the relation →_{β⊥} in Λ_{OA⊥}:

\xymatrix{X \ar[r]^{β} \ar[d]_{OA} & Y_{1} \ar@{.>}[d]^{OA} & X \ar[r]^{β⊥} \ar[d]_{OA} & Y_{1} \ar@{.>}[d]^{OA} \\ Y_{2} \ar@{.>}[r]|{=}_{β} & Z & Y_{2} \ar@{.>}[r]|{=}_{β⊥} & Z}

Proof. We give the proof for →_{β⊥OA}. The proof for →_{β} is similar, just drop all references to →_{⊥}.

Suppose that C[A(MN)] →_{OA} C[N] and C[A(MN)] →_{β⊥} X. We distinguish three cases depending on whether the →_{β⊥} reduction reduces a subterm in C[ ], M or N.

• A →_{β⊥} reduction step in C[ ] can cause substitutions of variables by terms belonging to Λ_{⊥} inside M and N. Hence the resulting term will be of the form C′[A(M′N′)]. Since M is strong zero (a property closed under substitution), the term M′ is strong zero too and A(M′N′) can be contracted. This gives rise to the following reduction diagram.

\xymatrix{C[A(MN)] \ar[r]^{β⊥} \ar[d]_{OA} & C′[A(M′N′)] \ar[d]^{OA} \\ C[N] \ar[r]_{β⊥} & C′[N′]}

• A →_{β⊥} reduction step in M does not affect the A(MN), because strong zero terms are closed under reduction. This gives us the diagram:

[figure: C[A(MN)]; β⊥; OA; C[A(M′N)]; OA; C[N]; C[N]]

• Finally a →_{β⊥}-reduction step in N commutes trivially:

\xymatrix{C[A(MN)] \ar[r]^{β⊥} \ar[d]_{OA} & C[A(MN′)] \ar[d]^{OA} \\ [N] \ar[r]_{β⊥} & C[N′]}

□

Proposition 2.15 There is at most one OA-redex in a term belonging to Λ_{OA⊥}. Hence →_{OA} is trivially confluent.

Proof. By definition O or A symbols in a term belonging to Λ_{OA⊥} can occur only on the left-spine. Moreover it follows from the conditions on the rules for O and A that a prerequisite for OX and AX to be an OA-redex is that X belongs to Λ_{⊥}. Therefore only the innermost occurrence of O or A can be a redex. □

Lemma 2.16 (i) The relation →_{β} is confluent in Λ_{OA}. (ii) The relation →_{β⊥} is confluent in Λ_{OA⊥}.

Proof. Because the O and A symbols are here not reduced they can be thought of as fresh free variables. Hence (i) and (ii) follow from the confluence property for →_{β} in Λ (see [4], Theorem 3.28) and →_{β⊥} in Λ_{⊥} (see [16,17]) respectively. □

Theorem 2.17 (i) The relation →_{βOA} is confluent in Λ_{OA}. (ii) The relation →_{β⊥OA} is confluent in Λ_{OA⊥}.

Proof. The Hindley-Rosen Lemma [4] states that if we know that two reduction relations →_{1} and →_{2} both are confluent, and that →_{1} commutes with →_{2}, then (→_{1} ∪ →_{2})^{∗} is confluent. The previous three lemmas imply these conditions both for →_{β} and →_{OA}, and for →_{β⊥} and →_{OA}. □

Remark 2.18 The extended calculus Λ_{OA} and the reduction rules (O) and (A) were chosen carefully in order to get confluent reduction relations.

• If we had allowed terms like (λx.O(ΩxΩ))A in Λ_{OA}, the extended calculus would not longer have been confluent. The term (λx.O(ΩxΩ))A can reduce to both ΩA and O(ΩAΩ), which cannot be joined.

• The condition on strong zero terms in the new rules (O) and (A) cannot be weakened to zero terms, because of loss of confluence, as shown by the following example: (λx.A(xI))I would reduce to both I and A(II). The term A(II) rewrites to the normal form AI and cannot be joined with I.

3 Observational equivalence implies tree equality

In this section we will prove that observational equivalence with respect to the extended calculus Λ_{OA} implies equality of Berarducci trees. The proof will be a variant of the Böhm out technique [4] defined for Böhm trees.

Some terminology first: A path^{3} is a finite string of 1’s and 2’s. The empty path is denoted by ⟨⟩. If a path u is a proper prefix of v we write u < v. Given a tree T and a path u, the subtree T |u, when it exists, is a subtree of T defined inductively thus:

• T | ⟨⟩ = T

• \begin{matrix}λx \\ T \end{matrix} | 1 · u = T |u

• [figure: @; T_{1}; T_{2}] | 1 · u = T_{1}|u

• [figure: @; T_{1}; T_{2}] | 2 · u = T_{2}|u

The label at the root of a tree T is denoted by ρ(T) and defined by cases:

ρ(x) = x, ρ( \begin{matrix}λx \\ T \end{matrix} ) = λx, ρ( [figure: @; T_{1}; T_{2}] ) = @, and ρ(⊥) = ⊥.

3 Synonyms in literature [17] are position and occurrence, we use here the terminology of [4].

Like in Definition 10.4.6 of [4] we will say that a path is useful to discriminate between two terms if looking at the corresponding Berarducci trees the labeled nodes traversed by the path are identical, while the labeled nodes at the end of the path are different.

Definition 3.1 A path u is useful for two trees T, T′ if ρ(T |v) = ρ(T′|v) for all v < u but ρ(T |u) ≠ ρ(T |u).

We will use substitutions that map any variable in Λ to a term in {Ω, ΩΩ}. More precisely we will consider the substitution σ_{Ω} defined by

σ_{Ω}(x) = Ω for all variables x

and the substitutions σ_{Ω}^{x}, one for each variable x, defined by

σ_{Ω}^{x}(y) = \{ \begin{matrix}ΩΩ & if x = y \\ Ω & otherwise. \end{matrix}

Lemma 3.2 Let M ∈ Λ be a zero term with respect to →_{β} and let σ be the substitution σ_{Ω} or σ_{Ω}^{x} for some fixed x. Then the substitution instance M^{σ} is a strong zero term with respect to →_{β}.

Proof. If M is a strong zero term with respect to →_{β}, then so is M^{σ} for all σ by definition. Otherwise M is convertible to a term of the shape yN_{1} … N_{n} for some variable y. Hence M^{σ} = ΩN_{1}^{σ} … N_{n}^{σ} or M^{σ} = ΩΩN_{1}^{σ} … N_{n}^{σ}, which are both strong zero terms with respect to →_{β}. □

Theorem 3.3 For all M, N ∈ Λ it holds that

∀C[ ] ∈ Λ_{OA} C[M] ∈ R_{OA} ⟺ C[N] ∈ R_{OA} ⇒ T (M) = T (N).

Proof. By contraposition. Let M, N be terms in Λ such that T (M) ≠ T (N). Then there exists a path u that is useful for T (M) and T (N). Depending on what label we see at the root of T (M)|u and T (N)|u, we define a substitution σ as follows:

• If T (M)|u = x and T (N)|u = y, let σ be σ_{Ω}^{x}.

• If T (M)|u = x and T (N)|u = ⊥ or conversely, let σ be σ_{Ω}^{x}.

• In all other cases let σ be σ_{Ω}.

By induction on the length of u we will define a context C[ ] that can discriminate M and N with respect to σ in the sense that either C[M^{σ}] ∈ R_{OA} and C[N^{σ}] ∉ R_{OA}, or vice versa.

Base case: u = ⟨⟩.

• If T (M) or T (N) is a leaf, then we choose C[ ] = [ ] as context to discriminate M and N with respect to σ. We have four subcases:

· if T (M) = x and T (N) = y then M^{σ} = ΩΩ and N^{σ} = Ω; · if T (M) = x and T (N) = ⊥ (or vice versa) then M^{σ} = ΩΩ ∉ R_{OA} and N^{σ} ∈ R_{OA} (or vice versa); · if T (M) is not a leaf and T (N) = x (or vice versa) then M^{σ} ∉ R_{OA} and N^{σ} = Ω ∈ R_{OA} (or vice versa); · if T (M) is not a leaf and T (N) = ⊥ (or vice versa) then M^{σ} ∉ R_{OA} and N^{σ} ∈ R_{OA} (or vice versa).

• If T (M) = [figure: @; T (M_{1}); T (M_{2})] and T (N) = \begin{matrix}λx \\ T (N_{1}) \end{matrix} (or vice versa),

then we choose C[ ] = A(O[ ]Ω). By the shape of T (M) it follows that M_{1} is a zero term with respect to →_{β}. Hence M_{1}^{σ} is a strong zero term with respect to →_{β} by Lemma 3.2. We get C[M^{σ}] = A(O(M_{1}^{σ}M_{2}^{σ})Ω) →_{βOA} A(M_{1}^{σ}Ω) →_{βOA} Ω, while C[N^{σ}] = A(O(λx.N_{1})^{σ}Ω) is rootstable with respect to →_{βOA} being irreducible.

Induction step: u = i · v.

• Suppose T (M) = [figure: @; T (M_{1}); T (M_{2})] and

T (N) = [figure: @; T (N_{1}); T (N_{2})].

If i = 1 then by the induction hypothesis we have a context C′[ ] that discriminates M_{1}, N_{1} with respect to σ. Then we define C[ ] = C′[O[ ]]. As in the base case we get that M_{1}^{σ} is a strong zero term with respect to →_{β}. Now clearly C[M^{σ}] = C′[O M^{σ}] = C′[O(M_{1}^{σ}M_{2}^{σ})] →_{βOA} C′[M_{1}^{σ}]. Similarly we see that C[N^{σ}] = C′[O(N_{1}^{σ}N_{2}^{σ})] →_{βOA} C′[N_{1}^{σ}]. Hence by induction C[ ] discriminates M and N with respect to σ.

If on the other hand i = 2, then by the induction hypothesis there is a context C′[ ] that discriminates M_{2} and N_{2} with respect to σ. We now choose C[ ] = C′[A[ ]] to discriminate M and N with respect to σ. The proof proceeds now as before. Again M_{1} is a zero term with respect to →_{β}, and M_{1}^{σ} is a strong zero term with respect to →_{β}. So we can calculate that C[M^{σ}] = C′[A M^{σ}] = C′[A(M_{1}^{σ}M_{2}^{σ})] →_{βOA} C′[M_{2}^{σ}] and similarly we see that C[N^{σ}] = C′[A(N_{1}^{σ}N_{2}^{σ})] →_{βOA} C′[N_{2}^{σ}]. Hence by induction C[ ] discriminates M and N with respect to σ.

• Suppose T (M) = \begin{matrix}λx \\ T (M_{1}) \end{matrix} and T (N) = \begin{matrix}λx \\ T (N_{1}) \end{matrix} . Then i = 1.

Let C′[ ] be the context that by induction hypothesis discriminates M_{1} and N_{1}. We now choose C[ ] = C′[[ ]σ(x)]. We observe that C[M^{σ}] = C′[(λx.M_{1})^{σ}σ(x)] →_{βOA} C′[M_{1}^{σ}] and similarly we see that C[N^{σ}] = C′[(λx.N_{1})^{σ}σ(x)] →_{βOA} C′[N_{1}^{σ}]. Hence by induction C[ ] discriminates M and N with respect to σ.

[figure: @; ⊥; x; @; @; λx; λx; x; x; @; @; λx; λx; λy; λy; x; x; @; @; ⊥; x; @; @; @; x; ⊥ ⊥; x]

Fig. 1. Berarducci trees of Ωx, Ω_{I}, Ω_{K}, and x(xΩ(Ωx))Ω.

Recapitulating, given the two terms M, N in Λ and a path u that is useful to discriminate their Berarducci trees, we have constructed a substitution σ and a discriminating context C′[ ]. We now build from C′[ ] and σ the new context

C[ ] = (λx_{1}...x_{n}.C′[ ])σ(x_{1}) … σ(x_{n}),

where x_{1}, … x_{n} is the set of free variables in M and N. Because C[M] = (λx_{1}...x_{n}.C′[M])σ(x_{1}) … σ(x_{n}) →_{βOA}^{∗} C′[M^{σ}] (being C′[ ] closed) and similarly C[N] →_{βOA}^{∗} C′[N^{σ}] and by construction C′[ ] discriminates M, N with respect to σ, we get that C[M] ∈ R_{OA} and C[N] ∉ R_{OA}, or vice versa. □

Example 3.4 The Berarducci trees of some terms considered in this example are shown in Figure 1.

(i) When M = Ω, N = ΩΩ and u = ⟨⟩ the above procedure gives us the empty context as a discriminating context for M and N.

(ii) If M = Ω, N = Ωx, and u = ⟨⟩, then we find that C[ ] = (λx.[ ])Ω

discriminates M and N. (iii) For M = Ωx, N = Ωy and u = 2 we find that C[ ] = (λxy.A[ ])(ΩΩ)Ω is

a discriminating context. (iv) Let M = Ω_{I}, N = Ω_{K}, and u = 2 · 1. The discriminating context we

obtain is the same mentioned in Section 2, i.e. C[ ] = A[ ]Ω.

(v) In case of M = x(xΩ(Ωx))Ω, N = y(yΩ(Ωy))Ω, and u = 1 · 2 · 2 · 2, a discriminating context is C[ ] = (λxy.A(A(A(O[ ]))))(ΩΩ)Ω.

This last case shows the power of the constants O, A. One problem in constructing such discriminating contexts is that different occurrences of the same variable may have to be used to select different arguments. This problem was solved in the original algorithm of Böhm by using suitable combinators which equate η-convertible terms (see Section 10.4 of [4]) and in [23], [12], [11] by allowing a non-deterministic choice operator. In all these cases the technique is to replace different occurrences of the same variable by different terms. Instead, in the above algorithm for Berarducci trees the selection is performed by the two constants O and A while the variables always get substituted by Ω or ΩΩ.

4 From Berarducci tree equality to observational equivalence via infinite rewriting

In this section we will represent Berarducci trees explicitly as terms. Then the Berarducci tree T (M) of a term M of Λ is nothing else but the (possibly infinite) unique normal form of M in the infinitary extension Λ_{⊥}^{∞} as shown in [16,18]. In this term interpretation, the previous coinductive construction of Berarducci tree translates into a parallel outermost reduction strategy which replaces occurring outermost rootactive subterms by ⊥. Because Berarducci trees of finite terms can be infinite (cf. Ω_{I} in Figure 1) one has to consider (possibly infinite) strongly convergent reductions. The fact that Λ_{⊥}^{∞} is infinitary confluent and has the unique normal form property has the following corollary:

Corollary 4.1 [24] For all terms M and contexts C[ ] in Λ_{⊥}^{∞} it holds that T (C[M]) = T (C[T (M)]).

The proof is simple, just recognize that the left hand side and the right hand side of the equation represent two ways of reducing to the unique normal form of C[M]. It follows immediately from the corollary that Berarducci tree equality in Λ_{⊥}^{∞} implies observational equivalence in Λ_{⊥}^{∞}. Formulated like this the result is actually stronger than Theorem 1.3, because it quantifies over Λ_{⊥}^{∞} instead of Λ.

The topic of this paper are Berarducci trees of terms in the extension Λ_{OA}. The goal of this section is to prove along similar lines as for Λ_{⊥}^{∞} that Berarducci tree equality in Λ_{OA⊥}^{∞} implies observational equivalence in Λ_{OA⊥}^{∞}.

Our first step is to define (possible infinite) strongly convergent reductions for Λ_{OA⊥}^{∞} and show that these reductions are infinitary confluent. Because terms in Λ_{OA⊥}^{∞} contain at most a finite number of symbols O and A we can base the proof via a few straightforward lemmas on the infinitary confluence of Λ_{⊥}^{∞}.

4.1 Strongly convergent reductions in Λ_{OA⊥}^{∞}

Infinite reductions that converge to a normal form have the nice property that the depth of the reduced redexes goes to infinity along the reduction. Such reductions are called strongly convergent.

Depending on the reduction order even a strongly convergent reduction to normal form may take more than ω steps. In fact such reductions can be of any countable ordinal length as shown in [15]. For example Ω_{x} reduces in ω many steps to (((… x)x)x). If we abbreviate this reduction by Ω_{x} →_{ω} (((… x)x)x), then we see that Ω_{x}Ω_{x} →_{ω} ((((… x)x)x)Ω_{x} →_{ω} ((((… x)x)x)(((… x)x)x is a leftmost outermost reduction to normal form of length ω + ω. Of course depth-first outermost reduction would have found this normal form faster in ω steps.

The definition of a transfinite strongly convergent reduction is somewhat lengthy. Using terminology from topology we can give a concise definition. We first define depth of a redex and distance between two terms. After the definition we give a few concrete instances, enough to apply to the reduction sequences we will encounter later in this section.

In analogy to the subtree T | u of T at the path u for trees (defined at page 13) we define the subterm X | u of the term X at the path u, when it exists. We need the extra clauses:

• (OX) | 1 · u = X | u,

• (AX) | 1 · u = X | u.

Similarly we extend the definition of the root label as follows:

• ρ(OX) = O,

• ρ(AX) = A.

In this way the set Λ_{OA⊥}^{∞} inherits from Definition 3.1 the notion of useful path.

Definition 4.2 ^{•} The depth of a subterm Y at path u in X ∈ Λ_{OA⊥}^{∞} is the

length of the path u.

• The distance d(X, Y) of two terms X, Y ∈ Λ_{OA⊥}^{∞} is 0 if X and Y are identical and is 2^{−k} if k is the length of the shortest path useful for X and Y.

With this distance Λ_{OA⊥}^{∞} becomes a complete metric space.

Definition 4.3 [15,18] A transfinite reduction with respect to a given reduction relation →_{R} of length α, where α is any ordinal number, is a function from α to reduction steps in →_{R} , of the form { X_{β} →_{R} X_{β+1} | β < α }. It is weakly continuous (resp. weakly convergent) if the induced function from ordinals to terms is continuous (resp. convergent) with respect to the usual topology on ordinals and the metric on terms. It is strongly continuous (resp. strongly convergent) if it is weakly so, and in addition, for every limit ordinal λ < α (resp. λ ≤ α) the sequence { d_{β} | β < λ } of the depths of the redexes it reduces tends to infinity.

This dense definition implies concretely that

• finite reductions are strongly convergent,

• a reduction sequence X_{0} →_{R} X_{1} →_{R} … is weakly convergent with limit X_{ω} if for all real numbers ϵ > 0 there is a n such that d(X_{n}, X_{ω}) < ϵ for all m > n,

• X_{0} →_{R} X_{1} →_{R} … is strongly convergent if it is weakly convergent and lim_{n→∞} d_{n} = ∞, • composition of a finite number of strongly convergent reduction sequences

is again strongly convergent.

Example 4.4 ^{•} Ω_{I} →_{β} Ω_{I}I →_{β} … is strongly convergent with limit the

infinite term (((…)I)I)I.

• O(ΩΩ) →_{OA} Ω →_{β} Ω →_{β} … is weakly convergent but not strongly convergent, as the depth of the reduced redexes is always zero.

• Let B denote λx.I(xx). Then BB →_{β} I(BB) →_{β} BB →_{β} I(BB) →_{β} … is not weakly convergent.

• Weakly convergent reductions are not confluent: Y(λy.K(Kyx)z) can reduce to the normal forms of both Y(λy.Kyx) and Y(λy.Kyz) which don’t have a common reduct. Here Y is the Turing fixpoint combinator, i.e. Y ≡ (λxy.y(xxy))(λxy.y(xxy)).

• Ω →_{⊥} ⊥, BB →_{⊥} ⊥, and Y(λy(K(Kyx)z)) →_{⊥} ⊥.

All this restricts to reductions in Λ_{⊥}^{∞}: a reduction in Λ_{⊥}^{∞} is strongly convergent if it is strongly convergent in Λ_{OA⊥}^{∞}.

Definition 4.5 Let →_{R} be a reduction relation. Then → →_{R} denotes a strongly convergent reduction with respect to →_{R}.

4.2 Confluence of strongly convergent reductions in Λ_{OA⊥}^{∞}

We will prove confluence of strongly convergent reductions in Λ_{OA⊥}^{∞} along the same lines as we proved confluence of finite reductions in Λ_{OA⊥}.

Lemma 4.6 (i) The relation →_{OA} commutes with the relation → →_{β⊥}. (ii) There is at most one OA-redex in a term belonging to Λ_{OA⊥}^{∞}. (iii) The relation → →_{β⊥} is confluent.

Proof.

(i) Similar to the finite case considered in Lemma 2.14. After construction of the three base cases the proof proceeds now by induction to the ordinal length of → →_{β⊥}. The limit ordinals are the interesting case: we construct

[figure: C[A(MN)]; β⊥; OA; C_{1}[A(M_{1}N_{1})]; OA; β⊥; C_{2}[A(M_{2}N_{2})]; OA; C_{λ}[A(M_{λ}N_{λ})]; OA; C[N]; β⊥; C_{1}[N_{1}]; β⊥; C_{2}[N_{2}]; C_{λ}[N_{λ}]]

Observe that the depth of the occurrences of A in the terms on the top row becomes fixed after a while. If that would not be the case, then by the strong convergence property there would be no A present in the limit. Now it is routine to verify that the reduction in the bottom row inherits the strongly convergent property of the reduction in the top row.

(ii) As in Lemma 2.15. (iii) One can use the infinitary confluence property for Λ_{⊥}^{∞} proved in [16,17]

in combination with the same observation as for the finite version (Lemma 2.16).

□

Theorem 4.7 The relation → →_{β⊥OA} is confluent in Λ_{OA⊥}^{∞}:

\xymatrix{X \ar@{->>}[r]^{β⊥OA} \ar@{->>}[d]_{β⊥OA} & Y_{1} \ar@{->>}[d]^{β⊥OA} \\ Y_{2} \ar@{->>}[r]_{β⊥OA} & Z}

Proof. Similar to the proof of Theorem 2.17 using the Hindley-Rosen Lemma and Lemma 4.6. □

Corollary 4.8 Every term in Λ_{OA⊥}^{∞} has a unique normal form.

Proof. One can construct a normal form by a depth-first outermost strategy in which ⊥ steps have priority over β, O and A steps. Hence inside rootactive terms no reduction will take place, and instead they will sooner or later be replaced as a whole by ⊥. The resulting reduction is strongly convergent: if not, there would be a rootactive subterm at some stage that would not be replaced by ⊥. But the strategy was depth-first outermost, so this cannot happen. Uniqueness follows from previous confluence result. □

4.3 From tree equivalence to observational equivalence

We have now all the machinery to pull the rabbit out of the hat. First we will extend the tree definition of Berarducci tree from terms in Λ to terms in Λ_{OA⊥}^{∞} and we show the correspondence with the unique normal forms. We conclude with a proof that Berarducci tree equality in Λ_{OA⊥}^{∞} implies observational equivalence in Λ_{OA⊥}^{∞}.

Definition 4.9 The Berarducci tree T (X) of a term X ∈ Λ_{OA⊥}^{∞} is defined by cases as follows:

(i) if X →_{βOA}^{∗} x then T (X) = x (ii) if X →_{βOA}^{∗} ⊥ then T (X) = ⊥

(iii) if X →_{βOA}^{∗} λx.Y then T (X) = \begin{matrix}λx \\ T (Y) \end{matrix}

(iv) if X →_{βOA}^{∗} Y M and Y is a zero term with respect to →_{βOA} then

T (X) = [figure: @; T (Y); T (M)].

(v) if X →_{βOA}^{∗} OY and Y is a OA-blocker with respect to →_{βOA} then T (X) =

\begin{matrix}O \\ T (Y) \end{matrix}

(vi) if X →_{βOA}^{∗} AY and Y is a OA-blocker with respect to →_{βOA} then T (X) =

\begin{matrix}A \\ T (Y) \end{matrix}

(vii) otherwise (exactly when X is rootactive with respect to →_{βOA}), T (X) = ⊥.

For example A(xΩ_{I}) → →_{βOA} A(x((… I)I)) with the following tree structure:

[figure: A; x; @; @; I; I]

Corollary 4.10 The parse tree of the infinite normal form of a term X ∈ Λ_{OA⊥}^{∞} is given by T (X), i.e. the Berarducci tree of X.

Proof. By coinduction on the structure of Berarducci tree of a term X ∈ Λ_{OA⊥}^{∞} using Lemma 2.12 to match the last clause of Definition 4.9 with rule (⊥). □

Corollary 4.11 For all terms X ∈ Λ_{OA⊥}^{∞} and context C[ ] ∈ Λ_{OA⊥}^{∞} it holds that T (C[T (X)]) = T (C[X]).

Proof. From C[X] we can construct a normal form via depth-first outermost reduction. By Theorem 4.8 this normal form is equal to the normal form obtained by first reducing X to normal form T (X) and then reducing C[T (X)] to normal form, as shown in the following diagram (identifying terms with their parse trees):

[figure: C[X]; β⊥OA; β⊥OA; C[T (X)]; β⊥OA; T (C[X]); T (C[T (X)])]

□

Finally we can prove that Berarducci tree equality in Λ_{OA⊥}^{∞} implies observational equivalence in Λ_{OA⊥}^{∞}.

Theorem 4.12 For all X, Y ∈ Λ_{⊥}^{∞}, T (X) = T (Y) implies

∀C[ ] ∈ Λ_{OA⊥}^{∞}. C[X] ∈ R_{OA⊥}^{∞} ⟺ C[Y] ∈ R_{OA⊥}^{∞},

where R_{OA⊥}^{∞} is the set of terms in Λ_{OA⊥}^{∞} which are rootactive with respect to →_{βOA}.

Proof. Let X, Y be terms in Λ_{⊥}^{∞}. Suppose T (X) = T (Y). Let C[ ] be a context in Λ_{OA⊥}^{∞}. Using the previous corollary we get:

T (C[X]) = T (C[T (X)])
= T (C[T (Y)])
= T (C[Y]).

Suppose C[X] ∈ R_{OA⊥}^{∞}. Then T (C[X]) = ⊥. Hence also T (C[Y]) = ⊥. And so we find that C[Y] ∈ R_{OA⊥}^{∞}. We conclude that X and Y are observational equivalent. □

Specializing the above theorem to the case X, Y ∈ Λ and C[ ] ∈ Λ_{OA} we obtain the converse of Theorem 3.3, i.e.:

Theorem 4.13 For all M, N ∈ Λ, T (M) = T (N) implies

∀C[ ] ∈ Λ_{OA}. C[M] ∈ R_{OA} ⟺ C[N] ∈ R_{OA}.

5 Conclusion

In this paper we study equivalence relations on the pure lambda calculus. In denotational semantics we consider equivalent two terms with the same meaning. In operational semantics the equivalent terms are those which behave in the same way when put in given contexts. Here we take as meaning of a term its Berarducci tree, and the behavior that we observe is whether or not a term has a rootstable form. As expected denotational equivalence implies operational equivalence, or more concretely put, Berarducci tree equality implies observational equivalence. The converse is not true for the pure lambda calculus, because the set of contexts is not expressive enough. One way of increasing the expressivity is by enlarging the set of contexts. We do this by defining an extension Λ_{OA} of the pure lambda calculus for which we can show that Berarducci tree equality of pure lambda terms coincides with observational equivalence. This means that Berarducci tree equality of pure lambda terms is fully abstract [20] for the extended lambda calculus. The above result does not holds for terms of the extended lambda calculus. For example O(AΩ) and O(OΩ) have different Berarducci trees but their behavior is the same in all contexts of Λ_{OA}. We plan to look for a calculus which allow to observe the differences between all terms of Λ_{OA} not semantically equal.

In [23] Sangiorgi proves that adding well-formed operators to pure lambda calculus we cannot discriminate more than Lévy-Longo trees do. As a matter of fact, our operators A, O are not well-formed according to the Groote-Vaandrager format allowed in [23]. The reason is that this format does not allow a premise asking for a term to be a strong zero term. In this respect our development completely agrees with that of Sangiorgi. We criticize only the following sentence from the introduction of [23]: “well-formed operators, intuitively operators whose behavior only depends on the semantics - not on the syntax - of their operands”. We think that the reduction rules of A, O depend on the semantics of their operands, since the notion of being a strong zero term is a semantical one, as shown by the observation that all and only the strong zero terms are equated to bottom in the Plotkin-Scott-Engeler models [19].

References

[1] S. Abramsky and C.-H. L. Ong. Full abstraction in the lazy lambda calculus. Inform. and Comput., 105(2):159–267, 1993.

[2] R. M. Amadio and P.-L. Curien. Domains and lambda-calculi. Cambridge University Press, Cambridge, 1998.

[3] F. Barbanera, M. Dezani-Ciancaglini, and F.-J. d. Vries. Types for trees. In PROCOMET’98 (Shelter Island, 1998), pages 6–29. Chapman & Hall, London, 1998.

[4] H. P. Barendregt. The lambda calculus Its syntax and semantics. North-Holland Publishing Co., Amsterdam, revised edition, 1984.

[5] M. Barr. Terminal coalgebras in well-founded set theory. Theoret. Comput. Sci., 114(2):299–315, 1993.

[6] J. Barwise and L. Moss. Vicious circles. CSLI Lecture Notes Number 60, CSLI Publications, Stanford, 1996.

[7] A. Berarducci. Infinite λ-calculus and non-sensible models. In Logic and algebra (Pontignano, 1994), pages 339–377. Dekker, New York, 1996.

[8] G. Boudol. Lambda-calculi for (strict) parallel functions. Inform. and Comput., 108(1):51–127, 1994.

[9] G. Boudol and C. Laneve. The discriminating power of multiplicities in the λ-calculus. Inform. and Comput., 126(1):83–102, 1996.

[10] M. Dezani-Ciancaglini, U. de’Liguoro, and A. Piperno. A filter model for concurrent λ-calculus. SIAM J. Comput., 27(5):1376–1419 (electronic), 1998.

[11] M. Dezani-Ciancaglini, B. Intrigila, and M. Venturini-Zilli. Böhm’s theorem for Böhm trees. In ICTCS’98 (Prato, 1998), pages 1–23. World Scientific, Oxford, 1998.

[12] M. Dezani-Ciancaglini, J. Tiuryn, and P. Urzyczyn. Discrimination by parallel observers: the algorithm. Inform. and Comput., 150(2):153–186, 1999.

[13] M. Hyland. A syntactic characterization of the equality in some models for the lambda calculus. J. London Math. Soc. (2), 12(3):361–370, 1975/76.

[14] B. Jacobs and J. Rutten. A tutorial on (co)algebras and (co)induction. Bulletin of EATCS, 62:222–259, 1997.

[15] R. Kennaway, J. W. Klop, R. Sleep, and F.-J. d. Vries. Transfinite reductions in orthogonal term rewriting systems. Inform. and Comput., 119(1):18–38, 1995.

[16] R. Kennaway, J. W. Klop, R. Sleep, and F.-J. d. Vries. Infinitary lambda calculus. Theoret. Comput. Sci., 175(1):93–125, 1997.

[17] R. Kennaway, V. v. Oostrom, and F.-J. d. Vries. Meaningless terms in rewriting. J. Funct. Logic Programming, Article 1:35 pp, 1999. (electronic) http://www.cs.tu-berlin.de/journal/jflp/articles/1999/A99-01/A99-01.html.

[18] R. Kennaway and F.-J. d. Vries. Infinitary rewriting. To appear as chapter in a book on rewriting edited by J. W. Klop. Draft is available at http://www.etl.go.jp/ ferjan/drafts.html, 2000.

[19] G. Longo. Set-theoretical models of λ-calculus: theories, expansions, isomorphisms. Ann. Pure Appl. Logic, 24(2):153–188, 1983.

[20] R. Milner. Fully abstract models of typed λ-calculi. Theoret. Comput. Sci., 4:1–22, 1977.

[21] J.-H. Morris. Lambda calculus models of programming languages. PhD thesis, M.I.T., 1968.

[22] G. Plotkin. LCF considered as a programming language. Theoret. Comput. Sci., 5:223–256, 1977.

[23] D. Sangiorgi. The lazy lambda calculus in a concurrency scenario. Inform. and Comput., 111(1):120–153, 1994.

[24] F.-J. d. Vries. Böhm trees, bisimulations and observations in lambda calculus. In Second Fuji International Workshop on Functional and Logic Programming Workshop, pages 230–245. World Scientific, Singapore, 1997.

[25] C. P. Wadsworth. The relation between computational and denotational properties for Scott’s D_{∞}-models of the lambda-calculus. SIAM J. Comput., 5(3):488–521, 1976.