# An Alpha-Corecursion Principle for the Infinitary Lambda Calculus

Alexander Kurz, Daniela Petrişan, Paula Severi, Fer-Jan De Vries

► To cite this version:

Alexander Kurz, Daniela Petrişan, Paula Severi, Fer-Jan De Vries. An Alpha-Corecursion Principle for the Infinitary Lambda Calculus. 11th International Workshop on Coalgebraic Methods in Computer Science (CMCS), Mar 2012, Tallinn, Estonia. pp.130-149, 10.1007/978-3-642-32784-1_8.hal-01539877

HAL Id: hal-01539877

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

Submitted on 15 Jun 2017

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

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

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

Distributed under a Creative Commons Attribution 4.0 International License
# An Alpha-Corecursion Principle for the Infinitary Lambda Calculus

Alexander Kurz, Daniela Petrişan, Paula Severi and Fer-Jan de Vries

Department of Computer Science, University of Leicester, UK

**Abstract.** Gabbay and Pitts proved that lambda-terms up to alpha-equivalence constitute an initial algebra for a certain endofunctor on the category of nominal sets. We show that the terms of the infinitary lambda-calculus form the final coalgebra for the same functor. This allows us to give a corecursion principle for alpha-equivalence classes of finite and infinite terms. As an application, we give corecursive definitions of substitution and of infinite normal forms (Böhm, Lévy-Longo and Berarducci trees).

## 1 Introduction

Classical λ-calculus considers only finite terms [5]. Infinitary λ-calculus aims to treat finite and infinite terms in one notational framework together with finite and infinite reductions [16,17,15]. In the calculus one can express that certain terms have an infinite normal form. We illustrate this idea with the example of streams. We choose the standard format of the Church numerals [5] to represent natural numbers by λ-terms. In this format n abbreviates the λ-term λfx.fⁿx which represents the natural number n; the successor function is written as **succ** = λyfx.f(yfx) and the pairing function as **cons** = λyxz.zxy. Using the fixed point combinator **fix** = λf.(λx.f(xx))λx.f(xx), the function **from** on streams given by

$$ \mathbf{from} \ x = \mathbf{cons} \ x \ (\mathbf{from}(\mathbf{succ} \ x)) $$

can now be defined in λ-calculus as follows:

$$ \mathbf{from} = \mathbf{fix}(\lambda f.\mathbf{cons} \ x \ (f(\mathbf{succ} \ x))) $$

The infinite β-reduction sequence

$$ \mathbf{from} \ 0 \to_\beta \mathbf{cons} \ 0 \ (\mathbf{from} \ 1) \to_\beta \mathbf{cons} \ 0 \ (\mathbf{cons} \ 1 \ (\mathbf{from} \ 2)) \dots \quad (1) $$

has the infinite λ-term **cons** 0 (**cons** 1 (**cons** 2(...))) as a limit.
How are such infinite terms defined? Let $\Lambda$ be the set of $\lambda$-terms over some fixed set $\mathcal{V}$ of variables extended with a constant $\perp$ [5]. The set $\Lambda^\infty$ of finite and infinite $\lambda$-terms is defined by coinduction from the grammar:

$$M ::= \perp | x | (\lambda x.M) | (MM) \qquad (2)$$

where $x$ ranges over a given set $\mathcal{V}$ of variables.

A typical corecursive definition on the set $\Lambda^\infty$ is the one of substitution. Substitution on $\Lambda^\infty$ is defined as for the set $\Lambda$ of finite terms but using corecursion instead of recursion. An attempt to define $M[x := N]$ as the result of substituting $x$ by $N$ in $M$ by corecursion is as follows.

$$ \begin{align} y[x := N] &= \begin{cases} N & \text{if } y = x \\ y & \text{otherwise} \end{cases} \tag{3} \\ (PQ)[x := N] &= (P[x := N]Q[x := N]) \\ (\lambda y.P)[x := N] &= \lambda y.(P[x := N]) \quad \text{if } y \notin \mathbf{fv}(N) \cup \{x\} \nonumber \end{align} $$

However, this is only a partial map on $\Lambda^\infty$. As for $\Lambda$, the problem resides in the side-condition $y \notin \mathbf{fv}(N) \cup \{x\}$, which is necessary to avoid the capture of free variables in $N$ by the abstraction in $\lambda y.(P[x := N])$. In the finitary $\lambda$-calculus, one can define substitution as a total map on the set $\Lambda_\alpha$ of $\alpha$-equivalence classes of $\lambda$-terms by choosing a suitable representative $\lambda y.P$ such that $y \notin \mathbf{fv}(N) \cup \{x\}$. This approach is not immediately viable for infinitary $\lambda$-calculus, because we may have terms (see also (4) below) that exhaust all the available variables, so that we cannot find a fresh $y$.

Nominal sets [11] provide an elegant way for establishing an $\alpha$-structural recursion principle [23] that allows one to define substitution on $\alpha$-equivalence classes of finite $\lambda$-terms starting from a partial function with a side-condition [14,23]. It is one of the aims of this paper to establish an $\alpha$-corecursion principle, which allows us to view (3) as a corecursive definition of substitution on $\alpha$-equivalence classes of terms in $\Lambda^\infty$.

Before starting on the details, we need to point out a subtlety that arises when treating infinite $\lambda$-terms. An infinite term in $\Lambda^\infty$ may have an infinite set of variables. Suppose that the set $\mathcal{V}$ of variables $\{x_0, x_1, x_2, \dots\}$ is countable. Then, we may not be able to have ‘enough fresh variables’ to work on $\alpha$-equivalence classes. For example, consider the term $\mathbf{allfv} = x_0(x_1(x_2(\dots))) \in \Lambda^\infty$ which contains all variables from $\mathcal{V}$. In the following $\beta$-step

$$(\lambda x_0 x_1 x_0 x_1)\mathbf{allfv} \to_\beta (\lambda x_1 x_0 x_1)[x_0 := \mathbf{allfv}] \qquad (4)$$

we have that $x_1 \in \mathbf{fv}(\mathbf{allfv})$ and, therefore, $x_1$ should be replaced by some fresh variable, which is impossible because $\mathbf{allfv}$ contains all of them [24]. However, in this paper, we will restrict our attention to the set

$$\Lambda_{\mathbf{fv}}^{\infty} = \{M \in \Lambda^{\infty} \mid \mathbf{fv}(M) \text{ is finite}\} \qquad (5)$$

of $\lambda$-terms with finitely many free variables, avoiding terms such as $\mathbf{allfv}$. On the one hand, finitely many free variables are sufficient in order to capture the infinite
normal forms of terms representing programs, since the limit of an infinite β-reduction sequence starting from a finite term has always a finite number of free variables. As a caveat, notice that such a limit may have infinitely many bound variables, since additional fresh variables may be needed at each reduction step to avoid capture. On the other hand, restricting to finitely many free variables has the advantage of allowing us to use the machinery of nominal sets [14].

To come back to α-(co)recursion, Pitts [23] derives structural recursion and induction principles for syntax with binding by using the result from [11] that the set $Λ/=$α of α-equivalence classes of finite λ-terms is the initial algebra for the functor $L_α$ on the category Nom of nominal sets defined by

$$L_α U = V + \{\perp\} + [V]U + U \times U \quad (6)$$

where $[V]U$ is the quotient of $V \times U$ by α-equivalence (and we added a constant $\{\perp\}$ for reasons that will be explained after Definition 1). We will prove that the final coalgebra of the same functor $L_α$ is the (nominal) set $Λ_{fv}^∞/=$α of α-equivalence classes of finite and infinite λ-terms with finitely many free variables. Using this result we will formulate an α-corecursion principle and give corecursive definitions of substitution and various notions of infinite normal form (Böhm, Lévy-Longo and Berarducci trees) on α-equivalence classes of terms.

The structure of the paper is as follows. Sections 2 and 3 review preliminaries on infinitary lambda calculus and nominal sets, respectively. Section 4 contains our main result on the final $L_α$-coalgebra and Section 5 its application to substitution and to the notions of Böhm, Lévy-Longo and Berarducci trees. Section 6 compares α-corecursion with α-recursion and comments on the relationship between Set- and Nom-based reasoning.

## 2 Preliminaries on Infinitary Lambda Calculus

We assume familiarity with basic notions and notations of the finite λ-calculus [5]. First we explain how the set $Λ^∞$ of finite and infinite λ-terms can be constructed as the metric completion of the set $Λ$ of finite λ-terms. Then we will briefly recall some notions and facts of infinitary λ-calculus [17,15]. We leave the treatment of α-conversion for Section 4.

The idea of putting a metric on a set of terms goes at least back to Arnold and Nivat [4]. To do so we define truncations.

**Definition 1 (Truncation).** The truncation of a term $M \in Λ$ at depth $n \in N$ is defined by induction on n:

$$M^0 = \perp \\ M^{n+1} = \begin{cases} x & \text{if } M = x \in V \\ \perp & \text{if } M = \perp \\ \lambda x.N^n & \text{if } M = \lambda x.N \\ N^n P^n & \text{if } M = NP \end{cases} \quad (7)$$
In this definition, we use the constant $\perp$ to represent “unknown information”. Later, in the constructions of normal forms of $\lambda$-terms we will, as it is customary in infinitary $\lambda$-calculus, use the same constant to replace computationally meaningless terms.

**Definition 2 (Metric).** We define a metric $d: \Lambda \times \Lambda \to [0, 1]$ by

$$d(M, N) = 2^{-m}, \qquad (8)$$

where $m = \sup\{n \in \mathbb{N} | M^n = N^n\}$ and we use the convention $2^{-\infty} = 0$.

