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?
can't deduce the numeral representation (church encoding) of a lambda expression λx.λy.x(xy)
172 Views Asked by matos416 At
1
Church encoding of integers is the following:
"0" ≡ (λf.(λx.x))
: Think of(λf.(λx.x))
as meaning: given a functionf
and an elementx
, the result isx
: it's like applying the functionf
zero times tox
."1" ≡ (λf.(λx.(fx)))
: Think of(λf.(λx.(fx)))
as meaning: given a functionf
and an elementx
, the result is(fx)
: which should be thought of as applyf
tox
or, in more standard mathematical notation, like f(x)."2" ≡ (λf.(λx.(f(fx))))
: Think of(λf.(λx.(f(fx))))
as meaning: given a functionf
and an elementx
, the result is(f(fx))
: which should be thought of as applyf
tox
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 functionf
and an elementx
, the result is(f(f(fx)))
: which should be thought of as applyf
tox
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 number2
(using alpha-equivalence, of course).The wikiped article is actually quite clear. What is it that you don't understand?