An Introduction to Functional Programming Through Lambda Calculus

Exercise 3.1

Define a λ calculus representation for implication:

def implies = λx.λy...

Show that the definition satisfies the truth table for all boolean values of x and y.

IMPLIES is a binary operator of the form:

<operand> -> <operand>

It can be modelled using the conditional expression:

X ? Y : TRUE

So we can define IMPLIES as:

def implies = λx.λy.(((cond y) true) x)

Which simplies to:

=> λx.λy.(((λe1.λe2.λs.((s e1) e2) y) true) x)
=> λx.λy.(λs.((s y) true) x)
=> λx.λy.((x y) true)

Demonstrations

False False

=> implies false false
=> λx.λy.((x y) true) false) false
=> ((false false) true)
=> true

False True

=> implies false true
=> λx.λy.((x y) true) false) true
=> ((false true) true)
=> true

True False

=> implies true false
=> λx.λy.((x y) true) true) false
=> ((false true) false)
=> false

True True

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

Exercise 3.2

Define a λ calculus representation for equivalance:

def equiv = λx.λy...

Show that the definition satisfies the truth table for all boolean values of x and y.

EQUIV is a binary operator of the form:

<operand> ≡ <operand>

It can be modelled using the conditional expression:

NOT X ? NOT Y : Y

So we can define EQUIV as:

def equiv = λx.λy.((((not cond) (not y)) y) x)

Which simplifies to:

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

Demonstrations

False False

=> equiv false false
=> λx.λy.(((not x) (not y)) y) false false
=> (((not false) (not false)) false)
=> (((λx.((x false) true) false) (λx.((x false) true) false)) false)
=> ((((false false) true) ((false false) true)) false)
=> ((true true) false)
=> true

False True

=> equiv false true
=> ...
=> (((not false) (not true)) true)
=> ((true false) false)
=> false

True False

=> equiv true false
=> ...
=> (((not true) (not false)) false)
=> ((false true) false)
=> false

True True

=> equiv true true
=> ...
=> (((not true) (not true)) true)
=> ((false false) true)
=> true

Exercise 3.3

For each of the following pairs, show that functions (i) and (ii) are equivalent for all boolean values of their arguments.

(a)

(i) λx.λy.(and (not x) (not y))
(ii) λx.λy.(not (or x y))

False False

(i)

=> (and (not false) (not false))
=> ((and true) true)
=> true

(ii)

=> (not (or false) false)
=> (not false)
=> true

This exercise is essentially just to evaluate the λ expressions so I don’t think there’s much value at this point in doing the rest.

Exercise 3.4

Show that:

λx.(succ (pred x))

and:

λx.(pred (succ x))

are equivalent for arbitrary non-zero integer arguments. Explain why they are not equivalent for a zero argument.

They aren’t equivalent for a zero argument because pred zero is defined as being zero instead of some representation of negative 1, since the succ and pred functions are only defined so far for the set of natural numbers.

To get the successor of the predesseor of a number is just to substract and then add 1. If the function can’t actually subtract 1 then its effect is just to add 1.

One

λx.(succ (pred x))

=> (λx.(succ (pred x)) one)
=> (succ (pred one))
=> (succ zero)
=> one

λx.(pred (succ x))

=> (λx.(pred (succ x)) one)
=> (pred (succ one))
=> (pred two)
=> one

Zero

λx.(succ (pred x))

=> (λx.(succ (pred x)) zero)
=> (succ (pred zero))
=> (succ zero)
=> one

λx.(pred (succ x))

=> (λx.(pred (succ x)) zero)
=> (pred (succ zero))
=> (pred one)
=> zero