In fact, $(\Lambda, d)$ is an ultrametric space, since for all $M, N, P \in \Lambda$ we have $d(M, N) \le \max\{d(M, P), d(P, N)\}$, as one can easily check.

The set $\Lambda^\infty$ of finite and infinite $\lambda$-terms (with the additional constant $\perp$) is now defined as the metric completion of the set $\Lambda$ of finite terms with respect to the metric $d$. Alternatively, $\Lambda^\infty$ can be defined by interpreting (2) as a coinductive definition. The fact that both definitions coincide is a consequence of Barr's theorem on final coalgebras for bicontinuous Set endofunctors [6, Theorem 3.2].

Indeed, interpreting (2) coinductively amounts to taking as $\lambda$-terms the elements of the final coalgebra for the Set-endofunctor

$$L U = \mathcal{V} + \{\perp\} + \mathcal{V} \times U + U \times U \qquad (9)$$

Notice that the set $\Lambda$ of finite $\lambda$-terms constitutes the initial algebra for $L$. A closer look at the proof of Barr [6, Theorem 3.2 and Proposition 3.1] shows now that the metric $d$ on $\Lambda$ of Definition 2 coincides with the metric induced by the final coalgebra. Hence, by [6, Proposition 3.1], the completion of the initial $L$-algebra $\Lambda$ in the metric $d$ is the final $L$-coalgebra.

To summarise, the final $L$-coalgebra $(\Lambda^\infty, \text{unfold}: \Lambda^\infty \to L(\Lambda^\infty))$ is the Cauchy completion of $\Lambda$ and we have a dense inclusion map $\iota: \Lambda \to \Lambda^\infty$. It is well-known that the structure map of the final coalgebra $\text{unfold}: \Lambda^\infty \to L(\Lambda^\infty)$ is an isomorphism, hence the set $L(\Lambda^\infty)$ can be equipped with a complete metric. The map $\text{unfold}: \Lambda^\infty \to L(\Lambda^\infty)$ is the unique uniformly continuous map from $\Lambda^\infty$ to $L(\Lambda^\infty)$ making diagram (10) commutative:

$$\begin{array}{ccc} \Lambda & \xrightarrow{\approx} & L(\Lambda) \\ \iota \downarrow & & \downarrow L(\iota) \\ \Lambda^\infty & \xrightarrow{\text{unfold}} & L(\Lambda^\infty) \end{array} \qquad (10)$$

Having defined the set $\Lambda^\infty$ of finite and infinite $\lambda$-terms we now extend the usual syntactic conventions for finite $\lambda$-calculus to infinitary $\lambda$-calculus. Terms and variables will respectively be written with (super- and subscripted) letters $M, N$ and $x, y, z$. Terms of the form $(M_1 M_2)$ and $(\lambda x M)$ will respectively be called applications and abstractions.

The truncation of an infinite term $M \in \Lambda^\infty$ at depth $n$ is defined just as in Definition 1 by induction on $n$. Observe that $(M^n)_{n \in \mathbb{N}}$ is a Cauchy sequence in $(\Lambda^\infty, d)$ that converges to $M$.
The set of free and bound variables of a finite term $M$ is defined as usual and denoted by $fv(M)$ and $bv(M)$ respectively. We extend $fv(M)$, $bv(M)$ to infinite terms $M \in \Lambda^\infty$ using truncations as below. Also, $var(M) = fv(M) \cup bv(M)$.

$$fv(M) = \bigcup_{n \in \mathbb{N}} fv(M^n) \quad bv(M) = \bigcup_{n \in \mathbb{N}} bv(M^n)$$

We define $\beta$-reduction on $\Lambda^\infty$ and denote it as $\rightarrow_\beta$ in the usual way: the smallest relation that contains $(\lambda x.P)Q \rightarrow_\beta P[x := Q]$ and is closed under contexts. The reflexive and transitive closure of $\rightarrow_\beta$ is denoted by $\dashv\dashv_\beta$. For the definition of $\dashv\dashv_\beta$ that assumes a sequence of reduction steps of any ordinal length, see for instance [16]. Terms of the form $(\lambda x.P)Q$ are called redexes. Normal forms are terms without redexes and hence cannot be changed by further computation.

The definition of infinitary $\lambda$-calculus is completed by adding $\perp$-reduction, denoted by $\rightarrow_\perp$: the smallest relation closed under context that contains $M \rightarrow_\perp \perp$ for $M$ belonging to some fixed set $\mathcal{U}$ of meaningless terms. If and only if the set $\mathcal{U}$ satisfies certain properties, the resulting infinitary calculus is confluent and normalising, in which case each term has a unique normal form [17,15].

The normal form of a $\lambda$-term can be thought to represent its meaning, the maximal amount of information embodied in the term, stable in the sense that it cannot be changed by further computation. Note that this concept of meaning depends on the chosen set $\mathcal{U}$ of meaningless terms for which there is ample, uncountable choice [25].

## Böhm, Lévy-Longo and Berarducci trees

For concrete sets of meaningless terms an alternative, “informal” corecursive definition of the normal form of a term in the corresponding infinitary $\lambda$-calculus can sometimes be given. Three of them are well known.

In his book [5], Barendregt argued that the terms without head normal forms should be considered as meaningless terms. Any finite $\lambda$-term is either a head normal form (hnf), that is, a term of the form $\lambda x_1 \dots \lambda x_n . x N_1 \dots N_m$, or it is a term of the form $\lambda x_1 \dots \lambda x_n . ((\lambda y.P)Q)N_1 \dots N_m$ where the redex $(\lambda y.P)Q$ is called the head redex. Starting with a term $M$ that is not in hnf one can repeatedly contract the head redex. Either this will go on forever or terminate with a hnf, which represents part of the information embodied in a term. In the latter case one can repeat this process on the subterms $N_i$ to try to compute more information. This idea led Barendregt to his elegant “informal” definition of the Böhm tree $\mathbf{BT}(M)$ of a term $M$, that we now recognise as a corecursive definition.

$$\mathbf{BT}(M) = \begin{cases} \lambda x_1 \dots \lambda x_n . \mathbf{BT}(M_1) \dots \mathbf{BT}(M_m) & \text{if } M \dashv\dashv_\beta \lambda x_1 \dots \lambda x_n . y M_1 \dots M_m \\ \perp & \text{otherwise} \end{cases} \quad (11)$$

Taking for $\mathcal{U}$ the set of terms without hnf, one can show using the confluence property that the normal forms of the corresponding infinite $\lambda$-calculus satisfy
the equations in (11). That is, the Böhm tree of a term $M$ is the normal form of $M$ in the infinitary $\lambda$-calculus that equates all terms without head normal form with $\perp$ [5,17].

Alternatively, as Abramsky has forcefully argued in [1], one can take the set of terms without weak head normal form (whnf) as set of meaningless terms. Any finite $\lambda$-term is either a weak head normal form, that is, a term of either of the two forms $xM_1...M_m$, or $\lambda x.N$, or it is a term of the form $((\lambda y.P)Q)M_1...M_m$ where the redex $(\lambda y.P)Q$ is called the weak head redex. In perfect analogy with before, starting with a term $M$ that is not in whnf one can repeatedly contract the weak head redex. Either this will go on forever or terminate with a whnf. In the latter case one can repeat this process on the subterms $M_i$ of the tail of the whnf or on the subterm $N$ of its body to try to compute more information. This describes a lazy computation strategy, that postpones reduction under abstractions as much as possible.

The normal forms of the corresponding infinitary $\lambda$-calculus that equates all terms without weak head normal form with $\perp$ satisfy the equations (12) that define the Lévy-Longo tree $LLT(M)$ of a term $M$ corecursively [19,18,2,17].

$$LLT(M) = \begin{cases} yLLT(M_1)...LLT(M_m) & \text{if } M \dashv\beta yM_1...M_m \\ \lambda x.LLT(N) & \text{if } M \dashv\beta \lambda x.N \\ \perp & \text{otherwise} \end{cases} \quad (12)$$

The least set of meaningless terms that gives rise to a confluent and normalising infinitary $\lambda$-calculus is the set of terms without a top normal form. Here a term $M$ is a top normal form (tnf) if it is either a variable, an abstraction or an application of the form $M_1M_2$ in which $M_1$ is a zero term, i.e. a term that cannot reduce to an abstraction. The well-known term $\Omega = (\lambda x.xx)(\lambda x.xx)$ has no tnf. The normal forms of this calculus can alternatively be characterised by the corecursive definition of the Berarducci tree [7,17] $BerT(M)$ of a term $M$:

$$BerT(M) = \begin{cases} x & \text{if } M \dashv\beta x \\ \lambda x.BerT(N) & \text{if } M \dashv\beta \lambda x.N \\ BerT(P)BerT(Q) & \text{if } M \dashv\beta \text{ NP and } N \text{ is a zero term} \\ \perp & \text{otherwise} \end{cases} \quad (13)$$

It is possible to formalise (11)-(13) using corecursion via the final $L$-coalgebra, provided we give concrete reduction strategies to compute the various forms used in the definitions. However, in order to take into account $\alpha$-conversion, we will prove an $\alpha$-corecursion principle based on nominal sets.

## 3 Preliminaries on Nominal Sets

We recall basic facts on nominal sets [14]. Consider a countable infinite set $V$ of ‘variables’ (or ‘atoms’ or ‘names’) and the group $\mathfrak{S}(V)$ of permutations on $V$ generated by transpositions, which are permutations of the form $(x y)$ that swap $x$ and $y$. Consider a set $U$ equipped with an action of the group $\mathfrak{S}(V)$, denoted by $\cdot: \mathfrak{S}(V) \times U \to U$. We say that $u \in U$ is supported by a set $S \subseteq V$ when for
all $\pi \in \mathfrak{S}(\mathcal{V})$ such that $\pi(x) = x$ for all $x \in S$ we have $\pi \cdot u = u$. We say that $u \in U$ is finitely supported if there exists a finite $S \subseteq \mathcal{V}$ which supports $u$.

