I have a definition of the natural numbers in lambda calculus as follow, which was my main goal.
-- Apply a function n times on x
apply = \f -> \n -> \x -> foldr ($) x $ replicate n f
-- Church numbers
churchZero = \f -> id
churchOne = \f -> \x -> apply f 1 x
churchTwo = \f -> \x -> apply f 2 x
churchNatural = \n -> \f -> \x -> apply f n x
Then, the next step was defining the operators churchSum
, churchMul
and churchExp
.
churchSum = \n -> \m -> \f -> \x -> n f (m f x)
churchMul = \n -> \m -> \f -> \x -> n (m f) x
churchExp = \n -> \m -> n m
Fine, it works, the first two functions are "easy" to deduce, but the exponentiation is not. For me at least. To understand a little bit more, i did the beta normalization on the lambda term:
(λf.λx. f(f x))(λf.λx f(f x))
to see that effectively the exponentiation is correct.
So, my question is: how could i deduce this lambda term for the exponentiation without known it? Even more, why something like λ> churchTwo churchTwo
type checks on Haskell
when the types are λ> churchTwo :: (b -> b) -> b -> b
? Inside it do the beta normalization of the function?
Your
exp
is a bit backwards:The correct(-er-ish) version would be
because it maintains the familiar order. This doesn't really affect how you might go around defining
exp
.Exponentation is repeated multiplication:
nm
isn
multiplied by itselfm
times. Church numerals represent repeated application of a function to a value. So,churchMul n
is a function that multiplies a numeral byn
,m
is function that repeats a functionm
times, andchurchOne
is the base value (identity of multiplication). Put them together, then simplify:The above stuff with the free theorem of
m
is really a rigorous version of the following argument (which probably translates better to the untyped lambda calculus):As for why
churchTwo churchTwo
typechecks, note each occurrence in that expression has a different type, becausechurchTwo
is polymorphic and describes an entire family of functions instead of just one.