diff --git a/info/exercises/ex-01-sol.pdf b/info/exercises/ex-01-sol.pdf
index 6db96e35fa1409ca04b404b2066d1f3e8b07b1e1..2e2049988eb84389b9b610df23e3c310b861fb36 100644
Binary files a/info/exercises/ex-01-sol.pdf and b/info/exercises/ex-01-sol.pdf differ
diff --git a/info/exercises/ex-01.pdf b/info/exercises/ex-01.pdf
index eabf51e7daaa98c91df1cca5a6f41b891422b980..7a126198f5a913b939d6bb16d92f731db2ab7ba0 100644
Binary files a/info/exercises/ex-01.pdf and b/info/exercises/ex-01.pdf differ
diff --git a/info/exercises/ex-02-sol.pdf b/info/exercises/ex-02-sol.pdf
index dbf4766ac7b88b695a01b9fb5502092554faa1a3..f0bbb86f699a4483abd89b8bf9a301a2200a3a10 100644
Binary files a/info/exercises/ex-02-sol.pdf and b/info/exercises/ex-02-sol.pdf differ
diff --git a/info/exercises/ex-02.pdf b/info/exercises/ex-02.pdf
index fabcabf82056b21a997ddb12bd4714de2c5390a6..ff45992616866aee932e017d8102d526c57241a1 100644
Binary files a/info/exercises/ex-02.pdf and b/info/exercises/ex-02.pdf differ
diff --git a/info/exercises/ex-03-sol.pdf b/info/exercises/ex-03-sol.pdf
index 7788932de52abb5dcd411ba7159c08e796607303..cf6439b2e78efd58e16ea1fde6a6310762d48629 100644
Binary files a/info/exercises/ex-03-sol.pdf and b/info/exercises/ex-03-sol.pdf differ
diff --git a/info/exercises/ex-03.pdf b/info/exercises/ex-03.pdf
index fa4561a336e6d8fcc225355c8410023e512d0740..3cd23d720f26a412da978946745a4cb7a6c3eaf8 100644
Binary files a/info/exercises/ex-03.pdf and b/info/exercises/ex-03.pdf differ
diff --git a/info/exercises/ex-04-sol.pdf b/info/exercises/ex-04-sol.pdf
new file mode 100644
index 0000000000000000000000000000000000000000..ba9f94c64a1bd5db966ad71fe9b8852c6b07cb8a
Binary files /dev/null and b/info/exercises/ex-04-sol.pdf differ
diff --git a/info/exercises/ex-04.pdf b/info/exercises/ex-04.pdf
new file mode 100644
index 0000000000000000000000000000000000000000..f817598177d5af26702ec14e4c83a9ba0996150b
Binary files /dev/null and b/info/exercises/ex-04.pdf differ
diff --git a/info/exercises/src/ex-04/ex/grammar.tex b/info/exercises/src/ex-04/ex/grammar.tex
new file mode 100644
index 0000000000000000000000000000000000000000..9fe75195547790eb2ee8736fc04101d4f62e9776
--- /dev/null
+++ b/info/exercises/src/ex-04/ex/grammar.tex
@@ -0,0 +1,263 @@
+
+\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}
+
diff --git a/info/exercises/src/ex-04/ex/semantics.tex b/info/exercises/src/ex-04/ex/semantics.tex
new file mode 100644
index 0000000000000000000000000000000000000000..889275d066a44f2afbfb705acd0f9c866530dbe6
--- /dev/null
+++ b/info/exercises/src/ex-04/ex/semantics.tex
@@ -0,0 +1,332 @@
+
+
+\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}
diff --git a/info/exercises/src/ex-04/ex/types.tex b/info/exercises/src/ex-04/ex/types.tex
new file mode 100644
index 0000000000000000000000000000000000000000..7e0f27aa92d14f3f5caf5c4d9a7a95db9078f820
--- /dev/null
+++ b/info/exercises/src/ex-04/ex/types.tex
@@ -0,0 +1,226 @@
+
+% 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}
diff --git a/info/exercises/src/ex-04/main.tex b/info/exercises/src/ex-04/main.tex
new file mode 100644
index 0000000000000000000000000000000000000000..af89da52163f315c9fba2336d43a9095a6d4e366
--- /dev/null
+++ b/info/exercises/src/ex-04/main.tex
@@ -0,0 +1,34 @@
+\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}
diff --git a/info/exercises/src/macro.tex b/info/exercises/src/macro.tex
index 716f8d6e652bf59ef226fa50656b185a67e2397a..fca3008ddd9f5e80b083ab42bd194749db298c43 100644
--- a/info/exercises/src/macro.tex
+++ b/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}}