6
$\begingroup$

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?

$\endgroup$
  • $\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$ – Gilles 'SO- stop being evil' Jan 29 '14 at 19:40
  • $\begingroup$ My instinct tells me that PA is stronger. $\endgroup$ – Andrej Bauer Jan 30 '14 at 9:43
3
$\begingroup$

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).

$\endgroup$
0
$\begingroup$

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.

$\endgroup$
  • $\begingroup$ But what if you stick to total functions? $\endgroup$ – Gilles 'SO- stop being evil' Jan 29 '14 at 19:38
  • 1
    $\begingroup$ The question is about total functions. $\endgroup$ – Andrej Bauer Jan 30 '14 at 9:43

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

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