Due: By the beginning of lecture on Wednesday, February 18.
Due date changed to "Monday, February 23"
Due date changed to "Wednesday, February 25"
You are required to typeset your answers. Not only will this make your
answers easier to read, but it will make your work easier since you can
use an editor to cut/paste/modify
parts of different problems. We strongly recommend using LaTeX since it
is superior for layout of mathematical material. If you choose to use
some other word processing application, please be sure that it produces
equally high quality output.
Your are strongly urged to follow the guidelines for
structuring proofs that were given by the staff of the Princeton Programming Languages course.
Do Exercise 1 in Section 1.9 (p. 15) of Harper's book.
Do Exercise 3 in Section 1.9 (p. 15) of Harper's book.
Refer to slide 16 from Inductive-PDF.
Using the rule set for variadic trees given there, give and justify an example of:
A derivability judgement that is valid given this rule set.
An admissibility judgement that is valid given this rule set.
A change to the rule set that would make the admissibility judgement you
gave in your answer to the previous question invalid.
Do Exercise 1 in Section 4.4 (p. 36) of Harper's book.
Using rules (5.2a) and (5.2b) on page 40 of Harper's book
(or the rules on slide 6 from Syntax1-PDF),
give a derivation for the judgement "ab^cd = abcd str".
Give an inductive definition of the judgement | s | = n str, where s str and n nat,
stating that a string s has length n, namely the number of symbols occurring within it.
Use the principle of string induction to show that this judgement defines a function.
Do Exercise 1 in Section 6.3 (p. 51) of Harper's book.
Do Exercise 2 in Section 6.3 (p. 51) of Harper's book.
Use the inductive definition of lexing (pages 55 and 56 in Harper's book)
to derive the lexical analysis of "1+2*3" to "NUM[1] ADD NUM[2] MUL NUM[3]".
Use the inductive definition of parsing (page 58 in Harper's book)
to produce two different derivations for "NUM[1] ADD NUM[2] MUL NUM[3]".
Give the (unique) derivation "NUM[1] ADD NUM[2] MUL NUM[3]" that can be
produced using the layered grammer on page 60 in Harper's book.
