16131 LABEL:LastPageAug. 17, 2018Mar. 11, 2020

# A new coinductive confluence proof for infinitary lambda calculus

Łukasz Czajka  University of Copenhagen, Universitetsparken 5, 2100
Copenhagen, Denmark<EMAIL_ADDRESS>
###### Abstract.

We present a new and formal coinductive proof of confluence and normalisation
of Böhm reduction in infinitary lambda calculus. The proof is simpler than
previous proofs of this result. The technique of the proof is new, i.e., it is
not merely a coinductive reformulation of any earlier proofs. We formalised
the proof in the Coq proof assistant.

###### Key words and phrases:

infinitary rewriting, confluence, normalisation, Böhm trees, coinduction

Supported by the European Union’s Horizon 2020 research and innovation
programme under the Marie Skłodowska-Curie grant agreement number 704111.

##  1\. Introduction

Infinitary lambda calculus is a generalisation of lambda calculus that allows
infinite lambda terms and transfinite reductions. This enables the
consideration of “limits” of terms under infinite reduction sequences. For
instance, for a term $M\equiv(\lambda mx.mm)(\lambda mx.mm)$ we have

$M\to_{\beta}\lambda x.M\to_{\beta}\lambda x.\lambda x.M\to_{\beta}\lambda
x.\lambda x.\lambda x.M\to_{\beta}\ldots$

Intuitively, the “value” of $M$ is an infinite term $L$ satisfying
$L\equiv\lambda x.L$, where by $\equiv$ we denote identity of terms. In fact,
$L$ is the normal form of $M$ in infinitary lambda calculus.

In [19, 17] it is shown that infinitary reductions may be defined
coinductively. The standard non-coinductive definition makes explicit mention
of ordinals and limits in a certain metric space [24, 22, 4]. A coinductive
approach is better suited to formalisation in a proof-assistant. Indeed, with
relatively little effort we have formalised our results in Coq (see Section
7).

In this paper we show confluence of infinitary lambda calculus, modulo
equivalence of so-called meaningless terms [26]. We also show confluence and
normalisation of infinitary Böhm reduction over any set of strongly
meaningless terms. All these results have already been obtained in [24, 26] by
a different and more complex proof method.

In a related conference paper [10] we have shown confluence of infinitary
reduction modulo equivalence of root-active subterms, and confluence of
infinitary Böhm reduction over root-active terms. The present paper is quite
different from [10]. A new and simpler method is used. The proof in [10]
follows the general strategy of [24]. There first confluence modulo
equivalence of root-active terms is shown, proving confluence of an auxiliary
$\epsilon$-calculus as an intermediate step. Then confluence of Böhm reduction
is derived from confluence modulo equivalence of root-active terms. Here we
first show that every term has a unique normal form reachable by a special
standard infinitary $N_{\mathcal{U}}$-reduction. Then we use this result to
derive confluence of Böhm reduction, and from that confluence modulo
equivalence of meaningless terms. We do not use any $\epsilon$-calculus at
all. See the beginning of Section 5 for a more detailed discussion of our
proof method.

###  1.1. Related work

Infinitary lambda calculus was introduced in [24, 23]. Meaningless terms were
defined in [26]. The confluence and normalisation results of this paper were
already obtained in [24, 26], by a different proof method. See also [22, 4,
18] for an overview of various results in infinitary lambda calculus and
infinitary rewriting.

Joachimski in [21] gives a coinductive confluence proof for infinitary lambda
calculus, but Joachimski’s notion of reduction does not correspond to the
standard notion of a strongly convergent reduction. Essentially, it allows for
infinitely many parallel contractions in one step, but only finitely many
reduction steps. The coinductive definition of infinitary reductions capturing
strongly convergent reductions was introduced in [19]. Later [16, 17]
generalised this to infinitary term rewriting systems. In [10] using the
definition from [19], confluence of infinitary lambda calculus modulo
equivalence of root-active subterms was shown coinductively. The proof in [10]
follows the general strategy of [24, 23]. The proof in the present paper bears
some similarity to the proof of the unique normal forms property of orthogonal
iTRSs in [30]. It is also similar to the coinductive confluence proof for
nearly orthogonal infinitary term rewriting systems in [12], but there the
“standard” reduction employed is not unique and need not be normalising.

Confluence and normalisation results in infinitary rewriting and infinitary
lambda calculus have been generalised to the framework of infinitary
combinatory reduction systems [27, 28, 29].

There are three well-known variants of infinitary lambda calculus: the
$\Lambda^{111}$, $\Lambda^{001}$ and $\Lambda^{101}$ calculi [4, 18, 24, 23].
The superscripts $111$, $001$, $101$ indicate the depth measure used: $abc$
means that we shall add $a$/$b$/$c$ to the depth when going down/left/right in
the tree of the lambda term [24, Definition 6]. In this paper we are concerned
only with a coinductive presentation of the $\Lambda^{111}$-calculus.

In the $\Lambda^{001}$-calculus, after addition of appropriate $\bot$-rules,
every finite term has its Böhm tree [23] as the normal form. In
$\Lambda^{111}$ and $\Lambda^{101}$, the normal forms are, respectively,
Berarducci trees and Levy-Longo trees [24, 23, 6, 35, 36]. With the addition
of infinite $\eta$\- or $\eta!$-reductions it is possible to also capture,
respectively, $\eta$-Böhm or $\infty\eta$-Böhm trees as normal forms [40, 44].

The addition of $\bot$-rules may be avoided by basing the definition of
infinitary terms on ideal completion. This line of work is pursued in [1, 2,
3]. Confluence of the resulting calculi is shown, but the proof depends on the
confluence results of [24].

##  2\. Infinite terms and corecursion

In this section we define many-sorted infinitary terms. We also explain and
justify guarded corecursion using elementary notions. The results of this
section are well-known.

A _many-sorted algebraic signature_
$\Sigma=\langle\Sigma_{s},\Sigma_{c}\rangle$ consists of a collection of _sort
symbols_ $\Sigma_{s}=\\{s_{i}\\}_{i\in I}$ and a collection of _constructors_
$\Sigma_{c}=\\{c_{j}\\}_{j\in J}$. Each constructor $c$ has an associated
_type_ $\tau(c)=(s_{1},\ldots,s_{n};s)$ where
$s_{1},\ldots,s_{n},s\in\Sigma_{s}$. If $\tau(c)=(;s)$ then $c$ is a
_constant_ of sort $s$. In what follows we use $\Sigma,\Sigma^{\prime}$, etc.,
for many-sorted algebraic signatures, $s,s^{\prime}$, etc., for sort symbols,
and $f,g,c,d$, etc., for constructors.

The set ${\mathcal{T}}^{\infty}(\Sigma)$, or just ${\mathcal{T}}(\Sigma)$, of
_infinitary terms over $\Sigma$_ is the set of all finite and infinite terms
over $\Sigma$, i.e., all finite and infinite labelled trees with labels of
nodes specified by the constructors of $\Sigma$ such that the types of labels
of nodes agree. More precisely, a term $t$ over $\Sigma$ is a partial function
from $\mathbb{N}^{*}$ to $\Sigma_{c}$ satisfying:

  * •

$t(\epsilon){\downarrow}$, and

  * •

if $t(p)=c\in\Sigma_{c}$ with $\tau(c)=(s_{1},\ldots,s_{n};s)$ then

    * –

$t(pi)=d\in\Sigma_{c}$ with
$\tau(d)=(s_{1}^{\prime},\ldots,s_{m_{i}}^{\prime};s_{i})$ for $i<n$,

    * –

$t(pi){\uparrow}$ for $i\geq n$,

  * •

if $t(p){\uparrow}$ then $t(pi){\uparrow}$ for every $i\in\mathbb{N}$,

where $t(p){\uparrow}$ means that $t(p)$ is undefined, $t(p){\downarrow}$
means that $t(p)$ is defined, and $\epsilon\in\mathbb{N}^{*}$ is the empty
string. We use obvious notations for infinitary terms, e.g., $f(g(t,s),c)$
when $c,f,g\in\Sigma_{c}$ and $t,s\in{\mathcal{T}}(\Sigma)$, and the types
agree. We say that a term $t$ _is of sort $s$_ if $t(\epsilon)$ is a
constructor of type $(s_{1},\ldots,s_{n};s)$ for some
$s_{1},\ldots,s_{n}\in\Sigma_{s}$. By ${\mathcal{T}}_{s}(\Sigma)$ we denote
the set of all terms of sort $s$ from ${\mathcal{T}}(\Sigma)$.

Let $A$ be a set. Let $\Sigma$ consist of two sorts $\mathfrak{s}$ and
$\mathfrak{d}$, one constructor $\mathtt{cons}$ of type
$(\mathfrak{d},\mathfrak{s};\mathfrak{s})$ and a distinct constant $a\in A$ of
sort $\mathfrak{d}$ for each element of $A$. Then
${\mathcal{T}}_{\mathfrak{s}}(\Sigma)$ is the set of streams over $A$. We also
write ${\mathcal{T}}_{\mathfrak{s}}(\Sigma)=A^{\omega}$ and
${\mathcal{T}}_{\mathfrak{d}}(\Sigma)=A$. Instead of $\mathtt{cons}(a,t)$ we
usually write $a:t$, and we assume that $:$ associates to the right, e.g.,
$x:y:t$ is $x:(y:t)$. We also use the notation $x:t$ to denote the application
of the constructor for $\mathtt{cons}$ to $x$ and $t$. We define the functions
$\mathtt{hd}:A^{\omega}\to A$ and $\mathtt{tl}:A^{\omega}\to A^{\omega}$ by

$\begin{array}[]{rcl}\mathtt{hd}(a:t)&=&a\\\ \mathtt{tl}(a:t)&=&t\end{array}$

Specifications of many-sorted signatures may be conveniently given by
coinductively interpreted grammars. For instance, the set $A^{\omega}$ of
streams over a set $A$ could be specified by writing

$A^{\omega}\operatorname{{\,::=\,}}\mathtt{cons}(A,A^{\omega}).$

A more interesting example is that of finite and infinite binary trees with
nodes labelled either with $a$ or $b$, and leaves labelled with one of the
elements of a set $V$:

$T\operatorname{{\,::=\,}}V\parallel a(T,T)\parallel b(T,T).$

As such specifications are not intended to be formal entities but only
convenient notation for describing sets of infinitary terms, we will not
define them precisely. It is always clear what many-sorted signature is meant.

For the sake of brevity we often use ${\mathcal{T}}={\mathcal{T}}(\Sigma)$ and
${\mathcal{T}}_{s}={\mathcal{T}}_{s}(\Sigma)$, i.e., we omit the signature
$\Sigma$ when clear from the context or irrelevant.

The class of _constructor-guarded_ functions is defined inductively as the
class of all functions $h:{\mathcal{T}}_{s}^{m}\to{\mathcal{T}}_{s^{\prime}}$
(for arbitrary $m\in\mathbb{N}$, $s,s^{\prime}\in\Sigma_{s}$) such that there
are a constructor $c$ of type $(s_{1},\ldots,s_{k};s^{\prime})$ and functions
$u_{i}:{\mathcal{T}}_{s}^{m}\to{\mathcal{T}}_{s_{i}}$ ($i=1,\ldots,k$) such
that

$h(y_{1},\ldots,y_{m})=c(u_{1}(y_{1},\ldots,y_{m}),\ldots,u_{k}(y_{1},\ldots,y_{m}))$

for all $y_{1},\ldots,y_{m}\in{\mathcal{T}}_{s}$, and for each $i=1,\ldots,k$
one of the following holds:

  * •

$u_{i}$ is constructor-guarded, or

  * •

$u_{i}$ is a constant function, or

  * •

$u_{i}$ is a projection function, i.e., $s_{i}=s$ and there is $1\leq j\leq m$
with $u_{i}(y_{1},\ldots,y_{m})=y_{j}$ for all
$y_{1},\ldots,y_{m}\in{\mathcal{T}}_{s}$.

Let $S$ be a set. A function
$h:S\times{\mathcal{T}}_{s}^{m}\to{\mathcal{T}}_{s^{\prime}}$ is constructor-
guarded if for every $x\in S$ the function
$h_{x}:{\mathcal{T}}_{s}^{m}\to{\mathcal{T}}_{s^{\prime}}$ defined by
$h_{x}(y_{1},\ldots,y_{m})=h(x,y_{1},\ldots,y_{m})$ is constructor-guarded. A
function $f:S\to{\mathcal{T}}_{s}$ is defined by _guarded corecursion_ from
$h:S\times{\mathcal{T}}_{s}^{m}\to{\mathcal{T}}_{s}$ and $g_{i}:S\to S$
($i=1,\ldots,m$) if $h$ is constructor-guarded and $f$ satisfies

$f(x)=h(x,f(g_{1}(x)),\ldots,f(g_{m}(x)))$

for all $x\in S$.

The following theorem is folklore in the coalgebra community. We sketch an
elementary proof. In fact, each set of many-sorted infinitary terms is a final
coalgebra of an appropriate set-functor. Then Theorem 1 follows from more
general principles. We prefer to avoid coalgebraic terminology, as it is
simply not necessary for the purposes of the present paper. See e.g. [20, 38]
for a more general coalgebraic explanation of corecursion.

######  Theorem 1.

For any constructor-guarded function
$h:S\times{\mathcal{T}}_{s}^{m}\to{\mathcal{T}}_{s}$ and any $g_{i}:S\to S$
($i=1,\ldots,m$), there exists a unique function $f:S\to{\mathcal{T}}_{s}$
defined by guarded corecursion from $h$ and $g_{1},\ldots,g_{m}$.

######  Proof 2.1.

Let $f_{0}:S\to{\mathcal{T}}_{s}$ be an arbitrary function. Define $f_{n+1}$
for $n\in\mathbb{N}$ by
$f_{n+1}(x)=h(x,f_{n}(g_{1}(x)),\ldots,f_{n}(g_{m}(x)))$. Using the fact that
$h$ is constructor-guarded, one shows by induction on $n$ that:

$f_{n+1}(x)(p)=f_{n}(x)(p)$ for $x\in S$ and $p\in\mathbb{N}^{*}$ with $|p|<n$

where $|p|$ denotes the length of $p$. Indeed, the base is obvious. We show
the inductive step. Let $x\in S$. Because $h$ is constructor-guarded, we have
for instance

$f_{n+2}(x)=h(x,f_{n+1}(g_{1}(x)),\ldots,f_{n+1}(g_{m}(x)))=c_{1}(c_{2},c_{3}(w,f_{n+1}(g_{1}(x))))$

Let $p\in\mathbb{N}^{*}$ with $|p|\leq n$. The only interesting case is when
$p=11p^{\prime}$, i.e., when $p$ points inside $f_{n+1}(g_{1}(x))$. But then
$|p^{\prime}|<|p|\leq n$, so by the inductive hypothesis
$f_{n+1}(g_{1}(x))(p^{\prime})=f_{n}(g_{1}(x))(p^{\prime})$. Thus
$f_{n+2}(x)(p)=f_{n+1}(g_{1}(x))(p^{\prime})=f_{n}(g_{1}(x))(p^{\prime})=f_{n+1}(x)(p)$.

Now we define $f:S\to{\mathcal{T}}_{s}$ by

$f(x)(p)=f_{|p|+1}(x)(p)$

for $x\in S$, $p\in\mathbb{N}^{*}$. Using $(\star)$ it is routine to check
that $f(x)$ is a well-defined infinitary term for each $x\in S$. To show that
$f:S\to{\mathcal{T}}_{s}$ is defined by guarded corecursion from $h$ and
$g_{1},\ldots,g_{m}$, using $(\star)$ one shows by induction on the length of
$p\in\mathbb{N}^{*}$ that for any $x\in S$:

$f(x)(p)=h(x,f(g_{1}(x)),\ldots,f(g_{m}(x)))(p).$

To prove that $f$ is unique it suffices to show that it does not depend on
$f_{0}$. For this purpose, using $(\star)$ one shows by induction on the
length of $p\in\mathbb{N}^{*}$ that $f(x)(p)$ does not depend on $f_{0}$ for
any $x\in S$.

We shall often use the above theorem implicitly, just mentioning that some
equations define a function by guarded corecursion.

Consider the equation

$\mathtt{even}(x:y:t)=x:\mathtt{even}(t)$

It may be rewritten as

$\mathtt{even}(t)=\mathtt{hd}(t):\mathtt{even}(\mathtt{tl}(\mathtt{tl}(t)))$

So $\mathtt{even}:A^{\omega}\to A^{\omega}$ is defined by guarded corecursion
from $h:A^{\omega}\times A^{\omega}\to A^{\omega}$ given by

$h(t,t^{\prime})=\mathtt{hd}(t):t^{\prime}$

and $g:A^{\omega}\to A^{\omega}$ given by

$g(t)=\mathtt{tl}(\mathtt{tl}(t))$

By Theorem 1 there is a unique function $\mathtt{even}:A^{\omega}\to
A^{\omega}$ satisfying the original equation.

Another example of a function defined by guarded corecursion is
$\mathtt{zip}:A^{\omega}\times A^{\omega}\to A^{\omega}$:

$\mathtt{zip}(x:t,s)=x:\mathtt{zip}(s,t)$

The following function
$\mathtt{merge}:\mathbb{N}^{\omega}\times\mathbb{N}^{\omega}\to\mathbb{N}^{\omega}$
is also defined by guarded corecursion:

