CS374: Programming Language Principles - The Lambda Calculus
Activity Goals
The goals of this activity are:- To relate the Lambda calculus to the Turing Machine abstraction, and to describe their equivalence
- To derive boolean expressions using the Lambda Calculus and beta-reductions
Supplemental Reading
Feel free to visit these resources for supplemental background reading material.The Activity
Directions
Consider the activity models and answer the questions provided. First reflect on these questions on your own briefly, before discussing and comparing your thoughts with your group. Appoint one member of your group to discuss your findings with the class, and the rest of the group should help that member prepare their response. Answer each question individually from the activity, and compare with your group to prepare for our whole-class discussion. After class, think about the questions in the reflective prompt and respond to those individually in your notebook. Report out on areas of disagreement or items for which you and your group identified alternative approaches. Write down and report out questions you encountered along the way for group discussion.Model 1: Lambda Calculus
λx.x
Questions
- The first statement defines a parameter called
x
and returnsx
. What does(λx.x)y
do?
Model 2: Fundamental Constructs with the Lambda Calculus
true = λxy.x
false = λxy.y
Here,
x
and y
are bound variables. Variables that appear in the lambda expression that are not defined are referred to as free variables.
Questions
- In your own words, what does it mean for something to be true in the lambda calculus, when choosing between two alternative parameters?
Model 3: Boolean Constructions with the Lambda Calculus
not x = λx.x false true
not x = (λx.x false true) true
Now, substitute
true
for x
:not x = (true false true)
Substitute
λxy.x
for true
:not x = (λxy.x false true)
Given two parameters, select the first one, where the parameters are
x = true
, y = false
:
not true = false
equals(x, y) = λxy.???
Apply one of the parameters to see if it expands to
true
or false
:equals(x, y) = λxy.x ???
If
x
is true
, then they are equal if y
is true
, and false
otherwise. In other words, the value of y
is the result.equals(x, y) = λxy.xy ???
Otherwise,
x
is false
, and so the result is true
if y
is also false
; in other words, the result is not y
.equals(x, y) = λxy.xy not y
Which we can expand from our prior definition:
equals(x, y) = λxy.xy y false true
Which we expand again to substitute our definitions for
true
and false
:
equals(x, y) = λxy.xy y λxy.y λxy.x
These substitutions are called beta-reductions.
and(x, y) = y
when x = true
, and false
if x = false
.λxy.xy false
Note that when
x = true
, this corresponds to choosing the first of the two following parameters (y
and false
) to resolve the boolean expression to y
. When x = false
, we choose the second of the two following parameters, and obtain false
.Finally, substitute
λab.b
for false
.
λxy.xy λab.b
Questions
- Verify the behavior of
not false
using the lambda expression above. - All boolean expressions can be constructed using the
NAND
operator. What is the lambda expression forNAND
, which is(NOT AND x y)
? - Derive the boolean expression for
A OR B
, given thatA OR B
istrue
whenA
istrue
, andB
otherwise. - Draw a truth table for the
XOR
operator. What is the result whenA
istrue
? How about whenA
isfalse
? Derive the lambda expression forXOR
. - Draw a truth table for the
equals
operator. What is its boolean expression? Derive its lambda expression.