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

Problem Set 4: Redex and the LC

 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 `(Add1 Zero)` and `One` `(Add1 One)` and `Two` `(((If True) M) N)` and `M` `(((If False) M) N)` and `M` `(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.

 last updated on Sun Nov 21 19:38:23 EST 2010 generated with PLT Scheme