Infinitary Lambda Calculus and Discrimination of Berarducci Trees ^{1}

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

Fer-Jan de Vries^{c,3}

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 Department of Mathematics & Computer Science, University of Leicester,

University Road, Leicester, LE1 7RH, United Kingdom E-mail: ferjan@mcs.le.ac.uk

We propose an extension of lambda calculus for which the Berarducci trees equality coincides with observational equivalence, when we observe rootstable or rootactive behavior of terms. In one direction the proof is an adaptation of the classical Böhm out technique. In the other direction the proof is based on confluence for strongly converging reductions in this extension.

Key words: Berarducci trees, observational equivalence, infinitary lambda calculus, Böhm out technique.

1 Introduction

In this paper we will prove equivalent an operational and a denotational semantics for lambda calculus with the β-rule. Both semantics are based on the

1 This paper was made possible thanks to the hospitality ETL offered in March 1999 to both Mariangiola Dezani and Paula Severi. 2 Partly supported by MURST COFIN’99 TOSCA Project and CNR-GNSAGA. 3 Part of this paper was completed when the third author was employed by ETL in Tsukuba, Japan. He acknowledges the excellent research conditions offered by ETL.

set of rootactive terms, which is the smallest set of computational meaningless terms that can consistently be equated. The operational semantics that we are interested in is observational equivalence with respect to rootactive behavior. The denotational semantics is the model of the Berarducci trees (Berarducci, 1996), which are a more detailed variant of Böhm trees: the main difference being that rootactive terms instead of terms without a head normal form get replaced by a dummy symbol ⊥.

Berarducci trees can be best dealt with as the β-⊥-normal forms of terms in the completion Λ_{⊥}^{∞} of the lambda calculus with a new symbol ⊥, infinite terms and the new rule that replaces β-rootactive terms by ⊥ (Berarducci, 1996), (Kennaway et al., 1997). In the calculus Λ_{⊥}^{∞} it is not difficult to see that if two terms have the same Berarducci tree then they are observationally equivalent. The converse however is not true, essentially for two reasons. The first reason is intrinsic for Berarducci trees: the lambda calculus is not powerful enough to Böhm out the argument of a β-rootactive term. The second reason is similar to why the analogous statement is not true for Böhm trees, namely the Böhm out of a subterm can return an η-expansion of it.

Therefore, in a move characteristic for full abstractness problems, we will enrich the lambda calculus Λ_{⊥}^{∞} in a rather minimal way with two more constants O and A with accompanying rules. Any term in the enriched calculus Λ_{⊥OA}^{∞} can reduce in a finite number of steps to a pure λ-term and therefore the Berarducci tree of a term in Λ_{⊥OA}^{∞} will not contain O and A. For any two terms of Λ_{⊥OA}^{∞} we can prove that Berarducci tree equality is equivalent to observational equivalence with respect to rootactive terms.

1.1 Previous Work

Historically, quoting from (Barendregt, 1984)(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 (Barendregt, 1984)(Section 10.3).

In (Wadsworth, 1976) Wadsworth, generalizing Böhm’s theorem, shows that two λ-terms M, N have the same Böhm tree modulo infinite η-expansions if and only if 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 the “if” part is the Böhm out technique.

The same property holds even considering Böhm trees modulo finite η-ex-pansions and normal forms, as shown in (Hyland, 1975/76). More precisely Hyland proves, using the Böhm out technique, that two λ-terms M, N have the same Böhm tree modulo finite η-expansions if and only if for all contexts C[ ] the following holds:

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

The results of (Wadsworth, 1976) and (Hyland, 1975/76) 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 et al. (Dezani-Ciancaglini et al., 1998b) add to the pure lambda calculus a nondeterministic choice operator + and an adequate numeral system (as defined in Section 6.4 of (Barendregt, 1984)). The reduction rules for + are:

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

Clearly the non-deterministic choice operator allows to define combinators like Plotkin’s parallel-or (Plotkin, 1977) when one considers may convergence, under which a term converges if at least one of the possible computations 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 (Milner, 1977), to have a fully abstract interpretation for the language. The numerals play an essential role to discriminate between a term possessing a head normal form and its η-expansion, essentially since they can never be applied to an argument, while all pure λ-terms can be seen both as functions and as arguments. This result is proved using a variation of the Böhm out technique as well as characteristic terms and test terms (Boudol, 1994).

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 (Sangiorgi, 1994), (Boudol and Laneve, 1996), (Dezani-Ciancaglini et al., 1999). Now, we briefly recall such approaches.

In (Sangiorgi, 1994), 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.

Boudol and Laneve (Boudol and Laneve, 1996) 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 et al. (Dezani-Ciancaglini et al., 1999) consider the behavior of pure λterms inside contexts of the concurrent lambda calculus as defined in (Dezani-Ciancaglini et al., 1998a). This calculus is obtained from the pure lambda calculus (with call-by-value and call-by-name variables) by adding the nondeterministic 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 for proving that observational equivalence implies tree equality is that of characteristic terms and test terms.

More recently Boudol in (Boudol, 2000) shows that the equivalence on λ-terms induced by the call-by-name CSP transform is Lévy-Longo tree equality.

In order to discriminate pure λ-terms having different Berarducci trees, the paper (Dezani-Ciancaglini et al., 2000) extends the lambda calculus with two constants O and A. The essential feature of the Böhm-out technique consists in selecting a subtree of the tree of a term by means of an appropriate context. The selection of a subtree was performed in the original Böhm algorithm by substituting a variable in head position by an appropriate combinator. For Berarducci trees, the top normal forms also include applications that may not have a variable in head position, as in ΩΩ (where Ω ≡ (λx.xx)(λx.xx)). For these new cases the selection of a subtree can be performed using the constants O and A. The constants O and A select the operator and the argument of a closed, β-rootstable application. These constants have the following reduction rules:

O(MN) ⟶ M if M is a closed β-zero term
A(MN) ⟶ N if M is a closed β-zero term

where a β-zero term is defined in Definition 2. For instance, ΩII (where I ≡ λx.x) and ΩΩI are discriminated by the context A(O[ ]). In fact:

A(O(ΩII)) ⟶ A(ΩI) ⟶ I

A(O(ΩΩI)) ⟶ A(ΩΩ) ⟶ Ω

All pure λ-terms having different Berarducci trees can be discriminated using these two constants (Dezani-Ciancaglini et al., 2000). However non-pure λterms having different Berarducci trees cannot be discriminated only with these rules. For example, O(AΩ) and O(OΩ) have different Berarducci trees, though they are observationally equivalent. Hence in this paper we add more reduction rules for the constants O and A in order to discriminate also nonpure λ-terms.

1.2 Summary

In this paper we consider an extended lambda calculus Λ_{OA} for which the equality of Berarducci trees coincides with observational equivalence. This calculus will be a variant of the one presented in (Dezani-Ciancaglini et al., 2000). As in (Dezani-Ciancaglini et al., 2000) it will contain the constants O and A that select the operator and argument of a β-rootstable application. The set Λ_{OA} of terms will be a restriction of the one in (Dezani-Ciancaglini et al., 2000) and new reduction rules will be added for the constants. In (Dezani-Ciancaglini et al., 2000), we have proved that Berarducci tree equality coincides with observational equivalence only for pure λ-terms. The new reduction rules will allow us to extend this result to non-pure λ-terms. Hence in this paper, we will prove:

Theorem 1 For all X, Y ∈ Λ_{OA} it holds that they have the same Berarducci tree if and only if for all contexts C[ ] ∈ Λ_{OA}

C[X] ∈ R_{OA} ⇔ C[Y] ∈ R_{OA}

where R_{OA} is the set of βOA-rootactive terms in Λ_{OA}.^{4}

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. We will prove that the Berarducci tree of a term is the unique normal form of the term in that calculus. Since this normal form always exists and is unique, we can build a model of the extended lambda calculus in which the interpretations of

4 The definition of βOA-rootactive is given in Definition 27.

terms are their Berarducci trees. Hence, our main theorem states that such a model of the extended lambda calculus is fully abstract.

1.3 Outline

In Section 2 we recall the definition of the finite lambda calculus Λ and its infinitary extension Λ_{⊥}^{∞}. We explain that the Berarducci tree of a term M in Λ_{⊥}^{∞} is just its normal form in Λ_{⊥}^{∞}. However nice the properties of Λ_{⊥}^{∞}, it is not expressive enough to prove that observational equivalence implies Berarducci tree equality. Therefore we introduce in Section 3 the infinitary extension Λ_{⊥OA}^{∞}. It is more expressive than Λ_{⊥}^{∞}, but inherits some of its nice properties. In Section 4 we show for terms in Λ_{⊥OA}^{∞} that Berarducci tree equality implies observational equivalence, and in Section 5 we prove the converse. The final Section 6 discusses the result.

2 Finite and Infinite Lambda Calculus

This section is to fix notations and concepts. We will recall the infinitary extension Λ_{⊥}^{∞} of the finite lambda calculus (Berarducci, 1996), (Kennaway et al., 1997). This is an extension not only with infinite terms but also with an extra symbol ⊥ and a rewrite rule

M ≠ ⊥ and β-rootactive

(⊥)
M → ⊥

where β-rootactivity is defined in Definition 4(ii).

The extension Λ_{⊥}^{∞} has the following important properties:

– the infinitary confluence property holds,

– each term has a unique normal form for the combined β, ⊥ reduction,

– each β-normal form is also a normal form for the new ⊥ rule.

The Berarducci tree of a term M is now the (tree of the) possibly infinite normal form of M for the β-⊥-reduction. In the present paper we will always identify terms with their trees.

2.1 Finite Lambda Calculus

Our starting point is the finite untyped lambda calculus (Barendregt, 1984). The set Λ of finite untyped λ-terms is given by the following inductive grammar:

M ::=_{ind} x | (λxM) | (MM),

where x is a variable from some fixed countable set of variables V. We follow the usual conventions on syntax. Terms and variables will respectively be written with (super- and subscripted) letters M, N and x, y, z. Terms of the form (M_{1}M_{2}) and (λxM) will respectively be called applications and abstractions. A context C[ ] is a term with a hole in it, and C[M] denotes the result of filling the hole by the term M, possibly by capturing some free variables of M. A term of the form (λxM)N is a β-redex.

We will silently take equivalence classes of terms modulo a change of bound variables and follow the variable naming convention (Barendregt, 1984)(2.1.13).

We will use the following abbreviations:

λx_{1} … x_{n}.M =_{def} (λx_{1}(λx_{2} … (λx_{n}M) …))
MN_{1} … N_{n} =_{def} (… (MN_{1}) … N_{n})
I =_{def} λx.x S =_{def} λxyz.(xz)yz K =_{def} λxy.x B =_{def} λxyz.x(yz)
Δ =_{def} λx.xx Δ_{η} =_{def} λx.x(λy.xy) Δ_{M} =_{def} λx.xxM
Ω =_{def} ΔΔ Ω_{M} =_{def} Δ_{M}Δ_{M}
Y =_{def} (λxy.y(xxy))(λxy.y(xxy))

The reduction relation →_{β} on Λ is the smallest binary relation that is closed under contexts^{5} and contains the rule:

(λxM)N → M[N/x] (β)

and →_{β}^{∗} is its reflexive and transitive closure.

The structure of a λ-term can be described with help of the notions of β-zero, β-rootstable and β-rootactive term.

Definition 2 (Berarducci, 1996) Let M be a λ-term in Λ. If M cannot βreduce to an abstraction, then M is called a β-zero term.

5 A relation →_{ρ} is closed under contexts if M →_{ρ} N implies C[M] →_{ρ} C[N] for all contexts C[ ].

[figure: @; @; λx; @; λx; x; x; \begin{matrix}λy_{0} \\ λy_{1} \\ λy_{2} \end{matrix}; @; @; @; @; @; @; @]

Fig. 1. Tree representation of the infinite β-normal forms of Ω_{I}, YK and YY.

It is easy to verify that:

Lemma 3 (Berarducci, 1996),(Kennaway et al., 1997) A λ-term β-reduces either to a variable, to an abstraction, to an application of the form MN where M is a β-zero term, or to a β-redex.

Definition 4 (Kennaway et al., 1997) Let M be a λ-term.

(i) If M cannot β-reduce to a β-redex, then M is called β-rootstable or a β-rootstable form.

(ii) If for all N such that M can β-reduce to N, the term N can further be β-reduced to a β-redex, then M is called β-rootactive.

For example, Ω is a β-zero term and it is β-rootactive. The term III is an example of a term which is neither β-rootactive nor β-rootstable, because it can β-reduce to the β-rootstable term I.

Note that:

Lemma 5 (Kennaway et al., 1997) A term can not β-reduce to a β-rootstable form if and only if it is β-rootactive.

A λ-term has a β-normal form if it can β-reduce to a term that does not contain β-redexes anymore. Of course not all finite terms have a finite βnormal form. Some of these terms however seem to converge to an infinite βnormal form well beyond the scope of the finite lambda calculus. For example:

Ω_{I} →_{β} Ω_{I}I →_{β} Ω_{I}II →_{β} Ω_{I}III →_{β} …

YK →_{β}^{∗} K(YK) →_{β} λy_{0}.YK →_{β}^{∗} λy_{0}y_{1}.YK →_{β}^{∗} …

YY →_{β}^{∗} Y(YY) →_{β}^{∗} YY(YY) →_{β}^{∗} YY(YY)(YY(YY)) →_{β}^{∗} …

The infinite β-normal forms of these reductions can more clearly be repre-

[figure: λy; λz; @; @; @; y; z; @; @; y; z]

Fig. 2. Tree representation of the infinite β-normal forms of BYS and BY.

sented as planar trees instead of linear formulas, see Figure 1.^{6}

For another example, one can calculate that BYS and BY β-reduce to the same infinite β-normal form λyz.yz(yz(yz(…))) (see Figure 2). This shows that infinite reductions are an alternative to adding Scott’s induction to the lambda calculus (Scott, 1975).^{7}

2.2 Infinite Lambda Calculus

We will now recall the infinitary extension Λ_{⊥}^{∞} (Kennaway et al., 1997). It provides the proper context to introduce infinite λ-terms and converging reductions formally.

We first define the set Λ_{⊥} of λ-terms extended with a constant ⊥.

Definition 6 The set Λ_{⊥} of partial terms is defined by the inductive grammar:

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

We give a coinductive definition of the set Λ_{⊥}^{∞} of infinite λ-terms which is equivalent to the one given in (Kennaway et al., 1997) and (Kennaway et al., 1999) as a metric completion.

6 The one-one correspondence between terms and trees is given in Definition 13. 7 Barendregt reformulated Scott’s remark as an open problem: Show that the equation BYS = BY cannot be proved in lambda calculus without induction. These terms are proved to be equal in (Kennaway et al., 1997) without using induction, provided one replaces the finite zig and zags in the definition of β-conversion by strongly converging β-reductions. Scott’s induction is then implicit in the definition of equality on the completion.

Definition 7 The set of terms of the infinitary extension Λ_{⊥}^{∞} of the pure lambda calculus is defined by the coinductive grammar^{8} :

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

Notice that the grammar of Λ_{⊥} differs from that of Λ_{⊥}^{∞} only for being inductive instead of coinductive.

We need an explicit definition of distance between two λ-terms in order to characterize Λ_{⊥}^{∞} as a metric completion, as it is defined in (Kennaway et al., 1997) (Kennaway et al., 1999), and to introduce the notion of converging reduction sequence.

Definition 8 (i) Occurrences are finite words over the set {0, 1, 2}. Let ⟨ ⟩

denote the empty word. (ii) The subterm M|_{u} of a term M ∈ Λ_{⊥}^{∞} at occurrence u is partially defined

by induction on the length of u as usual:

(a) M|⟨ ⟩ =_{def} M,

(b) (λxM_{0})|_{0u} =_{def} M_{0}|_{u},

(c) (M_{1}M_{2})|_{1u} =_{def} M_{1}|_{u},

(d) (M_{1}M_{2})|_{2u} =_{def} M_{2}|_{u}.

Note that the term M|_{u} may not exist. If it exists, then u is an occurrence of M.

(iii) The depth of a subterm N at occurrence u of M ∈ Λ_{⊥}^{∞} is the length of

the occurrence u. (iv) The distance d(M, N) of two terms M, N ∈ Λ_{⊥}^{∞} is 0 if M and N are

identical and it is 2^{−k} if k is the length of the shortest occurrence u such that M|_{u} and N|_{u} exist and differ.

With this distance Λ_{⊥}^{∞} becomes a metric space: it is easy to verify that Λ_{⊥}^{∞} is the metric completion of the set Λ_{⊥}.

We skip the details of extending substitution to infinite terms and refer to Definition 2 of (Kennaway et al., 1997).

We extend some concepts related to β-reduction from Λ to Λ_{⊥}^{∞}.

Definition 9 (i) The reduction relation →_{β} on Λ_{⊥}^{∞} is the smallest binary relation that is closed under contexts and contains the rule:

(λxM)N → M[N/x] (β)

8 In fact Λ_{⊥}^{∞} is the final coalgebra of the polynomial endofunctor F : Set ⟶ Set defined by F (X) = 1 + V + V × X + X × X, where V is the set of variables. See (Barr, 1993) for the categorical background.

(ii) If M ∈ Λ_{⊥}^{∞} cannot β-reduce to an abstraction, then M is called a β-zero

term. (iii) A term M ∈ Λ_{⊥}^{∞} is called β-rootstable if M[Ω/⊥] cannot β-reduce to a

β-redex. (iv) A term M ∈ Λ_{⊥}^{∞} is called β-rootactive if for all N ∈ Λ_{⊥}^{∞} such that

M[Ω/⊥] can β-reduce to N, the term N can further be β-reduced to a β-redex.

(v) R_{⊥}^{∞} is the set of β-rootactive terms in Λ_{⊥}^{∞}. (vi) The reduction relation →_{β⊥} on Λ_{⊥}^{∞} is the smallest binary relation that is

closed under contexts and contains the two rules:

(λxM)N → M[N/x] (β) \begin{matrix}M ≠ ⊥ and β-rootactive \\ & (⊥) \\ M → ⊥ \end{matrix}

Note that ⊥ is a β-rootactive term, since ⊥[Ω/⊥] = Ω and Ω is β-rootactive.

Definition 10 (i) An infinite reduction M_{0} →_{β⊥} M_{1} →_{β⊥} M_{2} →_{β⊥} … is Cauchy converging with limit M_{ω} (notation lim_{n→ω} M_{n} = M_{ω}) if ∀ϵ > 0.∃n.∀k ≥ n.d(M_{k}, M_{ω}) < ϵ.

(ii) An infinite reduction M_{0} →_{β⊥} M_{1} →_{β⊥} M_{2} →_{β⊥} … is strongly converging with limit M_{ω} if lim_{n→ω} M_{n} = M_{ω} and lim_{n→ω} d_{n} = ω, that is, ∀n.∃m.∀k ≥ m.d_{k} > n, where d_{k} denotes the depth of the redex at occurrence u in M_{k} reduced in the reduction step M_{k} →_{β⊥} M_{k+1}.

(iii) We say that a term M has a possibly infinite β-⊥-reduction to N (notation M → →_{β⊥} N) if either there is a finite β-⊥-reduction M →_{β⊥}^{∗} N or there is a strong converging β-⊥-reduction starting from M with limit N.

It is well known that without rule ⊥ strongly converging reductions jeopardize the confluence property for β-reduction. Unlike finite reductions, Cauchy converging and even strongly converging β-reductions are not confluent (Berarducci, 1996), (Kennaway et al., 1995), (Kennaway et al., 1997). The finite term Y(λz.K(Kzy)x) can converge in an infinite β-reduction to the infinite term K(K(… x)x) not containing y. It can also converge to the infinite term K(K(… y)y) that does not contain x. Both terms can not be joined; they can only β-reduce to themselves. A simpler example (Berarducci, 1996) is the term (λx.I(xx))(λx.I(xx)) which reduces to both Ω and to I(I …)); also these two terms cannot be joined.