**Definition 3 (Nominal set).** A nominal set $(U, \cdot)$ is set $U$ equipped with a $\mathfrak{S}(\mathcal{V})$-action such that all elements of $U$ are finitely supported. Given nominal sets $(U, \cdot)$ and $(V, \cdot)$, a map $f: U \to V$ is called equivariant when $f(\pi \cdot u) = \pi \cdot f(u)$ for all $\pi \in \mathfrak{S}(\mathcal{V})$ and $u \in U$. The category of nominal sets and equivariant maps is denoted by $\text{Nom}$.

A crucial property of nominal sets is that each element of a nominal set has a least finite support, see [14]. Indeed, if two finite sets $S_1$ and $S_2$ support $u$, then their intersection also supports $u$. The smallest finite support of $u$ is denoted by $\text{supp}(u)$. If $x \in \mathcal{V} \setminus \text{supp}(u)$ we say that $x$ is fresh for $u$, and write $x\#u$. More generally, given two nominal sets $(U, \cdot)$ and $(V, \cdot)$, $u \in U$ and $v \in V$, we write $u\#v$ for $\text{supp}(u) \cap \text{supp}(v) = \emptyset$. An important property of $\text{supp}$ is that for every equivariant $f: U \to V$ and $u \in U$, we have $\text{supp}(f(u)) \subseteq \text{supp}(u)$.

**Example 4.** The set of names $\mathcal{V}$ equipped with the evaluation action given by $\pi \cdot x = \pi(x)$ is a nominal set.

**Example 5.** The set $\Lambda$ of finite $\lambda$-terms with the action $\cdot : \mathfrak{S}(\mathcal{V}) \times \Lambda \to \Lambda$ inductively defined by

$$ \begin{aligned} \pi \cdot x &= \pi(x) \\ \pi \cdot \bot &= \bot \\ \pi \cdot (\lambda x.M) &= \lambda\pi(x).(\pi \cdot M) \\ \pi \cdot (MN) &= ((\pi \cdot M)(\pi \cdot N)) \end{aligned} \qquad (14) $$

is a nominal set. In this example we do not take into account $\alpha$-conversion, so the support of a $\lambda$-term $M$ is the set of all variables occurring either bound or free in $M$.

Given a $\mathfrak{S}(\mathcal{V})$-action $\cdot$ on a set $U$, let $U_{\mathrm{fs}}$ denote the set

$$ U_{\mathrm{fs}} = \{u \in U \mid \text{u is finitely supported}\}. \qquad (15) $$

Then $\cdot$ restricts to a $\mathfrak{S}(\mathcal{V})$-action on $U_{\mathrm{fs}}$ and $(U_{\mathrm{fs}}, \cdot)$ is a nominal set.

**Example 6.** The set $\Lambda^\infty$ of finite and infinite $\lambda$-terms can be equipped with the action $\cdot : \mathfrak{S}(\mathcal{V}) \times \Lambda^\infty \to \Lambda^\infty$ defined coinductively by (14). Alternatively, $\pi \cdot (-)$ can be defined using the universal property of the metric completion, as the unique map that extends $\Lambda \xrightarrow{\pi \cdot (-)} \Lambda \xleftarrow{\iota} \Lambda^\infty$. Observe that $(\pi \cdot M)^n = \pi \cdot M^n$ for all $M \in \Lambda^\infty$ and $n \in \mathbb{N}$. Notice that $(\Lambda^\infty, \cdot)$ is not a nominal set since the set of variables in a term, and hence its support, can be infinite. But $((\Lambda^\infty)_{\mathrm{fs}}, \cdot)$ is a nominal set and $\text{supp}(M) = \text{var}(M)$ for all $M \in (\Lambda^\infty)_{\mathrm{fs}}$.

**Definition 7 (Abstraction).** Let $(U, \cdot)$ be a nominal set. One defines $\sim_\alpha$ on $\mathcal{V} \times U$ by

