4 ms·

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 f

• bmacho 3y ago
  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.
• nightlyherb 3y ago
  Using church numerals[1], right_incr(n) = g => y => n(g)(g(y)) and using the following shorter fixed-point combinator[2], X(f) = ( a => a(a) )( x => f(x(x)) ) I get this junk: 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))) = ... Which, as you can see, only gets more complex when I try to transform it. [1] https://en.m.wikipedia.org/wiki/Church_encoding https://en.m.wikipedia.org/wiki/Church_encoding [2] https://en.m.wikipedia.org/wiki/Fixed-point_combinator#Other_fixed-point_combinators https://en.m.wikipedia.org/wiki/Fixed-point_combinator#Other...