Strongly converging reductions are Cauchy convergent, but not conversely. For example, Ω →_{β} Ω →_{β} … is weakly convergent but not strongly convergent, as the depth of the reduced redexes is always zero.

We recall here the crucial properties of → →_{β⊥} reduction which will be useful in the following and are proved in (Berarducci, 1996), (Kennaway et al., 1997), (Kennaway and de Vries, 2000), and we refer the reader to those papers to know more on this subject. In particular the interested reader will find there that → →_{β⊥} reduction has been defined for sequences of transfinite ordinal length. However these can be compressed into similarly converging reductions of at most ω length with same initial and final terms. The compression lemma of → →_{β⊥} for terms in Λ_{⊥}^{∞} easily generalizes to → →_{β⊥}-reductions of terms in the extensions considered later in this paper.

Theorem 11 (Berarducci, 1996) (Kennaway et al., 1997) (Kennaway and de Vries, 2000)

(i) If a term in Λ_{⊥}^{∞} has a β-rootstable form then such a form can be computed in finitely many steps.

(ii) The reduction → →_{β⊥} is confluent. (iii) Every term in Λ_{⊥}^{∞} has a unique β-⊥-normal form.

2.3 Berarducci Trees as Normal Forms in Λ_{⊥}^{∞}

In this section we give the central definition of this paper, i.e. the definition of Berarducci tree. Since the notion of Berarducci tree will be given as a corecursive function, the codomain of this function has to be given by coinduction. Hence we first define the codomain of this function, i.e. the set of trees.

Definition 12 The set of trees is defined by the coinductive grammar:

T ::=_{coind} ⊥ | x | \begin{matrix}λx \\ T \end{matrix} | [figure: @; T; T] , where x ∈ V.

It is not difficult to show that this notion of tree is a particular case of the notion of Σ-labelled tree defined in (Barendregt, 1984) (Definition 10.1.1) as a partial map from the set of sequence numbers to Σ, where Σ = {x, λx | x ∈ V} ∪ {⊥, @}. In our terminology, a tree is a partial map from the set of occurrences (see Definition 8(i)) to Σ.

Definition 13 gives a natural one-one correspondence between trees and terms of Λ_{⊥}^{∞}. So in the following we will freely identify trees and terms of Λ_{⊥}^{∞}.

Definition 13 The tree T (M) of the term M ∈ Λ_{⊥}^{∞} is defined by corecursion: T (⊥) = ⊥; T (x) = x;

T (λx.N) = \begin{matrix}λx \\ T (N) \end{matrix} ;

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

We can now give the definition of Berarducci tree in a graphically pleasing tree format in the spirit of Barendregt’s definition of Böhm tree (Barendregt, 1984).

Definition 14 (Berarducci, 1996) The Berarducci tree BeT (M) of a term M ∈ Λ_{⊥}^{∞} can be constructed via the following corecursive procedure:

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

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

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

