Due date: 10/15 @ at the beginning of class

The goal of this problem set is to understand the basics of the Lambda calculus as a computing system and to increase your familiarity with Redex and its interaction with Racket. Warning: It is nearly impossible to solve the problems 0 through 2 of this problem set separately. They are closely related and it is best to proceed sequentially. Problem 3 is about ISWIM, not the Lambda Calculus.

Background:

All problems in this assignment refer to this core grammar:

  (define-language Lambda0
    (e x
       (lambda (x) e)
       (e e))
    (x variable-not-otherwise-mentioned))

Furthermore, to help you along, this assignment comes with the definition of a substitution metafunction for Redex-style languages whose only 'binder' is lambda (see bottom). Both pieces are provided via library module that exports two identifier: Lambda0 and subst-n. Save the module and add

  (require "4provided.rkt")

to yours. Do not modify the module; I will link your solution against my version of the module not yours.

In contrast to the text book, your lambda calculus model is used modulo α-equivalence, an idea that is spelled out in chapter I.4 of the text book.

Problem 0:

Design the function =alpha, which consumes two expressions in Lambda0 and determines whether they are α-equivalent. Hint: One way to compute α-equivalence efficiently is to use a two-step procedure. First, translate the given expressions into the so-called "static distance" notation of problem set 1, problem 4, though without leaving the parameter list in place. Second, once the static-distance representation has been computed, it suffices to use equal? to compare the results. (A proof of this idea can be found in the appendix of Barendregt's tome on the Lambda Calculus, Its Syntax and Semantics.)

Problem 1:

Define terms in Lambda0 that encode the booleans True and False; the Church numerals Zero, One, and Two; the Add1 function and the Iszero function; and the If conditional.

Develop a Redex model of the lambda β calculus. That is, the model should use β as the only notion of reduction. As for the η notion of reduction, it is ignored; α is brought back separately.

Use the model to confirm the α-equivalence of

1. (Add1 Zero) and One
2. (Add1 One) and Two
3. (((If True) M) N) and M
4. (((If False) M) N) and M
5. (Iszero Zero) and False

The confirmations should take the shape of

  (check =alpha ... ...)

statements in your Racket modules.

Problem 2:

Use the consistency result of chapter I.3 to design =beta/semi, a semi-algorithm in Racket for equality (module α-equivalence) in the lambda calculus.

Here a semi-algorithm is a function that produces true (meaning the given terms are equal) in some cases but may diverge in others. What does divergence mean? In order to make this function total, equip it with an optional fuel argument that is suitable decreased and that causes the function to stop when it is zero or negative.

Use the semi-algorithm to solve exercise 3.15, i.e., ensure that the algorithm can validate the following unit test:

  (check =beta/semi (term (M (,Y M))) (term (,Y M)))

for a suitable definition of Y.

Finally investigate whether

  (define Apply (term (lambda (f) (lambda (x) (f x)))))
  (define Ident (term (lambda (x) x)))

  (=beta/semi (term (,Y Ident)) (term (,Y ,Apply)) i)

produces true for any i in 1, ..., 5. Should the two terms produce identical fixed points?

Problem 3:

Use define-extended-language to extend Lambda0 to the syntax of the numeric variant of ISWIM (chapter I.4 [page 48]). Then specify a reduction-relation that implements a Redex model of the β_v reduction relation for ISWIM plus the δ function for numerical primitives plus the if0 macro. Finally define the eval function from I.4.5 as a Racket function.

You do not need to design an α-equivalence relation for this exercise. You should develop a reasonably comprehensive test suite for eval, however.