Problem Set 4

home work!

Programming Language Reduction Relations

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.

The README.txt file must start with the following lines:

  ;; NameOfPartner1, NameOfPartner2


appropriately instantiated of course. Also separate the Redex code copied from problem set 3 with a line of the shape ";; " followed by 77 "="; for sub-problems of problem set 4 use "-". Each gives you a width of 80 chars. Stick to this line width for all of your code; if you also follow DrRacket’s indentation rules, it ensures some basic readability.