This paper appears in A Century since Principia’s Substitution Bedazzled
Haskell Curry, Fairouz Kamareddine (ed). College Publications (11 July 2023).
ISSN-10 1848904363, ISBN 13 978-1848904361. Here is the list of contents:
http://collegepublications.co.uk/contents/tbt00051.pdf []Fairouz Kamareddine

# Substitution in the $\lambda$-Calculus and the role of the Curry School

###### Abstract

Substitution plays a prominent role in the foundation and implementation of
mathematics and computation. In the $\lambda$-calculus, we cannot define
$\alpha$-congruence without a form of substitution but for substitution and
reduction to work, we need to assume a form of $\alpha$-congruence (e.g., when
we take $\lambda$-terms modulo bound variables). Students on a
$\lambda$-calculus course usually find this confusing. The elegant writings
and research of the Curry school [7, 14, 11] have settled this problem very
well. This article is an ode to the contributions of the Curry school
(especially the excellent book of Hindley and Seldin [12, 13]) on the subject
of $\alpha$-congruence and substitution.

##  1 Introduction

Jonathan Seldin completed his PhD thesis (Studies in Illative Combinatory
Logic [20]) in 1968 under the supervision of Haskell Curry at the University
of Amsterdam, and to this day, he has safeguarded all the manuscripts of Curry
as well as his legacy. This article is dedicated to Jonathan for the great
role he has played throughout the evolution of combinatory logic and the
$\lambda$-calculus.

The first half of the twentieth century had seen an explosion of new novel
ideas that would shape the foundations of mathematics and would lead to the
birth of computability. During those impressive times, new formal languages,
logics, and tools were invented that up to this day still represent the
undisputed standards for formalisation and computation. These standards
include the Turing machine, the $\lambda$-calculus, category theory,
combinatory logic and Gödel’s incompleteness. Although invented by different
people, they are all interconnected and each sheds light on the
Entscheidungsproblem in its own way. Alonzo Church gave us the
$\lambda$-calculus which is the language of the computable ($f$ is computable
iff $f$ is $\lambda$-definable), Haskell Curry gave us Combinatory Logic which
is another computation model that is equivalent to the $\lambda$-claculus.
Curry also gave us a number of concepts that we continue to heavily use today
(e.g., the Curry-Howard isomorphism which gives a correspondence between
proofs in proof systems and terms in models of computation, and the Currying
notion where a function of many arguments can be evaluated as a sequence of
unary-functions, as well as the _functionality_ concept, which became the
basis of what nowadays is called type assignment). Turing gave us another
equivalent model of computation: the Turing machine which is the machine of
the computable ($f:\mathbb{N}\mapsto\mathbb{N}$ is computable iff there is a
Turing machine $M_{f}$ that takes an input $n$ and halts with output
$f(n)$).111Samuel Eilenberg and Saunders Mac Lane gave us category theory
which is an elegant foundation of mathematics. And there was the new
developments of set theory and type theory which appropriately claim their
crucial role in the foundations of mathematics and computation. In this paper,
we only focus on the $\lambda$-calculus and on some of the lessons from the
Curry school on subtitution.

Substitution plays a prominent role in the foundation and implementation of
mathematics and computation. Bertrand Russell and others made a number of
attempts at defining substitution but most, if not all, of the attempts to
correctly define substitution with bound variables before the publication in
1934 of Hilbert and Bernays foundations of mathematics [10] were erroneous.
Although Russell’s type free substitutional theory of 1905 [19] enabled him to
prove the axiom of infinity, it also allowed contradictions and he was
frustrated by the paradoxes which as he explained in a letter to his friend
the mathematician Ralph Hawtrey "pilled the substitution theory" (see [21]).
The notion of substitution remained unsatisfactorily explained in his
Principia Mathematica.

This problem of substitution was the motivation of Curry222For Curry’s PhD
thesis (which was originally written in German) translated into English, see
[15]. to develop combinatory logic. In 1922, as a graduate student, Curry
noticed in the first chapter of Principia [22] that the rule of substitution
of well-formed formulas for propositional variables (which does not even
involve the well known complication of bound variables) was considerably more
tricky than the rule of detachment (which is equivalent to modus ponens). The
complication Curry noticed in the rule of substitution in Chapter 1 of
Principia is now considered to be the complication of its implementation by a
computer program although there were no electronic computers when Curry
noticed this.333It is precisely when Curry started looking for simpler forms
of substitution [3, 4], that he introduced some of the combinators and defined
in [5], what is nowadays called the _bracket abstract_
$[x_{1},x_{2},\cdots,x_{n}]{\mathfrak{X}}.$ Curry was able to prove that for
any term $\mathfrak{X}$ where free variables $x_{1},x_{2},\cdots,x_{n}$ may
appear, there is a term $X$ in which none of these variables appear with the
property that $Xx_{1}x_{2}\cdots x_{n}=\mathfrak{X}.$ This term $X$ is unique
by extensionality and is denoted by
$[x_{1},x_{2},\cdots,x_{n}]{\mathfrak{X}}$.

This article discusses substitution in the $\lambda$-calculus and the role of
the Curry school. One of the first hurdles after introducing students to the
extremely simple syntax of the type-free pure $\lambda$-calculus (variables,
abstraction and application) is how/when to introduce the substitution rule
and $\alpha$-congruence. In particular, should one use $\alpha$-congruence
(yes they should because $\alpha$-congruence is needed for the Church-Rosser
property of $\beta$-reduction444See Examples A1.1 and A1.2 of [13].), and
then, in which order should one introduce $\alpha$-conversion and
substitution? We cannot define $\alpha$-congruence without a form of
substitution but for substitution and reduction to work, we need to assume a
form of $\alpha$-congruence (e.g., when we take $\lambda$-terms modulo bound
variables). Students on a $\lambda$-calculus course usually find this
confusing. Moreover, to them, this does not fit with a purely syntactical
account where much of the work should be carried out using rules that can be
automated. This was behind most research on expliciting the notion of
substitution in the $\lambda$-calculus in order to bridge theory and
implementation.

The more the students appreciate the enormous intellectual debates triggered
by the paradoxes and the labour that led to the birth of computers and the
foundations and limits of computation,555Ranging from Frege’s abstraction
principle, his general concept of a function and his formalisations [8, 9], to
Russell’s paradox in Frege’s work and his monumental Principia Mathematica
[22], to Hilbert’s Entscheidungsproblem and the languages/models of Curry,
Turing, Church and others. the more they question representations that might
confuse them. Students prefer rules that they can apply or even implement to
being told to work things in their head. They get confusd if they are told at
the start that $\lambda$-terms will be taken modulo the name of their bound
variables and then shown how to build $\alpha$-reduction using substitution
and to give substitution modulo $\alpha$-equivalence classes. They ask which
is first ($\alpha$ or substitution). For them this is bothersome because they
feel that the dependence between $\alpha$-reduction and substitution is self-
referential.

The elegant writings and research of the Curry school [7, 14, 11] have settled
this problem very well. This article is an ode to the contributions of the
Curry school (especially the excellent book of Hindley and Seldin [12, 13]) on
the subject of $\alpha$-reduction and substitution.

In Section 2 we introduce the basic syntax (with the purely syntactic identity
$=_{\cal M}$), notational conventions and denotational semantics of the
$\lambda$-calculus. In Section 3 we move to computation and calculation with
$\lambda$-terms and explain the problem of the grafting $A\\{v:=B\\}$.666Which
is the purely syntactic replacement/substitution of a variable $v$ inside a
term $A$ by a term $B$. Then we introduce bound and free occurrences of
variables as well as the replacement $A\langle\langle v:=B\rangle\rangle$
based on an ordered variable list.777Which replaces/substitutes a variable $v$
inside a term $A$ by a term $B$ using an ordered variable list to avoid the
capture of free variables. We note that although calculating (which we called
$\overline{\beta}$-reducing) $\lambda$-terms using the substitution based on
an ordered variable list avoids the problem of variable capture, it does not
work on its own because the order in which a term is computed will affect the
answer. In Section 4 we discuss two alternatives to identify terms modulo
bound variables. One approach ($=_{\alpha}$) builds $\alpha$-congruence
directly from the replacement based on ordered variables while the other is
based on safe applications of grafting to build a notion $=_{\alpha^{\prime}}$
of term equivalence. Interestingly, both approaches give the same notion of
syntactic equivalence denoted by $\equiv$ where terms that only differ in the
name of their bound variables are equivalent. In Section 5 we introduce the
$\beta^{\prime}$ and $\beta^{\prime\prime}$ reduction relations. The basic
($\beta^{\prime}$) rule is the same as (${\overline{\beta}}$) but the
reflexive transitive closure $\rightarrow\rightarrow_{\beta^{\prime}}$ adds
$\alpha$-reduction in the sense that if
$A\rightarrow\rightarrow_{\beta^{\prime}}B$ then there is $C$ such that
$A\rightarrow\rightarrow_{\overline{\beta}}C\rightarrow\rightarrow_{\alpha}B$.
The basic ($\beta^{\prime\prime}$) adds $\alpha^{\prime}$-reduction to
transform the redex into a so-called clean term before any beta reduction
takes place and then safely uses grafting since this does not cause any
problems with clean terms. Not only the basic ($\beta^{\prime\prime}$) rule is
based on $\alpha^{\prime}$-reduction, but also the reflexive transitive
closure $\rightarrow\rightarrow_{\beta^{\prime\prime}}$. So, for grafting to
work, we use $\alpha^{\prime}$-reduction at the basic reduction stage (to
clean the term) and at the reflexive transitive stage. Unlike
$\overline{\beta}$-reduction, both $\beta^{\prime}$ and $\beta^{\prime\prime}$
reductions now satisfy CR. However, there is an oddity about
$\beta^{\prime\prime}$ compared to $\beta^{\prime}$. ($\beta^{\prime}$) is a
function in the sense that, if $(\lambda v.A)B\rightarrow_{\beta^{\prime}}C$
then $C$ is unique because the replacement relation for $\beta^{\prime}$ is
based on an ordered variable list.888Note that although ($\beta^{\prime}$) is
a function, $\rightarrow_{\beta^{\prime}}$ is not unless we take it as a
function of 2 arguments, the term and the particular redex-occurrence. For
example, $(\lambda x.\underline{(\lambda
y.y)x})u\rightarrow_{\beta^{\prime}}(\lambda x.x)u$ and $\underline{(\lambda
x.(\lambda y.y)x)u}\rightarrow_{\beta^{\prime}}(\lambda y.y)u$ but $(\lambda
x.x)u\not=_{\cal M}(\lambda y.y)u$. On the other hand,
($\beta^{\prime\prime}$) is not a function since ($\beta^{\prime\prime}$) uses
$\alpha^{\prime}$-reduction to clean terms. For example, we can clean
$(\lambda x.x(\lambda x.x))x$ into either $(\lambda z.z(\lambda y.y))x$ or
$(\lambda y.y(\lambda z.z))x$ and so we get $(\lambda x.x(\lambda
x.x))x\rightarrow_{\beta^{\prime\prime}}x(\lambda y.y)$ and $(\lambda
x.x(\lambda x.x))x\rightarrow_{\beta^{\prime\prime}}x(\lambda z.z)$ yet
$x(\lambda y.y)\not=_{\cal M}x(\lambda z.z)$. But since both $\beta^{\prime}$
and $\beta^{\prime\prime}$ reductions have used $\alpha/\alpha^{\prime}$
reduction and since we have built and understood the priorities and order of
substitution and equivalence classes modulo the names of bound variables
($\alpha/\alpha^{\prime}$), we can now move to the stage at which courses on
the $\lambda$-calculus usually start and take terms modulo the names of bound
variables. So in the rest of Section 5, we introduce the usual notion of
substitution and $\beta$-reduction and give a summary and comparison of all
the $\beta$-reductions introduced so far. For the sake of completeness, in
Section 6 we present the $\lambda$-calculus with de Bruijn indices where the
de Bruijn indices incorporate the equivalence classes of terms. We look at the
substitution and reduction rules with de Bruijn indices which will lead us
naturally to a calculus with explicit substitutions where we take the
classical $\lambda$-calculus with de Bruijn indices exactly as it is, but
simply turn its meta-updating and meta-substitution to the object level to
obtain a calculus of explicit substitutions. Extending $\lambda$-calculi with
explicit substitutions is essential for the implementations of these calculi.
We conclude in Section 7.

##  2 The Syntax and Denotational Semantics of the $\lambda$-calculus

######  Convention 1.

If Symb ranges over a set of entities ${\cal A}$ then also
$\mbox{Symb}^{\prime}$, $\mbox{Symb}^{\prime\prime}$, $\mbox{Symb}_{1}$,
$\mbox{Symb}_{2}$, etc., range over ${\cal A}$.

######  Definition 2 ($\lambda$-terms in ${\cal M}$).

  * •

Let ${\cal V}=\\{x,y,z,x^{\prime},y^{\prime},z^{\prime},x_{1},y_{1},\break
z_{1},\dots\\}$ be an infinite set of term variables and let meta variables
$u,v$ range over $\cal V$. By Convention 1, also $u^{\prime}$, $v_{1}$, etc.,
range over $\cal V$.
Note that ${\cal V}$ is a set and hence all its elements are pairwise
distinct.

  * •

The set of classical $\lambda$-terms (or $\lambda$-expressions) $\cal M$ is
given by:

$\cal M\>::=\>{\cal V}\>|\>(\lambda{{\cal V}}.{\cal M})\>|\>(\cal M\cal M)$.

We let capital letters $A,B,C,D,\cdots$ range over $\cal M$.

  * •

The set of contexts with one hole $\cal C$ is given by:

$\cal C\>::=\>[\>]\>|\>(\lambda{{\cal V}}.{\cal C})\>|\>(\cal C\cal
M)\>|\>(\cal M\cal C)$.

We call $[\>]$ a hole and let $C[\>],C^{\prime}[\>],C_{1}[\>],\cdots$ range
over $\cal C$.
We write $C[A]$ to denote the filling of the hole in $C[\>]$ with term $A$.
For example, if $C[\>]$ is $(\lambda x.([\>]x))$ then $C[x]$ is $(\lambda
x.(xx))$, $C[y]$ is $(\lambda x.(yx))$, and $C[(\lambda y.y)]$ is $(\lambda
x.((\lambda y.y)x))$.

  * •

The length of a term $A$ (written $\\#A$) is defined inductively as follows:
$\\#v=1\hskip 28.90755pt$ $\\#(AB)=\\#A+\\#B\hskip 28.90755pt$ $\\#(\lambda
v.A)=1+\\#A$.

######  Definition 3 (Compatibility).

We say that a relation999Note that if $R$ is a compatible relation and $ARB$,
then $C[A]RC[B]$ for any context $C[\>]$. $R$ on $\lambda$-terms is compatible
if the following hold for any $\lambda$-terms $A,B$ and $C$ and for any
variable $v$:

$\displaystyle\frac{ARB}{(AC)R(BC)}\hskip
36.135pt\displaystyle\frac{ARB}{(CA)R(CB)}\hskip
36.135pt\displaystyle\frac{ARB}{(\lambda v.A)R(\lambda v.B)}$

Here, $\displaystyle\frac{\mbox{above}}{\mbox{below}}$ means that if “above”
holds then “below” holds too.

######  Definition 4 (Strict Equality $=_{\cal M}$).

Strict equaliy $=_{\cal M}$ on the set ${\cal M}$ of $\lambda$-terms is
defined as the reflexive, transitive, symmetric and compatible closure under

$\displaystyle\frac{\mbox{$v\in{\cal V}$}}{v=v}\hskip
7.22743pt\hfill{(\mbox{Base $=_{\cal M}$})}$

Note that Strict Equality $=_{\cal M}$ is $\\{(A,A)|A\in{\cal M}\\}$.

To explain the meaning of terms, let us imagine a model ${\cal D}$ where every
$\lambda$-term denotes an element of that model. We let d range over ${\cal
D}$ (and hence by Convention 1, $\textbf{d}^{\prime}$,
$\textbf{d}^{\prime\prime}$, $\textbf{d}_{1}$, $\textbf{d}_{2}$ etc., also
range over ${\cal D}$).

The meaning of terms depends very much on the values we assign to variables.
This is why we need the so-called environment.

######  Definition 5 (ENV, Changing Environments).

We define the set of environments ENV as the set of total functions from
${\cal V}$ to ${\cal D}$. We let $\sigma$ range over ENV.

