$\mathsf{w}\in\reflectbox{{F}}(\mathsf{G})\cap\reflectbox{{B}}(\mathsf{G})\cap\reflectbox{{F}}(\mathsf{D})\cap(\mathbb{V}\setminus\\{\,\\!\mathsf{x}\,\\!\\})$
and let
$\mathsf{M}\stackrel{{\scriptstyle\text{\tiny{DEF}}}}{{=}}\lambda\mathsf{w}\langle\mathsf{w}/\mathsf{x}\rangle(\mathsf{G})$.
Since
$\mathsf{w}\in\reflectbox{{F}}(\mathsf{G})\cap\reflectbox{{B}}(\mathsf{G})$ it
follows that $\lambda\mathsf{x}\mathsf{G}\ \\!\sim\ \\!\mathsf{M}$ from
($\alpha$). By using ($\ell$) and ($s$), we obtain
$\lambda\mathsf{x}[\lambda\mathsf{x}\mathsf{A}]\ \\!\sim\
\\!\lambda\mathsf{x}[\lambda\mathsf{x}\mathsf{G}]$ and
$\lambda\mathsf{x}[\lambda\mathsf{x}\mathsf{G}]\ \\!\sim\
\\!\lambda\mathsf{x}\mathsf{M}$. From ($r$), we have $\mathsf{D}\ \\!\sim\
\\!\mathsf{D}$ and so we get
$[\lambda\mathsf{x}[\lambda\mathsf{x}\mathsf{A}]]\mathsf{D}\ \\!\sim\
\\![\lambda\mathsf{x}[\lambda\mathsf{x}\mathsf{G}]]\mathsf{D}$ and
$[\lambda\mathsf{x}[\lambda\mathsf{x}\mathsf{G}]]\mathsf{D}\ \\!\sim\
\\![\lambda\mathsf{x}\mathsf{M}]\mathsf{D}$ by ($a$). By Lemma 7.9, we have
$\reflectbox{{B}}(\langle\mathsf{w}/\mathsf{x}\rangle(\mathsf{G}))=\reflectbox{{B}}(\mathsf{G})$.
Hence, it follows that
$\reflectbox{{B}}(\mathsf{M})=\reflectbox{{B}}(\langle\mathsf{w}/\mathsf{x}\rangle(\mathsf{G}))\setminus\\{\,\\!\mathsf{w}\,\\!\\}=\reflectbox{{B}}(\mathsf{G})\setminus\\{\,\\!\mathsf{w}\,\\!\\}$.
Since $\mathsf{w}\in\reflectbox{{F}}(\mathsf{D})$ and
$\reflectbox{{B}}(\mathsf{G})\cup\reflectbox{{F}}(\mathsf{D})=\mathbb{V}$, we
have
$\reflectbox{{B}}(\mathsf{M})\cup\reflectbox{{F}}(\mathsf{D})=\big{(}\reflectbox{{B}}(\mathsf{G})\setminus\\{\,\\!\mathsf{w}\,\\!\\}\big{)}\cup\reflectbox{{F}}(\mathsf{D})=\reflectbox{{B}}(\mathsf{G})\cup\reflectbox{{F}}(\mathsf{D})=\mathbb{V}$.
From this, we obtain $[\lambda\mathsf{x}\mathsf{M}]\mathsf{D}\ \\!\sim\
\\!\langle\mathsf{D}/\mathsf{x}\rangle(\mathsf{M})$ by ($\beta$). As
$\mathsf{x}\neq\mathsf{w}$, we have
$\langle\mathsf{D}/\mathsf{x}\rangle(\mathsf{M})=\langle\mathsf{D}/\mathsf{x}\rangle(\lambda\mathsf{w}\langle\mathsf{w}/\mathsf{x}\rangle(\mathsf{G}))=\lambda\mathsf{w}\langle\mathsf{D}/\mathsf{x}\rangle(\langle\mathsf{w}/\mathsf{x}\rangle(\mathsf{G}))$,
and we get
$\langle\mathsf{D}/\mathsf{x}\rangle(\langle\mathsf{w}/\mathsf{x}\rangle(\mathsf{G}))=\langle\mathsf{w}/\mathsf{x}\rangle(\mathsf{G})$
by Lemma 7.11. Hence, we obtain
$\langle\mathsf{D}/\mathsf{x}\rangle(\mathsf{M})=\lambda\mathsf{w}\langle\mathsf{w}/\mathsf{x}\rangle(\mathsf{G})=\mathsf{M}$
and $[\lambda\mathsf{x}\mathsf{M}]\mathsf{D}\ \\!\sim\ \\!\mathsf{M}$. Since
$\mathsf{G}\ \\!\sim\ \\!\mathsf{A}$, we obtain $\lambda\mathsf{x}\mathsf{G}\
\\!\sim\ \\!\lambda\mathsf{x}\mathsf{A}$ from ($\ell$) and by using ($s$) we
have $[\lambda\mathsf{x}[\lambda\mathsf{x}\mathsf{A}]]\mathsf{D}\ \\!\sim\
\\![\lambda\mathsf{x}[\lambda\mathsf{x}\mathsf{G}]]\mathsf{D}\ \\!\sim\
\\![\lambda\mathsf{x}\mathsf{M}]\mathsf{D}\ \\!\sim\ \\!\mathsf{M}\ \\!\sim\
\\!\lambda\mathsf{x}\mathsf{G}\ \\!\sim\ \\!\lambda\mathsf{x}\mathsf{A}$. From
($t$), we finally obtain
$[\lambda\mathsf{x}[\lambda\mathsf{x}\mathsf{A}]]\mathsf{D}\ \\!\sim\
\\!\lambda\mathsf{x}\mathsf{A}$.

($\beta_{5}$) Suppose that $\mathsf{x}\neq\mathsf{y}$ and
$[\lambda\mathsf{y}\mathsf{D}]\mathsf{x}\ \\!\sim\ \\!\mathsf{D}$. Let
$\mathsf{C}\stackrel{{\scriptstyle\text{\tiny{DEF}}}}{{=}}[\lambda\mathsf{y}\mathsf{D}]\mathsf{x}$.
By Proposition 7.10, there exists a term $\mathsf{G}$ such that $\mathsf{G}\
\\!\sim\ \\!\mathsf{A}$ and
$\reflectbox{{B}}(\mathsf{G})\cup\reflectbox{{F}}(\mathsf{C})=\mathbb{V}$.
Since
$\reflectbox{{B}}(\mathsf{G})\cup\reflectbox{{F}}(\mathsf{C})=\mathbb{V}$, we
have $[\lambda\mathsf{x}\mathsf{G}]\mathsf{C}\ \\!\sim\
\\!\langle\mathsf{C}/\mathsf{x}\rangle(\mathsf{G})$ by ($\beta$). As
$\mathsf{G}\ \\!\sim\ \\!\mathsf{A}$, we have $\lambda\mathsf{x}\mathsf{G}\
\\!\sim\ \\!\lambda\mathsf{x}\mathsf{A}$ by ($\ell$). From this and
$\mathsf{C}\ \\!\sim\ \\!\mathsf{D}$ we obtain
$[\lambda\mathsf{x}\mathsf{G}]\mathsf{C}\ \\!\sim\
\\![\lambda\mathsf{x}\mathsf{A}]\mathsf{D}$ by ($a$). By using ($s$), we have
$\langle\mathsf{C}/\mathsf{x}\rangle(\mathsf{G})\ \\!\sim\
\\![\lambda\mathsf{x}\mathsf{G}]\mathsf{C}\ \\!\sim\
\\![\lambda\mathsf{x}\mathsf{A}]\mathsf{D}$ and we obtain
$\langle\mathsf{C}/\mathsf{x}\rangle(\mathsf{G})\ \\!\sim\
\\![\lambda\mathsf{x}\mathsf{A}]\mathsf{D}$ from ($t$). Hence, we get
$\lambda\mathsf{y}\langle\mathsf{C}/\mathsf{x}\rangle(\mathsf{G})\ \\!\sim\
\\!\lambda\mathsf{y}[[\lambda\mathsf{x}\mathsf{A}]\mathsf{D}]$ by ($\ell$).
Now, since $\mathsf{G}\ \\!\sim\ \\!\mathsf{A}$, we have
$\lambda\mathsf{x}[\lambda\mathsf{y}\mathsf{G}]\ \\!\sim\
\\!\lambda\mathsf{x}[\lambda\mathsf{y}\mathsf{A}]$ by using ($\ell$). As
$\mathsf{C}\ \\!\sim\ \\!\mathsf{D}$, we get
$[\lambda\mathsf{x}[\lambda\mathsf{y}\mathsf{G}]]\mathsf{C}\ \\!\sim\
\\![\lambda\mathsf{x}[\lambda\mathsf{y}\mathsf{A}]]\mathsf{D}$ by ($a$). Since
$\mathsf{x}\neq\mathsf{y}$, we have
$\mathsf{y}\in\big{(}\reflectbox{{F}}(\mathsf{D})\cup\\{\,\\!\mathsf{y}\,\\!\\}\big{)}\cap\big{(}\mathbb{V}\setminus\\{\,\\!\mathsf{x}\,\\!\\}\big{)}=\reflectbox{{F}}(\lambda\mathsf{y}\mathsf{D})\cap\reflectbox{{F}}(\mathsf{x})=\reflectbox{{F}}([\lambda\mathsf{y}\mathsf{D}]\mathsf{x})=\reflectbox{{F}}(\mathsf{C})$.
From this and
$\reflectbox{{B}}(\mathsf{G})\cup\reflectbox{{F}}(\mathsf{C})=\mathbb{V}$ it
follows that
$\reflectbox{{B}}(\lambda\mathsf{y}\mathsf{G})\cup\reflectbox{{F}}(\mathsf{C})=\big{(}\reflectbox{{B}}(\mathsf{G})\setminus\\{\,\\!\mathsf{y}\,\\!\\}\big{)}\cup\reflectbox{{F}}(\mathsf{C})=\reflectbox{{B}}(\mathsf{G})\cup\reflectbox{{F}}(\mathsf{C})=\mathbb{V}$.
Hence, we obtain $[\lambda\mathsf{x}[\lambda\mathsf{y}\mathsf{G}]]\mathsf{C}\
\\!\sim\ \\!\langle\mathsf{C}/\mathsf{x}\rangle(\lambda\mathsf{y}\mathsf{G})$
by ($\beta$). Since $\mathsf{x}\neq\mathsf{y}$, we have
$\langle\mathsf{C}/\mathsf{x}\rangle(\lambda\mathsf{y}\mathsf{G})=\lambda\mathsf{y}\langle\mathsf{C}/\mathsf{x}\rangle(\mathsf{G})$.
Thus, we get $[\lambda\mathsf{x}[\lambda\mathsf{y}\mathsf{G}]]\mathsf{D}\
\\!\sim\ \\!\lambda\mathsf{y}\langle\mathsf{C}/\mathsf{x}\rangle(\mathsf{G})$.
By using ($s$) we obtain
$[\lambda\mathsf{x}[\lambda\mathsf{y}\mathsf{A}]]\mathsf{D}\ \\!\sim\
\\![\lambda\mathsf{x}[\lambda\mathsf{y}\mathsf{G}]]\mathsf{C}\ \\!\sim\
\\!\lambda\mathsf{y}\langle\mathsf{C}/\mathsf{x}\rangle(\mathsf{G})\ \\!\sim\
\\!\lambda\mathsf{y}[[\lambda\mathsf{x}\mathsf{A}]\mathsf{D}]$. Hence, we
conclude that $[\lambda\mathsf{x}[\lambda\mathsf{y}\mathsf{A}]]\mathsf{D}\
\\!\sim\ \\!\lambda\mathsf{y}[[\lambda\mathsf{x}\mathsf{A}]\mathsf{D}]$ from
($t$).

($e_{a}$) This condition holds by Proposition 7.8. ∎

######  Proposition 8.4.

Every extensional congruence is an extensional theory.

###### Proof.

Let $\ \\!\sim\ \\!$ be an extensional congruence. In order to prove that $\
\\!\sim\ \\!$ is an extensional theory we have to show that $\ \\!\sim\ \\!$
satisfies conditions ($\beta$), ($\alpha$) and ($\eta$). By Theorem 6.3 we
know that $\ \\!\sim\ \\!$ is a lambda congruence and so by Proposition 8.2 it
satisfies ($\beta$) and ($\alpha$). As for ($\eta$), it holds by Proposition
6.2(ii). ∎

######  Proposition 8.5.

Every extensional theory is an extensional congruence.

###### Proof.

Let $\ \\!\sim\ \\!$ be an extensional theory. In order to prove that $\
\\!\sim\ \\!$ is an extensional congruence we have to show that $\ \\!\sim\
\\!$ satisfies all beta conditions and ($\eta_{e}$). Since, by definition, $\
\\!\sim\ \\!$ is also a lambda theory, we know by Proposition 8.3 that $\
\\!\sim\ \\!$ satisfies all beta conditions. As for ($\eta_{e}$), suppose that
$\mathsf{x}\neq\mathsf{y}$. Then, as
$\mathsf{x}\in\mathbb{V}\setminus\\{\,\\!\mathsf{y}\,\\!\\}=\reflectbox{{F}}(\mathsf{y})$,
we obtain $\mathsf{y}\ \\!\sim\ \\!\lambda\mathsf{x}[\mathsf{y}\mathsf{x}]$ by
($\eta$). ∎

######  Theorem 8.6.

The concepts of lambda and extensional congruence are respectively equivalent
to the notions of lambda and extensional theory.

###### Proof.

By the previous four propositions. ∎

By using the above theorem, it is also possible to give simplified
formalizations of lambda conversion and extensional conversion as we now
explain.

Recall that lambda conversion is the lambda theory inductively defined by
using structural conditions, ($\beta$) and ($\alpha$). In other words, lambda
conversion is the intersection of all lambda theories. By Theorem 8.6, the set
of all lambda theories is equal to the set of all lambda congruences. Thus,
lambda conversion is also the intersection of all lambda congruences. In
particular, lambda conversion can be equivalently characterized as the
relation inductively defined by using all structural and beta conditions
together with ($\alpha_{e}$).

By replacing ($\alpha_{e}$) by ($\eta_{e}$) in the discussion above, a
simplified axiomatization of extensional conversion is similarly given.

##  9 The Prelambda Congruence $\,\\!\sim_{I}\,\\!$

The aim of this section is to show that there exists a prelambda congruence
$\,\\!\sim_{I}\,\\!$ such that for all distinct variables $\mathsf{x}$ and
$\mathsf{y}$ we have $\lambda\mathsf{x}\mathsf{x}\ \\!\not\,\\!\sim_{I}\
\\!\lambda\mathsf{y}\mathsf{y}$. In other words, we now prove Theorem 3.3
whose proof was omitted in Section 3.

This is not an easy task, though. The reason is that the defining conditions
of prelambda congruence only deal with “provability” while our aim is to show
the “unprovability” of
$\lambda\mathsf{x}\mathsf{x}\,\\!\sim_{I}\,\\!\lambda\mathsf{y}\mathsf{y}$,
that is $\lambda\mathsf{x}\mathsf{x}\ \\!\not\,\\!\sim_{I}\
\\!\lambda\mathsf{y}\mathsf{y}$.

A reassuring fact is that similar situations frequently happen in logic and in
that setting well–known methods to solve these kinds of problems are
available. Consider for instance _intuitionistic theories_ and the law of
excluded middle — for the purposes of this discussion an intuitionistic theory
is just a set of formulas which is closed under the rules of intuitionistic
logic. We say that an intuitionistic theory is _classical_ if it contain every
instance of excluded middle. Of course, there are several intuitionistic
theories which are classical: classical logic is the primary example.

