Add exercise set 4

info/exercises/src/ex-04/ex/grammar.tex

+
+\begin{exercise}{}
+  For each of the following pairs of grammars, show that they are equivalent by
+  identifying them with inductive relations, and proving that the inductive
+  relations contain the same elements.
+
+  \begin{enumerate}
+    \item 
+    \(A_1 : S ::= S + S \mid \num \) \\ 
+    \(A_2 : R ::= \num ~R' \text{ and } R' ::= + R~ R' \mid \epsilon\)
+    \item 
+    \(B_1 : S ::= S(S)S \mid \epsilon \) \\ 
+    \(B_2 : R ::= RR \mid (R) \epsilon\)
+  \end{enumerate}
+
+  \begin{solution}
+    \begin{enumerate}
+      \item \(A_2\) is the result of left-recursion elimination on \(A_1\).
+      First, expressing them as inductive relations, with rules named as on the
+      right:
+      %
+      \addtolength{\jot}{1ex}
+      \begin{gather*}
+        \AxiomC{\phantom{\(w_1 \in S\)}}
+        \RightLabel{\(S_{num}\)}
+        \UnaryInfC{\(\num \in S\)}
+        \DisplayProof 
+        \quad
+        \AxiomC{\(w_1 \in S\)}
+        \AxiomC{\(w_2 \in S\)}
+        \RightLabel{\(S_+\)}
+        \BinaryInfC{\(w_1 + w_2 \in S\)}
+        \DisplayProof \\
+        %
+        \AxiomC{\(w \in S\)}
+        \RightLabel{\(A_{1}^{start}\)}
+        \UnaryInfC{\(w \in A_1\)}
+        \DisplayProof \\
+        %
+        \AxiomC{\(w \in R'\)}
+        \RightLabel{\(R_{num}\)}
+        \UnaryInfC{\(\num~ w\in R\)}
+        \DisplayProof \\
+        %
+        \AxiomC{\(w \in R\)}
+        \AxiomC{\(w' \in R'\)}
+        \RightLabel{\(R'_{+}\)}
+        \BinaryInfC{\(+w ~ w' \in R'\)}
+        \DisplayProof 
+        \quad
+        \AxiomC{\phantom{\(w' \in R'\)}}
+        \RightLabel{\(R'_{\epsilon}\)}
+        \UnaryInfC{\(\epsilon \in R'\)}
+        \DisplayProof \\
+        %
+        \AxiomC{\(w \in R\)}
+        \RightLabel{\(A_{2}^{start}\)}
+        \UnaryInfC{\(w \in A_2\)}
+        \DisplayProof
+      \end{gather*}
+
+      We must show that for any word \(w\), \(w \in A_1\) if and only if \(w \in
+      A_2\). For this, it must be the case that there is a derivation tree for
+      \(w \in A_1\) (equivalently, \(w \in S\)) if and only if there is a
+      derivation tree for \(w \in A_2\) (equivalently, \(w \in R\)) according to
+      the inference rules above.
+      \begin{enumerate}
+        \item \(w \in S \implies w \in R\): we induct on the depth of the
+        derivation tree. 
+        \begin{itemize}
+          \item Base case: derivation tree of depth 1. The tree must be
+          \begin{gather*}
+            \AxiomC{}
+            \RightLabel{\(S_{num}\)}
+            \UnaryInfC{\(\num \in S\)}
+            \DisplayProof
+          \end{gather*}
+          We can show that there is a corresponding derivation tree for \(w \in R\):
+          \begin{gather*}
+            \AxiomC{}
+            \RightLabel{\(R'_{\epsilon}\)}
+            \UnaryInfC{\(\epsilon \in R'\)}
+            \RightLabel{\(R_{num}\)}
+            \UnaryInfC{\(\num \in R\)}
+            \DisplayProof
+          \end{gather*}
+          \item Inductive case: derivation tree of depth \(n+1\), given that for
+          every derivation of depth \( \le n\) of \(w' \in S\) for any \(w'\), there
+          is a corresponding derivation of \(w' \in R\). The last rule applied
+          in the derivation must be \(S_+\):
+          \begin{gather*}
+            \AxiomC{\ldots}
+            \UnaryInfC{\(w_1 \in S\)}
+            \AxiomC{\ldots}
+            \UnaryInfC{\(w_2 \in S\)}
+            \RightLabel{\(S_+\)}
+            \BinaryInfC{\(w_1 + w_2 \in S\)}
+            \DisplayProof
+          \end{gather*}
+          By the inductive hypothesis, since \(w_1 \in S\) and \(w_2 \in S\)
+          have a derivation tree of smaller depth, there are derivation trees
+          for \(w_1 \in R\) and \(w_2 \in R\). In particular, the derivation for
+          \(w_1 \in R\) must end with the rule \(R_{num}\) (only case), so there
+          must be a derivation tree for \(\num ~w_1' \in R\) with \(w_1' \in
+          R'\) and \(num~w_1' = w_1\). We have the following pieces:
+          \begin{gather*}
+            \AxiomC{\ldots}
+            \UnaryInfC{\(w_1' \in R'\)}
+            \RightLabel{\(R_{num}\)}
+            \UnaryInfC{\(\num ~w_1' \in R\)}
+            \DisplayProof
+            \quad
+            \AxiomC{\ldots}
+            \UnaryInfC{\(w_2 \in R\)}
+            \DisplayProof
+          \end{gather*}
+          To show that \(w_1 + w_2 \in R\), i.e. \(\num ~w_1' + w_2 \in R\), we
+          must first show that \(w_1' + w_2 \in R'\), as required by the rule
+          \(R_{num}\). Note that words in \(R'\) are of the form \((+ \num)^*\).
+          We will prove this separately for all pairs of words at the end
+          (\(R'_{Lemma}\)). Knowing this, however, we can construct the
+          derivation tree for \(w_1 + w_2 \in R\):
+          \begin{gather*}
+            \AxiomC{\ldots}
+            \UnaryInfC{\(w_1' \in R'\)}
+            \AxiomC{\ldots}
+            \UnaryInfC{\(w_2 \in R\)}
+            \RightLabel{\(R'_{Lemma}\)}
+            \BinaryInfC{\(w_1' + w_2 \in R'\)}
+            \RightLabel{\(R_{num}\)}
+            \UnaryInfC{\(\num ~w_1' + w_2 \in R\)}
+            \DisplayProof
+          \end{gather*}
+          \(\num ~w_1' + w_2 = w_1 + w_2 = w\), as required.
+
+          Finally, we will show the required lemma. We will prove a stronger
+          property \(R'_{concat}\) first, that for any pair of words \(w_1, w_2
+          \in R'\), \(w_1 ~w_2 \in R'\) as well. We induct on the derivation of
+          \(w_1 \in R'\).
+          
+          Base case: derivation ends with \(R'_\epsilon\). Then \(w_1 =
+          \epsilon\), and \(w_1 ~w_2 = w_2 \in R'\) by assumption. 
+          
+          Inductive case: derivation ends with \(R'_+\). Then \(w_1 = + v v'\)
+          for some \(v \in R\) and \(v' \in R'\):
+          \begin{gather*}
+            \AxiomC{\ldots}
+            \UnaryInfC{\(v \in R\)}
+            \AxiomC{\ldots}
+            \UnaryInfC{\(v' \in R'\)}
+            \RightLabel{\(R'_+\)}
+            \BinaryInfC{\(+ v ~v' \in R'\)}
+            \DisplayProof
+          \end{gather*}
+
+          Since \(v' \in R'\) has a smaller derivation tree than \(w_1\), by the
+          inductive hypothesis, we can prove that \(v'~w_2 \in R'\). We get:
+          \begin{gather*}
+            \AxiomC{\ldots}
+            \UnaryInfC{\(v \in R\)}
+            \AxiomC{\ldots}
+            \UnaryInfC{\(v' \in R'\)}
+            \AxiomC{\ldots}
+            \UnaryInfC{\(w_2 \in R'\)}
+            \RightLabel{\(R'_{concat}\)}
+            \BinaryInfC{\(v' ~w_2 \in R'\)}
+            \RightLabel{\(R'_+\)}
+            \BinaryInfC{\(+ v ~v' ~w_2 \in R'\)}
+            \DisplayProof
+          \end{gather*}
+
+          So, \(R'_{concat}\) is proven. We can show \(R'_{lemma}\), i.e. \(w_1'
+          + w_2 \in R'\) if \(w_1' \in R'\) and \(w_2 \in R\) as:
+          \begin{gather*}
+            \AxiomC{\ldots}
+            \UnaryInfC{\(w_1' \in R'\)}
+            \AxiomC{\ldots}
+            \UnaryInfC{\(w_2 \in R\)}
+            \AxiomC{}
+            \RightLabel{\(R'_\epsilon\)}
+            \UnaryInfC{\(\epsilon \in R'\)}
+            \RightLabel{\(R'_+\)}
+            \BinaryInfC{\(+ w_2 \in R'\)}
+            \RightLabel{\(R'_{concat}\)}
+            \BinaryInfC{\(w_1' + w_2 \in R'\)}
+            \DisplayProof
+          \end{gather*}
+
+          Thus, the proof is complete.
+      \end{itemize}
+      \item \(w \in R \implies w \in S\): we induct on the depth of the
+      derivation tree for \(w \in R\). This direction is simpler than the other,
+      but the general method is similar.
+      
+      \begin{itemize}
+        \item Base case: derivation tree of depth 2 (minimum). The tree must be
+        \begin{gather*}
+          \AxiomC{}
+          \RightLabel{\(R'_{\epsilon}\)}
+          \UnaryInfC{\(\epsilon \in R'\)}
+          \RightLabel{\(R_{num}\)}
+          \UnaryInfC{\(\num \in R\)}
+          \DisplayProof
+        \end{gather*}
+  
+        We have the corresponding derivation tree for \(w \in S\):
+        \begin{gather*}
+          \AxiomC{}
+          \RightLabel{\(S_{num}\)}
+          \UnaryInfC{\(\num \in S\)}
+          \DisplayProof
+        \end{gather*}
+  
+        \item Inductive case: derivation tree of depth \(n+1\), given that for
+        every derivation of depth \(\le n\) of \(w' \in R\) for any \(w'\),
+        there is a corresponding derivation of \(w' \in S\). The last rules
+        applied must be \(R_{num}\) and \(R'_{+}\) (otherwise the derivation
+        would be of the base case):
+        \begin{gather*}
+          \AxiomC{\ldots}
+          \UnaryInfC{\(w_1 \in R\)}
+          \AxiomC{\ldots}
+          \UnaryInfC{\(w_2 \in R'\)}
+          \RightLabel{\(R'_{+}\)}
+          \BinaryInfC{\(+ w_1 ~w_2 \in R'\)}
+          \RightLabel{\(R_{num}\)}
+          \UnaryInfC{\(\num + w_1~ w_2 \in R\)}
+          \DisplayProof
+        \end{gather*}
+        %
+        where \(w = \num + w_1 ~w_2\). However, we are somewhat stuck here, as
+        we have no way to relate \(R'\) and \(S\). We will separately show that
+        if \(+w' \in R'\), then there is a derivation of \(w' in S\) (lemma
+        \(R'_{S}\)). This will allow us to complete the proof:
+        \begin{gather*}
+          \AxiomC{}
+          \RightLabel{\(S_{num}\)}
+          \UnaryInfC{\(\num \in S\)}
+          \AxiomC{\ldots}
+          \UnaryInfC{\(+w_1 ~w_2 \in R'\)}
+          \RightLabel{\(R'_{S}\)}
+          \UnaryInfC{\(w_1 ~w_2 \in S\)}
+          \RightLabel{\(S_{+}\)}
+          \BinaryInfC{\(\num + w_1 ~w_2 \in S\)}
+          \DisplayProof
+        \end{gather*}
+
+        The proof of the lemma \(R'_S\) is by induction again, and not shown
+        here. This completes the original proof.
+      \end{itemize}
+        
+      \end{enumerate}
+      \item Argument similar to Exercise Set 2 Problem 4 (same pair of
+      grammars). \(B_1 \subset B_2\) as relations can be seen by producing a
+      derivation tree for each possible case in \(B_1\). For the other
+      direction, \(B_2 \subseteq B_1\), it is first convenient to prove
+      that \(B_1\) is closed under concatenation, i.e., if \(w_1, w_2 \in B_1\)
+      then there is a derivation tree for \(w_1 ~ w_2 \in B_1\).
+    \end{enumerate}
+  \end{solution}
+  
+\end{exercise}
+

info/exercises/src/ex-04/ex/semantics.tex

+
+
+\begin{exercise}{}
+
+  Consider the following expression language over naturals, and a \emph{halving}
+  operator:
+  %
+  \begin{align*}
+    expr ::= \half(expr) \mid expr + expr \mid \num
+  \end{align*}
+  where \(\num\) is any natural number constant \(\ge 0\).
+
+  We will design the operational semantics of this language. The semantics
+  should define rules that apply to as many expressions as possible, while being
+  subjected to the following safety conditions:
+  \begin{itemize}
+    \item the semantics should \emph{not} permit halving unless the argument is even
+    \item they should evaluate operands from left-to-right
+  \end{itemize}
+
+  Of the given rules below, choose a \emph{minimal} set that satisfies the
+  conditions above. A set is \emph{not} minimal if removing any rule does not
+  change the set of expressions that can be evaluated by the semantics, i.e. the
+  domain of \(\leadsto, \{x \mid \exists y.\; x \leadsto y\}\), remains
+  unchanged. The removed rule is said to be \emph{redundant}.
+
+  
+  % \begin{multicols}{2}
+    \allowdisplaybreaks
+    \addtolength{\jot}{2ex}
+    \begin{gather*}
+      \AxiomC{\(e \leadsto e'\)}
+      \UnaryInfC{\(\half(e) \leadsto e'\)}
+      \DisplayProof \tag{A} \\
+      %
+      \AxiomC{\(n\) is a value}
+      \AxiomC{\(n = 2k\)}
+      \BinaryInfC{\(\half(n) \leadsto k\)}
+      \DisplayProof \tag{B} \\
+      %
+      \AxiomC{\(n\) is a value}
+      \UnaryInfC{\(\half(n) \leadsto \lfloor \frac{n}{2} \rfloor\)}
+      \DisplayProof \tag{C} \\
+      %
+      \AxiomC{\(\half(e) \leadsto \half(e')\)}
+      \UnaryInfC{\(\half(e) \leadsto e'\)}
+      \DisplayProof \tag{D} \\
+      %
+      \AxiomC{\(e \leadsto e'\)}
+      \UnaryInfC{\(\half(e) \leadsto \half(e')\)}
+      \DisplayProof \tag{E} \\
+      %
+      \AxiomC{\(e' \leadsto \half(e)\)}
+      \UnaryInfC{\(half(e) \leadsto e'\)}
+      \DisplayProof \tag{F} \\
+      %
+      \AxiomC{\(n_1\) is a value}
+      \AxiomC{\(n_2\) is a value}
+      \AxiomC{\(n_1 + n_2 = k\)}
+      \AxiomC{\(n_1\) is odd}
+      \QuaternaryInfC{\(n_1 + n_2 \leadsto k\)}
+      \DisplayProof \tag{G} \\
+      %
+      \AxiomC{\(e \leadsto e'\)}
+      \AxiomC{\(n\) is a value}
+      \BinaryInfC{\(n + e \leadsto n + e'\)}
+      \DisplayProof \tag{H} \\
+      %
+      \AxiomC{\(e_2 \leadsto e_2'\)}
+      \UnaryInfC{\(e_1 + e_2 \leadsto e_1 + e_2'\)}
+      \DisplayProof \tag{I} \\
+      %
+      \AxiomC{\(n_1\) is a value}
+      \AxiomC{\(n_2\) is a value}
+      \AxiomC{\(n_1 + n_2 = k\)}
+      \AxiomC{\(n_1, n_2\) are even}
+      \QuaternaryInfC{\(n_1 + n_2 \leadsto k\)}
+      \DisplayProof \tag{J} \\
+      %
+      \AxiomC{\(n_1\) is a value}
+      \AxiomC{\(n_2\) is a value}
+      \AxiomC{\(n_1 + n_2 = k\)}
+      \TrinaryInfC{\(n_1 + n_2 \leadsto k\)}
+      \DisplayProof \tag{K} \\
+      %
+      \AxiomC{\(e_1 \leadsto e_1'\)}
+      \UnaryInfC{\(e_1 + e_2 \leadsto e_1' + e_2\)}
+      \DisplayProof \tag{L} 
+    \end{gather*}
+  % \end{multicols}
+
+  \begin{solution}
+    A possible such minimal set of rules is \(\{B, E, H, K, L\}\). % TODO:
+
+    On what happens when the other rules are added to this set:
+    \begin{itemize}
+      \item A: incorrect; allows deducing \(\half(\half(10)) \leadsto 5\) with
+      rule B.
+      \item C: incorrect; allows deducing \(\half(3) \leadsto 1\).
+      \item D: incorrect; allows deducing \(\half(\half(10)) \leadsto 5\) with
+      rules B and E.
+      \item F: redundant; reverses a reduction.
+      \item G: redundant; special case of rule K.
+      \item I: incorrect; does not reduce the expression left-to-right.
+      \item J: redundant; special case of rule K.
+    \end{itemize}
+  \end{solution}
+
+\end{exercise}
+
+\begin{exercise}{}
+
+  Consider a simple programming language with integer arithmetic, boolean
+  expressions, and user-defined functions:
+
+  \begin{align*}
+    expr ::= &~ true \mid false \mid \num \\
+             &~ expr == expr \mid expr + expr \\
+             &~ expr ~\&\& ~expr \mid if ~(expr) ~expr ~else ~expr \\
+             &~ f(expr, \ldots, expr) \mid x
+  \end{align*}
+  %
+  where \(f\) represents a (user-defined) function, \(x\) represents a
+  variable, and \(\num\) represents an integer.
+
+  \begin{enumerate}
+    \item Inductively define a substitution operation for the terms in this
+      language, which replaces every free occurrence of a variable \(x\) with a
+      given expression \(e\).
+
+      The rule for substitution in an addition is provided as an example. Here,
+      \(t[x := e]\) represents the term \(t\), with every free occurrence of \(x\)
+      simultaneously replaced by \(e\).
+
+      \begin{equation*}
+        \AxiomC{\(t_1[x := e] \to t_1'\)}
+        \AxiomC{\(t_2[x := e] \to t_2'\)}
+        \BinaryInfC{\(t_1 + t_2[x := e] \to t_1' + t_2'\)}
+        \DisplayProof
+      \end{equation*}
+
+    \item Write the rules for the operational semantics for this language,
+    assuming \emph{call-by-name} semantics for function calls. In call-by-name
+    semantics, function arguments are not evaluated before the call. Instead,
+    the parameters are merely substituted into the function body.
+
+    \item Under the following environment (with function names, parameters, and
+    bodies):
+      \begin{gather*}
+        (sum, [x], if ~ (x == 0) ~ then ~ 0 ~ else ~ x + sum(x + (-1))) \\
+        (rec, [~], rec()) \\
+        (default, [b, x], if ~ b ~ then ~ x ~ else ~ 0)
+      \end{gather*}
+
+      evaluate each of the following expressions, showing the derivations:
+      \begin{enumerate}
+        \item \(sum(2)\)
+        \item \(if ~(1 == 2) ~ then ~ 3 ~ else ~ 4\)
+        \item \(sum(sum(0))\)
+        \item \(rec()\)
+        \item \(default(false, rec())\)
+      \end{enumerate}
+
+      How would the evaluations in each case change if we used \emph{call-by-value}
+      semantics instead?
+  \end{enumerate}
+
+  \begin{solution}
+    \allowdisplaybreaks
+
+    \begin{enumerate}
+      \item Substitution rules:
+      \begin{gather*}
+        \AxiomC{}
+        \UnaryInfC{\(true[x := e] \to true\)}
+        \DisplayProof \\
+        %
+        \AxiomC{}
+        \UnaryInfC{\(false[x := e] \to false\)}
+        \DisplayProof \\
+        %
+        \AxiomC{}
+        \UnaryInfC{\(\num[x := e] \to \num\)}
+        \DisplayProof \\
+        %
+        \AxiomC{\(t_1[x := e] \to t_1'\)}
+        \AxiomC{\(t_2[x := e] \to t_2'\)}
+        \BinaryInfC{\(t_1 == t_2[x := e] \to t_1' == t_2'\)}
+        \DisplayProof \\
+        %
+        \AxiomC{\(t_1[x := e] \to t_1'\)}
+        \AxiomC{\(t_2[x := e] \to t_2'\)}
+        \BinaryInfC{\(t_1 + t_2[x := e] \to t_1' + t_2'\)}
+        \DisplayProof \\
+        %
+        \AxiomC{\(t_1[x := e] \to t_1'\)}
+        \AxiomC{\(t_2[x := e] \to t_2'\)}
+        \BinaryInfC{\(t_1 ~\&\& ~t_2[x := e] \to t_1' ~\&\& ~t_2'\)}
+        \DisplayProof \\
+        %
+        \AxiomC{\(t_1[x := e] \to t_1'\)}
+        \AxiomC{\(t_2[x := e] \to t_2'\)}
+        \AxiomC{\(t_3[x := e] \to t_3'\)}
+        \TrinaryInfC{\(if ~(t_1) ~t_2 ~else ~t_3[x := e] \to if ~(t_1') ~t_2' ~else ~t_3'\)}
+        \DisplayProof \\
+        %
+        \AxiomC{\(t_1[x := e] \to t_1'\)}
+        \AxiomC{\(\ldots\)}
+        \AxiomC{\(t_n[x := e] \to t_3'\)}
+        \TrinaryInfC{\(f(t_1, \ldots, t_n)[x := e] \to f(t_1', \ldots, t_n')\)}
+        \DisplayProof \\
+        %
+        \AxiomC{}
+        \UnaryInfC{\(x[x := e] \to e\)}
+        \DisplayProof \\
+        %
+        \AxiomC{\(x \neq y\)}
+        \UnaryInfC{\(y[x := e] \to y\)}
+        \DisplayProof
+      \end{gather*}
+
+      \item Operational semantics:
+      \begin{itemize}
+        \item Equality:
+          \begin{gather*}
+            \AxiomC{\(n_1, n_2\) are integer values}
+            \AxiomC{\(n_1 = n_2\)}
+            \BinaryInfC{\(n_1 == n_2 \leadsto true\)}
+            \DisplayProof \\
+            %
+            \AxiomC{\(n_1, n_2\) are integer values}
+            \AxiomC{\(n_1 \neq n_2\)}
+            \BinaryInfC{\(n_1 == n_2 \leadsto false\)}
+            \DisplayProof
+          \end{gather*}
+        \item Addition:
+          \begin{gather*}
+            \AxiomC{\(t_1 \leadsto t_1'\)}
+            \UnaryInfC{\(t_1 + t_2 \leadsto t_1' + t_2\)}
+            \DisplayProof \\
+            %
+            \AxiomC{\(n\) is an integer value}
+            \AxiomC{\(t_2 \leadsto t_2'\)}
+            \BinaryInfC{\(n + t_2 \leadsto n + t_2'\)}
+            \DisplayProof \\
+            %
+            \AxiomC{\(n_1, n_2\) are integer values}
+            \AxiomC{\(n_1 + n_2 = k\)}
+            \BinaryInfC{\(n_1 + n_2 \leadsto k\)}
+            \DisplayProof
+          \end{gather*}
+        \item Conjunction:
+          \begin{gather*}
+            \AxiomC{\(t_1 \leadsto t_1'\)}
+            \UnaryInfC{\(t_1 ~\&\& ~t_2 \leadsto t_1' ~\&\& ~t_2\)}
+            \DisplayProof \\
+            %
+            \AxiomC{}
+            \UnaryInfC{\(true ~\&\&~ t \leadsto t\)}
+            \DisplayProof \\
+            %
+            \AxiomC{}
+            \UnaryInfC{\(false ~\&\&~ t \leadsto false\)}
+            \DisplayProof
+          \end{gather*}
+        \item Conditionals:
+          \begin{gather*}
+            \AxiomC{\(t_1 \leadsto t_1'\)}
+            \UnaryInfC{\(if ~(t_1) ~t_2 ~else ~t_3 \leadsto if ~(t_1') ~t_2 ~else ~t_3\)}
+            \DisplayProof \\
+            %
+            \AxiomC{}
+            \UnaryInfC{\(if ~(true) ~t_2 ~else ~t_3 \leadsto t_2\)}
+            \DisplayProof \\
+            %
+            \AxiomC{}
+            \UnaryInfC{\(if ~(false) ~t_2 ~else ~t_3 \leadsto t_3\)}
+            \DisplayProof
+          \end{gather*}
+        \item Function call:
+          \begin{gather*}
+            \alwaysNoLine
+            \AxiomC{\(b_0\) is the body of \(f\)}
+            \UnaryInfC{\((x_1, \ldots, x_n)\) are parameters of \(f\)}
+            \UnaryInfC{\(b_0[x_1 := t_1] \to b_1 \quad \ldots \quad b_{n-1}[x_n := t_n] \to b_n\)}
+            \alwaysSingleLine
+            \UnaryInfC{\(f(t_1, \ldots, t_n) \leadsto b_n\)}
+            \DisplayProof
+          \end{gather*}
+      \end{itemize}
+
+      \item Evaluations:
+      \begin{enumerate}
+        \item \(sum(2) \leadsto 3\):
+          \begin{align*}
+            &sum(2)\\
+            &\leadsto if ~(2 == 0) ~ then ~ 0 ~ else ~ 2 + sum(2 + (-1))\\
+            &\leadsto if ~(false) ~ then ~ 0 ~ else ~ 2 + sum(2 + (-1))\\
+            &\leadsto 2 + sum(2 + (-1))\\
+            &\leadsto 2 + if ~((2 + (-1)) == 0) ~ then ~ 0 ~ else ~ 1 + sum(2 + (-1))\\
+            &\leadsto 2 + if ~(1 == 0) ~ then ~ 0 ~ else ~ 1 + sum(2 + (-1))\\
+            &\leadsto 2 + if ~(false) ~ then ~ 0 ~ else ~ 1 + sum(2 + (-1) + (-1))\\
+            &\leadsto 2 + (1 + sum(2 + (-1) + (-1)))\\
+            & \ldots \\
+            &\leadsto 2 + (1 + 0) \\
+            &\leadsto 2 + 1 \\
+            &\leadsto 3
+          \end{align*}
+        \item \(sum(sum(0)) \leadsto 0\):
+        \begin{align*}
+          &sum(sum(0))\\
+          &\leadsto if ~(sum(0) == 0) ~ then ~ 0 ~ else ~ 0 + sum(sum(0) + (-1))\\
+          &\leadsto \ldots \textit{(expand \(sum(0)\) in the conditional)} \\
+          &\leadsto if ~(0 == 0) ~ then ~ 0 ~ else ~ 0 + sum(sum(0) + (-1))\\
+          &\leadsto if ~(true) ~ then ~ 0 ~ else ~ 0 + sum(sum(0) + (-1))\\
+          &\leadsto 0
+        \end{align*}
+        \item \(if ~(1 == 2) ~ then ~ 3 ~ else ~ 4 \leadsto 4\).
+        \item \(rec() \leadsto rec()\) (infinite loop).
+        \item \(default(false, rec()) \leadsto 0\).
+      \end{enumerate}
+
+      Under call-by-value-semantics, the structure of the evaluations would be
+      different. In \(sum(sum(0))\), we would evaluate the inner \(sum(0)\) to
+      \(0\) before evaluating the outer \(sum(\cdot)\). In \(default(false,
+      rec())\), we would need to evaluate \(rec()\), which would lead to an
+      infinite loop.
+    \end{enumerate}
+        
+  \end{solution}
+  
+\end{exercise}

info/exercises/src/ex-04/ex/types.tex

+
+% perform actual type derivation of some terms
+
+\begin{exercise}{}
+
+  Consider the following type system for a language with integers, conditionals, pairs, and
+  functions:
+
+  \allowdisplaybreaks
+  \addtolength{\jot}{0.5em}
+  \begin{gather*}
+    \AxiomC{\(n\) is an integer literal}
+    \UnaryInfC{\(\Gamma \vdash n : \lstinline|Int|\)}
+    \DisplayProof \quad
+    % variable
+    \AxiomC{\(x : \tau \in \Gamma\)}
+    \UnaryInfC{\(\Gamma \vdash x : \tau\)}
+    \DisplayProof \\
+    %
+    % addition
+    \AxiomC{\(\Gamma \vdash e_1 : \lstinline|Int|\)}
+    \AxiomC{\(\Gamma \vdash e_2 : \lstinline|Int|\)}
+    \BinaryInfC{\(\Gamma \vdash e_1 + e_2 : \lstinline|Int|\)}
+    \DisplayProof \\
+    %
+    % multiplication
+    \AxiomC{\(\Gamma \vdash e_1 : \lstinline|Int|\)}
+    \AxiomC{\(\Gamma \vdash e_2 : \lstinline|Int|\)}
+    \BinaryInfC{\(\Gamma \vdash e_1 \times e_2 : \lstinline|Int|\)}
+    \DisplayProof \\
+    %
+    % booleans
+    \AxiomC{\(b\) is a boolean literal}
+    \UnaryInfC{\(\Gamma \vdash b : \lstinline|Bool|\)}
+    \DisplayProof \quad
+    \AxiomC{\(\Gamma \vdash e : \lstinline|Bool|\)}
+    \UnaryInfC{\(\Gamma \vdash \lstinline|not e| : \lstinline|Bool|\)}
+    \DisplayProof \\
+    % boolean ops
+    \AxiomC{\(\Gamma \vdash e_1 : \lstinline|Bool|\)}
+    \AxiomC{\(\Gamma \vdash e_2 : \lstinline|Bool|\)}
+    \BinaryInfC{\(\Gamma \vdash e_1 \land e_2 : \lstinline|Bool|\)}
+    \DisplayProof
+    \quad
+    \AxiomC{\(\Gamma \vdash e_1 : \lstinline|Bool|\)}
+    \AxiomC{\(\Gamma \vdash e_2 : \lstinline|Bool|\)}
+    \BinaryInfC{\(\Gamma \vdash e_1 \lor e_2 : \lstinline|Bool|\)}
+    \DisplayProof \\
+    %
+    % conditionals
+    \AxiomC{\(\Gamma \vdash e_1 : \lstinline|Bool|\)}
+    \AxiomC{\(\Gamma \vdash e_2 : \tau\)}
+    \AxiomC{\(\Gamma \vdash e_3 : \tau\)}
+    \TrinaryInfC{\(\Gamma \vdash if ~e_1~ then ~e_2~ else ~e_3 : \tau\)}
+    \DisplayProof \\
+    % pairs
+    \AxiomC{\(\Gamma \vdash e_1 : \tau_1\)}
+    \AxiomC{\(\Gamma \vdash e_2 : \tau_2\)}
+    \BinaryInfC{\(\Gamma \vdash (e_1, e_2) : (\tau_1, \tau_2)\)}
+    \DisplayProof \\
+    %
+    % projections
+    \AxiomC{\(\Gamma \vdash e : (\tau_1, \tau_2)\)}
+    \UnaryInfC{\(\Gamma \vdash fst(e) : \tau_1\)}
+    \DisplayProof
+    \quad
+    \AxiomC{\(\Gamma \vdash e : (\tau_1, \tau_2)\)}
+    \UnaryInfC{\(\Gamma \vdash snd(e) : \tau_2\)}
+    \DisplayProof \\
+    %
+    % function
+    \AxiomC{\(\Gamma \oplus \{x : \tau_1\} \vdash e : \tau_2\)}
+    \UnaryInfC{\(\Gamma \vdash x \Rightarrow e : \tau_1 \to \tau_2\)}
+    \DisplayProof \quad
+    %
+    % application
+    \AxiomC{\(\Gamma \vdash e_1 : \tau_1 \to \tau_2\)}
+    \AxiomC{\(\Gamma \vdash e_2 : \tau_1\)}
+    \BinaryInfC{\(\Gamma \vdash e_1 e_2 : \tau_2\)}
+    \DisplayProof
+    %
+  \end{gather*}
+
+  \pagebreak
+
+  \begin{enumerate}
+    \item Given the following type derivation with type variables \(\tau_1,
+    \ldots, \tau_5\), choose the correct options:
+    \begin{equation*}
+      \AxiomC{\((x, \tau_4) \in \Gamma\)}
+      \UnaryInfC{\(\Gamma \vdash x: \tau_4\)}
+      \UnaryInfC{\(\Gamma \vdash fst(x): \tau_3\)}
+      \AxiomC{\((x, \tau_4) \in \Gamma\)}
+      \UnaryInfC{\(\Gamma \vdash x: \tau_4\)}
+      \UnaryInfC{\(\Gamma \vdash snd(x): \tau_5\)}
+      \BinaryInfC{\(\Gamma \vdash fst(x)(snd(x)) : \tau_2\)}
+      \UnaryInfC{\(\Gamma' \vdash x \Rightarrow fst(x)(snd(x)): \tau_1\)}
+      \DisplayProof
+    \end{equation*}
+
+    \begin{enumerate}
+      \item There are no valid assignments to the type variables such that the
+      above derivation is valid.
+      \item In all valid derivations, \(\tau_2 = \tau_5\).
+      \item There are \emph{no} valid derivations where \(\tau_2 = \lstinline|Int|\).
+      \item In all valid derivations, \(\tau_4 = (\tau_3, \tau_5)\)
+      \item In all valid derivations, \(\tau_2 = \tau_4 \to \tau_1\)
+      \item There is a valid derivation where \(\tau_1 = \tau_2\).
+    \end{enumerate}
+    \item For each of the following pairs of terms and types, provide a valid
+    type derivation or briefly argue why the typing is incorrect:
+    \begin{enumerate}
+      \item \(x \Rightarrow x + 5\): \lstinline|Int| \(\to\) \lstinline|Int|
+      \item \(x \Rightarrow y \Rightarrow x + y\): \lstinline|Int| \(\to\)
+      \lstinline|Int| \(\to\) \lstinline|Int|
+      \item \(x \Rightarrow y \Rightarrow y(2) \times x\): \lstinline|Int| \(\to\)
+      \lstinline|Int| \(\to\) \lstinline|Int|
+      \item \(x \Rightarrow (x, x)\): \lstinline|Int| \(\to\) \lstinline|(Int, Int)|
+      \item \(x \Rightarrow y \Rightarrow if ~fst(x) ~then ~snd(x) ~else~ y\): \lstinline|(Bool, Int)| \(\to\) \lstinline|(Int, Int)| \(\to\) \lstinline|Int|
+      \item \(x \Rightarrow y \Rightarrow if ~y~ then~ (z \Rightarrow y) ~else~ x \): (\lstinline|Bool| \(\to\) \lstinline|Bool|) \(\to\) \lstinline|Bool| \(\to\) (\lstinline|Bool| \(\to\) \lstinline|Bool|)
+      \item \(x \Rightarrow y \Rightarrow if ~y~ then~ (z \Rightarrow y) ~else~ x \): (\lstinline|Int| \(\to\) \lstinline|Bool|) \(\to\) \lstinline|Bool| \(\to\) (\lstinline|Int| \(\to\) \lstinline|Bool|)
+    \end{enumerate}
+
+    \item Prove that there is \emph{no} valid type derivation for the term
+    \begin{equation*}
+      x \Rightarrow if~ fst(x) ~then~ snd(x)~ else~ x
+    \end{equation*}
+  \end{enumerate}
+
+  \begin{solution}
+
+    \begin{enumerate}
+      \item The correct statements are d and e. For the remaining:
+      \begin{itemize}
+        \item \textbf{a}: set \(\tau_2 = \lstinline|Int|\), \(\tau_5 =
+        \lstinline|Bool|\), \(\tau_3 = \tau_5 \to \tau_2\), \(\tau_4 = (\tau_3,
+        \tau_5)\), and \(\tau_1 = \tau_4 \to \tau_2\).
+        \item \textbf{b}: see (a).
+        \item \textbf{c}: see (a).
+        \item \textbf{f}: given \(\tau_1 = \tau_2\), we also know from the rule
+        for lambda abstraction that \(\tau_1 = \tau_4 \to \tau_2\), and hence
+        \(\tau_2 = \tau_4 \to \tau_2\) recursively, which is a contradiction.
+      \end{itemize}
+
+      \item For the given terms and types:
+      \begin{enumerate}
+        \item \(x \Rightarrow x + 5\): \lstinline|Int| \(\to\) \lstinline|Int|: \cmark
+        \begin{equation*}
+          \AxiomC{\(x : \lstinline|Int| \in \Gamma\)}
+          \UnaryInfC{\(\Gamma \vdash x : \lstinline|Int|\)}
+          \AxiomC{}
+          \UnaryInfC{\(\Gamma \vdash 5 : \lstinline|Int|\)}
+          \BinaryInfC{\(\Gamma \vdash x + 5 : \lstinline|Int|\)}
+          \UnaryInfC{\(\Gamma' \vdash x \Rightarrow x + 5 : \lstinline|Int| \to \lstinline|Int|\)}
+          \DisplayProof
+        \end{equation*}
+        \item \(x \Rightarrow y \Rightarrow x + y\): \lstinline|Int| \(\to\)
+        \lstinline|Int| \(\to\) \lstinline|Int|: \cmark
+        \item \(x \Rightarrow y \Rightarrow y(2) \times x\): \lstinline|Int|
+        \(\to\) \lstinline|Int| \(\to\) \lstinline|Int|: \xmark. If \(y\) has
+        type \lstinline|Int|, then \(y(2)\) cannot not well-typed, as the
+        function application rule is not applicable.
+        \item \(x \Rightarrow (x, x)\): \lstinline|Int| \(\to\) \lstinline|(Int, Int)|: \cmark
+        \item \(x \Rightarrow y \Rightarrow if ~fst(x) ~then ~snd(x) ~else~ y\):
+        \lstinline|(Bool, Int)| \(\to\) \lstinline|(Int, Int)| \(\to\)
+        \lstinline|Int|: \xmark. The type of the two branches of a conditional
+        must match, but here they are \lstinline|Int| and (\lstinline|Int|,
+        \lstinline|Int|) respectively.
+        \item \(x \Rightarrow y \Rightarrow if ~y~ then~ (z \Rightarrow y) ~else~ x \): (\lstinline|Bool| \(\to\) \lstinline|Bool|) \(\to\) \lstinline|Bool| \(\to\) (\lstinline|Bool| \(\to\) \lstinline|Bool|): \cmark
+        \begin{equation*}
+          \AxiomC{\((y, \lstinline|Bool|) \in \Gamma\)}
+          \UnaryInfC{\(\Gamma \vdash y : \lstinline|Bool|\)}
+          \AxiomC{\((x, \lstinline|Bool| \to \lstinline|Bool|) \in \Gamma\)}
+          \UnaryInfC{\(\Gamma \vdash x : \lstinline|Bool| \to \lstinline|Bool|\)}
+          \AxiomC{\((y, \lstinline|Bool|) \in \Gamma \oplus \{(z, \lstinline|Bool|)\}\)}
+          \UnaryInfC{\(\Gamma \oplus \{(z, \lstinline|Bool|)\} \vdash y : \lstinline|Bool|\)}
+          \UnaryInfC{\(\Gamma \vdash z \Rightarrow y : \lstinline|Bool| \to \lstinline|Bool|\)}
+          \TrinaryInfC{\(\Gamma \vdash if ~y~ then~ (z \Rightarrow y) ~else~ x : \lstinline|Bool| \to \lstinline|Bool|\)}
+          \UnaryInfC{\(\Gamma' \vdash y \Rightarrow if ~y~ then~ (z \Rightarrow y) ~else~ x : (\lstinline|Bool| \to \lstinline|Bool|) \to \lstinline|Bool| \to (\lstinline|Bool| \to \lstinline|Bool|)\)}
+          \UnaryInfC{\(\Gamma'' \vdash x \Rightarrow y \Rightarrow if ~y~ then~ (z \Rightarrow y) ~else~ x : (\lstinline|Bool| \to \lstinline|Bool|) \to \lstinline|Bool| \to (\lstinline|Bool| \to \lstinline|Bool|)\)}
+          \DisplayProof
+        \end{equation*}
+        Note that the choice of type of \(z\) (and of the argument of \(x\)) is
+        arbitrary. Hence, the next typing is also valid.
+        \item \(x \Rightarrow y \Rightarrow if ~y~ then~ (z \Rightarrow y) ~else~ x \): (\lstinline|Int| \(\to\) \lstinline|Bool|) \(\to\) \lstinline|Bool| \(\to\) (\lstinline|Int| \(\to\) \lstinline|Bool|): \cmark
+      \end{enumerate}
+      \item Non-existence of a valid type derivation for the term:
+      \begin{equation*}
+        t = x \Rightarrow if~ fst(x) ~then~ snd(x)~ else~ x
+      \end{equation*}
+      Assume that there is a valid type derivation for the term. We will attempt
+      to derive a contradiction. We use the fact that if there exists a type
+      derivation, every step must use one of the rules above, and that the types
+      assigned to each variable must be consistent across the derivation.
+      
+      First, \(t\) has a type derivation \emph{if and only if} \(t_1 = if ~
+      fst(x)~then~snd(x)~else~x\) has a type derivation, by using the function
+      abstraction rule. We will work with \(t_1\) directly. The function
+      abstraction rule here does not give us more information.
+
+      Any type derivation for \(t_1\) must end in the conditional rule. For this
+      rule to be applicable, we must have that the following are derivable:
+      \begin{enumerate}
+        \item \(\Gamma \vdash fst(x) : \lstinline|Bool|\)
+        \item \(\Gamma \vdash snd(x) : \tau\)
+        \item \(\Gamma \vdash x : \tau\)
+      \end{enumerate}
+      where the type variable \(\tau\) is also the type of \(t_1\).
+
+      By using the projection rule on (a) and (b), we learn that the type of
+      \(x\) must be \((\lstinline|Bool|, \tau_1)\) and \((\tau_2, \tau)\) for
+      two fresh variables \(\tau_1\) and \(\tau_2\) respectively. Matching the
+      two, as \(x\) may only have one type, we must have \(\tau_1 = \tau\),
+      \(\tau_2 = \lstinline|Bool|\), and thus the type of \(x\) is
+      \((\lstinline|Bool|, \tau)\).
+
+      However, from (c), we learn that the type of \(x\) is \(\tau\). It must be
+      the case that \(\tau = (\lstinline|Bool|, \tau)\). This is not possible
+      for any type \(\tau\), and we have a contradiction.
+
+      Hence, there is no valid type derivation for the term \(t\).
+    \end{enumerate}
+    
+  \end{solution}
+
+\end{exercise}

info/exercises/src/ex-04/main.tex

+\documentclass[a4paper]{article}
+
+\input{../macro}
+
+\ifdefined\ANSWERS
+  \if\ANSWERS1
+    \printanswers
+  \fi
+\fi
+
+\DeclareMathOperator{\half}{half}
+\newcommand{\num}{\ensuremath{\mathbf{num}}}
+
+\title{CS 320 \\ Computer Language Processing\\Exercise Set 4}
+\author{}
+\date{March 26, 2025}
+
+\begin{document}
+\maketitle
+
+% inductive relations
+%% grammars as inductive relations
+\input{ex/grammar}
+
+% operational semantics
+%% old ex 5 problems 1 and 2
+\input{ex/semantics}
+
+% type systems
+%% type derivations
+%% type system exte
+\input{ex/types}
+
+\end{document}

info/exercises/src/macro.tex

@@ -106,10 +106,8 @@
 \newcommand{\naturals}{\mathbb{N}}
 \newcommand{\booleans}{\mathbb{B}}
 
-% church booleans
-\newcommand{\tru}{\lstinline|true|\xspace}
-\newcommand{\fls}{\lstinline|false|\xspace}
-
-% proof systems
-\newcommand{\natded}{\mathcal{N}} % natural deduction
+\usepackage{bussproofs}
 
+\usepackage{pifont}
+\newcommand{\cmark}{\ding{51}}
+\newcommand{\xmark}{\ding{55}}