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?

  • $\begingroup$ @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. $\endgroup$ Jan 29, 2014 at 19:40
  • $\begingroup$ My instinct tells me that PA is stronger. $\endgroup$ Jan 30, 2014 at 9:43

2 Answers 2


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.

  • $\begingroup$ But what if you stick to total functions? $\endgroup$ Jan 29, 2014 at 19:38
  • 1
    $\begingroup$ The question is about total functions. $\endgroup$ Jan 30, 2014 at 9:43

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.