CODEWITHSUNDEEP
lambda-calculuschurch-encoding
matos416
matos416

Reputation: 85

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?

Upvotes: 3

Views: 168

Answers (1)

gniourf_gniourf
gniourf_gniourf

Reputation: 46853

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?

Upvotes: 2

Related Questions