Suppose that we want to show that there exists an intuitionistic theory which
is _not_ classical. In order to do this, it suffices to construct a model $M$
and prove that the set of formulas which are valid in $M$ forms a
non–classical intuitionistic theory. Note that $M$ cannot be a standard model
of classical logic — excluded middle never fails there — but it has to be a
model specifically designed to this aim, such as a topological model or a
Kripke model; see, e.g., Sørensen and Urzyczyn [47, Ch. 2].

Now, if we think of prelambda congruences as intuitionistic theories and
“$\lambda\mathsf{x}\mathsf{x}\ \\!\sim\ \\!\lambda\mathsf{y}\mathsf{y}$ for
all $\mathsf{x}$ and $\mathsf{y}$” as the law of excluded middle, then the
situation is strikingly similar to the one described above. Hence, in order to
solve our problem we now build a kind of model with the required properties.
Since all models considered in the literature of the lambda calculus have been
conceived for the purpose of _validating_ (not _refuting_)
“$\lambda\mathsf{x}\mathsf{x}\ \\!\sim\ \\!\lambda\mathsf{y}\mathsf{y}$ for
all $\mathsf{x}$ and $\mathsf{y}$”, our construction, to the best of our
knowledge, seems to be new.

We now introduce some notation. Let $A$ and $B$ be sets. We write
$B\subseteq_{f}A$ to express the fact that $B$ is a finite subset of $A$. We
also write $P(A)$ and $P_{f}(A)$ for the set of all subsets and finite subsets
of $A$, respectively. Furthermore, we write $A\times B$ to denote the
Cartesian product of $A$ and $B$.

In order to construct our model we now introduce the notion of _formula_.

######  Definition 9.1 (Formula).

Let $\mathfrak{F}$ be the set inductively defined as follows:

  * ($\mathfrak{F}_{1}$)

$\mathsf{x}\in\mathbb{V}$ implies $\mathsf{x}\in\mathfrak{F}$;

  * ($\mathfrak{F}_{2}$)

$F\subseteq_{f}\mathfrak{F}$ and $\ell\in\mathfrak{F}$ imply
$(F,\ell)\in\mathfrak{F}$.

We call formula any element of the set $\mathfrak{F}$. Henceforth, we use $F$,
$G$, $H$,…and $\ell$, $m$, $n$, …to denote finite subsets and elements of
$\mathfrak{F}$, respectively. We also use the expression $F\vdash\ell$ as an
alternative notation for the ordered pair $(F,\ell)$. In particular, we write
$G\vdash F\vdash\ell$ for $(G,(F,\ell))$.

Let $\ell$ be a formula. We say that $\ell$ is an atomic formula if
$\ell\in\mathbb{V}$ and that $\ell$ is a compound formula if
$\ell\notin\mathbb{V}$; equivalently, if it is of the form $F\vdash m$.
$\triangle$

We now observe that our set $\mathfrak{F}$ belongs to the class of structures
called _graph algebras_ , in the terminology of Engeler [23]. In particular,
$\mathfrak{F}$ corresponds to the full graph algebra $G(\mathbb{V})$ built on
the set of variables $\mathbb{V}$. For our aims the fact that $\mathfrak{F}$
is specifically constructed out of the set of variables $\mathbb{V}$ turns out
to be essential, as we make clear later. Graph algebras are also known as
Engeler models and PSE–algebras in the literature; see, e.g., Meyer [33],
Longo [31], Barendregt [5], Krivine [30], Plotkin [39], Berline [6, 7] and
Hindley and Seldin [26]. Regarding our terminology, we refer to elements
$\mathfrak{F}$ as formulas because a similar terminology is employed in [30]
for similar structures.

Our aim is to interpret terms using the structure we have just defined. In
order to do so, it is necessary to introduce the concepts of environment and
update first.

######  Definition 9.2 (Environment, update).

We call environment any function $\sigma$ from $\mathbb{V}$ to
$P_{f}(\mathfrak{F})$. In the sequel, we use $\sigma$, $\rho$, $\tau$, …to
denote environments. We also denote the set of all environments by
$\mathbb{E}$.

Let $\sigma$ be an environment. Let $\mathsf{x}\in\mathbb{V}$ and let
$F\subseteq_{f}\mathfrak{F}$. We denote by
$\\{\,\\!F/\mathsf{x}\,\\!\\}\sigma$ the environment given by:

