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 `cons`

es (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.