►7400:   i  PPL
▼Problem Sets
    ← prev  up  next → 

Problem Set 4

home work!

Topic Reduction Relations

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.

image

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.

Successor configurations: Consider a flight-search configuration that specifies origin A, destination D, airline X, and a list of airports L.

  • 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—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

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

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.

    ← prev  up  next →