What would be the fixed point of f(x) = x + 1 in the classical untyped lambda calculus?
Sorry if this question is really basic, but it's honest and I find it fascinating.
Using church numerals[1],
right_incr(n) =
g => y => n(g)(g(y))
X(f) =
( a => a(a) )( x => f(x(x)) )
X(right_incr)
= ( a => a(a) )( x => g => y => x(x)(g)(g(y)) )
= ( x => g => y => x(x)(g)(g(y)) ) ( x => g => y => x(x)(g)(g(y)) )
X(right_incr)(g)(y)
= let f = ( x => g => y => x(x)(g)(g(y)) )
in f(f)(g)(y)
= let .. in f(f)(g)(g(y))
= let .. in f(f)(g)(g(g(y)))
= ...
[1] https://en.m.wikipedia.org/wiki/Church_encoding [2] https://en.m.wikipedia.org/wiki/Fixed-point_combinator#Other...
I think in untyped lambda calculus you work with expressions, so you take your f function (somehow represented as an expression in untyped lambda calculus), you put that in a fixed point combinator, and the resulting expression is a fixed point of your f function.
It most certainly won't be a representation of a number->number function, but a general element of untyped lambda calculus nevertheless.
It is somehow similar how you take square root of a negative number on the Complex plane. You represent your negative number as a complex number (r \mapsto r + 0i), then you can take a square root of it, but that won't correspond to a representation of a real number.
In a generic context a fixed point combinator will only return a fixed point of a function if one exists.
2. No. (see: 1. above)
Your confusion stems from the usual domain of application to function spaces where every function has a fixed point (ie. not all function spaces, just those that are made up of functions with at least one fixed point).
From the link above: