### Problem Set 4

Due Friday, February 19, 2016 at 1pm

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 FSL with a general reduction relation, dubbed ->fsl. The relation generates all possible successor configurations for any given configuration. That is, it really is a relation not a function.

If L contains airport A such that from A there are flights on airline X to two airports, B and C—

and there may be additional flights on airlines other than X to any airports— then the two valid successor configurations are those with (1) origin B, destination D, airline X, and airports L and (2) origin C, destination D, airline X, and airports L. If L contains airport A but there are no flights out of A on airline X, then there is no successor configuration.

If the origin A and destination D are the same airport—

i.e., if A equals D— then there is no successor configuration.

Create a submodule trace that contains a trace expression for an FSL configuration that contains more cycles than between just two airports.

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

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.

Deliverable Email a tar.gz bundle to me and Ben Chung at our
CCS email addresses. The name of the bundle should combine the last
names of the pair in alphabetical order. The tar bundle must contain
a single directory—

;; NameOfPartner1, NameOfPartner2 |

;; email@of.partner1.com, email@of.partner2.org |