$$ (x_1, u_1) \sim_\alpha (x_2, u_2) \Leftrightarrow (\exists z \# (x_1, u_1, x_2, u_2))(x_1 \ z) \cdot u_1 = (x_2 \ z) \cdot u_2 \qquad (16) $$
The $\sim_\alpha$-equivalence class of $(x, u)$ is denoted by $\langle x \rangle u$. The abstraction $[V]U$ of the nominal set $U$ is the quotient $(V \times U)/\sim_\alpha$. The $\mathfrak{S}(V)$-action on $[V]U$ is defined by

$$ \pi \cdot \langle x \rangle u = \langle \pi \cdot x \rangle \pi \cdot u. \qquad (17) $$

Given equivariant $f : (U, \cdot) \to (V, \cdot)$, we define $[V]f : [V]U \to [V]V$ by

$$ \langle x \rangle u \mapsto \langle x \rangle f(u). \qquad (18) $$

**Definition 8 (Concretion).** Let $(U, \cdot)$ be a nominal set. Concretion is the partial function $@: [V]U \times V \to U$ with $\langle y \rangle u@z$, the 'concretion of $\langle y \rangle u$ at $z'$, defined as $\langle y \rangle u@z = (z \ y) \cdot u$ if $z \in V \setminus \text{supp}(\langle y \rangle u)$.

Notice that $y\#\langle y \rangle u$ and $(\langle y \rangle u)@y = u$. Moreover, concretion is equivariant. If $z\#\langle y \rangle u$ then $\pi \cdot z\#\langle \pi \cdot y \rangle \pi \cdot u$ and $\pi \cdot (\langle y \rangle u@z) = (\langle \pi \cdot y \rangle \pi \cdot u)@\pi \cdot z$.

Further, we recall some general results form [22] that will be necessary to prove our main result on the final $L_\alpha$-coalgebra. The category Nom is complete and cocomplete. The forgetful functor to Set creates finite products and all colimits. For example, the product of two nominal sets $(U, \cdot)$ and $(V, \cdot)$ is $(U \times V, \cdot)$ where

$$ \pi \cdot (u, v) = (\pi \cdot u, \pi \cdot v). $$

Arbitrary products in Nom are computed differently than in Set. Given a family of nominal sets $(U_i, \cdot)$, we can equip the set of all tuples $\{(u_i)_{i \in I} \mid u_i \in U_i\}$ with the pointwise action given by

$$ \pi \cdot (u_i)_{i \in I} = (\pi \cdot u_i)_{i \in I}. \qquad (19) $$

This is a $\mathfrak{S}(V)$-action, but some tuples may not be finitely supported. The product of $(U_i, \cdot)$ in Nom is the nominal set $(\prod_{i \in I} (U_i, \cdot))_{fs}$ of tuples of the form $(u_i)_{i \in I}$ that are finitely supported with respect to the action of (19).

The abstraction functor $[V](-) : \text{Nom} \to \text{Nom}$ preserves all limits.

# 4 Infinitary Lambda Calculus in Nominal Sets

This section contains our main technical result, Theorem 22, which is then used to show Theorem 23, stating that the set $\Lambda_{ffv}^\infty/\sim_\alpha$ of finite and infinite $\lambda$-terms up to $\alpha$-equivalence is the final coalgebra for the functor $L_\alpha$ on Nom, see (6).

On finite terms, $\alpha$-conversion can be defined inductively using the permutation action $\cdot : \mathfrak{S}(V) \times \Lambda \to \Lambda$ of Example 5, see [14].

**Definition 9 ($\alpha$-conversion on finite $\lambda$-terms).** Let $M, N, M', N' \in \Lambda$.

$$ \begin{array}{c} \overline{\qquad} (\text{var}) \\ x =_\alpha x \\ \hline \\ \overline{\qquad} (\text{bot}) \\ \bot =_\alpha \bot \\ \hline \\ \frac{M =_\alpha N \quad M' =_\alpha N'}{MM' =_\alpha NN'} (\text{app}) \qquad \frac{(x \ z) \cdot M =_\alpha (y \ z) \cdot N \quad z\#(x, y, M, N)}{\lambda x.M =_\alpha \lambda y.N} (\text{abs}) \end{array} $$
The relation $=_{\alpha}$ is equivariant, that is, $M =_{\alpha} N$ implies $\pi \cdot M =_{\alpha} \pi \cdot N$ for all $\pi \in \mathfrak{S}(\mathcal{V})$. Thus we obtain a nominal set $(\Lambda/=_{\alpha}, \cdot)$ where $\text{supp}(M) = \text{fv}(M)$.

**Definition 10 (L_α).** We define $L_\alpha : \text{Nom} \to \text{Nom}$ as follows.

$$ 
\begin{aligned}
L_{\alpha} U &= \mathcal{V} + \{\perp\} + [\mathcal{V}]U + U \times U \\
L_{\alpha}(f) &= [\text{Id}^{\mathcal{V}}, \text{Id}^{\perp}, [\mathcal{V}]f, f \times f]
\end{aligned}
 $$

The nominal set $(\Lambda/=_{\alpha}, \cdot)$ of $\alpha$-equivalence classes of finite $\lambda$-terms is the initial algebra for the functor $L_\alpha$ [14].

We define $\alpha$-conversion on the set $\Lambda^{\infty}$ using truncations. This definition is slightly different from, though equivalent, to those used in [16,17,15].

**Definition 11 (α-conversion on finite and infinite λ-terms).** We extend the notion of α-conversion to the set $\Lambda^{\infty}$ via

$$ M =_{\alpha} N \text{ iff } M^n =_{\alpha} N^n \text{ for all } n \in \mathbb{N}. $$

If $M =_{\alpha} N$ then $M^n =_{\alpha} N^n$. The notion of truncation can be extended to $\Lambda^{\infty}/=_{\alpha}$ via $[M]_{\alpha}^n = [M^n]_{\alpha}$.

**Notation 12 (α-equivalence classes)** In this section, *metavariables of elements in $\Lambda^{\infty}/=_{\alpha}$ are denoted by $X, Y$. The $\alpha$-equivalence class of $M$ is denoted by $[M]_{\alpha}$.*

The reason we need to clearly distinguish between the class $X$ and the term $M \in X$ is that in Theorem 22 we need to construct a Cauchy sequence of representatives $M_1, M_2, \dots$ from a Cauchy sequence $X_1, X_2, \dots$ of $\alpha$-equivalence classes.

A second approach to define the set of $\alpha$-equivalence classes of infinitary terms is to consider the metric completion of the quotient $\Lambda/=_{\alpha}$.

**Definition 13 (Metric on α-equivalence classes).** We define $d_{\alpha} : \Lambda \times \Lambda \to [0, 1]$ via

$$ d_{\alpha}(M, N) = 2^{-m}, \qquad (20) $$

where $m = \sup\{n \in \mathbb{N} \mid M^n =_{\alpha} N^n\}$ and we use the convention $2^{-\infty} = 0$.

We have that $d_{\alpha}$ is a pseudometric on $\Lambda$ and $d_{\alpha}(M, N) = 0$ if and only if $M =_{\alpha} N$. Thus $d_{\alpha}$ gives rise to a metric on $\Lambda/=_{\alpha}$ denoted by abuse of notation also by $d_{\alpha}$. Observe that $d_{\alpha}$ extends to a pseudometric $d_{\alpha}^{\infty} : \Lambda^{\infty} \times \Lambda^{\infty} \to [0, 1]$ also given by

$$ d_{\alpha}^{\infty}(M, N) = 2^{-m}, \qquad (21) $$

where $m = \sup\{n \in \mathbb{N} \mid M^n =_{\alpha} N^n\}$ with the convention $2^{-\infty} = 0$. Then $M =_{\alpha} N$ in the sense of Definition 11 if and only if $d_{\alpha}^{\infty}(M, N) = 0$. Hence we obtain a metric, denoted also by $d_{\alpha}^{\infty}$ on $\Lambda^{\infty}/=_{\alpha}$.

We consider the metric completion of $\Lambda/=_{\alpha}$ with respect to $d_{\alpha}$ and denote it by $(\Lambda/=_{\alpha})^{\infty}$.
**Theorem 14.** Let $\mathcal{V}$ be uncountable. Then, we have that $(\Lambda^{\infty}/=_{\alpha}, d_{\alpha}^{\infty})$ is isomorphic to $(\Lambda/=_{\alpha})^{\infty}$.

We do not include the proof of this theorem, since in this paper we are only interested in the case where $\mathcal{V}$ is countable. The idea of the proof is to show that $(\Lambda^{\infty}/=_{\alpha}, d_{\alpha}^{\infty})$ is a complete metric space and then to use the universality property of the metric completion. This argument fails when the set of variables is at most countable. Indeed, we can show that for countable $\mathcal{V}$ the space $(\Lambda^{\infty}/=_{\alpha}, d_{\alpha}^{\infty})$ is not complete.

*Example 15.* Assume that $\mathcal{V}$ is countable, say $\mathcal{V} = \{x_0, x_1, \dots\}$ and consider the sequence $([\lambda x_n \cdot x_n(x_0 \dots x_{n-1})])_{\alpha})_{n \ge 1}$ in $\Lambda^{\infty}/=_{\alpha}$. This is a Cauchy sequence with respect to $d_{\alpha}^{\infty}$, but has no limit in $\Lambda^{\infty}/=_{\alpha}$. Indeed, assume for a contradiction that the limit $L$ exists. On the one hand we can prove that $\mathrm{fv}(L) = \mathcal{V}$, on the other hand $L$ should be of the form $\lambda u \cdot u x_0 x_1 \dots$ for some variable $u$. But this contradicts the fact that $u$ is free in $L$.

These problems of $\alpha$-equivalence in the presence of countably many variables disappear if we consider the set $\Lambda_{\mathrm{fv}}^{\infty}$ of terms with finitely many free variables (5) discussed in the introduction.

*Remark 16.* Note that $\Lambda_{\mathrm{fv}}^{\infty}$ is different from the set $(\Lambda^{\infty})_{\mathrm{fs}} = \Lambda_{\mathrm{fs}}^{\infty}$, defined in (15), of $\lambda$-terms with finitely many variables, bound or free. To see this, consider the term

$$ \mathbf{allbv} = \lambda x_1 \cdot x_1 (\lambda x_2 \cdot x_1 (x_2 (\lambda x_3 \cdot x_1 (x_2 (x_3 \dots))))) $$

We have that $\mathbf{allbv} \in \Lambda_{\mathrm{fv}}^{\infty}$ but $\mathbf{allbv} \notin \Lambda_{\mathrm{fs}}^{\infty}$. Actually, $[\mathbf{allbv}]_{\alpha} \cap \Lambda_{\mathrm{fs}}^{\infty} = \emptyset$ since every term in $[\mathbf{allbv}]_{\alpha}$ has infinitely many bound variables.

Moreover, the equivalence relation $=_{\alpha}$ (see Definition 11) restricts to $\Lambda_{\mathrm{fv}}^{\infty}$, but not to $\Lambda_{\mathrm{fs}}^{\infty}$. For example, we have $\lambda x_1 \cdot \lambda x_2 \cdot \lambda x_3 \dots =_{\alpha} \lambda x_1 \cdot \lambda x_1 \cdot \lambda x_1 \dots$, but only the latter term is in $\Lambda_{\mathrm{fs}}^{\infty}$.

For all $M, N \in \Lambda_{\mathrm{fv}}^{\infty}$ we have that $M =_{\alpha} N$ implies $\pi \cdot M =_{\alpha} \pi \cdot N$. Hence we can equip $\Lambda_{\mathrm{fv}}^{\infty}/=_{\alpha}$ with a $\mathfrak{S}(\mathcal{V})$ action given by $\pi \cdot [M]_{\alpha} = [\pi \cdot M]_{\alpha}$ and we can easily check that $(\Lambda_{\mathrm{fv}}^{\infty}/=_{\alpha}, \cdot)$ is a nominal set. Indeed, $[M]_{\alpha} \in \Lambda_{\mathrm{fv}}^{\infty}/=_{\alpha}$ is supported by the finite set $\mathrm{fv}(M)$.

The permutation action on $\Lambda/=_{\alpha}$ can be extended to $(\Lambda/=_{\alpha})^{\infty}$ as follows. For each $\pi \in \mathfrak{S}(\mathcal{V})$ we have that $\pi \cdot (-) : \Lambda/=_{\alpha} \to \Lambda/=_{\alpha}$ is a uniformly continuous function with respect to $d_{\alpha}$, thus can be extended to a uniformly continuous map on $(\Lambda/=_{\alpha})^{\infty}$ using the universal property of the metric completion:

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

Thus we have a nominal set $((\Lambda/=_{\alpha})_{\mathrm{fs}}^{\infty}, \cdot)$. A Cauchy sequence $(X_n)_{n \in \mathbb{N}}$ in $\Lambda/=_{\alpha}$ is finitely supported when there exists a finite set $S \subseteq \mathcal{V}$ such that $S$ supports $X_n$ for all $n \in \mathbb{N}$.
**Lemma 17.** $X \in (\Lambda/\alpha)_{\text{fs}}^{\infty}$ if and only if there exists a finitely supported Cauchy sequence of elements of $\Lambda/\alpha$ converging to $X$.

*Proof.* The right-to-left implication is trivial. For the left-to right implication, consider a Cauchy sequence $(X_n)_{n \in \mathbb{N}}$ in $\Lambda/\alpha$ converging to $X$. Then for all $k \in \mathbb{N}$ the sequence of truncations $(X_n^k)_{n \in \mathbb{N}}$ is constant from a point onwards and let $Y_k$ denote its limit in $\Lambda/\alpha$. We can show that each $\pi$ that fixes $\text{supp}(X)$ also fixes $Y_k$. The sequence $(Y_k)_{k \in \mathbb{N}}$ is a finitely supported Cauchy sequence that converges to $X$.

*Remark 18.* From the proof of Lemma 17 it follows that each $X \in (\Lambda/\alpha)^{\infty}$ can be expressed as the limit of a 'canonical' Cauchy sequence $(X_n)_{n \in \mathbb{N}}$ such that the truncation of $X_{n+1}$ at depth $n$ is equal to $X_n$.

**Definition 19 (α-safe term).** Let $M \in \Lambda$. We define the set of α-safe terms $\Gamma \subseteq \Lambda$ by the following inductive rules

$$ \frac{\begin{array}{c} \overline{\phantom{x \in \Gamma}}(\text{var}) \\ \phantom{\overline{\phantom{x \in \Gamma}}} \\ \phantom{\overline{\phantom{x \in \Gamma}}} \\ \phantom{\overline{\phantom{x \in \Gamma}}} \end{array}}{MN \in \Gamma} \quad (\text{app}) \quad \frac{\begin{array}{c} \overline{\phantom{\bot \in \Gamma}}(\text{bot}) \\ \phantom{\overline{\phantom{\bot \in \Gamma}}} \\ \phantom{\overline{\phantom{\bot \in \Gamma}}} \\ \phantom{\overline{\phantom{\bot \in \Gamma}}} \end{array}}{\lambda x.M \in \Gamma} \quad (\text{abs}) $$

Intuitively, a $\lambda$-term $M$ is $\alpha$-safe when $\text{bv}(M) \cap \text{fv}(M) = \emptyset$ and $M$ does not have two different $\lambda$'s with the same binding variable, i.e. if $\lambda x$ and $\lambda y$ occur in two different positions of $M$ then $x \neq y$. This is slightly stronger than Barendregt's Variable Convention, see [5, Convention 2.1.13].

In Definition 19 we interpret the freshness relation $\#$ in the nominal set $(\Lambda, \cdot)$ of Example 5. So, $\text{bv}(M)\#N$ means that $\text{bv}(M) \cap (\text{bv}(N) \cup \text{fv}(N)) = \emptyset$.

In the next lemma, we will prove that we can always find an $\alpha$-safe term in an $\alpha$-equivalence class. Note that the set of $\alpha$-safe terms is not closed under $\beta$. For example, $(\lambda x.xx)(\lambda y.y)$ is $\alpha$-safe but $(\lambda y.y)(\lambda y.y)$ is not.

**Lemma 20 (Choosing representatives).** Let $M \in \Lambda$ and a finite set $S \subseteq \mathcal{V}$. There exists an $\alpha$-safe term $N$ such that $\text{bv}(N) \cap S = \emptyset$ and $M =_{\alpha} N$.

*Proof.* The proof is by induction on the structure of $M$. It is immediate for the base cases $M = \bot$ and $M = x \in \mathcal{V}$.

Assume $M = PQ$. By the induction hypothesis there exists a $\alpha$-safe term $P'$ such that $\text{bv}(P') \cap (\text{fv}(M) \cup S) = \emptyset$ and $P =_{\alpha} P'$. Applying the induction hypothesis again, there exists a $\alpha$-safe term $Q'$ such that $\text{bv}(Q') \cap (\text{bv}(P') \cup \text{fv}(M) \cup S) = \emptyset$ and $Q =_{\alpha} Q'$. Then $M =_{\alpha} P'Q'$ and we can check that $P'Q'$ is $\alpha$-safe and $\text{bv}(P'Q') \cap S = \emptyset$.

