Problem Set 7
Topic Modeling a Full-fledged Language and Proving Type Safety
Purpose This problem set has two distinct goals. First, you will work
on a comparison of a program with a model. Second, you will do a proof of type
Problem 1 The solutions to the first six problem sets constitute both
an implementation of DADL as well as a model. You are now in a position to
compare the two to find out whether they are in sync.
Figure 1: Comparing language implementations and models
See figure 1
for a diagramatic overview of the process.
Here are the files that implement the mechanics of this comparison process:
cmp.bash, a Unix bash script that compares the two
for more than a dozen test files located in a local Tests/ directory;
3.rkt and 3-parser.rkt, the
Racket solution to Problem Set 3, including an XML-to-S-expression (term)
6.rkt, my Redex solution to Problem Set 6;
7-script.rkt, a Racket file that turns a
Redex solution into a Unix script.
The last script, 7-script.rkt re-uses 3-parser.rkt, the raw
parser from problem set 3, because the comparison effort focuses on the
static (type) checking and the semantics of the model and assumes basic
parsing is easy and requires no checks.
Your task is to adapt 7-script.rkt
solutions for Problem Set 3
and Problem Set 6
. First, you will
have to adjust the path to Racket’s executable in the header of the script
so that it points to your Racket installation. Second, you need to read the
Redex language definition in 6.rkt
and the Racket code in
. Third, you must modify the parser in 7-script.rkt
so that it translates the XML files into your
representation of DADL
in Redex. Fourth, you export evaluate
from your version of 6.rkt
so that 7-script.rkt
can import it; see my stub solution for how to
export a function from a module. Finally, you can run cmp.bash
comparison script takes the path to the two executable on the command line:
$ ./cmp.bash ./3.rkt ./7-script.rkt
and assume that the XML test files are located in a "Tests/"
directory. It runs the two executables on each file in "Tests/"
and diff’s the outcomes.
When the comparison process discovers a discrepancy between your
implementation and your model, investigate and fix either the
implementation or the model to eliminate the discrepancy. Then describe the
discrepancy in a paragraph of at most 30 words in your README file. You may
add a five-line sample XML configuration to a paragraph if you wish to
illustrate your point.
First, read Chapters 8 and 9 of Types and Programming Languages (TAPL). Make sure you understand the details of proving type soundness for Arith and STLC via progress and preservation.
Next, see here. Solutions to this problem should be submitted on paper at my office by 1pm on March 20th.
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 your 7-script.rkt Racket file.
To grade problem 1, I will use your solutions to Problem Set 3 and
Problem Set 6 as turned it with the latter. This gives me a chance to check
on the discrepancies you discovered or those that you didn’t discover.
The README.txt file must start with the following lines:
;; NameOfPartner1, NameOfPartner2
;; email@example.com, firstname.lastname@example.org
appropriately instantiated of course. For this homework, use the README to report
on the discrepancies found in problem 1.