Problem Set 4

Purpose The goal of this problem set is to formulate a general reduction relation and to explore its properties.

Problem 1 Extend your Redex model of DADL with a general reduction relation, dubbed ->dd. The relation generates all possible successor configurations for any given configuration. That is, it really is a traversal relation not a function.

Create a submodule trace that contains a trace expression for a DAD configuration that contains more cycles than between two adjacent rooms.

Use a Redex metafunction to formulate the conjecture that the path delivered by traverse (from the problem set 3) is one of the paths taken by ->dd.

Explain (with 30 words or fewer) why attempts to check this claim with redex-check fail. Start with the most naive way to run redex-check and successively refine your attempts until you know you understand why redex-check fails. Place all these attempts in a submodule called check.

You and your partner may choose whichever of your solutions for problem 2 of Problem Set 3 you like best.

Deliverable Email a tar.gz bundle to my CCS email address whose name combines the last names of the pair in alphabetical order. The tar bundle must contain a single directory—with the same name as the tar ball—with a README.txt file and a 4.rkt Redex file.