BeT (M) = [figure: @; BeT (M_{1}); BeT (M_{2})];

(iv) otherwise, (exactly when M is β-rootactive) BeT (M) = ⊥.

The infinitary lambda calculus with ⊥-rule Λ_{⊥}^{∞} is an extension of the lambda calculus that has been so designed that in this extension the Berarducci tree of a term is nothing else but its unique (possibly infinite) β-⊥-normal form that can be found by a possibly infinite reduction.

Theorem 15 (Berarducci, 1996)(Kennaway et al., 1997) The Berarducci tree BeT (M) of a term M ∈ Λ_{⊥}^{∞} is the unique β-⊥-normal form N such that M → →_{β⊥} N.

The following result connects Berarducci trees with contexts. It plays a crucial role in this paper:

Theorem 16 (de Vries, 1997) For all terms M and contexts C[ ] in Λ_{⊥}^{∞} it holds that BeT (C[M]) = BeT (C[BeT (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].

2.4 A brief note on Böhm Trees and Lévy-Longo Trees

Böhm Trees (Barendregt, 1984) and Lévy-Longo trees (Lévy, 1976), (Longo, 1983), (de Vries, 1997) can be seen as normal forms in similar extensions as Λ_{⊥}^{∞}. The extensions use the same syntax and β-rule but have both different and more ⊥-rules. In all cases the basic idea is that terms “without computational value” will be replaced by ⊥.

In (Kennaway et al., 1997), (Kennaway et al., 1999) candidate sets of terms with no computational value that lead to calculi with infinite confluence properties have been systematically investigated for lambda calculus. Three such sets resulted: the set of terms without β-head normal form^{9} (Barendregt, 1984), (Wadsworth, 1976), the set of terms without weak β-head normal form^{10} (Abramsky and Ong, 1993) and the set of β-rootactive terms.

The reduction relation →_{Böhm} on Λ_{⊥}^{∞} is the smallest binary relation that is closed under contexts and contains the four rules:

(λxM)N → M[N/x] (β)

M → ⊥, provided M ≠ ⊥ and has no β-head normal form (⊥)

λx.⊥ → ⊥ (⊥_{λ})
⊥M → ⊥ (⊥app)

The normal forms of λ-terms with these rules are better know as Böhm trees.

Definition 17 (Barendregt, 1984) The Böhm tree BöT (M) of a λ-term M can be constructed via the following corecursive procedure:

(i) if M →_{β}^{∗} λx_{1} … x_{n}.yM_{1} … M_{k}, then

BöT (M) = [figure: λx_{1} … x_{n}.y; BöT (M_{1}); …; BöT (M_{k})];

(ii) otherwise, when M has no β-head normal form BöT (M) = ⊥.

The reduction reduction relation →_{LeLo} on Λ_{⊥}^{∞} is the smallest binary relation

9 A λ-term has a β-head normal form when it β-reduces to a term of the form λx_{1} … x_{n}.yM_{1} … M_{k}. 10 A λ-term has a weak β-head normal form when it β-reduces to a term of the form λx.M or yM_{1} … M_{k}.

that is closed under contexts and contains the three rules:

(λxM)N → M[N/x] (β)

M → ⊥, provided M ≠ ⊥ and has no weak β-head normal form (⊥)

⊥M → ⊥ (⊥app)

The normal forms of λ-terms with these rules are better known as Lévy-Longo trees.

Definition 18 (Lévy, 1976), (Longo, 1983) The Lévy-Longo tree LLT (M) of a λ-term M can be constructed via the following corecursive procedure:

(i) if M →_{β}^{∗} xM_{1} … M_{k}, then LLT (M) = [figure: x; LLT (M_{1}); …; LLT (M_{k})];

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

(iii) otherwise, when M has no weak β-head normal form LLT (M) = ⊥.

Comparing the tree formats we find that the Lévy-Longo tree of a term reveals at least the same computational content of a term as its Böhm tree does. The Böhm tree of YK is just ⊥, as YK does not have a head normal form. In contrast, the Lévy-Longo tree of YK is the infinite term in the centre of Figure 1. Lévy-Longo trees don’t include all infinite normal forms of the finite lambda calculus: the Lévy-Longo tree of YY is ⊥ and not the term depicted in Figure 1. Berarducci trees are very nice from a theoretical point of view in that they provide the maximal^{11} “computational” value of a term. From a practical point of view they seem to be less useful than Böhm trees and Lévy-Longo trees, being it undecidable whether a term is a β-zero term or not.

3 The Extended Calculus Λ_{⊥OA}^{∞}

The notion of Berarducci tree gives an equivalence relation: two terms in Λ_{⊥}^{∞} are equivalent if and only if they have the same Berarducci tree (modulo αconversion, as defined in (Kennaway et al., 1997)). A completely different way of comparing terms in Λ_{⊥}^{∞} is observational equivalence (Morris Jr., 1968), in

11 The set of β-rootactive terms is the smallest set of terms in Λ which can be mapped into ⊥, such that the corresponding Λ_{⊥}^{∞} has the unique β-⊥-normal form property (Kennaway et al., 1997).

which we say that M is equivalent to N if:

∀C[ ] ∈ Λ (C[M] is β-rootactive ⇔ C[N] is β-rootactive).

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] are both β-rootactive terms. Berarducci tree equality implies observational equivalence (de Vries, 1997):

Theorem 19 For all M, N ∈ Λ_{⊥}^{∞}, BeT (M) = BeT (N) implies ∀C[ ] ∈ Λ C[M] ∈ R_{⊥}^{∞} ⇔ C[N] ∈ R_{⊥}^{∞}.

PROOF. This can be easily seen with help of Theorem 16 which for any term M and context C[ ] says:

BeT (C[M]) = BeT (C[BeT (M)]).

If M, N are two terms with the same Berarducci tree, then we find that

\begin{aligned}C[M] ∈ R_{⊥}^{∞} & ⇔ BeT (C[M]) = ⊥ ⇔ BeT (C[BeT (M)]) = ⊥ ⇔ \\ & ⇔ BeT (C[BeT (N)]) = ⊥ ⇔ BeT (C[N]) = ⊥ ⇔ C[N] ∈ R_{⊥}^{∞}. \end{aligned}

In a similar way we can prove that Böhm and Lévy-Longo tree equality implies observational equivalence.

The converse of Theorem 19 is not true: observational equivalence does not imply Berarducci tree equivalence. We show two examples of different nature. The first one shows that η-convertible terms cannot be discriminated. Con-

sider the η-convertible terms Δ and Δ_{η} whose Berarducci trees are [figure: λx; @; x; x]

and [figure: λx; @; x; λy; @; x; y]. Since both terms have no free variables, it is enough

to show that for all M ∈ Λ, M[x := Δ] ∈ R_{⊥}^{∞} ⇔ M[x := Δ_{η}] ∈ R_{⊥}^{∞}. This is proved by case analysis. We know that M →_{β}^{∗} N where N is either a variable, an abstraction, an application whose operator is a β-zero term or a β-rootactive term. The interesting case is when N is an application of the form xP_{1} … P_{n}. If P_{1} is a β-zero term then ΔP_{1} … P_{n} →_{β} P_{1}P_{1} … P_{n}, Δ_{η}P_{1} … P_{n} →_{β} P_{1}(λy.P_{1}y) … P_{n}, and both terms are β-rootstable. If P_{1} βreduces to an abstraction then ΔP_{1} … P_{n} and Δ_{η}P_{1} … P_{n} are β-convertible.

The second example shows that even if we consider Berarducci trees modulo ηexpansions, the converse of Theorem 19 is not true. Consider the terms ΩΩ and

ΩΩΩ whose Berarducci trees are [figure: @; ⊥; ⊥] and [figure: @; @; ⊥; ⊥; ⊥]. It is enough

to prove that for all M ∈ Λ, M[x := ΩΩ] ∈ R_{⊥}^{∞} ⇔ M[x := ΩΩΩ] ∈ R_{⊥}^{∞}. The proof proceeds by case analysis similarly to the previous example.

In order to obtain the converse of Theorem 19, we will extend the lambda calculus with two new symbols and four new rules.

3.1 Syntax

Associated with the pure lambda calculus Λ and its extensions Λ_{⊥}, Λ_{⊥}^{∞} we define the extensions Λ_{OA}, Λ_{⊥OA} and Λ_{⊥OA}^{∞} with the constants ⊥, O and A. First we introduce the syntax of these sets and then the reduction rules.

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

V :=_{ind} P | (OV) | (AV) | (λxV) | (V P), where P ∈ Λ is closed

X :=_{ind} M | V, where M ∈ Λ.

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

V :=_{ind} P | (OV) | (AV) | (λxV) | (V P), where P ∈ Λ_{⊥} is closed

X :=_{ind} M | V, where M ∈ Λ_{⊥}.

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

V :=_{ind} P | (OV) | (AV) | (λxV) | (V P), where P ∈ Λ_{⊥}^{∞} is closed

X :=_{ind} M | V, where M ∈ Λ_{⊥}^{∞}.

These extensions with two new constants O and A are rather minimal since the syntax definition implies the following conditions:

– a term can contain only finitely many occurrences of O and A,

– O and A themselves are not terms,

– O and A can only be applied to closed terms and

– O and A can occur in the argument of an application only if the operator is O or A.

For example, λx.O(AI) ∈ Λ_{⊥OA} but I(AI) ∉ Λ_{⊥OA}.

3.2 Rewrite Rules

We introduce now the reduction relations of the various calculi in a concise form. We will use some standard notational conventions. Let Λ′ be some extension of the set Λ.

Definition 21 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}.