$\mathtt{merge}(x:t_{1},y:t_{2})=\left\\{\begin{array}[]{cl}x:\mathtt{merge}(t_{1},y:t_{2})&\text{
if }x\leq y\\\ y:\mathtt{merge}(x:t_{1},t_{2})&\text{ otherwise
}\end{array}\right.$

##  3\. Coinduction

In this section111This section is largely based on [12, Section 2]. we give a
brief explanation of coinduction as it is used in the present paper. Our
presentation of coinductive proofs is similar to e.g. [19, 8, 37, 34, 31].

There are many ways in which our coinductive proofs could be justified. Since
we formalised our main results (see Section 7), the proofs may be understood
as a paper presentation of formal Coq proofs. They can also be justified by
appealing to one of a number of established coinduction principles. With
enough patience one could, in principle, reformulate all proofs to directly
employ the usual coinduction principle in set theory based on the Knaster-
Tarski fixpoint theorem [39]. One could probably also use the coinduction
principle from [31]. Finally, one may justify our proofs by indicating how to
interpret them in ordinary set theory, which is what we do in this section.

The purpose of this section is to explain how to justify our proofs by
reducing coinduction to transfinite induction. The present section does not
provide a formal coinduction proof principle as such, but only indicates how
one could elaborate the proofs so as to eliminate the use of coinduction.
Naturally, such an elaboration would introduce some tedious details. The point
is that all these details are essentially the same for each coinductive proof.
The advantage of using coinduction is that the details need not be provided
each time. A similar elaboration could be done to directly employ any of a
number of established coinduction principles, but as far as we know
elaborating the proofs in the way explained here requires the least amount of
effort in comparison to reformulating them to directly employ an established
coinduction principle. In fact, we do not wish to explicitly commit to any
single formal proof principle, because we do not think that choosing a
specific principle has an essential impact on the content of our proofs,
except by making it more or less straightforward to translate the proofs into
a form which uses the principle directly.

A reader not satisfied with the level of rigour of the explanations of
coinduction below is referred to our formalisation (see Section 7). The
present section provides one way in which our proofs can be understood and
verified without resorting to a formalisation. To make the observations of
this section completely precise and general one would need to introduce formal
notions of “proof” and “statement”. In other words, one would need to
formulate a system of logic with a capacity for coinductive proofs. We do not
want to do this here, because this paper is about a coinductive confluence
proof for infinitary lambda calculus, not about foundations of coinduction. It
would require some work, but should not be too difficult, to create a formal
system based on the present section in which our coinductive proofs could be
interpreted reasonably directly. We defer this to future work. The status of
the present section is that of a “meta-explanation”, analogous to an
explanation of how, e.g., the informal presentations of inductive
constructions found in the literature may be encoded in ZFC set theory.

Let $T$ be the set of all finite and infinite terms defined coinductively by

$T\operatorname{{\,::=\,}}V\parallel A(T)\parallel B(T,T)$

where $V$ is a countable set of variables, and $A$, $B$ are constructors. By
$x,y,\ldots$ we denote variables, and by $t,s,\ldots$ we denote elements of
$T$. Define a binary relation $\to$ on $T$ coinductively by the following
rules.

$x\to x\quad A(t)\to A(t^{\prime})t\to t^{\prime}\quad B(s,t)\to
B(s^{\prime},t^{\prime})\lx@proof@logical@and s\to s^{\prime}t\to
t^{\prime}\quad A(t)\to B(t^{\prime},t^{\prime})t\to t^{\prime}$

Formally, the relation ${\to}$ is the greatest fixpoint of a monotone function

$F:\mathcal{P}(T\times T)\to\mathcal{P}(T\times T)$

defined by

$F(R)=\left\\{\langle t_{1},t_{2}\rangle\mid\exists_{x\in V}(t_{1}\equiv
t_{2}\equiv x)\lor\exists_{t,t^{\prime}\in T}(t_{1}\equiv A(t)\land
t_{2}\equiv A(t^{\prime})\land R(t,t^{\prime}))\lor\ldots\right\\}.$

Alternatively, using the Knaster-Tarski fixpoint theorem, the relation $\to$
may be characterised as the greatest binary relation on $T$ (i.e. the greatest
subset of $T\times T$ w.r.t. set inclusion) such that ${\to}\subseteq
F({\to})$, i.e., such that for every $t_{1},t_{2}\in T$ with $t_{1}\to t_{2}$
one of the following holds:

  1. (1)

$t_{1}\equiv t_{2}\equiv x$ for some variable $x\in V$,

  2. (2)

$t_{1}\equiv A(t)$, $t_{2}\equiv A(t^{\prime})$ with $t\to t^{\prime}$,

  3. (3)

$t_{1}\equiv B(s,t)$, $t_{2}\equiv B(s^{\prime},t^{\prime})$ with $s\to
s^{\prime}$ and $t\to t^{\prime}$,

  4. (4)

$t_{1}\equiv A(t)$, $t_{2}\equiv B(t^{\prime},t^{\prime})$ with $t\to
t^{\prime}$.

Yet another way to think about $\to$ is that $t_{1}\to t_{2}$ holds if and
only if there exists a _potentially infinite_ derivation tree of $t_{1}\to
t_{2}$ built using the rules $(1)-(4)$.

The rules $(1)-(4)$ could also be interpreted inductively to yield the least
fixpoint of $F$. This is the conventional interpretation, and it is indicated
with a single line in each rule separating premises from the conclusion. A
coinductive interpretation is indicated with double lines.

The greatest fixpoint $\to$ of $F$ may be obtained by transfinitely iterating
$F$ starting with $T\times T$. More precisely, define an ordinal-indexed
sequence $(\to^{\gamma})_{\gamma}$ by:

  * •

$\to^{0}=T\times T$,

  * •

$\to^{\gamma+1}=F(\to^{\gamma})$,

  * •

$\to^{\delta}=\bigcap_{\gamma<\delta}\to^{\gamma}$ for a limit ordinal
$\delta$.

Then there exists an ordinal $\zeta$ such that ${\to}={\to^{\zeta}}$. The
least such ordinal is called the _closure ordinal_. Note also that
${\to^{\gamma}}\subseteq{\to^{\delta}}$ for $\gamma\geq\delta$ (we often use
this fact implicitly). See e.g. [14, Chapter 8]. The relation $\to^{\gamma}$
is called the _$\gamma$ -approximant_. Note that the $\gamma$-approximants
depend on a particular definition of $\to$ (i.e. on the function $F$), not
solely on the relation $\to$ itself. We use $R^{\gamma}$ for the
$\gamma$-approximant of a relation $R$.

It is instructive to note that the coinductive rules for $\to$ may also be
interpreted as giving rules for the $\gamma+1$-approximants, for any ordinal
$\gamma$.

$x\to^{\gamma+1}x\quad
A(t)\to^{\gamma+1}A(t^{\prime})t\to^{\gamma}t^{\prime}\quad
B(s,t)\to^{\gamma+1}B(s^{\prime},t^{\prime})\lx@proof@logical@and
s\to^{\gamma}s^{\prime}t\to^{\gamma}t^{\prime}\quad
A(t)\to^{\gamma+1}B(t^{\prime},t^{\prime})t\to^{\gamma}t^{\prime}$

Usually, the closure ordinal for the definition of a coinductive relation is
$\omega$, as is the case with all coinductive definitions appearing in this
paper. In general, however, it is not difficult to come up with a coinductive
definition whose closure ordinal is greater than $\omega$. For instance,
consider the relation $R\subseteq\mathbb{N}\cup\\{\infty\\}$ defined
coinductively by the following two rules.

$R(n+1)\lx@proof@logical@and R(n)n\in\mathbb{N}\quad\quad R(\infty)\exists
n\in\mathbb{N}.R(n)$

We have $R=\emptyset$, $R^{n}=\\{m\in\mathbb{N}\mid m\geq
n\\}\cup\\{\infty\\}$ for $n\in\mathbb{N}$, $R^{\omega}=\\{\infty\\}$, and
only $R^{\omega+1}=\emptyset$. Thus the closure ordinal of this definition is
$\omega+1$.

In this paper we are interested in proving by coinduction statements of the
form $\psi(R_{1},\ldots,R_{m})$ where

$\psi(X_{1},\ldots,X_{m})\equiv\forall x_{1}\ldots x_{n}.\varphi(\vec{x})\to
X_{1}(g_{1}(\vec{x}),\ldots,g_{k}(\vec{x}))\land\ldots\land
X_{m}(g_{1}(\vec{x}),\ldots,g_{k}(\vec{x})).$

and $R_{1},\ldots,R_{m}$ are coinductive relations on $T$, i.e, relations
defined as the greatest fixpoints of some monotone functions on the powerset
of an appropriate cartesian product of $T$, and $\psi(R_{1},\ldots,R_{m})$ is
$\psi(X_{1},\ldots,X_{m})$ with $R_{i}$ substituted for $X_{i}$. Statements
with an existential quantifier may be reduced to statements of this form by
skolemising, as explained in Example 3 below.

Here $X_{1},\ldots,X_{m}$ are meta-variables for which relations on $T$ may be
substituted. In the statement $\varphi(\vec{x})$ only $x_{1},\ldots,x_{n}$
occur free. The meta-variables $X_{1},\ldots,X_{m}$ _are not allowed to occur_
in $\varphi(\vec{x})$. In general, we abbreviate $x_{1},\ldots,x_{n}$ with
$\vec{x}$. The symbols $g_{1},\ldots,g_{k}$ denote some functions of
$\vec{x}$.

To prove $\psi(R_{1},\ldots,R_{m})$ it suffices to show by transfinite
induction that $\psi(R_{1}^{\gamma},\ldots,R_{m}^{\gamma})$ holds for each
ordinal $\gamma\leq\zeta$, where $R_{i}^{\gamma}$ is the $\gamma$-approximant
of $R_{i}$. It is an easy exercise to check that because of the special form
of $\psi$ (in particular because $\varphi$ does not contain
$X_{1},\ldots,X_{m}$) and the fact that each $R_{i}^{0}$ is the full relation,
the base case $\gamma=0$ and the case of $\gamma$ a limit ordinal hold. They
hold for _any_ $\psi$ of the above form, _irrespective_ of
$\varphi,R_{1},\ldots,R_{m}$. Note that $\varphi(\vec{x})$ is the same in all
$\psi(R_{1}^{\gamma},\ldots,R_{m}^{\gamma})$ for any $\gamma$, i.e., it does
not refer to the $\gamma$-approximants or the ordinal $\gamma$. Hence it
remains to show the inductive step for $\gamma$ a successor ordinal. It turns
out that a coinductive proof of $\psi$ may be interpreted as a proof of this
inductive step for a successor ordinal, with the ordinals left implicit and
the phrase “coinductive hypothesis” used instead of “inductive hypothesis”.

On terms from $T$ (see Example 3) we define the operation of substitution by
guarded corecursion.

$\begin{array}[]{rclcrcl}y[t/x]&=&y\quad\text{ if }x\neq
y&&(A(s))[t/x]&=&A(s[t/x])\\\
x[t/x]&=&t&&(B(s_{1},s_{2}))[t/x]&=&B(s_{1}[t/x],s_{2}[t/x])\end{array}$

We show by coinduction: if $s\to s^{\prime}$ and $t\to t^{\prime}$ then
$s[t/x]\to s^{\prime}[t^{\prime}/x]$, where $\to$ is the relation from Example
3. Formally, the statement we show by transfinite induction on
$\gamma\leq\zeta$ is: for $s,s^{\prime},t,t^{\prime}\in T$, if $s\to
s^{\prime}$ and $t\to t^{\prime}$ then
$s[t/x]\to^{\gamma}s^{\prime}[t^{\prime}/x]$. For illustrative purposes, we
indicate the $\gamma$-approximants with appropriate ordinal superscripts, but
it is customary to omit these superscripts.

Let us proceed with the proof. The proof is by coinduction with case analysis
on $s\to s^{\prime}$. If $s\equiv s^{\prime}\equiv y$ with $y\neq x$, then
$s[t/x]\equiv y\equiv s^{\prime}[t^{\prime}/x]$. If $s\equiv s^{\prime}\equiv
x$ then $s[t/x]\equiv t\to^{\gamma+1}t^{\prime}\equiv
s^{\prime}[t^{\prime}/x]$ (note that
${\to}\equiv{\to^{\zeta}}\subseteq{\to^{\gamma+1}}$). If $s\equiv A(s_{1})$,
$s^{\prime}\equiv A(s_{1}^{\prime})$ and $s_{1}\to s_{1}^{\prime}$, then
$s_{1}[t/x]\to^{\gamma}s_{1}^{\prime}[t^{\prime}/x]$ by the coinductive
hypothesis. Thus $s[t/x]\equiv
A(s_{1}[t/x])\to^{\gamma+1}A(s_{1}^{\prime}[t^{\prime}/x])\equiv
s^{\prime}[t^{\prime}/x]$ by rule $(2)$. If $s\equiv B(s_{1},s_{2})$,
$s^{\prime}\equiv B(s_{1}^{\prime},s_{2}^{\prime})$ then the proof is
analogous. If $s\equiv A(s_{1})$, $s^{\prime}\equiv
B(s_{1}^{\prime},s_{1}^{\prime})$ and $s_{1}\to s_{1}^{\prime}$, then the
proof is also similar. Indeed, by the coinductive hypothesis we have
$s_{1}[t/x]\to^{\gamma}s_{1}^{\prime}[t^{\prime}/x]$, so $s[t/x]\equiv
A(s_{1}[t/x])\to^{\gamma+1}B(s_{1}^{\prime}[t^{\prime}/x],s_{1}^{\prime}[t^{\prime}/x])\equiv
s^{\prime}[t^{\prime}/x]$ by rule $(4)$.

With the following example we explain how our proofs of existential statements
should be interpreted.

Let $T$ and $\to$ be as in Example 3. We want to show: for all
$s,t,t^{\prime}\in T$, if $s\to t$ and $s\to t^{\prime}$ then there exists
$s^{\prime}\in T$ with $t\to s^{\prime}$ and $t^{\prime}\to s^{\prime}$. The
idea is to skolemise this statement. So we need to find a Skolem function
$f:T^{3}\to T$ which will allow us to prove the Skolem normal form:

if $s\to t$ and $s\to t^{\prime}$ then $t\to f(s,t,t^{\prime})$ and
$t^{\prime}\to f(s,t,t^{\prime})$.

The rules for $\to$ suggest a definition of $f$:

$\begin{array}[]{rcl}f(x,x,x)&=&x\\\
f(A(s),A(t),A(t^{\prime}))&=&A(f(s,t,t^{\prime}))\\\
f(A(s),A(t),B(t^{\prime},t^{\prime}))&=&B(f(s,t,t^{\prime}),f(s,t,t^{\prime}))\\\
f(A(s),B(t,t),A(t^{\prime}))&=&B(f(s,t,t^{\prime}),f(s,t,t^{\prime}))\\\
f(A(s),B(t,t),B(t^{\prime},t^{\prime}))&=&B(f(s,t,t^{\prime}),f(s,t,t^{\prime}))\\\
f(B(s_{1},s_{2}),B(t_{1},t_{2}),B(t_{1}^{\prime},t_{2}^{\prime}))&=&B(f(s_{1},t_{1},t_{1}^{\prime}),f(s_{2},t_{2},t_{2}^{\prime}))\\\
f(s,t,t^{\prime})&=&\text{some fixed term if none of the above
matches}\end{array}$

This is a definition by guarded corecursion, so there exists a unique function
$f:T^{3}\to T$ satisfying the above equations. The last case in the above
definition of $f$ corresponds to the case in Definition 2 where all $u_{i}$
are constant functions. Note that any fixed term has a fixed constructor (in
the sense of Definition 2) at the root. In the sense of Definition 2 also the
elements of $V$ are nullary constructors.

We now proceed with a coinductive proof of $(\star)$. Assume $s\to t$ and
$s\to t^{\prime}$. If $s\equiv t\equiv t^{\prime}\equiv x$ then
$f(s,t,t^{\prime})\equiv x$, and $x\to x$ by rule $(1)$. If $s\equiv
A(s_{1})$, $t\equiv A(t_{1})$ and $t^{\prime}\equiv A(t_{1}^{\prime})$ with
$s_{1}\to t_{1}$ and $s_{1}\to t_{1}^{\prime}$, then by the coinductive
hypothesis $t_{1}\to f(s_{1},t_{1},t_{1}^{\prime})$ and $t_{1}^{\prime}\to
f(s_{1},t_{1},t_{1}^{\prime})$. We have $f(s,t,t^{\prime})\equiv
A(f(s_{1},t_{1},t_{1}^{\prime}))$. Hence $t\equiv A(t_{1})\to
f(s,t,t^{\prime})$ and $t\equiv A(t_{1}^{\prime})\to f(s,t,t^{\prime})$, by
rule $(2)$. If $s\equiv B(s_{1},s_{2})$, $t\equiv B(t_{1},t_{2})$ and
$t^{\prime}\equiv B(t_{1}^{\prime},t_{2}^{\prime})$, with $s_{1}\to t_{1}$,
$s_{1}\to t_{1}^{\prime}$, $s_{2}\to t_{2}$ and $s_{2}\to t_{2}^{\prime}$,
then by the coinductive hypothesis we have $t_{1}\to
f(s_{1},t_{1},t_{1}^{\prime})$, $t_{1}^{\prime}\to
f(s_{1},t_{1},t_{1}^{\prime})$, $t_{2}\to f(s_{2},t_{2},t_{2}^{\prime})$ and
$t_{2}^{\prime}\to f(s_{2},t_{2},t_{2}^{\prime})$. Hence $t\equiv
B(t_{1},t_{2})\to
B(f(s_{1},t_{1},t_{1}^{\prime}),f(s_{2},t_{2},t_{2}^{\prime}))\equiv
f(s,t,t^{\prime})$ by rule $(3)$. Analogously, $t^{\prime}\to
f(s,t,t^{\prime})$ by rule $(3)$. Other cases are similar.

Usually, it is inconvenient to invent the Skolem function beforehand, because
the definition of the Skolem function and the coinductive proof of the Skolem
normal form are typically interdependent. Therefore, we adopt an informal
style of doing a proof by coinduction of a statement

$\begin{array}[]{rcl}\psi(R_{1},\ldots,R_{m})&=&\forall_{x_{1},\ldots,x_{n}\in
T}\,.\,\varphi(\vec{x})\to\\\ &&\quad\exists_{y\in
T}.R_{1}(g_{1}(\vec{x}),\ldots,g_{k}(\vec{x}),y)\land\ldots\land
R_{m}(g_{1}(\vec{x}),\ldots,g_{k}(\vec{x}),y)\end{array}$

with an existential quantifier. We intertwine the corecursive definition of
the Skolem function $f$ with a coinductive proof of the Skolem normal form

$\begin{array}[]{l}\forall_{x_{1},\ldots,x_{n}\in
T}\,.\,\varphi(\vec{x})\to\\\ \quad\quad
R_{1}(g_{1}(\vec{x}),\ldots,g_{k}(\vec{x}),f(\vec{x}))\land\ldots\land
R_{m}(g_{1}(\vec{x}),\ldots,g_{k}(\vec{x}),f(\vec{x}))\end{array}$

We proceed as if the coinductive hypothesis was
$\psi(R_{1}^{\gamma},\ldots,R_{m}^{\gamma})$ (it really is the Skolem normal
form). Each element obtained from the existential quantifier in the
coinductive hypothesis is interpreted as a corecursive invocation of the
Skolem function. When later we exhibit an element to show the existential
subformula of $\psi(R_{1}^{\gamma+1},\ldots,R_{m}^{\gamma+1})$, we interpret
this as the definition of the Skolem function in the case specified by the
assumptions currently active in the proof. Note that this exhibited element
may (or may not) depend on some elements obtained from the existential
quantifier in the coinductive hypothesis, i.e., the definition of the Skolem
function may involve corecursive invocations.

To illustrate our style of doing coinductive proofs of statements with an
existential quantifier, we redo the proof done above. For illustrative
purposes, we indicate the arguments of the Skolem function, i.e., we write
$s^{\prime}_{s,t,t^{\prime}}$ in place of $f(s,t,t^{\prime})$. These
subscripts $s,t,t^{\prime}$ are normally omitted.

We show by coinduction that if $s\to t$ and $s\to t^{\prime}$ then there
exists $s^{\prime}\in T$ with $t\to s^{\prime}$ and $t^{\prime}\to
s^{\prime}$. Assume $s\to t$ and $s\to t^{\prime}$. If $s\equiv t\equiv
t^{\prime}\equiv x$ then take $s^{\prime}_{x,x,x}\equiv x$. If $s\equiv
A(s_{1})$, $t\equiv A(t_{1})$ and $t^{\prime}\equiv A(t_{1}^{\prime})$ with
$s_{1}\to t_{1}$ and $s_{1}\to t_{1}^{\prime}$, then by the coinductive
hypothesis we obtain $s^{\prime}_{s_{1},t_{1},t_{1}^{\prime}}$ with $t_{1}\to
s^{\prime}_{s_{1},t_{1},t_{1}^{\prime}}$ and $t_{1}^{\prime}\to
s^{\prime}_{s_{1},t_{1},t_{1}^{\prime}}$. More precisely: by corecursively
applying the Skolem function to $s_{1},t_{1},t_{1}^{\prime}$ we obtain
$s^{\prime}_{s_{1},t_{1},t_{1}^{\prime}}$, and by the coinductive hypothesis
we have $t_{1}\to s^{\prime}_{s_{1},t_{1},t_{1}^{\prime}}$ and
$t_{1}^{\prime}\to s^{\prime}_{s_{1},t_{1},t_{1}^{\prime}}$. Hence $t\equiv
A(t_{1})\to A(s^{\prime}_{s_{1},t_{1},t_{1}^{\prime}})$ and $t\equiv
A(t_{1}^{\prime})\to A(s^{\prime}_{s_{1},t_{1},t_{1}^{\prime}})$, by rule
$(2)$. Thus we may take $s^{\prime}_{s,t,t^{\prime}}\equiv
A(s^{\prime}_{s_{1},t_{1},t_{1}^{\prime}})$. If $s\equiv B(s_{1},s_{2})$,
$t\equiv B(t_{1},t_{2})$ and $t^{\prime}\equiv
B(t_{1}^{\prime},t_{2}^{\prime})$, with $s_{1}\to t_{1}$, $s_{1}\to
t_{1}^{\prime}$, $s_{2}\to t_{2}$ and $s_{2}\to t_{2}^{\prime}$, then by the
coinductive hypothesis we obtain $s^{\prime}_{s_{1},t_{1},t_{1}^{\prime}}$ and
$s^{\prime}_{s_{2},t_{2},t_{2}^{\prime}}$ with $t_{1}\to
s^{\prime}_{s_{1},t_{1},t_{1}^{\prime}}$, $t_{1}^{\prime}\to
s^{\prime}_{s_{1},t_{1},t_{1}^{\prime}}$, $t_{2}\to
s^{\prime}_{s_{2},t_{2},t_{2}^{\prime}}$ and $t_{2}^{\prime}\to
s^{\prime}_{s_{2},t_{2},t_{2}^{\prime}}$. Hence $t\equiv B(t_{1},t_{2})\to
B(s^{\prime}_{s_{1},t_{1},t_{1}^{\prime}},s^{\prime}_{s_{2},t_{2},t_{2}^{\prime}})$
by rule $(3)$. Analogously, $t^{\prime}\to
B(s^{\prime}_{s_{1},t_{1},t_{1}^{\prime}},s^{\prime}_{s_{2},t_{2},t_{2}^{\prime}})$
by rule $(3)$. Thus we may take $s^{\prime}_{s,t,t^{\prime}}\equiv
B(s^{\prime}_{s_{1},t_{1},t_{1}^{\prime}},s^{\prime}_{s_{2},t_{2},t_{2}^{\prime}})$.
Other cases are similar.

It is clear that the above informal proof, when interpreted in the way
outlined before, implicitly defines the Skolem function $f$. It should be kept
in mind that in every case the definition of the Skolem function needs to be
guarded. We do not explicitly mention this each time, but verifying this is
part of verifying the proof.

When doing proofs by coinduction the following criteria need to be kept in
mind in order to be able to justify the proofs according to the above
explanations.

  * •

When we conclude from the coinductive hypothesis that some relation
$R(t_{1},\ldots,t_{n})$ holds, this really means that only its approximant
$R^{\gamma}(t_{1},\ldots,t_{n})$ holds. Usually, we need to infer that the
next approximant $R^{\gamma+1}(s_{1},\ldots,s_{n})$ holds (for some other
elements $s_{1},\ldots,s_{n}$) by using $R^{\gamma}(t_{1},\ldots,t_{n})$ as a
premise of an appropriate rule. But we cannot, e.g., inspect (do case
reasoning on) $R^{\gamma}(t_{1},\ldots,t_{n})$, use it in any lemmas, or
otherwise treat it as $R(t_{1},\ldots,t_{n})$.

  * •

An element $e$ obtained from an existential quantifier in the coinductive
hypothesis is not really the element itself, but a corecursive invocation of
the implicit Skolem function. Usually, we need to put it inside some
constructor $c$, e.g. producing $c(e)$, and then exhibit $c(e)$ in the proof
of an existential statement. Applying at least one constructor to $e$ is
necessary to ensure guardedness of the implicit Skolem function. But we
cannot, e.g., inspect $e$, apply some previously defined functions to it, or
otherwise treat it as if it was really given to us.

  * •

In the proofs of existential statements, the implicit Skolem function cannot
depend on the ordinal $\gamma$. However, this is the case as long as we do not
violate the first point, because if the ordinals are never mentioned and we do
not inspect the approximants obtained from the coinductive hypothesis, then
there is no way in which we could possibly introduce a dependency on $\gamma$.

Equality on infinitary terms may be characterised coinductively.

Let $\Sigma$ be a many-sorted algebraic signature, as in Definition 2. Let
${\mathcal{T}}={\mathcal{T}}(\Sigma)$. Define on ${\mathcal{T}}$ a binary
relation ${=}$ of _bisimilarity_ by the coinductive rules

$f(t_{1},\ldots,t_{n})=f(s_{1},\ldots,s_{n})\lx@proof@logical@and
t_{1}=s_{1}\ldots t_{n}=s_{n}$

for each constructor $f\in\Sigma_{c}$.

It is intuitively obvious that on infinitary terms bisimilary is the same as
identity. The following easy (and well-known) proposition makes this precise.

######  Proposition 2.

For $t,s\in{\mathcal{T}}$ we have: $t=s$ iff $t\equiv s$.

######  Proof 3.1.

Recall that each term is formally a partial function from $\mathbb{N}^{*}$ to
$\Sigma_{c}$. We write $t(p)\approx s(p)$ if either both $t(p),s(p)$ are
defined and equal, or both are undefined.

Assume $t=s$. It suffices to show by induction of the length of
$p\in\mathbb{N}^{*}$ that ${t}_{|p}={s}_{|p}$ or
$t(p){\uparrow},s(p){\uparrow}$, where by ${t}_{|p}$ we denote the subterm of
$t$ at position $p$. For $p=\epsilon$ this is obvious. Assume $p=p^{\prime}j$.
By the inductive hypothesis, ${t}_{|p^{\prime}}={s}_{|p^{\prime}}$ or
$t(p^{\prime}){\uparrow},s(p^{\prime}){\uparrow}$. If
${t}_{|p^{\prime}}={s}_{|p^{\prime}}$ then ${t}_{|p^{\prime}}\equiv
f(t_{0},\ldots,t_{n})$ and ${s}_{|p^{\prime}}\equiv f(s_{0},\ldots,s_{n})$ for
some $f\in\Sigma_{c}$ with $t_{i}=s_{i}$ for $i=0,\ldots,n$. If $0\leq j\leq
n$ then ${t}_{|p}\equiv t_{j}=s_{j}={s}_{|p}$. Otherwise, if $j>n$ or if
$t(p^{\prime}){\uparrow},s(p^{\prime}){\uparrow}$, then
$t(p){\uparrow},s(p){\uparrow}$ by the definition of infinitary terms.

For the other direction, we show by coinduction that for any
$t\in{\mathcal{T}}$ we have $t=t$. If $t\in{\mathcal{T}}$ then $t\equiv
f(t_{1},\ldots,t_{n})$ for some $f\in\Sigma_{c}$. By the coinductive
hypothesis we obtain $t_{i}=t_{i}$ for $i=1,\ldots,n$. Hence $t=t$ by the rule
for $f$.

For infinitary terms $t,s\in{\mathcal{T}}$, we shall therefore use the
notations $t=s$ and $t\equiv s$ interchangeably, employing Proposition 2
implicitly. In particular, the above coinductive characterisation of term
equality is used implicitly in the proof of Lemma 35.

Recall the coinductive definitions of $\mathtt{zip}$ and $\mathtt{even}$ from
Example 2.

$\begin{array}[]{rcl}\mathtt{even}(x:y:t)&=&x:\mathtt{even}(t)\\\
\mathtt{zip}(x:t,s)&=&x:\mathtt{zip}(s,t)\end{array}$

By coinduction we show

$\mathtt{zip}(\mathtt{even}(t),\mathtt{even}(\mathtt{tl}(t)))=t$

for any stream $t\in A^{\omega}$. Let $t\in A^{\omega}$. Then $t=x:y:s$ for
some $x,y\in A$ and $s\in A^{\omega}$. We have

$\begin{array}[]{rcl}\mathtt{zip}(\mathtt{even}(t),\mathtt{even}(\mathtt{tl}(t)))&=&\mathtt{zip}(\mathtt{even}(x:y:s),\mathtt{even}(y:s))\\\
&=&\mathtt{zip}(x:\mathtt{even}(s),\mathtt{even}(y:s))\\\
&=&x:\mathtt{zip}(\mathtt{even}(y:s),\mathtt{even}(s))\\\ &=&x:y:s\quad\text{
(by~{}CH) }\\\ &=&t\end{array}$

In the equality marked with (by CH) we use the coinductive hypothesis, and
implicitly a bisimilarity rule from Definition 3.

The above explanation of coinduction is generalised and elaborated in much
more detail in [11]. Also [31] may be helpful as it gives many examples of
coinductive proofs written in a style similar to the one used here. The book
[39] is an elementary introduction to coinduction and bisimulation (but the
proofs there are presented in a different way than here, not referring to the
coinductive hypothesis but explicitly constructing a backward-closed set). The
chapters [7, 9] explain coinduction in Coq from a practical viewpoint. A
reader interested in foundational matters should also consult [20, 38] which
deal with the coalgebraic approach to coinduction.

In the rest of this paper we shall freely use coinduction, giving routine
coinductive proofs in as much (or as little) detail as it is customary with
inductive proofs of analogous difficulty.

##  4\. Definitions and basic properties

In this section we define infinitary lambda terms and the various notions of
infinitary reductions.

The set of _infinitary lambda terms_ is defined coinductively:

$\begin{array}[]{rcl}\Lambda^{\infty}&::=&C\parallel
V\parallel\Lambda^{\infty}\Lambda^{\infty}\parallel\lambda
V.\Lambda^{\infty}\end{array}$

where $V$ is an infinite set of _variables_ and $C$ is a set of _constants_
such that $V\cap C=\emptyset$. An _atom_ is a variable or a constant. We use
the symbols $x,y,z,\ldots$ for variables, and $c,c^{\prime},c_{1},\ldots$ for
constants, and $a,a^{\prime},a_{1},\ldots$ for atoms, and $t,s,\ldots$ for
terms. By $\mathrm{FV}(t)$ we denote the set of variables occurring free in
$t$. Formally, $\mathrm{FV}(t)$ could be defined using coinduction.

We define substitution by guarded corecursion.

$\begin{array}[]{rcl}x[t/x]&=&t\\\ a[t/x]&=&a\quad\text{if }a\neq x\\\
(t_{1}t_{2})[t/x]&=&(t_{1}[t/x])(t_{2}[t/x])\\\ (\lambda y.s)[t/x]&=&\lambda
y.s[t/x]\quad\text{if }y\notin\mathrm{FV}(t,x)\end{array}$

In our formalisation we use a de Bruijn representation of infinitary lambda
terms, defined analogously to the de Bruijn representation of finite lambda
terms [15]. Hence, infinitary lambda terms here may be understood as a human-
readable presentation of infinitary lambda terms based on de Bruijn indices.
Strictly speaking, also the definition of substitution above is not completely
precise, because it implicitly treats lambda terms up to renaming of bound
variables and we have not given a precise definition of free variables. The
definition of substitution can be understood as a human-readable presentation
of substitution defined on infinitary lambda terms based on de Bruijn indices.

Infinitary lambda terms could be precisely defined as the $\alpha$-equivalence
classes of the terms given in Definition 4, with a coinductively defined
$\alpha$-equivalence relation $=_{\alpha}$. Such a definition involves some
technical issues. If the set of variables $V$ is countable, then it may be
impossible to choose a “fresh” variable $x\notin\mathrm{FV}(t)$ for a term
$t\in\Lambda^{\infty}$, because $t$ may contain all variables free. This
presents a difficulty when trying to precisely define substitution. See also
[32, 33]. There are two ways of resolving this situation:

  1. (1)

assume that $V$ is uncountable,

  2. (2)

consider only terms with finitely many free variables.

Assuming that a fresh variable may always be chosen, one may precisely define
substitution and use coinductive techniques to prove: if
$t=_{\alpha}t^{\prime}$ and $s=_{\alpha}s^{\prime}$ then
$s[t/x]=_{\alpha}s^{\prime}[t^{\prime}/x]$. This implies that substitution
lifts to a function on the $\alpha$-equivalence classes, which is also
trivially true for application and abstraction. Therefore, all functions
defined by guarded corecursion using only the operations of substitution,
application and abstraction lift to functions on $\alpha$-equivalence classes
(provided the same defining equation is used for all terms within the same
$\alpha$-equivalence class). This justifies the use of Barendregt’s variable
convention [5, 2.1.13] (under the assumption that we may always choose a fresh
variable).

Since our formalisation is based on de Bruijn indices, we omit explicit
treatment of $\alpha$-equivalence in this paper.

We also mention that another principled and precise way of dealing with the
renaming of bound variables is to define the set of infinitary lambda terms as
the final coalgebra of an appropriate functor in the category of nominal sets
[32, 33].

Let $R\subseteq\Lambda^{\infty}\times\Lambda^{\infty}$ be a binary relation on
infinitary lambda terms. The _compatible closure_ of $R$, denoted $\to_{R}$,
is defined inductively by the following rules.

$\begin{array}[]{cccc}s\to_{R}t\langle s,t\rangle\in R&\quad
st\to_{R}s^{\prime}ts\to_{R}s^{\prime}&\quad
st\to_{R}st^{\prime}t\to_{R}t^{\prime}&\quad\lambda x.s\to_{R}\lambda
x.s^{\prime}s\to_{R}s^{\prime}\end{array}$

If $\langle t,s\rangle\in R$ then $t$ is an _$R$ -redex_. A term
$t\in\Lambda^{\infty}$ is in _$R$ -normal form_ if there is no
$s\in\Lambda^{\infty}$ with $t\to_{R}s$, or equivalently if it contains no
$R$-redexes. The _parallel closure_ of $R$, usually denoted $\Rightarrow_{R}$,
is defined coinductively by the following rules.

$\begin{array}[]{cccc}s\Rightarrow_{R}t\langle s,t\rangle\in
R&~{}a\Rightarrow_{R}a&~{}s_{1}s_{2}\Rightarrow_{R}t_{1}t_{2}\lx@proof@logical@and
s_{1}\Rightarrow_{R}t_{1}s_{2}\Rightarrow_{R}t_{2}&~{}\lambda
x.s\Rightarrow_{R}\lambda x.s^{\prime}s\Rightarrow_{R}s^{\prime}\end{array}$

Let ${\to}\subseteq\Lambda^{\infty}\times\Lambda^{\infty}$. By $\to^{*}$ we
denote the transitive-reflexive closure of $\to$, and by $\to^{\equiv}$ the
reflexive closure of $\to$. The _infinitary closure_ of $\to$, denoted
$\to^{\infty}$, is defined coinductively by the following rules.

$\begin{array}[]{ccc}s\to^{\infty}as\to^{*}a&\quad
s\to^{\infty}t_{1}^{\prime}t_{2}^{\prime}\lx@proof@logical@and
s\to^{*}t_{1}t_{2}t_{1}\to^{\infty}t_{1}^{\prime}t_{2}\to^{\infty}t_{2}^{\prime}&\quad
s\to^{\infty}\lambda x.r^{\prime}\lx@proof@logical@and s\to^{*}\lambda
x.rr\to^{\infty}r^{\prime}\end{array}$

Let $R_{\beta}=\\{\langle(\lambda x.s)t,s[t/x]\rangle\mid
t,s\in\Lambda^{\infty}\\}$. The relation $\to_{\beta}$ of _one-step
$\beta$-reduction_ is defined as the compatible closure of $R_{\beta}$. The
relation $\to^{*}_{\beta}$ of _$\beta$ -reduction_ is the transitive-reflexive
closure of $\to_{\beta}$. The relation $\to^{\infty}_{\beta}$ of _infinitary
$\beta$-reduction_ is defined as the infinitary closure of $\to_{\beta}$. This
gives the same coinductive definition of infinitary $\beta$-reduction as in
[19].

The relation $\to_{w}$ of _one-step weak head reduction_ is defined
inductively by the following rules.

$\begin{array}[]{cc}(\lambda x.s)t\to_{w}s[t/x]&\quad
st\to_{w}s^{\prime}ts\to_{w}s^{\prime}\end{array}$

The relations $\to^{*}_{w}$, $\to_{w}^{\equiv}$ and $\to^{\infty}_{w}$ are
defined accordingly. In a term $(\lambda x.s)tt_{1}\ldots t_{m}$ the subterm
$(\lambda x.s)t$ is the _weak head redex_. So $\to_{w}$ may contract only the
weak head redex.

Let $\bot$ be a distinguished constant. A $\Lambda^{\infty}$-term $t$ is in
_root normal form_ (rnf) if:

  * •

$t\equiv a$ with $a\not\equiv\bot$, or

  * •

$t\equiv\lambda x.t^{\prime}$, or

  * •

$t\equiv t_{1}t_{2}$ and there is no $s$ with
$t_{1}\to^{\infty}_{\beta}\lambda x.s$ (equivalently, there is no $s$ with
$t_{1}\to^{*}_{\beta}\lambda x.s$).

In other words, a term $t$ is in rnf if $t\not\equiv\bot$ and $t$ does not
infinitarily $\beta$-reduce to a $\beta$-redex. We say that $t$ _has rnf_ if
$t\to^{\infty}_{\beta}t^{\prime}$ for some $t^{\prime}$ in rnf. In particular,
$\bot$ has no rnf. A term with no rnf is also called _root-active_. By
${\mathcal{R}}$ we denote the set of all root-active terms.

A set ${\mathcal{U}}\subseteq\Lambda^{\infty}$ is a set of _meaningless terms_
(see [22]) if it satisfies the following axioms.

  * •

Closure: if $t\in{\mathcal{U}}$ and $t\to^{\infty}_{\beta}s$ then
$s\in{\mathcal{U}}$.

  * •

Substitution: if $t\in{\mathcal{U}}$ then $t[s/x]\in{\mathcal{U}}$ for any
term $s$.

  * •

Overlap: if $\lambda x.s\in{\mathcal{U}}$ then $(\lambda
x.s)t\in{\mathcal{U}}$.

  * •

Root-activeness: ${\mathcal{R}}\subseteq{\mathcal{U}}$.

  * •

Indiscernibility: if $t\in{\mathcal{U}}$ and $t\sim_{\mathcal{U}}s$ then
$s\in{\mathcal{U}}$, where $\sim_{\mathcal{U}}$ is the parallel closure of
${\mathcal{U}}\times{\mathcal{U}}$.

A set ${\mathcal{U}}$ of meaningless terms is a set of _strongly meaningless
terms_ if it additionally satisfies the following expansion axiom.

  * •

Expansion: if $t\in{\mathcal{U}}$ and $s\to^{\infty}_{\beta}t$ then
$s\in{\mathcal{U}}$.

Let ${\mathcal{U}}\subseteq\Lambda^{\infty}$. Let
$R_{\bot_{\mathcal{U}}}=\\{\langle t,\bot\rangle\mid t\in{\mathcal{U}}\text{
and }t\not\equiv\bot\\}$. We define the relation
$\to_{\beta\bot_{\mathcal{U}}}$ of _one-step
$\beta\bot_{\mathcal{U}}$-reduction_ as the compatible closure of
$R_{\beta\bot_{\mathcal{U}}}=R_{\beta}\cup R_{\bot_{\mathcal{U}}}$. A term $t$
is in _$\beta\bot_{\mathcal{U}}$ -normal form_ if it is in
$R_{\beta\bot_{\mathcal{U}}}$-normal form. The relation
$\to^{*}_{\beta\bot_{\mathcal{U}}}$ of _$\beta\bot_{\mathcal{U}}$ -reduction_
is the transitive-reflexive closure of $\to_{\beta\bot_{\mathcal{U}}}$. The
relation $\to^{\infty}_{\beta\bot_{\mathcal{U}}}$ of _infinitary
$\beta\bot_{\mathcal{U}}$-reduction_, or _Böhm reduction_ (over
${\mathcal{U}}$), is the infinitary closure of
$\to_{\beta\bot_{\mathcal{U}}}$. The relation
$\Rightarrow_{\bot_{\mathcal{U}}}$ of _parallel
$\bot_{\mathcal{U}}$-reduction_ is the parallel closure of
$R_{\bot_{\mathcal{U}}}$.

In general, relations on infinitary terms need to be defined coinductively.
However, if the relation depends only on finite initial parts of the terms
then it may often be defined inductively. Because induction is generally
better understood than coinduction, we prefer to give inductive definitions
whenever it is possible to give such a definition in a natural way, like with
the definition of compatible closure or one-step weak head reduction. This is
in contrast to e.g. the definition of infinitary reduction $\to^{\infty}$,
which intuitively may contain infinitely many reduction steps, and thus must
be defined by coinduction.

The idea with the definition of the infinitary closure $\to^{\infty}$ of a
one-step reduction relation $\to$ is that the depth at which a redex is
contracted should tend to infinity. This is achieved by defining
$\to^{\infty}$ in such a way that always after finitely many reduction steps
the subsequent contractions may be performed only under a constructor. So the
depth of the contracted redex always ultimately increases. The idea for the
definition of $\to^{\infty}$ comes from [19, 16, 17]. For infinitary
$\beta$-reduction $\to^{\infty}_{\beta}$ the definition is the same as in
[19]. To each derivation of $t\to^{\infty}s$ corresponds a strongly convergent
reduction sequence of length at most $\omega$ obtained by concatenating the
finite $\to^{*}$-reductions in the prefixes. See the proof of Theorem 57.

Our definition of meaningless terms differs from [22] in that it treats terms
with the $\bot$ constant, but it is equivalent to the original definition, in
the following sense. Let $\Lambda_{0}^{\infty}$ be the set of infinitary-
lambda terms without $\bot$. If ${\mathcal{U}}$ is a set of meaningless terms
defined as in [22] on $\Lambda_{0}^{\infty}$, then ${\mathcal{U}}_{\bot}$ (the
set of terms from ${\mathcal{U}}$ with some subterms in ${\mathcal{U}}$
replaced by $\bot$) is a set of meaningless terms according to our definition.
Conversely, if ${\mathcal{U}}$ is a set of meaningless terms according to our
definition, then ${\mathcal{U}}={\mathcal{U}}_{\bot}^{\prime}$ where
${\mathcal{U}}^{\prime}={\mathcal{U}}\cap\Lambda_{0}^{\infty}$
(${\mathcal{U}}^{\prime}$ then satisfies the axioms of [22]).

To show confluence of Böhm reduction over ${\mathcal{U}}$ we also need the
expansion axiom. The reason is purely technical. In the present coinductive
framework there is no way of talking about infinitary reductions of arbitrary
ordinal length, only about reductions of length $\omega$. We need the
expansion axiom to show that
$t\to^{\infty}_{\beta\bot_{\mathcal{U}}}t^{\prime}\Rightarrow_{\bot_{\mathcal{U}}}s$
implies $t\to^{\infty}_{\beta\bot_{\mathcal{U}}}s$.

The expansion axiom is necessary for this implication. Let ${\mathsf{O}}$ be
the _ogre_ [41] satisfying ${\mathsf{O}}\equiv\lambda x.{\mathsf{O}}$, i.e.,
${\mathsf{O}}\equiv\lambda x_{1}.\lambda x_{2}.\lambda x_{3}\ldots$. A term
$t$ is _head-active_ [41] if $t\equiv\lambda x_{1}\ldots x_{n}.rt_{1}\ldots
t_{m}$ with $r\in{\mathcal{R}}$ and $n,m\geq 0$. Define
${\mathcal{H}}=\\{t\in\Lambda^{\infty}\mid t\to^{*}_{\beta}t^{\prime}\text{
with }t^{\prime}\text{ head-active}\\}$,
${\mathcal{O}}=\\{t\in\Lambda^{\infty}\mid t\to^{*}_{\beta}{\mathsf{O}}\\}$
and ${\mathcal{U}}={\mathcal{H}}\cup{\mathcal{O}}$. One can show that
${\mathcal{U}}$ is a set of meaningless terms (see the appendix). Consider
$\Omega_{\mathsf{O}}=(\lambda xy.xx)(\lambda xy.xx)$. We have
$\Omega_{\mathsf{O}}\to^{\infty}_{\beta}{\mathsf{O}}\in{\mathcal{O}}$. But
$\Omega_{\mathsf{O}}\notin{\mathcal{U}}$, so ${\mathcal{U}}$ does not satisfy
the expansion axiom. Now,
$\Omega_{\mathsf{O}}\to^{\infty}_{\beta\bot_{\mathcal{U}}}{\mathsf{O}}\Rightarrow_{\bot_{\mathcal{U}}}\bot$,
but $\Omega_{\mathsf{O}}\not\to^{\infty}_{\beta\bot_{\mathcal{U}}}\bot$,
because no finite $\beta$-reduct of $\Omega_{\mathsf{O}}$ is in
${\mathcal{U}}$.

The expansion axiom could probably be weakened slightly, but the present
formulation is simple and it already appeared in the literature [42, 41, 25].
Sets of meaningless terms which do not satisfy the expansion axiom tend to be
artificial. A notion of a set of strongly meaningless terms equivalent to ours
appears in [41]. In the presence of the expansion axiom, the indiscernibility
axiom may be weakened [42, 41].

In the setup of [16, 17] it is possible to talk about reductions of arbitrary
ordinal length, but we have not investigated the possibility of adapting the
framework of [16, 17] to the needs of the present paper.

The axioms of a set ${\mathcal{U}}$ of meaningless terms are sufficient for
confluence and normalisation of Böhm reduction over ${\mathcal{U}}$. However,
they are not necessary. The paper [43] gives axioms necessary and sufficient
for confluence and normalisation.

The following two simple lemmas will often be used implicitly.

######  Lemma 3.

Let $\to^{\infty}$ be the infinitary and $\to^{*}$ the transitive-reflexive
closure of $\to$. Then the following conditions hold for all
$t,s,s^{\prime}\in\Lambda^{\infty}$:

  1. (1)

$t\to^{\infty}t$,

  2. (2)

if $t\to^{*}s\to^{\infty}s^{\prime}$ then $t\to^{\infty}s^{\prime}$,

  3. (3)

if $t\to^{*}s$ then $t\to^{\infty}s$.

######  Proof 4.1.

The first point follows by coinduction. The second point follows by case
analysis on $s\to^{\infty}s^{\prime}$. The last point follows from the
previous two.

The proof of the first point is straightforward, but to illustrate the
coinductive technique we give this proof in detail. A reader not familiar with
coinduction is invited to study this proof and insert the implicit ordinals as
in Section 3.

Let $t\in\Lambda^{\infty}$. There are three cases. If $t\equiv a$ then
$a\to^{*}a$, so $t\to^{\infty}t$ by the definition of $\to^{\infty}$. If
$t\equiv t_{1}t_{2}$ then $t_{1}\to^{\infty}t_{1}$ and
$t_{2}\to^{\infty}t_{2}$ by the coinductive hypothesis. Since also
$t\to^{*}t_{1}t_{2}$, we conclude $t\to^{\infty}t$. If $t\equiv\lambda
x.t^{\prime}$ then $t^{\prime}\to^{\infty}t^{\prime}$ by the coinductive
hypothesis. Since also $t\to^{*}\lambda x.t^{\prime}$, we conclude
$t\to^{\infty}t$.

######  Lemma 4.

If $R\subseteq S\subseteq\Lambda^{\infty}\times\Lambda^{\infty}$ then
${\to^{\infty}_{R}}\subseteq{\to^{\infty}_{S}}$.

######  Proof 4.2.

By coinduction.

The next three lemmas have essentially been shown in [19, Lemma 4.3–4.5].

######  Lemma 5.

If $s\to^{\infty}_{\beta}s^{\prime}$ and $t\to^{\infty}_{\beta}t^{\prime}$
then $s[t/x]\to^{\infty}_{\beta}s^{\prime}[t^{\prime}/x]$.

######  Proof 4.3.

By coinduction, with case analysis on $s\to^{\infty}_{\beta}s^{\prime}$, using
that $t_{1}\to^{*}_{\beta}t_{2}$ implies
$t_{1}[t/x]\to^{*}_{\beta}t_{2}[t/x]$.

######  Lemma 6.

If $t_{1}\to^{\infty}_{\beta}t_{2}\to_{\beta}t_{3}$ then
$t_{1}\to^{\infty}_{\beta}t_{3}$.

######  Proof 4.4.

Induction on $t_{2}\to_{\beta}t_{3}$, using Lemma 5.

######  Lemma 7.

If $t_{1}\to^{\infty}_{\beta}t_{2}\to^{\infty}_{\beta}t_{3}$ then
$t_{1}\to^{\infty}_{\beta}t_{3}$.

######  Proof 4.5.

By coinduction, with case analysis on $t_{2}\to^{\infty}_{\beta}t_{3}$, using
Lemma 6.

######  Lemma 8.

If $t$ is in rnf and $t\to^{\infty}_{\beta}s$ then $s$ is in rnf.

######  Proof 4.6.

Suppose $s$ is not in rnf, i.e., $s\equiv\bot$ or $s\equiv s_{1}s_{2}$ with
$s_{1}\to^{*}_{\beta}\lambda x.u$. If $s\equiv\bot$ then
$t\to^{*}_{\beta}\bot$, and thus either $t\equiv\bot$ or it $\beta$-reduces to
a redex. So $t$ is not in rnf. If $s\equiv s_{1}s_{2}$ with
$s_{1}\to^{\infty}_{\beta}\lambda x.u^{\prime}$, then
$t\to^{*}_{\beta}t_{1}t_{2}$ with $t_{i}\to^{\infty}_{\beta}s_{i}$. By Lemma 6
we have $t_{1}\to^{\infty}_{\beta}\lambda x.u$. Thus $t$ reduces to a redex
$(\lambda x.u)t_{2}$. Hence $t$ is not in rnf.

##  5\. Confluence and normalisation of Böhm reductions

In this section we use coinductive techniques to prove confluence and
normalisation of Böhm reduction over an arbitrary set of strongly meaningless
terms ${\mathcal{U}}$. The infinitary lambda calculus we are concerned with,
including the $\bot_{\mathcal{U}}$-reductions to $\bot$, shall be called the
$\lambda_{\beta\bot_{\mathcal{U}}}^{\infty}$-calculus.

More precisely, our aim is to prove the following theorems.

######  Theorem 39 (Confluence of the
$\lambda_{\beta\bot_{\mathcal{U}}}^{\infty}$-calculus).

