# How strong is equivalence of lambda expressions?

Consider two lambda expressions $\mu$, $\nu$ representing computable functions $f_{\mu,\nu}:\mathbb{N} \rightarrow \mathbb{N}$. If $\mu$ and $\nu$ are equivalent under the combination of $\beta$-reductions, $\alpha$-conversions and $\eta$-conversions then $f_\mu=f_\nu$.

Under what conditions does the converse hold? In particular, if it is possible to prove in Peano arithmetic that $f_\mu=f_\nu$, does it follow $\mu$, $\nu$ are equivalent in the above sense?

• @Raphael Now you know how I feel about complexity theory questions! This thread has part of the answer: you need to stick to total functions, and a corresponding result holds in the lambda calculus (intuitively, the $\eta$ rule captures extensionality). I need to think about translating it to Peano arithmetic; such results do not hold in just any logic. Jan 29 '14 at 19:40
• My instinct tells me that PA is stronger. Jan 30 '14 at 9:43

In general, there is always an infinite number of "computationally different" functions that are extensionally equal: take for instance the "$3n+1$-function" $g$, and for any function $f$ define $G_f$ to be:

$$G_f(n)=\begin{cases} f(n) & \mbox{if }g(n)\mbox{ cycles at }1 \\ 0 & \mbox{otherwise}\end{cases}$$

This function is (probably) extensionally equal to $f$ for every $f$, but this is (possibly) not provable in $\mathrm{PA}$, or indeed in the weak framework of $\beta\eta\alpha$-conversion.

More pragmatically, the identity function $\lambda x.x$ and the "stupid identity" $$\lambda n.n\ (\lambda x\ f.x)\ (\lambda m\ x\ f.f(m\ x \ f))$$

Denote the same function $\mathrm{id}:\mathbb{N}\rightarrow \mathbb{N}$, under the usual church encoding, but are not $\beta\eta$-equal, as can easily be seen (they are both in normal form).

It is false, because of lot of different lambda terms (not reducible to each other) define the same partial function $\mathbb N\to\mathbb N$ with empty domain.

• But what if you stick to total functions? Jan 29 '14 at 19:38
• The question is about total functions. Jan 30 '14 at 9:43