In what follows, we need the notions of β-zero, β-rootstable and β-rootactive term given in Definition 9. We now introduce the notion of OA-uniform term that will be used in Definition 24 . The idea behind this notion is that the constants O and A applied to certain terms called OA-uniform will behave like “constant functions”.

Definition 22 Let Λ_{⊥}^{∞} ⊇ Λ′ ⊇ Λ. We say that a term in Λ′ is OA-uniform if it is either an abstraction or a β-rootactive term.

Proposition 23 Let Λ_{⊥}^{∞} ⊇ Λ′ ⊇ Λ and M a closed term in Λ′. Then M →_{β}^{∗} N where N is either a OA-uniform term or a β-rootstable application.

PROOF. A closed term either β-reduces to an abstraction, to a β-rootactive term, or to P Q where P is a closed β-zero term.

Now we introduce the reduction rules for the constants O and A that will allow us to discriminate terms using the Böhm-out technique. If a closed term is a β-rootstable application then the constant O selects the operator of the application and A selects the argument. On the other hand, if the closed term is OA-uniform the constants O and A behave as “constants functions”.

Definition 24 Let Λ′ ⊇ Λ_{OA} and M, N be closed terms of Λ′ that do not contain O or A.

(i) We define the reduction relations →_{OA} on Λ′ as the smallest binary relation that is closed under contexts and contains the following rules:

M is β-zero

(O-selection)

O(MN) → M

M is β-zero

(A-selection)

A(MN) → N

M is OA-uniform

(O-constant)

OM → I M is OA-uniform

(A-constant)

AM → I

(ii) An OA-redex is a term in Λ′ of the form OM or AM where M is any closed term in Λ′ that does not contain O or A.

In (Dezani-Ciancaglini et al., 2000), the constants O and A only performed respectively the selection of the operator and of the argument of an application by rules O-selection and A-selection. By adding the rules O-constant and A-constant, terms having different Berarducci tree in (Dezani-Ciancaglini et al., 2000) are equated by reduction. For example, the terms O(AΩ) and O(OΩ) were different normal forms in (Dezani-Ciancaglini et al., 2000) and now they both OA-reduce to I.

Example 25 Let Λ′ ⊇ Λ_{⊥}. The fact that ⊥ is a closed β-zero term implies 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 closed λ-terms of Λ′ (n ≥ 0).

It is easy to show that the reduction →_{βOA} eliminates all occurrences of the constants O and A.

Lemma 26 Let X ∈ Λ_{⊥OA}^{∞}. Then there is M ∈ Λ_{⊥}^{∞} such that X →_{βOA}^{∗} M.

PROOF. The proof by induction on the definition of Λ_{⊥OA}^{∞} using Proposition 23 is easy.

We generalize the notions of β-zero, β-rootstable and β-rootactive term given in Definition 9. We say that a βOA-redex is either a β-redex or an OA-redex.

Definition 27 Let Λ′ ⊇ Λ_{OA} and ρ be β or βOA.

(i) We say that a term in Λ′ is ρ-zero if it cannot ρ-reduce to an abstraction. (ii) We say that a term X ∈ Λ′ is ρ-rootstable if X[Ω/⊥] cannot ρ-reduce to

a ρ-redex. (iii) We say that a term X ∈ Λ′ is ρ-rootactive if all the reducts of X[Ω/⊥]

can ρ-reduce to ρ-redexes.

Notice that a term is ρ-rootactive if and only if it can not ρ-reduce to a ρ-rootstable term.

A short notation for the set of terms in Λ_{OA}, Λ_{⊥OA}^{∞} which are βOA-rootactive will be handy.

Definition 28 (i) R_{OA} is the set of of terms in Λ_{OA} which are βOA-rootactive. (ii) R_{⊥OA}^{∞} is the set of of terms in Λ_{⊥OA}^{∞} which are βOA-rootactive.

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

Proposition 29 A term X in Λ_{⊥OA}^{∞} is βOA-rootstable if and only if it has one of the following shapes:

– a variable,

– an abstraction,

– an application of the form MN with M a β-zero term.

We can also say that βOA-rootactivity and β-rootactivity coincide in the following sense:

Lemma 30 (i) If X ∈ Λ_{⊥OA}^{∞} is βOA-rootactive then there exists a term

M ∈ Λ_{⊥}^{∞} such that X →_{βOA}^{∗} M and M is β-rootactive. (ii) If X ∈ Λ_{⊥OA}^{∞} is β-rootactive then X ∈ Λ_{⊥}^{∞}.

PROOF.

(i) It follows from Lemma 26. (ii) If X ∉ Λ_{⊥}^{∞} then X = (λx_{1} … x_{n}.Y)M_{1} … M_{k} and either O or A occur in

the head position of Y. Hence either X β-reduces to an abstraction or to an application whose head is O or A. In both cases, X is β-rootstable.

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

Definition 31 Let Λ′ ⊇ Λ_{⊥}. We define the reduction relation →_{⊥} as the smallest binary relation on Λ′ that is closed under contexts and contains the rule:

X ≠ ⊥ and X is β-rootactive

(⊥)
X → ⊥

where X ranges over Λ′.

We will now first consider the combinations (→_{βOA}, Λ_{OA}) and (→_{β⊥OA}, Λ_{⊥OA}), and later (→_{β⊥OA}, Λ_{⊥OA}^{∞}).

3.3 Confluence of Finite Reductions in Λ_{OA} and Λ_{⊥OA}

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

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

PROOF. By induction on the definition of Λ_{⊥OA}.

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

PROOF. Because the O and A symbols are not reduced they can be thought of as fresh free variables. More precisely: X →_{β} Y if and only if X[O/x, A/y] →_{β} Y [O/x, A/y] for all X ∈ Λ_{OA} and X →_{β⊥} Y if and only if X[O/x, A/y] →_{β⊥} Y [O/x, A/y] for all X ∈ Λ_{⊥OA}. Hence part (i) follows from the confluence property for →_{β} in Λ (see (Barendregt, 1984), Theorem 3.28) and part (ii) follows from the confluence property for →_{β⊥} in Λ_{⊥}^{∞} (see (Kennaway et al., 1997), (Kennaway et al., 1999)).

