4
$\begingroup$

In lambda calculus the fixed point combinator is defined as: $$Y=\lambda f \cdot(\lambda x \cdot f(x x))(\lambda x \cdot f(x x))$$

It is very easy to see how $Yg =g(Yg)$ for any $g$ by using $\beta$-reduction.

At the same time I wonder what is the meaning of $Yg$ when $g=\lambda x.x+1$, a fuction without fixed point. I need somebody to explain me that please.

I know that the fixed point combinator is related to the Curry paradox which proves that the lambda calculus as a deductive system is inconsistent. Does this inconsistency has to do with the case I wrote above?

$\endgroup$

4 Answers 4

8
$\begingroup$

The pure lambda calculus does not have an inbuilt notion of $+$ or $1$. There are various encodings of the natural numbers (and arithmetic) into the lambda calculus though. For example, the Church encoding. In these cases, the arithmetic operations work well on those lambda terms which denote natural numbers, but on the rest of the lambda terms they need not behave in nice ways.

In your case, if $N$ denotes the natural number $n$ in the coding method you have chosen, then $gN$ will reduce to the code of $n+1$ (here I`ve assumed that $g$ is the encoding of the function which sends $x$ to $x+1$ into the lambda calculus). On the other hand, if $M$ is some lambda term which doesn´t denote any natural number in your encoding, then $gM$ could potentially reduce to all sorts of strange things. In particular, $g$ does have fixed points, but these fixed points cannot denote natural numbers in your encoding.

$\endgroup$
3
  • $\begingroup$ so we can say that the lambda expression in Church encoding of $\lambda x.x+1$ has a fixed point when interpreted as a functional but not as a recursive function? $\endgroup$
    – holmes
    Commented Sep 17, 2014 at 21:50
  • $\begingroup$ I´m not sure I understand what you mean when you use ´functional` and ´recursive function`. In the pure (=untyped) lambda calculus, every single function has a fixed point. For example, using any fixed point combinator. But if you look at $g$ as a function that takes (encodings of) natural numbers to (encodings of) natural numbers, then it does not have a fixed point, because $+$ and $1$ behave as we expect them to (otherwise it wouldn´t be a very nice encoding of arithmetic!). $\endgroup$
    – user7835
    Commented Sep 17, 2014 at 22:49
  • $\begingroup$ Thanks, your answer is very clear. What I meant in my comment (using a bit of a confusing terminology) is that the fixed point of the lambda expression for λx.x+1 is not a value (a number, an integer as you stated clearly) but a function. Actually I can see a connection with the Kleene's recursion theorem which states that for every total recursive function $F$ there is an element $x_0$ such that $x_0$ and $F(x_0)$ are indexes of two recursive functions which are equivalent (i.e. they have the same output on the same input). $\endgroup$
    – holmes
    Commented Sep 18, 2014 at 13:00
4
$\begingroup$

I assuming that you're asking about the untyped lambda calculus. There every term $f$ has a fixed point, for example $Yf$. But only some terms have normal forms. This means that (using Church numberals to represent numbers) applying $Y$ to the successor function $Y\mbox{succ}$ is a valid term, a fixed point of succ, but $Y\mbox{succ}$ has no normal form that would correspond to a result.

In some typed lambda calculi such as System F all terms have normal form (such systems are called normalizing). And for example in System F it can be show that all values of type $\forall\alpha.\alpha\rightarrow(\alpha\rightarrow\alpha)\rightarrow\alpha$ correspond to a natural number. But in a normalizing system you can't have a fixed point combinator such as $Y$ that would allow arbitrary recursion.

$\endgroup$
2
$\begingroup$

This brilliant.org article on Lambda Calculus argues that applying the $Y$-combinator to the successor function, $S$, has the following effect:

Notice that applying the $Y$-combinator to $S$ does not yield a church numeral in any finite number of $\beta$ or $\eta$ reductions. Instead, we get something like this:

$S(S(S(S…)))$

One could think of it as an undefined value $\bot$ or infinity, in either of which cases a fixed-point is understandable.

$\endgroup$
1
  • $\begingroup$ In my opinion this is the best answer. $\endgroup$
    – MJD
    Commented Jan 12 at 22:19
2
$\begingroup$

The fixed point combinator you wrote down only makes sense in untyped lambda calculus. In the untyped lambda calculus every function you write down has to be able to take every other function in the untyped lambda calculus as input. The function you wrote down cannot be written down in typed lambda calculus, since it doesn't make sense for arbitrary functions but only for, say, integers.

$\endgroup$
0

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .