lambda.org 3.4 KB
Lambda
Encoding booleans in lambda calculus
Booleans can be seen as making a choice between 2 alternatives. Imagine an if~
expression in any programming language. If checks a condition, which results in
a boolean and depending on that boolean, it makes a choice between the things to
do, if the boolean is ~true and the alternative things to do, if the boolean is
~false~. So in principle all the boolean needs to do is allowing to make a
choice between 2 alternatives.
If booleans have this property, then it will be possible to design other boolean
functions like not on top of them. As long as they return true or ~false~
again, they create a perfect abstraction layer on top of the representation of
booleans. As long as booleans are the result, no other part of the program needs
to know anything more specific about them. How they are represented is merely an
implementation detail.
One way to encode booleans is the following:
true
true is encoded by choosing the first of 2 arguments:
λx.λy.x
false
false is encoded by choosing the second of 2 arguments:
λx.λy.y
Implementing another boolean function: not
not applies the choice of b to false and ~true~:
λb.b false true = λb.b (λx.λy.y) (λx.λy.x) = NOT
NOT true = (λb.b (λx.λy.y) (λx.λy.x)) true = (λb.b (λx.λy.y) (λx.λy.x)) (λx.λy.x) = (λx.λy.x) (λx.λy.y) (λx.λy.x) = λx is (λx.λy.y) . λy is (λx.λy.x) . x = (λx.λy.y) = λx.λy.y = false
In the case of b being false, this will result in the second argument being
chose, which is true. In the case of b being true, the first argument will
be chosen, which is false. not returns our representation of true and
~false~!
Function application ("β-reduction")
Function application is written by putting a function and its argument next to each other (juxtapositioning). For example:
λa.a b
In the expression above the function λa.a, the identity function, is applied
to its argument b.
Function composition
Function composition means taking 2 or more functions and building a new function, which applies them in an appropriate order. The newly built function is the composed function.
Function composition works by taking functions as arguments and then juxtapositioning them in the function body:
compose := λf.λg.λx.f (g x)