Lemma 34 (i) The relation →_{OA}^{∗} commutes with the relation →_{β}^{∗} in Λ_{OA}:

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

(ii) The relation →_{OA}^{∗} commutes with the relation →_{β⊥}^{∗} in Λ_{⊥OA}:

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

PROOF. We give the proof for →_{β⊥OA}. The proof for →_{βOA} is similar, just drop all references to →_{⊥}. Suppose that C[AM] →_{OA} C[N] and C[AM] →_{β⊥} X. We distinguish four cases depending on the shape of M and whether the →_{β⊥} reduction reduces a subterm in C[ ] or in M.

– A →_{β⊥} reduction step in C[ ] can cause substitutions of variables inside C[ ]. Since M does not contain free variables, it remains unchanged. Hence the resulting term will be of the form C′[AM].

\xymatrix{C[AM] \ar[r]^{β⊥} \ar[d]_{OA} & C′[AM] \ar[d]^{OA} \\ C[N] \ar[r]_{β⊥} & C′[N]}

– If M is OA-uniform, a →_{β⊥} reduction step in M does not affect the redex AM, because OA-uniform terms are closed under →_{β⊥}. This gives us the diagram:

[figure: C[AM]; β⊥; OA; C[AM′]; OA; C[I]; C[I]]

– If M ≡ P N where P is a β-zero term, a →_{β⊥} reduction step in P does not affect the redex A(P N), because β-zero terms are closed under →_{β⊥}. This gives us the diagram:

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

– Finally if M ≡ P N where P is a β-zero term, a →_{β⊥}-reduction step in N commutes trivially:

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

The proof for the cases involving O is similar.

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

PROOF. The Hindley-Rosen Lemma (Barendregt, 1984) states that if we know that two reduction relations →_{1}^{∗} and →_{2}^{∗} both are confluent, and that →_{1}^{∗} commutes with →_{2}^{∗}, then →_{12}^{∗} is confluent. Lemmas 32, 33 and 34 imply these conditions both for →_{β}^{∗} and →_{OA}^{∗}, and for →_{β⊥}^{∗} and →_{OA}^{∗}.

Remark 36 The extended calculus Λ_{OA} and the new reduction rules were chosen carefully in order to get confluent reduction relations. If the O-selection rule could be applied to open β-zero terms, then (λx.O(xI))K would reduce to both K and I. If the O-constant rule could be applied to open β-zero terms, then (λx.O(xI))Ω would reduce to both I and Ω. In both cases, we would loose confluence.

4 Tree Equality implies Observational Equivalence

The goal of this section is to prove along similar lines as for Λ_{⊥}^{∞} (Theorem 19) that Berarducci tree equality in Λ_{⊥OA}^{∞} implies observational equivalence in Λ_{⊥OA}^{∞}.

Our first step is to define → →_{β⊥OA}-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 on the infinitary confluence of Λ_{⊥}^{∞} via a few straightforward lemmas.

Definition 37 The relation → →_{β⊥OA} is defined as (→ →_{β⊥} ∪ →_{OA})^{∗}.

In order to avoid unnecessarily heavy notation we did not define → →_{β⊥OA} as a strongly converging reduction of arbitrary ordinal length, as customary in infinitary lambda calculus (Berarducci, 1996), (Kennaway et al., 1997), (Kennaway and de Vries, 2000). However, the reader may check that there is no loss of generality: any such arbitrary reduction would contain at most finitely many A, O-reduction steps, and the β⊥-reduction sequences in between can be compressed to β⊥-reductions of length at most ω.

4.1 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 38 (i) There is at most one OA-redex in a term belonging to Λ_{⊥OA}^{∞}. (ii) The relation →_{OA}^{∗} commutes with the relation → →_{β⊥}.

PROOF.

(i) By induction on Λ_{⊥OA}^{∞}. (ii) Similar to the finite case considered in Lemma 34. After construction of

the four base cases the proof proceeds now by induction on the ordinal length of → →_{β⊥}. The only interesting case is the limit ordinal ω: we construct

