lambda-calculus-notes/lambda.org

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)