Search code examples
lambda-calculuschurch-encoding

can't deduce the numeral representation (church encoding) of a lambda expression λx.λy.x(xy)


I have a lambda expression: λx.λy.x(xy), and I'm supposed to infer the integer representation of it. I've read a lot about Church encodings and Church numerals specifically but I can't find what number is. Can you explain it to me in a way a 3 year old can understand or refer me to a resource better than wikipedia?


Solution

  • Church encoding of integers is the following:

    • "0" ≡ (λf.(λx.x)): Think of (λf.(λx.x)) as meaning: given a function f and an element x, the result is x: it's like applying the function f zero times to x.
    • "1" ≡ (λf.(λx.(fx))): Think of (λf.(λx.(fx))) as meaning: given a function f and an element x, the result is (fx): which should be thought of as apply f to x or, in more standard mathematical notation, like f(x).
    • "2" ≡ (λf.(λx.(f(fx)))): Think of (λf.(λx.(f(fx)))) as meaning: given a function f and an element x, the result is (f(fx)): which should be thought of as apply f to x twice or, in more standard mathematical notation, like f(f(x)).
    • "3" ≡ (λf.(λx.(f(f(fx))))): Think of (λf.(λx.(f(f(fx))))) as meaning: given a function f and an element x, the result is (f(f(fx))): which should be thought of as apply f to x three times or, in more standard mathematical notation, like f(f(f(x))).

    I hope that you see the pattern (and the logic behind). In your case, (λx.(λy.(x(xy)))) is the Church encoding of the number 2 (using alpha-equivalence, of course).

    The wikiped article is actually quite clear. What is it that you don't understand?