If $t\to^{\infty}_{\beta\bot_{\mathcal{U}}}t_{1}$ and
$t\to^{\infty}_{\beta\bot_{\mathcal{U}}}t_{2}$ then there exists $t_{3}$ such
that $t_{1}\to^{\infty}_{\beta\bot_{\mathcal{U}}}t_{3}$ and
$t_{2}\to^{\infty}_{\beta\bot_{\mathcal{U}}}t_{3}$.

######  Theorem 40 (Normalisation of the
$\lambda_{\beta\bot_{\mathcal{U}}}^{\infty}$-calculus).

For every $t\in\Lambda^{\infty}$ there exists a unique $s\in\Lambda^{\infty}$
in $\beta\bot_{\mathcal{U}}$-normal form such that
$t\to^{\infty}_{\beta\bot_{\mathcal{U}}}s$.

In what follows we assume that ${\mathcal{U}}$ is an arbitrary fixed set of
strongly meaningless terms, unless specified otherwise. Actually, almost all
lemmas are valid for ${\mathcal{U}}$ being a set of meaningless terms, without
the expansion axiom. Unless explicitly mentioned before the statement of a
lemma, the proofs do not use the expansion axiom. To show confluence modulo
$\sim_{\mathcal{U}}$ (Theorem 54), it suffices that ${\mathcal{U}}$ is a set
of meaningless terms. Confluence and normalisation of the
$\lambda_{\beta\bot_{\mathcal{U}}}$-calculus (Theorem 39 and Theorem 40),
however, require the expansion axiom. But this is only because in the present
coinductive framework we are not able to talk about infinite reductions of
arbitrary ordinal length. Essentially, we need the expansion axiom to compress
the Böhm reductions to length $\omega$.

