functional-programming

Enter the vast world of programming languages by following the tutorials provided here to learn about functional programming in Haskell.

Project maintained by jd-anabi Hosted on GitHub Pages — Theme by mattgraham

Back to main

In most programming languages, the use of conditionals is very common. For example, if we want to choose the smaller number of two numbers, we write the following (pseudo-) code:

if x < y then x else y

If x is less than y, we take the then branch. However, if x isn’t less than y, we take the else branch. Also, as we can see, the if clause always evaluates a TRUE or FALSE statement. Thus, if we want to implement this logic in lambda calculus, we need to do things:

  1. We need a way of representing if-then-else logic itself
  2. We need a way of representing the booleans TRUE and FALSE

Let’s tackle the latter issue first.

TRUE and FALSE

We can represent TRUE and FALSE in lambda calculus by defining them as follows:

TRUE := λx.λy. x FALSE := λx.λy. y

Now, it might not mean much now, but once we have a way of implementing if-then-else logic, hopefully it will become more clear.

If-Then-Else

Now, if-then-else takes in three arguments:

  1. A boolean expression in the if clause
  2. A statement in the then clause
  3. A statement in the else clause

Thus, we can represent if-then-else in lambda calculus by using a abstraction with three binders as follows:

IF-THEN-ELSE := λx.λy.λz. x y z

This seems like a fairly standard abstraction with three binders, so how could this possibily give us our desired logic? Well, let’s combine it with our definitions of TRUE and FALSE

  1. (λx.λy.λz. x y z) (λx.λy. x) p q

  2. (λx.λy.λz. x y z) (λx.λy. y) p q

Now, the first statement represents

if TRUE then p else q

Let’s use our beta-reduction rules to see how this is the case.

(λx.λy.λz. x y z) (λx.λy. x) p q

→ (λy.λz. (λx.λy. x) y z) p q

→ (λz. (λx.λy. x) p z) q

→ (λx.λy. x) p q

→ (λy. p) q

→ p

As we can see, we take the then branch because our boolean expression in the if clause is TRUE. The same can be done for the second statement.

(λx.λy.λz. x y z) (λx.λy. y) p q

→ (λy.λz. (λx.λy. y) y z) p q

→ (λz. (λx.λy. y) p z) q

→ (λx.λy. y) p q

→ (λy. y) q

→ q

The beauty of lambda calculus, however, is that we don’t have to stop here. We can even define lambda expressions for AND, OR, and NOT.

AND, OR, NOT

If you are unfamilar with AND, OR, and NOT, that is ok.

AND, OR, and NOT are operators with the following truth tables (we will be dealing with AND2 and OR2 for simplicity):

AND

Input 1 Input 2 Output
FALSE FALSE FALSE
FALSE TRUE FALSE
TRUE FALSE FALSE
TRUE TRUE TRUE

OR

Input 1 Input 2 Output
FALSE FALSE FALSE
FALSE TRUE TRUE
TRUE FALSE TRUE
TRUE TRUE TRUE

NOT

Input Output
FALSE TRUE
TRUE FALSE

Thus, we define AND, OR, and NOT in lambda calculus as follows:

AND := λx.λy. x y x

OR := λx.λy. x x y

NOT := λx. (λp.λq. q) (λp.λq. p) = λx. FALSE TRUE

As an exercise, I would like you to verify these defintions of AND, OR, and NOT by using the truth tables above in addition to the defintions of TRUE and FALSE. Once you have done that, we can begin learning about De Bruijn indices.