CS374: Principles of Programming Languages - Lab: Lambda Calculus (100 Points)

Purpose, Task, and Criteria

Purpose: To evaluate lambda calculus expressions by hand with a partner — beta reduction with capture-avoiding substitution, and Church encodings of booleans and numerals — the theory floor beneath functional programming.

Task: With a partner, carry out step-by-step beta reductions including a capture-avoidance case, and verify Church-encoded booleans and numerals by reduction.

Criteria: Assessed on correct, fully-shown reduction sequences and correct Church-encoding verifications, weighted 55/45 across the two parts; see the rubric below for the full breakdown.

Assignment Goals

The goals of this assignment are:
  1. To perform beta reduction step by step, identifying redexes and applying capture-avoiding substitution
  2. To verify Church encodings of booleans and numerals by reduction
  3. To connect lambda calculus to the closures and higher-order functions of the surrounding course

Background Reading and References

Please refer to the following readings and examples offering templates to help get you started:

The Assignment

This lab is entirely on paper: you and a partner evaluate lambda calculus expressions by hand, the way the Lambda Calculus class sessions do on the board. It stands alone — nothing imports it — but it is deliberate preparation for two things: the Functional Programming assignment’s Direction C (Church encodings in code — the reductions you write here are the test cases your reducer must reproduce) and the closures material, where “a function that captures a variable” stops being mysterious once you have alpha-renamed by hand. Budget two to three hours.

Pair policy: this lab may be completed in pairs — reduce independently, then reconcile line by line; disagreements are where the learning is. Both partners submit the same document, each naming the other, and both earn the same grade. (You may also work alone.)

Part 1: Beta Reduction (55 points)

In reductions.md, reduce each expression to normal form, one beta-step per line, marking the redex you contract at each step:

  1. (λx. x) y
  2. (λx. λy. x) a b
  3. (λf. λx. f (f x)) (λz. z + 1) 0 — treat + and numerals as constants.
  4. The capture case: (λx. λy. x) y — blind substitution captures the free y; alpha-rename first and add one sentence explaining what would have gone wrong without it.
  5. (λx. x x) (λx. x x) — reduce three steps, then state what this term tells you about termination. Then answer: given (λx. z) ((λx. x x) (λx. x x)), which evaluation order (normal or applicative) terminates, and what does that imply about lazy evaluation?

Part 2: Church Encodings (45 points)

Using TRUE = λt. λf. t, FALSE = λt. λf. f, AND = λp. λq. p q p, and numerals ZERO = λf. λx. x, ONE = λf. λx. f x, SUCC = λn. λf. λx. f (n f x):

  1. Verify AND TRUE FALSE reduces to FALSE, showing every step.
  2. Verify AND TRUE TRUE reduces to TRUE.
  3. Verify SUCC ONE reduces to a term alpha-equivalent to TWO = λf. λx. f (f x).
  4. Close with a short answer: a Church numeral is a higher-order function — “apply f, n times.” Name the Python or Scheme idiom from the Functional Programming sessions that does exactly this, and one place your team language or interpreter could use the same trick.

Deliverables

Submit reductions.md (or a scanned/photographed handwritten equivalent, legible) containing both parts, with both partners named at the top.

Grading Breakdown

Component Points
Part 1: Beta Reduction 55
Part 2: Church Encodings 45
Total 100

Reflection Prompts

  • Which reduction did you and your partner disagree on, and what settled it?
  • If you worked in a pair, who did what. If you worked alone, note that instead.
  • AI disclosure: list any generative-AI tools you used, for what, and how you verified the results (or state ‘none’).
  • Approximately how many hours it took you to finish this lab (I will not judge you for this at all — I am simply using it to gauge if the labs are too easy or hard)?

Submission

In your submission, please include answers to any questions asked on the assignment page, as well as the questions listed below, in your README file. If you wrote code as part of this assignment, please describe your design, approach, and implementation in a separate document prepared using a word processor or typesetting program such as LaTeX. This document should include specific instructions on how to build and run your code, and a description of each code module or function that you created suitable for re-use by a colleague. In your README, please include answers to the following questions:
  • Describe what you did, how you did it, what challenges you encountered, and how you solved them.
  • Please answer any questions found throughout the narrative of this assignment.
  • If collaboration with a buddy was permitted, did you work with a buddy on this assignment? If so, who? If not, do you certify that this submission represents your own original work?
  • Please identify any and all portions of your submission that were not originally written by you (for example, code originally written by your buddy, or anything taken or adapted from a non-classroom resource). It is always OK to use your textbook and instructor notes; however, you are certifying that any portions not designated as coming from an outside person or source are your own original work.
  • Approximately how many hours it took you to finish this assignment (I will not judge you for this at all...I am simply using it to gauge if the assignments are too easy or hard)?
  • Your overall impression of the assignment. Did you love it, hate it, or were you neutral? One word answers are fine, but if you have any suggestions for the future let me know.
  • Using the grading specifications on this page, discuss briefly the grade you would give yourself and why. Discuss each item in the grading specification.
  • Any other concerns that you have. For instance, if you have a bug that you were unable to solve but you made progress, write that here. The more you articulate the problem the more partial credit you will receive (it is fine to leave this blank).

Assignment Rubric

Description Pre-Emerging (< 50%) Beginning (50%) Progressing (85%) Proficient (100%)
Beta Reduction (Goal 1) (55%) Reductions are missing or skip directly to claimed answers with no steps Simple reductions are correct but the capture-avoidance case substitutes blindly, capturing the free variable All reductions are correct including the alpha-renaming, but redexes are not marked or one sequence skips steps Every reduction is shown one beta-step at a time with the redex underlined or bracketed at each step, the capture case is handled by explicit alpha-renaming with a sentence explaining why, and the normal-order vs. applicative-order question is answered with the divergence example
Church Encodings (Goals 2, 3) (45%) Encodings are stated but never verified by reduction The boolean verifications are shown but the numeral ones are missing or incorrect All verifications are shown with one reduction error, or the connection question is unanswered TRUE/FALSE/AND and successor-of-one are all verified by complete reduction sequences, and the closing question connects Church encoding to a concrete higher-order-function idiom from the Functional Programming sessions

Please refer to the Style Guide for code quality examples and guidelines.