$\\{\,\\!F/\mathsf{x}\,\\!\\}\sigma(\mathsf{y})\,\stackrel{{\scriptstyle\text{\tiny{DEF}}}}{{=}}\,$
$\left\\{\begin{array}[]{cl}F&\hbox{if $\mathsf{x}=\mathsf{y}$}\\\
\sigma(\mathsf{y})&\hbox{if $\mathsf{x}\neq\mathsf{y}$\enspace, \quad for
$\mathsf{y}\in\mathbb{V}$\enspace.}\\\ \end{array}\right.$

We call $\\{\,\\!F/\mathsf{x}\,\\!\\}\sigma$ an update of $\sigma$.

Let $\mathsf{x}$ and $\mathsf{y}$ be variables, and let $F$ and $G$ in
$P_{f}(\mathfrak{F})$. Let $\sigma$ be an environment. If
$\rho=\\{\,\\!F/\mathsf{x}\,\\!\\}\sigma$ and
$\tau=\\{\,\\!G/\mathsf{y}\,\\!\\}\rho$, then we also write $\tau$ as
$\\{\,\\!G/\mathsf{y}\,\\!\\}\\{\,\\!F/\mathsf{x}\,\\!\\}\sigma$. $\triangle$

Updates obey the algebraic laws that we show in the next lemma.

######  Lemma 9.3.

Let $\sigma$ be an environment. Let $\mathsf{x}$ and $\mathsf{y}$ be variables
such that $\mathsf{x}\neq\mathsf{y}$, and let $F$ and $G$ be finite subsets of
$\mathfrak{F}$. Then, the following properties hold:

  * _(i)_

$\\{\,\\!G/\mathsf{x}\,\\!\\}\\{\,\\!F/\mathsf{x}\,\\!\\}\sigma=\\{\,\\!G/\mathsf{x}\,\\!\\}\sigma$;

  * _(ii)_

$\\{\,\\!G/\mathsf{y}\,\\!\\}\\{\,\\!F/\mathsf{x}\,\\!\\}\sigma=\\{\,\\!F/\mathsf{x}\,\\!\\}\\{\,\\!G/\mathsf{y}\,\\!\\}\sigma$.

###### Proof.

(i) We have
$\\{\,\\!G/\mathsf{x}\,\\!\\}\\{\,\\!F/\mathsf{x}\,\\!\\}\sigma(\mathsf{x})=G=\\{\,\\!G/\mathsf{x}\,\\!\\}\sigma(\mathsf{x})$.
Let $\mathsf{z}$ be a variable such that $\mathsf{x}\neq\mathsf{z}$. Then, we
have
$\\{\,\\!G/\mathsf{x}\,\\!\\}\\{\,\\!F/\mathsf{x}\,\\!\\}\sigma(\mathsf{z})=\\{\,\\!F/\mathsf{x}\,\\!\\}\sigma(\mathsf{z})=\sigma(\mathsf{z})=\\{\,\\!G/\mathsf{x}\,\\!\\}\sigma(\mathsf{z})$.

(ii) Since $\mathsf{x}\neq\mathsf{y}$, we have
$\\{\,\\!G/\mathsf{y}\,\\!\\}\\{\,\\!F/\mathsf{x}\,\\!\\}\sigma(\mathsf{x})=\\{\,\\!F/\mathsf{x}\,\\!\\}\sigma(\mathsf{x})=$
$F=\\{\,\\!F/\mathsf{x}\,\\!\\}\\{\,\\!G/\mathsf{y}\,\\!\\}\sigma(\mathsf{x})$
and
$\\{\,\\!G/\mathsf{y}\,\\!\\}\\{\,\\!F/\mathsf{x}\,\\!\\}\sigma(\mathsf{y})=G=\\{\,\\!G/\mathsf{y}\,\\!\\}\sigma(\mathsf{y})=\\{\,\\!F/\mathsf{x}\,\\!\\}\\{\,\\!G/\mathsf{y}\,\\!\\}\sigma(\mathsf{y})$.
Let $\mathsf{z}$ be a variable such that $\mathsf{x}\neq\mathsf{z}$ and
$\mathsf{y}\neq\mathsf{z}$. Then, we have
$\\{\,\\!G/\mathsf{y}\,\\!\\}\\{\,\\!F/\mathsf{x}\,\\!\\}\sigma(\mathsf{z})=\\{\,\\!F/\mathsf{x}\,\\!\\}\sigma(\mathsf{z})=\sigma(\mathsf{z})=\\{\,\\!G/\mathsf{y}\,\\!\\}\sigma(\mathsf{z})=\\{\,\\!F/\mathsf{x}\,\\!\\}\\{\,\\!G/\mathsf{y}\,\\!\\}\sigma(\mathsf{z})$.
∎

We now define our interpretation of terms. As is standard for graph algebras,
each term is interpreted via an environment as a subset of formulas.

######  Definition 9.4 (Interpretation of terms in $P(\mathfrak{F})$).

We define the function $I$ from $\mathbb{T}\times\mathbb{E}$ to
$P(\mathfrak{F})$ by induction on the structure of terms as follows:

  * ($I_{1}$)

$I(\mathsf{x},\sigma)\stackrel{{\scriptstyle\text{\tiny{DEF}}}}{{=}}\sigma(\mathsf{x})$;

  * ($I_{2}$)

$I(\mathsf{A}\mathsf{B},\sigma)\stackrel{{\scriptstyle\text{\tiny{DEF}}}}{{=}}\\{\,\\!\ell\
\,|\ \,$ there exists $F\subseteq_{f}I(\mathsf{B},\sigma)$ such that
$\phantom{asaasasaasaasas}F\vdash\ell\in I(\mathsf{A},\sigma)\,\\!\\}$;

  * ($I_{3}$)

$I(\lambda\mathsf{x}\mathsf{A},\sigma)\stackrel{{\scriptstyle\text{\tiny{DEF}}}}{{=}}\\{\,\\!F\vdash
m\ \,|\ \,m\in
I(\mathsf{A},\\{\,\\!F/\mathsf{x}\,\\!\\}\sigma)\,\\!\\}\,\cup\,\\{\,\\!\mathsf{x}\,\\!\\}$.

Let $\mathsf{A}$ and $\mathsf{B}$ be terms. We write
$\mathsf{A}\,\\!\sim_{I}\,\\!\mathsf{B}$ and say that $\mathsf{A}$ and
$\mathsf{B}$ have the same interpretation in $P(\mathfrak{F})$ if
$I(\mathsf{A},\sigma)=I(\mathsf{B},\sigma)$ for every environment $\sigma$. We
also call the relation $\,\\!\sim_{I}\,\\!$ the theory of $P(\mathfrak{F})$.
$\triangle$

While our _set_ $\mathfrak{F}$ is just an example of graph algebra, our
_interpretation_ of terms in $P(\mathfrak{F})$ is definitely non–standard, as
we now explain.

Firstly, environments are usually taken as function from $\mathbb{V}$ to
$P(\mathfrak{F})$ and not as functions from $\mathbb{V}$ to
$P_{f}(\mathfrak{F})$ as we do in this paper. The reason is practical: to show
our results we found it is not necessary consider environments having infinite
sets of formulas in their range.

Secondly, following the standard interpretation of terms in graph algebras
$I(\lambda\mathsf{x}\mathsf{A},\sigma)$ should be the set of formulas
$\\{\,\\!F\vdash m\ \,|\ \,m\in
I(\mathsf{A},\\{\,\\!F/\mathsf{x}\,\\!\\}\sigma)\,\\!\\}$ and _not_ our set
$\\{\,\\!F\vdash m\ \,|\ \,m\in
I(\mathsf{A},\\{\,\\!F/\mathsf{x}\,\\!\\}\sigma)\,\\!\\}\,\cup\,\\{\,\\!\mathsf{x}\,\\!\\}$.
As a consequence of this fact, in our setting each set of the form
$I(\lambda\mathsf{x}\mathsf{A},\sigma)$ contains compound formulas of the form
$F\vdash m$ and _exactly one_ atomic formula, namely $\mathsf{x}$. This
formula $\mathsf{x}$ gives us a “tag” for the “$\lambda\mathsf{x}$” in the
interpretation of $\lambda\mathsf{x}\mathsf{A}$ and the presence of this
unique atomic formula turns out to be crucial for our purposes. For this
reason, the fact that variables are also formulas is very important in our
setting.

We now show two lemmas that we need during the proof of Theorem 9.7.

######  Lemma 9.5.

Let $\mathsf{x}$ be a variable and let $\mathsf{A}$ be a term. Let $F$ and $G$
finite subsets of of formulas such that $F\subseteq G$. Then, for every
environment $\sigma$ we have
$I(\mathsf{A},\\{\,\\!F/\mathsf{x}\,\\!\\}\sigma)\subseteq
I(\mathsf{A},\\{\,\\!G/\mathsf{x}\,\\!\\}\sigma)$.

###### Proof.

We reason by induction on the structure of $\mathsf{A}$. Let $\sigma$ be an
environment and let $\ell$ be a formula.

Suppose that $\mathsf{A}=\mathsf{y}$. If $\mathsf{x}=\mathsf{y}$, then we have
$I(\mathsf{x},\\{\,\\!F/\mathsf{x}\,\\!\\}\sigma)=\\{\,\\!F/\mathsf{x}\,\\!\\}\sigma(\mathsf{x})=F\subseteq
G=\\{\,\\!G/\mathsf{x}\,\\!\\}\sigma(\mathsf{x})=I(\mathsf{x},\\{\,\\!G/\mathsf{x}\,\\!\\}\sigma)$.
If $\mathsf{x}\neq\mathsf{y}$, then we have
$I(\mathsf{y},\\{\,\\!F/\mathsf{x}\,\\!\\}\sigma)=\\{\,\\!F/\mathsf{x}\,\\!\\}\sigma(\mathsf{y})=\sigma(\mathsf{y})=\\{\,\\!G/\mathsf{x}\,\\!\\}\sigma(\mathsf{y})=I(\mathsf{y},\\{\,\\!G/\mathsf{x}\,\\!\\}\sigma)$.

Suppose that $\mathsf{A}=\mathsf{B}\mathsf{C}$. By inductive hypothesis, for
every environment $\rho$ and every
$\mathsf{D}\in\\{\,\\!\mathsf{B},\mathsf{C}\,\\!\\}$ we have
$I(\mathsf{D},\\{\,\\!F/\mathsf{x}\,\\!\\}\rho)\subseteq
I(\mathsf{D},\\{\,\\!G/\mathsf{x}\,\\!\\}\rho)$. Assume $\ell\in
I(\mathsf{B}\mathsf{C},\\{\,\\!F/\mathsf{x}\,\\!\\}\sigma)$. Then, there
exists $H\subseteq_{f}I(\mathsf{C},\\{\,\\!F/\mathsf{x}\,\\!\\}\sigma)$ such
that $H\vdash\ell\in I(\mathsf{B},\\{\,\\!F/\mathsf{x}\,\\!\\}\sigma)$. By
inductive hypothesis, it follows that
$H\subseteq_{f}I(\mathsf{C},\\{\,\\!G/\mathsf{x}\,\\!\\}\sigma)$ and
$H\vdash\ell\in I(\mathsf{B},\\{\,\\!G/\mathsf{x}\,\\!\\}\sigma)$. From this,
we conclude that $\ell\in
I(\mathsf{B}\mathsf{C},\\{\,\\!G/\mathsf{x}\,\\!\\}\sigma)$.

Suppose that $\mathsf{A}=\lambda\mathsf{y}\mathsf{B}$. Assume $\ell\in
I(\lambda\mathsf{y}\mathsf{B},\\{\,\\!F/\mathsf{x}\,\\!\\}\sigma)$. Suppose
that $\mathsf{x}=\mathsf{y}$. If $\ell=\mathsf{x}$, then we obviously have
$\mathsf{x}\in
I(\lambda\mathsf{x}\mathsf{B},\\{\,\\!G/\mathsf{x}\,\\!\\}\sigma)$. Otherwise,
it follows that $\ell=H\vdash m$ for some $H$ and $m$ such that $m\in
I(\mathsf{B},\\{\,\\!H/\mathsf{x}\,\\!\\}\\{\,\\!F/\mathsf{x}\,\\!\\}\sigma)$.
By using Lemma 9.3(i) it follows that $m\in
I(\mathsf{B},\\{\,\\!H/\mathsf{x}\,\\!\\}\\{\,\\!G/\mathsf{x}\,\\!\\}\sigma)$
and we obtain $H\vdash m\in
I(\lambda\mathsf{x}\mathsf{B},\\{\,\\!G/\mathsf{x}\,\\!\\}\sigma)$. Suppose
now that $\mathsf{x}\neq\mathsf{y}$. If $\ell=\mathsf{y}$, then we clearly
have $\mathsf{y}\in
I(\lambda\mathsf{y}\mathsf{B},\\{\,\\!G/\mathsf{x}\,\\!\\}\sigma)$. Otherwise,
it follows that $\ell=H\vdash m$ for some $H$ and $m$ such that $m\in
I(\mathsf{B},\\{\,\\!H/\mathsf{y}\,\\!\\}\\{\,\\!F/\mathsf{x}\,\\!\\}\sigma)$.
By inductive hypothesis, for every environment $\rho$ we have
$I(\mathsf{B},\\{\,\\!F/\mathsf{x}\,\\!\\}\rho)\subseteq
I(\mathsf{B},\\{\,\\!G/\mathsf{x}\,\\!\\}\rho)$. From this and Lemma 9.3(ii)
we obtain $m\in
I(\mathsf{B},\\{\,\\!H/\mathsf{y}\,\\!\\}\\{\,\\!F/\mathsf{x}\,\\!\\}\sigma)=I(\mathsf{B},\\{\,\\!F/\mathsf{x}\,\\!\\}\\{\,\\!H/\mathsf{y}\,\\!\\}\sigma)\subseteq
I(\mathsf{B},\\{\,\\!G/\mathsf{x}\,\\!\\}\\{\,\\!H/\mathsf{y}\,\\!\\}\sigma)=I(\mathsf{B},\\{\,\\!H/\mathsf{y}\,\\!\\}\\{\,\\!G/\mathsf{x}\,\\!\\}\sigma)$,
as $\mathsf{x}\neq\mathsf{y}$. Therefore, we get $H\vdash m\in
I(\lambda\mathsf{y}\mathsf{B},\\{\,\\!G/\mathsf{x}\,\\!\\}\sigma)$. ∎

######  Lemma 9.6.

Let $\mathsf{x}$ and $\mathsf{z}$ be variables such that
$\mathsf{x}\neq\mathsf{z}$, and let $\mathsf{A}$ be a term. Let $F$ be a
finite subset of formulas. Suppose that
$[\lambda\mathsf{x}\mathsf{A}]\mathsf{z}\,\\!\sim_{I}\,\\!\mathsf{A}$. Then,
we have
$I(\mathsf{A},\sigma)=I(\mathsf{A},\\{\,\\!F/\mathsf{x}\,\\!\\}\sigma)$ for
every environment $\sigma$.

###### Proof.

Let $\sigma$ be an environment and let $\ell$ be a formula. As
$[\lambda\mathsf{x}\mathsf{A}]\mathsf{z}\,\\!\sim_{I}\,\\!\mathsf{A}$, we have
$I([\lambda\mathsf{x}\mathsf{A}]\mathsf{z},\sigma)=I(\mathsf{A},\sigma)$ and
$I([\lambda\mathsf{x}\mathsf{A}]\mathsf{z},\\{\,\\!F/\mathsf{x}\,\\!\\}\sigma)=I(\mathsf{A},\\{\,\\!F/\mathsf{x}\,\\!\\}\sigma)$.

Assume $\ell\in
I(\mathsf{A},\sigma)=I([\lambda\mathsf{x}\mathsf{A}]\mathsf{z},\sigma)$. Then,
there exists $G\subseteq_{f}I(\mathsf{z},\sigma)$ such that $G\vdash\ell\in
I(\lambda\mathsf{x}\mathsf{A},\sigma)$ and $\ell\in
I(\mathsf{A},\\{\,\\!G/\mathsf{x}\,\\!\\}\sigma)$. Since
$\mathsf{x}\neq\mathsf{z}$, it follows that
$G\subseteq_{f}I(\mathsf{z},\sigma)=\sigma(\mathsf{z})=\\{\,\\!F/\mathsf{x}\,\\!\\}\sigma(\mathsf{z})=I(\mathsf{z},\\{\,\\!F/\mathsf{x}\,\\!\\}\sigma)$.
By using Lemma 9.3(i), it follows that $\ell\in
I(\mathsf{A},\\{\,\\!G/\mathsf{x}\,\\!\\}\\{\,\\!F/\mathsf{x}\,\\!\\}\sigma)$
and hence $G\vdash\ell\in
I(\lambda\mathsf{x}\mathsf{A},\\{\,\\!F/\mathsf{x}\,\\!\\}\sigma)$. Since
$G\subseteq_{f}I(\mathsf{z},\\{\,\\!F/\mathsf{x}\,\\!\\}\sigma)$, we obtain
$\ell\in
I([\lambda\mathsf{x}\mathsf{A}]\mathsf{z},\\{\,\\!F/\mathsf{x}\,\\!\\}\sigma)=I(\mathsf{A},\\{\,\\!F/\mathsf{x}\,\\!\\}\sigma)$.
This shows that $I(\mathsf{A},\sigma)\subseteq
I(\mathsf{A},\\{\,\\!F/\mathsf{x}\,\\!\\}\sigma)$. To show the opposite
inclusion, assume $\ell\in
I(\mathsf{A},\\{\,\\!F/\mathsf{x}\,\\!\\}\sigma)=I([\lambda\mathsf{x}\mathsf{A}]\mathsf{z},\sigma\\{\,\\!F/\mathsf{x}\,\\!\\})$.
Then, there exists some
$G\subseteq_{f}I(\mathsf{z},\sigma\\{\,\\!F/\mathsf{x}\,\\!\\})$ such that
$G\vdash\ell\in
I(\lambda\mathsf{x}\mathsf{A},\\{\,\\!F/\mathsf{x}\,\\!\\}\sigma)$ and
$\ell\in
I(\mathsf{A},\\{\,\\!G/\mathsf{x}\,\\!\\}\\{\,\\!F/\mathsf{x}\,\\!\\}\sigma)$.
By using Lemma 9.3(i), we get $\ell\in
I(\mathsf{A},\\{\,\\!G/\mathsf{x}\,\\!\\}\sigma)$. So, we have $G\vdash\ell\in
I(\lambda\mathsf{x}\mathsf{A},\sigma)$. As $\mathsf{x}\neq\mathsf{z}$, we get
$G\subseteq_{f}I(\mathsf{z},\\{\,\\!F/\mathsf{x}\,\\!\\}\sigma)=\\{\,\\!F/\mathsf{x}\,\\!\\}\sigma(\mathsf{z})=\sigma(\mathsf{z})=I(\mathsf{z},\sigma)$
and we obtain $\ell\in
I([\lambda\mathsf{x}\mathsf{A}]\mathsf{z},\sigma)=I(\mathsf{A},\sigma)$.
Therefore, we have $I(\mathsf{A},\\{\,\\!F/\mathsf{x}\,\\!\\}\sigma)\subseteq
I(\mathsf{A},\sigma)$. ∎

We can now prove the theory of our model is a prelambda congruence.

######  Theorem 9.7.

The relation $\,\\!\sim_{I}\,\\!$ is a prelambda congruence.

###### Proof.

All we have to do is to check that $\,\\!\sim_{I}\,\\!$ satisfies all
structural and beta conditions. Let $\sigma$ be an environment and let $\ell$
be a formula.

As for ($r$), ($s$) and ($t$), let $\rho$ be and environment. Since
$I(\mathsf{D},\rho)$ is a set for each term $\mathsf{D}$, the following
conditions hold: $I(\mathsf{A},\rho)=I(\mathsf{A},\rho)$,
$I(\mathsf{A},\rho)=I(\mathsf{B},\rho)$ implies
$I(\mathsf{B},\rho)=I(\mathsf{A},\rho)$,
$I(\mathsf{A},\rho)=I(\mathsf{B},\rho)$ and
$I(\mathsf{B},\rho)=I(\mathsf{C},\rho)$ imply
$I(\mathsf{A},\rho)=I(\mathsf{C},\rho)$. From this observation, the fact that
$\,\\!\sim_{I}\,\\!$ satisfies ($r$), ($s$) and ($t$) follows.

($\ell$) Suppose that $I(\mathsf{A},\rho)=I(\mathsf{B},\rho)$ for every
environment $\rho$. We have to show that
$I(\lambda\mathsf{x}\mathsf{A},\sigma)=I(\lambda\mathsf{x}\mathsf{B},\sigma)$.
For $\mathsf{M}\in\\{\,\\!\mathsf{A},\mathsf{B}\,\\!\\}$, let

$\mathsf{N}\,\stackrel{{\scriptstyle\text{\tiny{DEF}}}}{{=}}\,$
$\left\\{\begin{array}[]{cl}\mathsf{B}&\hbox{if $\mathsf{M}=\mathsf{A}$}\\\
\mathsf{A}&\hbox{if $\mathsf{M}=\mathsf{B}$\enspace.}\\\ \end{array}\right.$

Suppose that $\ell\in I(\lambda\mathsf{x}\mathsf{M},\sigma)$. If
$\ell=\mathsf{x}$, then we clearly have $\mathsf{x}\in
I(\lambda\mathsf{x}\mathsf{N},\sigma)$. Otherwise, it follows that
$\ell=F\vdash m$ for some $F$ and $m$ such that and $m\in
I(\mathsf{M},\\{\,\\!F/\mathsf{x}\,\\!\\}\sigma)$. Since
$I(\mathsf{A},\\{\,\\!F/\mathsf{x}\,\\!\\}\sigma)=I(\mathsf{B},\\{\,\\!F/\mathsf{x}\,\\!\\}\sigma)$,
we have
$I(\mathsf{M},\\{\,\\!F/\mathsf{x}\,\\!\\}\sigma)=I(\mathsf{N},\\{\,\\!F/\mathsf{x}\,\\!\\}\sigma)$
and hence $m\in I(\mathsf{N},\\{\,\\!F/\mathsf{x}\,\\!\\}\sigma)$. From this,
we conclude that $F\vdash m\in I(\lambda\mathsf{x}\mathsf{N},\sigma)$. This
shows that
$I(\lambda\mathsf{x}\mathsf{A},\sigma)=I(\lambda\mathsf{x}\mathsf{B},\sigma)$.

($a$) Suppose that $I(\mathsf{A},\rho)=I(\mathsf{B},\rho)$ for every
environment $\rho$ and $I(\mathsf{C},\tau)=I(\mathsf{D},\tau)$ for every
environment $\tau$. We have to show that
$I(\mathsf{A}\mathsf{C},\sigma)=I(\mathsf{B}\mathsf{D},\sigma)$. For
$\mathsf{M}\mathsf{M}^{\prime}\in\\{\,\\!\mathsf{A}\mathsf{C},\mathsf{B}\mathsf{D}\,\\!\\}$,
let

$\mathsf{N}\mathsf{N}^{\prime}\,\stackrel{{\scriptstyle\text{\tiny{DEF}}}}{{=}}\,$
$\left\\{\begin{array}[]{cl}\mathsf{B}\mathsf{D}&\hbox{if
$\mathsf{M}\mathsf{M}^{\prime}=\mathsf{A}\mathsf{C}$}\\\
\mathsf{A}\mathsf{C}&\hbox{if
$\mathsf{M}\mathsf{M}^{\prime}=\mathsf{B}\mathsf{D}$\enspace.}\\\
\end{array}\right.$

Suppose that $\ell\in I(\mathsf{M}\mathsf{M}^{\prime},\sigma)$. Then, there
exists $F\subseteq_{f}I(\mathsf{M}^{\prime},\sigma)$ such that $F\vdash\ell\in
I(\mathsf{M},\sigma)$. Since $I(\mathsf{A},\sigma)=I(\mathsf{B},\sigma)$ and
$I(\mathsf{C},\sigma)=I(\mathsf{D},\sigma)$, it follows that
$I(\mathsf{M},\sigma)=I(\mathsf{N},\sigma)$ and
$I(\mathsf{M}^{\prime},\sigma)=I(\mathsf{N}^{\prime},\sigma)$. Thus, we have
$F\subseteq_{f}I(\mathsf{N}^{\prime},\sigma)$ and $F\vdash\ell\in
I(\mathsf{N},\sigma)$. So, it follows that $\ell\in
I(\mathsf{N}\mathsf{N}^{\prime},\sigma)$. This proves that
$I(\mathsf{A}\mathsf{C},\sigma)=I(\mathsf{B}\mathsf{D},\sigma)$.

($\beta_{1}$) We have to show that
$I([\lambda\mathsf{x}\mathsf{x}]\mathsf{D},\sigma)=I(\mathsf{D},\sigma)$.
Suppose that $\ell\in I([\lambda\mathsf{x}\mathsf{x}]\mathsf{D},\sigma)$.
Then, there exists $F\subseteq_{f}I(\mathsf{D},\sigma)$ such that
$F\vdash\ell\in I(\lambda\mathsf{x}\mathsf{x},\sigma)$. Since we have $\ell\in
I(\mathsf{x},\\{\,\\!F/\mathsf{x}\,\\!\\}\sigma)=\\{\,\\!F/\mathsf{x}\,\\!\\}\sigma(\mathsf{x})=F$,
we conclude that $\ell\in F\subseteq_{f}I(\mathsf{D},\sigma)$. To show the
opposite inclusion, suppose now that $\ell\in I(\mathsf{D},\sigma)$. Let
$F\stackrel{{\scriptstyle\text{\tiny{DEF}}}}{{=}}\\{\,\\!\ell\,\\!\\}$. Since
$\ell\in
F=\\{\,\\!F/\mathsf{x}\,\\!\\}\sigma(\mathsf{x})=I(\mathsf{x},\\{\,\\!F/\mathsf{x}\,\\!\\}\sigma)$,
we have $F\vdash\ell\in I(\lambda\mathsf{x}\mathsf{x},\sigma)$. As
$F=\\{\,\\!\ell\,\\!\\}$, it follows that
$F\subseteq_{f}I(\mathsf{D},\sigma)$. Thus, we obtain $\ell\in
I([\lambda\mathsf{x}\mathsf{x}]\mathsf{D},\sigma)$.

($\beta_{2}$) Suppose that $\mathsf{x}\neq\mathsf{y}$. We have to show that
$I([\lambda\mathsf{x}\mathsf{y}]\mathsf{D},\sigma)=I(\mathsf{y},\sigma)$.
Assume $\ell\in I([\lambda\mathsf{x}\mathsf{y}]\mathsf{D},\sigma)$. Then,
there exists $F\subseteq_{f}I(\mathsf{D},\sigma)$ such that $F\vdash\ell\in
I(\lambda\mathsf{x}\mathsf{y},\sigma)$. Since $\mathsf{x}\neq\mathsf{y}$, we
have $\ell\in
I(\mathsf{y},\\{\,\\!F/\mathsf{x}\,\\!\\}\sigma)=\\{\,\\!F/\mathsf{x}\,\\!\\}\sigma(\mathsf{y})=\sigma(\mathsf{y})=I(\mathsf{y},\sigma)$.
As for the opposite inclusion, assume now $\ell\in I(\mathsf{y},\sigma)$.
Since $\mathsf{x}\neq\mathsf{y}$, we have
$I(\mathsf{y},\sigma)=\sigma(\mathsf{y})=\\{\,\\!\emptyset/\mathsf{x}\,\\!\\}\sigma(\mathsf{y})=I(\mathsf{y},\\{\,\\!\emptyset/\mathsf{x}\,\\!\\}\sigma)$.
Thus, we have $\ell\in
I(\mathsf{y},\\{\,\\!\emptyset/\mathsf{x}\,\\!\\}\sigma)$ and
$\emptyset\vdash\ell\in I(\lambda\mathsf{x}\mathsf{y},\sigma)$. As
$\emptyset\subseteq_{f}I(\mathsf{D},\sigma)$, we get $\ell\in
I([\lambda\mathsf{x}\mathsf{y}]\mathsf{D},\sigma)$.

($\beta_{3}$) We have to show that
$I([\lambda\mathsf{x}[\mathsf{A}\mathsf{B}]]\mathsf{D},\sigma)=I([[\lambda\mathsf{x}\mathsf{A}]\mathsf{D}][[\lambda\mathsf{x}\mathsf{B}]\mathsf{D}],\sigma)$.
Suppose that $\ell\in
I([\lambda\mathsf{x}[\mathsf{A}\mathsf{B}]]\mathsf{D},\sigma)$. Then, there
exists $F\subseteq_{f}I(\mathsf{D},\sigma)$ such that $F\vdash\ell\in
I(\lambda\mathsf{x}[\mathsf{A}\mathsf{B}],\sigma)$. From this, we obtain
$\ell\in I(\mathsf{A}\mathsf{B},\\{\,\\!F/\mathsf{x}\,\\!\\}\sigma)$. Thus,
there exists $G\subseteq_{f}I(\mathsf{B},\\{\,\\!F/\mathsf{x}\,\\!\\}\sigma)$
such that $G\vdash\ell\in I(\mathsf{A},\\{\,\\!F/\mathsf{x}\,\\!\\}\sigma)$.
Hence, we have $F\vdash G\vdash\ell\in I(\lambda\mathsf{x}\mathsf{A},\sigma)$.
Since $F\subseteq_{f}I(\mathsf{D},\sigma)$, we obtain $G\vdash\ell\in
I([\lambda\mathsf{x}\mathsf{A}]\mathsf{D},\sigma)$. Let $n\in G$. Since $n\in
I(\mathsf{B},\\{\,\\!F/\mathsf{x}\,\\!\\}\sigma)$, it follows that $F\vdash
n\in I(\lambda\mathsf{x}\mathsf{B},\sigma)$. Since
$F\subseteq_{f}I(\mathsf{D},\sigma)$, we have $n\in
I([\lambda\mathsf{x}\mathsf{B}]\mathsf{D},\sigma)$. Thus, we have
$G\subseteq_{f}I([\lambda\mathsf{x}\mathsf{B}]\mathsf{D},\sigma)$. Now, as
$G\vdash\ell\in I([\lambda\mathsf{x}\mathsf{A}]\mathsf{D},\sigma)$, we obtain
$\ell\in
I([[\lambda\mathsf{x}\mathsf{A}]\mathsf{D}][[\lambda\mathsf{x}\mathsf{B}]\mathsf{D}],\sigma)$.
To show the opposite inclusion, suppose now that $\ell\in
I([[\lambda\mathsf{x}\mathsf{A}]\mathsf{D}][[\lambda\mathsf{x}\mathsf{B}]\mathsf{D}],\sigma)$.
Then, there exists
$F\subseteq_{f}I([\lambda\mathsf{x}\mathsf{B}]\mathsf{D},\sigma)$ such that
$F\vdash\ell\in I([\lambda\mathsf{x}\mathsf{A}]\mathsf{D},\sigma)$. Let $m\in
F$. Since $m\in I([\lambda\mathsf{x}\mathsf{B}]\mathsf{D},\sigma)$, there
exists $G_{m}\subseteq_{f}I(\mathsf{D},\sigma)$ such that $G_{m}\vdash m\in
I(\lambda\mathsf{x}\mathsf{B},\sigma)$. From this, we obtain $m\in
I(\mathsf{B},\\{\,\\!G_{m}/\mathsf{x}\,\\!\\}\sigma)$. Now, as $F\vdash\ell\in
I([\lambda\mathsf{x}\mathsf{A}]\mathsf{D},\sigma)$, there exists
$H\subseteq_{f}I(\mathsf{D},\sigma)$ such that $H\vdash F\vdash\ell\in
I(\lambda\mathsf{x}\mathsf{A},\sigma)$. From this, we obtain $F\vdash\ell\in
I(\mathsf{A},\\{\,\\!H/\mathsf{x}\,\\!\\}\sigma)$. Let

$L\stackrel{{\scriptstyle\text{\tiny{DEF}}}}{{=}}\\{\,\\!n\ \,|\ \,n\in G_{m}$
for some $m\in F\,\\!\\}\cup H$

and note that it is a finite set of formulas. Let $m\in F$. Since
$G_{m}\subseteq L$ we obtain $m\in
I(\mathsf{B},\\{\,\\!G_{m}/\mathsf{x}\,\\!\\}\sigma)\subseteq
I(\mathsf{B},\\{\,\\!L/\mathsf{x}\,\\!\\}\sigma)$ by Lemma 9.5 and therefore
$F\subseteq_{f}I(\mathsf{B},\\{\,\\!L/\mathsf{x}\,\\!\\}\sigma)$. As
$H\subseteq L$, it follows from Lemma 9.5 that $F\vdash\ell\in
I(\mathsf{A},\\{\,\\!H/\mathsf{x}\,\\!\\}\sigma)\subseteq
I(\mathsf{A},\\{\,\\!L/\mathsf{x}\,\\!\\}\sigma)$. So, we obtain $\ell\in
I(\mathsf{A}\mathsf{B},\\{\,\\!L/\mathsf{x}\,\\!\\}\sigma)$ and
$L\vdash\ell\in I(\lambda\mathsf{x}[\mathsf{A}\mathsf{B}],\sigma)$. Since
$G_{m}\subseteq_{f}I(\mathsf{D},\sigma)$ for every $m$ and
$H\subseteq_{f}I(\mathsf{D},\sigma)$, it follows that
$L\subseteq_{f}I(\mathsf{D},\sigma)$. As $L\vdash\ell\in
I(\lambda\mathsf{x}[\mathsf{A}\mathsf{B}],\sigma)$, we finally obtain $\ell\in
I([\lambda\mathsf{x}[\mathsf{A}\mathsf{B}]]\mathsf{D},\sigma)$.

($\beta_{4}$) We have to show that
$I([\lambda\mathsf{x}[\lambda\mathsf{x}\mathsf{A}]]\mathsf{D},\sigma)=I(\lambda\mathsf{x}\mathsf{A},\sigma)$.
Suppose that $\ell\in
I([\lambda\mathsf{x}[\lambda\mathsf{x}\mathsf{A}]]\mathsf{D},\sigma)$. Then,
there exists $F\subseteq_{f}I(\mathsf{D},\sigma)$ such that $F\vdash\ell\in
I(\lambda\mathsf{x}[\lambda\mathsf{x}\mathsf{A}],\sigma)$. We also have
$\ell\in I(\lambda\mathsf{x}\mathsf{A},\\{\,\\!F/\mathsf{x}\,\\!\\}\sigma)$.
If $\ell=\mathsf{x}$, then we clearly have $\mathsf{x}\in
I(\lambda\mathsf{x}\mathsf{A},\sigma)$. Otherwise, it follows that
$\ell=G\vdash m$ for some $G$ and $m$ such that $m\in
I(\mathsf{A},\\{\,\\!G/\mathsf{x}\,\\!\\}\\{\,\\!F/\mathsf{x}\,\\!\\}\sigma)$.
By using Lemma 9.3(i), we obtain $m\in
I(\mathsf{A},\\{\,\\!G/\mathsf{x}\,\\!\\}\\{\,\\!F/\mathsf{x}\,\\!\\}\sigma)=I(\mathsf{A},\\{\,\\!G/\mathsf{x}\,\\!\\}\sigma)$
and hence $G\vdash m\in I(\lambda\mathsf{x}\mathsf{A},\sigma)$. As for the
opposite inclusion, suppose now that $\ell\in
I(\lambda\mathsf{x}\mathsf{A},\sigma)$. If $\ell=\mathsf{x}$, we also have
$\mathsf{x}\in
I(\lambda\mathsf{x}\mathsf{A},\\{\,\\!\emptyset/\mathsf{x}\,\\!\\}\sigma)$.
From this, we obtain $\emptyset\vdash\mathsf{x}\in
I(\lambda\mathsf{x}[\lambda\mathsf{x}\mathsf{A}],\sigma)$. Since
$\emptyset\subseteq_{f}I(\mathsf{D},\sigma)$ it follows that $\mathsf{x}\in
I([\lambda\mathsf{x}[\lambda\mathsf{x}\mathsf{A}]]\mathsf{D},\sigma)$.
Otherwise, we have $\ell=F\vdash m$ for some $F$ and $m$ such that $m\in
I(\mathsf{A},\\{\,\\!F/\mathsf{x}\,\\!\\}\sigma)$. By using Lemma 9.3(i), we
obtain $m\in
I(\mathsf{A},\\{\,\\!F/\mathsf{x}\,\\!\\}\sigma)=I(\mathsf{A},\\{\,\\!F/\mathsf{x}\,\\!\\}\\{\,\\!\emptyset/\mathsf{x}\,\\!\\}\sigma)$
and we get $\ell\in
I(\lambda\mathsf{x}\mathsf{A},\\{\,\\!\emptyset/\mathsf{x}\,\\!\\}\sigma)$ and
$\emptyset\vdash\ell\in
I(\lambda\mathsf{x}[\lambda\mathsf{x}\mathsf{A}],\sigma)$. Since
$\emptyset\subseteq_{f}I(\mathsf{D},\sigma)$, we then have $\ell\in
I([\lambda\mathsf{x}[\lambda\mathsf{x}\mathsf{A}]]\mathsf{D},\sigma)$.

($\beta_{5}$) Suppose that $\mathsf{x}\neq\mathsf{y}$ and
$[\lambda\mathsf{y}\mathsf{D}]\mathsf{x}\,\\!\sim_{I}\,\\!\mathsf{D}$. We now
show that
$I([\lambda\mathsf{x}[\lambda\mathsf{y}\mathsf{A}]]\mathsf{D},\sigma)=I(\lambda\mathsf{y}[[\lambda\mathsf{x}\mathsf{A}]\mathsf{D}],\sigma)$.
Assume $\ell\in
I([\lambda\mathsf{x}[\lambda\mathsf{y}\mathsf{A}]]\mathsf{D},\sigma)$. Then,
there exists $F\subseteq_{f}I(\mathsf{D},\sigma)$ such that $F\vdash\ell\in
I(\lambda\mathsf{x}[\lambda\mathsf{y}\mathsf{A}],\sigma)$. From this, it
follows that $\ell\in
I(\lambda\mathsf{y}\mathsf{A},\\{\,\\!F/\mathsf{x}\,\\!\\}\sigma)$. If
$\ell=\mathsf{y}$, then we obviously have $\mathsf{y}\in
I(\lambda\mathsf{y}[[\lambda\mathsf{x}\mathsf{A}]\mathsf{D}],\sigma)$.
Otherwise, we have $\ell=G\vdash m$ for some $G$ and $m$ such that $m\in
I(\mathsf{A},\\{\,\\!G/\mathsf{y}\,\\!\\}\\{\,\\!F/\mathsf{x}\,\\!\\}\sigma)$.
Since $\mathsf{x}\neq\mathsf{y}$, by using Lemma 9.3(ii) we obtain $m\in
I(\mathsf{A},\\{\,\\!F/\mathsf{x}\,\\!\\}\\{\,\\!G/\mathsf{y}\,\\!\\}\sigma)$.
So, we get $F\vdash m\in
I(\lambda\mathsf{x}\mathsf{A},\\{\,\\!G/\mathsf{y}\,\\!\\}\sigma)$. Since
$[\lambda\mathsf{y}\mathsf{D}]\mathsf{x}\,\\!\sim_{I}\,\\!\mathsf{D}$, we have
$I(\mathsf{D},\sigma)=I(\mathsf{D},\\{\,\\!G/\mathsf{y}\,\\!\\}\sigma)$ by
Lemma 9.6. Since $F\subseteq_{f}I(\mathsf{D},\sigma)$, we have
$F\subseteq_{f}I(\mathsf{D},\\{\,\\!G/\mathsf{y}\,\\!\\}\sigma)$. Now, as
$F\vdash m\in
I(\lambda\mathsf{x}\mathsf{A},\\{\,\\!G/\mathsf{y}\,\\!\\}\sigma)$, we obtain
$m\in
I([\lambda\mathsf{x}\mathsf{A}]\mathsf{D},\\{\,\\!G/\mathsf{y}\,\\!\\}\sigma)$.
Thus, we conclude that $G\vdash m\in
I(\lambda\mathsf{y}[[\lambda\mathsf{x}\mathsf{A}]\mathsf{D}],\sigma)$. To show
the opposite inclusion, assume now $\ell\in
I(\lambda\mathsf{y}[[\lambda\mathsf{x}\mathsf{A}]\mathsf{D}],\sigma)$. If
$\ell=\mathsf{y}$, then we also have $\mathsf{y}\in
I(\lambda\mathsf{y}\mathsf{A},\\{\,\\!\emptyset/\mathsf{x}\,\\!\\}\sigma)$.
From this, we obtain $\emptyset\vdash\mathsf{y}\in
I(\lambda\mathsf{x}[\lambda\mathsf{y}\mathsf{A}],\sigma)$. Since
$\emptyset\subseteq_{f}I(\mathsf{D},\sigma)$, it follows that $\mathsf{y}\in
I([\lambda\mathsf{x}[\lambda\mathsf{y}\mathsf{A}]]\mathsf{D},\sigma)$.
Otherwise, we have $\ell=F\vdash m$ for some $F$ and $m$ such that $m\in
I([\lambda\mathsf{x}\mathsf{A}]\mathsf{D},\\{\,\\!F/\mathsf{y}\,\\!\\}\sigma)$.
Furthermore, there exists
$G\subseteq_{f}I(\mathsf{D},\\{\,\\!F/\mathsf{y}\,\\!\\}\sigma)$ such that
$G\vdash m\in
I(\lambda\mathsf{x}\mathsf{A},\\{\,\\!F/\mathsf{y}\,\\!\\}\sigma)$. From this,
we obtain $m\in
I(\mathsf{A},\\{\,\\!G/\mathsf{x}\,\\!\\}\\{\,\\!F/\mathsf{y}\,\\!\\}\sigma)$.
Since $\mathsf{x}\neq\mathsf{y}$, we can apply Lemma 9.3(ii) and we get $m\in
I(\mathsf{A},\\{\,\\!F/\mathsf{y}\,\\!\\}\\{\,\\!G/\mathsf{x}\,\\!\\}\sigma)$.
From this, we obtain $F\vdash m\in
I(\lambda\mathsf{y}\mathsf{A},\\{\,\\!G/\mathsf{x}\,\\!\\}\sigma)$ and
$G\vdash F\vdash m\in
I(\lambda\mathsf{x}[\lambda\mathsf{y}\mathsf{A}],\sigma)$. Since
$[\lambda\mathsf{y}\mathsf{D}]\mathsf{x}\,\\!\sim_{I}\,\\!\mathsf{D}$, we have
$I(\mathsf{D},\sigma)=I(\mathsf{D},\\{\,\\!F/\mathsf{y}\,\\!\\}\sigma)$ by
Lemma 9.6. Since
$G\subseteq_{f}I(\mathsf{D},\\{\,\\!F/\mathsf{y}\,\\!\\}\sigma)$, we have
$G\subseteq_{f}I(\mathsf{D},\sigma)$. Now, since $G\vdash F\vdash m\in
I(\lambda\mathsf{x}[\lambda\mathsf{y}\mathsf{A}],\sigma)$, we finally obtain
$F\vdash m\in
I([\lambda\mathsf{x}[\lambda\mathsf{y}\mathsf{A}]]\mathsf{D},\sigma)$.

The proof of the theorem is now complete. ∎

We can now prove Theorem 3.3 as follows. By Theorem 9.7, the relation
$\,\\!\sim_{I}\,\\!$ is a prelambda congruence. Now, let $\mathsf{x}$ and
$\mathsf{y}$ two variables such that $\mathsf{x}\neq\mathsf{y}$. Let $\sigma$
be an environment. We have $\mathsf{x}\in
I(\lambda\mathsf{x}\mathsf{x},\sigma)$ and $\mathsf{x}\notin
I(\lambda\mathsf{y}\mathsf{y},\sigma)$, as $\mathsf{x}\neq\mathsf{y}$ and
$\mathsf{y}$ is the only atomic formula in
$I(\lambda\mathsf{y}\mathsf{y},\sigma)$. This shows that
$\lambda\mathsf{x}\mathsf{x}\ \\!\not\,\\!\sim_{I}\
\\!\lambda\mathsf{y}\mathsf{y}$.

##  10 Conclusions and Some Directions for Future Work

In this work we have obtained alternative and simplified formulations of the
concepts of lambda theory and extensional theory without introducing the
meta–theoretic notion of substitution and the conceptually inelegant sets of
all, free and bound variables occurring in a term. We have also clarified the
actual role of $\alpha$–renaming and $\eta$–extensionality in the lambda
calculus: from a convenient point of view — our prelambda congruences — both
of them can be equivalently described as properties of extensionality for
certain classes of terms.

Our proof of the elimination of the ancillary concepts is rather technical,
but conceptually speaking very simple. We also point out that in the relevant
literature discussed in Section 1 we could not find _complete_ and _detailed_
proofs of results similar to those we proved in Section 8 and Section 9. For
this reason — and also because we want to make the article readable by a wider
audience — we decided to make our exposition self–contained as much as
possible.

As for future work, we plan to apply the ideas we followed in this paper to
other contexts. For instance, we would like to provide similar formalizations
of various notions of _derivability_ (of formulas and sequents) for several
first– and higher–order logics and theories. As already observed by Révész
[41], some results for derivability in classical first–order logic with
equality which are in line with our motivations — the elimination of some
meta–theoretic notions included in our ancillary concepts — have been already
established by Tarski [51], Kalish and Montague [28] and Monk [34]. Similar
results for second–order classic logic have been established by Cocchiarella
[14]. But in our opinion, the most satisfactory axiomatization of first–order
classical logic with equality, due to Németi, is reported in the book of Blok
and Pigozzi [9, App. C]. In contrast to the aforementioned work, the
formulation described in that book has the pleasant property of being
completely free of ancillary concepts.

We believe that there is a more uniform way to tackle the problem of
eliminating the ancillary concepts from several logics, as we now intuitively
explain. It is well–known that substitution — which is usually introduced as a
tool for developing the proof–theory of the quantifiers — can be completely
handled by the lambda notation, as in Church’s theory of simple types [12].
This theory can be seen as (an extension of) classical higher–order logic and
we refer to Coquand [16, Sec. 1] for a very elegant presentation of its purely
logical part in an intuitionistic setting. We think that the ideas and the
approach employed in the present article can be exploited to remove the
ancillary concepts — which have no mathematical and logical substance — from
logic and hence simplify the presentations of intuitionistic and classical
higher–order logics.

We also plan to export our ideas to give new presentations of some frameworks
based on the lambda calculus (without types) whose aim is to formalize
(considerable parts of) mathematics such as the _type–free systems_ introduced
by Myhill and Flagg [35] and _map theory_ , a setting originally introduced by
Grue and recently simplified by Berline and Grue [8].

Finally, we also believe that some ideas we have introduced in this paper can
be useful to develop another approach to lambda calculi with _explicit
substitutions_ , see Abadi, Cardelli, Curien and Lévi [1] and also Kesner [29]
for a brief survey. Our suggestion is to internalize substitutions as in the
theory of lambda substitution algebras, the algebraic framework introduced by
Diskin and Beylin [21] discussed in Section 3. The expected advantage should
be the following: no ancillary concept other than substitution — which is not
a meta–theoretic notion in that context — would appear in the formalizations
of lambda and extensional theories in systems with explicit substitutions.

More generally, we believe that the _algebraic_ approach to binding
operations, see Cardone and Hindley [10, p. 736] for a brief survey, has been
relatively overlooked by the computer science community — exceptions are, of
course, lambda abstraction and lambda substitution algebras. While the primary
goals of those lines of work, namely _representation theorems_ , are perhaps
more palatable to algebraists than computer scientists, we think that the
study of the algebraic approach to quantification can be very useful for the
developments of better syntactical formalizations of theories in structures
with binding operations.

## References

  * Abadi et al. [1991] M. Abadi, L. Cardelli, P.-L. Curien, and J.-J. Lévy.  Explicit substitutions.  _Journal of Functional Programming_ , 1(4):375–416, 1991.  doi:10.1017/S0956796800000186.
  * Andrews [1965] P. B. Andrews.  _A Transfinite Type Theory with Type Variables_.  North–Holland, 1965.  doi:10.1016/S0049-237X(08)71167-4.
  * Andrews [1986] P. B. Andrews.  _Introduction to Mathematical Logic and Type Theory: To Truth Through Proof_.  Academic Press, 1986.
  * Barendregt [1971] H. P. Barendregt.  _Some extensional term models for combinatory logics and $\lambda$–calculi_.  PhD thesis, University of Utretch, 1971.  URL http://hdl.handle.net/2066/27329.  Revised in 2006.
  * Barendregt [1984] H. P. Barendregt.  _The Lambda Calculus. Its Syntax and Semantics_.  North–Holland, 1984.  doi:10.1016/B978-0-444-87508-2.50006-X.  Revised Edition.
  * Berline [2000] C. Berline.  From computation to foundations via functions and application: The $\lambda$–calculus and its webbed models.  _Theoretical Computer Science_ , 249(1):81–161, 2000.  doi:10.1016/S0304-3975(00)00057-8.
  * Berline [2006] C. Berline.  Graph models of $\lambda$–calculus at work, and variations.  _Mathematical Structures in Computer Science_ , 16(2):185–221, 2006.  doi:10.1017/S0960129506005123.
  * Berline and Grue [2016] C. Berline and K. Grue.  A synthetic axiomatization of Map Theory.  _Theoretical Computer Science_ , 614:1–62, 2016.  doi:10.1016/j.tcs.2015.11.028.
  * Blok and Pigozzi [1989] W. J. Blok and D. Pigozzi.  _Algebraizable Logics_ , volume 77.  Memoirs of the American Mathematical Society, 1989.  doi:10.1090/memo/0396.
  * Cardone and Hindley [2009] F. Cardone and J. R. Hindley.  Lambda–Calculus and Combinators in the 20th Century.  In D. M. Gabbay and J. Woods, editors, _Logic from Russell to Church_ , volume 5 of _Handbook of the History of Logic_ , pages 723–817. North–Holland, 2009.  doi:10.1016/S1874-5857(09)70018-4.
  * Church [1932] A. Church.  A Set of Postulates for the Foundation of Logic.  _Annals of Mathematics_ , 33(2):346–366, 1932\.  doi:10.2307/1968337.
  * Church [1940] A. Church.  A formulation of the simple theory of types.  _Journal of Symbolic Logic_ , 5(2):56–68, 1940\.  doi:10.2307/2266170.
  * Church [1941] A. Church.  _The Calculi of Lambda Conversion_.  Princeton University Press, 1941.  URL http://www.jstor.org/stable/j.ctt1b9x12d.
  * Cocchiarella [1969] N. B. Cocchiarella.  A substitution free axiom set for second order logic.  _Notre Dame Journal of Formal Logic_ , 10(1):18–30, 01 1969.  doi:10.1305/ndjfl/1093893584.
  * Copello et al. [2017] E. Copello, N. Szasz, and Á. Tasistro.  Formal Metatheory of the Lambda Calculus Using Stoughton’s Substitution.  _Theoretical Computer Science_ , 685:65–82, 2017.  doi:10.1016/j.tcs.2016.08.025.
  * Coquand [1986] T. Coquand.  An analysis of Girard’s paradox.  Technical Report RR–0531, INRIA, 1986.  URL https://hal.inria.fr/inria-00076023.
  * Crole [2012] R. L. Crole.  Alpha equivalence equalities.  _Theoretical Computer Science_ , 433:1–19, 2012.  doi:10.1016/j.tcs.2012.01.030.
  * Curry [1929] H. B. Curry.  An Analysis of Logical Substitution.  _American Journal of Mathematics_ , 51(3):363–384, 1929.  doi:10.2307/2370728.
  * Curry and Feys [1958] H. B. Curry and R. Feys.  _Combinatory Logic, Volume I_.  North–Holland, 1958.  doi:10.1016/S0049-237X(08)72029-9.
  * Curry et al. [1972] H. B. Curry, J. R. Hindley, and J. P. Seldin.  _Combinatory Logic, Volume II_.  North–Holland, 1972.  doi:10.1016/S0049-237X(09)70633-0.
  * Diskin and Beylin [1993] Z. Diskin and I. Beylin.  Lambda Substitution Algebras.  In A. M. Borzyszkowski and S. Sokołowski, editors, _Proceedings of Mathematical Foundations of Computer Science 1993_ , volume 711 of _Lecture Notes in Computer Science_ , pages 423–432, 1993\.  doi:10.1007/3-540-57182-5_34.
  * Došen and Petrić [2001] K. Došen and Z. Petrić.  The Typed Böhm Theorem.  _Electronic Notes in Theoretical Computer Science_ , 50(2):117–129, 2001.  doi:10.1016/S1571-0661(04)00168-9.
  * Engeler [1981] E. Engeler.  Algebras and combinators.  _Algebra Universalis_ , 13(1):389–392, 1981.  doi:10.1007/BF02483849.
  * Hankin [1994] C. Hankin.  _Lambda Calculi. A Guide for Computer Scientists_.  Clarendon Press, 1994.
  * Henkin [1963] L. Henkin.  A theory of propositional types.  _Fundamenta Mathematicae_ , 52(3):323–344, 1963\.  URL http://matwbn.icm.edu.pl/ksiazki/fm/fm52/fm52123.pdf.
  * Hindley and Seldin [2008] J. R. Hindley and J. P. Seldin.  _Lambda–Calculus and Combinators, an Introduction_.  Cambridge University Press, second edition, 2008.  doi:10.1017/CBO9780511809835.
  * Hindley and Longo [1980] R. Hindley and G. Longo.  Lambda–Calculus Models and Extensionality.  _Mathematical Logic Quarterly_ , 26(19–21):289–310, 1980.  doi:10.1002/malq.19800261902.
  * Kalish and Montague [1965] D. Kalish and R. Montague.  On Tarski’s formalization of predicate logic with identity.  _Archiv für mathematische Logik und Grundlagenforschung_ , 7(3):81–101, May 1965.  doi:10.1007/BF01969434.
  * Kesner [2007] D. Kesner.  The Theory of Calculi with Explicit Substitutions Revisited.  In J. Duparc and T. A. Henzinger, editors, _Proceedings of Computer Science Logic 2007_ , volume 4646 of _Lecture Notes in Computer Science_ , pages 238–252, 2007.  doi:10.1007/978-3-540-74915-8_20.
  * Krivine [1993] J.-L. Krivine.  _Lambda–Calculus, Types and Models_.  Ellis Horwood and Prentice–Hall, 1993.
  * Longo [1983] G. Longo.  Set–theoretical models of $\lambda$–calculus: theories, expansions, isomorphisms.  _Annals of Pure and Applied Logic_ , 24(2):153–188, 1983.  doi:10.1016/0168-0072(83)90030-1.
  * Manzonetto and Salibra [2010] G. Manzonetto and A. Salibra.  Applying Universal Algebra to Lambda Calculus.  _Journal of Logic and Computation_ , 20(4):877–915, 2010.  doi:10.1093/logcom/exn085.
  * Meyer [1982] A. R. Meyer.  What is a model of the lambda calculus?  _Information and Control_ , 52(1):87–122, 1982\.  doi:10.1016/S0019-9958(82)80087-9.
  * Monk [1965] D. Monk.  Substitutionless predicate logic with identity.  _Archiv für mathematische Logik und Grundlagenforschung_ , 7(3):102–121, 1965.  doi:10.1007/BF01969435.
  * Myhill and Flagg [1989] J. Myhill and B. Flagg.  A type–free system extending (ZFC).  _Annals of Pure and Applied Logic_ , 43(1):79–97, 1989.  doi:10.1016/0168-0072(89)90026-2.
  * Pigozzi and Salibra [1993] D. Pigozzi and A. Salibra.  An introduction to lambda abstraction algebras.  In M. Abad, editor, _Proceedings of IX Latin American Symposium on Mathematical Logic (Part I)_ , volume 38 of _Notas de Lógica Matemática_ , pages 93–112, 1993.  URL http://inmabb-conicet.gob.ar/publicaciones/nlm/Nlm-38.pdf.
  * Pigozzi and Salibra [1995] D. Pigozzi and A. Salibra.  Lambda abstraction algebras: representation theorems.  _Theoretical Computer Science_ , 140(1):5–52, 1995.  doi:10.1016/0304-3975(94)00203-U.
  * Pigozzi and Salibra [1998] D. Pigozzi and A. Salibra.  Lambda Abstraction Algebras: Coordinatizing Models of Lambda Calculus.  _Fundamenta Informaticae_ , 33(2):149–200, 1998\.  doi:10.3233/FI-1998-33203.
  * Plotkin [1993] G. D. Plotkin.  Set–theoretical and other elementary models of the $\lambda$–calculus.  _Theoretical Computer Science_ , 121(1):351–409, 1993.  doi:10.1016/0304-3975(93)90094-A.
  * Révész [1980] G. E. Révész.  Lambda–calculus without substitution.  _Bulletin of the European Association for Theoretical Computer Science_ , 11:140, 1980.
  * Révész [1985] G. E. Révész.  Axioms for the Theory of Lambda–Conversion.  _SIAM Journal on Computing_ , 14(2):373–382, 1985.  doi:10.1137/0214028.
  * Révész [1988] G. E. Révész.  _Lambda–Calculus, Combinators, and Functional Programming_.  Cambridge University Press, 1988.
  * Rosenbloom [1950] P. C. Rosenbloom.  _The Elements of Mathematical Logic_.  Dover Publications, 1950.  Reprinted in 2005.
  * Salibra [2000] A. Salibra.  On the algebraic models of lambda calculus.  _Theoretical Computer Science_ , 249(1):197–240, 2000.  doi:10.1016/S0304-3975(00)00059-1.
  * Seldin [2009] J. P. Seldin.  The Logic of Church and Curry.  In D. M. Gabbay and J. Woods, editors, _Logic from Russell to Church_ , volume 5 of _Handbook of the History of Logic_ , pages 819–873. North–Holland, 2009.  doi:10.1016/S1874-5857(09)70019-6.
  * Shönfinkel [1967] M. Shönfinkel.  On the building blocks of mathematical logic.  In J. van Heijenoort, editor, _From Frege to Gödel. A Source Book in Mathematical Logic, 1879–1931_ , pages 355–366. Harvard University Press, 1967.
  * Sørensen and Urzyczyn [2006] M. H. Sørensen and P. Urzyczyn.  _Lectures on the Curry–Howard Isomorphism_.  Elsevier, 2006.  doi:10.1016/S0049-237X(06)80001-7.
  * Stenlund [1972] S. Stenlund.  _Combinators, $\lambda$–Terms and Proof Theory_.  Reidel Publishing Company, 1972.
  * Stoughton [1988] A. Stoughton.  Substitution revisited.  _Theoretical Computer Science_ , 59(3):317–325, 1988.  doi:10.1016/0304-3975(88)90149-1.
  * Stoy [1977] J. E. Stoy.  _Denotational Semantics: The Scott–Strachey Approach to Programming Language Theory_.  MIT Press, 1977.
  * Tarski [1965] A. Tarski.  A simplified formalization of predicate logic with identity.  _Archiv für mathematische Logik und Grundlagenforschung_ , 7(1):61–79, 1965.  doi:10.1007/BF01972461.
  * Vestergaard [2003] R. Vestergaard.  _The Primitive Proof Theory of the $\lambda$–Calculus_.  PhD thesis, Heriot–Watt University, 2003.  URL http://hdl.handle.net/10399/415.
  * von Neumann [1967] J. von Neumann.  An Axiomatization of Set Theory.  In J. van Heijenoort, editor, _From Frege to Gödel. A Source Book in Mathematical Logic, 1879–1931_ , pages 393–413. Harvard University Press, 1967.
  * Wadsworth [1976] C. P. Wadsworth.  The Relation between Computational and Denotational Properties for Scott’s $D_{\infty}$–Models of the Lambda–Calculus.  _SIAM Journal on Computing_ , 5(3):488–521, 1976.  doi:10.1137/0205036.
  * Welch [1974] P. H. Welch.  _The Minimal Continuous Semantics of the Lambda–Calculus_.  PhD thesis, University of Warwick, 1974.  URL http://wrap.warwick.ac.uk/72113/.


# Self-Taught Hashing for Fast Similarity Search

Dell Zhang

Jun Wang

DCSIS  Birkbeck, University of London  Malet Street  London WC1E 7HX, UK
<EMAIL_ADDRESS>Dept of Computer Science  University College London  Gower
Street  London WC1E 6BT, UK<EMAIL_ADDRESS>Deng Cai

Jinsong Lu

State Key Lab of CAD&CG  Zhejiang University  100 Zijinggang Road  Hangzhou
310058, China<EMAIL_ADDRESS>DEMS  Birkbeck, University of London
Malet Street  London WC1E 7HX, UK<EMAIL_ADDRESS>
(2010)

###### Abstract

The ability of fast similarity search at large scale is of great importance to
many Information Retrieval (IR) applications. A promising way to accelerate
similarity search is semantic hashing which designs compact binary codes for a
large number of documents so that semantically similar documents are mapped to
similar codes (within a short Hamming distance). Although some recently
proposed techniques are able to generate high-quality codes for documents
known in advance, obtaining the codes for previously unseen documents remains
to be a very challenging problem. In this paper, we emphasise this issue and
propose a novel Self-Taught Hashing (STH) approach to semantic hashing: we
first find the optimal $l$-bit binary codes for all documents in the given
corpus via unsupervised learning, and then train $l$ classifiers via
supervised learning to predict the $l$-bit code for any query document unseen
before. Our experiments on three real-world text datasets show that the
proposed approach using binarised Laplacian Eigenmap (LapEig) and linear
Support Vector Machine (SVM) outperforms state-of-the-art techniques
significantly.

###### category:

H.2.8 Database Management Database Applications

###### keywords:

data mining

###### category:

H.3.1 Information Storage and Retrieval Content Analysis and Indexing

###### category:

H.3.3 Information Storage and Retrieval Information Search and Retrieval

###### category:

I.2.6 Artificial Intelligence Learning

###### category:

I.5.2 Pattern Recognition Design Methodology

###### keywords:

classifier design and evaluation

###### keywords:

Similarity Search, Semantic Hashing, Laplacian Eigenmap, Support Vector
Machine.

††conference: SIGIR’10, July 19–23, 2010, Geneva, Switzerland.††terms:
Algorithms, Experimentation, Performance

##  1 Introduction

The problem of _similarity search_ (aka _nearest neighbour search_) is: given
a query document111In similarity search, a document is used as the query for
retrieval, which is fundamentally different with the standard keyword search
paradigm, e.g., in TREC., find its most similar documents from a very large
document collection (corpus). It is of great importance to many Information
Retrieval (IR) [30] applications, such as near-duplicate detection [18],
plagiarism analysis [43], collaborative filtering [26], caching [32], and
content-based multimedia retrieval [28].

Recently, with the rapid evolution of the Internet and the increased amounts
of data to be processed, how to conduct fast similarity search at large scale
has become an urgent research issue. A promising way to accelerate similarity
search is _semantic hashing_ [34] which designs compact binary codes for a
large number of documents so that semantically similar documents are mapped to
similar codes (within a short Hamming distance). It is extremely fast to
perform similarity search over such binary codes [42], because

  * •

the encoded data are highly compressed and thus can be loaded into the main
memory;

  * •

the Hamming distance between two binary codes can be computed efficiently by
using bit XOR operation and counting the number of set bits [25, 46]: an
ordinary PC today would be able to do millions of Hamming distance computation
in just a few milliseconds.

Furthermore, we usually just need to retrieve a small number of the most
similar documents (i.e., nearest neighbours) for a given query document rather
than computing its similarity to all documents in the collection. In such
situations, we can simply return all the documents that are hashed into a
tight Hamming ball centred around the binary code of the query document. For
example, assuming that we use 4-bit binary codes, if the query document is
represented as ‘0000’, then we can just check this code as well as those 4
codes within one Hamming distance to it (i.e., having one bit difference with
it) — ‘1000’, ‘0100’, ‘0010’, and ‘0001’ — and return the associated documents
back. It will also be easy to filter or re-rank the very small set of “good”
documents (returned by semantic hashing) based on their full content, so as to
further improve the retrieval effectiveness with just a little extra time
[42].

In addition, similarity search serves as the basis of a classic non-parametric
machine learning method, the k-Nearest-Neighbours (kNN) algorithm [31], for
automated text categorisation [37] and so on. By enabling fast similarity
search at large scale, semantic hashing makes it feasible to exploit “the
unreasonable effectiveness of data” [14] to accomplish traditionally difficult
tasks. For example, researchers recently achieved great success in scene
completion and scene recognition using millions of images on the Web as
training data [15, 44].

Although some recently proposed techniques are able to generate high-quality
codes for the documents known in advance, obtaining the codes for previously
unseen documents remains to be a very challenging problem [42]. Existing
methods either have prohibitively high computational complexity or impose
exceedingly restrictive assumptions about data distribution (see Section 3.2).
In this paper, we emphasise this issue and propose a novel Self-Taught Hashing
(STH) approach to semantic hashing. As illustrated in Figure 1, we first find
the optimal $l$-bit binary codes for all documents in the given corpus via
unsupervised learning, and then train $l$ classifiers via supervised learning
to predict the $l$-bit code for any query document unseen before.

Our experiments on three real-world text datasets show that the proposed
approach using binarised Laplacian Eigenmap (LapEig) [3] and linear Support
Vector Machine (SVM) [23, 36] outperforms state-of-the-art techniques
significantly, while maintaining a high running speed.

The rest of this paper is organised as follows. In Section 2, we review the
related work. In Section 3, we present our approach in details. In Section 4,
we show the experimental results. In Section 5, we make conclusions.

Figure 1: The proposed STH approach to semantic hashing.

##  2 Related Work

There has been extensive research on fast similarity search due to its central
importance in many applications. For a low-dimensional feature space,
similarity search can be carried out efficiently with pre-built space-
partitioning index structures (such as KD-tree) or data-partitioning index
structures (such as R-tree) [7]. However, when the dimensionality of feature
space is high (say $>10$), similarity search aiming to return exact results
cannot be done better than the naive method — a linear scan of the entire
collection [45]. In the IR domain, documents are typically represented as
feature vectors in a space of more than thousands of dimensions [30].
Nevertheless, if the complete exactness of results is not really necessary,
similarity search in a high-dimensional space can be dramatically speeded up
by using hash-based methods which are purposefully designed to approximately
answer queries in virtually constant time [42].

Such hash-based methods for fast similarity search can be considered as a
means for embedding high-dimensional feature vectors to a low-dimensional
Hamming space (the set of all $2^{l}$ binary strings of length $l$), while
retaining as much as possible the semantic similarity structure of data.
Unlike standard dimensionality reduction techniques such as Latent Semantic
Indexing (LSI) [5, 8] and Locality-Preserving Indexing (LPI) [17, 16], hashing
techniques map feature vectors to _binary_ codes, which is key to extremely
fast similarity search (see Section 1). One possible way to get binary codes
for text documents is to binarise the real-valued low-dimensional vectors
(obtained from dimensionality reduction techniques like LSI) via thresholding
[34]. An improvement on binarised-LSI that directly optimises a Hamming
distance based objective function, namely Laplacian Co-Hashing (LCH), has been
proposed recently [50].

The most well-known hashing technique that preserves similarity information is
probably Locality-Sensitive Hashing (LSH) [1]. LSH simply employs random
linear projections (followed by random thresholding) to map data points close
in a Euclidean space to similar codes. It is theoretically guaranteed that as
the code length increases, the Hamming distance between two codes will
asymptotically approach the Euclidean distance between their corresponding
data points. However, since the design of hash functions for LSH is _data-
oblivious_ , LSH may lead to quite inefficient (long) codes in practice [34,
48].

Several recently proposed hashing techniques attempt to overcome this problem
by finding good _data-aware_ hash functions through machine learning. In [34],
the authors proposed to use stacked Restricted Boltzmann Machine (RBM) [19,
20], and showed that it was indeed able to generate compact binary codes to
accelerate document retrieval. Researchers have also tried the boosting
approach to Similarity Sensitive Coding (SSC) [38] and Forgiving Hashing (FgH)
[2] — they first train AdaBoost [35] classifiers with similar pairs of items
as positive examples (and also non-similar pairs of items as negative examples
in SCC), and then take the output of all (decision stump) weak learners on a
given document as its binary code. In [44], both stacked-RBM and boosting-SSC
were found to work significantly better and faster than LSH when applied to a
database containing tens of millions of images. In [48], a new technique
called Spectral Hashing (SpH) was proposed. It has demonstrated significant
improvements over LSH, stacked-RBM and boosting-SSC in terms of the number of
bits required to find good similar items. There is some resemblance between
the first step of SpH and the unsupervised learning stage of our STH approach,
because both are related to spectral graph partitioning [6, 13, 40].
Nevertheless, we use a different spectral method and take a different way to
address the _entropy maximising_ criterion (see Section 3.1). More
importantly, in order to process query documents, SpH has to assume that the
data are uniformly distributed in a hyper-rectangle, which is apparently very
restrictive. In contrast, our proposed STH approach can work with any data
distribution and it is much more flexible (see Section 3.2). The superiority
of STH to SpH has been confirmed by our experimental results (see Section 4).

A somewhat related, but different, line of research is to use hashing
representations for machine learning [41, 47]. The objective of such
techniques is to accelerate complex learning algorithms, but not similarity
search. Our work is basically the other way around.

##  3 Approach

The proposed Self-Taught Hashing (STH) approach to semantic hashing is a
_general_ learning framework that consists of two distinct stages, as
illustrated in Figure 1. We call the approach “self-taught” because the hash
function is learnt from the data that are auto-labelled by itself in the
previous stage222It is, however, worth noticing that the term “self-taught
learning” has been mentioned in [33] where the intention was to describe a
strategy for transfer learning based on sparse coding, whereas in this paper
the term has a rather different meaning..

###  3.1 Stage 1:
Unsupervised Learning of Binary Codes

Given a collection of $n$ documents which are represented as $m$-dimensional
vectors $\\{\mathbf{x}_{i}\\}_{i=1}^{n}\subset\mathbb{R}^{m}$. Let $X$ denote
the $m\times n$ term-document matrix:
$[\mathbf{x}_{1},\ldots,\mathbf{x}_{n}]$. Suppose that the desired length of
code is $l$ bits. We use $\mathbf{y}_{i}\in\\{-1,+1\\}^{l}$ to represent the
binary code for document vector $\mathbf{x}_{i}$, where the $p$-th element of
$\mathbf{y}_{i}$, i.e., $y_{i}^{(p)}$, is $+1$ if the $p$-th bit of code is
on, or $-1$ otherwise. Let $Y$ denote the $n\times l$ matrix whose $i$-th row
is the code for the $i$-th document, i.e.,
$[\mathbf{y}_{1},\ldots,\mathbf{y}_{n}]^{T}$.

A “good” semantic hashing should be _similarity preserving_ to ensure
effectiveness. That is to say, semantically similar documents should be mapped
to similar codes within a short Hamming distance.

Unlike the existing approaches (such as SpH [48]) that aim to preserve the
_global_ similarity structure of all document pairs, we focus on the _local_
similarity structure, i.e., $k$-nearest-neighbourhood, for each document.
Since IR applications usually put emphasis on a small number of most similar
documents for a given query document [30], preserving the global similarity
structure is not only unnecessary but also likely to be sub-optimal for our
problem. Therefore, using the _cosine similarity_ 333Our approach can work
with any legitimate similarity measure, though we focus on cosine similarity
in this paper. [30], we construct our $n\times n$ _local_ similarity matrix
$W$ as

$W_{ij}=\left\\{\begin{array}[]{cl}\frac{\mathbf{x}_{i}^{T}\mathbf{x}_{j}}{\|\mathbf{x}_{i}\|\cdot\|\mathbf{x}_{j}\|}&\qquad\text{if
}\mathbf{x}_{i}\in N_{k}(\mathbf{x}_{j})\text{ or }\mathbf{x}_{j}\in
N_{k}(\mathbf{x}_{i})\\\ 0&\qquad\text{otherwise}\end{array}\right.$ (1)

where $N_{k}(\mathbf{x})$ represents the set of $k$-nearest-neighbours of
document $\mathbf{x}$. In other words, $W$ is the adjacency matrix of the
$k$-nearest-neighbours graph for the given corpus [3]. A by-product of
focusing on such a local similarity structure instead of the global one is
that $W$ becomes a sparse matrix. This not only leads to much lower storage
overhead, but also brings a significant reduction to the computational
complexity of subsequent operations. Furthermore, we introduce a diagonal
$n\times n$ matrix $D$ whose entries are given by
$D_{ii}=\sum_{j=1}^{n}W_{ij}$. The matrix $D$ provides a natural measure of
document importance: the bigger the value of $D_{ii}$ is, the more “important”
is the document $\mathbf{x}_{i}$ as its neighbours are strongly connected to
it [3].

The Hamming distance between two binary codes $\mathbf{y}_{i}$ and
$\mathbf{y}_{j}$ (corresponding to documents $\mathbf{x}_{i}$ and
$\mathbf{x}_{j}$) is given by the number of bits that are different between
them, which can be calculated as
$\frac{1}{4}\|\mathbf{y}_{i}-\mathbf{y}_{j}\|^{2}$. To meet the _similarity
preserving_ criterion, we seek to minimise the weighted average Hamming
distance (as in SpH [48])

$\frac{1}{4}\sum_{i=1}^{n}\sum_{j=1}^{n}W_{ij}\|\mathbf{y}_{i}-\mathbf{y}_{j}\|^{2}$
(2)

because it incurs a heavy penalty if two similar documents are mapped far
apart. After some simple mathematical transformation, the above objective
function can be rewritten in matrix form as
$\frac{1}{4}\operatorname*{Tr}(Y^{T}LY)$, where $L=D-W$ is the _graph
Laplacian_ [6], and $\operatorname*{Tr}(\cdot)$ means the matrix trace.

We found the above objective function (2) actually proportional to that of a
well-known manifold learning algorithm, Laplacian Eigenmap (LapEig) [3],
except that LapEig does not have the constraint
$\mathbf{y}_{i}\in\\{-1,+1\\}^{l}$. So, if we relax this discreteness
condition but just keep the _similarity preserving_ requirement, we can get
the optimal $l$-dimensional real-valued vector $\tilde{\mathbf{y}}_{i}$ to
represent each document $\mathbf{x}_{i}$ by solving the following LapEig
problem:

$\displaystyle\operatorname*{arg\,min}_{\tilde{Y}}\qquad$
$\displaystyle\operatorname*{Tr}(\tilde{Y}^{T}L\tilde{Y})$ (3) subject to
$\displaystyle\tilde{Y}^{T}D\tilde{Y}=I$
$\displaystyle\tilde{Y}^{T}D\mathbf{1}=\mathbf{0}$

where $\operatorname*{Tr}(\tilde{Y}^{T}L\tilde{Y})$ gives the real relaxation
of the weighted average Hamming distance $\operatorname*{Tr}(Y^{T}LY)$, and
the two constraints prevent the collapse into a subspace of dimension less
than $l$. The solution of this optimisation problem is given by
$\tilde{Y}=[\mathbf{v}_{1},\ldots,\mathbf{v}_{l}]$ whose columns are the $l$
eigenvectors corresponding to the smallest eigenvalues of the following
generalised eigenvalue problem (except the trivial eigenvalue 0):

$L\mathbf{v}=\lambda D\mathbf{v}$ (4)

The above LapEig formulation (3) may look similar to the first step of SpH
[48]. This is because SpH is motivated by a spectral graph partitioning method
_ratio-cut_ [13], while LapEig is closely connected to another spectral graph
partitioning method _normalised-cut_ [40]. Many independent studies have shown
that normalised-cut has better theoretical properties and empirical
performances than ratio-cut [6, 40].

We now convert the above $l$-dimensional real-valued vectors
$\tilde{\mathbf{y}}_{1},\ldots,\tilde{\mathbf{y}}_{n}$ into binary codes via
thresholding: if the $p$-th element of $\tilde{\mathbf{y}}_{i}$ is larger than
the specified threshold, $y_{i}^{(p)}=+1$ (i.e., the $p$-th bit of the $i$-th
code is on); otherwise, $y_{i}^{(p)}=-1$ (i.e., the $p$-th bit of the $i$-th
code is off).

A “good” semantic hashing should also be _entropy maximising_ to ensure
efficiency, as pointed out by [2]. According to the _information theory_ [39]:
the maximal entropy of a source alphabet is attained by having a uniform
probability distribution. If the entropy of codes over the corpus is small, it
means that documents are mapped to only a small number of codes (hash bins),
thereby rendering the hash table inefficient. To meet this _entropy
maximising_ criterion, we set the threshold for binarising
$\tilde{y}_{1}^{(p)},\ldots,\tilde{y}_{n}^{(p)}$ to be the _median_ value of
$\mathbf{v}_{p}$. In this way, the $p$-th bit will be on for half of the
corpus and off for the other half. Furthermore, as the eigenvectors
$\mathbf{v}_{1},\ldots,\mathbf{v}_{l}$ given by LapEig are orthogonal to each
other, different bits $y^{(1)},\ldots,y^{(l)}$ in the generated binary codes
will be uncorrelated. Therefore this thresholding method gives each distinct
binary code roughly equal probability of occurring in the document collection,
thus achieves the best utilisation of the hash table.

###  3.2 Stage 2:
Supervised Learning of Hash Function

Mapping all documents in the given corpus to binary codes does not completely
solve the problem of semantic hashing, because we also need to know how to
obtain the binary codes for query documents, i.e., new documents that are
unseen before. This problem, called _out-of-sample extension_ in manifold
learning, is often addressed using the Nystrom method [4, 9]. However,
calculating the Nystrom extension of a new document is as computationally
expensive as an exhaustive similarity search over the corpus (that may contain
millions of documents), which makes it impractical for semantic hashing. In
LPI [17, 16], LapEig [3] is extended to deal with new samples by approximating
a linear function to the embedding of LapEig. However, the computational
complexity of LPI is very high because its learning algorithm involves eigen-
decompositions of two large dense matrices. It is infeasible to apply LPI if
the given training corpus is large. In SpH [48], new samples are handled by
utilising the latest results on the convergence of graph Laplacian
eigenvectors to the Laplace-Beltrami eigenfunctions of manifolds. It can
achieve both fast learning and fast prediction, but it relies on a very
restrictive assumption that the data are uniformly distributed in a hyper-
rectangle.

Overcoming the limitations of the above techniques [4, 9, 17, 16, 48], this
paper proposes a novel method to compute the binary codes for query documents
by considering it as a supervised444Since in the second stage, the supervised
learning algorithm uses only the _pseudo_ -labels input from the previous
unsupervised learning stage, the entire STH approach remains to be
unsupervised. learning problem: we think of each bit
$y_{i}^{(p)}\in\\{+1,-1\\}$ in the binary code for document $\mathbf{x}_{i}$
as a binary class label (class-“on” or class-“off”) for that document, and
train a binary classifier $y^{(p)}=f^{(p)}(\mathbf{x})$ on the given corpus
that has already been “labelled” by the above binarised-LapEig method, then we
can use the learned binary classifiers $f^{(1)},\ldots,f^{(l)}$ to predict the
$l$-bit binary code $y^{(1)},\ldots,y^{(l)}$ for any query document
$\mathbf{x}$. As mentioned in the previous section, different bits
$y^{(1)},\ldots,y^{(l)}$ in the generated binary codes are uncorrelated. Hence
there is no redundancy among the binary classifiers $f^{(1)},\ldots,f^{(l)}$,
and they can also be trained independently.

In this paper, we choose to use the Support Vector Machine (SVM) [23, 36]
algorithm to train these binary classifiers. SVM in its simplest form, linear
SVM $f(\mathbf{x})=\operatorname*{sgn}(\mathbf{w}^{T}\mathbf{x})$ consistently
provides state-of-the-art performance for text classification tasks [10, 22,
49]. Given the documents $\mathbf{x}_{1},\ldots,\mathbf{x}_{n}$ together with
their _self-taught_ binary labels for the $p$-th bit
$y_{1}^{(p)},\ldots,y_{n}^{(p)}$, the corresponding linear SVM can be trained
by solving the following quadratic optimisation problem

$\displaystyle\operatorname*{arg\,min}_{\mathbf{w},\xi_{i}\geq 0}\qquad$
$\displaystyle\frac{1}{2}{\mathbf{w}^{T}\mathbf{w}}+\frac{C}{n}{\sum_{i=1}^{n}\xi_{i}}$
(5) subject to
$\displaystyle\forall_{i=1}^{n}:y_{i}^{(p)}\mathbf{w}^{T}\mathbf{x}_{i}\geq
1-\xi_{i}$

A notable advantage of using SVM classifiers here is that we can easily
achieve non-linear mappings if necessary by plugging in non-linear kernels
[36], though we do not explore this potential in this paper.

###  3.3 Summary of Approach

We name the above proposed two-stage approach Self-Taught Hashing (STH). In
this paper, we choose binarised-LapEig [3] for the unsupervised learning stage
and linear-SVM [23, 36] for the supervised learning stage, but obviously it is
possible to use other machine learning algorithms.

The _learning_ process of STH for a given corpus can be summarized as follows.

  1. 1.

unsupervised learning of binary codes:

     * •

construct the $k$-nearest-neighbours graph for the given corpus;

     * •

embed the documents in an $l$-dimensional space through LapEig (4) to get an
$l$-dimensional real-valued vector for each document;

     * •

obtain an $l$-bit binary code for each document via thresholding the above
vectors at their median point, and then take each bit as a binary class label
for that document;

  2. 2.

supervised learning of hash function:

     * •

train $l$ SVM classifiers (5) based on the given corpus that has been
“labelled” as above.

Let $s$ denote the average number of non-zero features per document. In the
first stage, constructing the $k$-nearest-neighbours graph takes
$\operatorname*{O}(n^{2}s+n^{2}k)$ time using the selection algorithm [7],
solving the LapEig problem (4) takes $\operatorname*{O}(lnkt)$ time using the
Lanczos algorithm [12] of $t$ iterations (the value of $t$ is usually quite
small), and the median-based binarisation takes $\operatorname*{O}(ln)$ time
again using the selection algorithm [7]. In the second stage, thanks to the
recent advances in large-scale optimisation, each of the $l$ linear SVM
classifiers can be trained in $\operatorname*{O}(sn)$ time or even less [24,
21], so all training can be done in $\operatorname*{O}(lsn)$ time. Both the
value of $l$ and the value of $k$ can be regarded as small constants, as
usually a short code length is desirable and just a few nearest neighbours are
needed. For example, $l\leq 64$ and $k=25$ in our experiments (see Section 4).
Therefore the overall computational complexity of the learning process is
roughly quadratic to the number of documents in the corpus while linear to the
average size of the documents in the corpus.

The _predicting_ process of STH for a given query document is simply to
classify the query document using those $l$ learned classifiers and then
assemble the output $l$ binary labels into an $l$-bit binary code. For linear
SVM, classifying a document only requires one dot-product operation between
two vectors, the aggregated support vector and the document vector (with
$s^{\prime}$ non-zero features), which can be done quickly in
$\operatorname*{O}(s^{\prime})$ time. Therefore the overall computational
complexity of the prediction process for each query document is linear to the
size of the query document.

##  4 Experiments

We now empirically evaluate our proposed STH approach (using binarised-LapEig
and linear-SVM), and compare its performance with binarised-LSI [34], LCH
[50], and SpH [48] that represents the state of the art (see Section 2).

In the following STH experiments, the parameter $k=25$ when constructing the
$k$-nearest-neighbours graph for LapEig555In principle, the value of $k$ for
LapEig should be set to the desired number of original nearest neighbours to
be retrieved (see Section 4.2)., and the SVM implementation is from LIBLINEAR
[11] with the default parameter values666It is not necessary to fine tune the
SVM parameters (such as $C$) because it has already worked very well with its
default parameter values..

###  4.1 Data

We have conducted experiments on three publicly available real-world text
datasets: Reuters21578777http://www.daviddlewis.com/resources/testcollections/
reuters21578/,
20Newsgroups888http://people.csail.mit.edu/jrennie/20Newsgroups/ and
TDT2999http://www.nist.gov/speech/tests/tdt/tdt98/index.htm.

The Reuters21578 corpus is a collection of documents that appeared on Reuters
newswire in 1987. It contains 21578 documents in 135 categories. In our
experiments, those documents appearing in more than one category were
discarded, and only the largest 10 categories were kept, thus leaving us with
7285 documents in total. We use the ModeApte split here which gives 5228 (72%)
documents for training and 2057 (28%) documents for testing.

The 20Newsgroups corpus was collected and originally used for document
categorisation by Lang [27]. We use the popular ‘bydate’ version which
contains 18846 documents, evenly distributed across 20 categories. The time-
based split leads to 11314 (60%) documents for training and 7532 (40%)
documents for testing.

The TDT2 (NIST Topic Detection and Tracking) corpus consists of data collected
during the first half of 1998 and taken from 6 sources, including 2 newswires
(APW, NYT), 2 radio programs (VOA, PRI) and 2 television programs (CNN, ABC).
It consists of 11201 on-topic documents which are classified into 96 semantic
categories. In our experiments, those documents appearing in more than one
category were discarded, and only the largest 30 categories were kept, thus
leaving us with 9394 documents in total. We randomly selected 5597 (60%)
documents for training and 3797 (40%) documents for testing. The averaged
performance based on 10 such random selections is reported in this paper.

All the above datasets have been pre-processed by stop-word removal, Porter
stemming, and TF-IDF weighting [30].

For the purpose of reproducibility, we shall make the datasets and code used
in our experiments publicly available at the first author’s homepage upon
paper publication.

###  4.2 Evaluation

Given a dataset, we use each document in the test set as a query to retrieve
documents in the training set within a specified Hamming distance, and then
compute standard retrieval performance measures: _precision_ , _recall_ , and
their harmonic mean ($F_{1}$ measure) [30].

$\displaystyle precision$ $\displaystyle=\frac{\text{the number of retrieved
relevant documents}}{\text{the number of all retrieved documents}}$ (6)
$\displaystyle recall$ $\displaystyle=\frac{\text{the number of retrieved
relevant documents}}{\text{the number of all relevant documents}}$ (7)

The reported performance scores in the following Section are averaged over all
test queries in the dataset.

To determine whether a retrieved document is “relevant” to the given query
document, we adopt the following two evaluation methodologies:

  1. 1.

retrieving original nearest neighbours — the $k$ most similar documents, i.e.,
nearest neighbours, in the original vector space are considered as the ground-
truth relevant documents ($k=25$ in our experiments);

  2. 2.

retrieving same-topic documents — the documents on the same topic, i.e., in
the same category, are considered as the ground-truth relevant documents.

The former methodology is used in [48]101010Actually only precision is used in
[48], which is appropriate for their application of pattern recognition but
obviously insufficient from the IR perspective. Due to this difference in
performance measurement, their results are not directly comparable with ours.,
while the latter methodology is used in [34]. In our opinion, these two
methodologies emphasise different aspects of semantic hashing, and thus are
suitable for different target IR applications. Therefore we use both of them
in this paper.

The absolute performance scores of STH are not as important as how they
compare with those of other semantic hashing techniques. As previously
mentioned in Section 1, if necessary, we can always spend a little extra time
to filter or re-rank the similarity search results based on their full
content, thus achieve higher performance scores [42].

###  4.3 Results

Figure 2 and Figure 3 show the $F_{1}$ measure of STH for retrieving original
nearest neighbours and same-topic documents respectively111111The $F_{1}$
measure scores reported here should not be directly compared with those in
text categorisation papers, as we are addressing a very different problem even
though the same datasets may have been used for experimentation.. We vary the
code length from 4-bit to 64-bit and also the Hamming ball radius (i.e., the
maximum Hamming distance between any retrieved document and the query
document) from 0 to 3, in order to show their influences on the retrieval
performance. It can be seen that when the code length increases, STH is able
to achieve a higher $F_{1}$ measure (using a bigger Hamming ball radius).
However, longer binary codes demand more memory and a bigger Hamming ball
radius requires more computation. The optimal trade-off between effectiveness
and efficiency can be found by using a validation set of query documents.

(a) Reuters21578

(b) 20Newsgroups

(c) TDT2

Figure 2: The $F_{1}$ measure of STH for retrieving original nearest
neighbours.

(a) Reuters21578

(b) 20Newsgroups

(c) TDT2

Figure 3: The $F_{1}$ measure of STH for retrieving same-topic documents.

Figure 4 and Figure 5 compare STH with several other typical semantic hashing
methods in terms of their _precision-recall curves_ (created by varying the
code length from 4-bit to 64-bit while fixing the Hamming ball radius at $1$),
for retrieving original nearest neighbours and same-topic documents
respectively121212Although we could achieve higher retrieval performance by
utilising a bigger Hamming ball radius (e.g., 4), a large number of binary
codes (e.g., $C_{64}^{4}=635376$ for 64-bit codes) would need to be checked
for each query and then the efficiency gain brought by semantic hashing would
diminish.. It is clear that on all datasets and under both evaluation
methodologies, STH outperforms binarised-LSI, LCH, and the state-of-the-art
technique SpH (that has already been shown to work much better than LSH [1],
stacked-RBM131313For example, on the 20Newsgroups dataset, stacked-RBM
achieves a maximum of $F_{1}=0.276$ for retrieving same-topic documents with
128-bit codes, while the same level of performance can be obtained using our
STH approach with just 8-bit codes. [34] and boosting-SSC [38]). Using 16-bit
codes and Hamming ball radius $1$, the performance improvements are all
statistically significant ($P$ value $<0.01$) according to one-sided micro
sign test ($s$-test) [49].

(a) Reuters21578

(b) 20Newsgroups

(c) TDT2

Figure 4: The precision-recall curve for retrieving original nearest
neighbours.

(a) Reuters21578

(b) 20Newsgroups

(c) TDT2

Figure 5: The precision-recall curve for retrieving same-topic documents.

We think the superior performance of STH is due to two reasons:

  * •

the binary codes produced by binarised-LapEig effectively preserve the
semantic similarity structure while maximising the entropy of the hash table;

  * •

the maximum-margin hyperplane produced by linear-SVM ensures high
generalisation ability [36].

We have also examined the approximation errors accumulated in each step of STH
(see Section 3.3). Our anatomy reveals that almost all approximation errors
come from the dimensionality reduction step using LapEig. However, LapEig does
work better than alternative methods (such as LSI) for this step in our
experiments, and it is a well-known hard problem to accurately detect the
(intrinsic) dimensionality of data or effectively reduce the dimensionality of
data. The median-based binarisation and SVM-based out-of-sample extension both
work perfectly incurring little approximation errors.

The proposed STH approach (using binarised-LapEig and linear-SVM) to semantic
hashing is pretty fast: on an ordinary PC with Intel Pentium4 3.00GHz CPU and
2GB RAM, our Matlab implementation of 64-bit STH takes approximately 0.0165
second per document for training (which is about 10 times faster than SpH),
and 0.0007 second per document for prediction.

##  5 Conclusions

The main contribution of this paper is a novel Self-Taught Hashing (STH)
approach to semantic hashing for fast similarity search. By decomposing the
problem of finding small codes for large data into two stages — unsupervised
learning and supervised learning — we achieve great flexibility in choosing
learning algorithms. Using binarised-LapEig for the first stage and linear-SVM
for the second stage, STH significantly outperforms binarised-LSI, LCH, and
the state-of-the-art technique SpH [48]. Since STH is a general learning
framework, it is promising to achieve even higher effectiveness and efficiency
if more powerful unsupervised or supervised learning algorithms can be
employed.

We shall apply this technique to text mining tasks (such as automated text
categorisation [37]) and content-based multimedia retrieval [28] in the near
future. It would also be interesting to combine semantic hashing and
distributed computing (e.g., [29]) to further improve the speed and
scalability of similarity search.

## Acknowledgements

We are grateful to Dr Xi Chen (Alberta) for his valuable discussion and the
London Mathematical Society (LMS) for their support of this work
(SC7-09/10-6). We would also like to thank the anonymous reviewers for their
helpful comments.

## References

  * [1] A. Andoni and P. Indyk.  Near-optimal hashing algorithms for approximate nearest neighbor in high dimensions.  In Proceedings of the 47th Annual IEEE Symposium on Foundations of Computer Science (FOCS), pages 459–468, Berkeley, CA, USA, 2006.
  * [2] S. Baluja and M. Covell.  Learning to hash: Forgiving hash functions and applications.  Data Mining and Knowledge Discovery (DMKD), 17(3):402–430, 2008\.
  * [3] M. Belkin and P. Niyogi.  Laplacian eigenmaps for dimensionality reduction and data representation.  Neural Computation, 15(6):1373–1396, 2003.
  * [4] S. Belongie, C. Fowlkes, F. Chung, and J. Malik.  Spectral partitioning with indefinite kernels using the nystrom extension.  In Proceedings of the 7th European Conference on Computer Vision (ECCV), pages 531–542, Copenhagen, Denmark, 2002.
  * [5] M. W. Berry, S. T. Dumais, and G. W. O’Brien.  Using linear algebra for intelligent information retrieval.  SIAM Review, 37(4):573–595, 1995.
  * [6] F. R. K. Chung.  Spectral Graph Theory.  American Mathematical Society, 1997.
  * [7] T. H. Cormen, C. E. Leiserson, R. L. Rivest, and C. Stein.  Introduction to Algorithms.  MIT Press and McGraw-Hill, 2nd edition, 2001.
  * [8] S. Deerwester, S. T. Dumais, G. W. Furnas, T. K. Landauer, and R. Harshman.  Indexing by latent semantic analysis.  Journal of the American Society of Information Science (JASIS), 41(6):391–407, 1990.
  * [9] P. Drineas and M. W. Mahoney.  On the nystrom method for approximating a gram matrix for improved kernel-based learning.  Journal of Machine Learning Research (JMLR), 6:2153–2175, 2005\.
  * [10] S. Dumais, J. Platt, D. Heckerman, and M. Sahami.  Inductive learning algorithms and representations for text categorization.  In Proceedings of the 7th ACM International Conference on Information and Knowledge Management (CIKM), pages 148–155, Bethesda, MD, 1998\.
  * [11] R.-E. Fan, K.-W. Chang, C.-J. Hsieh, X.-R. Wang, and C.-J. Lin.  LIBLINEAR: A library for large linear classification.  Journal of Machine Learning Research, 9:1871–1874, 2008.
  * [12] G. H. Golub and C. F. V. Loan.  Matrix Computations.  The Johns Hopkins University Press, 3rd edition, 1996.
  * [13] L. W. Hagen and A. B. Kahng.  New spectral methods for ratio cut partitioning and clustering.  IEEE Transactions on CAD of Integrated Circuits and Systems, 11(9):1074–1085, 1992.
  * [14] A. Y. Halevy, P. Norvig, and F. Pereira.  The unreasonable effectiveness of data.  IEEE Intelligent Systems, 24(2):8–12, 2009.
  * [15] J. Hays and A. A. Efros.  Scene completion using millions of photographs.  ACM Transactions on Graphics (TOG), 26(3):4, 2007.
  * [16] X. He, D. Cai, H. Liu, and W.-Y. Ma.  Locality preserving indexing for document representation.  In Proceedings of the 27th Annual International ACM SIGIR Conference on Research and Development in Information Retrieval (SIGIR), pages 96–103, Sheffield, UK, 2004.
  * [17] X. He and P. Niyogi.  Locality preserving projections.  In Advances in Neural Information Processing Systems (NIPS), volume 16, pages 153–160, Vancouver and Whistler, Canada, 2003.
  * [18] M. R. Henzinger.  Finding near-duplicate web pages: A large-scale evaluation of algorithms.  In Proceedings of the 29th Annual International ACM SIGIR Conference on Research and Development in Information Retrieval (SIGIR), pages 284–291, Seattle, WA, USA, 2006.
  * [19] G. Hinton, S. Osindero, and Y. W. Teh.  A fast learning algorithm for deep belief nets.  Neural Computation, 18(7):1527–1554, 2006.
  * [20] G. Hinton and R. Salakhutdinov.  Reducing the dimensionality of data with neural networks.  Science, 313(5786):504–507, July 2006.
  * [21] C.-J. Hsieh, K.-W. Chang, C.-J. Lin, S. S. Keerthi, and S. Sundararajan.  A dual coordinate descent method for large-scale linear svm.  In Proceedings of the 25th International Conference on Machine Learning (ICML), pages 408–415, Helsinki, Finland, 2008.
  * [22] T. Joachims.  Text categorization with support vector machines: Learning with many relevant features.  In Proceedings of the 10th European Conference on Machine Learning (ECML), pages 137–142, Chemnitz, Germany, 1998.
  * [23] T. Joachims.  Learning to Classify Text using Support Vector Machines.  Kluwer, 2002.
  * [24] T. Joachims.  Training linear SVMs in linear time.  In Proceedings of the 12th ACM SIGKDD International Conference on Knowledge Discovery and Data Mining (KDD), pages 217–226, Philadelphia, PA, 2006.
  * [25] D. Knuth.  The Art of Computer Programming.  Addison-Wesley, 3rd edition, 1997.
  * [26] Y. Koren.  Factorization meets the neighborhood: a multifaceted collaborative filtering model.  In Proceedings of the 14th ACM SIGKDD International Conference on Knowledge Discovery and Data Mining (KDD), pages 426–434, Las Vegas, NV, USA, 2008.
  * [27] K. Lang.  Newsweeder: Learning to filter netnews.  In Proceedings of the 12th International Conference on Machine Learning (ICML), pages 331–339, Tahoe City, CA, 1995.
  * [28] M. S. Lew, N. Sebe, C. Djeraba, and R. Jain.  Content-based multimedia information retrieval: State of the art and challenges.  ACM Transactions on Multimedia Computing, Communications, and Applications (TOMCCAP), 2(1):1–19, 2006.
  * [29] J. Lin.  Brute force and indexed approaches to pairwise document similarity comparisons with mapreduce.  In Proceedings of the 32nd Annual International ACM SIGIR Conference on Research and Development in Information Retrieval (SIGIR), pages 155–162, Boston, MA, USA, 2009.
  * [30] C. D. Manning, P. Raghavan, and H. Schütze.  Introduction to Information Retrieval.  Cambridge University Press, 2008.
  * [31] T. Mitchell.  Machine Learning.  McGraw Hill, international edition, 1997.
  * [32] S. Pandey, A. Broder, F. Chierichetti, V. Josifovski, R. Kumar, and S. Vassilvitskii.  Nearest-neighbor caching for content-match applications.  In Proceedings of the 18th International Conference on World Wide Web (WWW), pages 441–450, Madrid, Spain, 2009.
  * [33] R. Raina, A. Battle, H. Lee, B. Packer, and A. Y. Ng.  Self-taught learning: Transfer learning from unlabeled data.  In Proceedings of the 24th International Conference on Machine Learning (ICML), pages 759–766, Corvalis, OR, USA, 2007.
  * [34] R. Salakhutdinov and G. Hinton.  Semantic hashing.  International Journal of Approximate Reasoning (IJAR), 50(7):969–978, 2009.
  * [35] R. E. Schapire.  The boosting approach to machine learning: An overview.  In Nonlinear Estimation and Classification. Springer, 2003.
  * [36] B. Scholkopf and A. J. Smola.  Learning with Kernels.  MIT Press, Cambridge, MA, 2002.
  * [37] F. Sebastiani.  Machine learning in automated text categorization.  ACM Computing Surveys, 34(1):1–47, 2002.
  * [38] G. Shakhnarovich, P. A. Viola, and T. Darrell.  Fast pose estimation with parameter-sensitive hashing.  In Proceedings of the 9th IEEE International Conference on Computer Vision (ICCV), pages 750–759, Nice, France, 2003.
  * [39] C. E. Shannon.  A mathematical theory of communication.  Bell System Technical Journal, 27:379–423, 623–656, 1948.
  * [40] J. Shi and J. Malik.  Normalized cuts and image segmentation.  IEEE Transactions on Pattern Analysis and Machine Intelligence (TPAMI), 22(8):888–905, 2000.
  * [41] Q. Shi, J. Petterson, G. Dror, J. Langford, A. Smola, and S. Vishwanathan.  Hash kernels for structured data.  Journal of Machine Learning Research (JMLR), 10:2615–2637, 2009\.
  * [42] B. Stein.  Principles of hash-based text retrieval.  In Proceedings of the 30th Annual International ACM SIGIR Conference on Research and Development in Information Retrieval (SIGIR), pages 527–534, Amsterdam, The Netherlands, 2007.
  * [43] B. Stein, S. M. zu Eissen, and M. Potthast.  Strategies for retrieving plagiarized documents.  In Proceedings of the 30th Annual International ACM SIGIR Conference on Research and Development in Information Retrieval (SIGIR), pages 825–826, Amsterdam, The Netherlands, 2007.
  * [44] A. B. Torralba, R. Fergus, and Y. Weiss.  Small codes and large image databases for recognition.  In Proceedings of the IEEE Computer Society Conference on Computer Vision and Pattern Recognition (CVPR), pages 1–8, Anchorage, AK, USA, 2008.
  * [45] R. Weber, H.-J. Schek, and S. Blott.  A quantitative analysis and performance study for similarity-search methods in high-dimensional spaces.  In Proceedings of 24th International Conference on Very Large Data Bases (VLDB), pages 194–205, New York City, USA, 1998.
  * [46] P. Wegner.  A technique for counting ones in a binary computer.  Communications of the ACM (CACM), 3(5):322, 1960.
  * [47] K. Q. Weinberger, A. Dasgupta, J. Langford, A. J. Smola, and J. Attenberg.  Feature hashing for large scale multitask learning.  In Proceedings of the 26th Annual International Conference on Machine Learning (ICML), page 140, Montreal, Quebec, Canada, 2009.
  * [48] Y. Weiss, A. B. Torralba, and R. Fergus.  Spectral hashing.  In Advances in Neural Information Processing Systems (NIPS), volume 21, pages 1753–1760, Vancouver, Canada, 2008.
  * [49] Y. Yang and X. Liu.  A re-examination of text categorization methods.  In Proceedings of the 22nd Annual International ACM SIGIR Conference on Research and Development in Information Retrieval (SIGIR), pages 42–49, Berkeley, CA, 1999.
  * [50] D. Zhang, J. Wang, D. Cai, and J. Lu.  Laplacian co-hashing of terms and documents.  In Proceedings of the 32nd European Conference on IR Research (ECIR), page 577–580, Milton Keynes, UK, 2010.