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—
;; NameOfPartner1, NameOfPartner2
;; email@example.com, firstname.lastname@example.org