$\texttt{ENV}={\cal V}\stackrel{{\scriptstyle\hbox{\tiny
tot}}}{{\longrightarrow}}{\cal D}.$

We define the new environment $\sigma[\textbf{d}/v]\in{\cal
V}\stackrel{{\scriptstyle\hbox{\tiny tot}}}{{\longrightarrow}}{\cal D}$ as
follows:

$\sigma[\textbf{d}/v](v^{\prime})=\begin{cases}\textbf{d}&\mbox{ if
$v^{\prime}=v$}\\\ \sigma(v^{\prime})&\mbox{otherwise}\end{cases}$

Note that
$\sigma[\textbf{d}/v][\textbf{d}^{\prime}/v](v)=\textbf{d}^{\prime}$,
$\sigma[\textbf{d}/v][\textbf{d}^{\prime}/v]=\sigma[\textbf{d}^{\prime}/v]$
and if $v\not=v^{\prime}$ then
$\sigma[\textbf{d}/v][\textbf{d}^{\prime}/v^{\prime}]=\sigma[\textbf{d}^{\prime}/v^{\prime}][\textbf{d}/v]$.

######  Definition 6 (Denotational meaning of terms).

We define the following:101010Note that we defined our environments to be
total functions on ${\cal V}$ ( $\texttt{ENV}={\cal
V}\stackrel{{\scriptstyle\hbox{\tiny tot}}}{{\longrightarrow}}{\cal D}$) and
we defined our meaning function $\llbracket\>\rrbracket\in{\cal
M}\stackrel{{\scriptstyle\hbox{\tiny
tot}}}{{\longrightarrow}}(\texttt{ENV}\stackrel{{\scriptstyle\hbox{\tiny
tot}}}{{\longrightarrow}}{\cal D})$ to be a total function on ${\cal M}$ and
hence, for any $\sigma\in\texttt{ENV}$ and $A\in{\cal M}$, $\llbracket
A\rrbracket_{\sigma}$ is defined and is an element of ${\cal D}$. We also see
that when $A$ is an abstraction $(\lambda v.B)$, then $\llbracket(\lambda
v.B)\rrbracket_{\sigma}$ is a partial function in ${\cal
D}\stackrel{{\scriptstyle\circ}}{{\longrightarrow}}{\cal D}$.

  * •

The function $\llbracket\>\rrbracket\in{\cal
M}\stackrel{{\scriptstyle\hbox{\tiny
tot}}}{{\longrightarrow}}(\texttt{ENV}\stackrel{{\scriptstyle\hbox{\tiny
tot}}}{{\longrightarrow}}{\cal D})$ as follows:

    * –

$\llbracket v\rrbracket_{\sigma}=\sigma(v)$.

    * –

$\llbracket(AB)\rrbracket_{\sigma}=\llbracket A\rrbracket_{\sigma}(\llbracket
B\rrbracket_{\sigma})$.

    * –

$\llbracket(\lambda v.A)\rrbracket_{\sigma}=\textbf{f}\in{\cal
D}\stackrel{{\scriptstyle\circ}}{{\longrightarrow}}{\cal D}$ such that
$\forall\textbf{d}\in{\cal D}$, $\textbf{f}(\textbf{d})=\llbracket
A\rrbracket_{\sigma[\textbf{d}/v]}$.

  * •

$A$ and $B$ have the same meaning in environment $\sigma$ iff $\llbracket
A\rrbracket_{\sigma}=\llbracket B\rrbracket_{\sigma}$.

  * •

$\llbracket A\rrbracket=\llbracket B\rrbracket$ iff $\llbracket
A\rrbracket_{\sigma}=\llbracket B\rrbracket_{\sigma}$ for every environment
$\sigma$.

We will assume the usual parenthesis convention where application associates
to the left, outer parenthesis can be dropped, the body of a $\lambda$
includes everything that comes after it and a sequence of $\lambda$’s is
compressed to one. So, $ABCD$ denotes $(((AB)C)D)$ and $\lambda
vv^{\prime}.AB$ denotes $\lambda v.(\lambda v^{\prime}.(AB))$.

##  3 Computing $\lambda$-terms

The abstraction term $(\lambda v.A)$ alone is a bachelor waiting for its
partner. As soon as a $B$ stands to the right of the abstraction $(\lambda
v.A)$ we get a partnered couple $(\lambda v.A)B$. When the time comes and we
are ready for computation, $(\lambda v.A)B$ can produce a child ${A}_{v:=B}$
which is the body $A$ of the abstraction in which all the occurrences of $v$
are replaced by $B$ as follows: $(\lambda v.A)B\mbox{ computes to }{A}_{v:=B}$
(1) This replacement ${A}_{v:=B}$ still needs to be defined.

###  3.1 Defining ${A}_{v:=B}$ as Grafting $A\\{v:=B\\}$ does not work

One might immediately think of defining ${A}_{v:=B}$ by a strict syntactic
replacement (a.k.a. grafting) as given in Definition 7 below, however, this is
the wrong definition as we will see in Table 1.

######  Definition 7 (Grafting $A\\{v:=B\\}$).

For any $A,B,v$, we define the grafting relation $A\\{v:=B\\}$ to be the
result of syntactically replacing $B$ for every occurrence of $v$ in $A$, as
follows:111111We use $=_{def}$ here instead of M to draw attention that this
definition will not work as we will see in the rest of this paper.

$\begin{array}[]{llll}1.\>v\\{v:=B\\}&=_{def}&B\\\
2.\>v^{\prime}\\{v:=B\\}&=_{def}&v^{\prime}\hskip 36.135pt\mbox{if
$v\not=_{\cal M}v^{\prime}$}\\\
3.\>(AC)\\{v:=B\\}&=_{def}&A\\{v:=B\\}C\\{v:=B\\}\\\
4.\>(\lambda{v}.{A})\\{v:=B\\}&=_{def}&\lambda{v}.{A}\\\
5.\>(\lambda{v^{\prime}}.{A})\\{v:=B\\}&=_{def}&\lambda{v^{\prime}}.{A\\{v:=B\\}}\hskip
36.135pt\mbox{if $v\not=_{\cal M}v^{\prime}$}\end{array}$

Let $\sigma$ be an environment.
---
Let $\textbf{f},\textbf{g},\textbf{g}^{\prime}$ and h be such that
$\forall\textbf{d},\textbf{d}^{\prime}\in{\cal D}$:
$\textbf{f}(\textbf{d})(\textbf{d}^{\prime})=\textbf{d}(\textbf{d}^{\prime})$,
$\textbf{g}(\textbf{d})=\llbracket y\rrbracket_{\sigma}(\textbf{d})$,
$\textbf{g}^{\prime}(\textbf{d})=\llbracket x\rrbracket_{\sigma}(\textbf{d})$
and $\textbf{h}(\textbf{d})=\textbf{d}(\textbf{d})$.
Clearly g, $\textbf{g}^{\prime}$ and h are different and $\llbracket\lambda
z.xz\rrbracket_{\sigma}=\llbracket\lambda
y.xy\rrbracket_{\sigma}=\textbf{g}^{\prime}$.
If we allow Definition 6 to cover the $=_{def}$ of Grafting Definition 7
(i.e., if $A\\{v:=B\\}=_{def}C$ then $\llbracket
A\\{v:=B\\}\rrbracket_{\sigma}=\llbracket C\rrbracket_{\sigma}$), then:
$\bullet$ $\llbracket(\lambda
z.xz)\\{x:=y\\}\rrbracket_{\sigma}=\llbracket\lambda
z.yz\rrbracket_{\sigma}=\textbf{g}$
$\bullet$ $\llbracket(\lambda
y.xy)\\{x:=y\\}\rrbracket_{\sigma}=\llbracket\lambda
y.yy\rrbracket_{\sigma}=\textbf{h}$.
$\bullet$ So, $\llbracket\lambda z.xz\rrbracket_{\sigma}=\llbracket\lambda
y.xy\rrbracket_{\sigma}$ but $\llbracket(\lambda
z.xz)\\{x:=y\\}\rrbracket_{\sigma}\not=$
$\qquad\llbracket(\lambda y.xy)\\{x:=y\\}\rrbracket_{\sigma}$.
This is not good.
$\bullet$ If $({\lambda v.A})_{v:=B}$ is the grafting $A\\{v:=B\\}$ of
Definition 7,
then by (1):
1\. $(\lambda xz.xz)y\mbox{ computes to }(\lambda
z.xz)\\{x:=y\\}=_{def}\lambda z.yz$.
And, $\llbracket(\lambda
xz.xz)y\rrbracket_{\sigma}=\textbf{g}=\llbracket\lambda
z.yz\rrbracket_{\sigma}$.
2\. $(\lambda xy.xy)y\mbox{ computes to }(\lambda
y.xy)\\{x:=y\\}=_{def}\lambda y.yy$.
But, $\llbracket(\lambda
xy.xy)y\rrbracket_{\sigma}=\textbf{g}\not=\llbracket\lambda
y.yy\rrbracket_{\sigma}=\textbf{h}$.
This is bad and so we cannot use the computation rule $({\beta^{w}})$:
$\quad\hskip 21.68121pt\quad(\lambda v.A)B\rightarrow_{\beta^{w}}A\\{v:=B\\}$
because $(\lambda xy.xy)y$ and $(\lambda xz.xz)y$ have the same meaning g,
$(\lambda xy.xy)y\rightarrow_{\beta^{w}}\lambda y.yy$ and $(\lambda
xz.xz)y\rightarrow_{\beta^{w}}\lambda z.yz$
but $\lambda z.yz$ and $\lambda y.yy$ have different meanings (g resp. h).
Table 1: Grafting does not work

