Due date: 10/14 @ 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's testing facilities.

Problem 1:

The goal of this exercise is to equip the calculational model of arithmetic from class with three additional operations: -, *, if0:

  (define-language Expressions
    (e n
       (e + e)
       (e * e)
       (e - e)
       (e / e)
       error
       x
       (if0 e e e))
    (n number))

The interpretation of the operations is the obvious one. In particular, an if0 expression reduces to the second sub-expression if its first one reduces to 0 and to the third sub-expression otherwise.

Also the model comes with error so that your model can deal with division by 0. Specifically, your model should reduce expressions such as (1 / 0) to error, and operations that encounter error should propagate it, e.g., (1 + error) should reduce to error.

The variable x is to remain uninterpreted. It serves as a reminder that this kind of expression language could appear as a part of a full-fledged programming language.

Equip the model with a collection of test reductions that show that the terms are reduced to normal form. Since testing reductions is a common activity for semantics engineers, Redex comes with appropriate constructs. See documentation.

Background for Problems 2 through 4:

All remaining problems in this assignment refer to this core grammar:

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

This language is defined and exported from the library module "4provided.rkt". In addition to the language, the module provides a capture-avoiding substitution function, subst-n. Save the module under its given name and add

  (require "4provided.rkt")

to your solution file. Do not modify the module. Program to its interface only.

Problem 2:

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

Here is a definition of a Racket function that determines whether two terms in Lambda0 are indeed α-equivalent:

  ;; e[Lambda0] e[Lambda0] -> Boolean 
  ;; are t1 and t2 alpha equivalent?
  (define (alpha= t1 t2)
    (define sd1 (term (sd ,t1)))
    (define sd2 (term (sd ,t2)))
    (equal? sd1 sd2))

It assumes the definition of the function sd, which translates a Lambda0 term into the so-called "static distance" notation of problem set 1, problem 5. In class, this form is referred to as the "arrow" form of terms.

Design the sd function and all necessary auxiliaries in Redex. Do not escape to Racket for any reason. In addition to replacing bound variables into static distance numbers, the function must also change all parameters to dummy or some other fixed name. Doing so is legitimate because parameter names no longer play a role in static-distance notation. It enables the simple comparison via equal? in alpha= above.

Problem 3:

Develop a Redex model of the lambda β calculus. That is, the model should use β as the only notion of reduction.

Demonstrate with three reduction tests that the model can reduce Lambda0 to normal form, i.e., to terms that do not contain a β redex. At least one of the tests must demonstrate that doing so may require several steps. Another test must demonstrate that you can predict the outcome only up to α equivalence.

Problem 4:

Implement the stacks from problem set 2 via Lambda0 expressions. Do not use recursion, i.e., the Y combinator. Instead use the OO-encoding model.

Demonstrate with reduction tests that the expressions implement the reduction laws of stacks for concrete examples. Note: when I worked through this exercise, I had to disable 'debugging' in DrRacket to get decent performance. I only did so after debugging the model of course.