# New Results on Morris's Observational Theory

Flavien Breuvart, Giulio Manzonetto, Andrew Polonsky, Domenico Ruoppolo

► To cite this version:

Flavien Breuvart, Giulio Manzonetto, Andrew Polonsky, Domenico Ruoppolo. New Results on Morris's Observational Theory: the benefits of separating the inseparable. Leibniz International Proceedings in Informatics, 2016, 1st International Conference on Formal Structures for Computation and Deduction, pp.560. 10.4230/LIPIcs.FSCD.2016.70 . hal-01337192

HAL Id: hal-01337192

https://inria.hal.science/hal-01337192

Submitted on 24 Jun 2016

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_1.png" /></figure>

Distributed under a Creative Commons Attribution 4.0 International License
# New Results on Morris's Observational Theory: the benefits of separating the inseparable

Flavien Breuvart¹, Giulio Manzonetto², Andrew Polonsky³, and Domenico Ruoppolo²

1 Inria Sophia Antipolis
flavien.breuvart@inria.fr

2 Université Paris 13, Laboratoire LIPN, CNRS UMR 7030, France
{giulio.manzonetto,domenico.ruoppolo}@lipn.univ-paris13.fr

3 Université Paris Diderot, Laboratoire IRIF, CNRS UMR 8243, France
andrew.polonsky@gmail.com

## Abstract

Working in the untyped lambda calculus, we study Morris's λ-theory $\mathcal{H}^+$. Introduced in 1968, this is the original extensional theory of contextual equivalence. On the syntactic side, we show that this λ-theory validates the $\omega$-rule, thus settling a long-standing open problem. On the semantic side, we provide sufficient and necessary conditions for relational graph models to be fully abstract for $\mathcal{H}^+$. We show that a relational graph model captures Morris's observational preorder exactly when it is extensional and λ-König. Intuitively, a model is λ-König when every λ-definable tree has an infinite path which is witnessed by some element of the model.

Both results follows from a weak separability property enjoyed by terms differing only because of some infinite $\eta$-expansion, which is proved through a refined version of the Böhm-out technique.

**1998 ACM Subject Classification** F.4.1 Mathematical Logic

**Keywords and phrases** Lambda calculus, relational models, fully abstract, Böhm-out, $\omega$-rule.

**Digital Object Identifier** 10.4230/LIPIcs.FSCD.2016.70

## Introduction

The problem of determining when two programs are equivalent is crucial in computer science: for instance, it allows to verify that the optimizations performed by a compiler preserve the meaning of the input program. For λ-calculi, it has become standard to regard two λ-terms $M$ and $N$ as equivalent when they are contextually equivalent with respect to some fixed set $\mathcal{O}$ of observables. This means that one can plug either $M$ or $N$ into any context $C[\neg]$ without noticing any difference in the global behaviour: $C[M]$ reduces to an observable in $\mathcal{O}$ exactly when $C[N]$ does. The underlying intuition is that the terms in $\mathcal{O}$ represent sufficient stable amounts of information coming out of the computation. The problem of working with this definition, is that the quantification over all possible contexts is difficult to handle. Therefore, various researchers undertook a quest for characterizing observational equivalences both semantically, by defining fully abstract denotational models, and syntactically, by comparing (possibly infinite) trees representing the programs executions.

The observational equivalence obtained by considering the λ-terms in head normal form as observables is by far the most famous and well studied since it enjoys many interesting properties. By definition, it corresponds to the λ-theory $\mathcal{H}^*$ which is the greatest sensible consistent λ-theory. As shown in [1, Thm. 16.2.7], two λ-terms are equivalent in $\mathcal{H}^*$ exactly when their Böhm trees are equal up to denumerable many $\eta$-expansions of (possibly) infinite

<figure><img src="image_2.png" /></figure>

© Flavien Breuvart, Giulio Manzonetto, Andrew Polonsky, Domenico Ruoppolo;
licensed under Creative Commons License CC-BY

1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016).

<figure><img src="image_3.png" /></figure>

Leibniz International Proceedings in Informatics

LIPICS Schloss Dagstuhl - Leibniz-Zentrum für Informatik, Dagstuhl Publishing, Germany
depth. These kinds of characterizations based on infinite trees have been recently rewritten using the modern approach of infinitary rewriting, thus initiating an interesting line of research [25]. From a semantic perspective, it is well known that $\mathcal{H}^*$ is the theory induced by Scott's model $\mathcal{D}_\infty$, a result first reported in [14, 26]. In other words, the model $\mathcal{D}_\infty$ is fully abstract for $\mathcal{H}^*$. Until recently, researchers were only able to introduce individual models of $\mathcal{H}^*$ [11], or at best to provide sufficient conditions for models living in some class to be fully abstract [18]. A substantial advance was made by Breuvart in [4] where he proposed the notion of *hyperimmune* model of $\lambda$-calculus, and showed that a continuous $K$-model is fully abstract for $\mathcal{H}^*$ iff it is extensional and hyperimmune, thus providing a characterization.

In the present paper we study Morris's observational equivalence generated by considering the $\beta$-normal forms as observables [21], and we denote by $\mathcal{H}^+$ the corresponding $\lambda$-theory. (This $\lambda$-theory is denoted by $\mathcal{T}_{\text{NF}}$ in Barendregt's book [1].) The $\lambda$-theory $\mathcal{H}^+$ is extensional and sensible; therefore, as $\mathcal{H}^*$ is maximal, we have $\mathcal{H}^+ \subseteq \mathcal{H}^*$. Even if it has been less ubiquitously studied in the literature, also the equality in $\mathcal{H}^+$ has been characterized both syntactically, in terms of trees, and semantically. Indeed, two $\lambda$-terms are equivalent in $\mathcal{H}^+$ if and only if their Böhm trees are equal up to denumerable many $\eta$-expansions of finite depth [13], and this holds exactly when they have the same interpretation in Coppo, Dezani and Zacchi's filter model [6]. More recently, Manzonetto and Ruoppolo defined a class of relational graph models (rgms, for short), and proved that every extensional rgm preserving the polarities of the empty multiset (in a technical sense) is fully abstract for $\mathcal{H}^+$.

