Fixed point combinator and functions with no fixed point

Question

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?

Answer 1

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.

Answer 2

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.

Answer 3

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 untyped lambda calculus, since it doesn't make sense for arbitrary functions but only for, say, integers.

Answer 4

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.