I don't understand the formal side of things, but I've used Y before, so here goes: In the lambda calculus, functions are nameless. Recursion is when an expre

I don't understand the formal side of things, but I've used Y before, so here goes: In the lambda calculus, functions are nameless. Recursion is when an expression refers to itself by name. The Y combinator gives you recursion despite the contradiction in my last two sentences. > So what is the fixed point of f(x) = x + 1? We don't have names, so what is the fixed point of (λx. x + 1)? Introduce a new variable into the expression's body to act as the expression's name, and also include it as the first parameter: (λf x. x + 1) (Your function did not refer to itself which is why there's no f in the body of the above expression). Now let's take the ingredients and put them together. I'm including an 'input' so that we can converge on an output: Y = (λg. (λh. g (h h)) (λh. g (h h))) fixf = (λf x. x + 1) input = 3 Y fixf input = (λg. (λh. g (h h)) (λh. g (h h))) (λf x. x + 1) 3 Now we just apply those lambdas to their terms and see what we end up with: (λg. (λh. g (h h)) (λh. g (h h))) (λf x. x + 1) 3 ^ | g | (λh. (λf x. x + 1) (h h)) (λh. (λf x. x + 1) (h h)) 3 ^ | h | (λf x. x + 1) ((λh. (λf x. x + 1) (h h)) (λh. (λf x. x + 1) (h h))) 3 ^ | f | (λx. x + 1) 3 ^ |x| 4