Inspired by the work done in [4], we are going to strengthen this result and provide sufficient and necessary conditions on rgms to induce $\mathcal{H}^+$ as $\lambda$-theory. Now, as all extensional rgms equate at least as $\mathcal{H}^+$, the difficult part is to find a condition guaranteeing that they do not equate more. In other words, we need to analyze in detail the equations in $\mathcal{H}^* \setminus \mathcal{H}^+$. We show that if two $\lambda$-terms $M, N$ are equal in $\mathcal{H}^*$, but not in $\mathcal{H}^+$, then their Böhm trees are similar but there exists a position $\sigma$ where they differ because of an infinite $\eta$-expansion of a variable $x$, that follows the structure of some computable infinite tree $T$. Thanks to a refined (almost chirurgical) Böhm-out technique, we prove that it is always possible to extract such a difference by defining a suitable context $C[-]$. To ensure that this difference is still detectable in an rgm, we introduce the notion of $\lambda$-König model: intuitively, an rgm is $\lambda$-König when every computable infinite tree $T$ has an infinite path (which always exists by König's lemma) witnessed by some element of the model. In our main result (Theorem 36) we prove that an rgm $\mathcal{D}$ is fully abstract for $\mathcal{H}^+$ iff it is extensional and $\lambda$-König, thus providing a complete characterization. From our syntactic weak separation theorem it also follows that $\mathcal{H}^+$ satisfies the $\omega$-rule, a property of extensionality stronger than the $\eta$-rule. Hence, our Theorem 40 answers positively this longstanding open problem, and brings us closer to the solution of Sallé's conjecture $B\omega \subseteq \mathcal{H}^+$ (cf. [1, Thm. 17.4.16]).

# 1 Preliminaries

## Sequences and Trees

We denote by $\mathbb{N}$ the set of natural numbers and by $\mathbb{N}^{<\omega}$ the set of finite sequences over $\mathbb{N}$.
The empty sequence is denoted by $\varepsilon$.

Let $\sigma = (n_1, \dots, n_k)$ and $\tau = (m_1, \dots, m_{k'})$ be two sequences and let $n \in \mathbb{N}$. We write:

- $\ell(\sigma)$ for the length of $\sigma$,

- $\sigma.n$ for the sequence $(n_1, \dots, n_k, n)$,

- $\sigma \star \tau$ for the concatenation of $\sigma$ and $\tau$, that is for the sequence $(n_1, \dots, n_k, m_1, \dots, m_{k'})$.
We say that $\sigma$ is a *subsequence of* $\tau$, denoted $\sigma \subseteq \tau$, when $\tau = \sigma \star \sigma'$ for some $\sigma' \in \mathbb{N}^{<\omega}$.
Given a map $f: \mathbb{N} \to \mathbb{N}$, its *prefix of length* $n$ is the sequence $\langle f|n \rangle := \langle f(0), \dots, f(n-1) \rangle$.

**► Definition 1.** A tree is a partial function $T: \mathbb{N}^{<\omega} \to \mathbb{N}$ such that $\text{dom}(T)$ is closed under prefixes and for all $\sigma \in \text{dom}(T)$ and $n \in \mathbb{N}$ we have $\sigma.n \in \text{dom}(T)$ if and only if $n < T(\sigma)$.

The elements of $\text{dom}(T)$ are called *positions*. For all $\sigma \in \text{dom}(T)$, $T(\sigma)$ gives the number of children of the node in position $\sigma$; therefore $T(\sigma) = 0$ when $\sigma$ corresponds to a leaf.

Let $T$ be a tree. We say that $T$ is: *recursive* if the function $T$ is partial recursive; *finite* if $\text{dom}(T)$ is finite; *infinite* otherwise. We denote by $\mathbb{T}_{\text{rec}}^{\infty}$ the set of all recursive infinite trees.

The *subtree of* $T$ at $\sigma$ is the tree $T|_{\sigma}$ defined by $T|_{\sigma}(\tau) = T(\sigma \star \tau)$ for all $\tau \in \mathbb{N}^{<\omega}$.

A map $f: \mathbb{N} \to \mathbb{N}$ is an *infinite path of* $T$ if $\langle f|n \rangle \in \text{dom}(T)$ for all $n \in \mathbb{N}$.

We denote by $\Pi(T)$ the set of all infinite paths of $T$. By König's lemma, a tree $T$ is infinite if and only if $\Pi(T) \neq \emptyset$.

## The Lambda Calculus

We generally use the notation of Barendregt's book [1] for $\lambda$-calculus. The set $\Lambda$ of $\lambda$-terms over an infinite set $\mathbb{V}$ of variables is defined by the following grammar:

$$ \Lambda: M, N ::= x \mid \lambda x.M \mid MN \quad \text{for all } x \in \mathbb{V}. $$

We assume that application associates to the left, while $\lambda$-abstraction to the right. Application has a higher precedence than $\lambda$-abstraction. E.g., $\lambda xyz.xyz := \lambda x.(\lambda y.(\lambda z.((xy)z)))$.

The set $\text{FV}(M)$ of free variables of $M$ and the $\alpha$-conversion are defined as in [1, Ch. 1§2]. A $\lambda$-term $M$ is *closed* whenever $\text{FV}(M) = \emptyset$ and in this case it is also called a *combinator*. The set of all combinators is denoted by $\Lambda^\circ$. Hereafter, we consider $\lambda$-terms up to $\alpha$-conversion and we adopt the variable convention [1, Conv. 2.1.13]. We fix the following combinators:

$$ \begin{align*} \mathbf{I} &::= \lambda x.x & \Delta &::= \lambda x.xx & \mathbf{1}_n &::= \lambda x y_1 \dots y_n x y_1 \dots y_n \\ \mathbf{K} &::= \lambda x y.x & \Omega &::= \Delta \Delta & \mathbf{Y} &::= \lambda f.(\lambda x.f(xx))(\lambda x.f(xx)) \\ \mathbf{S}^+ &::= \lambda n f s.n f(fs) & c_n &::= \lambda f z.f^n(z) & \mathbf{J} &::= \mathbf{Y}(\lambda z x y.x(zy)) \end{align*} $$

where $f^n(z) := f(\cdots f(f(z))\cdots)$. We will simply denote by $\mathbf{1}$ the combinator $\mathbf{1}_1 := \lambda x y.x$.

Given two $\lambda$-terms $M, N$ we denote by $M\{N/x\}$ the capture-free simultaneous substitution of $N$ for all free occurrences of $x$ in $M$. The $\beta$- and $\eta$- reductions are defined by:

$$ (\beta) \quad (\lambda x.M)N \to_{\beta} M\{N/x\} \qquad (\eta) \quad \lambda x.Mx \to_{\eta} M \text{ provided } x \notin \text{FV}(M). $$

Given a reduction $\to_{\mathbb{R}}$, we write $\to_{\mathbb{R}}$ for its transitive-reflexive closure, we denote by $\text{nf}_{\mathbb{R}}(M)$ the $\mathbb{R}$-normal form of $M$ (if it exists) and by $\text{NF}_{\mathbb{R}}$ the set of all $\mathbb{R}$-normal forms. We denote by $\to_{\mathbb{R}}$ the corresponding $\mathbb{R}$-conversion.

A context $C[-]$ is a $\lambda$-term with a *hole* denoted by $[-]$. Given a context $C[-]$, we write $C[M]$ for the $\lambda$-term obtained from $C$ by substituting $M$ for the hole possibly with capture of free variables in $M$. A context $C[-]$ is called: a *head context* if it has the shape $(\lambda x_1 \dots x_k[-])M_1 \dots M_n$ for $k, n \ge 0$; a *applicative* if it is of the form $[-]M_1 \dots M_n$ for $n \ge 0$. A head (resp. applicative) context $C[-]$ is *closed* when all the $M_i$'s are closed $\lambda$-terms.

**► Definition 2.** A $\lambda$-term $M$ is *solvable* when there is a (head) context $C[-]$ such that $C[M] \to_{\beta} \mathbf{I}$. Otherwise $M$ is called *unsolvable*.

Wadsworth proved in [26] that a $\lambda$-term $M$ is solvable if and only if $M$ has a *head normal form* (hnf), which means that $M \to_{\beta} \lambda x_1 \dots x_n.y N_1 \dots N_k$ (for some $n, k \ge 0$).

The *principal head normal form* of a $\lambda$-term $M$, denoted $\text{phnf}(M)$, is the head normal form obtained from $M$ by *head reduction* [1, Def. 8.3.10].
<figure><img src="image_4.png" /><figcaption>Figure 1 Some examples of Böhm trees. We refer to [1, Lemma 16.4.4] for the definition of P, Q.</figcaption></figure>

## Böhm trees

The *Böhm tree* $\mathrm{BT}(M)$ of a $\lambda$-term $M$ is defined coinductively: if $M$ is unsolvable then $\mathrm{BT}(M) = \perp$; if $M$ is solvable and $\mathrm{phnf}(M) = \lambda x_1 \dots x_n y N_1 \dots N_k$ then:

$$ \mathrm{BT}(M) = \lambda x_1 \dots x_n y \quad \overbrace{\mathrm{BT}(N_1) \dots \mathrm{BT}(N_k)} $$

More generally, we say that $T$ is a *Böhm tree* if there is a $\lambda$-term $M$ such that $\mathrm{BT}(M) = T$. In Figure 1 we provide some examples of Böhm trees. Since every Böhm tree can be seen as a labelled tree over $\mathcal{L} = \{\perp\} \cup \{\lambda\vec{x}.y \mid \vec{x}, y \in \mathbb{V}\}$, we adopt the same notions and notations introduced for trees. However, we will write $\sigma \in \mathrm{BT}(M)$ rather than $\sigma \in \mathrm{dom}(\mathrm{BT}(M))$.

Given two Böhm trees $T, T'$ we set $T \leq_T T'$ if and only if $T$ results from $T'$ by replacing some subtrees with $\perp$. When $T$ is finite, we say that $T$ is a *finite approximant of T*.

The set $\mathrm{NF}_{\perp}$ of *finite approximants* is the set of normal $\lambda$-terms possibly containing $\perp$ inductively defined as follows: $\perp \in \mathrm{NF}_{\perp}$; if $t_i \in \mathrm{NF}_{\perp}$ for $i \in [1..n]$ then $\lambda\vec{x}.yt_1 \dots t_n \in \mathrm{NF}_{\perp}$. The *size* of a finite approximant $t \in \mathrm{NF}_{\perp}$, written $\mathrm{size}(t)$, is defined as usual:

■ $\mathrm{size}(\perp) = 0$ and $\mathrm{size}(\lambda x_1 \dots x_n yt_1 \dots t_k) = \mathrm{size}(t_1) + \dots + \mathrm{size}(t_k) + n + 1$.

The set $\mathrm{BT}^k(M)$ of all finite approximants of $\mathrm{BT}(M)$ of size at most $k$ is defined by

■ $\mathrm{BT}^k(M) = \{t \in \mathrm{NF}_{\perp} \mid \mathrm{size}(t) \leq k, t \leq \perp \mathrm{BT}(M)\}$.

The set $\mathrm{BT}^*(M) = \bigcup_{k \in \mathbb{N}} \mathrm{BT}^k(M)$ is therefore the set of all finite approximants of $\mathrm{BT}(M)$.

## Observational Preorders and Lambda Theories

Observational preorders and $\lambda$-theories become the main object of study when considering the computational equivalence more important than the process of calculus.

A relation on $\Lambda$ is *compatible* if it is compatible with application and $\lambda$-abstraction.

**► Definition 3.** A *preorder theory* is any compatible preorder on $\Lambda$ containing the $\beta$-conversion. A $\lambda$-theory is any compatible equivalence on $\Lambda$ containing the $\beta$-conversion.

Given a $\lambda$-theory (resp. preorder theory) $\mathcal{T}$ we write $M =_{\mathcal{T}} N$ ($M \sqsubseteq_{\mathcal{T}} N$) for $(M, N) \in \mathcal{T}$. The set of all $\lambda$-theories, ordered by inclusion, forms a (quite rich) complete lattice [17].

A $\lambda$-theory $\mathcal{T}$ is called: *consistent* if it does not equate all $\lambda$-terms; *extensional* if it contains the $\eta$-conversion; *sensible* if it equates all unsolvables.

We denote by $\lambda$ the least $\lambda$-theory, by $\lambda\eta$ the least extensional $\lambda$-theory, by $\mathcal{H}$ the least sensible $\lambda$-theory, and by $\mathcal{B}$ the (sensible) $\lambda$-theory equating all $\lambda$-terms having the same Böhm tree. Given a $\lambda$-theory $\mathcal{T}$, we write $\mathcal{T}\eta$ for the least $\lambda$-theory containing $\mathcal{T} \cup \lambda\eta$.
Several interesting λ-theories are obtained via suitable observational preorders defined with respect to a set O of observables. Given O ⊆ Λ, we write $M \in_R O$ if $M \to_R M' \in O$.
Given O ⊆ Λ, the O-observational preorder is given by:

$$M \sqsubseteq^O N \iff \forall C[-] . C[M] \in_β O \text{ entails } C[N] \in_β O.$$

The induced equivalence $M \equiv^O N$ is defined as $M \sqsubseteq^O N$ and $N \sqsubseteq^O M$.

**► Definition 4.** We focus on the following observational preorders and equivalences:

- Hyland's preorder $\sqsubseteq^{\text{hnf}}$ and equivalence $\equiv^{\text{hnf}}$ are obtained by taking as O the set of head normal forms. They are maximal among preorder theories and λ-theories, respectively.

- for Morris's preorder $\sqsubseteq^{\text{nf}}$ and equivalence $\equiv^{\text{nf}}$ we consider as O the set NF$_β$ [21].

We denote by $\mathcal{H}^*$ and $\mathcal{H}^+$ the λ-theories corresponding to $\equiv^{\text{hnf}}$ and $\equiv^{\text{nf}}$, respectively.

## The ω-Rule

The ω-rule is a strong form of extensionality defined as follows:

$$(\omega) \quad \forall P \in \Lambda^o. MP = NP \text{ entails } M = N.$$

We write $(\omega^0)$ for the ω-rule restricted to combinators $M, N \in \Lambda^o$.

Given a λ-theory $\mathcal{T}$ we denote its closure under the ω-rule by $\mathcal{T}\omega$.

We say that $\mathcal{T}$ satisfies the ω-rule, written $\mathcal{T} \vdash \omega$, if $\mathcal{T} = \mathcal{T}\omega$.

By collecting some results in [1, §4.1] we have for all λ-theories $\mathcal{T}$:

- $\mathcal{T}\eta \subseteq \mathcal{T}\omega$,

- $\mathcal{T} \vdash \omega$ if and only if $\mathcal{T} \vdash \omega^0$,

- $\mathcal{T} \subseteq \mathcal{T}'$ entails $\mathcal{T}\omega \subseteq \mathcal{T}'\omega$.

The picture on the right, where $\mathcal{T}$ is above $\mathcal{T}'$ if $\mathcal{T} \subsetneq \mathcal{T}'$, is taken from [1, Thm. 17.4.16] and shows some facts about the λ-theories under consideration. In [1, §17.4], Sallé conjectured that $B\omega \subsetneq \mathcal{H}^+$.

<figure><img src="image_5.png" /></figure>

The counterexample showing that $\lambda\eta \nvdash \omega$ is based on Plotkin's terms [1, Def. 17.3.26]. Since these terms are unsolvable, they become useless when considering sensible λ-theories. The techniques to analyze the ω-rule for sensible λ-theories are discussed in Section 2.2.

# 2 The Lambda Theories $\mathcal{H}^+$ and $\mathcal{H}^*$

In this section we recall the characterizations of $\mathcal{H}^+$ and $\mathcal{H}^*$ in terms of “extensional” Böhm-trees, and we discuss the ω-rule for sensible λ-theories in the interval $[\mathcal{B}, \mathcal{H}^*]$.

## 2.1 Böhm Trees and Their η-Expansions

Morris's theory $\mathcal{H}^+$ and preorder $\sqsubseteq^{\text{nf}}$ correspond to the contextual theories where the observables are the β-normal forms. Notice that it is equivalent to take as observables the βη-normal forms since $M \to_β nf_β(M)$ exactly when $M \to_{\beta\eta} nf_{\beta\eta}(M)$, so $\lambda\eta \subseteq \mathcal{H}^+$.

Moreover, by the Context Lemma for β-normalizable terms [7, Lemma 1.2], the context $C[-]$ separating two combinators $M \sqsupseteq^{\text{nf}} N$ can be chosen applicative and closed.

**► Theorem 5.** [13, Thm. 2.6] Let $M, N \in \Lambda$. Then $M =_{\mathcal{H}^+} N$ if and only if BT$(M)$ and BT$(N)$ are equal up to denumerable many η-expansions of finite depth.

This means that there exists a Böhm tree $T$ such that both BT$(M)$ and BT$(N)$ can be transformed into $T$ by performing a denumerable (possibly finite) number of η-expansions.
<figure><img src="image_6.png" /><figcaption>Figure 2 A situation witnessing the fact that $M \sqsubseteq^{\text{hnf}} N$ holds.</figcaption></figure>

Consider, for instance, the two $\lambda$-terms $P, Q$ whose Böhm trees are depicted in Figure 1, where $\eta^n(x)$ denotes the $\eta$-expansion of $x$ having depth $n$. (Such terms exist by [1, §16.4].) Now, $\text{BT}(P)$ is such that at every level $2n$ the variable $x$ is $\eta$-expanded $n$ times (in depth). We have $P =_{\mathcal{H}^+} Q$ because we can perform infinitely many finite $\eta$-expansions of increasing depth in $\text{BT}(Q)$ and obtain $\text{BT}(P)$ (but in general we may need to $\eta$-expand both trees).

As a brief digression, notice that the existence of such $P, Q$ entails that $B\eta \subseteq \mathcal{H}^+$. Indeed, for $M, N \in \Lambda$, $M \to_{\eta} N$ entails that $\text{BT}(M)$ can be obtained from $\text{BT}(N)$ by performing at most one $\eta$-expansion at every level (see [1, Lemma 16.4.3]). It is easy to show that $P \neq_{B\eta} Q$.

Hyland's theory $\mathcal{H}^*$ and preorder $\sqsubseteq^{\text{hnf}}$ correspond to the contextual theories where the observables are the head normal forms (equivalently, the solvable $\lambda$-terms). It is easy to show that $M \sqsubseteq^{\text{nf}} N$ entails $M \sqsubseteq^{\text{hnf}} N$, so $\mathcal{H}^+ \subseteq \mathcal{H}^*$. Terms $M, N$ such that $M \sqsubseteq^{\text{hnf}} N$ are called *semi-separable* in [1]. Also in this case, the context lemma for solvable terms [26, Lemma 6.1] entails that the semi-separating contexts can be chosen applicative and closed.

The characterization of $\mathcal{H}^*$ in terms of trees, needs the notion of infinite $\eta$-expansion of a Böhm tree. The classical definition is given in terms of tree extensions in [1, Def. 10.2.10].

**Definition 6.** Given two Böhm trees $T$ and $T'$, we say that $T$ is a (possibly) infinite $\eta$-expansion of $T'$, written $T \rightsquigarrow_{\eta} T'$, if $T$ is obtained from $T'$ by performing denumerable many $\eta$-expansions of possibly infinite depth.

We prefer not to use Barendregt's classical notation $T \geq_{\eta} T'$ as it could be confusing. Our notation is borrowed from infinite rewriting since $\rightsquigarrow_{\eta}$ can also be defined in this way [25]. (We refer here to the strongly converging $\eta$-reduction of [25] restricted to Böhm trees.)

**Theorem 7.** [1, Thm. 19.2.9] Let $M, N \in \Lambda$.

$M \sqsubseteq^{\text{hnf}} N$ iff there are Böhm trees $T, T'$ such that $\text{BT}(M) \eta \rightsquigarrow T \leq_{\perp} T' \rightsquigarrow_{\eta} \text{BT}(N)$.

$M =_{\mathcal{H}^*} N$ iff $\text{BT}(M)$ and $\text{BT}(N)$ are equal up to denumerable many (possibly) infinite $\eta$-expansions; this means that there is a Böhm tree $T$ such that $\text{BT}(M) \eta \rightsquigarrow T \rightsquigarrow_{\eta} \text{BT}(N)$.

The typical example is $\mathbf{I} \sqsubseteq^{\text{hnf}} \mathbf{J}$, since clearly $\text{BT}(\mathbf{J}) \rightsquigarrow_{\eta} \mathbf{I}$ (on the contrary, $\mathbf{I} \sqsupseteq^{\text{nf}} \mathbf{J}$), but in general to show that $M \sqsubseteq^{\text{hnf}} N$ one may need infinitely $\eta$-expand also $\text{BT}(N)$ and cut some subtree of $\text{BT}(N)$. This is the case for $M = \lambda xy.xx\Omega(\mathbf{J}x)$ and $N = \lambda xy.x(\mathbf{J}x)yx$. We recall from [14, Thm. 5.4(a)] that the relation $\sqsubseteq^{\text{hnf}}$ can be stratified as follows.

**Lemma 8.** For $M, N \in \Lambda$, $M \sqsubseteq_k^{\text{hnf}} N$ iff either $k = 0$, or $M$ is unsolvable, or $k > 0$ and
$$M =_{\beta} \lambda x_1 \dots x_{n_1} \cdot y M_1 \dots M_{m_1} \quad \text{and} \quad N =_{\beta} \lambda x_1 \dots x_{n_2} \cdot y N_1 \dots N_{m_2}$$

where $n_1 - m_1 = n_2 - m_2$ and either $y$ is free or $y = x_j$ for some $j \le \min\{n_1, n_2\}$. So if, say, $m_1 \le m_2$ then $n_1 \le n_2$ and there exists $p \ge 0$ such that $n_2 = n_1 + p$ and $m_2 = m_1 + p$. Moreover $M_i \sqsubseteq_{k-1}^{\text{hnf}} N_i$ for all $i \le m_1$ and $x_{n_1+j} \sqsubseteq_{k-1}^{\text{hnf}} N_{m_1+j}$ for all $j \le p$. (The case $m_1 > m_2$ is symmetrical.) Finally we have $M \sqsubseteq^{\text{hnf}} N$ iff $M \sqsubseteq_k^{\text{hnf}} N$ for all $k \in \mathbb{N}$.
<figure><img src="image_7.png" /><figcaption>Figure 3 The Böhm tree of $\mathbf{J}_T$, an infinite $\eta$-expansion of $\mathbf{I}$ following $T \in \mathbb{T}_{\text{rec}}^{\infty}$. To lighten the notations we write $T\sigma$ rather than $T(\sigma)$ and we let $\tilde{w}_n := w_1, \dots, w_n$.</figcaption></figure>

## The Infinite $\eta$-Expansion $\mathbf{J}_T$.

Note that $\mathbf{J}$ is not the unique infinite $\eta$-expansion of the identity. For each $T \in \mathbb{T}_{\text{rec}}^{\infty}$ there is a $\lambda$-term $\mathbf{J}_T$ which is an infinite $\eta$-expansion of $\mathbf{I}$ following $T$ in the sense of Figure 3.

We could just say that the existence of such a $\mathbf{J}_T$ follows directly from the fact that $T$ is recursive and [1, Thm. 10.1.23]. We prefer to give a more explicit definition.

Let us fix a bijective encoding $\# : \mathbb{N}^* \to \mathbb{N}$ and let $\text{Cons} \in \Lambda^0$ be such that

$$ \text{Cons} \ c_{\#\sigma} \ c_n =_{\beta} c_{\#(\sigma,n)} $$

for all $\sigma \in \mathbb{N}^*$, $n \in \mathbb{N}$. Notice that such a combinator $\text{Cons}$ exists by Church's thesis.

Given $M, N \in \Lambda$ and $x \notin \text{FV}(M)$, we set:

$$ [M, N] := \lambda x.xMN, \quad M \circ N := \lambda x.M(Nx). $$

We associate with every tree $T$ a partial map $f_T : \mathbb{N} \to \mathbb{N}$ such $n \in \text{dom}(f_T)$ iff $n = \#\sigma$ for $\sigma \in \text{dom}(T)$, and in this case $f_T(n) = T(\sigma)$. When $T$ is recursive $f_T$ is clearly $\lambda$-definable.

**Definition 9.** Let $F \in \Lambda^0$ be the term $\lambda$-defining $f_T$. Define (for $X \in \Lambda$ arbitrary):

1. $L^X p := \lambda z.p(\lambda n x y.z(S^+ n)(x(Xny)));$

2. $M^X nx := nL^X[c_0, x](\mathbf{KI});$

3. $N_s := M^{N \circ (\text{Cons} s)}(Fs)$, using the fixed point combinator $\mathbf{Y}$;

4. $\mathbf{J}_T := N c_{\#\varepsilon}$.

**Lemma 10.** $\mathbf{J}_T$ is such that the underlying tree of $\text{BT}(\mathbf{J}_T)$ is $T$ and $\text{BT}(\mathbf{J}_T) \rightsquigarrow_{\eta} \mathbf{I}$.

**Proof sketch.** First one verifies that for all $X \in \Lambda$ and $n \in \mathbb{N}$ the following hold:

1. $(L^X)^n[c_0, x] =_{\beta} \lambda z y_1 \dots y_n . z c_n(x(Xc_0 y_1) \dots (Xc_{n-1} y_n));$

2. $M^X c_n x =_{\beta} \lambda y_1 \dots y_n . x(Xc_0 y_1) \dots (Xc_{n-1} y_n);$

3. $N c_{\#\sigma} x =_{\beta} \lambda y_1 \dots y_n . x(N c_{\#(\sigma,0)} y_1) \dots (N c_{\#(\sigma,(n-1))} y_n)$, where $n = T(\sigma)$;

In particular, $\text{BT}(\mathbf{J}_T)$ is $\perp$-free. From this, and the fact that $\mathbf{I}$ is $\beta\eta$-normal, we have that $\text{BT}(\mathbf{J}_T) \rightsquigarrow_{\eta} \mathbf{I}$ if and only if $\mathbf{J}_T \sqsubseteq_k^{\text{hnf}} \mathbf{I}$ for all $k \in \mathbb{N}$ (by Lemma 8).

We prove by induction on $k - \ell(\sigma)$, that for all $k \in \mathbb{N}$ and $\sigma \in \text{dom}(T)$ such that $\ell(\sigma) < k$, we have $N c_{\#\sigma} x \sqsubseteq_k^{\text{hnf}} x$. If $k - \ell(\sigma) = 0$ or $T(\sigma) = 0$ then it is trivial. Otherwise, it follows from (3) and the induction hypothesis since $\sigma.i \in \text{dom}(T)$ for all $i < T(\sigma)$ and $k - \ell(\sigma.i) < k - \ell(\sigma)$. Finally, we conclude since $\mathbf{J}_T := N c_{\#\varepsilon}$. $\quad$

**Lemma 11.** For all $T \in \mathbb{T}_{\text{rec}}^{\infty}$, we have $\mathbf{J}_T 1_{T(\varepsilon)} =_{\beta} \mathbf{J}_T$.

In Section 3 we consider $M \sqsubseteq_k^{\text{hnf}} N$ for some $M, N$ such that $M$ is $\beta$-normal and $\text{BT}(N)$ is infinite. We show that $M$ and $\text{BT}(N)$ have similar structure, except for the fact that there is a position $\sigma$ in $\text{BT}(N)$ where an infinite $\eta$-expansion following some $T \in \mathbb{T}_{\text{rec}}^{\infty}$ occurs. Moreover, we show that this difference can be extracted via a suitable Böhm-out technique.
## 2.2 The $\omega$-Rule for Sensible Theories

The validity of the $\omega$-rule for $\lambda$-theories $\mathcal{T}$ containing $\mathcal{B}$ can be tricky to prove (or disprove). We have seen that the terms $P, Q$ of Figure 1 are equated in $\mathcal{H}^+$, but different in $\mathcal{B}\eta$. Perhaps surprisingly, they can also be used to prove that $\mathcal{B}\eta \subsetneq \mathcal{B}\omega$ since $P =_{\mathcal{B}\omega} Q$ holds. The following argument is due to Barendregt, see [1, Lemma 16.4.4].

Recall the following basic fact: for every $M \in \Lambda^\circ$, there exists $k \ge 0$ such that $M\Omega \cdots \Omega$, $k$ times, becomes unsolvable (see [1, Lemma 17.4.4]). By inspecting Figure 1, we notice that in $\mathrm{BT}(P)$ the variable $y$ is applied to an increasing number of $\Omega$'s (represented by $\perp$). So, when substituting some $M \in \Lambda^\circ$ for $y$ in $\mathrm{BT}(Py)$, there will be a level $k$ of the tree where $M\Omega \cdots \Omega$ become $\perp$, thus cutting $\mathrm{BT}(PM)$ at level $k$. The same reasoning can be done for $\mathrm{BT}(QM)$. Therefore $\mathrm{BT}(PM)$ and $\mathrm{BT}(QM)$ only differ because of finitely many $\eta$-expansions. Since $\mathcal{B}\eta \subseteq \mathcal{B}\omega$, we conclude that $P =_{\mathcal{B}\omega} Q$.

The fact that $\mathcal{H}^* \vdash \omega$ is clearly a consequence of its maximality. However, there are several direct proofs: see [1, §17.2] for a syntactic demonstration and [26] for a semantic one. The longstanding open question whether $\mathcal{H}^+ \vdash \omega$ will be answered positively in Theorem 40. We believe that the $\lambda$-terms $P$ and $Q$, suitably modified to get rid of the $\Omega$'s in their Böhm trees, are good candidates to show that $\mathcal{B}\omega \subsetneq \mathcal{H}^+$, but the question remains open.

# 3 Böhming-out Infinite $\eta$-Expansions

The Böhm out technique [3, 1, 23] aims to build a context which extracts (an instance of) the subterm of a $\lambda$-term $M$ at position $\sigma$. It is used for separating two $\lambda$-terms $M, N$ provided that their structure is sufficiently different (depending on the notion of separation under consideration). We show that when $M \sqsubseteq^{\mathrm{nf}} N$ this difference can be Böhmed out via an appropriate head context, even when $M$ and $N$ have a similar structure (i.e. $M \sqsubseteq^{\mathrm{hnf}} N$).

## 3.1 Morris Separators

We start by providing a notion of Morris separator, that is a sequence $\sigma$ witnessing the fact that $M \sqsubseteq^{\mathrm{nf}} N$ for $\lambda$-terms $M$ and $N$ such that $M$ is $\beta$-normal and $M \sqsubseteq^{\mathrm{hnf}} N$ holds.

We recall from Section 1 that we use for Böhm trees, the same notions and notations introduced for trees. However, we write $\sigma \in \mathrm{BT}(M)$ to indicate that $\sigma \in \mathrm{dom}(\mathrm{BT}(M))$.

Given $\sigma \in \mathrm{BT}(M)$ we define the subterm $M_\sigma$ of $M$ at $\sigma$ (relative to its Böhm tree) by:

- $M_\epsilon = M,$

- $M_{i.\sigma} = (M_{i+1})_\sigma$ whenever $\mathrm{phnf}(M) = \lambda\vec{x}.yM_1 \cdots M_n$.

**► Definition 12.** We say that $\sigma \in \mathrm{BT}(M) \cap \mathrm{BT}(N)$ is a Morris separator for $M, N$, written $\sigma : M \sqsubseteq^{\mathrm{nf}} N$, if there exists $i > 0$ such that, for some $p \ge i$, we have:

$$M_{\sigma} =_{\beta} \lambda x_1 \dots x_n.y M_1 \dots M_m \quad \text{and} \quad N_{\sigma} =_{\beta} \lambda x_1 \dots x_{n+p}.y N_1 \dots N_{m+p}$$

where $N_{m+i} =_{\mathcal{B}} \mathbf{J}_T x_{n+i}$ for some $T \in \mathbb{T}_{\mathrm{rec}}^{\infty}$.

It is easy to check that $\sigma : M \sqsubseteq^{\mathrm{nf}} N$ and $\sigma = \langle k \rangle \star \tau$ entail $\tau : M_{k+1} \sqsubseteq^{\mathrm{nf}} N_{k+1}$.

Recall that we are considering $\lambda$-terms $M, N$ such that $M$ is $\beta$-normal, $M \sqsubseteq^{\mathrm{nf}} N$, but $M \sqsubseteq^{\mathrm{hnf}} N$. Obviously such $M$ and $N$ are not semi-separable (using the terminology of [1]). Since $M$ is $\beta$-normal, its Böhm tree is finite and $\perp$-free. Since $M \sqsubseteq^{\mathrm{hnf}} N$, by Lemma 8 also $\mathrm{BT}(N)$ is $\perp$-free; moreover, at every position $\sigma \in \mathrm{BT}(M) \cap \mathrm{BT}(N)$, $M_\sigma$ and $N_\sigma$ have similar hnfs (the number of abstractions and applications can be matched via $\eta$-expansions). Note
<figure><img src="image_8.png" /><figcaption>Figure 4 Two terms M, N such that M is β-normal, M ⊑<sup>hnf</sup> N, but M ⊑<sup>nf</sup> N.</figcaption></figure>

that $\mathrm{BT}(M)$ might have $\eta$-expansions that are not present in $\mathrm{BT}(N)$. As $M \not\subseteq^\mathrm{nf} N$, the Böhm tree of $N$ must have infinite subtrees of the form $\mathrm{BT}(\mathbf{J}_T x)$ for some $x \in V, T \in \mathbb{T}^\infty_\mathrm{rec}$.

To explain the idea behind Morris separators, we use the terms **M** and **N** whose Böhm trees are depicted in Figure 4. This example admits two Morris separators: $\varepsilon$ and $\langle 1, 0 \rangle$.

The empty sequence $\varepsilon$ is a separator since $N_{\langle 2 \rangle} =_B \mathbf{J}_{T_2} w$ where $T_2$ is the complete binary tree. The sequence $\langle 1, 0 \rangle$ is a separator because $N_{\langle 1,0,0 \rangle} =_B \mathbf{J}_{T_1} z_1$ where $T_1$ is the complete unary tree (i.e. $\mathbf{J}_{T_1} =_B \mathbf{J}$).

**Proposition 13.** Let $M, N \in \Lambda$ such that $M$ is $\beta$-normal, $N \notin_\beta \mathrm{NF}_\beta$ and $M \subseteq^\mathrm{hnf} N$. Then there exists a position $\sigma \in \mathrm{BT}(M) \cap \mathrm{BT}(N)$ such that $\sigma : M \not\subseteq^\mathrm{nf} N$.

**Proof.** Since $M$ is $\beta$-normal, $N$ does not have a $\beta$-normal form and $M \subseteq^\mathrm{hnf} N$, $\mathrm{BT}(N)$ must be infinite and $\perp$-free. By König's lemma there is $f \in \Pi(\mathrm{BT}(N))$ and since $\mathrm{BT}(M)$ is finite there exists $n > 0$ such that $\sigma := \langle f|n-1 \rangle \in \mathrm{BT}(M) \cap \mathrm{BT}(N)$ but $\langle f|n \rangle \notin \mathrm{BT}(M)$. By applying Lemma 8, there exists $p > 0$ such that $M_\sigma =_\beta \lambda x_1 \dots x_{n_1} \cdot y M_1 \dots M_{n_1}$ and $N_\sigma =_\beta \lambda x_1 \dots x_{n_1+p} \cdot y N_1 \dots N_{m_1+p}$. Moreover, $x_{n_1+j} \subseteq^\mathrm{hnf} N_{m_1+j}$ where $j = f(n) + 1 - m$. Since $\mathrm{BT}(N_{m_1+j})$ is infinite we must have $N_{m_1+j} =_B \mathbf{J}_T x_{n_1+j}$ for some $T \in \mathbb{T}^\infty_\mathrm{rec}$. $\quad$

## 3.2 A Böhm-out Technique for Separating the Inseparable

The following combinators will be used (among others) to build the Böhm-out context:

$$ \mathbf{U}_k^n := \lambda x_1 \dots x_n \cdot x_k \qquad \mathbf{P}_n := \lambda x_1 \dots x_n \cdot \lambda z \cdot z x_1 \dots x_n $$

The combinator $\mathbf{U}_k^n$ is called *projector* and $\mathbf{P}_n$ *tupler* as they enjoy the following properties.

**Lemma 14.** Let $k \ge n \ge 0$ and $X_1, \dots, X_n, Y_1, \dots, Y_{k-n} \in \Lambda^o$.

$$ 1. \ (\mathbf{P}_k X_1 \cdots X_n) Y_1 \cdots Y_{k-n} =_\beta \lambda z \cdot z X_1 \cdots X_n Y_1 \cdots Y_{k-n} $$

$$ 2. \ (\lambda z \cdot z X_1 \cdots X_n) \mathbf{U}_i^n =_\beta X_i $$

When $\mathbf{U}_k^n$ is substituted for $y$ in $\lambda \vec{x} \cdot y M_1 \cdots M_n$, it extracts an instance of $M_k$. Let us consider the $\lambda$-term $N$ whose Böhm tree is given in Figure 4. The context $[-]\mathbf{U}_1^2$ extracts from $N$ the subterm $yx$ where $x$ is replaced by $\mathbf{U}_1^2$. The idea of the Böhm-out technique is to replace every variable along the path $\sigma$ with the correct projector.

The issue is when the same variable occurs several times in $\sigma$ and we must select different children in these occurrences. For example, to extract $N_{\langle 1,0 \rangle}$, the first occurrence of $x$ should be replaced by $\mathbf{U}_2^3$, the second by $\mathbf{U}_1^1 := \mathbf{I}$. The problem was originally solved by Böhm in [3] by first replacing the occurrences of the same variables along the path by different variables using the tupler, and then replacing each variable by the suitable projector. In the example under consideration, the context $[-]\mathbf{P}_3 \Omega \mathbf{U}_2^3 \mathbf{U}_1^1 \Omega \cdot \Omega \mathbf{U}_1^3$ extracts from $N$ the instance of $N_{\langle 1,0 \rangle}$ where $z_0$ is replaced by $\mathbf{I}$.

Obviously, finite $\eta$-differences can be destroyed during the process of Böhming out. In contrast, we show that infinite $\eta$-differences can always be preserved.
**► Lemma 15 (Böhm-out).** Let $M, N \in \Lambda$ such that $M \sqsubseteq^{\text{hnf}} N$, let $\vec{y} = \text{FV}(MN)$ and $\sigma: M \not\sqsubseteq^{\text{hnf}} N$. Then for all $k \in \mathbb{N}$ large enough, there are combinators $\vec{X} \in \Lambda^\sigma$ such that $M\{\mathbf{P}_k/\vec{y}\}\vec{X} =_{\beta} \mathbf{1}_{T(\varepsilon)}$ and $N\{\mathbf{P}_k/\vec{y}\}\vec{X} =_{\mathcal{B}} \mathbf{J}_T$ for some $T \in \mathbb{T}^\infty_{\text{rec}}$.

**Proof.** We proceed by induction on $\sigma$.

**Base case** $\sigma = \varepsilon$. Then there exists $i > 0$ such that, for some $p \ge i$, we have:

$$M =_{\beta} \lambda x_1 \dots x_n \cdot y M_1 \dots M_m \text{ and } N =_{\beta} \lambda x_1 \dots x_{n+p} \cdot y N_1 \dots N_{m+p}$$

where $N_{m+i} =_{\mathcal{B}} \mathbf{J}_T x_{n+i}$. For any $k \ge n+m+p$ let us set $\vec{X} := \mathbf{P}_k^{\sim n} \mathbf{1}_{T(\varepsilon)}^p \Omega^{\sim k-m-p} \mathbf{U}_{m+i}^k$, where $M^{\sim n}$ denotes the sequence of $\lambda$-terms containing $n$ copies of $M$.

We split into cases depending on whether $y$ is free or $y = x_j$ for some $j \le n$. We consider the former case, as the latter is analogous. On the one side we have:

$$ \begin{align*} (\lambda x_1 \dots x_n \cdot y M_1 \dots M_m)\{\mathbf{P}_k/\vec{y}\}\vec{X} &= \\ (\lambda x_1 \dots x_n \cdot \mathbf{P}_k M_1' \dots M_m')\vec{X} &=_{\beta} \text{where } M'_{\ell} := M_{\ell}\{\mathbf{P}_k/\vec{y}\} \\ (\mathbf{P}_k M_1'' \dots M_m'')\mathbf{1}_{T(\varepsilon)}^{\sim p} \Omega^{\sim k-m-p} \mathbf{U}_{m+i}^k &=_{\beta} \text{where } M''_{\ell} := M'_{\ell}\{\mathbf{P}_k/\vec{x}\} \\ (\lambda z \cdot z M_1'' \dots M_m''')\mathbf{1}_{T(\varepsilon)}^{\sim p} \Omega^{\sim k-m-p} \mathbf{U}_{m+i}^k &=_{\beta} \text{by Lemma 14.1 and 14.2.} \end{align*} $$

On the other side, we have:

$$ \begin{align*} (\lambda x_1 \dots x_{n+p} \cdot x_j N_1 \dots N_{m+p})\{\mathbf{P}_k/\vec{y}\}\vec{X} &= \\ (\lambda x_1 \dots x_{n+p} \cdot \mathbf{P}_k N_1' \dots N_{m+p}')\vec{X} &=_{\beta} \text{for } N'_{\ell} := N_{\ell}\{\mathbf{P}_k/\vec{y}\} \\ (\lambda x_{n+1} \dots x_{n+p} \cdot \mathbf{P}_k N_1'' \dots N_{m+p}'')\mathbf{1}_{T(\varepsilon)}^{\sim p} \Omega^{\sim k-m-p} \mathbf{U}_{m+i}^k &= \text{for } N''_{\ell} := N'_{\ell}\{\mathbf{P}_k/x_1, \dots, x_n\} \\ (\mathbf{P}_k N_1''^* \dots N_{m+p}'^*) \Omega^{\sim k-m-p} \mathbf{U}_{m+i}^k &= \text{for } N''_{\ell} := N''_{\ell}\{\mathbf{1}_{T(\varepsilon)}/x_{n+1}, \dots, x_{n+p}\} \\ (\lambda z \cdot z N_1''^* \dots N_{m+p}'^* \Omega^{\sim k-m-p}) \mathbf{U}_{m+i}^k &= \text{by Lemma 14.1} \\ N_{m+i}''^* &= (\mathbf{J}_T x_{n+i})\{\mathbf{1}_{T(\varepsilon)}/x_{n+i}\} = \mathbf{J}_T \mathbf{1}_{T(\varepsilon)} = \mathbf{J}_T \text{ by Lemma 14.2 and 11} \end{align*} $$

**Induction case.** $\sigma = \langle i \rangle \star \sigma'$.

By Lemma 8, for $n-m=n'-m'$ and $i+1 \le \min\{m, m'\}$ we have:

$$M = \lambda x_1 \dots x_n \cdot y M_1 \dots M_m \qquad N = \lambda x_1 \dots x_{n'} \cdot y N_1 \dots N_{m'}$$

where $M_j \sqsubseteq^{\text{hnf}} N_j$ for all $j \le \min\{m, m'\}$ and either $y$ is free or $y = x_j$ for $j \le \min\{n, n'\}$. Suppose that, say, $n \le n'$. Then there is $p \ge 0$ such that $n' = n+p$ and $m' = m+p$. Since $M_{i+1} \sqsubseteq^{\text{hnf}} N_{i+1}$ and $\sigma' : M_{i+1} \not\sqsubseteq^{\text{hnf}} N_{i+1}$ we apply the induction hypothesis and get, for any $k'$ large enough, $\vec{Y} \in \Lambda^\sigma$ such that $M_{i+1}\{\mathbf{P}_{k'}/\vec{y}, \vec{x}\}\vec{Y} =_{\beta} \mathbf{1}_{T(\varepsilon)}$ and $N_{i+1}\{\mathbf{P}_{k'}/\vec{y}, \vec{x}\}\vec{Y} =_{\mathcal{B}} \mathbf{J}_T$. For any $k \ge \max\{k', n+m+p\}$, we set $\vec{X} := \mathbf{P}_k^{\sim n+p} \Omega^{\sim k-m-p} \mathbf{U}_{i+1}^k \vec{Y}$.

We suppose that $y$ is free, the other case being analogous. On the one side we have:

$$ \begin{align*} (\lambda x_1 \dots x_n \cdot y M_1 \dots M_m)\{\mathbf{P}_k/\vec{y}\}\vec{X} &= \\ (\lambda x_1 \dots x_n \cdot \mathbf{P}_k M_1' \dots M_m')\mathbf{P}_k^{\sim n+p} \Omega^{\sim k-m-p} \mathbf{U}_{i+1}^k \vec{Y} &=_{\beta} \text{where } M'_{\ell} := M_{\ell}\{\mathbf{P}_k/\vec{y}\} \\ (\mathbf{P}_k M_1'' \dots M_m'')\mathbf{P}_k^{\sim p} \Omega^{\sim k-m-p} \mathbf{U}_{i+1}^k \vec{Y} &=_{\beta} \text{where } M''_{\ell} := M'_{\ell}\{\mathbf{P}_k/\vec{x}\} \\ (\lambda z \cdot z M_1'' \dots M_m''')\mathbf{P}_k^{\sim p} \Omega^{\sim k-m-p} \mathbf{U}_{i+1}^k \vec{Y} &=_{\beta} \text{by Lemma 14.1} \\ M_{i+1}'' \vec{Y} &= M_{i+1}\{\mathbf{P}_k/\vec{y}, \vec{x}\}\vec{Y} =_{\beta} \mathbf{1}_{T(\varepsilon)} \text{ by Lemma 14.2 and IH} \end{align*} $$

On the other side, we have:

$$ \begin{align*} (\lambda x_1 \dots x_{n+p} \cdot y N_1 \dots N_{m+p})\{\mathbf{P}_k/\vec{y}\}\vec{X} &= \\ (\lambda x_1 \dots x_{n+p} \cdot \mathbf{P}_k N_1' \dots N_{m+p}')\vec{X} &=_{\beta} \text{where } N'_{\ell} := N_{\ell}\{\mathbf{P}_k/\vec{y}\} \\ (\mathbf{P}_k N_1'' \dots N_{m+p}'')\Omega^{\sim k-m-p} \mathbf{U}_{i+1}^k \vec{Y} &=_{\beta} \text{where } N''_{\ell} := N'_{\ell}\{\mathbf{P}_k/\vec{x}\} \\ (\lambda z \cdot z N_1'' \dots N_{m+p}'')\Omega^{\sim k-m-p} \mathbf{U}_{i+1}^k \vec{Y} &=_{\beta} \text{by Lemma 14.1} \\ N_{i+1}'' \vec{Y} &= N_{i+1}\{\mathbf{P}_k/\vec{y}, \vec{x}\}\vec{Y} =_{\mathcal{B}} \mathbf{J}_T \text{ by Lemma 14.2 and IH} \end{align*} $$

<figure><img src="image_9.png" /></figure>
From Proposition 13 we get this immediate corollary of Lemma 15.

**Corollary 16.** Let $M, N \in \Lambda$ such that $M$ is $\beta$-normal, $N \notin \beta$ $NF_\beta$ and $M \sqsubseteq^{\text{hnf}} N$. Then there is a head context $C[-]$ such that $C[M] =_{\beta\eta} \mathbf{I}$ and $C[N] =_{\mathcal{B}} \mathbf{J}_T$ for some $T \in \mathbb{T}^{\infty}_{\text{rec}}$.

**Theorem 17 (Morris Separation).** Let $M, N \in \Lambda$ such that $M \sqsubseteq^{\text{hnf}} N$ while $M \nsqsubseteq^{\text{hnf}} N$. There is a head context $C[-]$ such that $C[M] =_{\beta\eta} \mathbf{I}$ and $C[N] =_{\mathcal{B}} \mathbf{J}_T$ for some $T \in \mathbb{T}^{\infty}_{\text{rec}}$. When $M, N \in \Lambda^\circ$ the context $C[-]$ can be chosen closed and applicative.

**Proof.** Since $M \nsqsubseteq^{\text{hnf}} N$, there is a head context $D_2[-]$ such that $D_2[M] \in_{\beta} NF_\beta$, while $D_2[N] \notin_{\beta} NF_\beta$. From $M \sqsubseteq^{\text{hnf}} N$ we obtain $D_2[M] \sqsubseteq^{\text{hnf}} D_2[N]$. Therefore we can apply Corollary 16, and get a head context $D_1[-]$ such that $D_1[D_2[M]] =_{\beta\eta} \mathbf{I}$ and $D_1[D_2[N]] =_{\mathcal{B}} \mathbf{J}_T$ for some $T \in \mathbb{T}^{\infty}_{\text{rec}}$. Hence the head context $C[-]$ we are looking for is actually $D_1[D_2[-]]$. When $M, N$ are closed, all the contexts can be chosen closed and applicative. ◀

# 4 Relational Graph Models

In this section we recall the definition of *relational graph models* (rgm, for short). Individual examples of such models were previously studied in the literature (e.g., in [15]), but the class of rgms was formally introduced in [20]. We refer the reader to [22] for a detailed analysis.

## 4.1 The Relational Semantics

Relational graph models are called *relational* since they are reflexive objects in the cartesian closed category $\mathbf{MRel}$ [5], which is the Kleisli category of $\mathbf{Rel}$ with respect to the finite multisets comonad $\mathcal{M}_f(-)$. Before going further we briefly recall the category $\mathbf{MRel}$, but we refer to [5] for a detailed presentation.

Given a set $A$, a *multiset* over $A$ is any map $a : A \to \mathbb{N}$. Given $\alpha \in A$ and a multiset $a$ over $A$, the *multiplicity of $\alpha$ in $a$* is given by $a(\alpha)$. A multiset $a$ is called *finite* if its *support* $\text{supp}(a) = \{\alpha \in A \mid a(\alpha) \neq 0\}$ is finite. A finite multiset $a$ is represented by the unordered list of its elements $[\alpha_1, \dots, \alpha_n]$, possibly with repetitions, and the empty multiset is denoted by $[\cdot]$. We write $\mathcal{M}_f(A)$ for the set of all finite multisets over $A$. Given $a_1, a_2 \in \mathcal{M}_f(A)$, their *multiset union* is denoted by $a_1 + a_2$ and defined as a pointwise sum.

The objects of $\mathbf{MRel}$ are all the sets. A morphism $f \in \mathbf{MRel}(A, B)$ is any relation between $\mathcal{M}_f(A)$ and $B$, in other words $\mathbf{MRel}(A, B) = \mathcal{P}(\mathcal{M}_f(A) \times B)$. The composition of $f \in \mathbf{MRel}(A, B)$ and $g \in \mathbf{MRel}(B, C)$ is defined as follows:

$$f;g = \{(a_1 + \dots + a_k, \gamma) \mid \exists \beta_1, \dots, \beta_k, \text{ such that } (a_i, \beta_i) \in f, ([\beta_1, \dots, \beta_k], \gamma) \in g\}.$$

The identity of $A$ is the relation $\text{Id}_A = \{([\alpha], \alpha) \mid \alpha \in A\}$. It is easy to check that the product is the disjoint union $A \uplus B$ and the exponential object $A \Rightarrow B$ is $\mathcal{M}_f(A) \times B$. As usual, we will silently use Seely's isomorphisms between $\mathcal{M}_f(A \uplus B)$ and $\mathcal{M}_f(A) \times \mathcal{M}_f(B)$.

Relational graph models correspond to a particular subclass of reflexive objects in living in $\mathbf{MRel}$. In particular, they are all *linear* in the sense that the morphisms inducing the retraction are linear [19]. Therefore, they are also models of the resource calculus [8].

**Definition 18.** A *relational graph model* $\mathcal{D} = (D, i)$ is given by an infinite set $D$ and a total injection $i : \mathcal{M}_f(D) \times D \to D$. We say that $\mathcal{D}$ is *extensional* when $i$ is bijective.

We denote $i(a, \alpha)$ by $a \to_i \alpha$, or simply by $a \to \alpha$ when $i$ is clear.

Notice that any function $f : A \to B$ can be sent to a relation $f^\dagger \in \mathbf{MRel}(A, B)$ by setting $f^\dagger = \{([a], f(a)) \mid a \in A\}$. Therefore, every rgm $\mathcal{D} = (D, i)$ induces a reflexive object.
70:12 New Results on Morris's Observational Theory

**Remark.** The set $\mathcal{D}$ is a reflexive object since $i^{\dagger}$; $(i^{-1})^{\dagger} = \text{Id}_{\mathcal{D}\to\mathcal{D}}$. If $\mathcal{D}$ is extensional (in the sense that $i$ is bijective) the model is extensional in the sense that $(i^{-1})^{\dagger}$; $i^{\dagger} = \text{Id}_{\mathcal{D}}$.

Note that, when $i$ is just injective, there are different (linear) morphisms that can be chosen as inverses. There are therefore linear reflexive objects in $\mathbf{MRel}$ that are not rgms. However, the class of extensional rgms coincide with the class of extensional (linear) reflexive objects.

Relational graph models, just like the regular ones [2], can be built by performing the free completion of a partial pair.

**Definition 19.** A partial pair $\mathcal{A}$ is a pair $(A, j)$ where $A$ is a non-empty set of elements (called *atoms*) and $j: \mathcal{M}_f(A) \times A \to A$ is a partial injection. We say that $\mathcal{A}$ is *extensional* when $j$ is a bijection between $\text{dom}(j)$ and $A$.

Hereafter, we will only consider partial pairs $\mathcal{A}$ whose underlying set $A$ does not contain any pair. This is not restrictive because partial pairs can be considered up to isomorphism.

**Definition 20.** The completion $\overline{\mathcal{A}}$ of a partial pair $\mathcal{A}$ is the pair $(\overline{A}, \overline{j})$ defined as follows: $\overline{A} = \bigcup_{n \in \mathbb{N}} A_n$, where $A_0 = A$ and $A_{n+1} = ((\mathcal{M}_f(A_n) \times A_n) - \text{dom}(j)) \cup A$; moreover

$$ \overline{j}(a, \alpha) = \begin{cases} j(a, \alpha) & \text{if } (a, \alpha) \in \text{dom}(j), \\ (a, \alpha) & \text{otherwise.} \end{cases} $$

We say that an atom $\alpha \in A$ has *rank 0*, whilst an element $\alpha \in \overline{A} - A$ has *rank k* if $\alpha \in A_k - A_{k-1}$. Note that, for every rgm $\mathcal{D}$ we have that $\overline{\mathcal{D}} = \mathcal{D}$ (up to isomorphism).

**Proposition 21.** If $\mathcal{A}$ is an (extensional) partial pair, then $\overline{\mathcal{A}}$ is an (extensional) rgm.

**Proof.** The proof of the fact that $\overline{\mathcal{A}}$ is an rgm is analogous to the one for regular graph models [2]. It is easy to check that when $j$ is bijective, also its completion $\overline{j}$ is. ◀

**Example 22.** We define the relational analogues of:

- Engeler's model [10]: $\mathcal{E} = (\mathbb{N}, \emptyset)$, first defined in [15],

- Scott's model [24]: $\mathcal{D}_{\omega} = (\{\star\}, \{(\llbracket, \star) \mapsto \star\})$, first defined (up to isomorphism) in [5],

- Coppo, Dezani and Zacchi's model [6]: $\mathcal{D}_{\star} = (\{\star\}, \{(\llbracket, \star) \mapsto \star\})$, introduced in [20].

Notice that $\mathcal{D}_{\omega}$ and $\mathcal{D}_{\star}$ are extensional, while $\mathcal{E}$ is not.

## 4.2 The Approximation Theorem

We now show how $\lambda$-terms and Böhm trees can be interpreted in an rgm, and we recall the main properties enjoyed by these models. Using the terminology of [1], rgms are *continuous* models, in the sense that they all enjoy the approximation theorem (Theorem 27). From this, it follows that the $\lambda$-theory induced by an extensional rgm always includes $\mathcal{H}^+$ (Corollary 29).

Given two $n$-uples $\vec{a}, \vec{b} \in \mathcal{M}_f(A)^n$ we write $\vec{a} + \vec{b}$ for $(a_1 + b_1, \dots, a_n + b_n) \in \mathcal{M}_f(A)^n$.

**Definition 23.** Let $M \in \Lambda$ and let $\vec{x} \in \mathbb{V}^n$ be such that $\text{FV}(M) \subseteq \vec{x}$. The interpretation of $M$ in $\mathcal{D}$ w.r.t. $\vec{x}$ is the relation $[[M]]_{\vec{x}} \subseteq \mathcal{M}_f(D)^n \times D$ defined inductively as follows:

- $[[x_k]]_{\vec{x}} = \{(\llbracket, \dots, \llbracket, \alpha \rrbracket, \dots, \llbracket, \dots, \llbracket \alpha \rrbracket) \mid \alpha \in D\}$, where $[\alpha]$ stands in $k$-th position,

- $[[MN]]_{\vec{x}} = \{(\vec{a}_0 + \dots + \vec{a}_k), \alpha) \mid \exists \beta_1, \dots, \beta_k \in \mathcal{D}, \text{ such that } (\vec{a}_0, [\beta_1, \dots, \beta_k] \to \alpha) \in [[M]]_{\vec{x}}^D \text{ and, for all } 1 \le \ell \le k, (\vec{a}_\ell, \beta_\ell) \in [[N]]_{\vec{x}}^D\}$.

- $[[\lambda y.N]]_{\vec{x}}^D = \{(\vec{a}, (b \to \alpha)) \mid ((\vec{a}, b), \alpha) \in [[N]]_{\vec{x},y}^D\}$, where by $\alpha$-equivalence we assume $y \notin \vec{x}$.

This definition extends to approximants $t \in \text{NF}_{\perp}$ by setting $[[\perp]]_{\vec{x}}^D = \emptyset$ and to Böhm trees by interpreting all their finite approximants $[[\text{BT}(M)]]_{\vec{x}}^D = \bigcup_{t \in \text{BT}^*(M)} [[t]]_{\vec{x}}^D$.

Whenever we write $[[M]]_{\vec{x}}^D$ we always assume that $\text{FV}(M) \subseteq \vec{x}$. When $M$ is a combinator, we consider $[[M]]^D \subseteq D$. In all our notations we will omit the model $\mathcal{D}$ when it is clear.
**► Example 24.** Let $\mathcal{D}$ be any rgm. Then we have:

1. $[[\mathbf{I}]^\mathcal{D} = [[\alpha] \to \alpha \mid \alpha \in D]}$ and $[[\mathbf{1}]^\mathcal{D} = [[a \to \alpha] \to a \to \alpha \mid \alpha \in D, a \in \mathcal{M}_f(D)]}$, thus:

2. $[[\mathbf{J}]^\mathcal{D} = [[\alpha] \to \alpha \mid \alpha \in D'] \subseteq [[\mathbf{1}]^\mathcal{D} \subseteq [[\mathbf{I}]^\mathcal{D}],}$ where $D'$ is the smallest subset of $D$ satisfying: if $\alpha \in D$ then $[] \to \alpha \in D'$; if $\alpha \in D$ and $a \in \mathcal{M}_f(D')$ then $a \to \alpha \in D'$,

3. $[[\Delta]^\mathcal{D} = \{(a + [a \to \alpha]) \to \alpha \mid \alpha \in D, a \in \mathcal{M}_f(D)\}$ therefore $[[\Omega]^\mathcal{D} = [[\perp]^\mathcal{D} = \emptyset]$,

4. $[[\lambda x.x\Omega]^\mathcal{D} = \{[[ \to \alpha ] \to \alpha \mid \alpha \in D]}$.

It follows that $[[\mathbf{I}] = [[\mathbf{1}]}$ in both $\mathcal{D}_\omega$ and $\mathcal{D}_\star$, but $[[\mathbf{I}]^\mathcal{D}_\omega = [[\mathbf{J}]^\mathcal{D}_\omega$, while $\star \in [[\mathbf{I}]^\mathcal{D}_\star - [[\mathbf{J}]^\mathcal{D}_\star]$.

Rgms satisfy the following substitution property, and are sound models of $\lambda$-calculus.

**► Lemma 25.** (cf. [22]) Let $M, N \in \Lambda$ and $\mathcal{D}$ be a relational graph model.

1. (Substitution) $(\vec{a}, \alpha) \in [[M\{N/y}\]]_{\vec{x}}^\mathcal{D}$ iff there are $\beta_1, \dots, \beta_k \in D$, $\vec{a}_0, \dots, \vec{a}_k \in \mathcal{M}_f(D)^n$ such that $(\vec{a}_\ell, \beta_\ell) \in [[N]\]_{\vec{x}}^\mathcal{D}$, for $1 \le \ell \le k$, $((a_0, [\beta_1, \dots, \beta_k]), \alpha) \in [[M]\]_{\vec{x},y}^\mathcal{D}$ and $\vec{a} = \sum_{\ell=0}^k \vec{a}_\ell$.

2. (Soundness) If $M =_\beta N$ then $[[M]\]_{\vec{x}}^\mathcal{D} = [[N]\]_{\vec{x}}^\mathcal{D}$ for all $\vec{x}$ containing $\mathrm{FV}(M) \cup \mathrm{FV}(N)$.

The $\lambda$-theory induced by $\mathcal{D}$ is defined by $\mathrm{Th}(\mathcal{D}) = \{(M, N) \in \Lambda \times \Lambda \mid [[M]\]_{\vec{x}} = [[N]\]_{\vec{x}}\}$. The preorder theory induced by $\mathcal{D}$ is given by $\mathrm{Th}_\subseteq(\mathcal{D}) = \{(M, N) \in \Lambda \times \Lambda \mid [[M]\]_{\vec{x}} \subseteq [[N]\]_{\vec{x}}\}$. We will write $\mathcal{D} \models M = N$ when $(M, N) \in \mathrm{Th}(\mathcal{D})$, and $\mathcal{D} \models M \sqsubseteq N$ when $(M, N) \in \mathrm{Th}_\subseteq(\mathcal{D})$.

**► Definition 26.** A model $\mathcal{D}$ is called *inequationally $\mathcal{O}$-fully abstract* when $\mathcal{D} \models M \sqsubseteq N$ iff $M \sqsubseteq^\mathcal{O} N$. A model $\mathcal{D}$ is called *$\mathcal{O}$-fully abstract* whenever $\mathcal{D} \models M = N$ iff $M \equiv^\mathcal{O} N$.

It is easy to check that in every extensional rgm $\mathcal{D}$ we have $\mathcal{D} \models \mathbf{I} = \mathbf{1}$, thus $\lambda\eta \subseteq \mathrm{Th}(\mathcal{D})$. As a consequence, the $\lambda$-theories induced by rgms and by ordinary graph models are different, since no graph model is extensional. For instance, the $\lambda$-theory of $\mathcal{D}_\omega$, the relational analogue of Scott's model $\mathcal{D}_\infty$, is $\mathcal{H}^*$ [18]. In other words, the model $\mathcal{D}_\omega$ is hnf-fully abstract.

All rgms enjoy the approximation theorem for Böhm trees below. As usual, this result can be proved via techniques based on finite approximants (see [18]). However, in [20] we provided a new proof exploiting the following facts: rgms are models of Ehrhard and Regnier's resource calculus [8]; they satisfy the Taylor expansion [19]; two $\lambda$-terms have the same Böhm tree iff the normal form of the support of their Taylor expansions coincide [9].

Recall from page 4 that $\mathrm{BT}^*(M)$ denotes the set of all finite approximants of $\mathrm{BT}(M)$.

**► Theorem 27 (Approximation Theorem [20]).** Let $M$ be a $\lambda$-term. Then $(\vec{a}, \alpha) \in [[M]\]_{\vec{x}}$ if and only if there exists $t \in \mathrm{BT}^*(M)$ such that $(\vec{a}, \alpha) \in [[t]\]_{\vec{x}}$. Therefore $[[M]\]_{\vec{x}} = [[\mathrm{BT}(M)]\]_{\vec{x}}$.

**► Corollary 28.** For all rgms $\mathcal{D}$ we have that $\mathcal{B} \subseteq \mathrm{Th}(\mathcal{D})$. In particular $\mathrm{Th}(\mathcal{D})$ is sensible and $[[M]\]_{\vec{x}}^\mathcal{D} = \emptyset$ for all unsolvable $\lambda$-terms $M$.

*Proof.* From Theorem 27 we get $[[M]\]_{\vec{x}} = [[\mathrm{BT}(M)]\]_{\vec{x}} = \bigcup_{t \in \mathrm{BT}^*(M)} [[t]\]_{\vec{x}}$. Therefore, whenever $\mathrm{BT}(M) = \mathrm{BT}(N)$ we have $[[M]\]_{\vec{x}} = [[\mathrm{BT}(M)]\]_{\vec{x}} = [[\mathrm{BT}(N)]\]_{\vec{x}} = [[N]\]_{\vec{x}}$. Thus $\mathcal{B} \subseteq \mathrm{Th}(\mathcal{D})$. $\quad$

In the next corollary we are going to use the following characterization of Morris's pre-order $\sqsubseteq^\mathcal{nf}$, which is based on Lévy's notion of extensional Böhm trees [16]:

$$ \mathrm{BT}^e(M) = \{\mathrm{nf}_\eta(t) \mid t \in \mathrm{BT}^*(M'), M' \to_\eta M\}. $$

By [13], we have $M \sqsubseteq^\mathcal{nf} N$ if and only if $\mathrm{BT}^e(M) \subseteq \mathrm{BT}^e(N)$.

**► Corollary 29.** The order theory of any extensional rgm $\mathcal{D}$ contains $\sqsubseteq^\mathcal{nf}$, so $\mathcal{H}^+ \subseteq \mathrm{Th}(\mathcal{D})$.

*Proof.* From Theorem 27 we obtain $[[M]\]_{\vec{x}} = \bigcup_{t \in \mathrm{BT}^*(M)} [[t]\]_{\vec{x}}$. From the extensionality of $\mathcal{D}$, we get $[[M]\]_{\vec{x}} = \bigcup_{M' \to_\eta M, t \in \mathrm{BT}^*(M')} [[t]\]_{\vec{x}} = \bigcup_{M' \to_\eta M, t \in \mathrm{BT}^*(M')} [[\mathrm{nf}_\eta(t)]\]_{\vec{x}} = [[\mathrm{BT}^e(M)]\]_{\vec{x}}$. So, we have that $\mathrm{BT}^e(M) \subseteq \mathrm{BT}^e(N)$ entails $[[M]\]_{\vec{x}} = [[\mathrm{BT}^e(M)]\]_{\vec{x}} \subseteq [[\mathrm{BT}^e(N)]\]_{\vec{x}} = [[N]\]_{\vec{x}}$. $\quad$
By applying the Approximation Theorem we get the following characterization of $W_D(T)$.

**Proposition 32.** For any extensional rgm $\mathcal{D}$ and any tree $T \in \mathbb{T}_{\text{rec}}^{\infty}$:

$$W_D(T) = \{\alpha \in D \mid ([\alpha], \alpha) \notin [[\mathbf{J}_T x]]_x\}.$$

**Proof.** ($\subseteq$) Follows immediately from the Approximation Theorem 27 and from Lemma 31.

($\supseteq$) Let $\alpha \in D$ such that $([\alpha], \alpha) \notin [[\mathbf{J}_T x]]_x$. We coinductively construct a path $f$ such that $\alpha \in W_f(T)$. As $T$ is infinite we have $\mathbf{J}_T x = \beta \lambda x_0 \dots x_n x(\mathbf{J}_{T|_{\langle 0 \rangle}} x_0) \dots (\mathbf{J}_{T|_{\langle n \rangle}} x_n)$ and since $\mathcal{D}$ is extensional $\alpha = a_0 \to \dots \to a_n \to \alpha'$. From $([\alpha], \alpha) \notin [[\mathbf{J}_T x]]_x$ and Lemma 25.2 we get $([\alpha], \alpha) \notin [[\lambda x_0 \dots x_n x(\mathbf{J}_{T|_{\langle 0 \rangle}} x_0) \dots (\mathbf{J}_{T|_{\langle n \rangle}} x_n)]_x$, therefore there is an index $k \le n$ such that $a_k \ne []$ and an element $\beta \in a_k$ such that $([\beta], \beta) \notin [[\mathbf{J}_{T|_{\langle k \rangle}} x_k]]_{x_k}$. By the coinductive hypothesis, there exists a function $g$ such that $\beta \in W_g(T|_{\langle k \rangle})$. We conclude since $\alpha \in W_f(T)$ where $f$ is the function defined as follows: $f(0) = k$ and $f(n+1) = g(n)$ for all $n \in \mathbb{N}$. $\blacksquare$

It should be now clear that in an rgm $\mathcal{D}$ fully abstract for $\mathcal{H}^+$, every infinite $\lambda$-definable tree needs an element in $\mathcal{D}$ witnessing its infinite path, which exists by König's lemma.

**Definition 33** ($\lambda$-König models). An rgm $\mathcal{D}$ is $\lambda$-König if for every $T \in \mathbb{T}_{\text{rec}}^{\infty}$, $W_D(T) \ne \emptyset$.

## 5.2 The Characterization

We will focus on the $\lambda$-König condition, since the extensionality is necessary, as $\lambda\eta \subseteq \mathcal{H}^+$.

### Lambda-König Implies Inequational Full Abstraction.

Let $\mathcal{D}$ be an extensional $\lambda$-König relational graph model. Since every $T \in \mathbb{T}_{\text{rec}}^{\infty}$ has a non-empty set of witnesses $W_D(T)$, by Proposition 32, there is an element $\alpha \in W_D(T)$ such that $[\alpha] \to \alpha \notin [[\mathbf{I}] - [[\mathbf{J}_T]]]$. Thus, $\mathcal{D}$ separates $\mathbf{I}$ from all the $\mathbf{J}_T$'s.

**Theorem 34** (Inequational Full Abstraction). Let $\mathcal{D}$ be an extensional $\lambda$-König rgm, then:

$$M \sqsubseteq^{\text{nf}} N \iff \mathcal{D} \models M \sqsubseteq N$$

**Proof.** ($\Rightarrow$) This follows directly from Corollary 29.

($\Leftarrow$) We assume, by the way of contradiction, that $\mathcal{D} \models M \sqsubseteq N$ but $M \not\sqsubseteq^{\text{nf}} N$. Since $\sqsubseteq^{\text{hnf}}$ is maximal (cf. [1, Lemma 16.2.4]) and $[[M]]_{\vec{x}} \subseteq [[N]]_{\vec{x}}$ we must have $M \sqsubseteq^{\text{hnf}} N$. By Theorem 17 there exists a context $C[-]$ such that $C[M] =_{\beta\eta} \mathbf{I}$ and $C[N] =_{\beta} \mathbf{J}_T$ for some $T \in \mathbb{T}_{\text{rec}}^{\infty}$. Since $[[\cdot]]$ is contextual and, by Corollary 29, $B\eta \subseteq \mathcal{H}^+ \subseteq \text{Th}(\mathcal{D})$ we have $[[\mathbf{I}]] = [[C[M]]] \subseteq [[C[N]]] = [[\mathbf{J}_T]]$. We derive a contradiction by applying Proposition 32. $\blacksquare$

### Inequational Full Abstraction Implies Lambda-König.

**Theorem 35.** Let $\mathcal{D}$ be an rgm. If $\text{Th}_{\subseteq}(\mathcal{D}) = \sqsubseteq^{\text{nf}}$ then $\mathcal{D}$ is extensional and $\lambda$-König.

**Proof.** Obviously $\mathcal{D}$ must be extensional since $\mathcal{H}^*$ is an extensional $\lambda$-theory. By the way of contradiction, we suppose that it is not $\lambda$-König, then there is $T \in \mathbb{T}_{\text{rec}}^{\infty}$ such that $W_D(T) = \emptyset$ and, by Proposition 32, we get $[[\mathbf{I}]] = [[\mathbf{J}_T]]$. This is impossible since $\mathbf{I} \not\sqsubseteq^{\text{nf}} \mathbf{J}_T$. $\blacksquare$

From Theorems 34 and 35 we get the main semantic result of the paper.

**Theorem 36.** An extensional rgm $\mathcal{D}$ is $\lambda$-König if and only if $\mathcal{D}$ is inequationally fully abstract for Morris's preorder $\sqsubseteq^{\text{nf}}$.

The following result first appeared in [20].

**Corollary 37.** The model $\mathcal{D}_*$ of Example 22 is inequationally fully abstract for Morris's preorder $\sqsubseteq^{\text{nf}}$. In particular $\text{Th}(\mathcal{D}_*) = \mathcal{H}^+$.
**6 The λ-Theory $\mathcal{H}^+$ Satisfies the ω-Rule**

This section is devoted to show that $\mathcal{H}^+$ satisfies the $\omega$-rule. We will focus on its restriction to closed terms $\omega^0$, and conclude since $T \vdash \omega$ if and only if $T \vdash \omega^0$, as shown in [12].

Recall that, by the context lemma, if two closed λ-terms $M$ and $N$ are such that $M \not\sqsubseteq^\text{hnf} N$ holds, then the context $C[-]$ semi-separating them can be chosen applicative and closed, that is $C[-] = [-]\vec{Z}$ for $\vec{Z} \in \Lambda^o$.

**Lemma 38.** Let $M, N \in \Lambda^o$ be such that $M \in \beta \text{ NF}_\beta$, while $N \notin \beta \text{ NF}_\beta$. Then, there exist $n \ge 1$ and combinators $Z_1, \dots, Z_n \in \Lambda^o$ such that $MZ \in \beta \text{ NF}_\beta$ while $NZ \notin \beta \text{ NF}_\beta$.

**Proof.** By hypothesis $M \not\sqsubseteq^\text{H+} N$. There are two possible cases.

Case $M \sqsubseteq^\text{hnf} N$. Therefore, by Theorem 17 there are $Z_1, \dots, Z_k \in \Lambda^o$ such that $MZ =_{\beta\eta} I$ and $N\vec{Z} =_B J_T$ for some $T \in \mathbb{T}^\infty_{\text{rec}}$. If $k=0$ just take the λ-term $1_{T(\varepsilon)}$ as $Z_1$ and conclude since $J_T 1_{T(\varepsilon)} =_B J_T$.

Case $M \not\sqsubseteq^\text{hnf} N$. By semi-separability, there are $Z_1, \dots, Z_k \in \Lambda^o$ such that $MZ =_\beta I$ and $N\vec{Z} =_\beta U$ for some unsolvable $U$. If $k=0$ just take the identity $I$ as $Z_1$. ▲

**Lemma 39.** Let $M, N \in \Lambda^o$. If $\forall Z \in \Lambda^o, MZ =_H NZ$, then

$$ \forall \vec{P} \in \Lambda^o (M\vec{P} \in \beta \text{ NF}_\beta \iff N\vec{P} \in \beta \text{ NF}_\beta). $$

**Proof.** Suppose that for all $Z, \vec{Q} \in \Lambda^o, MZ\vec{Q} \in \beta \text{ NF}_\beta$ if and only if $NZ\vec{Q} \in \beta \text{ NF}_\beta$. We show by induction on the length $k$ of $\vec{P} \in \Lambda^o$ that $M\vec{P} \in \beta \text{ NF}_\beta$ if and only if $N\vec{P} \in \beta \text{ NF}_\beta$.

Base: $k=0$. Since the contrapositive holds by Lemma 38.

Induction: $k > 0$. It follows trivially from the induction hypothesis. ▲

This shows that $\mathcal{H}^+ \vdash \omega^0$. As a consequence, we get our main syntactic result.

**Theorem 40.** $\mathcal{H}^+$ satisfies the ω-rule.

This solves positively the question whether $\mathcal{H}^+ \vdash \omega$ holds. The question whether a more constructive proof can be provided will be addressed in further works.

Sallé's conjecture saying that the inclusion $B\omega \subseteq \mathcal{H}^+$ is proper, which is stated in the proof of [1, Thm. 17.4.16], is still open and under investigation.

**Remark.** In first-order logic, $\omega$-completeness is closely related to the notion of a *standard model*, which has as domain the Herbrand's universe generated by the signature of the given theory. In higher-order languages, Morris-style observational equality is the untyped analogue of extensional equality defined by a logical relation on — again — the ground *term model* of the higher-order language.

Our result perhaps gives some indication that these logical and computational aspects are not at all independent, with the universal property of observational equality being powerful enough to imply $\omega$-completeness in the purely syntactic sense of validating the $\omega$-rule.

**Acknowledgements.**

This work is partly supported by ANR Project Coquas 12JS0200601. We are grateful to Barendregt, Intrigila and Ronchi della Rocca for interesting discussions. We thank the anonymous reviewers for providing helpful remarks to improve the presentation of this paper.
References

1. H.P. Barendregt. *The lambda-calculus, its syntax and semantics*. Number 103 in Studies in Logic and the Foundations of Mathematics. North-Holland, second edition, 1984.

2. C. Berline. From computation to foundations via functions and application: The λ-calculus and its webbed models. *Theoretical Computer Science*, 249(1):81–161, 2000.

3. C. Böhm. Alcune proprietà delle forme β-η-normali nel λ-K-calcolo. *Pub. INAC*, 696, 1968.

4. F. Breuvart. On the characterization of models of $\mathcal{H}^*$. In T. Henzinger and D. Miller, editors, *Joint Meeting CSL-LICS '14*, pages 24:1–24:10. ACM, 2014.

5. A. Bucciarelli, T. Ehrhard, and G. Manzonetto. Not enough points is enough. In *CSL'07*, volume 4646 of *Lecture Notes in Comput. Sci.*, pages 298–312. Springer, 2007.

6. M. Coppo, M. Dezani, and M. Zacchi. Type theories, normal forms and $D_\infty$-lambda-models. *Inf. Comput.*, 72(2):85–116, 1987.

7. M. Dezani-Ciancaglini and E. Giovannetti. From Bohm's theorem to observational equi- valences: an informal account. *Electr. Notes Theor. Comput. Sci.*, 50(2):83–116, 2001.

8. T. Ehrhard and L. Regnier. The differential λ-calculus. *Th. Comp. Sci.*, 309(1):1–41, 2003.

9. T. Ehrhard and L. Regnier. Böhm trees, Krivine's machine and the Taylor expansion of lambda-terms. In *CiE*, volume 3988 of *Lecture Notes in Comput. Sci.*, pages 186–197, 2006.

10. E. Engeler. Algebras and combiners. *Algebra Universalis*, 13(3):389–392, 1981.

11. P. Di Gianantonio, G. Franco, and F. Honsell. Game semantics for untyped λβη-calculus. In *TLCA '99*, volume 1581 of *Lecture Notes in Comput. Sci.*, pages 114–128. Springer, 1999.

12. R. Hindley and G. Longo. Lambda-calculus models and extensionality. *Z. Math. Logik Grundlag. Math.*, 26(4):289–310, 1980.

13. J.M.E. Hyland. A survey of some useful partial order relations on terms of the λ-calculus. In *Lambda-Calculus and Comp. Sci. Th.*, volume 37 of LNCS, pages 83–95. Springer, 1975.

14. J.M.E. Hyland. A syntactic characterization of the equality in some models for the λ-calculus. *J. London Math. Soc. (2)*, 12(3):361–370, 1975/76.

15. J.M.E. Hyland, M. Nagayama, J. Power, and G. Rosolini. A category theoretic formulation for Engeler-style models of the untyped λ-calculus. *Electr. Notes in TCS*, 161:43–57, 2006.

16. J.-J. Lévy. Le lambda calcul - notes du cours, 2005. In French.
http://pauillac.inria.fr/~levy/courses/X/M1/lambda/dea-spp/jjl.pdf.

17. S. Lusin and A. Salibra. The lattice of λ-theories. *J. Log. Comput.*, 14(3):373–394, 2004.

18. G. Manzonetto. A general class of models of $\mathcal{H}^*$. In *MFCS 2009*, volume 5734 of *Lecture Notes in Comput. Sci.*, pages 574–586. Springer, 2009.

19. G. Manzonetto. What is a categorical model of the differential and the resource λ-calculi? *Mathematical Structures in Computer Science*, 22(3):451–520, 2012.

20. G. Manzonetto and D. Ruopolo. Relational graph models, Taylor expansion and extensionality. *Electr. Notes Theor. Comput. Sci.*, 308:245–272, 2014.

21. J.H. Morris. Lambda calculus models of programming languages. PhD thesis, MIT, 1968.

22. L. Paolini, M. Piccolo, and S. Ronchi Della Rocca. Essential and relational models. *Mathematical Structures in Computer Science*, 2015. Doi:10.1017/S0960129515000316.

23. S. Ronchi Della Rocca and L. Paolini. *The Parametric Lambda Calculus - A Metamodel for Computation*. Texts in Theoretical Computer Science. An EATCS Series. Springer, 2004.

24. D. Scott. Continuous lattices. In Lawvere, editor, *Toposes, Algebraic Geometry and Logic*, volume 274 of *Lecture Notes in Math.*, pages 97–136. Springer, 1972.

25. P. Severi and F.J. de Vries. The infinitary lambda calculus of the infinite eta Böhm trees. *To appear in Math. Struct. Comp. Sci.*, 2016.

26. C.P. Wadsworth. The relation between computational and denotational properties for Scott's $D_\infty$-models of the lambda-calculus. *SIAM J. Comput.*, 5(3):488–521, 1976.