The case $M = \lambda x.P$ is solved similarly. By the induction hypothesis there exists a $\alpha$-safe term $P'$ such that $P =_{\alpha} P'$ and $\text{bv}(P') \cap (S \cup \text{fv}(M) \cup \{x\}) = \emptyset$. Then $\lambda x.P'$ is $\alpha$-safe by Definition 19, $M =_{\alpha} \lambda x.P'$ and $S\#\lambda x.P'$.

**Lemma 21.** Let $M, P \in \Lambda$ be two $\alpha$-safe terms such that $P^n =_{\alpha} M$, $\text{bv}(M)\#P$, and $\text{bv}(P)\#M$. Then there exists a $\alpha$-safe term $N$ such that
1. $N =_\alpha P,$

2. the truncation of $N$ at depth $n$ is exactly $M$ in $\Lambda$,

3. $\mathrm{bv}(N) \subseteq \mathrm{bv}(M) \cup \mathrm{bv}(P).$

*Proof.* This is proved by induction on the structure of $M$. We prove the case that $M = \lambda x.M_0$. Then $P = \lambda y.P_0$. Since $y\#M$, we have that $((y x) \cdot P_0)^{n-1} =_\alpha M_0$. By induction hypothesis, there exists $N_0$ such that $N_0 =_\alpha (y x) \cdot P_0$, $N_0^{n-1} = M_0$ and $\mathrm{bv}(N_0) \subseteq \mathrm{bv}(M_0) \cup \mathrm{bv}((y x)P_0)$. We set $N = \lambda x.N_0$. We can check that $N$ is $\alpha$-safe and satisfies the required properties.

In the following theorem, we show that Theorem 14 holds for countable $V$ if interpreted internally in the category of nominal sets.

**Theorem 22 (Completion and quotient by $\approx_\alpha$ commute in Nom).** Let $V$ be countable. The nominal sets $(\Lambda_{\mathrm{fv}}^\infty/\approx_\alpha, \cdot)$ and $((\Lambda/\approx_\alpha)_{\mathrm{fs}}^\infty, \cdot)$ are isomorphic.

*Proof.* Define $f : \Lambda_{\mathrm{fv}}^\infty/\approx_\alpha \to (\Lambda/\approx_\alpha)_{\mathrm{fs}}^\infty$ by

$$ \Lambda_{\mathrm{fv}}^\infty/\approx_\alpha \ni X \mapsto \lim_{n \to \infty} X^n \in (\Lambda/\approx_\alpha)_{\mathrm{fs}}^\infty $$

where $X^n$ is the truncation of $X$ at depth $n$. This is well defined by Lemma 17 and the fact that the sequence $(X^n)_{n \in \mathbb{N}}$ is supported by the finite set $\mathrm{supp}(X)$. It is easy to check that $f$ is equivariant.

Next we give $g : (\Lambda/\approx_\alpha)_{\mathrm{fs}}^\infty \to \Lambda_{\mathrm{fv}}^\infty/\approx_\alpha$. Consider $X \in (\Lambda/\approx_\alpha)_{\mathrm{fs}}^\infty$. By Lemma 17 we have a finitely supported Cauchy sequence $(X_n)_{n \in \mathbb{N}} \subseteq \Lambda/\approx_\alpha$ converging to $X$ with $\mathrm{supp}(X_n) \subseteq \mathrm{supp}(X)$ for all $n \in \mathbb{N}$. Moreover we can assume that the truncation of $X_{n+1}$ at depth $n$ is $X_n$.

*Claim.* There exist representatives $M_n \in X_n$ such that the sequence $(M_n)_{n \in \mathbb{N}}$ is Cauchy in the metric space $(\Lambda, d)$.

Moreover we have that $\mathrm{fv}(M_n) \subseteq \mathrm{supp}(X)$ for all $n \in \mathbb{N}$, thus the limit $M \in \Lambda^\infty$ of the sequence $(M_n)_{n \in \mathbb{N}}$ has finitely many free variables. We put $g(X) = [M]_\alpha$. We can show that $g$ is well defined, equivariant and is the inverse of $f$.

We now sketch the proof of the claim. The idea is to start with an arbitrary sequence of representatives and to inductively rename the bound variables, so that we preserve $\alpha$-equivalence. In a first step, we construct a sequence of representatives $P_n \in X_n$ by induction on $n \in \mathbb{N}$ such that $\mathrm{bv}(P_n) \cap S_n = \emptyset$ where $S_n = \mathrm{supp}(X) \cup \bigcup_{i=1}^{n-1} \mathrm{var}(P_i)$ and $P_n$ is $\alpha$-safe using Lemma 20. Notice that $S$ is finite because $P_1, \dots, P_{n-1}$ are all finite. Notice that this sequence satisfies that the truncation of $P_{n+1}$ at depth $n$ is $\alpha$-convertible to $P_n$.

In a second step we define a sequence $(M_n)_{n \in \mathbb{N}}$ of $\alpha$-safe terms by induction that satisfy the following:

1. $M_n =_\alpha P_n,$

2. the truncation of $M_{n+1}$ at depth $n$ is exactly $M_n,$

3. $\mathrm{bv}(M_n) \subseteq \bigcup_{i=1}^n \mathrm{bv}(P_i).$
For $n = 0$, set $M_0 = P_0$. For the induction step, we have that:

$$ (P_{n+1})^n =_\alpha P_n \text{ by assumption} \\ =_\alpha M_n \text{ by induction hypothesis} $$

Since $bv(M_n) \subseteq \bigcup_{i=1}^n bv(P_i)$, we have that $bv(M_n) \cap bv(P_{n+1}) = \emptyset$. Since $fv(P_{n+1})$ and $fv(M_n)$ are subsets of $supp(X)$ and every $bv(P_i)$ is disjoint from $supp(X)$, we have that $bv(M_n) \cap fv(P_{n+1}) = \emptyset$ and $bv(P_{n+1}) \cap fv(M_n) = \emptyset$. Therefore we can apply Lemma 21 to $M_n$ and $P_{n+1}$, hence there exists $M_{n+1} =_\alpha P_{n+1}$ such that the truncation of $M_{n+1}$ at depth $n$ is exactly $M_n$. We also have that

$$ \begin{aligned} bv(M_{n+1}) &\subseteq bv(M_n) \cup bv(P_{n+1}) & \text{by Lemma 21} \\ &\subseteq \bigcup_{i=1}^{n+1} bv(P_i) & \text{by induction hypothesis} \end{aligned} $$

**Theorem 23 (Final $L_\alpha$-coalgebra).** We have that $((\Lambda_{ffv}^\infty/=\alpha, \cdot), \text{unfold}_\alpha)$ is the final coalgebra for the functor $L_\alpha : \text{Nom} \to \text{Nom}$ given by

$$ L_\alpha U = \mathcal{V} + \{\perp\} + [\mathcal{V}]U + U \times U. $$

*Proof.* The functor $L_\alpha$ is continuous, that is, it preserves limits of $\omega^{op}$-chains. Therefore a final coalgebra for $L_\alpha$ is obtained as the limit of the diagram

$$ 1 \leftarrow! L_\alpha(1) \xleftarrow{L_\alpha(1)!} L_\alpha^2(1) \xleftarrow{L_\alpha^2(1)!} \dots \leftarrow \lim_{n<\omega} L_\alpha^n(1) \quad (22) $$

If we think of the singleton 1 as $\{\perp\}$, we can identify elements of $L_\alpha^n(1)$ with truncations of elements in $\Lambda/=\alpha$ at depth $n$. Recall how limits are computed in $\text{Nom}$. An element of $\lim_{n<\omega} L_\alpha^n(1)$ is a *finitely supported* tuple $(X_n)_{n<\omega} \in \prod n$ such that for all $n < \omega$ we have

$$ L_{\alpha}^{n+1}(!) (X_{n+1}) = X_n, \quad (23) $$

or equivalently, that the truncation of $X_{n+1}$ at depth $n$ is $X_n$.

Then $(X_n)_{n<\omega}$ is a finitely supported Cauchy sequence. By Lemma 17, its limit is in $(\Lambda/=\alpha)_{fs}^\infty$. Conversely, by Remark 18, each $X \in (\Lambda/=\alpha)_{fs}^\infty$ is the limit of a finitely supported Cauchy sequence $(X_n)_{n<\omega} \in \prod n$ satisfying (23).

Thus we have an isomorphism $\lim_{n<\omega} L_\alpha^n(1) \simeq (\Lambda/=\alpha)_{fs}^\infty$, whose equivariance can be easily checked. By Theorem 22 we have

$$ \lim_{n<\omega} L_\alpha^n(1) \simeq \Lambda_{ffv}^\infty/=\alpha. $$

**Remark 24 (Alternative proof to Theorem 23).** To prove Theorem 23, we could have applied a generalisation of Barr's theorem on the existence of final coalgebras to locally finitely presentable categories given by Adámek [3]. We know that the initial algebra of $L_\alpha$ is the nominal set $\Lambda/=\alpha$. To prove that $(\Lambda/=\alpha)_{fs}^\infty$ is the carrier of the final coalgebra amounts to showing that for all finitely presentable nominal sets $B$ we have that $\text{Nom}(B, (\Lambda/=\alpha)_{fs}^\infty)$ is the metric completion of $\text{Nom}(B, \Lambda/=\alpha)$.
## 5 An $\alpha$-corecursion principle and applications

Using corecursion, we define an $\alpha$-invariant substitution into infinitary $\lambda$-terms and we define $\alpha$-invariant notions of the infinite normal forms (Böhm, Lévy-Longo and Berarducci) discussed in Section 2. The defined notions will arise from a unique arrow into the final $L_\alpha$-coalgebra given by the nominal set $\Lambda_{\text{ffv}}^\infty/\alpha$ of Theorem 23.

**Notation 25 (Injections)** The injections for the coproduct $U+V$ are denoted as $\text{inl}^{U,V}: U \to U+V$ and $\text{inr}^{U,V}: V \to U+V$. But for the case of $L(U)$ and $L_\alpha(U)$, we denote them as

$$ 
\begin{array}{ll}
\text{inbot}^U : \{\perp\} \to L(U) & \text{inbot}_\alpha^U : \{\perp\} \to L_\alpha(U) \\
\text{invar}^U : \mathcal{V} \to L(U) & \text{invar}_\alpha^U : \mathcal{V} \to L_\alpha(U) \\
\text{inabs}^U : \mathcal{V} \times U \to L(U) & \text{inabs}_\alpha^U : [\mathcal{V}]U \to L_\alpha(U) \\
\text{inapp}^U : U \times U \to L(U) & \text{inapp}_\alpha^U : U \times U \to L_\alpha(U)
\end{array}
$$

We drop the superscripts when they are clear from the context.

**Notation 26 ($\alpha$-equivalence classes)** We write $\Lambda_\alpha$ for the (nominal) set $\Lambda/\alpha$ of finite $\lambda$-terms up to $\alpha$-equivalence and $\Lambda_\alpha^\infty$ for the (nominal) set $\Lambda_{\text{ffv}}^\infty/\alpha$ of infinitary $\lambda$-terms with finitely many free variables up to $\alpha$-equivalence (see Theorem 23). We continue to denote terms in $\Lambda$ or $\Lambda_{\text{ffv}}^\infty$ by $M, N$, but will denote terms in $\Lambda_\alpha$ or $\Lambda_\alpha^\infty$ by $M, N$.

**Notation 27 (Elements of $\Lambda_\alpha^\infty$)** Since $\text{unfold}_\alpha$ is an isomorphism that partitions its domain $\Lambda_\alpha^\infty$ into four disjoint components, see (6), we write typical elements of $\Lambda_\alpha^\infty$ as $x, \perp, M_1M_2, \lambda y.M$ where

$$ 
\begin{align}
x &= \text{unfold}_\alpha^{-1}(\text{invar}_\alpha x) \notag \\
\perp &= \text{unfold}_\alpha^{-1}(\text{inbot}_\alpha \perp) \tag{24} \\
\lambda y.M &= \text{unfold}_\alpha^{-1}(\text{inabs}_\alpha(y)M) \notag \\
M_1M_2 &= \text{unfold}_\alpha^{-1}(\text{inapp}_\alpha(M_1, M_2)) \notag
\end{align}
$$

We use $x$ to denote both an element in $\mathcal{V}$ and also its copy in $\Lambda_\alpha^\infty$.

The following lemma [21, Lemma 2.1] allows parameters in coinductive definitions. It dualises the way in which primitive recursion strengthens induction. In order to express substitution, the set $U$ will be used for the term $N$ in $M[x := N]$ which is not subject to recursion and the set $V$ will be used for the recursion.

**Lemma 28.** Let $\delta: D \to F(D)$ be a final coalgebra and $g: U \to F(U)$ an arbitrary $F$-coalgebra. Then, there is a unique map $f: V \to D$ such that for any $h: V \to F(U+V)$, the following diagram commutes:

$$ 
\begin{tikzcd}
V \arrow[r, "f"] \arrow[d, "h"] & D \arrow[d, "\delta"] \\
F(U+V) \arrow[r, "F([g^*, f])"'] & F(D)
\end{tikzcd}
$$
where $g^* : U \to D$ is the unique homomorphism between $(U, g)$ and $(D, \delta)$.

We need to fix some notation:

**Notation 29 (α-corecursion)** We consider the final $L_\alpha$-coalgebra $\mathbf{unfold}_\alpha : \Lambda_\alpha^\infty \to L_\alpha(\Lambda_\alpha^\infty)$.

1. Given $g: U \to L_\alpha(U)$, the unique map to the final $L_\alpha$-coalgebra $\mathbf{unfold}_\alpha : \Lambda^\infty \to L_\alpha(\Lambda^\infty)$ is denoted by $\mathbf{corec}_\alpha(g)$.

2. Given $g: U \to L_\alpha(U)$ and $h: V \to L_\alpha(U+V)$, the unique map from $h$ to $\mathbf{unfold}_\alpha : \Lambda^\infty \to L_\alpha(\Lambda^\infty)$ given by Lemma 28 is denoted by $\mathbf{corec}_\alpha(g, h)$.

We now define substitution using the finality of $\mathbf{unfold}_\alpha : \Lambda_\alpha^\infty \to L_\alpha(\Lambda_\alpha^\infty)$.

**Definition 30 (Substitution on α-equivalence classes).** We define substitution $\mathbf{subs}_\alpha : \Lambda_\alpha^\infty \times \mathcal{V} \times \Lambda_\alpha^\infty \to \Lambda_\alpha^\infty$ as

$$ \mathbf{subs}_\alpha = \mathbf{corec}_\alpha(\mathbf{unfold}_\alpha, \mathbf{h}_{\mathbf{subs}_\alpha}), $$

where $\mathbf{subs}_\alpha$ arises from the instance of Lemma 28, see the diagram below,

$$ \begin{tikzcd} & \Lambda_\alpha^\infty \times \mathcal{V} \times \Lambda_\alpha^\infty \arrow[r, "\mathbf{subs}_\alpha"] & \Lambda_\alpha^\infty \arrow[r, "\mathbf{h}_{\mathbf{subs}_\alpha}", "\Lambda_\alpha^\infty \to L_\alpha(\Lambda_\alpha^\infty + \Lambda_\alpha^\infty \times \mathcal{V} \times \Lambda_\alpha^\infty)"'] \arrow[d, "\Lambda_\alpha^\infty \to L_\alpha(\Lambda_\alpha^\infty)"'] \arrow[u, "\Lambda_\alpha^\infty \to L_\alpha(\Lambda_\alpha^\infty)"'] \end{tikzcd} \quad (25) $$

where $\mathbf{h}_{\mathbf{subs}_\alpha} : \Lambda_\alpha^\infty \times \mathcal{V} \times \Lambda_\alpha^\infty \to L_\alpha(\Lambda_\alpha^\infty + \Lambda_\alpha^\infty \times \mathcal{V} \times \Lambda_\alpha^\infty)$ is given by

$$ \begin{align*} \mathbf{h}_{\mathbf{subs}_\alpha}(x, x, N) &= L_\alpha \mathrm{inl}(\mathbf{unfold}_\alpha(N)) \\ \mathbf{h}_{\mathbf{subs}_\alpha}(x, y, N) &= \mathrm{invar}_\alpha x \qquad \text{if } y \neq x \\ \mathbf{h}_{\mathbf{subs}_\alpha}(\perp, y, N) &= \mathrm{inbot}_\alpha \perp \\ \mathbf{h}_{\mathbf{subs}_\alpha}(M_1 M_2, x, N) &= \mathrm{inapp}_\alpha(\mathrm{inr}(M_1, x, N), \mathrm{inr}(M_2, x, N)) \\ \mathbf{h}_{\mathbf{subs}_\alpha}(\lambda y.M, x, N) &= \mathrm{inabs}_\alpha(z)\langle\mathrm{inr}(((y)M)@z, x, N)\rangle \quad \text{if } z\#(\lambda y.M, x, N). \end{align*} $$

The map $\mathbf{h}_{\mathbf{subs}_\alpha}$ is well-defined since the last clause is independent of the choice of $z$ (which always exists due to all terms being finitely supported) and $\mathbf{h}_{\mathbf{subs}_\alpha}$ is equivariant since all operations involved, in particular abstraction and concretion, are equivariant.

**Remark 31.** To see how Definition 30 captures (3), note that, by (25), we have that $\mathbf{subs}_\alpha = \mathbf{unfold}_\alpha^{-1} \circ L_\alpha([\mathbf{unfold}_\alpha^*, \mathbf{subs}_\alpha]) \circ \mathbf{h}_{\mathbf{subs}_\alpha}$, that is, using (24) and the fact that one can choose $z = y$ in the last clause of $\mathbf{h}_{\mathbf{subs}_\alpha}$,

$$ \begin{align*} \mathbf{subs}_\alpha(x, x, N) &= N \\ \mathbf{subs}_\alpha(x, y, N) &= x \qquad \text{if } y \neq x \\ \mathbf{subs}_\alpha(\perp, y, N) &= \perp \\ \mathbf{subs}_\alpha(M_1 M_2, x, N) &= \mathbf{subs}_\alpha(M_1, x, N)\mathbf{subs}_\alpha(M_2, x, N) \\ \mathbf{subs}_\alpha(\lambda y.M, x, N) &= \lambda y.\mathbf{subs}_\alpha(M, x, N) \quad \text{if } y\#(x, N) \end{align*} $$

which looks indeed just like a notational variant of the Set-based (3), but is now fully justified as a coinductive definition on $\alpha$-equivalence classes of $\lambda$-terms.
**Definition 32 (β-reduction on α-equivalence classes).** We define $\beta_{\alpha}$-reduction as the smallest relation on $\Lambda_{\alpha}^{\infty} \times \Lambda_{\alpha}^{\infty}$ that satisfies

$$ \frac{\overline{(\lambda x.P)Q \to_{\beta_{\alpha}} \text{subs}_{\alpha}(P, x, N)} (\beta_{\alpha})}{\frac{P \to_{\beta_{\alpha}} P'}{\lambda x.P \to_{\beta_{\alpha}} \lambda x.P'} (\text{abs})} $$

$$ \frac{\frac{P \to_{\beta_{\alpha}} P'}{PQ \to_{\beta_{\alpha}} P'Q} (app_L)}{\frac{Q \to_{\beta_{\alpha}} Q'}{PQ \to_{\beta_{\alpha}} PQ'} (app_R)} $$

The informal definitions of Böhm, Lévy-Longo and Berarducci trees given in (11), (12) and (13) use the notion of β-reduction relation which is not a function. To formally define the notions of trees, we need to define evaluation strategies, i.e. some restricted notions of β-reduction which are actually partial functions.

We first define the notion of β-head reduction which contracts only the redex at the head position and corresponds to the normalising leftmost strategy. This reduction is used to define Böhm trees.

**Definition 33 (Head β-reduction on α-equivalence classes).** We define $\beta_{h\alpha}$-reduction as the smallest relation on $\Lambda_{\alpha}^{\infty} \times \Lambda_{\alpha}^{\infty}$ closed under

$$ \frac{\overline{(\lambda x.P)Q \to_{\beta_{h\alpha}} \text{subs}_{\alpha}(P, x, Q)} (\beta_{h\alpha})}{\frac{P \to_{\beta_{h\alpha}} P' \quad \text{P is not an abstraction}}{PQ \to_{\beta_{h\alpha}} P'Q} (app_L)} \frac{P \to_{\beta_{h\alpha}} P' \quad \text{P is not an abstraction}}{\lambda x.P \to_{\beta_{h\alpha}} \lambda x.P'} (\text{abs}) $$

A term M is in head normal form (hnf) if it is of the form $\lambda x_1 \dots x_n y N_1 \dots N_m$.

We restrict the β-head reduction by not contracting β-redexes in the body of an abstraction and obtain the weak head β-reduction which is needed to define the notion of Lévy-Longo tree.

**Definition 34 (Weak head β-reduction on α-equivalence classes).** We define $\beta_{wh\alpha}$-reduction as the smallest relation on $\Lambda_{\alpha}^{\infty} \times \Lambda_{\alpha}^{\infty}$ closed under

$$ (\lambda x.P)Q \to_{\beta_{wh\alpha}} \text{subs}_{\alpha}(P, x, Q) (\beta_{wh\alpha}) \frac{P \to_{\beta_{h\alpha}} P'}{PQ \to_{\beta_{wh\alpha}} P'Q} (app_L) $$

A term M is in weak head normal form (whnf) if it is either a head normal form or an abstraction.

The reflexive, transitive closure of $\to_{\beta_{\alpha}}$, $\to_{\beta_{h\alpha}}$ and $\to_{\beta_{wh\alpha}}$ are denoted by $\Rightarrow \beta_{\alpha}$, $\Rightarrow \beta_{h\alpha}$ and $\Rightarrow \beta_{wh\alpha}$, respectively.

We now define the notion of top β-reduction which only contracts β-weak head redexes at depth 0 and it will be used to define Berarducci trees.
**Definition 35 (Top β-reduction on α-equivalence classes).** We define $\beta_{t_α}$ reduction as the smallest relation on $\Lambda_\alpha^\infty \times \Lambda_\alpha^\infty$ closed under

$$ \frac{M \to_{\beta_{wh\alpha}} (\lambda x.P)}{MQ \to_{\beta_{t\alpha}} \text{subs}_\alpha(P, x, Q)} (\beta_{t\alpha}) $$

A term M is a top normal form (tnf) if it is either a weak head normal form or an application of the form NP where N cannot reduce to an abstraction.

The reflexive and transitive closure of $\to_{\beta_t}$ is denoted by $\Rightarrow_{\beta_t}$.

We now define the notion of Böhm tree, Lévy-Longo tree, and Berarducci tree using the finality of $\text{unfold}_\alpha : \Lambda_\alpha^\infty \to L_\alpha(\Lambda_\alpha^\infty)$.

**Definition 36 (Böhm tree on α-equivalence classes).** We define the Böhm tree of M as $\text{BT}_\alpha(M)$ where $\text{BT}_\alpha = \text{corec}_\alpha(\text{g}_{\text{BT}_\alpha})$ is the unique map such that

$$ \begin{array}{ccc} \Lambda_\alpha^\infty & \xrightarrow{\text{BT}_\alpha} & \Lambda_\alpha^\infty \\ \text{g}_{\text{BT}_\alpha} & \downarrow & \downarrow \\ L_\alpha(\Lambda_\alpha^\infty) & \xrightarrow{\text{BT}_\alpha} & L_\alpha(\Lambda_\alpha^\infty) \end{array} $$

commutes, with $\text{g}_{\text{BT}_\alpha} : \Lambda_\alpha^\infty \to L_\alpha(\Lambda_\alpha^\infty)$ being defined as

$$ \text{g}_{\text{BT}_\alpha}(M) = \begin{cases} \text{unfold}_\alpha N & \text{if } M \Rightarrow_{\beta_{h\alpha}} N \text{ and } N \text{ is in hnf} \\ \text{inbot}_\alpha \perp & \text{otherwise} \end{cases} $$

**Definition 37 (Lévy-Longo tree on α-equivalence classes).** We define the Lévy-Longo tree of M as $\text{LLT}_\alpha(M)$ where $\text{LLT}_\alpha = \text{corec}_\alpha(\text{g}_{\text{LLT}_\alpha})$ is the unique map such that

$$ \begin{array}{ccc} \Lambda_\alpha^\infty & \xrightarrow{\text{LLT}_\alpha} & \Lambda_\alpha^\infty \\ \text{g}_{\text{LLT}_\alpha} & \downarrow & \downarrow \\ L_\alpha(\Lambda_\alpha^\infty) & \xrightarrow{\text{LLT}_\alpha} & L_\alpha(\Lambda_\alpha^\infty) \end{array} $$

commutes, with $\text{g}_{\text{LLT}_\alpha} : \Lambda_\alpha^\infty \to L_\alpha(\Lambda_\alpha^\infty)$ being defined as

$$ \text{g}_{\text{LLT}_\alpha}(M) = \begin{cases} \text{unfold}_\alpha N & \text{if } M \Rightarrow_{\beta_{wh\alpha}} N \text{ and } N \text{ is in whnf} \\ \text{inbot}_\alpha \perp & \text{otherwise} \end{cases} $$

**Definition 38 (Berarducci tree on α-equivalence classes).** We define the Berarducci tree of M as $\text{BerT}_\alpha(M)$ where $\text{BerT}_\alpha = \text{corec}_\alpha(\text{g}_{\text{BerT}_\alpha})$ is the unique map such that

$$ \begin{array}{ccc} \Lambda_\alpha^\infty & \xrightarrow{\text{BerT}_\alpha} & \Lambda_\alpha^\infty \\ \text{g}_{\text{BerT}_\alpha} & \downarrow & \downarrow \\ L_\alpha(\Lambda_\alpha^\infty) & \xrightarrow{\text{BerT}_\alpha} & L_\alpha(\Lambda_\alpha^\infty) \end{array} $$
commutes, with $\mathbf{g}_{\text{BerT}_\alpha} : \Lambda_\alpha^\infty \to \text{L}_\alpha(\Lambda_\alpha^\infty)$ being defined as follows.

$$ \mathbf{g}_{\text{BerT}_\alpha}(M) = \begin{cases} \text{unfold}_\alpha N & \text{if } M \stackrel{\beta_{\alpha}}{\to} N \text{ and } N \text{ is in tnf} \\ \text{inbot}_\alpha \perp & \text{otherwise} \end{cases} $$

# 6 Comparison of $\alpha$-recursion and corecursion

The $\alpha$-recursion principle of [23] is based on the initial $\text{L}_\alpha$-algebra $\Lambda_\alpha$ (the principle applies of course to general functors, but we only consider the example $\text{L}_\alpha$ here). Thus, in order to make an inductive definition, that is, in order to define an arrow from $\Lambda_\alpha$ into some set $U$, one needs, in particular, to give a map $[V]U \to U$. This is done in [23] by giving a map $f : V \times U \to U$ which has to satisfy a certain condition, the freshness condition for binders (FCB). FCB makes sure that $f$ factors (uniquely) through $[V]U$, thus giving the required $[V]U \to U$.

In the coinductive case, we need instead give a map $U \to [V]U$. Note that not every equivariant $U \to [V]U$ factors through an equivariant $U \to V \times U$. So we could say that a not necessarily equivariant $U \to V \times U$ satisfies the dual of FCB if the composition $U \to V \times U \to [V]U$ is equivariant. In our examples, 'the dual of FCB' is automatic because of the equivariance of the ingredients used, see e.g. the definition of $\mathbf{h}_{\text{subs}}_\alpha$ in Definition 30.

Next we compare $\alpha$-corecursion with corecursion. Duppen [9] attempts to obtain a corecursive definition of substitution, as in (3), using the unique arrow into the final coalgebra for an endofunctor on the category Set of sets and functions. However, this approach does not take into account $\alpha$-conversion: (3) defines a partial map on $\lambda$-terms which induces a total map only on 'λ-terms up to $\alpha$-equivalence' (as can be seen, for example, by using Barendregt's variable convention [5] and comparing his definition of substitution [5, 2.1.15] with (3)).

For a general introduction to the problems arising in Set-based as opposed to Nom-based reasoning with binders, see [23, Section 1] and [22, Section 2]. Typically, Set-based induction in the presence of binders is complicated by side conditions as in (3) which lead to partial functions with the domain of definition restricted to 'safe terms' having no conflicts between free and bound variables. But 'safe terms' are not closed under the operations of abstraction and binding and so do not carry an algebra structure that can serve as a codomain $U$ to define an arrow $\Lambda \to U$ by initiality.

In the coinductive case, however, we can equip the safe terms with a coalgebra structure. The details are as follows. In analogy to Notation 29, we consider the final L-coalgebra unfold : $\Lambda^\infty \to L(\Lambda^\infty)$ and, given $g : U \to L(U)$ and $h : V \to L(U + V)$, we denote the unique map from $h : V \to L(U + V)$ to unfold : $\Lambda^\infty \to L(\Lambda^\infty)$ by corec($g, h$). The set of safe terms (with respect to substitution) is defined as $(\Lambda^\infty \times V \times \Lambda^\infty)_{\text{safe}} = \{(M, x, N) \in \Lambda^\infty \times V \times \Lambda^\infty | \text{bv}(M) \cap \text{fv}(N) = \emptyset\}$. In analogy with Definition 30, we then define substitution

$$ \text{subs} : (\Lambda^\infty \times V \times \Lambda^\infty)_{\text{safe}} \to \Lambda^\infty $$
as corec(unfold, $h_{subs}$), where $h_{subs} : (\Lambda^\infty \times \mathcal{V} \times \Lambda^\infty)_{safe} \to L(\Lambda^\infty + (\Lambda^\infty \times \mathcal{V} \times \Lambda^\infty)_{safe})$ is as in Definition 30 but with

$$h_{subs}((\lambda x.M), x, N) = \text{inabs} (x, \text{inl} (M, x, N))$$

$$h_{subs}((\lambda y.M), x, N) = \text{inabs} (y, \text{inr} (M, x, N)) \text{ if } y \neq x$$

where we have that $y \notin \text{fv}(N)$ because $\text{bv}(\lambda y.M) \cap \text{fv}(N) = \emptyset$. Although $\text{subs}$ is well-defined on safe tuples $(M, x, N)$, it is not immediately clear how to extend the definition of substitution to tuples of the form $([M]_\alpha, x, [N]_\alpha)$. As illustrated by the term $(\lambda x_0 x_1 x_0 x_1)\text{allfv}$ in the introduction, finding “safe” representatives for $\alpha$-equivalence classes of arbitrary infinitary terms is problematic.

Further, the $\beta$-rule could be defined on the set $(\Lambda^\infty)_{safe} = \{M \in \Lambda^\infty_{fv} | \text{fv}(M) \cap \text{bv}(M) = \emptyset\}$ using $\text{subs}$. Since $(\Lambda^\infty)_{safe}$ is closed under $\to_{\beta_{wh}}$, in most lazy functional programming languages which use $\beta_{wh}$-reduction such as Haskell we could work with representatives without having to consider equivalence classes. In spite of this, to define the notion of Lévy-Longo tree, we also need to extend the $\beta_{wh}$-reduction to $\Lambda^\infty_\alpha$ because the function that computes the $\beta_{wh}$-normal form is not an L-coalgebra since $P$ may not belong to $(\Lambda^\infty)_{safe}$ when $\lambda x.P \in (\Lambda^\infty)_{safe}$.

To summarize, it pays off to work in $\text{Nom}$ from the beginning, because all constructions are automatically invariant under $\alpha$-conversion.

# 7 Conclusion

As far as we know this is the first paper applying nominal techniques to the infinitary $\lambda$-calculus. In particular, we have derived a principle for making coin-ductive definitions up to $\alpha$-equivalence and applied it to fully formalising some important concepts from infinitary $\lambda$-calculus. In the context of presheaf models substitution into non-well founded syntax such as the infinitary lambda calculus has been investigated in [20].

Let us emphasise that Theorem 23 extends to other signatures. Not only is the presence of $\perp$ irrelevant for Theorem 23, it also applies if we replace $L_\alpha$ by other polynomial functors, for example by those that fall into the nominal (universal) algebra of [13]. We are confident that the future will uncover more interesting examples of $\alpha$-corecursion.

In future work we will study $\alpha$-corecursion for $\lambda$-terms that may contain infinitely many free variables, for example using the generalised theory of names [12] or the ideal-supported subsets of [8].

It will also be interesting to explore whether nominal rewriting [10] has applications in the infinitary $\lambda$-calculus.

# References

1. S. Abramsky. The lazy lambda calculus. In *Research Topics in Functional Programming*, pages 65–116. Addison-Wesley, 1990.
2. S. Abramsky and C.-H. Luke Ong. Full abstraction in the lazy lambda calculus. Inform. and Comput., 105(2):159-267, 1993.

3. J. Adámek. On final coalgebras of continuous functors. *Theor. Comput. Sci.*, 294(1/2):3–29, 2003.

4. A. Arnold and M. Nivat. The metric space of infinite trees. algebraic and topological properties. *Fundamenta Informaticae*, 4:445–476, 1980.

5. H. P. Barendregt. *The Lambda Calculus: Its Syntax and Semantics*. North-Holland, Amsterdam, Revised edition, 1984.

6. M. Barr. Terminal coalgebras for endofunctors on sets. *Theor. Comp. Sci.*, 114(2):299–315, 1999.

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

8. J. Cheney. Completeness and Herbrand theorems for nominal logic. *J. Symb. Log.*, 71(1):299–320, 2006.

9. Y. D. Duppen. A coalgebraic approach to lambda calculus. Master's thesis, Vrije Universiteit Amsterdam, 2000.

10. M. Fernández and M. Gabbay. Nominal rewriting. *Inf. Comput.*, 205(6):917–965, 2007.

11. M. Gabbay and A. M. Pitts. A new approach to abstract syntax involving binders. In *LICS*, pages 214–224, 1999.

12. M. J. Gabbay. A general mathematics of names. *Inf. Comput.*, 205(7):982–1011, 2007.

13. M. J. Gabbay and A. Mathijssen. Nominal (universal) algebra: Equational logic with names and binding. *J. Log. Comput.*, 19(6):1455–1508, 2009.

14. M. J. Gabbay and A. M. Pitts. A new approach to abstract syntax with variable binding. *Formal Aspects of Computing*, 13(3-5):341–363, 2001.

15. J. R. Kennaway and F. J. de Vries. Infinitary rewriting. In Terese, editor, *Term Rewriting Systems*, volume 55 of *Cambridge Tracts in Theor. Comp. Sci.*, pages 668–711. Cambridge University Press, 2003.

16. J. R. Kennaway, J. W. Klop, M. R. Sleep, and F. J. de Vries. Infinite lambda calculus and Böhm models. In *RTA*, volume 914 of *LNCS*, pages 257–270. Springer, 1995.

17. J. R. Kennaway, J. W. Klop, M. R. Sleep, and F. J. de Vries. Infinitary lambda calculus. *Theor. Comp. Sci.*, 175(1):93–125, 1997.

18. J.-J. Lévy. An algebraic interpretation of the λβK-calculus, and an application of a labelled λ-calculus. *Theor. Comp. Sci.*, 2(1):97–114, 1976.

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

20. R. Matthes and T. Uustalu. Substitution in non-wellfounded syntax with variable binding. *Theor. Comput. Sci*, 327:155–174, 2004.

21. L. S. Moss. Parametric corecursion. *Theor. Comp. Sci.*, 260:139–163, 2001.

22. A. M. Pitts. Nominal logic, a first order theory of names and binding. *Information and Computation*, 186:165–193, 2003.

23. A. M. Pitts. Alpha-structural recursion and induction. In Joe Hurd and Thomas F. Melham, editors, *TPHOLs*, volume 3603 of *LNCS*, pages 17–34. Springer, 2005.

24. A. Salibra. Nonmodularity results for lambda calculus. *Fundamenta Informaticae*, 45:379–392, 2001.

25. P. G. Severi and F. J. de Vries. Weakening the axiom of overlap in the infinitary lambda calculus. In *RTA*, volume 10 of *LIPIcs*, pages 313–328. Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik, 2011.