[figure: C[AM]; β⊥; OA; C_{1}[AM_{1}]; OA; β⊥; C_{2}[AM_{2}]; OA; C_{ω}[AM_{ω}]; 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 were not the case, then by the strongly 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 convergence property of the reduction in the top row.

Theorem 39 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 35 using the Hindley-Rosen Lemma, Theorem 11(iii) and Lemma 38. Notice that → →_{β⊥OA} is by definition (→ →_{β⊥} ∪ →_{OA})^{∗}.

We have now the tools to conclude the unique normal form property for Λ_{⊥OA}^{∞} from the unique normal form property for Λ_{⊥}^{∞}.

Corollary 40 For each term in Λ_{⊥OA}^{∞} there is a unique normal form N such that M → →_{β⊥OA} N.

PROOF. Normalization follows from Lemma 26 and normalization of → →_{β⊥} in Λ_{⊥}^{∞} (Theorem 11(iii)). Unicity follows from Theorem 39.

4.2 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 definition of Berarducci tree from terms in Λ_{⊥}^{∞} to terms in Λ_{⊥OA}^{∞}. We will show the correspondence with the unique normal forms. We will conclude with a proof that Berarducci tree equality in Λ_{⊥OA}^{∞} implies observational equivalence in Λ_{⊥OA}^{∞}.

Definition 41 The Berarducci tree BeT : Λ_{⊥OA}^{∞} → Λ_{⊥}^{∞} is defined by corecursion on Λ_{⊥OA}^{∞} as follows:

(i) if X →_{βOA}^{∗} x then BeT (X) = x;

(ii) if X →_{βOA}^{∗} λx.M then BeT (X) = \begin{matrix}λx \\ BeT (M) \end{matrix};

(iii) if X →_{βOA}^{∗} MN and M is a βOA-zero term then

BeT (X) = [figure: @; BeT (M); BeT (N)];

(iv) otherwise (exactly when X is βOA-rootactive), BeT (X) = ⊥.

Note that this definition does not need to consider clauses for O, A because of confluence of →_{βOA} and Lemma 26.

Theorem 42 Let X ∈ Λ_{⊥OA}^{∞}.

(i) BeT (X) is in normal form; (ii) X → →_{β⊥OA} BeT (X); (iii) BeT (X) is the unique normal form of X.

PROOF.

(i) Suppose that BeT (X) is not in normal form. Then a subtree of BeT (X) contains a β-redex of the form BeT (M)BeT (N). But M is a βOA-zero term. A contradiction.

(ii) We consider the strongly convergent reduction sequence obtained by the depth-first outermost strategy ^{12} . The limit of this sequence satisfies the

12 The depth-first outermost strategy reduces at each step the leftmost redex with minimal depth. Notice that this strategy applied to XY, where X is a βOA-zero term and it has an infinite normal form and Y can be reduced, does always reduce

conditions of the definition of BeT (X). By the coinduction principle, this limit is BeT (X).

(iii) It follows from the previous parts and Corollary 40.

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

PROOF. Theorem 42(iii) gives the following diagram:

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

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

Theorem 44 (i) For all X, Y ∈ Λ_{OA}, BeT (X) = BeT (Y) implies

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

(ii) For all X, Y ∈ Λ_{⊥OA}^{∞}, BeT (X) = BeT (Y) implies

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

PROOF. We prove (ii) since (i) is a particular case of (ii). Let X, Y be terms in Λ_{⊥OA}^{∞}. Suppose BeT (X) = BeT (Y). Let C[ ] be a context in Λ_{⊥OA}^{∞}. Using the previous corollary we get:

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

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

Y after a finite number of steps. This is because if n is the minimal depth of redexes in Y, there is always an integer m such that if the depth-first outermost strategy applied to X after m reduction steps gives X′, then the minimal depth of redexes in X′ is greater than n.

Remark 45 Theorem 44 cannot be proved using approximants as for Böhm (Dezani-Ciancaglini et al., 1998b) or Lévy-Longo trees (Boudol and Laneve, 1996). This is because application is not continuous with respect to the Berarducci tree topology (see also (Berarducci and Dezani-Ciancaglini, 1999)). For example, take the context C[ ] = [ ]I and the directed set X = {⊥, λx.⊥}. Clearly, ⊥ = C[⨆ X] ≠ ⨆ C[X] = ⊥I. Application is, a fortiori, not monotonic. E.g. ⊥ ⊏ λx.⊥, but C[⊥] = ⊥I ⊐ ⊥ = C[λx.⊥].

5 Observational Equivalence implies Tree Equality

In this section we will prove that observational equivalence of terms in Λ_{⊥OA}^{∞} with respect to the extended calculi Λ_{OA} implies equality of Berarducci trees. The proof will be a variant of the Böhm out technique (Barendregt, 1984) defined for Böhm trees.

Some terminology first. The label at the root of a tree T is denoted by root(T) and defined by cases:

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

Like in Definition 10.4.6 of (Barendregt, 1984) we will say that an occurrence is useful to discriminate between two Berarducci trees if the labeled nodes in all proper prefixes of the occurrence are identical, while the labeled nodes at the end of the occurrence are different.

Definition 46 An occurrence u is useful for two trees T, T′ if root(T |_{v}) = root(T′|_{v}) for all v < u, but root(T |_{u}) ≠ root(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 47 Let M ∈ Λ_{⊥}^{∞} be a β-zero term and let σ be the substitution σ_{Ω} or σ_{Ω}^{x} for some fixed x. Then the substitution instance M^{σ} is a closed β-zero term.

PROOF. By definition of σ, M^{σ} is a closed term. Suppose towards a contradiction that M^{σ} β-reduces to an abstraction. Then either M β-reduces to an abstraction or to a term of the shape yN_{1} … N_{n} for some variable y. By hypothesis M is a β-zero term and so it cannot β-reduce to an abstraction. Hence M β-reduces to yN_{1} … N_{n}. This implies M^{σ} β-reduces to ΩN_{1}^{σ} … N_{n}^{σ} or to ΩΩN_{1}^{σ} … N_{n}^{σ}, which are both closed β-zero terms.

Theorem 48 (i) For all X, Y ∈ Λ_{OA} it holds that

∀C[ ] ∈ Λ_{OA} C[X] ∈ R_{OA} ⇔ C[Y] ∈ R_{OA} ⇒ BeT (X) = BeT (Y).

(ii) For all X, Y ∈ Λ_{⊥OA}^{∞} it holds that

∀C[ ] ∈ Λ_{⊥OA}^{∞} C[X] ∈ R_{⊥OA}^{∞} ⇔ C[Y] ∈ R_{⊥OA}^{∞} ⇒ BeT (X) = BeT (Y).

PROOF. The proof of (i) and (ii) is essentially the same, since we consider only the Berarducci trees of X and Y which in both cases belong to Λ_{⊥}^{∞}. So we only show (i). The proof will be by contraposition.

Let X, Y be terms in Λ_{OA} such that BeT (X) ≠ BeT (Y). Then there exists an occurrence u that is useful for BeT (X) and BeT (Y). Depending on what label we see at the root of BeT (X)|_{u} and BeT (Y)|_{u}, we define a substitution σ as follows:

– If BeT (X)|_{u} = x and BeT (Y)|_{u} = y, let σ be σ_{Ω}^{x}.

– If BeT (X)|_{u} = x and BeT (Y)|_{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[ ] ∈ Λ_{OA} that can discriminate X and Y with respect to σ in the sense that either C[X^{σ}] ∈ R_{OA} and C[Y^{σ}] ∉ R_{OA}, or vice versa.

Base case: u = ⟨⟩.

– If BeT (X) or BeT (Y) is a leaf, then we choose C[ ] = [ ] as context to discriminate X and Y with respect to σ. We have four sub-cases: · if BeT (X) = x and BeT (Y) = y then X^{σ} →_{βOA}^{∗} ΩΩ and Y^{σ} →_{βOA}^{∗} Ω; · if BeT (X) = x and BeT (Y) = ⊥ (or vice versa) then X^{σ} →_{βOA}^{∗} ΩΩ ∉ R_{OA} and Y^{σ} ∈ R_{OA} (or vice versa); · if BeT (X) is not a leaf and BeT (Y) = x (or vice versa) then X^{σ} ∉ R_{OA} and Y^{σ} →_{βOA}^{∗} Ω ∈ R_{OA} (or vice versa); · if BeT (X) is not a leaf and BeT (Y) = ⊥ (or vice versa) then X^{σ} ∉ R_{OA} and Y^{σ} ∈ R_{OA} (or vice versa).

– If BeT (X) = [figure: @; BeT (M_{1}); BeT (M_{2})] ^{13} with X →_{βOA}^{∗} M_{1}M_{2}

and BeT (Y) = \begin{matrix}λx \\ BeT (N_{1}) \end{matrix} with X →_{βOA}^{∗} λx.N_{1} (or vice versa),

then we choose C[ ] = O[ ]Ω. By the shape of BeT (X) it follows that M_{1} is a β-zero term. Hence M_{1}^{σ} is a closed β-zero term by Lemma 47. ¿From this fact and because C[X^{σ}] →_{βOA}^{∗} O(M_{1}^{σ}M_{2}^{σ})Ω →_{OA} M_{1}^{σ}Ω, we find that is C[X^{σ}] is βOA-rootstable. On the other hand we find that C[Y^{σ}] is βOA-rootactive, because C[Y^{σ}] →_{βOA}^{∗} O(λx.N_{1})^{σ}Ω →_{OA} IΩ →_{β} Ω.

Induction step: u = i · v.

– Suppose BeT (X) = [figure: @; BeT (M_{1}); BeT (M_{2})]with X →_{βOA}^{∗} M_{1}M_{2}

and BeT (Y) = [figure: @; BeT (N_{1}); BeT (N_{2})] with Y →_{βOA}^{∗} N_{1}N_{2}.

We have two sub-cases: · 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 closed β-zero term. Now clearly C[X^{σ}] →_{βOA}^{∗} C′[O(M_{1}^{σ}M_{2}^{σ})] →_{OA} C′[M_{1}^{σ}] and similarly C[Y^{σ}] →_{βOA}^{∗} C′[O(N_{1}^{σ}N_{2}^{σ})] →_{OA} C′[N_{1}^{σ}]. Hence by induction C[ ] discriminates X and Y 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 X and Y with respect to σ. The proof proceeds as before. Again M_{1} is a β-zero term, and M_{1}^{σ} is a closed β-zero term. So we can calculate that C[X^{σ}] →_{βOA}^{∗} C′[A(M_{1}^{σ}M_{2}^{σ})] →_{OA} C′[M_{2}^{σ}] and similarly we see that C[Y^{σ}] →_{βOA}^{∗} C′[A(N_{1}^{σ}N_{2}^{σ})] →_{OA} C′[N_{2}^{σ}]. Hence by induction C[ ] discriminates X and Y with respect to σ.

– Suppose BeT (X) = \begin{matrix}λx \\ BeT (M_{1}) \end{matrix} with X →_{βOA}^{∗} λx.M_{1}

13 Notice that BeT (X) = [figure: @; BeT (M_{1}); BeT (M_{2})] does not imply X →_{βOA}^{∗}

M_{1}M_{2}, since, for example, BeT (I(ΩΩ)) = [figure: @; BeT (IΩ); BeT (IΩ)] = [figure: @; ⊥; ⊥].

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

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

and BeT (Y) = \begin{matrix}λx \\ BeT (N_{1}) \end{matrix} with Y →_{βOA}^{∗} λx.N_{1}.

Then i = 0. 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[X^{σ}] →_{βOA}^{∗} C′[(λx.M_{1})^{σ}σ(x)] →_{β} C′[M_{1}^{σ}] and similarly we see that C[Y^{σ}] →_{βOA}^{∗} C′[(λx.N_{1})^{σ}σ(x)] →_{β} C′[N_{1}^{σ}]. Hence, by induction, C[ ] discriminates X and Y with respect to σ.

Recapitulating, given the two terms X, Y in Λ_{OA} and an occurrence u that is useful to discriminate their Berarducci trees, we have constructed a context C′[ ] together with a substitution σ able to discriminate X and Y. To finish off the proof we will now build a context from these two ingredients that can discriminate X and Y:

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

where x_{1}, … x_{n} is the set of free variables in X and Y.

Since (λx_{1}...x_{n}.X)σ(x_{1}) … σ(x_{n}) and (λx_{1}...x_{n}.Y)σ(x_{1}) … σ(x_{n}) are closed, we note that C[X] and C[Y] belong to Λ_{OA}. Now, because

C[X] = C′[(λx_{1}...x_{n}.X)σ(x_{1}) … σ(x_{n})] →_{βOA}^{∗} C′[X^{σ}]

and similarly C[Y] →_{βOA}^{∗} C′[Y^{σ}] and by construction C′[ ] discriminates X, Y with respect to σ, we get that C[X] is βOA-rootactive and C[Y] is not, or vice versa.

Example 49 The Berarducci trees of some terms considered in this example are shown in Figure 3.

(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[ ] = A((λxy.[ ])(ΩΩ)Ω)

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

obtain is 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[ ] = A(A(A(O((λxy.[ ])(ΩΩ)Ω)))).

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 (Barendregt, 1984)) and in (Sangiorgi, 1994), (Dezani-Ciancaglini et al., 1999), (Dezani-Ciancaglini et al., 1998b) by allowing a non-deterministic choice operator. In all these cases the trick 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 ΩΩ.

By Theorems 48 and 44, Berarducci tree equality of terms (possibly non-pure and/or infinite) coincides with observational equivalence. So the Berarducci trees build a fully abstract model of the (infinitary) lambda calculus extended with the constants O and A.

6 Conclusions

In (Sangiorgi, 1994) Sangiorgi proves that by 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 O, A are not well-formed according to the Groote-Vaandrager format allowed in (Sangiorgi, 1994). The reason is that this format does not allow a premise asking for a term to be a closed β-zero term. In this respect our development completely agrees with that of Sangiorgi.

Looking back at the present work and the related papers (Dezani-Ciancaglini et al., 1998b) and (Dezani-Ciancaglini et al., 1999) that define extensions of pure lambda calculus that can internally discriminate as respectively Böhm trees and Lévy-Longo trees do, then one can wonder to what extent the chosen discriminating extensions actually depend on the nature of the problems dealt with. For instance it is not clear whether there are extensions of lambda calculus completely different from the present one and which internally discriminate as Berarducci trees do: we are tempted to conjecture that the extension with O, A is minimal in the sense that any other extension with the same discriminatory power contains translations of O, A and their rewrite rules.

Acknowledgement

We thank Vincent van Oostrom for discussions. Moreover we are grateful to the referees for their useful remarks and suggestions.

References

Abramsky, S., Ong, C.-H. L., 1993. Full abstraction in the lazy lambda calcu-

lus. Inform. and Comput. 105 (2), 159–267. Barendregt, H. P., 1984. The Lambda Calculus Its Syntax and Semantics,

Revised Edition. North-Holland Publishing Co., Amsterdam. Barr, M., 1993. Terminal coalgebras in well-founded set theory. Theoret. Com-

put. Sci. 114 (2), 299–315. Berarducci, A., 1996. Infinite λ-calculus and non-sensible models. In: Logic

and algebra (Pontignano, 1994). Dekker, New York, pp. 339–377. Berarducci, A., Dezani-Ciancaglini, M., 1999. Infinite λ-calculus and types.

Theoret. Comput. Sci. 212 (1-2), 29–75, gentzen (Rome, 1996). Boudol, G., 1994. Lambda-calculi for (strict) parallel functions. Inform. and

Comput. 108 (1), 51–127. Boudol, G., 2000. Note on the semantics of the call-by-name CSP transform.

Theoret. Comput. Sci. 234, 309–321. Boudol, G., Laneve, C., 1996. The discriminating power of multiplicities in

the λ-calculus. Inform. and Comput. 126 (1), 83–102. Dezani-Ciancaglini, M., de’Liguoro, U., Piperno, A., 1998a. A filter model for

concurrent λ-calculus. SIAM J. Comput. 27 (5), 1376–1419 (electronic). Dezani-Ciancaglini, M., Intrigila, B., Venturini-Zilli, M., 1998b. Böhm’s theo-

rem for Böhm trees. In: ICTCS’98 (Prato, 1998). World Scientific, Oxford, pp. 1–23.

Dezani-Ciancaglini, M., Severi, P., de Vries, F.-J., 2000. Böhm theorem for Berarducci trees. In: CATS’00 (Canberra, 2000). Vol. 31(1) of Electronic Notes in Theoretical Computer Science. Elsevier, pp. 143–166.

Dezani-Ciancaglini, M., Tiuryn, J., Urzyczyn, P., 1999. Discrimination by par-

allel observers: the algorithm. Inform. and Comput. 150 (2), 153–186. Hyland, M., 1975/76. A syntactic characterization of the equality in some

models for the lambda calculus. J. London Math. Soc. (2) 12 (3), 361–370. Kennaway, R., de Vries, F.-J., 2000. Infinitary rewriting, to appear as chap-

ter in a book on term rewriting edited by J. W. Klop. Draft available at: http://www.mcs.le.ac.uk/˜ ferjan/Distribution/draft.ps.gz.

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

Kennaway, R., Klop, J. W., Sleep, R., de Vries, F.-J., 1997. Infinitary lambda

calculus. Theoret. Comput. Sci. 175 (1), 93–125. Kennaway, R., van Oostrom, V., de Vries, F.-J., 1999. Meaningless terms in

rewriting. J. Funct. Logic Programming Article 1, 35 pp, article available at: http://danae.uni-muenster.de/lehre/kuchen/JFLP/articles/1999/A99-01/A99-01.html.

Lévy, J.-J., 1976. An algebraic interpretation of the λβK-calculus, and an

application of a labelled λ-calculus. Theoret. Comput. Sci. 2 (1), 97–114. Longo, G., 1983. Set-theoretical models of λ-calculus: theories, expansions,

isomorphisms. Ann. Pure Appl. Logic 24 (2), 153–188. Milner, R., 1977. Fully abstract models of typed λ-calculi. Theoret. Comput.

Sci. 4, 1–22. Morris Jr., J. H., 1968. Lambda calculus models of programming languages.

Ph.D. thesis, M.I.T. Plotkin, G., 1977. LCF considered as a programming language. Theoret. Com-

put. Sci. 5, 223–256. Sangiorgi, D., 1994. The lazy lambda calculus in a concurrency scenario. In-

form. and Comput. 111 (1), 120–153. Scott, D., 1975. Open problem. In: Lambda Calculus and Computer Science

Theory. Vol. 37 of Lecture Notes in Computer Science. Springer, Berlin, p. 369.

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

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