Due date: 11/19 (11am) @ at the beginning of class

The goal of this problem set is to understand the CESK register machine.

Your solution should import "8provided.rkt". (Yes, the "8" is correct.)

Problem:

The purpose of this problem is to develop a CESK machine for the ISWIM*s language from problem set 6. Your CESK machine must use the store to safe-keep all values.

Task 1 Encode your CESK machine in Redex.

Task 2 Define the cesk function, which uses the CESK machine to map ISWIM*s programs to answers.

Task 3 Formulate a conjecture about the relationship between eval*-s (solution for problem set 6, imported from 8provided.rkt) and cesk as a metafunction. Test the conjecture manually and with redex-check.

If testing finds a counter-example to your conjecture, formulate the counter-example as a failing test case and explain the failure with a one-line comment. Then fix those parts of your solution that broke so that the test case passes.

Task 4 Fix up your cek function from problem set 8 (task 2), formulate a conjecture about the relationship between cesk and cek, and test the conjecture with redex-check.