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

The goal of this problem set is to revisit representations in the lambda calculus and to get acquainted with ISWIM.

Background:

The file "5provided.rkt" provides all the items that "4provided.rkt" provides, plus a reduction relation that implements beta one-step, a Racket function that determines α equivalence, and several useful Lambda terms (for booleans and pairs). The latter come with verified equations.

Problem 1:

An alternative way to encode numerals in Lambda is to say that 0 corresponds to the identity function and that n+1 is represented by the pair of ff (false) and the representation of n.

Your first task is to design a metafunction that maps Racket's natural numbers to their numeral representation in Lambda.

Your second task is to define Lambda representations of the following functions on natural numbers: succ, which creates the successor for a given numeral; pred, which extracts n from the representation of n+1; and iszero, which produces tt (true) for 0 and ff for all other numerals.

Third, formulate reduction tests that show that your functions satisfy or falsify the following properties for numerals n:

  (iszero zero) =β tt 
  (iszero (succ n)) =β ff 

  (pred (succ n)) =β n 
  (succ (pred n)) =β n 

Warning: do not use redex-check. Use small numbers for which the tests terminate in a reasonable amount of time (less than 30s).

Finally, prove the above properties unless you have falsified them. Each line in your proof must either justify the step as "by def. of ..." or as "by beta" or "by equation for ...". You may collapse several (un)foldings of definitions or several beta steps into one line. Keep the proofs concise.

Problem 2:

Develop a model of the numeric variant of ISWIM (chapter I.4 [page 48]). The model should provide the β_v reduction relation for ISWIM plus a δ reduction relation for the numerical primitives. Also equip the language with an if0 construct, though introduce a syntactic reduction that just translates an if0 expression into an expression in the rest of the language.

Define the eval-v function, which maps closed ISWIM expressions to numbers if they are provably reducible to numbers and 'closure if the are provably reducible to lambda expressions. Recall that our eval-v functions are partial on their domain.

Use the imports from "5provided.rkt" to reduce your work load.

Problem 3:

Extend the language of problem 2 with a Racket-style lists data type. It should come with the following constants and functions: empty, empty?, cons, cons?, first, and rest. Like in Racket, cons combines two values into one, and a list is a tree of conses (of values) whose right-most spine ends in empty. We call the extended language ISWIM*.

Define the eval*-v function, which maps closed ISWIM* expressions to numbers, empty, or cons trees of values if they are provably reducible to those or 'closure if the are provably reducible to lambda expressions.