CS374: Programming Language Principles - The Lambda Calculus

Activity Goals

The goals of this activity are:
  1. To relate the Lambda calculus to the Turing Machine abstraction, and to describe their equivalence
  2. To derive boolean, numeric, and recursive structures using the Lambda Calculus, beta-reductions, and the Y Combinator

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 on the Class Activity Questions discussion board. 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

  1. The first statement defines a parmeter called x and returns x. 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

  1. 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
These expansions are called currying. 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
λxy.xy λab.b

Questions

  1. Verify the behavior of not false using the lambda expression above.
  2. All boolean expressions can be constructed using the NAND operator. What is the lambda expression for NAND, which is (NOT AND x y)?

Model 4: Arithmetic with the Lambda Calculus

let 0 = λn(λz.z)
let 1 = λnz.n(z)
let 2 = λnz.n(n(z))
...
successor(n) = λwyx.y(wyx) (n)
successor(0) = λwyx.y(wyx) (0) = λwyx.y(wyx) (λnz.z) = λnz.n(z) = 1
mul(x, y) = λxyz.x(yz)
mul(3, 2) = λxyz.x(yz) 3 2 = λz.3(2z) = 6

Questions

  1. How might you define addition using the successor function?

Model 5: Recursion and the Y Combinator

Y = λf.(λx.f(x x)) (λx.f(x x))
Y g = λf.(λx.f(x x)) (λx.f(x x)) g
Y g = (λx.g(x x)) (λx.g(x x))
Y g = g ((λx.g(x x)) (λx.g(x x)))
Y g = g (Y g)

Questions

  1. How can this model be extended to support recursive procedures?

Submission

Submit your answers to the questions using the Class Activity Questions discussion board. You may also respond to questions or comments made by others, or ask follow-up questions there. Answer any reflective prompt questions in the Reflective Journal section of your OneNote Classroom personal section.