Principles of PL

Assignment 3: Operational Semantics

This short homework assignment will give you some practice with operational semantics before starting to write your F♭ interpreter. Please consult Chapter 2 of the book for the full details on various definitions and for more examples beyond those in the lecture if you have any questions.

1. [6 points] Compute the following substitutions. Note that the substitution function is defined formally in Section 2.3.2 of the book.

   a. (Fun x -> Fun z -> (x + y) = z) [4/y]

   b. (If z Then (Fun x -> Fun z -> x And z) Else 22) [True/z]

   c. (Fun x -> y - z + 1) [3/x]

   d. ((Fun f -> Fun x -> f x) (Fun y -> x)) [2/x]

   e. (Let y = x + 1 In y + 2) [5/y]

   f. (Let f = f In f f) [(Fun f -> f)/f]

2. [9 points] The following F♭ proof trees contain errors. Describe why the proof tree is not valid (i.e., why the last line is, in fact, not a theorem).
   

   a. \[ \begin{prooftree} \AxiomBar{y \Rightarrow y} \AxiomBar{3 \Rightarrow 3} \BinaryInfC{$\mathtt{Let}\ x = y\ \mathtt{In}\ 3 \Rightarrow 3$} \end{prooftree} \]

   b. \[ \begin{prooftree} \AxiomBar{3 \Rightarrow 3} \AxiomBar{0 \Rightarrow 0} \BinaryInfC{$3 + 0 \Rightarrow 3$} \AxiomBar{2 \Rightarrow 2} \BinaryInfC{$\mathtt{If}\ 3 + 0\ \mathtt{Then}\ 2\ \mathtt{Else}\ 2 \Rightarrow 2$} \end{prooftree} \]

   c. \[ \begin{prooftree} \AxiomBar{\mathtt{Fun}\ x \to x + 2 \Rightarrow \mathtt{Fun}\ x \to x + 2} \AxiomBar{3 \Rightarrow 3} \AxiomBar{((\mathtt{Fun}\ x \to x + 2)[3/x]) \Rightarrow \mathtt{Fun}\ x \to 3 + 2} \TrinaryInfC{$(\mathtt{Fun}\ x \to x + 2)\ 3 \Rightarrow \mathtt{Fun}\ x \to 3 + 2$} \end{prooftree} \]

3. [15 points] Write operational semantics proofs (i.e., proof trees) showing what the following expressions evaluate to in the Fb operational semantics. Please give the whole proof trees using the rules in Chapter 2. You may reference one proof tree in another like a “proof tree macro” to make your answer more readable if you want (in other words, you can re-use any one proof tree in another, just like how proofs of Lemmas can be used in Theorems in math). Note: it is not a bad idea to start by running them in the reference interpreter to make sure you are on the right path.

   a. Let f = (Fun y -> y - 1) In Fun z -> 5 + (f z) +1

   b. (Let f = (Fun y -> y - 1) In Fun z -> 5 + (f z) + 1) 4

   c. (Fun x -> (Fun a -> a) (If x = 2 Then x + 1 Else 1)) 2

4. [10 points] Consider the following simple arithmetic language Arith, consisting of:

   • integer constants
   • unary negation
   • binary addition
   • binary subtraction
   • binary multiplication

   For example, valid Arith expressions include:

   9
   3 + 3
   -3 + (2 * 6)
   (4 * (2 + 8)) - 3

   Parentheses indicate grouping in the usual way.

   a. Define the grammar of expressions and values for Arith using BNF notation.

   b. Give the full set of operational semantics rules for Arith.

   c. The Arith language is normalizing: for every Arith expression e, there exists a value v such that e ⇒ v. Prove this fact. (Hint: follow the structure of the normalization proof for the BOOL language in Chapter 2.)

Submission and Grading

Upload your homework pdf to Gradescope. The format is fine as long as you can make a PDF, and we can read it. So, scans of your handwritten solution are fine as long as they are readable and are in PDF format. Please verify the scans are readable before uploading!

Please remember to list any collaborators at the top of your submission as was done in assignments 1 and 2.