Search code examples
lambdafunctional-programmingsicp

lambda calculus - if more parameters needed

Lambda Calculus Question:

TRUE = lambda x y . x
FALSE = lambda x y . y
1 = lambda s z . s z
2 = lambda s z . s (s z) ...

BoolAnd = lambda x y . x y FALSE
BoolOr = lambda x y. x TRUE y
BoolNot = lambda x . x FALSE TRUE 

If I want to know the result of BoolNot 1:
BoolNot 1
(lambda x . x FALSE TRUE)(lambda s z . s (s z))
(lambda s z . s z) FALSE TRUE
(lambda x y . y) (lambda x y . x)

Here needs x and y 2 parameters, but only have 1 here, How can I continue this calculus?

Solution

  • λ x y. E is "shorthand" for λx. (λy. E).

    Thus,

    (λ x y. y) (λ x y. x)

==> (λx. (λy. y)) (λ x y. x)

==> λy. y

    That is, the identity function.