I have a question about the church figures and the successor function.
I think I understand the basics of beta reduction and that I can implement church figures (somehow)
So, it defines a general encoding of a value n as
n = 𝜆f.𝜆x.f^n x
^ n is f raised to n, I do not know how to format by exponent / index here …
0 = 𝜆f.𝜆x.x 1 = 𝜆f.𝜆x.fx 2 = 𝜆f.𝜆x.f(fx)
What I get as a number is just an account of the encapsulation of a function
f more than
He then defines
SUC as a way to add 1 to
SUC = 𝜆n.𝜆f.𝜆x.nf(fx)
SUC_n = (𝜆n.𝜆f.𝜆x.nf(fx))(𝜆f.𝜆x.f^n x) (n := (𝜆f.𝜆x.f^n x)) = 𝜆f.𝜆x.(𝜆f.𝜆x.f^n x)f(fx) (f := f) = 𝜆f.𝜆x.(𝜆x.f^n x)(fx) (x := (fx)) = 𝜆f.𝜆x.f^n(fx) = 𝜆f.𝜆x.f^(n+1)x This step I get, we are increasing n as an encapsulation of f over x = n + 1 There is step here I don't get. How are we losing f^(n+1)x to get just n+1
So, my question is. This last step, how are you
𝜆f.𝜆x.f^(n+1)x for just
Is it a beta reduction that I do not understand / miss here?