The idea of the proof is to show that for every term there exists a certain
standard infinitary $\beta\bot_{\mathcal{U}}$-reduction to normal form. This
reduction is called an infinitary $N_{\mathcal{U}}$-reduction (Definition 5.4
and Lemma 34). We show that the normal forms obtained through infinitary
$N_{\mathcal{U}}$-reductions are unique (Lemma 35). Then we prove that
prepending infinitary $\beta\bot_{\mathcal{U}}$-reduction to an
$N_{\mathcal{U}}$-reduction results in an $N_{\mathcal{U}}$-reduction (Theorem
38). Since an $N_{\mathcal{U}}$-reduction is an infinitary
$\beta\bot_{\mathcal{U}}$-reduction of a special form (Lemma 33), these
results immediately imply confluence (Theorem 39) and normalisation (Theorem
40) of infinitary $\beta\bot_{\mathcal{U}}$-reduction. Hence, in essence we
derive confluence from a strengthened normalisation result. See Figure 1.

$\textstyle{{t_{1}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{N_{\mathcal{U}}}$$\textstyle{{t}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\infty}$$\scriptstyle{\beta\bot_{\mathcal{U}}}$$\scriptstyle{N_{\mathcal{U}}}$$\scriptstyle{\infty}$$\scriptstyle{\beta\bot_{\mathcal{U}}}$$\scriptstyle{N_{\mathcal{U}}}$$\textstyle{{t_{2}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{N_{\mathcal{U}}}$$\textstyle{{t_{1}^{\prime}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{{\displaystyle\equiv}}$$\textstyle{{t_{2}^{\prime}}}$

Figure 1. Confluence of infinitary Böhm reduction.

In our proof we use a standardisation result for infinitary $\beta$-reductions
from [19] (Theorem 28). In particular, this theorem is needed to show
uniqueness of canonical root normal forms (Definition 5.3). Theorem 38 depends
on this. Even when counting in the results of [19] only referenced here, our
confluence proof may be considered simpler than previous proofs of related
results. In particular, it is much easier for formalise.

We also show that the set of root-active terms is strongly meaningless.
Together with the previous theorems this implies confluence and normalisation
of the $\lambda_{\beta\bot_{\mathcal{R}}}^{\infty}$-calculus. Confluence of
the $\lambda_{\beta\bot_{\mathcal{R}}}^{\infty}$-calculus in turn implies
confluence of $\to^{\infty}_{\beta}$ modulo equivalence of meaningless terms.
The following theorem does not require the expansion axiom.

######  Theorem 54 (Confluence modulo equivalence of meaningless terms).

If $t\sim_{\mathcal{U}}t^{\prime}$, $t\to^{\infty}_{\beta}s$ and
$t^{\prime}\to^{\infty}_{\beta}s^{\prime}$ then there exist $r,r^{\prime}$
such that $r\sim_{\mathcal{U}}r^{\prime}$, $s\to^{\infty}_{\beta}r$ and
$s^{\prime}\to^{\infty}_{\beta}r^{\prime}$.

Note that our overall proof strategy is different from [10, 22, 24]. We first
derive a strengthened normalisation result for Böhm reduction, from this we
derive confluence of Böhm reduction, then we show that root-active terms are
strongly meaningless thus specialising the confluence result, and only using
that we show confluence modulo equivalence of meaningless terms. In [10, 22,
24] first confluence modulo equivalence of meaningless terms is shown, and
from that confluence of Böhm reduction is derived. Of course, some
intermediate lemmas we prove have analogons in [10, 22, 24], but we believe
the general proof strategy to be fundamentally different.

###  5.1. Properties of $\sim_{\mathcal{U}}$

In this subsection ${\mathcal{U}}$ is an arbitrary fixed set of meaningless
terms, and $\sim_{\mathcal{U}}$ is the parallel closure of
${\mathcal{U}}\times{\mathcal{U}}$. The expansion axiom is not used in this
subsection.

######  Lemma 9.

If $t\sim_{\mathcal{U}}t^{\prime}$ and $s\sim_{\mathcal{U}}s^{\prime}$ then
$t[s/x]\sim_{\mathcal{U}}t^{\prime}[s^{\prime}/x]$.

######  Proof 5.1.

By coinduction, using the substitution axiom.

######  Lemma 10.

If $t\to_{\beta}s$ and $t\sim_{{\mathcal{U}}}t^{\prime}$ then there is
$s^{\prime}$ with $t^{\prime}\to_{\beta}^{\equiv}s^{\prime}$ and
$s\sim_{{\mathcal{U}}}s^{\prime}$.

######  Proof 5.2.

Induction on $t\to_{\beta}s$. If the case $t,t^{\prime}\in{\mathcal{U}}$ in
the definition of $t\sim_{\mathcal{U}}t^{\prime}$ holds then
$s\in{\mathcal{U}}$ by the closure axiom, so $t^{\prime}\sim_{\mathcal{U}}s$
and we may take $s^{\prime}\equiv t^{\prime}$. Thus assume otherwise. Then all
cases follow directly from the inductive hypothesis, except when $t$ is the
contracted $\beta$-redex. Then $t\equiv(\lambda x.t_{1})t_{2}$ and $s\equiv
t_{1}[t_{2}/x]$. First assume $t\in{\mathcal{U}}$. Then also
$t^{\prime}\in{\mathcal{U}}$ by the indiscernibility axiom (note this does not
imply that the first case in the definition of $t\sim_{\mathcal{U}}t^{\prime}$
holds). Also $s\in{\mathcal{U}}$ by the closure axiom, so
$t^{\prime}\sim_{\mathcal{U}}s$ and we may take $s^{\prime}\equiv t^{\prime}$.
So assume $t\notin{\mathcal{U}}$. Then $\lambda x.t_{1}\notin{\mathcal{U}}$ by
the overlap axiom. Hence $t^{\prime}\equiv(\lambda
x.t_{1}^{\prime})t_{2}^{\prime}$ with $t_{i}\sim_{\mathcal{U}}t_{i}^{\prime}$.
Thus $t_{1}[t_{2}/x]\sim_{\mathcal{U}}t_{1}^{\prime}[t_{2}^{\prime}/x]$ by
Lemma 9. So we may take $s^{\prime}\equiv t_{1}^{\prime}[t_{2}^{\prime}/x]$.

######  Lemma 11.

If $t\to^{\infty}_{\beta}s$ and $t\sim_{{\mathcal{U}}}t^{\prime}$ then there
is $s^{\prime}$ with $t^{\prime}\to^{\infty}_{\beta}s^{\prime}$ and
$s\sim_{{\mathcal{U}}}s^{\prime}$.

######  Proof 5.3.

By coinduction. If $s\equiv a$ then $t\to^{*}_{\beta}s$ and the claim follows
from Lemma 10. If $s\equiv s_{1}s_{2}$ then $t\to^{*}_{\beta}t_{1}t_{2}$ with
$t_{i}\to^{\infty}_{\beta}s_{i}$. By Lemma 10 there is $u$ with
$t_{1}t_{2}\sim_{\mathcal{U}}u$ and $t^{\prime}\to^{*}_{\beta}u$. If
$t_{1}t_{2},u\in{\mathcal{U}}$ then $s\in{\mathcal{U}}$ by the closure axiom,
and thus we may take $s^{\prime}\equiv u$. Otherwise $u\equiv u_{1}u_{2}$ with
$t_{i}\sim_{\mathcal{U}}u_{i}$. By the coinductive hypothesis we obtain
$s_{1}^{\prime},s_{2}^{\prime}$ with $u_{i}\to^{\infty}_{\beta}s_{i}^{\prime}$
and $s_{i}\sim_{\mathcal{U}}s_{i}^{\prime}$. Take $s^{\prime}\equiv
s_{1}^{\prime}s_{2}^{\prime}$. Then $t^{\prime}\to^{\infty}_{\beta}s^{\prime}$
and $s\sim_{\mathcal{U}}s^{\prime}$. If $s\equiv\lambda x.s^{\prime}$ then the
argument is analogous to the previous case.

######  Lemma 12.

If $t\sim_{\mathcal{U}}s$ and $s\sim_{\mathcal{U}}u$ then
$t\sim_{\mathcal{U}}s$.

######  Proof 5.4.

By coinduction, using the indiscernibility axiom.

######  Lemma 13.

If $t\sim_{\mathcal{U}}s$ then there is $r$ with
$t\Rightarrow_{\bot_{\mathcal{U}}}r$ and $s\Rightarrow_{\bot_{\mathcal{U}}}r$.

######  Proof 5.5.

By coinduction.

###  5.2. Properties of parallel $\bot_{\mathcal{U}}$-reduction

Recall that ${\mathcal{U}}$ is an arbitrary fixed set of strongly meaningless
terms. The expansion axiom is not used in this subsection except for Corollary
24, Lemma 25, Corollary 26 and Lemma 27.

######  Lemma 14.

If $s\Rightarrow_{\bot_{\mathcal{U}}}s^{\prime}$ and
$t\Rightarrow_{\bot_{\mathcal{U}}}t^{\prime}$ then
$s[t/x]\Rightarrow_{\bot_{\mathcal{U}}}s^{\prime}[t^{\prime}/x]$.

######  Proof 5.6.

Coinduction with case analysis on
$s\Rightarrow_{\bot_{\mathcal{U}}}s^{\prime}$, using the substitution axiom.

######  Lemma 15.

If $t\Rightarrow_{\bot_{\mathcal{U}}}s$ then
$t\to^{\infty}_{\beta\bot_{\mathcal{U}}}s$.

######  Proof 5.7.

By coinduction.

######  Lemma 16.

If $t\in{\mathcal{U}}$ and $t\Rightarrow_{\bot_{\mathcal{U}}}s$ or
$s\Rightarrow_{\bot_{\mathcal{U}}}t$ then $s\in{\mathcal{U}}$.

######  Proof 5.8.

Using the root-activeness axiom and that $\bot$ is root-active, show by
coinduction that $t\sim_{\mathcal{U}}s$. Then use the indiscernibility axiom.

######  Lemma 17.

If
$t_{1}\Rightarrow_{\bot_{\mathcal{U}}}t_{2}\Rightarrow_{\bot_{\mathcal{U}}}t_{3}$
then $t_{1}\Rightarrow_{\bot_{\mathcal{U}}}t_{3}$.

######  Proof 5.9.

Coinduction with case analysis on
$t_{2}\Rightarrow_{\bot_{\mathcal{U}}}t_{3}$, using Lemma 16.

######  Lemma 18.

If $t_{1}\Rightarrow_{\bot_{\mathcal{U}}}t_{2}\to_{\beta}t_{3}$ then there
exists $t_{1}^{\prime}$ such that
$t_{1}\to_{\beta}t_{1}^{\prime}\Rightarrow_{\bot_{\mathcal{U}}}t_{3}$.

######  Proof 5.10.

Induction on $t_{2}\to_{\beta}t_{3}$. The only interesting case is when
$t_{2}\equiv(\lambda x.s_{1})s_{2}$ and $t_{3}\equiv s_{1}[s_{2}/x]$. Then
$t_{1}\equiv(\lambda x.u_{1})u_{2}$ with
$u_{i}\Rightarrow_{\bot_{\mathcal{U}}}s_{i}$. By Lemma 14,
$u_{1}[u_{2}/x]\Rightarrow_{\bot_{\mathcal{U}}}s_{1}[s_{2}/x]$. Thus take
$t_{1}^{\prime}\equiv u_{1}[u_{2}/x]$.

######  Lemma 19.

If $s\to^{*}_{\beta\bot_{\mathcal{U}}}t$ then there exists $r$ such that
$s\to^{*}_{\beta}r\Rightarrow_{\bot_{\mathcal{U}}}t$.

######  Proof 5.11.

Induction on the length of $s\to^{*}_{\beta\bot_{\mathcal{U}}}t$, using Lemma
18 and Lemma 17.

######  Corollary 20.

If
$t_{1}\Rightarrow_{\bot_{\mathcal{U}}}t_{2}\to^{*}_{\beta\bot_{\mathcal{U}}}t_{3}$
then there is $s$ with
$t_{1}\to^{*}_{\beta}s\Rightarrow_{\bot_{\mathcal{U}}}t_{3}$.

######  Proof 5.12.

Follows from Lemmas 19, 18, 17.

######  Lemma 21.

If
$t_{1}\Rightarrow_{\bot_{\mathcal{U}}}t_{2}\to^{\infty}_{\beta\bot_{\mathcal{U}}}t_{3}$
then $t_{1}\to^{\infty}_{\beta\bot_{\mathcal{U}}}t_{3}$.

######  Proof 5.13.

By coinduction. There are three cases.

  * •

$t_{3}\equiv a$. Then
$t_{1}\Rightarrow_{\bot_{\mathcal{U}}}t_{2}\to^{*}_{\beta\bot_{\mathcal{U}}}a$.
By Corollary 20 there is $s$ with
$t_{1}\to^{*}_{\beta}s\Rightarrow_{\bot_{\mathcal{U}}}a$. By Lemma 15 we have
$s\to^{\infty}_{\beta\bot_{\mathcal{U}}}a$. Thus
$t_{1}\to^{\infty}_{\beta\bot_{\mathcal{U}}}a$.

  * •

$t_{3}\equiv s_{1}s_{2}$. Then
$t_{1}\Rightarrow_{\bot_{\mathcal{U}}}t_{2}\to^{*}_{\beta\bot_{\mathcal{U}}}s_{1}^{\prime}s_{2}^{\prime}$
with $s_{i}^{\prime}\to^{\infty}_{\beta\bot_{\mathcal{U}}}s_{i}$. By Corollary
20 there is $u$ with
$t_{1}\to^{*}_{\beta}u\Rightarrow_{\bot_{\mathcal{U}}}s_{1}^{\prime}s_{2}^{\prime}$.
Then $u\equiv u_{1}u_{2}$ with
$u_{i}\Rightarrow_{\bot_{\mathcal{U}}}s_{i}^{\prime}\to^{\infty}_{\beta\bot_{\mathcal{U}}}s_{i}$.
By the coinductive hypothesis
$u_{i}\to^{\infty}_{\beta\bot_{\mathcal{U}}}s_{i}$. Thus
$t_{1}\to^{\infty}_{\beta\bot_{\mathcal{U}}}s_{1}s_{2}\equiv t_{3}$.

  * •

$t_{3}\equiv\lambda x.r$. The argument is analogous to the previous case.

The following lemma is an analogon of [22, Lemma 12.9.22].

######  Lemma 22 (Postponement of parallel $\bot_{\mathcal{U}}$-reduction).

If $t\to^{\infty}_{\beta\bot_{\mathcal{U}}}s$ then there exists $r$ such that
$t\to^{\infty}_{\beta}r\Rightarrow_{\bot_{\mathcal{U}}}s$.

######  Proof 5.14.

By coinduction with case analysis on
$t\to^{\infty}_{\beta\bot_{\mathcal{U}}}s$, using Lemmas 19, 21.

Since this is the first of our coinductive proofs involving an implicit Skolem
function (see Example 3), we give it in detail. The reader is invited to
extract from this proof an explicit corecursive definition of the Skolem
function.

Assume $t\to^{\infty}_{\beta\bot_{\mathcal{U}}}s$. There are three cases.

  * •

$s\equiv a$ and $t\to^{*}_{\beta\bot_{\mathcal{U}}}a$. Then the claim follows
from Lemma 19.

  * •

$s\equiv s_{1}s_{2}$ and $t\to^{*}_{\beta\bot_{\mathcal{U}}}t_{1}t_{2}$ and
$t_{i}\to^{\infty}_{\beta\bot_{\mathcal{U}}}s_{i}$. By Lemma 19 there is
$t^{\prime}$ with
$t\to^{*}_{\beta}t^{\prime}\Rightarrow_{\bot_{\mathcal{U}}}t_{1}t_{2}$.
Because $t_{1}t_{2}\not\equiv\bot$, we must have $t^{\prime}\equiv
t_{1}^{\prime}t_{2}^{\prime}$ with
$t_{i}^{\prime}\Rightarrow_{\bot_{\mathcal{U}}}t_{i}$. By Lemma 21 we have
$t_{i}^{\prime}\to^{\infty}_{\beta\bot_{\mathcal{U}}}s_{i}$. By the
coinductive hypothesis we obtain $s_{1}^{\prime},s_{2}^{\prime}$ such that
$t_{i}^{\prime}\to^{\infty}_{\beta}s_{i}^{\prime}\Rightarrow_{\bot_{\mathcal{U}}}s_{i}$.
Hence
$t\to^{\infty}_{\beta}s_{1}^{\prime}s_{2}^{\prime}\Rightarrow_{\bot_{\mathcal{U}}}s_{1}s_{2}\equiv
s$.

  * •

$s\equiv\lambda x.s^{\prime}$ and $t\to^{*}_{\beta\bot_{\mathcal{U}}}\lambda
x.t^{\prime}$ and
$t^{\prime}\to^{\infty}_{\beta\bot_{\mathcal{U}}}s^{\prime}$. By Lemma 19
there is $u$ with $t\to^{*}_{\beta}u\Rightarrow_{\bot_{\mathcal{U}}}\lambda
x.t^{\prime}$. Then $u\equiv\lambda x.u^{\prime}$ with
$u^{\prime}\Rightarrow_{\bot_{\mathcal{U}}}t^{\prime}$. By Lemma 21 we have
$u^{\prime}\to^{\infty}_{\beta\bot_{\mathcal{U}}}s^{\prime}$. By the
coinductive hypothesis we obtain $w$ such that
$u^{\prime}\to^{\infty}_{\beta}w\Rightarrow_{\bot_{\mathcal{U}}}s^{\prime}$.
Hence $t\to^{\infty}_{\beta}\lambda x.w\Rightarrow_{\bot_{\mathcal{U}}}\lambda
x.s^{\prime}\equiv s$.

######  Corollary 23.

If $t\in{\mathcal{U}}$ and $t\to^{\infty}_{\beta\bot_{\mathcal{U}}}s$ then
$s\in{\mathcal{U}}$.

######  Proof 5.15.

Follows from Lemma 22, the closure axiom and Lemma 16.

The following depend on the expansion axiom.

######  Corollary 24.

If $s\in{\mathcal{U}}$ and $t\to^{\infty}_{\beta\bot_{\mathcal{U}}}s$ then
$t\in{\mathcal{U}}$.

######  Proof 5.16.

Follows from Lemma 22, Lemma 16 and the expansion axiom.

######  Lemma 25.

If
$t\to^{\infty}_{\beta\bot_{\mathcal{U}}}t^{\prime}\Rightarrow_{\bot_{\mathcal{U}}}s$
then $t\to^{\infty}_{\beta\bot_{\mathcal{U}}}s$.

######  Proof 5.17.

By coinduction, analysing $t^{\prime}\Rightarrow_{\bot_{\mathcal{U}}}s$. All
cases follow directly from the coinductive hypothesis, except when
$s\equiv\bot$ and $t^{\prime}\in{\mathcal{U}}$. But then $t\in{\mathcal{U}}$
by Corollary 24, so $t\Rightarrow_{\bot_{\mathcal{U}}}s$, and thus
$t\to^{\infty}_{\beta\bot_{\mathcal{U}}}s$ by Lemma 15.

######  Corollary 26.

If $t\to^{\infty}_{\beta\bot_{\mathcal{U}}}s\to^{*}_{\beta}r$ then
$t\to^{\infty}_{\beta\bot_{\mathcal{U}}}r$.

######  Proof 5.18.

By Lemma 22 we have
$t\to^{\infty}_{\beta}t^{\prime}\Rightarrow_{\bot_{\mathcal{U}}}s\to^{*}_{\beta}r$.
By Lemma 18 there is $s^{\prime}$ with
$t^{\prime}\to^{*}_{\beta}s^{\prime}\Rightarrow_{\bot_{\mathcal{U}}}r$. By
Lemma 6 we have $t\to^{\infty}_{\beta}s^{\prime}$, and thus
$t\to^{\infty}_{\beta\bot_{\mathcal{U}}}s^{\prime}$. By Lemma 25 we finally
obtain $t\to^{\infty}_{\beta\bot_{\mathcal{U}}}r$.

######  Lemma 27.

If $t\notin U$ and $t\Rightarrow_{\bot_{\mathcal{U}}}s$ and $s$ is in rnf,
then $t$ is in rnf.

######  Proof 5.19.

We consider possible forms of $s$.

  * •

$s\equiv a$ with $a\not\equiv\bot$. Then $t\equiv a$ and $t$ is in rnf.

  * •

$s\equiv\lambda x.s^{\prime}$. Then $t\equiv\lambda x.t^{\prime}$ with
$t^{\prime}\Rightarrow_{\bot_{\mathcal{U}}}s^{\prime}$, so $t$ is in rnf.

  * •

$s\equiv s_{1}s_{2}$ and there is no $r$ with
$s_{1}\to^{\infty}_{\beta}\lambda x.r$. Then $t\equiv t_{1}t_{2}$ with
$t_{i}\Rightarrow_{\bot_{\mathcal{U}}}s_{i}$. Then also
$t_{1}\sim_{\mathcal{U}}s_{1}$. Suppose $t_{1}\to^{\infty}_{\beta}\lambda
x.r$. By Lemma 11 there is $r^{\prime}$ with
$s_{1}\to^{\infty}_{\beta}r^{\prime}\sim_{\mathcal{U}}\lambda x.r$. There are
two cases.

    * –

$r^{\prime},\lambda x.r\in{\mathcal{U}}$. Then $(\lambda
x.r)t_{2}\in{\mathcal{U}}$ by the overlap axiom, and thus $t\in{\mathcal{U}}$
by the expansion axiom. Contradiction.

    * –

$r^{\prime}\equiv\lambda x.r^{\prime\prime}$ with
$r\sim_{\mathcal{U}}r^{\prime\prime}$. But then
$s_{1}\to^{\infty}_{\beta}\lambda x.r^{\prime\prime}$. Contradiction.

###  5.3. Weak head reduction

######  Theorem 28 (Endrullis, Polonsky [19]).

$t\to^{\infty}_{\beta}s$ iff $t\to^{\infty}_{w}s$.

Strictly speaking, in [19] the above theorem is shown for a different set of
infinitary lambda terms which do not contain constants. However, it is clear
that for the purposes of [19] constants may be treated as variables not
occuring bound, and thus the proof of the above theorem may be used in our
setting. We omit the proof of this theorem here, but we included the proof in
our formalisation.

######  Lemma 29.

If $t\to^{\infty}_{w}t_{1}$ and $t\to_{w}t_{2}$ then there is $t_{3}$ with
$t_{2}\to^{\infty}_{w}t_{3}$ and $t_{1}\to_{w}^{\equiv}t_{3}$.

######  Proof 5.20.

If the weak head redex in $t$ is contracted in $t\to^{\infty}_{w}t_{1}$ then
$t\to_{w}t_{2}\to^{\infty}_{w}t_{1}$ and we may take $t_{3}\equiv t_{1}$.
Otherwise $t\equiv(\lambda x.s)uu_{1}\ldots u_{m}$, $t_{2}\equiv
s[u/x]u_{1}\ldots u_{m}$ and $t_{1}\equiv(\lambda
x.s^{\prime})u^{\prime}u_{1}^{\prime}\ldots u_{m}^{\prime}$ with
$s\to^{\infty}_{w}s^{\prime}$, $u\to^{\infty}_{w}u^{\prime}$ and
$u_{i}\to^{\infty}_{w}u_{i}^{\prime}$ for $i=1,\ldots,m$. By Theorem 28 and
Lemma 5 we obtain $s[u/x]\to^{\infty}_{w}s^{\prime}[u^{\prime}/x]$. Take
$t_{3}\equiv s^{\prime}[u^{\prime}/x]u_{1}^{\prime}\ldots u_{m}^{\prime}$.
Then $t_{2}\to^{\infty}_{w}t_{3}$ and $t_{1}\to_{w}t_{3}$.

######  Lemma 30.

If $t\to^{\infty}_{\beta}s$ with $s$ in rnf, then there is $s^{\prime}$ in rnf
with $t\to^{*}_{w}s^{\prime}\to^{\infty}_{w}s$.

######  Proof 5.21.

By Theorem 28 we have $t\to^{\infty}_{w}s$. Because $s$ is in rnf, there are
three cases.

  * •

$s\equiv a$ with $a\not\equiv\bot$. Then $t\to^{*}_{w}s$ and we may take
$s^{\prime}\equiv s$.

  * •

$s\equiv\lambda x.s_{0}$. Then $t\to^{*}_{w}\lambda x.t_{0}$ with
$t_{0}\to^{\infty}_{w}s_{0}$. So take $s^{\prime}\equiv\lambda x.t_{0}$.

  * •

$s\equiv s_{1}s_{2}$ and there is no $r$ with
$s_{1}\to^{\infty}_{\beta}\lambda x.r$. Then $t\to^{*}_{w}t_{1}t_{2}$ with
$t_{i}\to^{\infty}_{w}s_{i}$. Suppose $t_{1}\to^{\infty}_{\beta}\lambda x.u$.
Then $t_{1}\to^{*}_{w}\lambda x.u^{\prime}$ for some $u^{\prime}$, by Theorem
28. By Lemma 29 there is $r$ with $\lambda x.u^{\prime}\to^{\infty}_{w}r$ and
$s_{1}\to^{*}_{w}r$. But then $r\equiv\lambda x.r^{\prime}$, so $s_{1}$
reduces to an abstraction. Contradiction. Hence $t_{1}t_{2}$ is in rnf, so we
may take $s^{\prime}\equiv t_{1}t_{2}$.

######  Lemma 31.

If $t\to^{*}_{w}s_{1}$, $t\to^{*}_{w}s_{2}$ and these reductions have the same
length, then $s_{1}\equiv s_{2}$.

######  Proof 5.22.

By induction on the length of the reduction, using the fact that weak head
redexes are unique if they exist.

The _canonical root normal form_ (crnf) of a term $t$ is an rnf $s$ such that
$t\to^{*}_{w}s$ and this reduction is shortest among all finitary weak head
reductions of $t$ to root normal form.

It follows from Lemma 30 and Lemma 31 that if $t$ has a rnf then it has a
unique crnf. We shall denote this crnf by $\mathrm{crnf}(t)$.

######  Lemma 32.

If $t\to^{\infty}_{\beta}s$ with $s$ in rnf, then
$t\to^{*}_{w}\mathrm{crnf}(t)\to^{\infty}_{w}s$.

######  Proof 5.23.

Follows from Lemma 30 and Lemma 31.

###  5.4. Infinitary $N_{\mathcal{U}}$-reduction

In the $\lambda_{\beta\bot_{\mathcal{U}}}^{\infty}$-calculus every term has a
unique normal form. This normal form may be obtained through an infinitary
$N_{\mathcal{U}}$-reduction, defined below.

The relation $\leadsto_{N_{\mathcal{U}}}$ is defined coinductively.

$\begin{array}[]{c}t\leadsto_{N_{\mathcal{U}}}a\lx@proof@logical@and
t\notin{\mathcal{U}}\mathrm{crnf}(t)\equiv
a\quad\quad\,t\leadsto_{N_{\mathcal{U}}}s_{1}s_{2}\lx@proof@logical@and
t\notin{\mathcal{U}}\mathrm{crnf}(t)\equiv
t_{1}t_{2}t_{1}\leadsto_{N_{\mathcal{U}}}s_{1}t_{2}\leadsto_{N_{\mathcal{U}}}s_{2}\\\
\\\ t\leadsto_{N_{\mathcal{U}}}\lambda x.s\lx@proof@logical@and
t\notin{\mathcal{U}}\mathrm{crnf}(t)\equiv\lambda
x.t^{\prime}t^{\prime}\leadsto_{N_{\mathcal{U}}}s\quad\quad\,t\leadsto_{N_{\mathcal{U}}}\bot
t\in{\mathcal{U}}\end{array}$

Note that because ${\mathcal{R}}\subseteq{\mathcal{U}}$, every term
$t\notin{\mathcal{U}}$ has a rnf, so $\mathrm{crnf}(t)$ is defined for
$t\notin{\mathcal{U}}$. Also note that $\leadsto_{N_{\mathcal{U}}}$ is not
closed under contexts, e.g., $t\leadsto_{N_{\mathcal{U}}}t^{\prime}$ does
_not_ imply $ts\leadsto_{N_{\mathcal{U}}}t^{\prime}s$.

The infinitary $N_{\mathcal{U}}$-reduction $\leadsto_{N_{\mathcal{U}}}$
reduces a term to its normal form — its Böhm-like tree. It is a “standard”
reduction with a specifically regular structure, which allows us to prove
Theorem 38: if
$t\to^{\infty}_{\beta\bot_{\mathcal{U}}}t^{\prime}\leadsto_{N_{\mathcal{U}}}s$
then $t\leadsto_{N_{\mathcal{U}}}s$. This property allows us to derive
confluence from the fact that every term has a unique normal form reachable by
an infinitary $N_{\mathcal{U}}$-reduction. See Figure 1. It is crucial here
that canonical root normal forms are unique, and that Lemma 32 holds. This
depends on Theorem 28 — the standardisation result shown by Endrullis and
Polonsky.

######  Lemma 33.

If $t\leadsto_{N_{\mathcal{U}}}s$ then
$t\to^{\infty}_{\beta\bot_{\mathcal{U}}}s$.

######  Proof 5.24.

By coinduction.

######  Lemma 34.

For every term $t\in\Lambda^{\infty}$ there is $s$ with
$t\leadsto_{N_{\mathcal{U}}}s$.

######  Proof 5.25.

By coinduction. If $t\in{\mathcal{U}}$ then $t\leadsto_{N_{\mathcal{U}}}\bot$
and we may take $s\equiv\bot$. Otherwise there are three cases depending on
the form of $\mathrm{crnf}(t)$.

  * •

$\mathrm{crnf}(t)\equiv a$. Then $t\leadsto_{N_{\mathcal{U}}}a$ by the first
rule, so we may take $s\equiv a$.

  * •

$\mathrm{crnf}(t)\equiv t_{1}t_{2}$. Then by the coinductive hypothesis we
obtain $s_{1},s_{2}$ with $t_{i}\leadsto_{N_{\mathcal{U}}}s_{i}$. Take
$s\equiv s_{1}s_{2}$. Then $t\leadsto_{N_{\mathcal{U}}}s$.

  * •

$\mathrm{crnf}(t)\equiv\lambda x.t^{\prime}$. Analogous to the previous case.

######  Lemma 35.

If $t\leadsto_{N_{\mathcal{U}}}s_{1}$ and $t\leadsto_{N_{\mathcal{U}}}s_{2}$
then $s_{1}\equiv s_{2}$.

######  Proof 5.26.

By coinduction. If $s_{1}\equiv\bot$ then $t\in{\mathcal{U}}$, so we must also
have $s_{2}\equiv\bot$. Otherwise there are three cases, depending on the form
of $\mathrm{crnf}(t)$. Suppose $\mathrm{crnf}(t)\equiv t_{1}t_{2}$, other
cases being similar. Then $s_{1}\equiv u_{1}u_{2}$ with
$t_{i}\leadsto_{N_{\mathcal{U}}}u_{i}$ and $s_{2}\equiv w_{1}w_{2}$ with
$t_{i}\leadsto_{N_{\mathcal{U}}}w_{i}$. By the coinductive hypothesis
$u_{i}\equiv w_{i}$. Thus $s_{1}\equiv u_{1}u_{2}\equiv w_{1}w_{2}\equiv
s_{2}$.

The next two lemmas and the theorem depend on the expansion axiom.

######  Lemma 36.

If $t\leadsto_{N_{\mathcal{U}}}s$ then $s$ is in
$\beta\bot_{\mathcal{U}}$-normal form.

######  Proof 5.27.

Suppose $s$ contains a $\beta\bot_{\mathcal{U}}$-redex. Without loss of
generality, assume the redex is at the root. First assume that $s$ is a
$\bot_{\mathcal{U}}$-redex, i.e., $s\in{\mathcal{U}}$ and $s\not\equiv\bot$.
Using Lemma 33 we conclude $t\to^{\infty}_{\beta\bot_{\mathcal{U}}}s$. Then
$t\in{\mathcal{U}}$ by Corollary 24. Thus $s\equiv\bot$, giving a
contradiction. So assume $s$ is a $\beta$-redex, i.e., $s\equiv(\lambda
x.s_{1})s_{2}$. But by inspecting the definition of
$t\leadsto_{N_{\mathcal{U}}}s$ one sees that this is only possible when
$\mathrm{crnf}(t)$ is a $\beta$-redex. Contradiction.

######  Lemma 37.

Suppose $t\to^{\infty}_{\beta\bot_{\mathcal{U}}}s$ and $t,s$ are in rnf.

  * •

If $s\equiv a$ then $t\equiv s$.

  * •

If $s\equiv s_{1}s_{2}$ then $t\equiv t_{1}t_{2}$ with
$t_{i}\to^{\infty}_{\beta\bot_{\mathcal{U}}}s_{i}$.

  * •

If $s\equiv\lambda x.s^{\prime}$ then $t\equiv\lambda x.t^{\prime}$ with
$t^{\prime}\to^{\infty}_{\beta\bot_{\mathcal{U}}}s^{\prime}$.

######  Proof 5.28.

First note that by Lemma 22 there is $r$ with
$t\to^{\infty}_{\beta}r\Rightarrow_{\bot_{\mathcal{U}}}s$.

  * •

If $s\equiv a$ then $a\not\equiv\bot$ and $r\equiv a$, and thus
$t\to^{*}_{\beta}a$. But because $t$ is in rnf it does not reduce to a
$\beta$-redex, so in fact $t\equiv a$.

  * •

If $s\equiv s_{1}s_{2}$ then $r\equiv r_{1}r_{2}$ with
$r_{i}\Rightarrow_{\bot_{\mathcal{U}}}s_{i}$. Thus
$t\to^{*}_{\beta}t_{1}^{\prime}t_{2}^{\prime}$ where
$t_{i}^{\prime}\to^{\infty}_{\beta}r_{i}$. Because $t$ is in rnf, we must in
fact have $t\equiv t_{1}t_{2}$ with $t_{i}\to^{*}_{\beta}t_{i}^{\prime}$. Then
$t_{i}\to^{\infty}_{\beta}r_{i}\Rightarrow_{\bot_{\mathcal{U}}}s_{i}$, so
$t_{i}\to^{\infty}_{\beta\bot_{\mathcal{U}}}s_{i}$ by Lemma 25.

  * •

The case $s\equiv\lambda x.s^{\prime}$ is analogous to the previous one.

######  Theorem 38.

If
$t\to^{\infty}_{\beta\bot_{\mathcal{U}}}t^{\prime}\leadsto_{N_{\mathcal{U}}}s$
then $t\leadsto_{N_{\mathcal{U}}}s$.

######  Proof 5.29.

By coinduction. If $s\equiv\bot$ then $t^{\prime}\in{\mathcal{U}}$. By
Corollary 24 also $t\in{\mathcal{U}}$. Hence
$t\leadsto_{N_{\mathcal{U}}}\bot\equiv s$. If $s\not\equiv\bot$ then
$t^{\prime}\notin{\mathcal{U}}$ and
$t^{\prime}\to^{*}_{w}\mathrm{crnf}(t^{\prime})$. By Corollary 26 we have
$t\to^{\infty}_{\beta\bot_{\mathcal{U}}}\mathrm{crnf}(t^{\prime})$. By Lemma
22 there is $r$ with
$t\to^{\infty}_{\beta}r\Rightarrow_{\bot_{\mathcal{U}}}\mathrm{crnf}(t^{\prime})$.
We have $t\notin{\mathcal{U}}$ by Corollary 23. Then $r$ is in rnf by Lemma
27. Hence
$t\to^{*}_{w}\mathrm{crnf}(t)\to^{\infty}_{\beta\bot_{\mathcal{U}}}\mathrm{crnf}(t^{\prime})$
by Lemma 32 and Lemma 25. Now there are three cases depending on the form of
$\mathrm{crnf}(t^{\prime})$.

  * •

$\mathrm{crnf}(t^{\prime})\equiv a$. Then $s\equiv a$, and
$\mathrm{crnf}(t)\equiv a$ by Lemma 37. Thus
$t\leadsto_{N_{\mathcal{U}}}a\equiv s$.

  * •

$\mathrm{crnf}(t^{\prime})\equiv t_{1}^{\prime}t_{2}^{\prime}$. Then $s\equiv
s_{1}s_{2}$ with $t_{i}^{\prime}\leadsto_{N_{\mathcal{U}}}s_{i}$. By Lemma 37
we have $\mathrm{crnf}(t)\equiv t_{1}t_{2}$ with
$t_{i}\to^{\infty}_{\beta\bot_{\mathcal{U}}}t_{i}^{\prime}$. By the
coinductive hypothesis $t_{i}\leadsto_{N_{\mathcal{U}}}s_{i}$. Hence
$t\leadsto_{N_{\mathcal{U}}}s_{1}s_{2}\equiv s$.

  * •

The case $\mathrm{crnf}(t^{\prime})\equiv\lambda x.u$ is analogous to the
previous one.

###  5.5. Confluence and normalisation

Recall that ${\mathcal{U}}$ is an arbitrary fixed set of strongly meaningless
terms.

######  Theorem 39 (Confluence of the
$\lambda_{\beta\bot_{\mathcal{U}}}^{\infty}$-calculus).

If $t\to^{\infty}_{\beta\bot_{\mathcal{U}}}t_{1}$ and
$t\to^{\infty}_{\beta\bot_{\mathcal{U}}}t_{2}$ then there exists $t_{3}$ such
that $t_{1}\to^{\infty}_{\beta\bot_{\mathcal{U}}}t_{3}$ and
$t_{2}\to^{\infty}_{\beta\bot_{\mathcal{U}}}t_{3}$.

######  Proof 5.30.

By Lemma 34 there are $t_{1}^{\prime},t_{2}^{\prime}$ with
$t_{i}\leadsto_{N_{\mathcal{U}}}t_{i}^{\prime}$ for $i=1,2$. By Theorem 38 we
have $t\leadsto_{N_{\mathcal{U}}}t_{i}^{\prime}$ for $i=1,2$. By Lemma 35 we
have $t_{1}^{\prime}\equiv t_{2}^{\prime}$. Take $t_{3}\equiv
t_{1}^{\prime}\equiv t_{2}^{\prime}$. We have
$t_{i}\leadsto_{N_{\mathcal{U}}}t_{3}$ for $i=1,2$, so
$t_{1}\to^{\infty}_{\beta\bot_{\mathcal{U}}}t_{3}$ and
$t_{2}\to^{\infty}_{\beta\bot_{\mathcal{U}}}t_{3}$ by Lemma 33.

######  Theorem 40 (Normalisation of the
$\lambda_{\beta\bot_{\mathcal{U}}}^{\infty}$-calculus).

For every $t\in\Lambda^{\infty}$ there exists a unique $s\in\Lambda^{\infty}$
in $\beta\bot_{\mathcal{U}}$-normal form such that
$t\to^{\infty}_{\beta\bot_{\mathcal{U}}}s$.

######  Proof 5.31.

By Lemma 34 there is $s$ with $t\leadsto_{N_{\mathcal{U}}}s$. By Lemma 36, $s$
is in $\beta\bot_{\mathcal{U}}$-normal form. By Lemma 33 we have
$t\to^{\infty}_{\beta\bot_{\mathcal{U}}}s$. The uniqueness of $s$ follows from
Theorem 39.

###  5.6. Root-active terms are strongly meaningless

We define the relation $\succ_{x}$ coinductively

$t\succ_{x}xu_{1}\ldots u_{n}u_{1},\ldots,u_{n}\in\Lambda^{\infty}\quad\quad
a\succ_{x}a\quad\quad ts\succ_{x}t^{\prime}s^{\prime}\lx@proof@logical@and
t\succ_{x}t^{\prime}s\succ_{x}s^{\prime}\quad\quad\lambda y.t\succ_{x}\lambda
y.t^{\prime}\lx@proof@logical@and t\succ_{x}t^{\prime}x\neq y$

In other words, $s\succ_{x}s^{\prime}$ iff $s^{\prime}$ may be obtained from
$s$ by changing some arbitrary subterms in $s$ into some terms having the form
$xu_{1}\ldots u_{n}$.

######  Lemma 41.

If $t\succ_{x}t^{\prime}$, $s\succ_{x}s^{\prime}$ and $x\neq y$ then
$t[s/y]\succ_{x}t^{\prime}[s^{\prime}/y]$.

######  Proof 5.32.

By coinduction, analysing $t\succ_{x}t^{\prime}$.

######  Lemma 42.

If $t\succ_{x}s$ and $t\to_{\beta}t^{\prime}$ then there is $s^{\prime}$ with
$t^{\prime}\succ_{x}s^{\prime}$ and $s\to_{\beta}^{\equiv}s^{\prime}$.

######  Proof 5.33.

Induction on $t\to_{\beta}t^{\prime}$. The interesting case is when
$t\equiv(\lambda y.t_{1})t_{2}$, $t^{\prime}\equiv t_{1}[t_{2}/y]$, $s\equiv
s_{1}s_{2}$, $\lambda y.t_{1}\succ_{x}s_{1}$ and $t_{2}\succ_{x}s_{2}$. If
$s_{1}\equiv xu_{1}\ldots u_{m}$ then $t^{\prime}\succ_{x}xu_{1}\ldots
u_{m}s_{2}$ and we may take $s^{\prime}\equiv s$. Otherwise
$s_{1}\equiv\lambda y.s_{1}^{\prime}$ with $t_{1}\succ_{x}s_{1}^{\prime}$ (by
the variable convention $x\neq y$). Then $t^{\prime}\equiv
t_{1}[t_{2}/y]\succ_{x}s_{1}^{\prime}[s_{2}/y]$ by Lemma 41. We may thus take
$s^{\prime}\equiv s_{1}^{\prime}[s_{2}/y]$.

######  Lemma 43.

If $t\succ_{x}s$ and $s\to_{\beta}s^{\prime}$ then there is $t^{\prime}$ with
$t^{\prime}\succ_{x}s^{\prime}$ and $t\to_{\beta}^{\equiv}t^{\prime}$.

######  Proof 5.34.

Induction on $s\to_{\beta}s^{\prime}$, using Lemma 41 for the redex case.

######  Lemma 44.

If $t\succ_{x}t^{\prime}$ and $t$ is in rnf, then so is $t^{\prime}$.

######  Proof 5.35.

Assume $t^{\prime}$ is not in rnf. Then $t^{\prime}\equiv\bot$ or
$t^{\prime}\equiv t_{1}^{\prime}t_{2}^{\prime}$ with $t_{1}^{\prime}$ reducing
to an abstraction. If $t^{\prime}\equiv\bot$ then $t\equiv\bot$, so assume
$t^{\prime}\equiv t_{1}^{\prime}t_{2}^{\prime}$ and
$t_{1}^{\prime}\to^{*}_{\beta}\lambda y.u^{\prime}$ with $x\neq y$. Then
$t\equiv t_{1}t_{2}$ with $t_{i}\succ_{x}t_{i}^{\prime}$. By Lemma 43 there is
$u$ with $t_{1}\to^{*}_{\beta}\lambda y.u$ and $u\succ_{x}u^{\prime}$. But
this implies that $t\equiv t_{1}t_{2}$ is not in rnf. Contradiction.

######  Lemma 45.

If $t_{1},t_{2}\in\Lambda^{\infty}$ and $t_{1}$ has no rnf, then neither does
$t_{1}[t_{2}/x]$.

######  Proof 5.36.

Assume $t_{1}[t_{2}/x]$ has a rnf. Then $t_{1}[t_{2}/x]\to^{*}_{\beta}s$ for
some $s$ in rnf, by Lemma 30. By the variable convention
$t_{1}[t_{2}/x]\succ_{x}t_{1}$. Hence by Lemma 42 there is $s^{\prime}$ such
that $t_{1}\to^{*}_{\beta}s^{\prime}$ and $s\succ_{x}s^{\prime}$. Since $s$ is
in rnf, so is $s^{\prime}$, by Lemma 44. Thus $t_{1}$ has a rnf.
Contradiction.

######  Lemma 46.

If $t\sim_{\mathcal{R}}t^{\prime}$ and $s\sim_{\mathcal{R}}s^{\prime}$ then
$t[s/x]\sim_{\mathcal{R}}t^{\prime}[s^{\prime}/x]$.

######  Proof 5.37.

By coinduction, using Lemma 45.

######  Lemma 47.

If $t\to_{\beta}t^{\prime}$ and $t\sim_{\mathcal{R}}s$ then there is
$s^{\prime}$ with $s\to_{\beta}^{\equiv}s^{\prime}$ and
$t^{\prime}\sim_{\mathcal{R}}s^{\prime}$.

######  Proof 5.38.

Induction on $t\to_{\beta}t^{\prime}$. There are two interesting cases.

  * •

$t,s\in{\mathcal{R}}$, i.e., they have no rnf. Then also
$t^{\prime}\in{\mathcal{R}}$, so we may take $s^{\prime}\equiv s$.

  * •

$t\equiv(\lambda x.t_{1})t_{2}$, $t^{\prime}\equiv t_{1}[t_{2}/x]$,
$s\equiv(\lambda x.s_{1})s_{2}$ and $t_{i}\sim_{\mathcal{R}}s_{i}$. Then
$t^{\prime}\sim_{\mathcal{R}}s_{1}[s_{2}/x]$ by Lemma 46. Hence we may take
$s^{\prime}\equiv s_{1}[s_{2}/x]$.

######  Lemma 48.

If $t$ is in rnf and $t\sim_{\mathcal{R}}s$, then so is $s$.

######  Proof 5.39.

Because $t$ is in rnf, there are three cases.

  * •

$t\equiv a$ with $a\not\equiv\bot$. Then $s\equiv t$, so it is in rnf.

  * •

$t\equiv\lambda x.t^{\prime}$. Then $s\equiv\lambda x.s^{\prime}$, so $s$ is
in rnf.

  * •

$t\equiv t_{1}t_{2}$ and $t_{1}$ does not $\beta$-reduce to an abstraction.
Then $s\equiv s_{1}s_{2}$ with $t_{i}\sim_{\mathcal{R}}s_{i}$. Assume
$s_{1}\to^{*}_{\beta}\lambda x.s^{\prime}$. Then by Lemma 47 there is
$t^{\prime}$ with $t_{1}\to^{*}_{\beta}t^{\prime}\sim_{\mathcal{R}}\lambda
x.s^{\prime}$. But then $t^{\prime}$ must be an abstraction. Contradiction.

######  Corollary 49.

If $t$ has a rnf and $t\sim_{\mathcal{R}}s$, then so does $s$.

######  Proof 5.40.

Follows from Lemma 47 and Lemma 48.

######  Lemma 50.

If $t\to^{\infty}_{\beta}s$ and $t$ has a rnf, then so does $s$.

######  Proof 5.41.

Suppose $t$ has a rnf. Then by Lemma 30 there is $t^{\prime}$ in rnf with
$t\to^{*}_{w}t^{\prime}$. By Theorem 28 and Lemma 29 there is $r$ with
$s\to^{*}_{w}r$ and $t^{\prime}\to^{\infty}_{\beta}r$. Since $t^{\prime}$ is
in rnf, by Lemma 8 so is $r$. Hence $s$ has a rnf $r$.

######  Theorem 51.

The set ${\mathcal{R}}$ of root-active terms is a set of strongly meaningless
terms.

######  Proof 5.42.

We check the axioms. The root-activeness axiom is obvious. The closure axiom
follows from Lemma 7. The substitution axiom follows from Lemma 45. The
overlap axiom follows from the fact that lambda abstractions are in rnf. The
indiscernibility axiom follows from Corollary 49. The expansion axiom follows
from Lemma 50.

######  Corollary 52 (Confluence of the
$\lambda_{\beta\bot_{\mathcal{R}}}^{\infty}$-calculus).

If $t\to^{\infty}_{\beta\bot_{\mathcal{R}}}t_{1}$ and
$t\to^{\infty}_{\beta\bot_{\mathcal{R}}}t_{2}$ then there exists $t_{3}$ such
that $t_{1}\to^{\infty}_{\beta\bot_{\mathcal{R}}}t_{3}$ and
$t_{2}\to^{\infty}_{\beta\bot_{\mathcal{R}}}t_{3}$.

######  Corollary 53 (Normalisation of the
$\lambda_{\beta\bot_{\mathcal{R}}}^{\infty}$-calculus).

For every $t\in\Lambda^{\infty}$ there exists a unique $s\in\Lambda^{\infty}$
in $\beta\bot_{\mathcal{R}}$-normal form such that
$t\to^{\infty}_{\beta\bot_{\mathcal{R}}}s$.

###  5.7. Confluence modulo equivalence of meaningless terms

From confluence of the $\lambda_{\beta\bot_{\mathcal{R}}}^{\infty}$-calculus
we may derive confluence of infinitary $\beta$-reduction
$\to^{\infty}_{\beta}$ modulo equivalence of meaningless terms. The expansion
axiom in not needed for the proof of the following theorem.

######  Theorem 54 (Confluence modulo equivalence of meaningless terms).

If $t\sim_{\mathcal{U}}t^{\prime}$, $t\to^{\infty}_{\beta}s$ and
$t^{\prime}\to^{\infty}_{\beta}s^{\prime}$ then there exist $r,r^{\prime}$
such that $r\sim_{\mathcal{U}}r^{\prime}$, $s\to^{\infty}_{\beta}r$ and
$s^{\prime}\to^{\infty}_{\beta}r^{\prime}$.

######  Proof 5.43.

By Lemma 11 and Lemma 12 it suffices to consider the case $t\equiv
t^{\prime}$. By Corollary 52 there is $u$ with
$s\to^{\infty}_{\beta\bot_{\mathcal{R}}}u$ and
$s^{\prime}\to^{\infty}_{\beta\bot_{\mathcal{R}}}u$. By Theorem 51 and Lemma
22 there are $r,r^{\prime}$ with $s\to^{\infty}_{\beta}r\sim_{{\mathcal{R}}}u$
and $s^{\prime}\to^{\infty}_{\beta}r^{\prime}\sim_{\mathcal{R}}u$. Because
${\mathcal{R}}\subseteq{\mathcal{U}}$, by Lemma 12 we obtain
$r\sim_{\mathcal{U}}r^{\prime}$.

##  6\. Strongly convergent reductions

In this section we prove that the existence of coinductive infinitary
reductions is equivalent to the existence of strongly convergent reductions,
under certain assumptions. As a corollary, this also yields
$\omega$-compression of strongly convergent reductions, under certain
assumptions. The equivalence proof is virtually the same as in [19]. The
notion of strongly convergent reductions is the standard notion of infinitary
reductions used in non-coinductive treatments of infinitary lambda calculus.

On the set of infinitary lambda terms we define a metric $d$ by

$d(t,s)=\inf\\{2^{-n}\mid t^{\upharpoonright n}\equiv
s^{\upharpoonright{n}}\\}$

where $r^{\upharpoonright n}$ for $r\in\Lambda^{\infty}$ is defined as the
infinitary lambda term obtained by replacing all subterms of $r$ at depth $n$
by $\bot$. This defines a metric topology on the set of infinitary lambda
terms. Let $R\subseteq\Lambda^{\infty}\times\Lambda^{\infty}$ and let $\zeta$
be an ordinal. A map $f:\\{\gamma\leq\zeta\\}\to\Lambda^{\infty}$ together
with reduction steps $\sigma_{\gamma}:f(\gamma)\to_{R}f(\gamma+1)$ for
$\gamma<\zeta$ is a _strongly convergent $R$-reduction sequence of length
$\zeta$ from $f(0)$ to $f(\zeta)$_ if the following conditions hold:

  1. (1)

if $\delta\leq\zeta$ is a limit ordinal then $f(\delta)$ is the limit in the
metric topology on infinite terms of the ordinal-indexed sequence
$(f(\gamma))_{\gamma<\delta}$,

  2. (2)

if $\delta\leq\zeta$ is a limit ordinal then for every $d\in\mathbb{N}$ there
exists $\gamma<\delta$ such that for all $\gamma^{\prime}$ with
$\gamma\leq\gamma^{\prime}<\delta$ the redex contracted in the step
$\sigma_{\gamma^{\prime}}$ occurs at depth greater than $d$.

We write $s\xrightarrow{S,\zeta}_{R}t$ if $S$ is a strongly convergent
$R$-reduction sequence of length $\zeta$ from $s$ to $t$.

A relation ${\to}\subseteq\Lambda^{\infty}\times\Lambda^{\infty}$ is
_appendable_ if $t_{1}\to^{\infty}t_{2}\to t_{3}$ implies
$t_{1}\to^{\infty}t_{3}$. We define $\to^{2\infty}$ as the infinitary closure
of $\to^{\infty}$. We write $\to^{\infty*}$ for the transitive-reflexive
closure of $\to^{\infty}$.

######  Lemma 55.

If $\to$ is appendable then $t_{1}\to^{\infty}t_{2}\to^{\infty}t_{3}$ implies
$t_{1}\to^{\infty}t_{3}$.

######  Proof 6.1.

By coinduction. This has essentially been shown in [19, Lemma 4.5].

######  Lemma 56.

If $\to$ is appendable then $s\to^{2\infty}t$ implies $s\to^{\infty}t$.

######  Proof 6.2.

By coinduction. There are three cases.

  * •

$t\equiv a$. Then $s\to^{\infty*}a$, so $s\to^{\infty}a$ by Lemma 55.

  * •

$t\equiv t_{1}t_{2}$. Then there are $t_{1}^{\prime},t_{2}^{\prime}$ with
$s\to^{\infty*}t_{1}^{\prime}t_{2}^{\prime}$ and
$t_{i}^{\prime}\to^{2\infty}t_{i}$. By Lemma 55 we have
$s\to^{\infty}t_{1}^{\prime}t_{2}^{\prime}$, so there are $u_{1},u_{2}$ with
$s\to^{*}u_{1}u_{2}$ and $u_{i}\to^{\infty}t_{i}^{\prime}$. Then
$u_{i}\to^{2\infty}t_{i}$. By the coinductive hypothesis
$u_{i}\to^{\infty}t_{i}$. Hence $s\to^{\infty}t_{1}t_{2}\equiv t$.

  * •

$t\equiv\lambda x.r$. Then by Lemma 55 there is $s^{\prime}$ with
$s\to^{\infty}\lambda x.s^{\prime}$ and $s^{\prime}\to^{2\infty}r$. So there
is $s_{0}$ with $s\to^{*}\lambda x.s_{0}$ and $s_{0}\to^{\infty}s^{\prime}$.
Then also $s_{0}\to^{2\infty}r$. By the coinductive hypothesis
$s_{0}\to^{\infty}r$. Thus $s\to^{\infty}\lambda x.r\equiv t$.

######  Theorem 57.

For every $R\subseteq\Lambda^{\infty}\times\Lambda^{\infty}$ such that
$\to_{R}$ is appendable, and for all $s,t\in\Lambda^{\infty}$, we have the
equivalence: $s\to^{\infty}_{R}t$ iff there exists a strongly convergent
$R$-reduction sequence from $s$ to $t$. Moreover, if $s\to^{\infty}_{R}t$ then
the sequence may be chosen to have length at most $\omega$.

######  Proof 6.3.

The proof is a straightforward generalisation of the proof of Theorem 3 in
[19].

Suppose that $s\to^{\infty}_{R}t$. By traversing the infinite derivation tree
of $s\to^{\infty}_{R}t$ and accumulating the finite prefixes by concatenation,
we obtain a reduction sequence of length at most $\omega$ which satisfies the
depth requirement by construction.

For the other direction, by induction on $\zeta$ we show that if
$s\xrightarrow{S,\zeta}_{R}t$ then $s\to^{2\infty}_{R}t$, which suffices for
$s\to^{\infty}_{R}t$ by Lemma 56. There are three cases.

  * •

$\zeta=0$. If $s\xrightarrow{S,0}_{R}t$ then $s\equiv t$, so
$s\to^{2\infty}_{R}t$.

  * •

$\zeta=\gamma+1$. If $s\xrightarrow{S,\gamma+1}_{R}t$ then
$s\xrightarrow{S^{\prime},\gamma}_{R}s^{\prime}\to_{R}t$. Hence
$s\to^{2\infty}_{R}s^{\prime}$ by the inductive hypothesis. Then
$s\to^{\infty}_{R}s^{\prime}\to_{R}t$ by Lemma 56. So $s\to^{\infty}_{R}t$
because $\to_{R}$ is appendable.

  * •

$\zeta$ is a limit ordinal. By coinduction we show that if
$s\xrightarrow{S,\zeta}_{R}t$ then $s\to^{2\infty}_{R}t$. By the depth
condition there is $\gamma<\zeta$ such that for every $\delta\geq\gamma$ the
redex contracted in $S$ at $\delta$ occurs at depth greater than zero. Let
$t_{\gamma}$ be the term at index $\gamma$ in $S$. Then by the inductive
hypothesis we have $s\to^{2\infty}_{R}t_{\gamma}$, and thus
$s\to^{\infty}_{R}t_{\gamma}$ by Lemma 56. There are three cases.

    * –

$t_{\gamma}\equiv a$. This is impossible because then there can be no
reduction of $t_{\gamma}$ at depth greater than zero.

    * –

$t_{\gamma}\equiv\lambda x.r$. Then $t\equiv\lambda x.u$ and
$r\xrightarrow{S^{\prime},\delta}_{R}u$ with $\delta\leq\zeta$. Hence
$r\to^{2\infty}_{R}u$ by the coinductive hypothesis if $\delta=\zeta$, or by
the inductive hypothesis if $\delta<\zeta$. Since $s\to^{\infty}_{R}\lambda
x.r$ we obtain $s\to^{2\infty}_{R}\lambda x.u\equiv t$.

    * –

$t_{\gamma}\equiv t_{1}t_{2}$. Then $t\equiv u_{1}u_{2}$ and the tail of the
reduction $S$ past $\gamma$ may be split into two parts:
$t_{i}\xrightarrow{S_{i},\delta_{i}}_{R}u_{i}$ with $\delta_{i}\leq\zeta$ for
$i=0,1$. Then $t_{i}\to^{2\infty}_{R}u_{i}$ by the inductive and/or the
coinductive hypothesis. Since $s\to^{\infty}_{R}t_{1}t_{2}$ we obtain
$s\to^{2\infty}_{R}u_{1}u_{2}\equiv t$.

######  Corollary 58 ($\omega$-compression).

If $\to_{R}$ is appendable and there exists a strongly convergent
$R$-reduction sequence from $s$ to $t$ then there exists such a sequence of
length at most $\omega$.

######  Corollary 59.

Let ${\mathcal{U}}$ be a set of strongly meaningless terms.

  * •

$s\to^{\infty}_{\beta\bot_{\mathcal{U}}}t$ iff there exists a strongly
convergent $\beta\bot_{\mathcal{U}}$-reduction sequence from $s$ to $t$.

  * •

$s\to^{\infty}_{\beta}t$ iff there exists a strongly convergent
$\beta$-reduction sequence from $s$ to $t$.

######  Proof 6.4.

By Theorem 57 it suffices to show that $\to_{\beta\bot_{\mathcal{U}}}$ and
$\to_{\beta}$ are appendable. For $\to_{\beta\bot_{\mathcal{U}}}$ this follows
from Lemma 25 and Corollary 26. For $\to_{\beta}$ this follows from Lemma 6.

##  7\. The formalisation

The results of this paper have been formalised in the Coq proof assistant. The
formalisation is available at:

https://github.com/lukaszcz/infinitary-confluence

The formalisation contains all results of Section 5. We did not formalise the
proof from Section 6 of the equivalence between the coinductive definition of
the infinitary reduction relation and the standard notion of strongly
convergent reductions.

In our formalisation we use a representation of infinitary lambda terms with
de Bruijn indices, and we do not allow constants except $\bot$. Hence, the
results about $\alpha$-conversion alluded to in Section 4 are not formalised
either. Because the formalisation is based on de Bruijn indices, many tedious
lifting lemmas need to be proved. These lemmas are present only in the
formalisation, but not in the paper.

In general, the formalisation follows closely the text of the paper. Each
lemma from Section 5 has a corresponding statement in the formalisation
(annotated with the lemma number from the paper). There are, however, some
subtleties, described below.

One difficulty with a Coq formalisation of our results is that in Coq the
coinductively defined equality (bisimilarity) $=$ on infinite terms (see
Definition 3) is not identical with Coq’s definitional equality $\equiv$. In
the paper we use $\equiv$ and $=$ interchangeably, following Proposition 2. In
the formalisation we needed to formulate our definitions “modulo”
bisimilarity. For instance, the inductive definition of the transitive-
reflexive closure $R^{*}$ of a relation $R$ on infinite terms is as follows.

  1. (1)

If $t_{1}=t_{2}$ then $R^{*}t_{1}t_{2}$ (where $=$ denotes bisimilarity
coinductively defined like in Definition 3).

  2. (2)

If $Rt_{1}t_{2}$ and $R^{*}t_{2}t_{3}$ then $R^{*}t_{1}t_{3}$.

Changing the first point to

  1. (1)

$R^{*}tt$ for any term $t$

would not work with our formalisation. Similarly, the formal definition of the
compatible closure of a relation $R$ follows the inductive rules

$\begin{array}[]{cccc}s\to_{R}t\langle s,t\rangle\in R&\quad
st\to_{R}s^{\prime}t^{\prime}\lx@proof@logical@and
s\to_{R}s^{\prime}t=t^{\prime}&\quad
st\to_{R}s^{\prime}t^{\prime}\lx@proof@logical@and
t\to_{R}t^{\prime}s=s^{\prime}&\quad\lambda x.s\to_{R}\lambda
x.s^{\prime}s\to_{R}s^{\prime}\end{array}$

where $=$ denotes the coinductively defined bisimilarity relation.

Another limitation of Coq is that it is not possible to directly prove by
coinduction statements of the form $\forall\vec{x}.\varphi(\vec{x})\to
R_{1}(\vec{x})\land R_{2}(\vec{x})$, i.e., statements with a conjuction of two
coinductive predicates. Instead, we show $\forall\vec{x}.\varphi(\vec{x})\to
R_{1}(\vec{x})$ and $\forall\vec{x}.\varphi(\vec{x})\to R_{2}(\vec{x})$
separately. In all our coinductive proofs we use the coinductive hypothesis in
a way that makes this separation possible.

The formalisation assumes the following axioms.

  1. (1)

The constructive indefinite description axiom:

$\forall A:\mathrm{Type}.\forall P:A\to\mathrm{Prop}.(\exists
x:A.Px)\to\\{x:A\mid Px\\}.$

This axiom states that if there exists an object $x$ of type $A$ satisfying
the predicate $P$, then it is possible to choose a fixed such object. This is
not provable in the standard logic of Coq. We need this assumption to be able
to define the implicit functions in some coinductive proofs which show the
existence of an infinite object, when the form of this object depends on which
case in the definition of some (co)inductive predicate holds. More precisely,
the indefinite description axiom is needed in the proof of Lemma 22, in the
definition of canonical root normal forms (Definition 5.3), and in the proofs
of Lemma 11, Lemma 13 and Lemma 34.

  2. (2)

Excluded middle for the property of being in root normal form: for every term
$t$, either $t$ is in root normal form or not.

  3. (3)

Excluded middle for the property of having a root normal form: for every term
$t$, either $t$ has a root normal form or not.

  4. (4)

Excluded middle for the property of belonging to a set of strongly meaningless
terms: for any set of strongly meaningless terms ${\mathcal{U}}$ and any term
$t$, either $t\in{\mathcal{U}}$ or $t\notin{\mathcal{U}}$.

Note that the last axiom does not constructively imply the third. We define
being root-active as not having a root normal form. In fact, we need the third
axiom to show that if a term does not belong to a set of meaningless terms
then it has a root normal form.

The first axiom could probably be avoided by making the reduction relations
$\mathrm{Set}$-valued instead of $\mathrm{Prop}$-valued. We do not use the
impredicativity of $\mathrm{Prop}$. The reason why we chose to define the
relations as $\mathrm{Prop}$-valued is that certain automated proof search
tactics work better with $\mathrm{Prop}$-valued relations, which makes the
formalisation easier to carry out.

Because the $\bot_{\mathcal{U}}$-reduction rule, for any set of meaningless
terms ${\mathcal{U}}$, requires an oracle to check whether it is applicable,
the present setup is inherently classical. It is an interesting research
question to devise a constructive theory of meaningless terms.

Aside of the axioms (1)–(4), everything else from Section 5 is formalised in
the constructive logic of Coq, including the proof of Theorem 28 only cited in
this paper. Our formalisation of Theorem 28 closely follows [19].

In our formalisation we extensively used the CoqHammer tool [13].

##  8\. Conclusions

We presented new and formal coinductive proofs of the following results.

  1. (1)

Confluence and normalisation of Böhm reduction over any set of strongly
meaningless terms.

  2. (2)

Confluence and normalisation of Böhm reduction over root-active terms, by
showing that root-active terms are strongly meaningless.

  3. (3)

Confluence of infinitary $\beta$-reduction modulo any set of meaningless terms
(expansion axiom not needed).

We formalised these results in Coq. Our formalisation uses a definition of
infinitary lambda terms based on de Bruijn indices. Strictly speaking, the
precise relation of this definition to other definitions of infinitary lambda
terms in the literature has not been established. We leave this for future
work. The issue of the equivalence of various definitions of infinitary lambda
terms is not necessarily trivial [32, 33].

By a straightforward generalisation of a result in [19] we also proved
equivalence, in the sense of existence, of the coinductive definitions of
infinitary rewriting relations with the standard definitions based on strong
convergence. However, we did not formalise this result.

In Section 3 we explained how to elaborate our coinductive proofs by reducing
them to proofs by transfinite induction and thus eliminating coinduction. This
provides one way to understand and verify our proofs without resorting to a
formalisation. After properly understanding the observations of Section 3 it
should be “clear” that coinduction may in principle be eliminated in the
described manner. We use the word “clear” in the same sense that it is “clear”
that the more sophisticated inductive constructions commonly used in the
literature can be formalised in ZFC set theory. Of course, this notion of
“clear” may always be debated. The only way to make this completely precise is
to create a formal system based on Section 3 in which our proofs could be
interpreted reasonably directly. We do not consider the observations of
Section 3 to be novel or particularly insightful. However, distilling them
into a formal system could perhaps arise some interest. This is left for
future work.

## References

  * [1] Patrick Bahr.  Partial order infinitary term rewriting and Böhm trees.  In Christopher Lynch, editor, Proceedings of the 21st International Conference on Rewriting Techniques and Applications, RTA 2010, July 11-13, 2010, Edinburgh, Scottland, UK, volume 6 of LIPIcs, pages 67–84. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2010\.
  * [2] Patrick Bahr.  Partial order infinitary term rewriting.  Logical Methods in Computer Science, 10(2), 2014.
  * [3] Patrick Bahr.  Strict ideal completions of the lambda calculus.  In Hélène Kirchner, editor, 3rd International Conference on Formal Structures for Computation and Deduction, FSCD 2018, July 9-12, 2018, Oxford, UK, volume 108 of LIPIcs, pages 8:1–8:16. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2018.
  * [4] Henk Barendregt and Jan Willem Klop.  Applications of infinitary lambda calculus.  Information and Computation, 207(5):559–582, 2009.
  * [5] Henk P. Barendregt.  The Lambda Calculus: Its Syntax and Semantics.  North Holland, 2nd edition, 1984.
  * [6] Alessandro Berarducci.  Infinite lambda-calculus and non-sensible models.  In Aldo Ursini and Paolo Aglianò, editors, Logic and Algebra, volume 180 of Lecture Notes in Pure and Applied Mathematics, pages 339–378. CRC Press, 1996.
  * [7] Yves Bertot and Pierre Castéran.  Interactive Theorem Proving and Program Development: Coq’Art: the Calculus of Inductive Constructions, chapter 13.  Springer, 2004.
  * [8] Marc Bezem, Keiko Nakata, and Tarmo Uustalu.  On streams that are finitely red.  Logical Methods in Computer Science, 8:1–20, 2012.
  * [9] Adam Chlipala.  Certified Programming with Dependent Types, chapter 5.  The MIT Press, 2013.
  * [10] Łukasz Czajka.  A coinductive confluence proof for infinitary lambda-calculus.  In Rewriting and Typed Lambda Calculi - Joint International Conference, RTA-TLCA 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 14-17, 2014. Proceedings, pages 164–178, 2014\.
  * [11] Łukasz Czajka.  Coinduction: an elementary approach.  CoRR, abs/1501.04354, 2015.
  * [12] Łukasz Czajka.  Confluence of nearly orthogonal infinitary term rewriting systems.  In RTA 2015, pages 106–126, 2015.
  * [13] Łukasz Czajka and Cezary Kaliszyk.  Hammer for Coq: Automation for dependent type theory.  J. Autom. Reasoning, 61(1-4):423–453, 2018.
  * [14] Brian A. Davey and Hilary A. Priestley.  Introduction to Lattices and Order.  Cambridge University Press, 2nd edition, 2002.
  * [15] N. G. de Bruijn.  Lambda-calculus notation with nameless dummies: a tool for automatic formula manipulation with application to the Church-Rosser theorem.  Indagationes Mathematicae, 34(5):381–392, 1972.
  * [16] Jörg Endrullis, Helle Hvid Hansen, Dimitri Hendriks, Andrew Polonsky, and Alexandra Silva.  A coinductive framework for infinitary rewriting and equational reasoning.  In RTA 2015, 2015.
  * [17] Jörg Endrullis, Helle Hvid Hansen, Dimitri Hendriks, Andrew Polonsky, and Alexandra Silva.  Coinductive foundations of infinitary rewriting and infinitary equational logic.  Logical Methods in Computer Science, 14(1), 2018.
  * [18] Jörg Endrullis, Dimitri Hendriks, and Jan Willem Klop.  Highlights in infinitary rewriting and lambda calculus.  Theoretical Computer Science, 464:48–71, 2012.
  * [19] Jörg Endrullis and Andrew Polonsky.  Infinitary rewriting coinductively.  In Nils Anders Danielsson and Bengt Nordström, editors, TYPES, volume 19 of LIPIcs, pages 16–27. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2011.
  * [20] Bart Jacobs and Jan J.M.M. Rutten.  An introduction to (co)algebras and (co)induction.  In Advanced Topics in Bisimulation and Coinduction, pages 38–99. Cambridge University Press, 2011.
  * [21] Felix Joachimski.  Confluence of the coinductive [lambda]-calculus.  Theoretical Computer Science, 311(1-3):105–119, 2004.
  * [22] Richard Kennaway and Fer-Jan de Vries.  Infinitary rewriting.  In Terese, editor, Term Rewriting Systems, volume 55 of Cambridge Tracts in Theoretical Computer Science, chapter 12, pages 668–711. Cambridge University Press, 2003.
  * [23] Richard Kennaway, Jan Willem Klop, M. Ronan Sleep, and Fer-Jan de Vries.  Infinitary lambda calculi and Böhm models.  In Jieh Hsiang, editor, RTA, volume 914 of Lecture Notes in Computer Science, pages 257–270. Springer, 1995.
  * [24] Richard Kennaway, Jan Willem Klop, M. Ronan Sleep, and Fer-Jan de Vries.  Infinitary lambda calculus.  Theoretical Computer Science, 175(1):93–125, 1997.
  * [25] Richard Kennaway, Paula Severi, M. Ronan Sleep, and Fer-Jan de Vries.  Infinitary rewriting: From syntax to semantics.  In Aart Middeldorp, Vincent van Oostrom, Femke van Raamsdonk, and Roel C. de Vrijer, editors, Processes, Terms and Cycles: Steps on the Road to Infinity, Essays Dedicated to Jan Willem Klop, on the Occasion of His 60th Birthday, volume 3838 of Lecture Notes in Computer Science, pages 148–172. Springer, 2005.
  * [26] Richard Kennaway, Vincent van Oostrom, and Fer-Jan de Vries.  Meaningless terms in rewriting.  Journal of Functional and Logic Programming, 1:1–35, 1999.
  * [27] Jeroen Ketema and Jakob Grue Simonsen.  Infinitary combinatory reduction systems: Confluence.  Logical Methods in Computer Science, 5(4), 2009.
  * [28] Jeroen Ketema and Jakob Grue Simonsen.  Infinitary combinatory reduction systems: Normalising reduction strategies.  Logical Methods in Computer Science, 6(1), 2010.
  * [29] Jeroen Ketema and Jakob Grue Simonsen.  Infinitary combinatory reduction systems.  Information and Computation, 209(6):893–926, 2011.
  * [30] Jan Willem Klop and Roel C. de Vrijer.  Infinitary normalization.  In Sergei N. Artëmov, Howard Barringer, Artur S. d’Avila Garcez, Luís C. Lamb, and John Woods, editors, We Will Show Them! Essays in Honour of Dov Gabbay, Volume Two, pages 169–192. College Publications, 2005.
  * [31] Dexter Kozen and Alexandra Silva.  Practical coinduction.  Mathematical Structures in Computer Science, 27(7):1132–1152, 2017\.
  * [32] Alexander Kurz, Daniela Petrisan, Paula Severi, and Fer-Jan de Vries.  An alpha-corecursion principle for the infinitary lambda-calculus.  In CMCS, pages 130–149, 2012.
  * [33] Alexander Kurz, Daniela Petrisan, Paula Severi, and Fer-Jan de Vries.  Nominal coalgebraic data types with applications to lambda calculus.  Logical Methods in Computer Science, 9:1–51, 2013.
  * [34] Xavier Leroy and Hervé Grall.  Coinductive big-step operational semantics.  Information and Computation, 207(2):284–304, 2009.
  * [35] Jean-Jacques Lévy.  An algebraic interpretation of the lambda beta - calculus and a labeled lambda - calculus.  In Corrado Böhm, editor, Lambda-Calculus and Computer Science Theory, Proceedings of the Symposium Held in Rome, March 25-27, 1975, volume 37 of Lecture Notes in Computer Science, pages 147–165. Springer, 1975.
  * [36] Giuseppe Longo.  Set-theoretical models of $\lambda$-calculus: theories, expansions, isomorphisms.  Annals of Pure and Applied Logic, 24(2):153 – 188, 1983.
  * [37] Keiko Nakata and Tarmo Uustalu.  Resumptions, weak bisimilarity and big-step semantics for while with interactive I/O: An exercise in mixed induction-coinduction.  In L. Aceto and P. Sobociński, editors, Seventh Workshop on Structural Operational Semantics (SOS ’10), pages 57–75, 2010.
  * [38] Jan J.M.M. Rutten.  Universal coalgebra: a theory of systems.  Theoretical Computer Science, 249(1):3–80, 2000.
  * [39] Davide Sangiorgi.  Introduction to Bisimulation and Coinduction.  Cambridge University Press, 2012.
  * [40] Paula Severi and Fer-Jan de Vries.  An extensional Böhm model.  In Sophie Tison, editor, RTA, volume 2378 of Lecture Notes in Computer Science, pages 159–173. Springer, 2002.
  * [41] Paula Severi and Fer-Jan de Vries.  Order structures on Böhm-like models.  In C.-H. Luke Ong, editor, Computer Science Logic, 19th International Workshop, CSL 2005, 14th Annual Conference of the EACSL, Oxford, UK, August 22-25, 2005, Proceedings, volume 3634 of Lecture Notes in Computer Science, pages 103–118. Springer, 2005.
  * [42] Paula Severi and Fer-Jan de Vries.  Decomposing the lattice of meaningless sets in the infinitary lambda calculus.  In Lev D. Beklemishev and Ruy J. G. B. de Queiroz, editors, Logic, Language, Information and Computation - 18th International Workshop, WoLLIC 2011, Philadelphia, PA, USA, May 18-20, 2011. Proceedings, volume 6642 of Lecture Notes in Computer Science, pages 210–227. Springer, 2011\.
  * [43] Paula Severi and Fer-Jan de Vries.  Weakening the axiom of overlap in infinitary lambda calculus.  In Manfred Schmidt-Schauß, editor, Proceedings of the 22nd International Conference on Rewriting Techniques and Applications, RTA 2011, May 30 - June 1, 2011, Novi Sad, Serbia, volume 10 of LIPIcs, pages 313–328. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2011.
  * [44] Paula Severi and Fer-Jan de Vries.  The infinitary lambda calculus of the infinite eta Böhm trees.  Mathematical Structures in Computer Science, 27(5):681–733, 2017\.

##  Appendix A A set of meaningless terms not satisfying the expansion axiom

We recall the definitions from page 14. Let ${\mathsf{O}}$ be the _ogre_
satisfying ${\mathsf{O}}\equiv\lambda x.{\mathsf{O}}$. A term $t$ is _head-
active_ if $t\equiv\lambda x_{1}\ldots x_{n}.rt_{1}\ldots t_{m}$ with
$r\in{\mathcal{R}}$ and $n,m\geq 0$. Define:

  * •

${\mathcal{H}}=\\{t\in\Lambda^{\infty}\mid t\to^{*}_{\beta}t^{\prime}\text{
with }t^{\prime}\text{ head-active}\\}$,

  * •

${\mathcal{O}}=\\{t\in\Lambda^{\infty}\mid t\to^{*}_{\beta}{\mathsf{O}}\\}$,

  * •

${\mathcal{U}}={\mathcal{H}}\cup{\mathcal{O}}$.

We will show that ${\mathcal{U}}$ is a set of meaningless terms. The proofs in
this appendix rely on the results established in the paper. In particular, we
use that ${\mathcal{R}}$ is a set of strongly meaningless terms and that
$\to^{\infty}_{\beta}$ is confluent modulo ${\mathcal{R}}$.

######  Lemma 60.

  1. (1)

If $t\in{\mathcal{U}}$ then $ts\in{\mathcal{U}}$.

  2. (2)

If $t\in{\mathcal{U}}$ then $\lambda x.t\in{\mathcal{U}}$.

  3. (3)

If $t\in{\mathcal{U}}$ then $t[s/x]\in{\mathcal{U}}$.

######  Proof A.1.

Follows from definitions and the fact that ${\mathcal{R}}$ satisfies the
substitution axiom.

######  Lemma 61.

If $t\to^{\infty}_{\beta}t^{\prime}$ and $t\in{\mathcal{H}}$ then
$t^{\prime}\in{\mathcal{H}}$.

######  Proof A.2.

We have $t\to^{*}_{\beta}u$ with $u$ head-active. By confluence modulo
${\mathcal{R}}$ there are $s,s^{\prime}$ with $u\to^{\infty}_{\beta}s$,
$t^{\prime}\to^{\infty}_{\beta}s^{\prime}$ and
$s\sim_{\mathcal{R}}s^{\prime}$. It follows from the closure and
indiscernibility axioms for ${\mathcal{R}}$ that $s^{\prime}$ is head-active.
Now, using the expansion axiom for ${\mathcal{R}}$ one may show that there is
a head-active $w$ such that
$t^{\prime}\to^{*}_{\beta}w\to^{\infty}_{\beta}s^{\prime}$.

######  Lemma 62.

If $t\to^{\infty}_{\beta}t^{\prime}$ and $t\in{\mathcal{O}}$ then
$t^{\prime}\in{\mathcal{O}}$.

######  Proof A.3.

We have $t\to^{*}_{\beta}{\mathsf{O}}$. Because the reduction is finite, no
$\beta$-contractions occur below a fixed depth $d$. We can write
${\mathsf{O}}\equiv\lambda\vec{x}.{\mathsf{O}}$ where on the right side
${\mathsf{O}}$ occurs below depth $d$. Then there is $u$ with exactly one
occurrence of $z$ (where $z\notin\vec{x}$) such that
$u\to^{*}_{\beta}\lambda\vec{x}.z$ and $t\equiv u[{\mathsf{O}}/z]$.

Write $s\succ_{z}^{\mathsf{O}}s^{\prime}$ if $s^{\prime}$ may be obtained from
$s$ by changing some ${\mathsf{O}}$ subterms in $s$ into some terms having the
form $zu_{1}\ldots u_{n}$, defined coinductively analogously to Definition
5.6. One shows:

  1. (1)

if $s\succ_{z}^{\mathsf{O}}s^{\prime}$ and $s\to^{*}_{\beta}w$ then there is
$w^{\prime}$ with $s^{\prime}\to^{*}_{\beta}w^{\prime}$ and
$w\succ_{z}^{\mathsf{O}}w^{\prime}$,

  2. (2)

if $s\succ_{z}^{\mathsf{O}}s^{\prime}$ and
$s^{\prime}\to^{*}_{\beta}w^{\prime}$ then there is $w$ with
$s\to^{*}_{\beta}w$ and $w\succ_{z}^{\mathsf{O}}w^{\prime}$,

  3. (3)

if $s\succ_{z}^{\mathsf{O}}s^{\prime}$ and $s\to^{\infty}_{\beta}w$ then there
is $w^{\prime}$ with $s^{\prime}\to^{\infty}_{\beta}w^{\prime}$ and
$w\succ_{z}^{\mathsf{O}}w^{\prime}$,

The first two points are proved by induction. The third one follows from the
first one using coinduction.

Hence, there exists $u^{\prime}$ such that $u\to^{\infty}_{\beta}u^{\prime}$,
and $t^{\prime}\succ_{z}^{\mathsf{O}}u^{\prime}$. By confluence modulo
${\mathcal{R}}$ and the fact that $\lambda\vec{x}.z$ is a finite normal form,
we have $u^{\prime}\to^{*}_{\beta}\lambda\vec{x}.z$. Thus there is $w$ with
$t^{\prime}\to^{*}_{\beta}w\succ_{z}^{\mathsf{O}}\lambda\vec{x}.z$. This is
possible only when $w\equiv{\mathsf{O}}$.

######  Corollary 63.

If $t\to^{\infty}_{\beta}t^{\prime}$ and $t\in{\mathcal{U}}$ then
$t^{\prime}\in{\mathcal{U}}$.

######  Lemma 64.

If $t_{1}\sim_{\mathcal{U}}s_{1}$ and $t_{2}\sim_{\mathcal{U}}s_{2}$ then
$t_{1}[t_{2}/x]\sim_{\mathcal{U}}s_{1}[s_{2}/x]$.

######  Proof A.4.

By coinduction, using Lemma 60(3).

######  Lemma 65.

If $t\to_{\beta}t^{\prime}$ and $t\sim_{\mathcal{U}}s$ then there is
$s^{\prime}$ with $s\to_{\beta}^{\equiv}s^{\prime}$ and
$t^{\prime}\sim_{\mathcal{U}}s^{\prime}$.

######  Proof A.5.

Induction on $t\to_{\beta}t^{\prime}$. If the case $t,s\in{\mathcal{U}}$ in
the definition of $t\sim_{\mathcal{U}}s$ holds, then
$t^{\prime}\in{\mathcal{U}}$ by Corollary 63, so
$t^{\prime}\sim_{\mathcal{U}}s$ and we may take $s^{\prime}\equiv s$. So
assume otherwise. Then all cases follow directly from the inductive hypothesis
except when $t$ is the contracted $\beta$-redex. Then $t\equiv(\lambda
x.t_{1})t_{2}$ and $t^{\prime}\equiv t_{1}[t_{2}/x]$ and $s=s_{0}s_{2}$ with
$\lambda x.t_{1}\sim_{\mathcal{U}}s_{0}$ and $t_{2}\sim_{\mathcal{U}}s_{2}$.
If $\lambda x.t_{1},s_{0}\in{\mathcal{U}}$ then $t,s\in{\mathcal{U}}$ by Lemma
60, and thus $t^{\prime}\in{\mathcal{U}}$ by Corollary 63, and thus
$t^{\prime}\sim_{\mathcal{U}}s$ and we may take $s^{\prime}\equiv s$.
Otherwise, $s_{0}\equiv\lambda x.s_{1}$ with $t_{1}\sim_{\mathcal{U}}s_{1}$.
By Lemma 64 we have
$s\to_{\beta}s_{1}[s_{2}/x]\sim_{\mathcal{U}}t_{1}[t_{2}/x]\equiv t^{\prime}$,
so we take $s^{\prime}\equiv s_{1}[s_{2}/x]$.

######  Lemma 66.

If $t\in{\mathcal{R}}$ and $t\sim_{\mathcal{U}}t^{\prime}$ then
$t^{\prime}\in{\mathcal{U}}$.

######  Proof A.6.

Assume $t^{\prime}\to^{\infty}_{\beta}s_{0}$ with $s_{0}$ in rnf. Then by
Lemma 30 there is $s^{\prime}$ in rnf with
$t^{\prime}\to^{*}_{\beta}s^{\prime}$. By Lemma 65 there is $s$ with
$t\to^{*}_{\beta}s$ and $s\sim_{\mathcal{U}}s^{\prime}$. If
$s,s^{\prime}\in{\mathcal{U}}$ then $t^{\prime}\in{\mathcal{U}}$. Otherwise,
because $t\in{\mathcal{R}}$, we must have $s\equiv s_{1}s_{2}$,
$s^{\prime}\equiv s_{1}^{\prime}s_{2}^{\prime}$ with
$s_{i}\sim_{\mathcal{U}}s_{i}^{\prime}$. Because $t\in{\mathcal{R}}$ and
$t\to^{*}_{\beta}s_{1}s_{2}$, there exists $u$ such that
$s_{1}\to^{*}_{\beta}\lambda x.u$. Then by Lemma 65 there is $u_{0}$ with
$s_{1}^{\prime}\to^{*}_{\beta}u_{0}\sim_{\mathcal{U}}\lambda x.u$. If
$u_{0},\lambda.u\in{\mathcal{U}}$ then $s_{1}^{\prime}\in{\mathcal{U}}$, and
thus $s^{\prime}\in{\mathcal{U}}$, and thus $t^{\prime}\in{\mathcal{U}}$.
Otherwise $u_{0}\equiv\lambda x.u^{\prime}$ with
$u\sim_{\mathcal{U}}u^{\prime}$. But this contradicts that $s^{\prime}$ is in
rnf.

######  Lemma 67.

If $t\in{\mathcal{U}}$ and $t\sim_{\mathcal{U}}t^{\prime}$ then
$t^{\prime}\in{\mathcal{U}}$.

######  Proof A.7.

First assume $t\in{\mathcal{H}}$, i.e., $t\to^{*}_{\beta}u\equiv\lambda
x_{1}\ldots x_{n}.rt_{1}\ldots t_{m}$ with $r\in{\mathcal{R}}$. By Lemma 65
there is $u$ with $t^{\prime}\to^{*}_{\beta}u^{\prime}\sim_{\mathcal{U}}u$. We
may assume $u^{\prime}\equiv\lambda x_{1}\ldots
x_{n}.r^{\prime}t_{1}^{\prime}\ldots t_{m}^{\prime}$ with
$r^{\prime}\sim_{\mathcal{U}}r$ (otherwise $u^{\prime}\in{\mathcal{U}}$, using
Lemma 60, so $t^{\prime}\in{\mathcal{U}}$). But then
$r^{\prime}\in{\mathcal{R}}$ by Lemma 66. Hence
$t^{\prime}\in{\mathcal{H}}\subseteq{\mathcal{U}}$.

Now assume $t\in{\mathcal{O}}$, i.e., $t\to^{*}_{\beta}{\mathsf{O}}$. By Lemma
65 there is $u^{\prime}$ with
$t^{\prime}\to^{*}_{\beta}u^{\prime}\sim_{\mathcal{U}}{\mathsf{O}}$. Using
Lemma 60 one checks that $u^{\prime}\sim_{\mathcal{U}}{\mathsf{O}}$ implies
$u^{\prime}\in{\mathcal{U}}$. Then also $t^{\prime}\in{\mathcal{U}}$.

######  Theorem 68.

${\mathcal{U}}$ is a set of meaningless terms.

######  Proof A.8.

The closure axiom follows from Corollary 63. The substitution axiom follows
from Lemma 60(3). The overlap axiom follows from Lemma 60(1). The root-
activeness axiom follows from
${\mathcal{R}}\subseteq{\mathcal{H}}\subseteq{\mathcal{U}}$. The
indiscernibility axiom follows from Lemma 67.