Introduction

In the pure $\lambda$-calculus, conversion $=_\beta$ is not extensional, in the sense that it does not satisfy the property

$$ \tag{ext} \label{eq:ext} \infer{MP = NP\quad\text{for every $P\in\Lambda$}}{M = N} $$

Example. Take $M=y$ and $N=(\lambda x.yx)$, for some $y\in\mathcal{V}$ variable. Then $MP = yP =_\beta (\lambda x.yx)P = NP$ but $M\not=_\beta N$.

Instead of directly adding $\eqref{eq:ext}$ to $=_\beta$ to make it extensional, there are two other well-known rules that, when added to $=_\beta$, also make it extensional, namely the $\zeta$ and $\eta$ rules:

$$ \tag{$\zeta$} \label{eq:zeta} \infer{Mx = Nx\quad\text{$x\not\in\FV(MN)$}}{M = N} $$

$$ \tag{$\eta$} \label{eq:eta} \infer{x\not\in\FV(MN)}{M = (\lambda x. Mx)} $$

The $\beta\eta$ and $\beta\zeta$ conversions

Let $=_\betaext$, $=_\betazeta$ and $=_\betaeta$ be the conversions induced by the rule $\beta$ together with, respectively, $\eqref{eq:ext}$, $\eqref{eq:zeta}$, and $\eqref{eq:eta}$. To be clear, given a relation $R\subseteq\Lambda\times\Lambda$, its induced conversion $=_{R}\subseteq\Lambda\times\Lambda$ is the smallest relation satisfying, for all $M,N,P\in\Lambda$ and $x\in\mathcal{V}$:

$$ \tag{$R$} \infer{M~R~N}{M=_RN} $$

$$ \tag{$\mu$}\label{eq:mu} \infer{M=_RN}{PM=_RPN} $$

$$ \tag{$\nu$}\label{eq:nu} \infer{M=_RN}{MP=_RNP}
$$

$$ \tag{$\xi$}\label{eq:xi} \infer{M=_RN}{\lambda x. M =_R \lambda x.N} $$

$$ \tag{$\rho$}\label{eq:rho} {M=_RM} $$

$$ \tag{$\sigma$}\label{eq:sigma} \infer{M=_RN}{N=_RM} $$

$$ \tag{$\tau$}\label{eq:tau} \infer{M=_RN\quad N=_RP}{M=_RP} $$

In other words, $=_R$ is the least compatible (cf. $\ref{eq:mu}$, $\ref{eq:nu}$, $\ref{eq:xi}$) equivalence relation (cf. $\ref{eq:rho}$, $\ref{eq:sigma}$, $\ref{eq:tau}$) containing $R$.

Proposition. $M=_\betaext N \iff M=_\betazeta N$.

Proof. By double implication.

• $\implies$ By induction on the definition of $M=_\betaext N$. Only one interesting case.

  • Case $\eqref{eq:ext}$. By hypothesis, $MP=_\betazeta NP$ for every $P\in\Lambda$. In particular, $Mx =_\betazeta Nx$ for all $x\not\in\FV(MN)$. Therefore, by $\eqref{eq:zeta}$, $M=_\betazeta N$.

• $\impliedby$ By induction on the definition of $M=_\betazeta N$. Only one interesting case.

  • Case $\eqref{eq:zeta}$. By hypothesis, $Mx=_{\betaext} Nx$ and $x\not\in\FV(MN)$. By $\eqref{eq:xi}$, $(\lambda x. Mx)=_{\betaext}(\lambda x. Nx)$. By $\eqref{eq:nu}$, with arbitrary $P\in\Lambda$, $(\lambda x.Mx)P=_{\betaext}(\lambda x. Nx)P$. By $\beta$, together with $x\not\in\FV(MN)$, $MP=_{\betaext}NP$. Therefore, by $\eqref{eq:ext}$, $M =_{\betaext} N$.

Proposition. $M=_{\beta\zeta}N \iff M=_{\beta\eta}N$.

Proof. By double implication.

• $\implies$ By induction on the definition of $M=_{\beta\zeta}N$. Only one interesting case.

  • Case $\eqref{eq:zeta}$. By hypothesis, $Mx =_{\beta\eta} Nx$ and $x\not\in\FV(MN)$. By $\eqref{eq:xi}$, $(\lambda x. Mx) =_{\beta\eta} (\lambda x. Nx)$. By $\eqref{eq:eta}$, together with $x\not\in\FV(MN)$, $(\lambda x. Mx) =_{\beta\eta} M$ and $(\lambda x. Nx) = _{\beta\eta} N$. By $\eqref{eq:tau}$, twice, $M=_{\beta\eta}N$.

• $\impliedby$ By induction on the definition of $M=_{\beta\eta}N$. Only one interesting case.

  • Case $\eqref{eq:eta}$. By hypothesis, $x\not\in\FV(M)$. By $\beta$, $Mx=_{\beta\zeta}(\lambda x. Mx)x$. By $\eqref{eq:zeta}$, together with $x\not\in\FV(\lambda x.Mx)$ and $x\not\in\FV(M)$, $M=_{\beta\zeta}(\lambda x. Mx)$.

Theorem. Conversions $=_{\beta\zeta}$ and $=_{\beta\eta}$ are (equivalent) extensional variants of $=_{\beta}$.

A curiosity: $\zeta$ implies $\xi$

The $\beta\zeta-\xi$ conversion

In the presence of $\eqref{eq:zeta}$, rule $\eqref{eq:xi}$ is no longer needed. More precisely, let $=_{\beta\zeta-\xi}$ be the conversion induced by $\beta$ whilst replacing $\eqref{eq:xi}$ for $\eqref{eq:zeta}$.

Proposition. $M =_{\beta\zeta-\xi} N \iff M =_{\beta\zeta}N$.

Proof. By double implication.

• $\implies$ By induction on the definition of $M=_{\beta\zeta-\xi} N$. Routine.

• $\impliedby$ By induction on the definition of $M=_{\beta\zeta} N$. Only one interesting case.

  • Case $\eqref{eq:xi}$. By hypothesis, $M=_{\beta\zeta-\xi} N$. Let $x\in\mathcal{V}$. By $\beta$, together with lemma «$M[x:=x] = M$ for all $M$ and $x$», $M =_{\beta\zeta-\xi} (\lambda x. M)x$ and $N =_{\beta\zeta-\xi} (\lambda x. N)x$. By $\eqref{eq:tau}$, twice, $(\lambda x.M)x =_{\beta\zeta-\xi} (\lambda x. N)x$. By $\eqref{eq:zeta}$, together with $x\not\in\FV(\lambda x. M)\cup\FV(\lambda x.N)$, $\lambda x.M =_{\beta\zeta-\xi} \lambda x.N$.

References

• Lambda-Calculus and Combinators: An Introduction. (Hindley, J. Roger and Jonathan P. Seldin; 2008).