Teaching G7400 F'11 Assignments Set 1 Set 2 Set 3 Set 4 Set 5 Set 6 Set 7 Set 8 Set 9

### Problem Set 4: The Lambda Calculus as a Model of Computation

 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.

 last updated on Tue Nov 15 15:51:00 EST 2011 generated with Racket