Table 1 gives examples where equation (1) is used with the grafting of
Definition 7 resulting in comptation rule $({\beta^{w}})$. As we see,
computing $(\lambda xz.xz)\leavevmode\hbox to11.4pt{\vbox
to11.4pt{\pgfpicture\makeatletter\hbox{\hskip 5.69975pt\lower-5.69975pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{
{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}{{{}}}{{}}{}{}{}{}{}{}{}{}{}{{}\pgfsys@moveto{5.49976pt}{0.0pt}\pgfsys@curveto{5.49976pt}{3.03746pt}{3.03746pt}{5.49976pt}{0.0pt}{5.49976pt}\pgfsys@curveto{-3.03746pt}{5.49976pt}{-5.49976pt}{3.03746pt}{-5.49976pt}{0.0pt}\pgfsys@curveto{-5.49976pt}{-3.03746pt}{-3.03746pt}{-5.49976pt}{0.0pt}{-5.49976pt}\pgfsys@curveto{3.03746pt}{-5.49976pt}{5.49976pt}{-3.03746pt}{5.49976pt}{0.0pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{
} }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-2.6308pt}{-1.18056pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$y$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} }
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{{{}}}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}$ to $(\lambda
z.xz)\\{x:=\leavevmode\hbox to11.4pt{\vbox
to11.4pt{\pgfpicture\makeatletter\hbox{\hskip 5.69975pt\lower-5.69975pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{
{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}{{{}}}{{}}{}{}{}{}{}{}{}{}{}{{}\pgfsys@moveto{5.49976pt}{0.0pt}\pgfsys@curveto{5.49976pt}{3.03746pt}{3.03746pt}{5.49976pt}{0.0pt}{5.49976pt}\pgfsys@curveto{-3.03746pt}{5.49976pt}{-5.49976pt}{3.03746pt}{-5.49976pt}{0.0pt}\pgfsys@curveto{-5.49976pt}{-3.03746pt}{-3.03746pt}{-5.49976pt}{0.0pt}{-5.49976pt}\pgfsys@curveto{3.03746pt}{-5.49976pt}{5.49976pt}{-3.03746pt}{5.49976pt}{0.0pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{
} }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-2.6308pt}{-1.18056pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$y$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} }
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{{{}}}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}\\}=_{def}\lambda
z.\leavevmode\hbox to11.4pt{\vbox
to11.4pt{\pgfpicture\makeatletter\hbox{\hskip 5.69975pt\lower-5.69975pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{
{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}{{{}}}{{}}{}{}{}{}{}{}{}{}{}{{}\pgfsys@moveto{5.49976pt}{0.0pt}\pgfsys@curveto{5.49976pt}{3.03746pt}{3.03746pt}{5.49976pt}{0.0pt}{5.49976pt}\pgfsys@curveto{-3.03746pt}{5.49976pt}{-5.49976pt}{3.03746pt}{-5.49976pt}{0.0pt}\pgfsys@curveto{-5.49976pt}{-3.03746pt}{-3.03746pt}{-5.49976pt}{0.0pt}{-5.49976pt}\pgfsys@curveto{3.03746pt}{-5.49976pt}{5.49976pt}{-3.03746pt}{5.49976pt}{0.0pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{
} }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-2.6308pt}{-1.18056pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$y$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} }
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{{{}}}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}z$ is correct whereas
computing $(\lambda xy.xy)\leavevmode\hbox to11.4pt{\vbox
to11.4pt{\pgfpicture\makeatletter\hbox{\hskip 5.69975pt\lower-5.69975pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{
{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}{{{}}}{{}}{}{}{}{}{}{}{}{}{}{{}\pgfsys@moveto{5.49976pt}{0.0pt}\pgfsys@curveto{5.49976pt}{3.03746pt}{3.03746pt}{5.49976pt}{0.0pt}{5.49976pt}\pgfsys@curveto{-3.03746pt}{5.49976pt}{-5.49976pt}{3.03746pt}{-5.49976pt}{0.0pt}\pgfsys@curveto{-5.49976pt}{-3.03746pt}{-3.03746pt}{-5.49976pt}{0.0pt}{-5.49976pt}\pgfsys@curveto{3.03746pt}{-5.49976pt}{5.49976pt}{-3.03746pt}{5.49976pt}{0.0pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{
} }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-2.6308pt}{-1.18056pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$y$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} }
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{{{}}}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}$ to $(\lambda
y.xy)\\{x:=\leavevmode\hbox to11.4pt{\vbox
to11.4pt{\pgfpicture\makeatletter\hbox{\hskip 5.69975pt\lower-5.69975pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{
{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}{{{}}}{{}}{}{}{}{}{}{}{}{}{}{{}\pgfsys@moveto{5.49976pt}{0.0pt}\pgfsys@curveto{5.49976pt}{3.03746pt}{3.03746pt}{5.49976pt}{0.0pt}{5.49976pt}\pgfsys@curveto{-3.03746pt}{5.49976pt}{-5.49976pt}{3.03746pt}{-5.49976pt}{0.0pt}\pgfsys@curveto{-5.49976pt}{-3.03746pt}{-3.03746pt}{-5.49976pt}{0.0pt}{-5.49976pt}\pgfsys@curveto{3.03746pt}{-5.49976pt}{5.49976pt}{-3.03746pt}{5.49976pt}{0.0pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{
} }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-2.6308pt}{-1.18056pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$y$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} }
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{{{}}}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}\\}=_{def}\lambda
y.\leavevmode\hbox to11.4pt{\vbox
to11.4pt{\pgfpicture\makeatletter\hbox{\hskip 5.69975pt\lower-5.69975pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{
{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}{{{}}}{{}}{}{}{}{}{}{}{}{}{}{{}\pgfsys@moveto{5.49976pt}{0.0pt}\pgfsys@curveto{5.49976pt}{3.03746pt}{3.03746pt}{5.49976pt}{0.0pt}{5.49976pt}\pgfsys@curveto{-3.03746pt}{5.49976pt}{-5.49976pt}{3.03746pt}{-5.49976pt}{0.0pt}\pgfsys@curveto{-5.49976pt}{-3.03746pt}{-3.03746pt}{-5.49976pt}{0.0pt}{-5.49976pt}\pgfsys@curveto{3.03746pt}{-5.49976pt}{5.49976pt}{-3.03746pt}{5.49976pt}{0.0pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{
} }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-2.6308pt}{-1.18056pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$y$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} }
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{{{}}}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}y$ is wrong. Since
$\lambda$ is a binder (like $\forall$), the $y$ which is free in the original
term $(\lambda xy.xy)\leavevmode\hbox to11.4pt{\vbox
to11.4pt{\pgfpicture\makeatletter\hbox{\hskip 5.69975pt\lower-5.69975pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{
{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}{{{}}}{{}}{}{}{}{}{}{}{}{}{}{{}\pgfsys@moveto{5.49976pt}{0.0pt}\pgfsys@curveto{5.49976pt}{3.03746pt}{3.03746pt}{5.49976pt}{0.0pt}{5.49976pt}\pgfsys@curveto{-3.03746pt}{5.49976pt}{-5.49976pt}{3.03746pt}{-5.49976pt}{0.0pt}\pgfsys@curveto{-5.49976pt}{-3.03746pt}{-3.03746pt}{-5.49976pt}{0.0pt}{-5.49976pt}\pgfsys@curveto{3.03746pt}{-5.49976pt}{5.49976pt}{-3.03746pt}{5.49976pt}{0.0pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{
} }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-2.6308pt}{-1.18056pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$y$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} }
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{{{}}}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}$ is now bound in its
computation $\lambda y.\leavevmode\hbox to11.4pt{\vbox
to11.4pt{\pgfpicture\makeatletter\hbox{\hskip 5.69975pt\lower-5.69975pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{
{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}{{{}}}{{}}{}{}{}{}{}{}{}{}{}{{}\pgfsys@moveto{5.49976pt}{0.0pt}\pgfsys@curveto{5.49976pt}{3.03746pt}{3.03746pt}{5.49976pt}{0.0pt}{5.49976pt}\pgfsys@curveto{-3.03746pt}{5.49976pt}{-5.49976pt}{3.03746pt}{-5.49976pt}{0.0pt}\pgfsys@curveto{-5.49976pt}{-3.03746pt}{-3.03746pt}{-5.49976pt}{0.0pt}{-5.49976pt}\pgfsys@curveto{3.03746pt}{-5.49976pt}{5.49976pt}{-3.03746pt}{5.49976pt}{0.0pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{
} }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-2.6308pt}{-1.18056pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$y$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} }
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{{{}}}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}y$. So $(\lambda
y.xy)\\{x:=\leavevmode\hbox to11.4pt{\vbox
to11.4pt{\pgfpicture\makeatletter\hbox{\hskip 5.69975pt\lower-5.69975pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{
{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}{{{}}}{{}}{}{}{}{}{}{}{}{}{}{{}\pgfsys@moveto{5.49976pt}{0.0pt}\pgfsys@curveto{5.49976pt}{3.03746pt}{3.03746pt}{5.49976pt}{0.0pt}{5.49976pt}\pgfsys@curveto{-3.03746pt}{5.49976pt}{-5.49976pt}{3.03746pt}{-5.49976pt}{0.0pt}\pgfsys@curveto{-5.49976pt}{-3.03746pt}{-3.03746pt}{-5.49976pt}{0.0pt}{-5.49976pt}\pgfsys@curveto{3.03746pt}{-5.49976pt}{5.49976pt}{-3.03746pt}{5.49976pt}{0.0pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{
} }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-2.6308pt}{-1.18056pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$y$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} }
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{{{}}}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}\\}$ gives the wrong
answer and we need to find a different definition of replacement which
respects the free status of $y$.

First, we define the notions of free and bound occurrences of variables.

###  3.2 Free and bound occurrences of variables

######  Definition 8 (Term Occurrence).

We define an occurrence relation between $\lambda$-terms as follows:

  * •

$A$ occurs in $A$.

  * •

If $A$ occurs in either $B$ or $C$ then $A$ occurs in $BC$.

  * •

If $A$ occurs in $B$ or $A=_{\cal M}v$ then $A$ occurs in $\lambda v.B$.

We can number the occurrences as in $\overline{xy}^{\circ_{1}}(\lambda
x.y(\lambda y.z)(\overline{xy}^{\circ_{2}}))$. When the term $A$ is a
variable, we leave out the overline as in $x^{\circ_{1}}(\lambda
x^{\circ_{2}}.y(\lambda y.z)\break(x^{\circ_{3}}z))$.

######  Definition 9 (Scope, Free/Bound Occurrences, Combinator).

  1. 1.

For a particular occurrence of a $\lambda{v}.A$ in a term $C$, we call the
occurrence of $A$ the scope of the occurrence of the $\lambda v$.

  2. 2.

We call an occurrence of a variable $v$ in a term $C$,

    1. (a)

bound if it is in the scope of a $\lambda v$ in $C$.121212That is, if the
occurrence of $v$ is inside the term $A$ of a $\lambda v.A$ which occurs in
$C$.

    2. (b)

bound and binding, if it is the $v$ of a $\lambda v$ in $C$.

    3. (c)

free if it is not bound.

  3. 3.

We say that $v$ is bound (resp. free) in $C$ if $v$ has at least one binding
(resp. free) occurrence in $C$. We write $BV(C)$ (resp. $FV(C)$) for the set
of bound (resp. free) variables of $C$.

  4. 4.

A closed expression is an expression in which all occurrences of variables are
bound. A closed expression is also called a combinator.

###  3.3 Defining ${A}_{v:=B}$ as Replacement $A\langle\langle
v:=B\rangle\rangle$ Using Ordered Variables

In order to avoid the problem of grafting as we saw in Table 1, replacement
needs to be handled with care due to the distinct roles played by bound and
free occurrences of variables. Since ${(\lambda{y}.{xy})}_{x:=\leavevmode\hbox
to8.94pt{\vbox to8.94pt{\pgfpicture\makeatletter\hbox{\hskip
4.47221pt\lower-4.47221pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{
{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}{{{}}}{{}}{}{}{}{}{}{}{}{}{}{{}\pgfsys@moveto{4.27222pt}{0.0pt}\pgfsys@curveto{4.27222pt}{2.3595pt}{2.3595pt}{4.27222pt}{0.0pt}{4.27222pt}\pgfsys@curveto{-2.3595pt}{4.27222pt}{-4.27222pt}{2.3595pt}{-4.27222pt}{0.0pt}\pgfsys@curveto{-4.27222pt}{-2.3595pt}{-2.3595pt}{-4.27222pt}{0.0pt}{-4.27222pt}\pgfsys@curveto{2.3595pt}{-4.27222pt}{4.27222pt}{-2.3595pt}{4.27222pt}{0.0pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{
} }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-1.84155pt}{-0.8264pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$y$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} }
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{{{}}}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}$ must not return
$\lambda{y}.{\leavevmode\hbox to11.4pt{\vbox
to11.4pt{\pgfpicture\makeatletter\hbox{\hskip 5.69975pt\lower-5.69975pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{
{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}{{{}}}{{}}{}{}{}{}{}{}{}{}{}{{}\pgfsys@moveto{5.49976pt}{0.0pt}\pgfsys@curveto{5.49976pt}{3.03746pt}{3.03746pt}{5.49976pt}{0.0pt}{5.49976pt}\pgfsys@curveto{-3.03746pt}{5.49976pt}{-5.49976pt}{3.03746pt}{-5.49976pt}{0.0pt}\pgfsys@curveto{-5.49976pt}{-3.03746pt}{-3.03746pt}{-5.49976pt}{0.0pt}{-5.49976pt}\pgfsys@curveto{3.03746pt}{-5.49976pt}{5.49976pt}{-3.03746pt}{5.49976pt}{0.0pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{
} }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-2.6308pt}{-1.18056pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$y$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} }
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{{{}}}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}y}$ and we should not
change the free $y$, then we should change the name of the bound variable $y$
in $\lambda{y}.{xy}$ to $v\not\in\\{x,y\\}$ obtaining $\lambda v.xv$. Then,
replacing the $x$ of $\lambda v.xv$ by $y$ gives $\lambda v.\leavevmode\hbox
to11.4pt{\vbox to11.4pt{\pgfpicture\makeatletter\hbox{\hskip
5.69975pt\lower-5.69975pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{
{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}{{{}}}{{}}{}{}{}{}{}{}{}{}{}{{}\pgfsys@moveto{5.49976pt}{0.0pt}\pgfsys@curveto{5.49976pt}{3.03746pt}{3.03746pt}{5.49976pt}{0.0pt}{5.49976pt}\pgfsys@curveto{-3.03746pt}{5.49976pt}{-5.49976pt}{3.03746pt}{-5.49976pt}{0.0pt}\pgfsys@curveto{-5.49976pt}{-3.03746pt}{-3.03746pt}{-5.49976pt}{0.0pt}{-5.49976pt}\pgfsys@curveto{3.03746pt}{-5.49976pt}{5.49976pt}{-3.03746pt}{5.49976pt}{0.0pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{
} }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-2.6308pt}{-1.18056pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$y$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} }
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{{{}}}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}v$ which is fine
because $v\not\in\\{x,y\\}$. Clearly we need to change the following rule 5.
of Definition 7:

$5.\
(\lambda{v^{\prime}}.{A})\\{v:=B\\}=_{def}\lambda{v^{\prime}}.{A\\{v:=B\\}}\hskip
36.135pt\mbox{if $v\not=_{\cal M}v^{\prime}$}.$

We could split 5. into 2 rules as follows:

$\begin{array}[]{lll}5.\>(\lambda{v^{\prime}}.{A})\\{v:=B\\}&=_{def}&\lambda{v^{\prime}}.{A\\{v:=B\\}}\hskip
36.135pt\mbox{if $v\not=_{\cal M}v^{\prime}$}\\\ &&\mbox{and
($v^{\prime}\not\in FV(B)$ or $v\not\in FV(A)$)}\\\
6.\>(\lambda{v^{\prime}}.{A})\\{v:=B\\}&=???&\lambda{v^{\prime\prime}}.{A\\{v^{\prime}:=v^{\prime\prime}}\\}\\{v:=B\\}\hskip
21.68121pt\mbox{if $v\not=_{\cal M}v^{\prime}$}\\\ &&\mbox{and ($v^{\prime}\in
FV(B)$ and $v\in FV(A)$)}\\\ &&\mbox{and $v^{\prime\prime}\not\in
FV(AB)$}\end{array}$

We still need to precise the $v^{\prime\prime}$ of rule 6. Clearly if we stick
to the strict equality of Definition 4, then $v^{\prime\prime}$ must be unique
since if $\lambda{v^{\prime\prime}_{1}}.yv^{\prime\prime}_{1}=_{\cal
M}\lambda{v^{\prime\prime}_{2}}.yv^{\prime\prime}_{2}$ then
$v^{\prime\prime}_{1}=_{\cal M}v^{\prime\prime}_{2}$ follows from the
following consequence of Definition 4:

$(\lambda v.A)=_{\cal M}(\lambda v^{\prime}.A^{\prime})\mbox{ iff ($v=_{\cal
M}v^{\prime}$ and $A=_{\cal M}A^{\prime}$)}$ (2)

One way to get a unique result in rule 6. would be to order the list of
variables ${\cal V}$ and then to take $v^{\prime\prime}$ to be the first
variable in the ordered list ${\cal V}$ which is different from $v$ and
$v^{\prime}$ and which occurs after all the free variables of $AB$. To do
this, we add to clause 6 the condition that $v^{\prime\prime}$ is the first
variable in the ordered list ${\cal V}$ which satisfies the conditions of
clause 6. That is, we replace Definition 7 by:

######  Definition 10 (Replacement $A\langle\langle v:=B\rangle\rangle$ using
ordered variables).

We define $A{\langle\langle v:=B\rangle\rangle}$ to be the result of replacing
$B$ for every free occurrence of $v$ in $A$:

$\begin{array}[]{llll}1.\>v{\langle\langle v:=B\rangle\rangle}&=_{\cal M}&B\\\
2.\>v^{\prime}{\langle\langle v:=B\rangle\rangle}&=_{\cal M}&v^{\prime}\hskip
36.135pt\mbox{if $v\not=_{\cal M}v^{\prime}$}\\\ 3.\>(AC){\langle\langle
v:=B\rangle\rangle}&=_{\cal M}&A{\langle\langle
v:=B\rangle\rangle}C{\langle\langle v:=B\rangle\rangle}\\\
4.\>(\lambda{v}.{A}){\langle\langle v:=B\rangle\rangle}&=_{\cal
M}&\lambda{v}.{A}\\\ 5.\>(\lambda{v^{\prime}}.{A}){\langle\langle
v:=B\rangle\rangle}&=_{\cal M}&\lambda{v^{\prime}}.{A{\langle\langle
v:=B\rangle\rangle}}\hskip 36.135pt\mbox{if $v\not=_{\cal M}v^{\prime}$}\\\
&&\mbox{and ($v^{\prime}\not\in FV(B)$ or $v\not\in FV(A)$)}\\\
6.\>(\lambda{v^{\prime}}.{A}){\langle\langle v:=B\rangle\rangle}&=_{\cal
M}&\lambda{v^{\prime\prime}}.{A{\langle\langle
v^{\prime}:=v^{\prime\prime}\rangle\rangle}}{\langle\langle
v:=B\rangle\rangle}\\\ &&\mbox{if $v\not=_{\cal M}v^{\prime}$}\\\ &&\mbox{and
($v^{\prime}\in FV(B)$ and $v\in FV(A)$)}\\\ &&\mbox{and $v^{\prime\prime}$ is
the first variable in the ordered}\\\ &&\mbox{variable list ${\cal V}$ such
that $v^{\prime\prime}\not\in FV(AB)$.}\end{array}$

For example, if the ascending order in ${\cal V}$ is

$x,y,z,x^{\prime},y^{\prime},z^{\prime},x^{\prime\prime},y^{\prime\prime},z^{\prime\prime},\dots$

then $z$ the first variable in this list which is different from $x$ and $y$
and which is not free in either $y$ or $xy$. So,
$(\lambda{y}.xy)\langle\langle x:=y\rangle\rangle$ can only be
$(\lambda{z}.yz)$.

The next lemma plays some initial steps of comparing grafting with replacement
using ordered variables. Note especially item 3 which shows that under some
strict conditions, grafting is replacement.

######  Lemma 1.

  1. 1.

If $v\not\in FV(A)$ then for any $B$, $A\langle\langle
v:=B\rangle\rangle=_{\cal M}A$.131313Also, if $v\not\in FV(A)$ then
$A\\{v:=B\\}=_{\cal M}A$.

  2. 2.

If $v\in FV(A)$ then $FV(A\langle\langle
v:=B\rangle\rangle)=(FV(A)\setminus\\{v\\})\cup FV(B)$.141414This does not
hold for $A\\{v:=B\\}$. E.g., $(FV(\lambda
x.y)\setminus\\{y\\})\cup\\{x\\}=\\{x\\}\not=FV((\lambda
x.y)\\{y:=x\\})=FV(\lambda x.x)=\emptyset$. However,
$FV(A\\{v:=B\\})\subseteq(FV(A)\setminus\\{v\\})\cup FV(B)$.

  3. 3.

If $v^{\prime}\not\in FV(vA)$, $v,v^{\prime}\not\in BV(A)$ then
$A\\{v:=v^{\prime}\\}=_{\cal M}A\langle\langle v:=v^{\prime}\rangle\rangle$.

  4. 4.

If $v\not=v^{\prime}$, $v\not\in FV(C)$ and whenever $\lambda
v^{\prime\prime}.D$ occurs in $A$ then $v^{\prime\prime}\not\in FV(BC)$ (i.e.,
no bound variable of $A$ occurs free in $BC$), then $A\langle\langle
v:=B\rangle\rangle\langle\langle v^{\prime}:=C\rangle\rangle=_{\cal
M}A\langle\langle v^{\prime}:=C\rangle\rangle\langle\langle v:=B\langle\langle
v^{\prime}:=C\rangle\rangle\rangle\rangle$.

###### Proof.

1\. and 2. are by induction on the derivation $A\langle\langle
v:=B\rangle\rangle$. 3. is by induction on the derivation
$A\\{v:=v^{\prime}\\}=_{def}C$. 4. is by induction on $A$. ∎

With this lemma, we are starting to see some of the complications of having to
take the first relevant variable in the ordered variable list in the
definition of $A\langle\langle v:=B\rangle\rangle$. In fact, without the
condition “whenever $\lambda v^{\prime\prime}.D$ occurs in $A$ then
$v^{\prime\prime}\not\in FV(BC)$”, we would not be able to prove Lemma 1.4.
This defeats the purpose of having an ordered list of variables.

However, there is a more substantial reason as to why an ordered list of
variables on its own will not work (see Example 1 below). As you recall, we
are trying to define the replacement ${A}_{v:=B}$ in order to define the
computation of equation (1). If we use the replacement Definition 10 to define
computation, we get this definition:

######  Definition 11.

We define $\rightarrow_{\overline{\beta}}$ as the least compatible relation
closed under:

$({\overline{\beta}})\hskip
36.135pt(\lambda{v}.A)B\rightarrow_{\overline{\beta}}A\langle\langle
v:=B\rangle\rangle\hskip 36.135pt$

We call this reduction relation $\overline{\beta}$-reduction. We define
$\rightarrow\rightarrow_{\overline{\beta}}$ as the reflexive transitive
closure of $\rightarrow_{\overline{\beta}}$.

With this definition we would lose the so-called Church-Rosser (CR) Property
which is defined for a relation $R$ as follows:

######  Definition 12.

We say that a relation $R$ on ${\cal M}$ enjoys the CR property if whenever
$ARB$ and $ARC$ then there is $D$ such that $BRD$ and $CRD$.

$\rightarrow\rightarrow_{\overline{\beta}}$ does not enjoy the CR property.
This can be seen as follows (example is taken from [13]):

######  Example 1.

$(\lambda xy.yx)((\lambda
z.x^{\prime})y)\rightarrow\rightarrow_{\overline{\beta}}\lambda y.yx^{\prime}$
and $(\lambda xy.yx)((\lambda
z.x^{\prime})y)\rightarrow\rightarrow_{\overline{\beta}}\lambda
y^{\prime}.y^{\prime}x^{\prime}$ (assuming the ordered variable list given on
page 10). It is clear that $\lambda y.yx^{\prime}\not=_{\cal M}\lambda
y^{\prime}.y^{\prime}x^{\prime}$ and there is no $D$ such that $\lambda
y.yx^{\prime}\rightarrow\rightarrow_{\overline{\beta}}D$ and $\lambda
y^{\prime}.y^{\prime}x^{\prime}\rightarrow\rightarrow_{\overline{\beta}}D$.
Note that $\llbracket\lambda y.yx^{\prime}\rrbracket=\llbracket\lambda
y^{\prime}.y^{\prime}x^{\prime}\rrbracket$.

##  4 Syntactic identity revised, Searching for $\equiv$

In the previous section we discussed computation using either grafting
($\beta^{w}$ which does not work) or replacement based on ordered variables
($\overline{\beta}$ which has its complications, and moreover, will still not
work as we saw in Example 1).

In this section we will discuss two alternatives both of which identify terms
modulo bound variables. One approach builds the so-called $\alpha$-congruence
$=_{\alpha}$ directly from the replacement based on ordered variables given in
Definition 10 (see Definition 13) while the other is based on safe
applications of the grafting of Definition 7 (see Definition 14) to build a
notion $=_{\alpha^{\prime}}$ of term equivalence. Interestingly, both
approaches give the same notion of syntactic equivalence denoted by $\equiv$
where terms that only differ in the name of their bound variables are
equivalent. For example: $\lambda{y}.{xy}\equiv\lambda{z}.{xz}$,
$\lambda{x}.{x}\equiv\lambda{y}.{y}$,
$\lambda{x^{\prime}}.yx^{\prime}{\equiv}\lambda{y^{\prime}}.yy^{\prime}$ and
$\lambda{x^{\prime}}.yx^{\prime}{\equiv}\lambda{z}.yz$, etc. Note that
$\lambda{x}.{xy}\not=_{\cal M}\lambda{z}.{xz}$, $\lambda{x}.{x}\not=_{\cal
M}\lambda{y}.{y}$, etc.

###  4.1 Defining $=_{\alpha}$ using the replacement based on ordered
variables

######  Definition 13.

We define $\rightarrow_{\alpha}$ as the least compatible relation closed
under:

$(\alpha)\hskip
36.135pt\lambda{v}.A\rightarrow_{\alpha}\lambda{v^{\prime}}.A\langle\langle
v:=v^{\prime}\rangle\rangle\hskip 36.135pt\mbox{where $v^{\prime}\not\in
FV(A)$}$

We call this reduction relation $\alpha$-reduction, $\lambda{v}.A$ an
$\alpha$-redex and$\lambda{v^{\prime}}.A\langle\langle
v:=v^{\prime}\rangle\rangle$ its $\alpha$-contractum. If $R$ is an
$\alpha$-redex, we write $\Gamma_{\alpha}[R]$ for its $\alpha$-contractum. We
define $\rightarrow\rightarrow_{\alpha}$ (resp. $=_{\alpha}$) as the reflexive
transitive (resp. equivalence) closure of $\rightarrow_{\alpha}$.

Note that $\rightarrow_{\alpha}$ is not symmetric. E.g., using the variable
list of page 10:

  * •

$\lambda xy.xy\rightarrow_{\alpha}\lambda y.(\lambda y.xy)\langle\langle
x:=y\rangle\rangle=_{\cal M}$
$\lambda y.\lambda z.(xy)\langle\langle y:=z\rangle\rangle\langle\langle
x:=y\rangle\rangle=_{\cal M}\lambda yz.yz$.

  * •

$\lambda yz.yz\rightarrow_{\alpha}\lambda x.(\lambda z.yz)\langle\langle
y:=x\rangle\rangle=_{\cal M}\lambda xz.xz\not=_{\cal M}\lambda xy.xy$.

  * •

So, $\lambda xy.xy\rightarrow_{\alpha}\lambda yz.yz$ but $\lambda
yz.yz\not\rightarrow_{\alpha}\lambda xy.xy$.
However, $\lambda yz.yz\rightarrow\rightarrow_{\alpha}\lambda xy.xy$.

In fact, $\rightarrow\rightarrow_{\alpha}$ is symmetric and hence $=_{\alpha}$
is the same relation as $\rightarrow\rightarrow_{\alpha}$. See Lemma 4.8.

Note also that $=_{\alpha}$ is closed under replacement (Definition 10), and
denotational meaning (Definition 6) and we can now remove the bound variable
conditions in Lemma 1.4 as long as we use $=_{\alpha}$ instead of $=_{\cal
M}$.

######  Lemma 2.

  1. 1.

If $A=_{\alpha}B$ then $FV(A)=FV(B)$ and $\llbracket A\rrbracket=\llbracket
B\rrbracket$.

  2. 2.

If $v\not=v^{\prime}$, $v^{\prime}\not\in FV(A)$ then $A\langle\langle
v:=v^{\prime}\rangle\rangle\langle\langle
v^{\prime}:=B\rangle\rangle=_{\alpha}A\langle\langle v:=B\rangle\rangle$.

  3. 3.

If $A=_{\alpha}B$ then $C\langle\langle
v:=A\rangle\rangle=_{\alpha}C\langle\langle v:=B\rangle\rangle$ and
$A\langle\langle v:=C\rangle\rangle=_{\alpha}B\langle\langle
v:=C\rangle\rangle$.

  4. 4.

If $v\not=v^{\prime}$ and $v\not\in FV(C)$, then $A\langle\langle
v:=B\rangle\rangle\langle\langle
v^{\prime}:=C\rangle\rangle=_{\alpha}A\langle\langle
v^{\prime}:=C\rangle\rangle\langle\langle v:=B\langle\langle
v^{\prime}:=C\rangle\rangle\rangle\rangle$.

###### Proof.

1. is by induction on the derivation $A=_{\alpha}B$ using Lemma 1.(1 and 2) for the case $A=_{\cal M}\lambda v.A^{\prime}\rightarrow_{\alpha}\lambda v^{\prime}.A^{\prime}\langle\langle v:=v^{\prime}\rangle\rangle=_{\cal M}B$ where $v^{\prime}\not\in FV(A^{\prime})$.
2. is by induction on $A$ using Lemma 1.(1 and 2). This also involves a number of sublemmas, all are proved by straightforward induction (see [6]).
3. The proof of $C\langle\langle v:=A\rangle\rangle=_{\alpha}C\langle\langle v:=B\rangle\rangle$ is by induction on $\\#A$. The proof of $A\langle\langle v:=C\rangle\rangle=_{\alpha}B\langle\langle v:=C\rangle\rangle$ is by induction on the derivation $A=_{\alpha}B$. Both proofs use 1. above.
4. By induction on $\\#A$ using Lemma 1.(1 and 2). This also involves a number of sublemmas, all are proved by straightforward induction. ∎

###  4.2 Defining $=_{\alpha^{\prime}}$

In Section 3 we stated that the use of a replacement/substitution via an
ordered list of variables suffers from complications and in Lemma 2 we saw
that we can remove the bound variables conditions in Lemma 1.4 as long as we
use $=_{\alpha}$ instead of $=_{\cal M}$. But $=_{\alpha}$ (Definition 13) is
still built on the replacement/substitution via an ordered list of variables
(Definition 10).

Can we forget completely about the ordered variable list and the replacement
notion using the ordered variable list (step 1 in the above approach), and
simply use grafting (Definition 7) to define an alternative to
$\alpha$-conversion that we can use to define $\beta$-reduction?

The next definition attempts to introduce syntactic equivalence
$=_{\alpha^{\prime}}$ which uses grafting but will coincide with the
$\alpha$-congruence (which is based on the replacement which uses an ordered
variable list). The use of grafting here will not cause problems since we are
applying grafting in a well controlled situation which is guaranteed by the
preconditions of the $({\alpha^{\prime}})$ rule (recall Lemma 1.3).

######  Definition 14.

We define $\rightarrow_{\alpha^{\prime}}$ as the compatible closure of the
following rule:

$({\alpha^{\prime}})\hskip 7.22743pt\lambda
v.A\rightarrow_{\alpha^{\prime}}\lambda v^{\prime}.A\\{v:=v^{\prime}\\}\hskip
14.45377pt\mbox{ if $v^{\prime}\not\in FV(vA)$ and $v,v^{\prime}\not\in
BV(A)$}$

We define $\rightarrow\rightarrow_{\alpha^{\prime}}$ (resp.
$=_{\alpha^{\prime}}$) as the reflexive transitive (resp. equivalence) closure
of $\rightarrow_{\alpha^{\prime}}$.

######  Lemma 3.

If $v^{\prime}\not\in FV(vA)$ and $v,v^{\prime}\not\in BV(A)$ then
$A\\{v:=v^{\prime}\\}\\{v^{\prime}:=v\\}=A$ and hence
$\rightarrow_{\alpha^{\prime}}$ (resp.
$\rightarrow\rightarrow_{\alpha^{\prime}}$) is symmetric and so,
$\rightarrow\rightarrow_{\alpha^{\prime}}$ is the same relation as
$=_{\alpha^{\prime}}$ on $\lambda$-terms.

###### Proof.

The first part is by induction on $A$. Symmetry of
$\rightarrow_{\alpha^{\prime}}$ is by induction on
$\rightarrow_{\alpha^{\prime}}$ using what we just proved. Symmetry of
$\rightarrow\rightarrow_{\alpha^{\prime}}$ then follows. ∎

Here is a lemma that establishes that using grafting inside the
$\alpha^{\prime}$ rule is safe and that $=_{\alpha}$ is the same relation as
$=_{\alpha^{\prime}}$.

######  Lemma 4.

  1. 1.

If $A\rightarrow_{\alpha^{\prime}}B$ then $\\#A=\\#B$, $FV(A)=FV(B)$ and if
$A=\lambda v.A^{\prime}$ then $B=\lambda v^{\prime}.B^{\prime}$.

  2. 2.

If $v^{\prime}\not\in FV(vA)$ and $v,v^{\prime}\not\in BV(A)$ then
$A\\{v:=v^{\prime}\\}=_{\cal M}A\langle\langle v:=v^{\prime}\rangle\rangle$.

  3. 3.

If $A\rightarrow_{\alpha^{\prime}}B$ then $A\rightarrow_{\alpha}B$. Hence if
$A\rightarrow\rightarrow_{\alpha^{\prime}}B$ (resp. $A=_{\alpha^{\prime}}B$)
then $A\rightarrow\rightarrow_{\alpha}B$ (resp. $A=_{\alpha}B$).

  4. 4.

For any $A$, $v_{1},v_{2},\cdots v_{n}$, we can find $A^{\prime}$ such that
$A\rightarrow\rightarrow_{\alpha^{\prime}}A^{\prime}$ and
$BV(A^{\prime})\cap\\{v_{1},v_{2},\cdots v_{n}\\}=\emptyset$.

  5. 5.

For any $A$, $v$ and $v^{\prime}\not\in FV(vA)$, there is $A^{\prime}$ such
that $v^{\prime}\not\in FV(vA^{\prime})$, $v,v^{\prime}\not\in
BV(A^{\prime})$, $A\rightarrow\rightarrow_{\alpha^{\prime}}A^{\prime}$ and
$A\langle\langle
v:=v^{\prime}\rangle\rangle\rightarrow\rightarrow_{\alpha^{\prime}}A^{\prime}\langle\langle
v:=v^{\prime}\rangle\rangle$.

  6. 6.

If $A\rightarrow_{\alpha}B$ then $A\rightarrow\rightarrow_{\alpha^{\prime}}B$.
Hence if $A\rightarrow\rightarrow_{\alpha}B$ (resp. $A=_{\alpha}B$) then
$A\rightarrow\rightarrow_{\alpha^{\prime}}B$ (resp. $A=_{\alpha^{\prime}}B$).

  7. 7.

$=_{\alpha}$ is the same relation as $=_{\alpha^{\prime}}$

  8. 8.

$\rightarrow\rightarrow_{\alpha}$ is symmetric.

###### Proof.

  1. 1.

Easy induction.

  2. 2.

By induction on $A$.

  3. 3.

By induction on the derivation $A\rightarrow_{\alpha^{\prime}}B$ resp.
$A\rightarrow\rightarrow_{\alpha^{\prime}}B$ resp. $A=_{\alpha^{\prime}}B$.

  4. 4.

By induction on $A$. We only do the case $A=_{\cal M}\lambda v.B$. By
induction hypothesis, there is $B^{\prime}$ such that
$B\rightarrow\rightarrow_{\alpha^{\prime}}B^{\prime}$ and
$BV(B^{\prime})\cap(\\{v_{1},v_{2},\cdots v_{n}\\}\cup\\{v\\})=\emptyset$. Let
$v^{\prime}\not\in(FV(vB^{\prime})\cup\\{v_{1},v_{2},\cdots v_{n}\\}\cup
BV(B^{\prime}))$. Then, $A=_{\cal M}\lambda
v.B\rightarrow\rightarrow_{\alpha^{\prime}}\lambda
v.B^{\prime}\rightarrow_{\alpha^{\prime}}\lambda
v^{\prime}.B^{\prime}\\{v:=v^{\prime}\\}$. Let $A^{\prime}=_{\cal M}\lambda
v^{\prime}.B^{\prime}\\{v:=v^{\prime}\\}$. Now,
$BV(A^{\prime})\cap\\{v_{1},v_{2},\cdots,v_{n}\\}=(\\{v^{\prime}\\}\cup
BV(B^{\prime}))\cap\\{v_{1},v_{2},\cdots,v_{n}\\}=(\\{v^{\prime}\\}\cap\\{v_{1},v_{2},\cdots,v_{n}\\})\cup(BV(B^{\prime})\cap\\{v_{1},v_{2},\cdots,v_{n}\\})=\emptyset$.

  5. 5.

By induction on $\\#A$. We only do the case $A=\lambda v^{\prime\prime}.B$.

     * •

Case $v^{\prime\prime}\not\in\\{v,v^{\prime}\\}$ then by the induction
hypothesis (IH), there is $B^{\prime}$ such that $v^{\prime}\not\in
FV(vB^{\prime})$, $v,v^{\prime}\not\in BV(B^{\prime})$,
$B\rightarrow\rightarrow_{\alpha^{\prime}}B^{\prime}$ and $B\langle\langle
v:=v^{\prime}\rangle\rangle\rightarrow\rightarrow_{\alpha^{\prime}}B^{\prime}\langle\langle
v:=v^{\prime}\rangle\rangle$. Hence $v^{\prime}\not\in FV(v(\lambda
v^{\prime\prime}.B^{\prime}))$, $v,v^{\prime}\not\in BV(\lambda
v^{\prime\prime}.B^{\prime})$, $\lambda
v^{\prime\prime}.B\rightarrow\rightarrow_{\alpha^{\prime}}\lambda
v^{\prime\prime}.B^{\prime}$ and $\lambda v^{\prime\prime}.B\langle\langle
v:=v^{\prime}\rangle\rangle\rightarrow\rightarrow_{\alpha^{\prime}}\lambda
v^{\prime\prime}.B^{\prime}\langle\langle v:=v^{\prime}\rangle\rangle$. But
$(\lambda v^{\prime\prime}.B)\langle\langle v:=v^{\prime}\rangle\rangle=_{\cal
M}\lambda v^{\prime\prime}.B\langle\langle v:=v^{\prime}\rangle\rangle$ and
$(\lambda v^{\prime\prime}.B^{\prime})\langle\langle
v:=v^{\prime}\rangle\rangle=_{\cal M}\lambda
v^{\prime\prime}.B^{\prime}\langle\langle v:=v^{\prime}\rangle\rangle$. We are
done.

     * •

Case $v^{\prime\prime}=v$ (i.e., $A=_{\cal M}\lambda v.B$) then by 4. and 1.
above, there is $\lambda v_{1}.B^{\prime}$ such that $\lambda
v.B\rightarrow\rightarrow_{\alpha^{\prime}}\lambda v_{1}.B^{\prime}$,
$\\#B=\\#B^{\prime}$, $FV(\lambda v.B)=FV(\lambda v_{1}.B^{\prime})$ and
$BV(\lambda v_{1}.B^{\prime})\cap\\{v,v^{\prime}\\}=\emptyset$. By IH, let $C$
be such that $B^{\prime}\rightarrow\rightarrow_{\alpha^{\prime}}C$,
$B^{\prime}\langle\langle
v:=v^{\prime}\rangle\rangle\rightarrow\rightarrow_{\alpha^{\prime}}C\langle\langle
v:=v^{\prime}\rangle\rangle$, $v^{\prime}\not\in FV(C)$ and
$v,v^{\prime}\not\in BV(C)$. Hence $\lambda
v.B\rightarrow\rightarrow_{\alpha^{\prime}}\lambda
v_{1}.B^{\prime}\rightarrow\rightarrow_{\alpha^{\prime}}\lambda v_{1}.C$,
$v^{\prime}\not\in FV(v(\lambda v_{1}.C))$, $v,v^{\prime}\not\in BV(\lambda
v_{1}.C)$, and since $v\not\in FV(\lambda v_{1}.C)$, then $(\lambda
v.B)\langle\langle v:=v^{\prime}\rangle\rangle=_{\cal M}\lambda
v.B\rightarrow\rightarrow_{\alpha^{\prime}}\lambda v_{1}.C=_{\cal M}(\lambda
v_{1}.C)\langle\langle v:=v^{\prime}\rangle\rangle$.

     * •

Case $v^{\prime\prime}=v^{\prime}$ (i.e., $A=_{\cal M}\lambda v^{\prime}.B$)
and $v\not\in FV(B)$ then by 4. and 1. above, there is $\lambda
v_{1}.B^{\prime}$ such that $\lambda
v^{\prime}.B\rightarrow\rightarrow_{\alpha^{\prime}}\lambda v_{1}.B^{\prime}$,
$\\#B=\\#B^{\prime}$, $FV(\lambda v^{\prime}.B)=FV(\lambda v_{1}.B^{\prime})$
and $BV(\lambda v_{1}.B^{\prime})\cap\\{v,v^{\prime}\\}=\emptyset$. Since
$v^{\prime}\not\in
FV(B^{\prime})\subseteq(FV(B)\setminus\\{v^{\prime}\\})\cup\\{v_{1}\\}$, then
by IH, there is $C$ such that
$B^{\prime}\rightarrow\rightarrow_{\alpha^{\prime}}C$,
$B^{\prime}\langle\langle
v:=v^{\prime}\rangle\rangle\rightarrow\rightarrow_{\alpha^{\prime}}C\langle\langle
v:=v^{\prime}\rangle\rangle$, $v^{\prime}\not\in FV(C)$ and
$v,v^{\prime}\not\in BV(C)$ and by 1. above, $v\not\in FV(C)$. Hence $\lambda
v^{\prime}.B\rightarrow\rightarrow_{\alpha^{\prime}}\lambda
v_{1}.B^{\prime}\rightarrow\rightarrow_{\alpha^{\prime}}\lambda v_{1}.C$,
$v^{\prime}\not\in FV(v(\lambda v_{1}.C))$, $v,v^{\prime}\not\in BV(\lambda
v_{1}.C)$, and since $v\not\in FV(v^{\prime}v_{1}BC)$, $(\lambda
v^{\prime}.B)\langle\langle v:=v^{\prime}\rangle\rangle=_{\cal M}\lambda
v^{\prime}.B\rightarrow\rightarrow_{\alpha^{\prime}}\lambda v_{1}.C=_{\cal
M}(\lambda v_{1}.C)\langle\langle v:=v^{\prime}\rangle\rangle$.

     * •

Case $v^{\prime\prime}=v^{\prime}$ (i.e., $A=_{\cal M}\lambda v^{\prime}.B$)
and $v\in FV(B)$ then
$(\lambda v^{\prime}.B)\langle\langle v:=v^{\prime}\rangle\rangle=_{\cal
M}\lambda v^{\prime\prime}_{1}.B\langle\langle
v^{\prime}:=v^{\prime\prime}_{1}\rangle\rangle\langle\langle
v:=v^{\prime}\rangle\rangle$ where $v^{\prime\prime}_{1}$ is the first
variable such that $v^{\prime\prime}_{1}\not\in FV(v^{\prime}B)$ (and so,
$v^{\prime\prime}_{1}\not=v$). By Lemma 1.(1 and 2), $v^{\prime}\not\in
FV(B\langle\langle v^{\prime}:=v^{\prime\prime}_{1}\rangle\rangle$. By IH,
there is $C$ such that $v^{\prime}\not\in FV(C)$, $v,v^{\prime}\not\in BV(C)$,
$B\langle\langle
v^{\prime}:=v^{\prime\prime}_{1}\rangle\rangle\rightarrow\rightarrow_{\alpha^{\prime}}C$,
$\lambda v^{\prime\prime}_{1}.B\langle\langle
v^{\prime}:=v^{\prime\prime}_{1}\rangle\rangle\rightarrow\rightarrow_{\alpha^{\prime}}\lambda
v^{\prime\prime}_{1}.C$ and
$B\langle\langle v^{\prime}:=v^{\prime\prime}_{1}\rangle\rangle\langle\langle
v:=v^{\prime}\rangle\rangle\rightarrow\rightarrow_{\alpha^{\prime}}C\langle\langle
v:=v^{\prime}\rangle\rangle$.

Hence $\lambda v^{\prime\prime}_{1}.B\langle\langle
v^{\prime}:=v^{\prime\prime}_{1}\rangle\rangle\langle\langle
v:=v^{\prime}\rangle\rangle\rightarrow\rightarrow_{\alpha^{\prime}}\lambda
v^{\prime\prime}_{1}.C\langle\langle v:=v^{\prime}\rangle\rangle$ and so,
$(\lambda v^{\prime}.B)\langle\langle
v:=v^{\prime}\rangle\rangle\rightarrow\rightarrow_{\alpha^{\prime}}(\lambda
v^{\prime\prime}_{1}.C)\langle\langle v:=v^{\prime}\rangle\rangle$.

All that is left now is to show that $\lambda
v^{\prime}.B\rightarrow\rightarrow_{\alpha^{\prime}}\lambda
v^{\prime\prime}_{1}.C$.

Since $v^{\prime\prime}_{1}\not\in FV(v^{\prime}B)$ then by IH, there is $D$
such that $v^{\prime},v^{\prime\prime}_{1}\not\in BV(D)$,
$v^{\prime\prime}_{1}\not\in FV(v^{\prime}D)$,
$B\rightarrow\rightarrow_{\alpha^{\prime}}D$, and $B\langle\langle
v^{\prime}:=v^{\prime\prime}_{1}\rangle\rangle\rightarrow\rightarrow_{\alpha^{\prime}}D\langle\langle
v^{\prime}:=v^{\prime\prime}_{1}\rangle\rangle$. Hence, $\lambda
v^{\prime}.B\rightarrow\rightarrow_{\alpha^{\prime}}\lambda v^{\prime}.D$, and
$\lambda v^{\prime\prime}_{1}.B\langle\langle
v^{\prime}:=v^{\prime\prime}_{1}\rangle\rangle\rightarrow\rightarrow_{\alpha^{\prime}}\lambda
v^{\prime\prime}_{1}.D\langle\langle
v^{\prime}:=v^{\prime\prime}_{1}\rangle\rangle$.
Since $v^{\prime},v^{\prime\prime}_{1}\not\in BV(D)$,
$v^{\prime\prime}_{1}\not\in FV(v^{\prime}D)$, then by 2. above,
$\lambda v^{\prime}.D\rightarrow_{\alpha^{\prime}}\lambda
v^{\prime\prime}_{1}.D\\{v^{\prime}:=v^{\prime\prime}_{1}\\}=_{\cal M}\lambda
v^{\prime\prime}_{1}.D\langle\langle
v^{\prime}:=v^{\prime\prime}_{1}\rangle\rangle$.
Since $\rightarrow\rightarrow_{\alpha^{\prime}}$ is symmetric (Lemma 3), then
$\lambda v^{\prime\prime}_{1}.D\langle\langle
v^{\prime}:=v^{\prime\prime}_{1}\rangle\rangle\rightarrow\rightarrow_{\alpha^{\prime}}\lambda
v^{\prime\prime}_{1}.B\langle\langle
v^{\prime}:=v^{\prime\prime}_{1}\rangle\rangle$. Hence:
$\lambda v^{\prime}B.\rightarrow\rightarrow_{\alpha^{\prime}}\lambda
v^{\prime}.D\rightarrow_{\alpha^{\prime}}\lambda
v^{\prime\prime}_{1}.D\langle\langle
v^{\prime}:=v^{\prime\prime}_{1}\rangle\rangle\rightarrow\rightarrow_{\alpha^{\prime}}\lambda
v^{\prime\prime}_{1}.B\langle\langle
v^{\prime}:=v^{\prime\prime}_{1}\rangle\rangle\rightarrow\rightarrow_{\alpha^{\prime}}\lambda
v^{\prime\prime}_{1}.C$ and we are done.

  6. 6.

The proof of
$\rightarrow_{\alpha}\subseteq\rightarrow\rightarrow_{\alpha^{\prime}}$ is by
induction on the derivation $A\rightarrow_{\alpha}B$. We only do one case.
Assume $\lambda v.C\rightarrow_{\alpha}\lambda v^{\prime}.C\langle\langle
v:=v^{\prime}\rangle\rangle$ where $v^{\prime}\not\in FV(vC)$ (the case
$v=v^{\prime}$ is trivial). Then by 5. above, there is $C^{\prime}$ such that
$v^{\prime}\not\in FV(vC^{\prime})$, $v,v^{\prime}\not\in BV(C^{\prime})$,
$C\rightarrow\rightarrow_{\alpha^{\prime}}C^{\prime}$ and $C\langle\langle
v:=v^{\prime}\rangle\rangle\rightarrow\rightarrow_{\alpha^{\prime}}C^{\prime}\langle\langle
v:=v^{\prime}\rangle\rangle$. Hence $\lambda
v.C\rightarrow\rightarrow_{\alpha^{\prime}}\lambda v.C^{\prime}$ and $\lambda
v^{\prime}.C\langle\langle
v:=v^{\prime}\rangle\rangle\rightarrow\rightarrow_{\alpha^{\prime}}\lambda
v^{\prime}.C^{\prime}\langle\langle v:=v^{\prime}\rangle\rangle$. By
symmetricity Lemma 3, $\lambda v^{\prime}.C^{\prime}\langle\langle
v:=v^{\prime}\rangle\rangle\rightarrow\rightarrow_{\alpha^{\prime}}\lambda
v^{\prime}.C\langle\langle v:=v^{\prime}\rangle\rangle$. By 2. above, $\lambda
v^{\prime}.C^{\prime}\\{v:=v^{\prime}\\}=_{\cal M}\lambda
v^{\prime}.C^{\prime}\langle\langle v:=v^{\prime}\rangle\rangle$.
Hence $\lambda v.C\rightarrow\rightarrow_{\alpha^{\prime}}\lambda
v.C^{\prime}\rightarrow_{\alpha^{\prime}}\lambda
v^{\prime}.C^{\prime}\langle\langle
v:=v^{\prime}\rangle\rangle\rightarrow\rightarrow_{\alpha^{\prime}}\lambda
v^{\prime}.C\langle\langle v:=v^{\prime}\rangle\rangle$.

  7. 7.

Use 3 and 6 above.

  8. 8.

If $A\rightarrow\rightarrow_{\alpha}B$ then by 6. above,
$A\rightarrow\rightarrow_{\alpha^{\prime}}B$ and by symmetric Lemma 3,
$B\rightarrow\rightarrow_{\alpha^{\prime}}A$ which mean by 3. above,
$B\rightarrow\rightarrow_{\alpha}A$.

∎

Now that $=_{\alpha}$ is the same as $=_{\alpha^{\prime}}$, we use $\equiv$ to
denote these relations.

######  Definition 15 ($\equiv$).

We write $A\equiv B$ iff $A=_{\alpha^{\prime}}B$ iff $A=_{\alpha}B$.
When $A\equiv B$, we say that $A$ and $B$ are syntactically equivalent.

##  5 Beta Reduction

So far, $\beta^{w}$-reduction of Table 1 does not work and
$\overline{\beta}$-reduction of Definition 11 does not satisfy CR. But, we are
ready to define the computation that will work and will guarantee CR.

###  5.1 Computation ${\beta^{\prime}}$-reduction based on $=_{\alpha}$

In this section we define the $\beta$-reduction relation (called here
${\beta^{\prime}}$) given in [13]. Note that although
$\rightarrow_{{\beta^{\prime}}}$ is the same as
$\rightarrow_{\overline{\beta}}$, a ${\beta^{\prime}}$-redex (resp.
${\beta^{\prime}}$-contractum) is also a $\overline{\beta}$-redex (resp.
${\overline{\beta}}$-contractum) and vice-versa. However, the reflexive
transitive closure $\rightarrow\rightarrow_{\beta^{\prime}}$ incorporates also
$\alpha$-reduction (unlike $\rightarrow\rightarrow_{\overline{\beta}}$).

######  Definition 16.

We define $\rightarrow_{\beta^{\prime}}$ as $\rightarrow_{\overline{\beta}}$
and similarly define a ${\beta^{\prime}}$-redex, a
${\beta^{\prime}}$-contractum and $\Gamma_{\beta^{\prime}}[R]$ when $R$ is a
$\beta^{\prime}$-redex.

We define $\rightarrow\rightarrow_{\beta^{\prime}}$ as the reflexive
transitive closure of $\rightarrow_{\beta^{\prime}}\cup\rightarrow_{\alpha}$.

Unlike $\rightarrow\rightarrow_{\overline{\beta}}$ (see Example 1), this
$\rightarrow\rightarrow_{\beta^{\prime}}$ relation satisfies the CR property
(see [12]).

The next help lemma which is based on lemmas 1.12, 1.13 and 1.14 of [13]
establishes the closure of $\alpha$-congruence under
${\beta^{\prime}}$-reduction.

######  Lemma 5.

  1. 1.

If $R$ is a ${\beta^{\prime}}$-redex and $v$, $A$ are such that $FV(vA)\cap
BV(R)=\emptyset$ then $R\langle\langle v:=A\rangle\rangle$ is a
${\beta^{\prime}}$-redex and
$\Gamma_{\beta^{\prime}}[R\langle\langle
v:=A\rangle\rangle]=_{\alpha}(\Gamma_{\beta^{\prime}}[R])\langle\langle
v:=A\rangle\rangle$.

  2. 2.

If $R$ is a ${\beta^{\prime}}$-redex and $R=_{\alpha}R^{\prime}$ then
$R^{\prime}$ is also a ${\beta^{\prime}}$-redex and
$\Gamma_{\beta^{\prime}}[R]=_{\alpha}\Gamma_{\beta^{\prime}}[R^{\prime}]$.

  3. 3.

If $A=_{\alpha}B$ and ${\beta^{\prime}}$-redex $R$ occurs in $A$, then a
${\beta^{\prime}}$-redex $R^{\prime}$ occurs in $B$ such that if
$A\rightarrow_{\beta^{\prime}}A^{\prime}$ using ${\beta^{\prime}}$-redex $R$
and $B\rightarrow_{\beta^{\prime}}B^{\prime}$ using ${\beta^{\prime}}$-redex
$R^{\prime}$, then $A^{\prime}=_{\alpha}B^{\prime}$.

###### Proof.

  * 1.

Assume $R=_{\cal M}(\lambda v^{\prime}.B)C$. Then, $v^{\prime}\not=v$ and
$v^{\prime}\not\in FV(A)$. Hence, $R\langle\langle v:=A\rangle\rangle=_{\cal
M}(\lambda v^{\prime}.B)\langle\langle v:=A\rangle\rangle C\langle\langle
v:=A\rangle\rangle=_{\cal M}(\lambda v^{\prime}.B\langle\langle
v:=A\rangle\rangle)C\langle\langle v:=A\rangle\rangle$ is a
${\beta^{\prime}}$-redex. Moreover,
$\Gamma_{\beta^{\prime}}[R\langle\langle
v:=A\rangle\rangle]=_{\alpha}B\langle\langle v:=A\rangle\rangle\langle\langle
v^{\prime}:=C\langle\langle
v:=A\rangle\rangle\rangle\rangle=_{\alpha}^{Lemma~{}\ref{orderedmeta-
sublema}.\ref{orderedmeta-sublema3}}B\langle\langle
v^{\prime}:=C\rangle\rangle\langle\langle
v:=A\rangle\rangle=_{\alpha}(\Gamma_{\beta^{\prime}}[R])\langle\langle
v:=A\rangle\rangle$.

  * 2.

By induction on the derivation $R=_{\alpha}R^{\prime}$ using Lemmas 2.(2, 3).

  * 3.

See [13], Lemma A1.14 (b).

∎

In the next lemma we connect both the ${\beta^{\prime}}$ and
$\overline{\beta}$ relations.

######  Lemma 6.

  1. 1.

$A\rightarrow_{\beta^{\prime}}B$ iff $A\rightarrow_{\overline{\beta}}B$.

  2. 2.

If $A\rightarrow\rightarrow_{\overline{\beta}}B$ then
$A\rightarrow\rightarrow_{\beta^{\prime}}B$.

  3. 3.

If $A\rightarrow\rightarrow_{\beta^{\prime}}B$ then there is $C$ such that
$A\rightarrow\rightarrow_{\overline{\beta}}C\rightarrow\rightarrow_{\alpha}B$.

###### Proof.

1. is obvious since $({\beta^{\prime}})$ and $({\overline{\beta}})$ rules are the same.
2. is a corollary of 1.
3. By definition of $\rightarrow\rightarrow_{\beta^{\prime}}$, $A\rightarrow\rightarrow_{\beta^{\prime}}B$ is a sequence (possibly empty) of $\rightarrow_{\beta^{\prime}}$ and $\rightarrow_{\alpha}$ steps. We will show that any $A_{1}\rightarrow_{\alpha}A_{2}\rightarrow_{\beta^{\prime}}A_{3}$ can be written as $A_{1}\rightarrow_{\beta^{\prime}}A_{4}\rightarrow\rightarrow_{\alpha}A_{3}$ for some $A_{4}$.

Since $A_{1}\rightarrow_{\alpha}A_{2}\rightarrow_{\beta}A_{3}$ then
$A_{1}=_{\alpha}A_{2}$ and $A_{2}\rightarrow_{\beta^{\prime}}A_{3}$ (say by
${\beta^{\prime}}$-redex $R$). By Lemma 5.3, there is a
${\beta^{\prime}}$-redex $R^{\prime}$ in $A_{1}$ such that
$A_{1}\rightarrow_{\beta^{\prime}}A_{4}$ using ${\beta^{\prime}}$-redex
$R^{\prime}$ and $A_{4}=_{\alpha}A_{3}$. But $=_{\alpha}$ is the same as
relation as $\rightarrow\rightarrow_{\alpha}$ and therefore,
$A_{1}\rightarrow_{\beta^{\prime}}A_{4}\rightarrow\rightarrow_{\alpha}A_{3}$.

This means all the $\rightarrow_{\alpha}$-steps can be postponed till after
all the $\rightarrow_{\beta^{\prime}}$-steps. By what we just proved and 1
above, if $A\rightarrow\rightarrow_{\beta^{\prime}}B$ then there is $C$ such
that
$A\rightarrow\rightarrow_{\overline{\beta}}C\rightarrow\rightarrow_{\alpha}B$.
∎

###  5.2 ${\beta^{\prime\prime}}$-reduction based on clean terms and
$=_{\alpha^{\prime}}$

In this section we define the $\beta^{\prime\prime}$-reduction relation. The
basic ($\beta^{\prime\prime}$) rule first transforms the redex into a so-
called clean term before any beta reduction takes place and uses grafting
since clean terms are safe with grafting. Here, the reflexive transitive
closure $\rightarrow\rightarrow_{\beta^{\prime\prime}}$ also incorporates
$\alpha^{\prime}$-reduction. So, for grafting to work, we use
$\alpha^{\prime}$-reduction at the basic reduction stage (to clean the term)
and at the reflexive transitive stage.

######  Definition 17.

A $\lambda$-term $A$ is clean iff the following two conditions hold:

  * •

$BV(A)\cap FV(A)=\emptyset$.

  * •

For any $v$, $\lambda v$ may occur at most once in $A$.

So $\lambda x.\lambda y.(\lambda z.xz(yz))(\lambda y.yz)$ is not clean.
However, a clean version is $\lambda x.\lambda y.(\lambda
z^{\prime}.xz^{\prime}(yz^{\prime}))(\lambda y^{\prime}.y^{\prime}z)$. Of
course a term may have different clean versions. E.g., $\lambda
x^{\prime}.\lambda y.(\lambda
z^{\prime}.x^{\prime}z^{\prime}(yz^{\prime}))(\lambda y^{\prime}.y^{\prime}z)$
is also a (different) clean version of the term above.

######  Lemma 7.

For any $A$, there is a clean $B$ such that
$A\rightarrow\rightarrow_{\alpha^{\prime}}B$.

###### Proof.

By Lemma 4.4, we can find $A^{\prime}$ such that
$A\rightarrow\rightarrow_{\alpha^{\prime}}A^{\prime}$ and
$BV(A^{\prime})\cap(FV(A)\cup BV(A))=\emptyset$. By Lemma 4.1,
$FV(A)=FV(A^{\prime})$. Hence, $BV(A^{\prime})\cap FV(A^{\prime})=\emptyset$.
If $BV(A^{\prime})=\emptyset$, we are done. Take $B$ to be $A^{\prime}$.

Else, assume that $A^{\prime}$ has $n$ $\lambda$s $\lambda v_{1},\lambda
v_{2},\cdots,\lambda v_{n}$ (note that some of the $v_{i}$s may be equal)
occurring from left to right in that order. Then $A^{\prime}=_{\cal
M}C_{n}[\lambda v_{n}.B_{n}]$ for some context $C_{n}[\>]$ and some term
$B_{n}$. Let $v^{\prime}_{n}\not\in FV(A^{\prime})\cup BV(A^{\prime})$. Hence,
$v^{\prime}_{n}\not\in FV(v_{n}B_{n})\cup BV(B_{n})$ and
$A^{\prime}\rightarrow_{\alpha^{\prime}}C_{n}[\lambda
v^{\prime}_{n}.B_{n}\\{v_{n}:=v^{\prime}_{n}\\}]=_{\cal M}A^{\prime}_{n}$.
Note that $FV(A^{\prime})=FV(A^{\prime}_{n})$, $v^{\prime}_{n}\not\in
FV(A^{\prime}_{n})$ and $A^{\prime}_{n}$ has $n$ $\lambda$s $\lambda
v_{1},\lambda v_{2},\cdots,\lambda v_{n-1},\lambda v^{\prime}_{n}$ occurring
from left to right in that order, where $\lambda v^{\prime}_{n}$ occurs once
in $A^{\prime}_{n}$ and $\\{v_{1},v_{2},\cdots,v_{n-1},\break
v^{\prime}_{n}\\}\cap FV(A^{\prime}_{n})=\emptyset$.
Repeat the above process for $\lambda v_{n-1}$ where $A^{\prime}_{n}=_{\cal
M}C_{n-1}[\lambda v_{n-1}.B_{n-1}]$ for some context $C_{n-1}$ and term
$B_{n-1}$. Let $v^{\prime}_{n-1}\not\in FV(A^{\prime}_{n})\cup
BV(A^{\prime}_{n})$. Hence, $v^{\prime}_{n-1}\not\in FV(v_{n-1}B_{n-1})\cup
BV(B_{n-1})$ and
$A^{\prime}_{n}\rightarrow_{\alpha^{\prime}}C_{n-1}\break[\lambda
v^{\prime}_{n-1}.B_{n-1}\\{v_{n-1}:=v^{\prime}_{n-1}\\}]=_{\cal
M}A^{\prime}_{n-1}$. Note that $FV(A^{\prime}_{n})=\break
FV(A^{\prime}_{n-1})$, $v^{\prime}_{n-1}\not\in FV(A^{\prime}_{n-1})$ and
$A^{\prime}_{n-1}$ has $n$ $\lambda$s $\lambda v_{1}$, $\lambda v_{2}$,
$\cdots$, $\lambda v_{n-2}$, $\lambda v^{\prime}_{n-1},\lambda v^{\prime}_{n}$
occurring from left to right in that order, where $v_{n}\not=v_{n-1}$ and each
of $\lambda v^{\prime}_{n}$ and $\lambda v^{\prime}_{n-1}$ occurs once in
$A^{\prime}_{n-1}$ and $\\{v_{1},v_{2},\cdots,v_{n-2},\break
v^{\prime}_{n-1},v^{\prime}_{n}\\}\cap FV(A^{\prime}_{n-1})=\emptyset$.
Like we constructed $A^{\prime}_{n}$, $A^{\prime}_{n-1}$, we continue to
construct $A^{\prime}_{n-2}$, $\cdots$, $A^{\prime}_{2}$, $A^{\prime}_{1}$
such that
$A^{\prime}\rightarrow_{\alpha^{\prime}}A^{\prime}_{n}\rightarrow_{\alpha^{\prime}}A^{\prime}_{n-1}\rightarrow_{\alpha^{\prime}}A^{\prime}_{n-2}\cdots\rightarrow_{\alpha^{\prime}}A^{\prime}_{1}$.
$A^{\prime}_{1}$ is the clean term we are after. ∎

######  Lemma 8.

If $(\lambda v.A)B$ is clean then $A\\{v:=B\\}=_{\cal M}A\langle\langle
v^{\prime}:=B\rangle\rangle$.

###### Proof.

By induction on $A$. ∎

Based on Lemmas 7 and 8, we can define beta reduction based on clean terms and
$\alpha^{\prime}$-reduction as follows:

######  Definition 18.

We define $\rightarrow_{\beta^{\prime\prime}}$ as the least compatible
relation closed under:

$\begin{array}[]{lll}({\beta^{\prime\prime}})&(\lambda{v}.A)B\rightarrow_{\beta^{\prime\prime}}A^{\prime}\\{v^{\prime}:=B^{\prime}\\}\\\
&\mbox{where $(\lambda v.A)B\rightarrow\rightarrow_{\alpha^{\prime}}(\lambda
v^{\prime}.A^{\prime})B^{\prime}$ and $(\lambda
v^{\prime}.A^{\prime})B^{\prime}$ is clean.}\end{array}$

We call this reduction relation ${\beta^{\prime\prime}}$-reduction. We define
$\rightarrow\rightarrow_{\beta^{\prime\prime}}$ as the reflexive transitive
closure of
$\rightarrow_{\beta^{\prime\prime}}\cup\rightarrow_{\alpha^{\prime}}$.151515Note
that in the above definition of
$\rightarrow\rightarrow_{\beta^{\prime\prime}}$, the reflexive transitive
closure of
$\rightarrow_{\beta^{\prime\prime}}\cup\rightarrow_{\alpha^{\prime}}$ is
necessary since otherwise, if we take
$\rightarrow\rightarrow_{\beta^{\prime\prime}}$ as the reflexive transitive
closure of $\rightarrow_{\beta^{\prime\prime}}$ then we would lose CR. For
example, $(\lambda x.(\lambda
x.x)x)x\rightarrow_{\beta^{\prime\prime}}x(\lambda y.y)$ and $(\lambda
x.(\lambda x.x)x)x\rightarrow_{\beta^{\prime\prime}}x(\lambda z.z)$ but in the
absence of $\rightarrow_{\alpha^{\prime}}$ we can never show that $x(\lambda
y.y)$ and $x(\lambda z.z)$ ${\beta^{\prime\prime}}$-reduce to a common term
(say $x(\lambda u.u)$).

######  Lemma 9.

  1. 1.

If $A\rightarrow_{\beta^{\prime\prime}}B$ then
$A\rightarrow\rightarrow_{\beta^{\prime}}B$.

  2. 2.

If $A\rightarrow_{\beta^{\prime}}B$ then
$A\rightarrow\rightarrow_{\beta^{\prime\prime}}B$.

###### Proof.

1\. By induction on $A\rightarrow_{\beta^{\prime\prime}}B$. For the case
$(\lambda{v}.A)B\rightarrow_{\beta^{\prime\prime}}A^{\prime}\\{v^{\prime}:=B^{\prime}\\}$
where $(\lambda v.A)B\rightarrow\rightarrow_{\alpha^{\prime}}(\lambda
v^{\prime}.A^{\prime})B^{\prime}$ and $(\lambda
v^{\prime}.A^{\prime})B^{\prime}$ is clean, use Lemmas 8 and 4.
2\. By induction on $A\rightarrow_{\beta^{\prime}}B$. We do the case
$(\lambda{v}.A)B\rightarrow_{\beta^{\prime}}A\langle\langle
v:=B\rangle\rangle$. By Lemmas 7 and 8, for a clean $(\lambda
v^{\prime}.A^{\prime})B^{\prime}$,
$(\lambda{v}.A)B\rightarrow_{\alpha^{\prime}}(\lambda
v^{\prime}.A^{\prime})B^{\prime}$ and
$(\lambda{v}.A)B\rightarrow_{\beta^{\prime\prime}}A^{\prime}\langle\langle
v^{\prime}:=B^{\prime}\rangle\rangle$. By Lemma 5.2, since
$(\lambda{v}.A)B=_{\alpha}(\lambda{v^{\prime}}.A^{\prime})B^{\prime}$ then
$A\langle\langle v:=B\rangle\rangle=_{\cal
M}\Gamma_{\beta^{\prime}}[(\lambda{v}.A)B]=_{\alpha}\Gamma_{\beta^{\prime}}[(\lambda{v^{\prime}}.A^{\prime})B^{\prime}]=_{\cal
M}A^{\prime}\langle\langle v^{\prime}:=B^{\prime}\rangle\rangle$. Hence by
Lemma 4, $A^{\prime}\langle\langle
v^{\prime}:=B^{\prime}\rangle\rangle\rightarrow\rightarrow_{\alpha^{\prime}}A\langle\langle
v:=B\rangle\rangle$ and so,
$(\lambda{v}.A)B\rightarrow\rightarrow_{\beta^{\prime\prime}}A\langle\langle
v:=B\rangle\rangle$. ∎

Since ${\beta^{\prime}}$ satisfies CR, by Lemma 9, also
${\beta^{\prime\prime}}$ satisfies CR.

However, there is an oddity about $\beta^{\prime\prime}$ compared to
$\beta^{\prime}$. The latter is a function whereas the former is not. If
$A\rightarrow_{\beta^{\prime}}B$ then $B$ is unique because the replacement
relation for $\beta^{\prime}$ is based on an ordered variable list. This is
not the case for $\rightarrow_{\beta^{\prime\prime}}$ where for example,
$(\lambda x.x(\lambda x.x))x\rightarrow_{\beta^{\prime\prime}}x(\lambda y.y)$
and $(\lambda x.x(\lambda x.x))x\rightarrow_{\beta^{\prime\prime}}x(\lambda
z.z)$ but $x(\lambda y.y)\not=x(\lambda z.z)$.

###  5.3 Equating terms modulo $\equiv$

Now that syntactic equivalence $\equiv$ is defined (and is the same relation
as $\alpha$-congruence $=_{\alpha}$ set up in terms of replacement using an
ordered variable list and $\alpha^{\prime}$-congruence $=_{\alpha^{\prime}}$
set up in terms of grafting), we could identify terms modulo syntactic
equivalence $\equiv$, and then define substitution as a refined form of both
replacement using an ordered variable list and grafting. For this, all we need
to do is to use $\equiv$ instead $=_{\cal M}$ in Definition 10 and to remove
the statement “and $v^{\prime\prime}$ is the first variable in the ordered
list ${\cal V}$” from clause 6. This gives us the following definition:

######  Definition 19 (Substitution $A[v:=B]$, using $\equiv$).

For any $A,B,v$, we define $A{[v:=B]}$ to be the result of substituting $B$
for every free occurrence of $v$ in $A$, as follows:

$\begin{array}[]{llll}1.\>v{[v:=B]}&\equiv&B\\\
2.\>v^{\prime}{[v:=B]}&\equiv&v^{\prime}\hskip 36.135pt\mbox{if
$v\not=v^{\prime}$}\\\ 3.\>(AC){[v:=B]}&\equiv&A{[v:=B]}C{[v:=B]}\\\
4.\>(\lambda{v}.{A}){[v:=B]}&\equiv&\lambda{v}.{A}\\\
5.\>(\lambda{v^{\prime}}.{A}){[v:=B]}&\equiv&\lambda{v^{\prime}}.{A{[v:=B]}}\hskip
36.135pt\mbox{if $v\not=v^{\prime}$}\\\ &&\mbox{and ($v^{\prime}\not\in FV(B)$
or $v\not\in FV(A)$)}\\\
6.\>(\lambda{v^{\prime}}.{A}){[v:=B]}&\equiv&\lambda{v^{\prime\prime}}.{A{[v^{\prime}:=v^{\prime\prime}]}}{[v:=B]}\hskip
21.68121pt\mbox{if $v\not=v^{\prime}$}\\\ &&\mbox{and ($v^{\prime}\in FV(B)$
and $v\in FV(A)$)}\\\ &&\mbox{such that $v^{\prime\prime}\not\in
FV(AB)$.}\end{array}$

Recall Lemma 2.3 which implies that if $A\equiv B$ and $C\equiv D$ then
$A\langle\langle v:=C\rangle\rangle\equiv B\langle\langle v:=D\rangle\rangle$.
Using $\equiv$ instead of $=_{\cal M}$ means that we can also move from
$A\langle\langle v:=B\rangle\rangle$ to $A[v:=B]$ as seen by the following
lemma which is proven by induction on $\\#A$.

######  Lemma 10.

For any $v$, $A$ and $B$, $A[v:=B]\equiv A\langle\langle v:=B\rangle\rangle$.

We could even go one step further in our use of $=_{\alpha}$ and use the so-
called variable convention [2] where we assume that no variable name is both
free and bound within the same term.161616Clean terms satisfy the variable
convention, but the other way round does not necessarily hold. So, we will
never have terms like $(\lambda v.B)[v:=C]$ or $(\lambda v.B)v$. Instead, the
$\lambda v$ would be changed to a $\lambda v^{\prime}$ where
$v\not=v^{\prime}$. This way, clauses 4 and 6 of Definition 19 do not hold and
we know that in clause 5, $v\not=v^{\prime}$ and ($v^{\prime}\not\in FV(B)$ or
$v\not\in FV(A)$) always hold. Hence, if we always write terms following the
variable convention, can define substitution as:

######  Definition 20.

For any $A,B,v$, we define $A{[v:=B]}$ to be the result of substituting $B$
for every free occurrence of $v$ in $A$, as follows:

$\begin{array}[]{llll}1.\>v{[v:=B]}&\equiv&B\\\
2.\>v^{\prime}{[v:=B]}&\equiv&v^{\prime}\hskip 36.135pt\mbox{if
$v\not=v^{\prime}$}\\\ 3.\>(AC){[v:=B]}&\equiv&A{[v:=B]}C{[v:=B]}\\\
5.\>(\lambda{v^{\prime}}.{A}){[v:=B]}&\equiv&\lambda{v^{\prime}}.{A{[v:=B]}}\\\
\end{array}$

So here, we always use terms modulo names of bound variables and use $\equiv$
(which is the same as $=_{\alpha}$ and $=_{\alpha^{\prime}}$). In this case,
we could use the replacement given in Definition 19. If we also want our terms
to be written according to the variable convention (where the names of bound
variables are always different from the free ones) then instead of Definition
19, we can use Definition 20. Whicever style we take here (always modulo bound
variable names, with or without variable convention), we define
$\beta$-reduction as follows:

######  Definition 21.

We define $\rightarrow_{\beta}$ as the least compatible relation closed under:

$({\beta})\hskip 36.135pt(\lambda{v}.A)B\rightarrow_{\beta}A[v:=B]\hskip
36.135pt$

We call this reduction relation $\beta$-reduction. We define
$\rightarrow\rightarrow_{\beta}$ as the reflexive transitive closure of
$\rightarrow_{\beta}$.

Let $r\in\\{{\overline{\beta}},{\beta^{\prime}},{\beta^{\prime\prime}}\\}$. It
is easy to show that $\rightarrow_{r}\subseteq\rightarrow_{\beta}$ and that,
if $A\rightarrow_{\beta}B$ then there are $A^{\prime}$, $B^{\prime}$ such that
$A^{\prime}\equiv A$, $B^{\prime}\equiv B$, and
$A^{\prime}\rightarrow_{r}B^{\prime}$.

We end this section by summarising the substitutions and $\beta$-reductions
introduced in this paper. The basic axioms introduced are:

  * •

$({\beta^{w}})\hskip 7.22743pt(\lambda
v.A)B\rightarrow_{\beta^{w}}A\\{v:=B\\}$.

  * •

$(\alpha)\hskip
7.22743pt\lambda{v}.A\rightarrow_{\alpha}\lambda{v^{\prime}}.A\langle\langle
v:=v^{\prime}\rangle\rangle\hskip 7.22743pt\mbox{where $v^{\prime}\not\in
FV(A)$}$.

  * •

$({\alpha^{\prime}})\hskip 3.61371pt\lambda
v.A\rightarrow_{\alpha^{\prime}}\lambda v^{\prime}.A\\{v:=v^{\prime}\\}\hskip
2.168pt\mbox{ if $v^{\prime}\not\in FV(vA)$ and $v,v^{\prime}\not\in BV(A).$}$

  * •

$({\overline{\beta}})\hskip
7.22743pt(\lambda{v}.A)B\rightarrow_{\overline{\beta}}A\langle\langle
v:=B\rangle\rangle.$

  * •

$({\beta^{\prime}})\hskip
7.22743pt(\lambda{v}.A)B\rightarrow_{\beta^{\prime}}A\langle\langle
v:=B\rangle\rangle.$

  * •

$\begin{array}[]{lll}({\beta^{\prime\prime}})&(\lambda{v}.A)B\rightarrow_{\beta^{\prime\prime}}A^{\prime}\\{v^{\prime}:=B^{\prime}\\}\\\
&\mbox{where $(\lambda v.A)B\rightarrow\rightarrow_{\alpha^{\prime}}(\lambda
v^{\prime}.A^{\prime})B^{\prime}$ and $(\lambda
v^{\prime}.A^{\prime})B^{\prime}$ is clean.}\end{array}$

  * •

$({\beta})\hskip 7.22743pt(\lambda v.A)B\rightarrow_{\beta}A[v:=B]$.

The reduction relations based on these axioms are:

  * •

For each
$r\in\\{{\beta^{w}},\alpha,\alpha^{\prime},\overline{\beta},{\beta^{\prime}},{\beta^{\prime\prime}},\beta\\}$:

    * –

We define $\rightarrow_{r}$ as the compatible closure of $(r)$ and call this
reduction relation $r$-reduction.

    * –

We call the term on the left (resp. right) of $\rightarrow_{r}$ in $(r)$, an
$r$-redex (resp. an $r$-contractum).

    * –

If $R$ is an $r$-redex, we write $\Gamma_{r}[R]$ for its $r$-contractum.

  * •

For each
$r\in\\{{\beta^{w}},\alpha,\alpha^{\prime},\overline{\beta},\beta\\}$, we
define $\rightarrow\rightarrow_{r}$ (resp. $=_{r}$) as the reflexive
transitive (resp. equivalence) closure of $\rightarrow_{r}$.

  * •

We define $\rightarrow\rightarrow_{\beta^{\prime}}$ as the reflexive
transitive (resp. equivalence) closure of
$\rightarrow_{\beta^{\prime}}\cup\rightarrow_{\alpha}$.

  * •

We define $\rightarrow\rightarrow_{\beta^{\prime\prime}}$ as the reflexive
transitive closure of
$\rightarrow_{\beta^{\prime\prime}}\cup\rightarrow_{\alpha^{\prime}}$.

Replacement | = on | $(\lambda v.A)B$ | Extra |  $\rightarrow\rightarrow_{r}$ | CR
---|---|---|---|---|---
$A_{v:=B}$ | ${\cal M}$ | $\rightarrow_{r}?$ |  |  |
$A\\{v:=B\\}$ | $=_{\cal M}$ |  $r=\beta^{w}$ ✗ |  |  |
|  | ? is $A_{v:=B}$ |  |  |
$A\langle\langle v:=B\rangle\rangle$ | $=_{\cal M}$ | $r=\overline{\beta}$ |  |  ref. tran. clos. | ✗
|  | ? is $A_{v:=B}$ |  |  of $\rightarrow_{r}$ |
$A\langle\langle v:=B\rangle\rangle$ | $=_{\cal M}$ | $r={\beta^{\prime}}=\overline{\beta}$ | $=_{\alpha}$ |  ref. tran. clos. | ✓
|  | ? is $A_{v:=B}$ |  |  of $\rightarrow_{r}\cup\rightarrow_{\alpha}$ |
$A\\{v:=B\\}$ | $=_{\cal M}$ | $r={\beta^{\prime\prime}}$ | $=_{\alpha^{\prime}}$ |  ref. tran. clos. | ✓
|  | ? is $A^{\prime}_{v^{\prime}:=B^{\prime}}$, |  |  of $\rightarrow_{r}\cup\rightarrow_{\alpha}$ |
|  | $(\lambda v.A)B=_{\alpha^{\prime}}$ |  |  |
|  |  $(\lambda v^{\prime}.A^{\prime})B^{\prime}$ clean |  |  |
A[v:=B] | $=_{\alpha}$ | $r=\beta$ | var. |  ref. tran. clos. | ✓
|  | ? is $A_{v:=B}$ | conv. |  of $\rightarrow_{r}$ |

##  6 The $\lambda$-calculus with de Bruijn indices,
towards Explicit Substitutions

We can avoid the problem of variable capture by getting rid of variables and
using De Bruijn indices which are natural numbers that represent the
occurrences of variables in the term. In this section, we introduce the
$\lambda$-calculus with de Bruijn indices and look at the substitution and
reduction rules with de Bruijn indices which will lead us naturally to a
calculus with explicit substitutions.

###  6.1 The classical $\lambda$-calculus with de Bruijn indices

In this approach, an index $n$ in a term $A$ is bound by the $n$th $\lambda$
on the left of $n$. For example, using de Bruijn indices, we write $\lambda
xy.yx$ and $\lambda xy.xy$ as follows:

$\lambda$${\lambda}$${1}$$2$$\lambda$${\lambda}$${2}$$1$

If $n$ is free in $A$, then we look in a so-called free variable list. Say:

$x,y,z,x^{\prime},y^{\prime},z^{\prime},x^{\prime\prime},y^{\prime\prime},z^{\prime\prime},\dots$

For example, the trees of $\lambda x.\lambda y.zxy$ and its translation
$\lambda\lambda 521$ are as follows (here $\delta$ stands for application, the
trees are drawn horizontally to save space, and the dashed lines represent the
free variable list):

$\lambda z$$\lambda y$$\lambda x$$\lambda x$$\lambda
y$$\delta$$\delta$$z$$y$$x$$\lambda$$\lambda$$\lambda$$\lambda$$\lambda$$\delta$$\delta$$5$$1$$2$

######  Definition 22.

We define $\Lambda$, the set of terms with de Bruijn indices, as follows:

$\Lambda::=\mathbb{N}\>\>|\>\>(\Lambda\Lambda)\>\>|\>\>(\lambda\Lambda)\;\;\;\;\;\;\,$

As for $\cal M$, we use $A,B,\dots$ to range over $\Lambda$. We also use
$m,n,\dots$ to range over $\mathbb{N}$ (positive natural numbers).

We use similar notational conventions and compatibility rules as before.
However, here we cannot compress a sequence of $\lambda$’s to one. While we
write $\lambda z.\lambda y.yz$ as $\lambda zy.yz$, we cannot write
$\lambda\lambda 12$ as $\lambda 12$ (which is $\lambda y.yx$).

Before we can do substitution, we must learn how to update variables. This
will be needed. For example, $\beta$-reducing
$(\lambda\lambda{\texttt{5}21})(\lambda{\texttt{3}1})$ should result in
$\lambda{\texttt{5}21}$ where the variable $2$ that was bound by the $\lambda$
that disappeared is replaced by the argument $\lambda 31$. But we cannot just
put $\lambda 31$ instead of 2 in $\lambda 521$. First, the 5 should be
decreased by 1 because one $\lambda$ has disappeared from
$\lambda\lambda{\texttt{5}21}$. Also, the 3 of $\lambda 31$ should be
increased by 1 when it is inserted in the hole of $\lambda 5[\>]1$ since the
$[\>]$ is inside an extra $\lambda$ and so all the free variables of $\lambda
31$ must be increased. The next definition introduces this updating. The
intuition behind $U^{i}_{k}$ is that $k$ tests for free variables and $i-1$ is
the value by which a variable, if free, must be incremented.

######  Definition 23.

The meta-updating functions $U^{i}_{k}:\Lambda\rightarrow\Lambda$ for $k\geq
0$ and $i\geq 1$ are defined inductively as follows:
$\begin{array}[]{l}U^{i}_{k}(AB)\equiv U^{i}_{k}(A)\,U^{i}_{k}(B)\\\\[10.0pt]
U^{i}_{k}(\lambda A)\equiv\lambda(U^{i}_{k+1}(A))\end{array}$
$\begin{array}[]{l}U^{i}_{k}({\texttt{n}})\equiv\left\\{\begin{array}[]{ll}{\texttt{n}+i-1}&\mbox{if
$\,\;n>k$}\\\ {\texttt{n}}&\mbox{if $\,\;n\leq
k\,.$}\end{array}\right.\end{array}$

Using this updating, we define substitution in the obvious way. The first two
equalities propagate the substitution through applications and abstractions
and the last one carries out the substitution of the intended variable (when
$n=i$) by the updated term. If the variable is not the intended one it must be
decreased by 1 if it is free (case $n>i$) because one $\lambda$ has
disappeared, whereas if it is bound (case $n<i$) it must remain unaltered.

######  Definition 24.

The meta-substitutions at level $\,i\,$, for $\,i\geq 1\,$, of a term
$\,B\in\Lambda\,$ in a term $\,A\in\Lambda\,$, denoted
$\,A\\{\\!\\!\\{{\texttt{i}}\leftarrow B\\}\\!\\!\\}\,$, is defined
inductively on $A$ as follows:
$\begin{array}[]{ll}(A_{1}A_{2})\\{\\!\\!\\{{i}\leftarrow
B\\}\\!\\!\\}&\equiv\>(A_{1}\\{\\!\\!\\{{i}\leftarrow
B\\}\\!\\!\\})\,(A_{2}\\{\\!\\!\\{{i}\leftarrow B\\}\\!\\!\\})\\\ (\lambda
A)\\{\\!\\!\\{{i}\leftarrow
B\\}\\!\\!\\}&\equiv\>\lambda(A\\{\\!\\!\\{{i+1}\leftarrow B\\}\\!\\!\\})\\\
{n}\\{\\!\\!\\{{i}\leftarrow
B\\}\\!\\!\\}&\equiv\>\left\\{\begin{array}[]{ll}{n-1}&\mbox{if $\,\;n>i$}\\\
U^{i}_{0}(B)&\mbox{if $\,\;n=i$}\\\ {n}&\mbox{if
$\,\;n<i\,.$}\end{array}\right.\end{array}$

The following lemma establishes the properties of the meta-substitutions and
meta-updating functions. The proof of this lemma is obtained by induction on
$A$ and can be found in [16] (the proof of 3 requires 2 with $p=0$; the proof
of 4 uses 1 and 3 both with $k=0$; finally, 5 with $p=0$ is needed to prove
6).

######  Lemma 11.

  1. 1.

For $\,k<n\leq k+i\,$ we have:
$U^{i}_{k}(A)\equiv{U^{i+1}_{k}(A)}\\{\\!\\!\\{{\texttt{n}}\\!\leftarrow\\!{B}\\}\\!\\!\\}\,$.

  2. 2.

For $\,p\leq k<j+p\,$ we have: $U^{i}_{k}(U^{j}_{p}(A))\equiv
U^{j+i-1}_{p}(A)\,.$

  3. 3.

For $\,i\leq n-k\,$ we have:
${U^{i}_{k}(A)}\\{\\!\\!\\{{\texttt{n}}\\!\leftarrow\\!{B}\\}\\!\\!\\}\equiv
U^{i}_{k}({A}\\{\\!\\!\\{{\texttt{n}-i+1}\\!\leftarrow\\!{B}\\}\\!\\!\\})\,.$

  4. 4.

[Meta-substitution lemma] For $\,1\leq i\leq n\,$ we have:
${{A}\\{\\!\\!\\{{\texttt{i}}\\!\leftarrow\\!{B}\\}\\!\\!\\}}\\{\\!\\!\\{{\texttt{n}}\\!\leftarrow\\!{C}\\}\\!\\!\\}\equiv{{A}\\{\\!\\!\\{{\texttt{n}+1}\\!\leftarrow\\!{C}\\}\\!\\!\\}}\\{\\!\\!\\{{\texttt{i}}\\!\leftarrow\\!{{B}\\{\\!\\!\\{{\texttt{n}-i+1}\\!\leftarrow\\!{C}\\}\\!\\!\\}}\\}\\!\\!\\}$.

  5. 5.

For $\,m\leq k+1\,$ we have: $U^{i}_{k+p}(U^{m}_{p}(A))\equiv
U^{m}_{p}(U^{i}_{k+p+1-m}(A))\,$.

  6. 6.

[Distribution lemma]
For $\,n\leq k+1\,$ we have:
$\begin{array}[]{l}U^{i}_{k}({A}\\{\\!\\!\\{{\texttt{n}}\\!\leftarrow\\!{B}\\}\\!\\!\\})\equiv\\\
\qquad{U^{i}_{k+1}(A)}\\{\\!\\!\\{{\texttt{n}}\\!\leftarrow\\!{U^{i}_{k-n+1}(B)}\\}\\!\\!\\}\,.\end{array}$

Case 4 is the version of Lemma 1.4 using de Bruijn indices.

######  Definition 25.

$\beta_{1}$-reduction is the least compatible relation on $\Lambda$ generated
by:
($\beta_{1}$-rule) $(\lambda
A)\,B\rightarrow_{\beta_{1}}{A}\\{\\!\\!\\{{\texttt{1}}\\!\leftarrow\\!{B}\\}\\!\\!\\}$
We define $\rightarrow\rightarrow_{\beta_{1}}$ as the reflexive transitive
closure of $\rightarrow_{\beta_{1}}$.

It is easy to check ,that
${(\lambda{\texttt{5}21})}\\{\\!\\!\\{{\texttt{1}}\\!\leftarrow\\!{(\lambda{\texttt{3}1})}\\}\\!\\!\\}\equiv\lambda{\texttt{4}}(\lambda{\texttt{4}1}){\texttt{1}}$
and hence
$(\lambda\lambda{\texttt{5}21})(\lambda{\texttt{3}1})\rightarrow_{\beta_{1}}\lambda{\texttt{4}}(\lambda{\texttt{4}1}){\texttt{1}}$.

The $\lambda$-calculi with variable names and with de Bruijn indices are
isomorphic (there are translation functions between $\cal M$ and $\Lambda$
which are inverses of each other and which preserve their respective
$\beta$-reductions, see [18]).

###  6.2 The classical $\lambda$-calculus with de Bruijn indices and explicit
substitutions

Although the $\lambda$-calculus with de Bruijn indices is not easy for humans,
it is very straightforward for machines to implement its meta-updating, meta-
substitution and beta rules. In fact, the $\lambda$-calculus with de Bruijn
has an important place in the implementations of functional languages. In this
section, we take the classical $\lambda$-calculus with de Bruijn indices
exactly as it is, but simply turn its meta-updating and meta-substitution to
the object level to obtain a calculus of explicit substitutions. Extending
$\lambda$-calculi with explicit substitutions is essential for the
implementations of these calculi.

######  Definition 26 (Syntax of the $\lambda s$-calculus).

Terms of the $\lambda s$-calculus are given by:

$\Lambda s::=\mathbb{N}\>\>|\>\>(\Lambda s\Lambda s)\>\>|\>\>(\lambda\Lambda
s)\>\>|\>\>(\Lambda s\,\sigma^{i}\Lambda s)\>\>|\>\>(\varphi^{i}_{k}\Lambda
s)\;\;\;\;\;\,where\;\;\;i\geq 1\,,\;\;k\geq 0\,.$

We use the notational conventions to get rid of unnecessary parenthesis.

Now, we need to include reduction rules that operate on the new terms built
with updating and substitutions. Definitions 23 and 24 suggest these rules.
The resulting calculus is the explicit substitution calculus $\lambda s$ of
[16] whose set of rules is given in Figure 1. Note that these rules are
nothing more than $\beta_{1}$ written now as $\sigma$-generation, together
with the rules of Definitions 23 and 24 oriented as expected.

######  Definition 27.

The set of rules $\lambda s$ is given in Figure 1.

$\sigma$-generation | $(\lambda A)\,B$ | $\longrightarrow$ | $A\,\sigma^{1}\,B$
---|---|---|---
$\sigma$-$\lambda$-transition | $(\lambda A)\,\sigma^{i}B$ | $\longrightarrow$ | $\lambda(A\,\sigma^{i+1}\,B)$
$\sigma$-app-transition | $\;\;\;(A_{1}\,A_{2})\,\sigma^{i}B$ | $\longrightarrow$ | $(A_{1}\,\sigma^{i}B)\,(A_{2}\,\sigma^{i}B)$
$\sigma$-destruction | ${\texttt{n}}\,\sigma^{i}B$ | $\longrightarrow$ | $\left\\{\begin{array}[]{ll}{\texttt{n}-1}&\mbox{if $\,\;n>i$}\\\ \varphi^{i}_{0}\,B&\mbox{if $\,\;n=i$}\\\ {\texttt{n}}&\mbox{if $\,\;n<i\,$}\end{array}\right.$
$\varphi$-$\lambda$-transition | $\varphi^{i}_{k}(\lambda A)$ | $\longrightarrow$ | $\lambda(\varphi^{i}_{k+1}\,A)$
$\varphi$-app-transition | $\varphi^{i}_{k}(A_{1}\,A_{2})$ | $\longrightarrow$ | $(\varphi^{i}_{k}\,A_{1})\,(\varphi^{i}_{k}\,A_{2})$
$\varphi$-destruction | $\varphi^{i}_{k}\,{\texttt{n}}$ | $\longrightarrow$ | $\left\\{\begin{array}[]{ll}{\texttt{n}+i-1}&\mbox{if $\,\;n>k$}\\\ {\texttt{n}}&\mbox{if $\,\;n\leq k\,\;\;\;$}\end{array}\right.$
Figure 1: The $\lambda s$-rules

The $\lambda s$-calculus is the reduction system $(\Lambda
s,\rightarrow_{\lambda s})$ where $\rightarrow_{\lambda s}$ is the least
compatible reduction on $\Lambda s$ generated by the set of rules $\lambda s$.

[16] establishes that the $s$-calculus (i.e., the reduction system whose rules
are those of Figure 1 excluding $\sigma$-generation) is strongly normalising,
that the $\lambda s$-calculus is confluent, simulates $\beta$-reduction and
has the property of preservation of strong normalisation PSN (i.e., if a term
terminates in the calculus with de Bruijn indices, then it terminates in the
$\lambda s$-calculus).

In Definition 2 we presented contexts with one hole which we used in some of
our statements and proofs about $\lambda$-terms. In fact, contexts (with one
or more holes, also known as open terms) are an important aspect of
$\lambda$-calculi and their implementations. Since extending $\lambda$-calculi
with explicit substitutions is crucial for implementations, these extensions
must also cover terms with holes. To extend the $\lambda s$-calculus with open
terms, we need to add to the syntax of $\lambda s$ variables $X,Y,\cdots$ that
range over terms. However, just adding these variables to the syntax of
$\lambda s$ and keeping the rules of Figure 1 as they are does not guarantee
confluence. For example $((\lambda
X)Y)\sigma^{1}1\rightarrow(X\sigma^{1}Y)\sigma^{1}1$ and $((\lambda
X)Y)\sigma^{1}1\rightarrow((\lambda X)\sigma^{1}1)(Y\sigma^{1}1)$ but
$(X\sigma^{1}Y)\sigma^{1}1$ and $((\lambda X)\sigma^{1}1)(Y\sigma^{1}1)$ have
no common reduct. In addition to extending the syntax with variables that
range over terms, we need to extend the rules to guarantee confluence. The
extra rules needed are none other than those of Lemma 11 oriented in the
obvious way. This results in the calculus $\lambda s_{e}$ which is confluent
on open terms [17]. Like $\lambda\sigma$ of [1], this calculus does not
satisfy PSN.

######  Definition 28 (The $\lambda s_{e}$-calculus).

Terms of the $\lambda s_{e}$-calculus are given by:
$\Lambda s_{op}::=\mbox{\bf$V$}\>\>|\>\>\mathbb{N}\>\>|\>\>(\Lambda
s_{op}\Lambda s_{op})\>\>|\>\>(\lambda\Lambda s_{op})\>\>|\>\>(\Lambda
s_{op}\,\sigma^{j}\Lambda s_{op})\>\>|\>\>(\varphi^{i}_{k}\Lambda s_{op})$
where $j,\,i\geq 1$, $k\geq 0$ and V stands for a set of variables, over which
$X$, $Y$, … range.

The set of rules $\lambda s_{e}$ is obtained by adding the rules given in
Figure 2 to the set $\lambda s$ of Figure 1.

$\sigma$-$\sigma$ | $(A\,\sigma^{i}B)\,\sigma^{j}\,C$ | $\longrightarrow$ | $(A\,\sigma^{j+1}\,C)\,\,\sigma^{i}\,(B\,\sigma^{j-i+1}\,C)$ | if | $i\leq j$
---|---|---|---|---|---
$\sigma$-$\varphi_{1}$ | $(\varphi^{i}_{k}\,A)\,\sigma^{j}\,B$ | $\longrightarrow$ | $\varphi^{i-1}_{k}\,A$ | if | $k<j<k+i$
$\sigma$-$\varphi_{2}$ | $(\varphi^{i}_{k}\,A)\,\sigma^{j}\,B$ | $\longrightarrow$ | $\varphi^{i}_{k}(A\,\sigma^{j-i+1}\,B)$ | if | $k+i\leq j$
$\varphi$-$\sigma$ | $\varphi^{i}_{k}(A\,\sigma^{j}\,B)$ | $\longrightarrow$ | $(\varphi^{i}_{k+1}\,A)\,\sigma^{j}\,(\varphi^{i}_{k+1-j}\,B)$ | if | $j\leq k+1$
$\varphi$-$\varphi_{1}$ | $\varphi^{i}_{k}\,(\varphi^{j}_{l}\,A)$ | $\longrightarrow$ | $\varphi^{j}_{l}\,(\varphi^{i}_{k+1-j}\,A)$ | if | $l+j\leq k$
$\varphi$-$\varphi_{2}$ | $\varphi^{i}_{k}\,(\varphi^{j}_{l}\,A)$ | $\longrightarrow$ | $\varphi^{j+i-1}_{l}\,A$ | if | $l\leq k<l+j$

Figure 2: The new rules of the $\lambda s_{e}$-calculus

The $\lambda s_{e}$-calculus is the reduction system $(\Lambda
s_{op},\rightarrow_{\lambda s_{e}})$ where $\rightarrow_{\lambda s_{e}}$ is
the least compatible reduction on $\Lambda s_{op}$ generated by the set of
rules $\lambda s_{e}$.

##  7 Conclusion

In this paper we discussed a number of approaches for substitution and
reduction in the $\lambda$-calculus, Most of which are influenced by the Curry
school and none of which would make sense without the lessons learned from the
Curry tradition. These notes are based on students questions where they wanted
to see the build up of terms and computation stepwise from the bottom up and
without hidden steps or working modulo classes. By working through grafting,
replacement using ordered variable lists, and then different reduction
relations based on this grafting and replacement as well as understanding the
role of variable renaming, the students are able to appreciate the move to
manipulating terms modulo $\alpha$-classes and then seem to appreciate de
Bruijn indices and the $\lambda$-calculus à la de Bruijn with or without
explicit substitutions. The $\beta^{\prime}$ reduction we saw here is the same
reduction relation given in Hindley and Seldin’s book [13] and is an accurate
representation of how we should manage variables, substitution and alpha
conversion.

## Acknowledgements

I am very appreciative for Jonathan Seldin for all the wonderful discussions
and collaboration and friendship we have had for a quarter of a century.

## References

  * [1] M. Abadi, L. Cardelli, P.-L. Curien, and J.-J. Lévy.  Explicit Substitutions.  Journal of Functional Programming, 1(4):375416, 1991.
  * [2] Henk Barendregt. _The lambda calculus - its syntax and semantics._ Studies in logic and the foundations of mathematics 103, North-Holland, 1985.
  * [3] H. B. Curry.  An Analysis of Logical Substitution.  American Journal of Mathematics, 51: 363–384, 1929.
  * [4] H. B. Curry.  On the Definition of Substitution, Replacement, and Allied Notions in an Abstract Formal System.  Revue Philosophique de Louvain, 50:251–-269, 1952.
  * [5] H. B. Curry.  Apparent variables from the standpoint of combinatory logic.  Annals of Mathematics, 34:381–404, 1933.
  * [6] H. B. Curry and R. Feys.  _Combinatory Logic_ , volume 1.  North-Holland Publishing Company, Amsterdam, 1958.
  * [7] H. B. Curry, J. R. Hindley, and J. P. Seldin.  _Combinatory Logic_ , volume 2.  North-Holland Publishing Company, Amsterdam and London, 1972.
  * [8] G. Frege.  Begriffsschrift, eine der arithmetischen nachgebildete Formelsprache des reinen Denkens. Nebert, Halle, 1879.
  * [9] G. Frege.  Grundlagen der Arithmetik, eine logisch-mathematische Untersuchung ¨uber den Begriff der Zahl. Breslau, 1884.
  * [10] D. Hilbert and P. Bernays.  Grundlagen der Mathematik, volume I.  Springer, Berlin, 1934.
  * [11] J. R. Hindley and J. P. Seldin, editors.  _To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism_.  Academic Press, New York, 1980.
  * [12] J. R. Hindley and J. P. Seldin.  _Introduction to Combinators and $\lambda$-Calculus_.  Cambridge University Press, 1986.
  * [13] J. R. Hindley and J. P. Seldin.  _Lambda-Calculus and Combinators, an Introduction_.  Cambridge University Press, 2008.
  * [14] J. R. Hindley, B. Lercher, and J. P. Seldin.  _Introduction to Combinatory Logic_.  Cambridge University Press, 1972.  London Math. Soc. Lecture Note No. 7.
  * [15] F. Kamareddine and J. P. Seldin.  Foundations of Combinatory Logic, by H.B.Curry: Translation into English. Haskell Curry, 1930, University of Goettingen, Grundlagen der kombinatorischen Logik (Foundations of Combinatory logic).  Kings College Publications. ISBN 978-1-84890-202-2. 2016.
  * [16] F. Kamareddine and A. Ríos.  A $\lambda$-calculus à la de Bruijn with Explicit Substitutions.  PLILP 1995.  Springer.
  * [17] F. Kamareddine and A. Ríos.  Extending a $\lambda$-calculus with explicit substitution which preserves strong normalisation into a confluent calculus on open terms  Journal of Functional Programming volume 7, no. (4), pages 395-420, 1997.
  * [18] M. Mauny.  Compilation des langages fonctionnels dans les combinateurs catégoriques. Application au langage ML.  PhD thesis, Université Paris VII. Paris, 1985.
  * [19] B. Russell.  On Denoting.  Mind, 14:479-493, 1905.
  * [20] J. P. Seldin.  _Studies in Illative Combinatory Logic_.  PhD thesis, University of Amsterdam, 1968.
  * [21] A. Urquhart.  Russell and Gödel. The Bulletin of Symbolic Logic , DECEMBER 2016, Vol. 22, No. 4, pp. 504-520.
  * [22] A. N. Whitehead and B. Russell.  Principia Mathematica.  Cambridge University Press, Cambridge, England, 1910–1913.  Second edition, 1925–1927.