5
$\begingroup$

Can someone give a clear and simple answer for why the fixed point theorem holds for every $\lambda$-term, in contrast with the fact that not all numerical function have a fixed point?

$\endgroup$
  • $\begingroup$ Very simply: $\lambda$-terms are not the same as numerical functions. $\endgroup$ – Zhen Lin Jan 6 '15 at 13:48
  • $\begingroup$ In my current (non-)understanding, I would rather reverse the question: How can you apply the fixed point theorem for $\lambda$-terms to numerical functions? I asked this in cstheory.stackexchange.com/questions/27322/… but don't know the answer yet. $\endgroup$ – Hanno Jan 6 '15 at 13:48
  • 1
    $\begingroup$ One might say that every numerical function has a fixed point, but the fixed point might not be a number. For example, there is a family of lambda terms that model the natural numbers, and a lambda term $S$ that models the numerical function $x\mapsto x+1$, and $S$ has a fixed point, but the fixed point of $S$ is not one of the terms that models a number. $\endgroup$ – MJD Jan 6 '15 at 14:27
  • $\begingroup$ @MJD function x↦x+1 has the fixed point in λ-calculs not in arithmetic. and my question is about reason the existence of fixed point in λ-calculs. $\endgroup$ – user140092 Jan 6 '15 at 14:43
0
$\begingroup$

As was noted by others lambda terms are more general than numerical functions so you are able to draw answer(fixed point) from different set. While for numerical function e.g. $f: \mathbb{R} \rightarrow \mathbb{R}$ your fixed point must belong to $\mathbb{R}$. On contrary lambda terms reduces to other lambda terms some of them can designate numbers from $\mathbb{R}$ some of them do not designate the numbers.

For more rigorous explanations you should read some proofs of fixed point theorem for lambda calculus.

$\endgroup$
0
$\begingroup$

Numerical functions typically accept only numbers as arguments, whereas lambda-terms can accept other lambda-terms.

For your example, $\lambda x.x+1$, the following is a fixed point:

$$ Y(\lambda x.x+1)$$

where $Y$ is Turing's Y-combinator: $Y=UU$ and $U=\lambda ux.x(uux)$

This is a fixed point because:

$Y(\lambda x.x+1) = UU(\lambda x.x+1) = (\lambda ux.x(uux))U(\lambda x.x+1) = (\lambda x.x+1)(UU(\lambda x.x+1)) = (\lambda x.x+1)(Y(\lambda x.x+1))$

(using '=' loosely for congruence or $\beta$-reduction)

We have shown $(\lambda x.x+1)(Y(\lambda x.x+1))$ is $\beta$-equivalent to $Y(\lambda x.x+1)$, meaning that $Y(\lambda x.x+1)$ is a fixed point of $\lambda x.x+1$

Turing's Y-combinator will actually find a fixed point for any lambda-term $X$. That is, following the steps above but generalizing the example $\lambda x.x+1$ to any $X$, we get $X(YX)=_\beta YX$, so $YX$ is a fixed point of $X$. This is essentially the proof of the fixed point theorem.

$Y(\lambda x.x+1)$ is a lambda-term, so it's not a numerical fixed point of $x \rightarrow x+1$

$\endgroup$

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.