info/exercises/src/ex-03/ex/prefix.tex

+
+\begin{exercise}{}
+
+  If \(L\) is a regular language, then the set of prefixes of words in \(L\) is
+  also a regular language. Given this fact, from a regular expression for \(L\),
+  we should be able to obtain a regular expression for the set of all prefixes
+  of words in \(L\) as well.
+  
+  We want to do this with a function \(\prefixes\) that is recursive over the
+  structure of the regular expression for \(L\), i.e. of the form:
+  %
+  \begin{align*}
+    \prefixes(\epsilon) &= \epsilon \\
+    \prefixes(a) &= a \mid \epsilon \\
+    \prefixes(r \mid s) &= \prefixes(r) \mid \prefixes(s) \\
+    \prefixes(r \cdot s) &= \ldots \\
+    \prefixes(r^*) &= \ldots \\
+    \prefixes(r^+) &= \ldots
+  \end{align*}
+
+  \begin{enumerate}
+    \item Complete the definition of \(\prefixes\) above by filling in the
+    missing cases.
+    \item Use this definition to find:
+    \begin{enumerate}
+      \item \(\prefixes(ab^*c)\)
+      \item \(\prefixes((a \mid bc)^*)\)
+    \end{enumerate}
+  \end{enumerate}
+
+  \begin{solution}
+    The computation for \(\prefixes(\cdot)\) is similar to the computation of
+    \(\first(\cdot)\) for grammars.
+
+    \begin{enumerate}
+      \item The missing cases:
+      \begin{enumerate}
+        \item \(\prefixes(r \cdot s) = \prefixes(r) \mid r \cdot \prefixes(s)\).
+        Either we have read \(r\) partially, or we have read all of \(r\), and a
+        part of \(s\).
+        \item \(\prefixes(r^*) = r*\cdot\prefixes(r)\). We can
+        consider \(r^* = \epsilon \mid r \mid rr \mid \ldots\), and apply the
+        rules for union and concatenation. Intuitively, if the word has \(n \ge
+        0\) instances of \(r\), we can read \(m < n\) instances of \(r\), and
+        then a prefix of the next instance of \(r\).
+        \item \(\prefixes(r^+) = r^* \cdot \prefixes(r)\). Same as
+        previous. Why does the empty case still appear?
+      \end{enumerate}
+      \item The prefix computations are:
+      \begin{enumerate}
+        \item \(\prefixes(ab^*c) = \epsilon \mid a \mid ab^*(b \mid c \mid \epsilon)\). Computation:
+        \begin{align*}
+          \prefixes(ab^*c) &= \prefixes(a) \mid a\cdot\prefixes(b^*c) & [\text{concatenation}]\\
+                           &= (a \mid \epsilon) \mid a\cdot\prefixes(b^*c) &[a]\\
+                           &= (a \mid \epsilon) \mid a\cdot(\prefixes(b^*) \mid b^*\prefixes(c)) &[\text{concatenation}]\\
+                           &= (a \mid \epsilon) \mid a\cdot(\prefixes(b^*) \mid b^*(c \mid \epsilon)) &[c]\\
+                           &= (a \mid \epsilon) \mid a\cdot(b^*\prefixes(b) \mid b^*(c \mid \epsilon)) &[\text{star}]\\
+                           &= (a \mid \epsilon) \mid a\cdot(b^*(b \mid \epsilon) \mid b^*(c \mid \epsilon)) &[b]\\
+                           &= (a \mid \epsilon) \mid a\cdot(b^*(b \mid c \mid \epsilon)) &[\text{rewrite}]\\
+                           &= \epsilon \mid a \mid a\cdot(b^*(b \mid c \mid \epsilon)) & [\text{rewrite}]\\
+        \end{align*}
+        \item \(\prefixes((a \mid bc)^*) = (a \mid bc)^*(\epsilon \mid a \mid b \mid bc)\).
+      \end{enumerate}
+    \end{enumerate}
+  \end{solution}
+  
+\end{exercise}

info/exercises/src/ex-03/ex/table.tex

+
+% this language is not LL 1 actually, I think
+
+% \begin{exercise}{}
+%   Consider the following grammar of \(\mathbf{if}-\mathbf{then}-\mathbf{else}\) expressions with assignments:
+%   %
+%   \begin{align*}
+%     stmt &::= \mathbf{if} ~id = id~ \mathbf{then} ~stmt ~optStmt \\
+%          &::= \{ stmt^* \} \\
+%          &::= id = id; \\
+%     optStmt &::= \epsilon \mid \mathbf{else} ~stmt \\
+%   \end{align*}
+  
+%   \begin{enumerate}
+%     \item Show that the grammar is ambiguous.
+%     \item Is the grammar LL(1)?
+%   \end{enumerate}
+
+% \end{exercise}
+
+
+\begin{exercise}{}
+  Argue that the following grammar is \emph{not} LL(1). Produce an equivalent
+  LL(1) grammar.
+
+  \begin{equation*}
+    E ::= \mathbf{num} + E \mid \mathbf{num} - E \mid \mathbf{num}
+  \end{equation*}
+
+  \begin{solution}
+    The language is clearly not LL(1), as on seeing a token \(\mathbf{num}\), we
+    cannot decide whether to continue parsing it as \(\mathbf{num} + E\),
+    \(\mathbf{num} - E\), or the end. 
+
+    The notable problem is the common prefix between the rules. We can separate
+    this out by introducing a new non-terminal \(T\). This is a transformation
+    known as \emph{left factorization}.
+
+    \begin{align*}
+      E &::= \mathbf{num} ~T \\
+      T &::= + E \mid - E \mid \epsilon
+    \end{align*}
+
+    % without changing the terms or the overall "structure" of the grammar, we
+    % have logically partitioned it to fit within our parsing schema.
+
+  \end{solution}
+\end{exercise}
+
+\begin{exercise}{}
+  Consider the following grammar:
+
+  \begin{equation*}
+    S ::= S(S) \mid S[S] \mid () \mid [\;]
+  \end{equation*}
+    
+  Check whether the same transformation as the previous case can be applied to
+  produce an LL(1) grammar. If not, argue why, and suggest a different
+  transformation.
+
+  \begin{solution}
+    Applying left factorization to the grammar, we get:
+    \begin{align*}
+      S &::= S ~T \mid S ~T \mid () \mid [\;] \\
+      T &::= (S) \mid [S]
+    \end{align*}
+
+    This is not LL(1), as on reading a token ``\((\)'', we cannot decide whether
+    this is the final parentheses (base case) in the expression, or whether
+    there is a \(T\) following it.
+
+    The problem is that this version of the grammar is left-recursive. A
+    recursive-descent parser for this grammar would loop forever on the first
+    rule. This is caused by the fact that our parsers are top-down, left to
+    right. We can fix this by \emph{moving} the recursion to the right. This is
+    generally called \emph{left recursion elimination}.
+
+    Transformed grammar steps (explanation below):
+    \begin{align*}
+      S &::= ()S' \mid [\;]S' \\
+      S' &::= (S)S' \mid [S]S' \mid \epsilon
+    \end{align*}
+
+    To eliminate left-recursion in general, consider a non-terminal \(A ::=
+    A\alpha \mid \beta\), where \(\beta\) does not start with \(A\) (not
+    left-recursive). We can remove the left recursion by introducing a new
+    non-terminal, \(A'\), such that:
+    \begin{align*}
+      A &::= \beta A' \\
+      A' &::= \alpha A' \mid \epsilon
+    \end{align*}
+    i.e., for the left-recursive rule \(A\alpha\), we instead attempt to parse
+    an \(\alpha\) followed by the rest. In exchange, the base case \(\beta\) now
+    expects an \(A'\) to follow it.
+    %
+    Note that \(\beta\) can be empty as well.
+    
+    Intuitively, we are shifting the direction in which we look for instances of
+    \(A\). Consider a partial derivation starting from \(\beta \alpha \alpha
+    \alpha\). The original version of the grammar would complete the parsing as:
+    \begin{center}
+      \begin{forest}
+        [\(A\)
+          [\(A\)
+            [\(A\)
+              [\(A\)
+                [\(\beta\)]
+              ]
+              [\(\alpha\)]
+            ]
+            [\(\alpha\)]
+          ]
+          [\(\alpha\)]
+        ]     
+      \end{forest}
+    \end{center}
+    but with the new grammar, we parse it as:
+    \begin{center}
+      \begin{forest}
+        [\(A\)
+          [\(\beta\)]
+          [\(A'\)
+            [\(\alpha\)]
+            [\(A'\)
+              [\(\alpha\)]
+              [\(A'\)
+                [\(\alpha\)]
+                [\(A'\)
+                  [\(\epsilon\)]
+                ]
+              ]
+            ]
+          ]
+        ]
+      \end{forest}
+    \end{center}
+
+    There are two main pitfalls to remember with left-recursion elimination:
+    \begin{enumerate}
+      \item it may need to be applied several times till the grammar is
+      unchanged, as the first transformation may introduce new (indirect)
+      recursive rules (check \(A ::= AA\alpha \mid \epsilon\)).
+      \item it may require \emph{inlining} some non-terminals, when the left
+      recursion is \emph{indirect}. For example, consider \(A ::= B\alpha, B ::=
+      A\beta\), where there is no immediate reduction to do, but inlining \(B\),
+      we get \(A ::= A\beta\alpha\), where the elimination can be applied.
+    \end{enumerate}
+  \end{solution}
+
+\end{exercise}

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

+\documentclass[a4paper]{article}
+
+\input{../macro}
+
+\ifdefined\ANSWERS
+  \if\ANSWERS1
+    \printanswers
+  \fi
+\fi
+
+\DeclareMathOperator{\prefixes}{prefixes}
+\DeclareMathOperator{\first}{first}
+\DeclareMathOperator{\nullable}{nullable}
+\DeclareMathOperator{\follow}{follow}
+
+\title{CS 320 \\ Computer Language Processing\\Exercise Set 3}
+\author{}
+\date{March 19, 2025}
+
+\begin{document}
+\maketitle
+
+% prefixes of regular expressions
+\input{ex/prefix}
+
+% compute nullable follow first for CFGs
+\input{ex/compute}
+
+% build ll1 parsing table, parse or attempt to parse some strings
+\input{ex/table}
+
+\end{document}

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) \mid \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 \subseteq 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. You may assume
+    that function parameters are named distinctly from variables in the program.
+
+    \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{\(t_1 \leadsto t_1'\)}
+            \UnaryInfC{\(t_1 == t_2 \leadsto t_1' == t_2\)}
+            \DisplayProof \\
+            %
+            \AxiomC{\(n_1\) is an integer value}
+            \AxiomC{\(t_2 \leadsto t_2'\)}
+            \BinaryInfC{\(n_1 == t_2 \leadsto n_1 == t_2'\)}
+            \DisplayProof \\
+            \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 ~ 2 + (-1) + sum(2 + (-1) + (-1))\\
+            &\leadsto 2 + if ~(1 == 0) ~ then ~ 0 ~ else ~ 2 + (-1) + sum(2 + (-1) + (-1))\\
+            &\leadsto 2 + if ~(false) ~ then ~ 0 ~ else ~ 2 + (-1) + sum(2 + (-1) + (-1))\\
+            &\leadsto 2 + (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_1 = \tau_4 \to \tau_2\).
+      \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/ex-05/ex/check.tex

+
+% do type checking for some simple terms
+
+\pagebreak
+\begin{exercise}{}
+  For each of the following term-type pairs \((t, \tau)\), check whether the
+  term can be ascribed with the given type, i.e., whether there exists a
+  derivation of \(\Gamma \vdash t: \tau\) for some typing context \(\Gamma\) in
+  the given system. If not, briefly argue why.
+
+  \begin{enumerate}
+    \item \(\lstinline|x|, \abool\)
+    \item \(\lstinline|x| + 1, \aint\)
+    \item \(\lstinline|(x && y)  ==  (x <=  0)|, \abool\)
+    \item \(\lstinline|f| ~\ato~ \lstinline|x| ~\ato~ \lstinline|y| ~\ato~ \lstinline|f((x, y))|\): 
+    
+    \lstinline|((List[Int], Bool) => Int) => List[Int] => Bool => Int|
+    \item \lstinline|Cons(x, x)| : \lstinline|List[List[Int]]|
+  \end{enumerate}
+
+  \begin{solution}
+    \begin{enumerate}
+      \item \lstinline|x, Bool|. Derivation, assume \lstinline|x| is a boolean:
+      \begin{equation*}
+        \AxiomC{\((\lstinline|x|, \abool) \in \{(\lstinline|x|, \abool)\}\)}
+        \UnaryInfC{\(\{(\lstinline|x|, \abool)\} \vdash \lstinline|x: Bool|\)}
+        \DisplayProof
+      \end{equation*}
+      Note that this would work with any type, as there are no constraints.
+      \item \(\lstinline|x| + 1, \aint\). Derivation, assume \lstinline|x| is an
+      integer:
+      \begin{equation*}
+        \AxiomC{\((\lstinline|x|, \aint) \in \{(\lstinline|x|, \aint)\}\)}
+        \UnaryInfC{\(\{(\lstinline|x|, \aint)\} \vdash \lstinline|x: Int|\)}
+        \AxiomC{\(1 \in \naturals\)}
+        \UnaryInfC{\(\{(\lstinline|x|, \aint)\} \vdash \lstinline|1: Int|\)}
+        \BinaryInfC{\(\{(\lstinline|x|, \aint)\} \vdash \lstinline|x + 1: Int|\)}
+        \DisplayProof
+      \end{equation*}
+      Due to addition constraining the type of \lstinline|x|, other possible
+      types would not work.
+      \item \(\lstinline|(x && y)  ==  (x <=  0)|, \abool\). Not well-typed.
+      From the left-hand side, we would enforce that \lstinline|x: Bool|, but on
+      the right, we find \lstinline|x: Int|. Due to this conflict, there is no
+      valid derivation for this term.
+      \item \lstinline|f => x => y => f((x, y))|: this is the currying function.
+      Note that it will conform to \lstinline|((a, b) => c) => a => b => c| for any choice 
+      of \lstinline|a|, \lstinline|b|, and \lstinline|c|. (check)
+      \item \lstinline|Cons(x, x)| : \lstinline|List[List[Int]]|. Not
+      well-typed. The \(cons\) rule tells us that the second argument must have
+      the same type as the result, so \lstinline|x: List[List[Int]]|, but the first
+      argument enforces the type to be \lstinline|List[Int]| (again, due to result
+      type). As \(\aint \neq \alist{\aint}\), this is not well-typed.
+
+      Note that the singular assignment of \lstinline|x| to \lstinline|Nil()|
+      can make a well typed term here, but the typing must hold for \emph{all}
+      possible values of \lstinline|x|.
+    \end{enumerate}
+  \end{solution}
+  
+\end{exercise}

info/exercises/src/ex-05/ex/map.tex

+
+\begin{exercise}{}
+  Consider the following term \(t\):
+  %
+  \begin{center}
+    \(t = \) \lstinline{l =>  map(l)(x =>  fst(x)(snd(x))  + snd(x))}
+    % t = \lstinline|l| ~\ato~ \lstinline|map|(\lstinline|l|, \lstinline|x| ~\ato~ \afst{\lstinline|x|}(\asnd{\lstinline|x|}) + \asnd{\lstinline|x|})
+  \end{center}
+
+  where \lstinline|map| is a function with type \(\forall \tau, \pi.\;
+  \alist{\tau} ~\ato~ (\tau ~\ato~ \pi) ~\ato~ \alist{\pi}\).
+
+  \begin{enumerate}
+    \item Label and assign type variables to each subterm of \(t\).
+    \item Generate the constraints on the type variables, assuming \(t\) is
+    well-typed, to infer the type of \(t\).
+    \item Solve the constraints via unification to deduce the type of \(t\).
+  \end{enumerate}
+  
+  \begin{solution}
+    \begin{enumerate}
+      \item We can label the subterms in the following way:
+      \begin{gather}
+        t: \tau = \lstinline|l =>  map(l)(x =>  fst(x)(snd(x))  + snd(x))| \\
+        t_1: \tau_1 = \lstinline|map(l)(x =>  fst(x)(snd(x))  + snd(x))| \\
+        t_2: \tau_2 = \lstinline|x =>  fst(x)(snd(x))  + snd(x)| \\
+        t_3: \tau_3 = \lstinline|fst(x)(snd(x)) + snd(x)| \\
+        t_4: \tau_4 = \lstinline|fst(x)(snd(x))| \\
+        t_5: \tau_5 = \lstinline|snd(x)| \\
+        t_6: \tau_6 = \lstinline|fst(x)| \\
+        \lstinline|l|: \tau_7 = \lstinline|l| \\
+        \lstinline|x|: \tau_8 = \lstinline|x| \\
+        \lstinline|map|: \tau_9 = \lstinline|map|
+      \end{gather}
+      We can choose to separately label \lstinline|x|, \lstinline|l|, and
+      \lstinline|map|, but it does not make any difference to the result.
+
+      \item
+      Inserting the type of \lstinline|map| (thus removing \(\tau_9\)), and
+      adding constraints by looking at the top-level of each subterm, we can get
+      the set of initial constraints, labelled by the subterm equation above
+      they come from:
+      \begin{gather*}
+        \tau = \tau_7 ~\ato~ \tau_1 \tag{1} \\
+        \tau_1 = \alist{\tau_3} \tag{2, 4} \\
+        \tau_7 = \alist{\tau_8} \tag{2, 9} \\
+        \tau_2 = \tau_8 ~\ato~ \tau_3 \tag{3} \\
+        \tau_3 = \aint \tag{4} \\
+        \tau_4 = \aint \tag{4} \\
+        \tau_5 = \aint \tag{4} \\
+        \tau_6 = \tau_5 ~\ato~ \tau_4 \tag{5} \\
+        \tau_8 = (\tau_5', \tau_5) \tag{6} \\
+        \tau_8 = (\tau_6, \tau_6') \tag{7}
+      \end{gather*}
+      for fresh type variables \(\tau_5'\) and \(\tau_6'\) arising from the rule
+      for pairs.
+
+      \item 
+      The constraints can be solved step-by-step (major steps shown):
+      \begin{enumerate}
+        \item Eliminating known types (\(\tau_3, \tau_4, \tau_5\)):
+        \begin{gather*}
+          \tau = \tau_7 ~\ato~ \tau_1  \\
+          \tau_1 = \alist{\aint} \\
+          \tau_7 = \alist{\tau_8} \\
+          \tau_2 = \tau_8 ~\ato~ \aint  \\
+          \tau_6 = \aint ~\ato~ \aint \\
+          \tau_8 = (\tau_5', \aint) \\
+          \tau_8 = (\tau_6, \tau_6')
+        \end{gather*}
+        \item Eliminating \(\tau_1, \tau_6\):
+        \begin{gather*}
+          \tau = \tau_7 ~\ato~ \alist{\aint}  \\
+          \tau_7 = \alist{\tau_8} \\
+          \tau_2 = \tau_8 ~\ato~ \aint  \\
+          \tau_8 = (\tau_5', \aint) \\
+          \tau_8 = (\aint ~\ato~ \aint, \tau_6')
+        \end{gather*}
+        \item Eliminating \(\tau_8\) using either of its equations:
+        \begin{gather*}
+          \tau = \tau_7 ~\ato~ \alist{\aint}  \\
+          \tau_7 = \alist{(\tau_5', \aint)} \\
+          \tau_2 = (\tau_5', \aint) ~\ato~ \aint  \\
+          (\tau_5', \aint) = (\aint ~\ato~ \aint, \tau_6')
+        \end{gather*}
+        \item Performing unification of the pair type:
+        \begin{gather*}
+          \tau = \tau_7 ~\ato~ \alist{\aint}  \\
+          \tau_7 = \alist{(\tau_5', \aint)} \\
+          \tau_2 = (\tau_5', \aint) ~\ato~ \aint  \\
+          \tau_5' = \aint ~\ato~ \aint \\
+          \aint  = \tau_6'
+        \end{gather*}
+        \item Eliminating \(\tau_5'\) and \(\tau_6'\):
+        \begin{gather*}
+          \tau = \tau_7 ~\ato~ \alist{\aint}  \\
+          \tau_7 = \alist{(\aint ~\ato~ \aint, \aint)} \\
+          \tau_2 = (\aint ~\ato~ \aint, \aint) ~\ato~ \aint
+        \end{gather*}
+        \item Eliminating \(\tau_2, \tau_7\):
+        \begin{gather*}
+          \tau = \alist{(\aint ~\ato~ \aint, \aint)} ~\ato~ \alist{\aint}
+        \end{gather*}
+        \item Finally, all type variables are assigned, as we eliminate \(\tau\):
+        \begin{gather*}
+          \emptyset \text{ (no constraints left)}
+        \end{gather*}
+      \end{enumerate}
+
+      The type of \(t\) as discovered by the unification process is:
+      \begin{gather*}
+        \tau = \alist{(\aint ~\ato~ \aint, \aint)} ~\ato~ \alist{\aint}
+      \end{gather*}
+    \end{enumerate}
+  \end{solution}
+
+\end{exercise}

info/exercises/src/ex-05/ex/program.tex

+
+\begin{exercise}{}
+
+  A \emph{program} is a top-level expression \(t\) accompanied by a set of
+  user-provided function definitions. The program is well-typed if each of the
+  function bodies conform to the type of the function, and the top-level
+  expression is well-typed in the context of the function definitions.
+
+  For each of the following function definitions, check whether the function
+  body is well-typed:
+  %
+  \begin{enumerate}
+    \item \lstinline|def f(x: Int)(y: Int): Bool =  x <= y|
+    \item \lstinline|def rec(x: Int): Int =  rec(x)|
+    \item \lstinline|def fib(n: Int): Int = if n <=  1 then 1 else (fib(n - 1)  + fib(n - 2))|
+  \end{enumerate}
+
+  \begin{solution}
+    \begin{enumerate}
+      \item Well-typed, apply rule \(Leq\).
+      \item Well-typed. We need to check if the body conforms to the output
+      type, if we know the function and its parameters have their ascribed type.
+      So, under the context \lstinline|rec: Int => Int, x: Int|, we need to
+      prove that \lstinline|rec(x): Int|. This follows from the \(app\) rule.
+
+      So, if we allow recursion and do not check for termination, we can prove
+      unexpected things using the non-terminating programs.
+      \item Well-typed. We need to produce a derivation of the following:
+      \begin{equation*}
+        \lstinline|fib: Int => Int|, \lstinline|n: Int| \vdash \lstinline|if n <=  1 then 1 else (fib(n - 1)  + fib(n - 2)): Int|
+      \end{equation*} 
+      i.e., given that \lstinline|fib| inductively has type \lstinline|Int => Int| and
+      the parameter \lstinline|n| has type \lstinline|Int|, we need to prove that the
+      body of the function has the ascribed type \lstinline|Int|.
+       
+      The derivation can be constructed by following the structure of the term
+      on the right-hand side, the body. We set \(\Gamma = 
+      %
+      \lstinline|fib: Int => Int|, \lstinline|n: Int|\) for brevity. The \lstinline|n-2|
+      branch is skipped due to space and being the same as the \lstinline|n-1| branch.
+      \begin{equation*}
+        \hspace*{-4cm}
+        \AxiomC{\((\lstinline|n|, \aint) \in \Gamma\)}
+        \UnaryInfC{\(\Gamma \vdash \lstinline|n: Int|\)}
+        \AxiomC{\(1 \in \naturals\)}
+        \UnaryInfC{\(\Gamma \vdash \lstinline|1: Int|\)}
+        \BinaryInfC{\(\Gamma \vdash \lstinline|n <= 1: Bool|\)}
+        %
+        \AxiomC{\(1 \in \naturals\)}
+        \UnaryInfC{\(\Gamma \vdash \lstinline|1: Int|\)}
+        %
+        \AxiomC{\((\lstinline|fib, Int => Int|) \in \Gamma\)}
+        \UnaryInfC{\(\Gamma \vdash \lstinline|fib: Int => Int|\)}
+        \AxiomC{\((\lstinline|n|, \aint) \in \Gamma\)}
+        \UnaryInfC{\(\Gamma \vdash \lstinline|n: Int|\)}
+        \AxiomC{\(1 \in \naturals\)}
+        \UnaryInfC{\(\Gamma \vdash \lstinline|1: Int|\)}
+        \BinaryInfC{\(\Gamma \vdash \lstinline|(n - 1): Int|\)}
+        \BinaryInfC{\(\Gamma \vdash \lstinline|fib(n - 1): Int|\)}
+        %
+        \AxiomC{\ldots}
+        \UnaryInfC{\(\Gamma \vdash \lstinline|fib(n - 2): Int|\)}
+        %
+        \BinaryInfC{\(\Gamma \vdash \lstinline|fib(n - 1) + fib(n - 2): Int|\)}
+        %
+        \TrinaryInfC{\(\Gamma \vdash \lstinline|if n <=  1 then 1 else (fib(n - 1)  + fib(n - 2)): Int|\)}
+        \DisplayProof
+      \end{equation*}
+    \end{enumerate}
+    
+  \end{solution}
+  
+\end{exercise}

info/exercises/src/ex-05/ex/rec-inf.tex

+
+
+\pagebreak
+\begin{exercise}{}
+
+  Consider the following definition for a recursive function \(g\):
+
+  \begin{equation*}
+    \lstinline|def g(n)(x)  = if n <=  2 then (x, x)  else (x, g(n - 1)(x))|
+  \end{equation*}
+
+  \begin{enumerate}
+    \item Evaluate \(g(3)(1)\) and \(g(4)(2)\) using the definition of \(g\).
+      Suggest a type for the function \(g\) based on your observations.
+    \item Label and assign type variables to the definition parameters, body,
+      and its subterms.
+    \item Generate the constraints on the type variables, assuming the
+      definition of \(g\) is well-typed.
+    \item Attempt to solve the generated constraints via unification. Argue how
+    the result correlates to your observations from evaluating \(g\).
+  \end{enumerate}
+  
+  \begin{solution}
+    \begin{enumerate}
+      \item \lstinline|g(3)(1)| evaluates to \lstinline|(1, (1, 1))| and
+      \lstinline|g(4)(2)| evaluates to \lstinline|(2, (2, (2, 2)))|. Notably,
+      these two come from disjoint types. This suggests that the function \(g\)
+      is not well-typed.
+      \item We can label the parameters, subterms, and assign a type to the
+      function:
+      \setcounter{equation}{0}
+      \begin{gather}
+        \lstinline|g|: \tau \\
+        \lstinline|n|: \tau_n \\
+        \lstinline|x|: \tau_x \\
+        body: \tau_1 = \lstinline|if n <=  2 then (x, x)  else (x, g(n - 1)(x))| \\
+        t_1: \tau_2 = \lstinline|n <=  2| \\
+        t_2: \tau_3 = \lstinline|(x, x)| \\
+        t_3: \tau_4 = \lstinline|(x, g(n - 1)(x))| \\
+        t_4: \tau_5 = \lstinline|g(n - 1)(x)| \\
+        t_5: \tau_6 = \lstinline|n - 1|
+      \end{gather}
+      \item We can generate the constraints by looking at the top-level of each
+      subterm equation:
+      \begin{gather*}
+        \tau = \tau_n ~\ato~ \tau_x ~\ato~ \tau_1 \tag{1, def} \\
+        \tau_1 = \tau_3 \tag{4} \\
+        \tau_1 = \tau_4 \tag{4} \\
+        \tau_2 = \abool \tag{4} \\
+        \tau_n = \aint \tag{5} \\
+        \tau_3 = (\tau_x, \tau_x) \tag{6} \\
+        \tau_4 = (\tau_x, \tau_5) \tag{6} \\
+        \tau_5 = \tau_1 \tag{7, def} \\
+        \tau_6 = \aint \tag{9}
+      \end{gather*}
+      \item The constraints can be solved (eliminating \(\tau_4, \tau_5\)) to
+      reach a set of constraints containing the recursive constraint \(\tau_1 =
+      (\tau_x, \tau_1)\). There is no type \(\tau_1\) (the output type of
+      \lstinline|g|!) satisfying this. 
+
+      This matches our previous observation where \lstinline|g| produced two
+      different sized tuples as its output. 
+    \end{enumerate}
+  \end{solution}
+  
+\end{exercise}
\ No newline at end of file

info/exercises/src/ex-05/ex/system.tex

+
+% we want lists, pairs
+% both parametric
+% we want some functions, as well as function definitions
+% we want to be able to define and typecheck recursive functions
+
+Consider a type system for a simple functional language, consisting of integers,
+booleans, parametric pairs, and lists. The rest of the exercises will revolve
+around this system.
+
+% language components
+\newcommand{\aint}{\lstinline|int|}
+\newcommand{\abool}{\lstinline|bool|}
+\newcommand{\aif}{\lstinline|if|}
+\newcommand{\athen}{\lstinline|then|}
+\newcommand{\aelse}{\lstinline|else|}
+\newcommand{\apair}[2]{(#1, #2)}
+\newcommand{\afst}[1]{\lstinline|fst|(#1)}
+\newcommand{\asnd}[1]{\lstinline|snd|(#1)}
+\newcommand{\alist}[1]{\lstinline|List[|#1\lstinline|]|}
+\newcommand{\anil}{\lstinline|Nil()|}
+\newcommand{\acons}[2]{\lstinline|Cons(|#1, #2\lstinline|)|}
+\newcommand{\ato}{\lstinline|=>|}
+
+%%% Actual type system
+\begin{gather*}
+  % variables
+  \AxiomC{\((x, \tau) \in \Gamma\)}
+  \RightLabel{(var)}
+  \UnaryInfC{\(\Gamma \vdash x : \tau\)}
+  \DisplayProof \\
+  % integers
+  \AxiomC{\(n\) is an integer value}
+  \RightLabel{(int)}
+  \UnaryInfC{\(\Gamma \vdash n : \aint\)}
+  \DisplayProof \\
+  % + -
+  \AxiomC{\(e_1 : \aint\)}
+  \AxiomC{\(e_2 : \aint\)}
+  \RightLabel{(+)}
+  \BinaryInfC{\(\Gamma \vdash e_1 + e_2 : \aint\)}
+  \DisplayProof \qquad
+  \AxiomC{\(e_1 : \aint\)}
+  \AxiomC{\(e_2 : \aint\)}
+  \RightLabel{(-)}
+  \BinaryInfC{\(\Gamma \vdash e_1 - e_2 : \aint\)}
+  \DisplayProof \\
+  % booleans
+  \AxiomC{\(b\) is a boolean value}
+  \RightLabel{(bool)}
+  \UnaryInfC{\(\Gamma \vdash \abool(b) : \abool\)}
+  \DisplayProof \\
+  % props
+  \AxiomC{\(\Gamma \vdash e_1 : \abool\)}
+  \AxiomC{\(\Gamma \vdash e_2 : \abool\)}
+  \RightLabel{(and)}
+  \BinaryInfC{\(\Gamma \vdash e_1 \land e_2 : \abool\)}
+  \DisplayProof \qquad
+  \AxiomC{\(\Gamma \vdash e_1 : \abool\)}
+  \AxiomC{\(\Gamma \vdash e_2 : \abool\)}
+  \RightLabel{(or)}
+  \BinaryInfC{\(\Gamma \vdash e_1 \lor e_2 : \abool\)}
+  \DisplayProof \\
+  \AxiomC{\(\Gamma \vdash e_1 : \abool\)}
+  \RightLabel{(not)}
+  \UnaryInfC{\(\Gamma \vdash \neg e_1 : \abool\)}
+  \DisplayProof \\
+  % predicates
+  %% eq
+  \AxiomC{\(\Gamma \vdash e_1 : \tau\)}
+  \AxiomC{\(\Gamma \vdash e_2 : \tau\)}
+  \RightLabel{(eq)}
+  \BinaryInfC{\(\Gamma \vdash e_1 \lstinline|=| e_2 : \abool\)}
+  \DisplayProof \qquad
+  %% lte
+  \AxiomC{\(\Gamma \vdash e_1 : \aint\)}
+  \AxiomC{\(\Gamma \vdash e_2 : \aint\)}
+  \RightLabel{(lte)}
+  \BinaryInfC{\(\Gamma \vdash e_1 \lstinline|<=| e_2 : \abool\)}
+  \DisplayProof \\
+  % ite
+  \AxiomC{\(\Gamma \vdash e_1 : \abool\)}
+  \AxiomC{\(\Gamma \vdash e_2 : \tau\)}
+  \AxiomC{\(\Gamma \vdash e_3 : \tau\)}
+  \RightLabel{(ite)}
+  \TrinaryInfC{\(\Gamma \vdash \aif \, e_1 \, \athen \, e_2 \, \aelse \, e_3 : \tau\)}
+  \DisplayProof \\
+  % pairs
+  \AxiomC{\(\Gamma \vdash e_1 : \tau_1\)}
+  \AxiomC{\(\Gamma \vdash e_2 : \tau_2\)}
+  \RightLabel{(pair)}
+  \BinaryInfC{\(\Gamma \vdash \apair{e_1}{e_2} : \apair{\tau_1}{\tau_2}\)}
+  \DisplayProof \\
+  % fst
+  \AxiomC{\(\Gamma \vdash e : \apair{\tau_1}{\tau_2}\)}
+  \RightLabel{(fst)}
+  \UnaryInfC{\(\Gamma \vdash \afst{e} : \tau_1\)}
+  \DisplayProof \qquad
+  % snd
+  \AxiomC{\(\Gamma \vdash e : \apair{\tau_1}{\tau_2}\)}
+  \RightLabel{(snd)}
+  \UnaryInfC{\(\Gamma \vdash \asnd{e} : \tau_2\)}
+  \DisplayProof \\
+  % lists
+  \AxiomC{\phantom{\(e \in \alist{\tau}\)}}
+  \RightLabel{(nil)}
+  \UnaryInfC{\(\Gamma \vdash \anil : \alist{\tau}\)}
+  \DisplayProof \qquad
+  \AxiomC{\(\Gamma \vdash e_1 : \tau\)}
+  \AxiomC{\(\Gamma \vdash e_2 : \alist{\tau}\)}
+  \RightLabel{(cons)}
+  \BinaryInfC{\(\Gamma \vdash \acons{e_1}{e_2} : \alist{\tau}\)}
+  \DisplayProof \\
+  % functions
+  \AxiomC{\(\Gamma, x : \tau_1 \vdash e : \tau_2\)}
+  \RightLabel{(fun)}
+  \UnaryInfC{\(\Gamma \vdash \lambda x : \tau_1 ~\ato~ e : \tau_1 ~\ato~ \tau_2\)}
+  \DisplayProof \qquad
+  % application
+  \AxiomC{\(\Gamma \vdash e_1 : \tau_1 ~\ato~ \tau_2\)}
+  \AxiomC{\(\Gamma \vdash e_2 : \tau_1\)}
+  \RightLabel{(app)}
+  \BinaryInfC{\(\Gamma \vdash e_1 \, e_2 : \tau_2\)}
+  \DisplayProof \\
+\end{gather*}

info/exercises/src/ex-05/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 5}
+\author{}
+\date{April 02, 2025}
+
+\begin{document}
+\maketitle
+
+% type system
+% do some type checking
+% some unification
+% some inference
+\input{ex/system}
+
+\input{ex/check}
+
+\input{ex/program}
+
+\input{ex/map}
+
+\input{ex/rec-inf}
+
+\end{document}

info/exercises/src/ex-review/ex/ll1.tex

+
+\begin{exercise}{2016}
+  Consider the grammar:
+  \begin{align*}
+    decl &::= varDecl \mid funDecl \\
+    varDecl &::= type ~\lstinline|ID|; \\
+    funDecl &::= type ~\lstinline|ID|~ ( optIDs ); \\
+    optIDs &::= \epsilon \mid IDs \\
+    IDs &::= \lstinline|ID| \mid IDs ~\lstinline|ID| \\
+    type &::= \lstinline|int| \mid type \lstinline|*| \\
+  \end{align*}
+
+  Note that \(type\lstinline|*|\) is \(type\) followed by the terminal
+  \(\lstinline|*|\), not a Kleene star.
+
+  \begin{enumerate}
+    \item Compute \(\nullable\) and \(\first\) for each non-terminal of the grammar above.
+    \begin{solution}
+      Only \(optIDs\) is nullable. The first sets are:
+      %
+      \begin{gather*}
+        \first(decl) = \{\lstinline|int|\} \\
+        \first(varDecl) = \{\lstinline|int|\} \\
+        \first(funDecl) = \{\lstinline|int|\} \\
+        \first(optIDs) = \{\lstinline|ID|\} \\
+        \first(IDs) = \{\lstinline|ID|\} \\
+        \first(type) = \{\lstinline|int|\}
+      \end{gather*}
+    \end{solution}
+    \item Explain why the grammar is not LL(1).
+    \begin{solution}
+      \(decl\), \(IDs\), and \(type\) each have two rules with the same
+      \(\first\) set. 
+    \end{solution}
+    \item Give an LL(1) grammar describing the same sequences of tokens as the
+    previous grammar.
+    \begin{solution}
+      We can remove the common prefix from \(decl\):
+      \begin{gather*}
+        decl = type~\lstinline|ID|~decl' \\
+        decl' = \lstinline|;| \mid \lstinline|(| ~optIDs~\lstinline|);|
+      \end{gather*}
+
+      We can remove the left recursion from the \(IDs\) rule:
+      \begin{gather*}
+        IDs = \lstinline|ID| ~IDs' \\
+        IDs' = \epsilon \mid \lstinline|ID| ~IDs'
+      \end{gather*}
+
+      We can also remove the left recursion from the \(type\) rule:
+      \begin{gather*}
+        type = \lstinline|int| ~type' \\
+        type' = \epsilon \mid \lstinline|*| ~type'
+      \end{gather*}
+
+      Note that \(IDs\) can be followed only by a closing parenthesis.
+    \end{solution}
+  \end{enumerate}
+\end{exercise}
+
+\begin{exercise}{2022}
+  Consider the following grammar with non-terminals \(S\) and \(A\) and
+  terminals \(\eof, (, ), [, \text{ and }]\):
+
+  \begin{align*}
+    S &::= A ~\eof \\
+    A &::= (A) ~A \mid A~[A] \mid \epsilon
+  \end{align*}
+
+  \begin{enumerate}
+    \item Choose all true statements about the grammar above:
+    \begin{enumerate}
+      \item \(``[]()([)]"\) is accepted by the grammar.
+      \item The grammar is LL(1).
+      \item The grammar is ambiguous. \ifAns{\checkmark}
+      \item \(\nullable(A) = true\). \ifAns{\checkmark}
+      \item \(\nullable(S) = true\).
+    \end{enumerate}
+    \item Choose the correct option:
+    \begin{enumerate}
+      \item \(\first(S) = \{\eof\}\)
+      \item \(\first(S) = \{(, [\}\)
+      \item \(\first(S) = \{(, ), \eof\}\)
+      \item \(\first(S) = \{(, [, \eof\}\) \ifAns{\checkmark}
+      \item \(\first(S) = \{(,), [,], \eof\}\)
+    \end{enumerate}
+    \item Choose the correct option:
+    \begin{enumerate}
+      \item \(\follow(A) = \{), ]\}\)
+      \item \(\follow(A) = \{), ], \eof\}\)
+      \item \(\follow(A) = \{(, [, ), ]\}\)
+      \item \(\follow(A) = \{(, [, ], \eof\}\)
+      \item \(\follow(A) = \{(, [, ), ], \eof\}\)
+    \end{enumerate}
+    \ifAns{None of the above are correct; \(\follow(A) = \{), [, ], \eof\}\)}
+  \end{enumerate}
+\end{exercise}

info/exercises/src/ex-review/ex/regex.tex

+
+\begin{exercise}{2016}
+  Let \(\Sigma = \{a, b\}\) for distinct \(a, b\). Let \(L_1, L_2, L\) range
+  over subsets of \(\Sigma^*\) (languages). Remember that for languages,
+  concatenation is given by:
+  %%
+  \begin{gather*}
+    L_1L_2 = \{u_1u_2 \mid u_1 \in L_1 \land u_2 \in L_2\}
+  \end{gather*}
+  %%
+  We that a language \(L\) left-cancels if and only if for every \(L_1, L_2\):
+  %%
+  \begin{gather*}
+    LL_1 = LL_2 \implies L_1 = L_2
+  \end{gather*}
+
+  \begin{enumerate}
+    \item Does \(L = \emptyset\) left-cancel? \ifAns{No}
+    \item Does \(L = \epsilon\) left-cancel? \ifAns{Yes}
+    \item Give a regular expression describing an infinite language \(L\) that left-cancels. \ifAns{\(a^*b\)}
+    \item Give a context-free grammar for another language \(L\) that
+    left-cancels, but is not regular. \ifAns{\(S ::= aRb; R ::= aRb \mid \epsilon\)}
+  \end{enumerate}
+\end{exercise}

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

+
+\begin{exercise}{2022}
+  Complete (on the next page) the type derivation for the body of the function
+  \lstinline|f|.
+
+  \begin{lstlisting}
+    def f(x: Int, u: Int, v: Int): Int = {
+      if (x < u) {
+        u
+      }
+      else if (v < x) {
+        v
+      }
+      else {
+        x
+      }
+    }
+  \end{lstlisting}
+
+  You may use the following type rules:
+  %%
+  \addtolength{\jot}{2em}
+  \begin{gather*}
+    \AxiomC{\((x, T) \in \Gamma\)}
+    \UnaryInfC{\(\Gamma \vdash x : T\)}
+    \DisplayProof 
+    \qquad
+    % +
+    \AxiomC{\(\Gamma \vdash e_1 : Int\)}
+    \AxiomC{\(\Gamma \vdash e_2 : Int\)}
+    \BinaryInfC{\(\Gamma \vdash e_1 + e_2 : Int\)}
+    \DisplayProof
+    \quad
+    % *
+    \AxiomC{\(\Gamma \vdash e_1 : Int\)}
+    \AxiomC{\(\Gamma \vdash e_2 : Int\)}
+    \BinaryInfC{\(\Gamma \vdash e_1 * e_2 : Int\)}
+    \DisplayProof
+    \\
+    % &&
+    \AxiomC{\(\Gamma \vdash e_1 : Bool\)}
+    \AxiomC{\(\Gamma \vdash e_2 : Bool\)}
+    \BinaryInfC{\(\Gamma \vdash e_1 \&\& e_2 : Bool\)}
+    \DisplayProof
+    \qquad
+    % ||
+    \AxiomC{\(\Gamma \vdash e_1 : Bool\)}
+    \AxiomC{\(\Gamma \vdash e_2 : Bool\)}
+    \BinaryInfC{\(\Gamma \vdash e_1 || e_2 : Bool\)}
+    \DisplayProof
+    \\
+    % lt
+    \AxiomC{\(\Gamma \vdash e_1 : Int\)}
+    \AxiomC{\(\Gamma \vdash e_2 : Int\)}
+    \BinaryInfC{\(\Gamma \vdash e_1 < e_2 : Bool\)}
+    \DisplayProof
+    \qquad
+    % if
+    \AxiomC{\(\Gamma \vdash e_1 : Bool\)}
+    \AxiomC{\(\Gamma \vdash e_2 : T\)}
+    \AxiomC{\(\Gamma \vdash e_3 : T\)}
+    \TrinaryInfC{\(\Gamma \vdash if~e_1~then~e_2~else~e_3 : T\)}
+    \DisplayProof
+  \end{gather*}
+
+  \pagebreak
+  \begin{center}
+    \scalebox{1.2}{\rotatebox{90}{
+      %
+        \AxiomC{\((x, Int) \in \Gamma\)}
+        \UnaryInfC{\(\Gamma \vdash x : Int\)}
+        \AxiomC{\((u, Int) \in \Gamma\)}
+        \UnaryInfC{\(\Gamma \vdash u : Int\)}
+      \BinaryInfC{\(\Gamma \vdash x < u : Bool\)}
+      %
+        \AxiomC{\((u, Int) \in \Gamma\)}
+      \UnaryInfC{\(\Gamma \vdash u : Int\)}
+      %
+          \AxiomC{\((\ifAns{v}, \ifAns{Int}) \in \Gamma\)}
+          \UnaryInfC{\(\Gamma \vdash \ifAns{v} : \ifAns{Int}\)}
+          \AxiomC{\((\ifAns{x}, \ifAns{Int}) \in \Gamma\)}
+          \UnaryInfC{\(\Gamma \vdash \ifAns{x} : \ifAns{Int}\)}
+        \BinaryInfC{\(\Gamma \vdash \ifAns{v < x} : \ifAns{Bool}\)}
+        %
+          \AxiomC{\((\ifAns{v}, \ifAns{Int}) \in \Gamma\)}
+        \UnaryInfC{\(\Gamma \vdash \ifAns{v} : \ifAns{Int}\)}
+        %
+          \AxiomC{\((\ifAns{x}, \ifAns{Int}) \in \Gamma\)}
+        \UnaryInfC{\(\Gamma \vdash \ifAns{x} : \ifAns{Int}\)}
+        %
+      \TrinaryInfC{\(\Gamma \vdash \ifAns{if ~ (v < x) ~ v ~ else ~ x}~ : \ifAns{Int}\)}
+      %
+      \TrinaryInfC{\(\Gamma \vdash if~ (x < u) ~ then~ u ~else ~ if ~ (v < x) ~ v ~ else ~ x ~: Int\)}
+      \DisplayProof
+    }}
+  \end{center}
+\end{exercise}
+
+\begin{exercise}{2022, contd}
+  For which of the following expressions does type unification succeed? For the
+  \(+\) operator, assume the type rules as in the previous question.
+  %
+  \begin{enumerate}
+    \item \(x \Rightarrow y \Rightarrow y(z \Rightarrow 6) + y(7)\)
+    \item \(g \Rightarrow f \Rightarrow x \Rightarrow g(f(x))\)
+    \item \(x \Rightarrow y \Rightarrow ((z \Rightarrow y), y)\)
+    \item \(g \Rightarrow f \Rightarrow x \Rightarrow g(f(x)) + f(g(x)) + x\)
+  \end{enumerate}
+\end{exercise}
+
+\begin{exercise}{2022, contd}
+  Consider a programming language with pairs and the usual typing rules, as in
+  the lecture. Apply the unification algorithm on the following function:
+  %
+  \begin{lstlisting}
+    def swap(t) = {
+      (t._2, t._1)
+    }
+  \end{lstlisting}
+  %%
+  assuming the following type variables assigned to tree nodes:
+  %
+  \begin{equation*}
+    ((t: \tau)._2: \tau_1, (t: \tau)._1: \tau_2): \tau_3
+  \end{equation*}
+  %%
+  Write each step of the unification algorithm, mentioning what rules of the
+  algorithm you are applying. We provide you with the initial step:
+  %
+  \begin{gather*}
+    \tau = (\tau_{10}, \tau_1) \\
+    \tau = (\tau_{2}, \tau_{20}) \\
+    \tau_3 = (\tau_{1}, \tau_{2})
+  \end{gather*}
+
+  \begin{solution}
+    \begin{enumerate}
+      \item Substituting \(\tau = (\tau_{10}, \tau_1)\):
+      \begin{gather*}
+        (\tau_{10}, \tau_1) = (\tau_{2}, \tau_{20}) \\
+        \tau_3 = (\tau_{1}, \tau_{2})
+      \end{gather*}
+      \item Unifying the pair expression:
+      \begin{gather*}
+        \tau_{10} = \tau_{2} \\
+        \tau_1 = \tau_{20} \\
+        \tau_3 = (\tau_{1}, \tau_{2})
+      \end{gather*}
+      \item Substituting \(\tau_1\) and \(\tau_2\) per equations:
+      \begin{gather*}
+        \tau_3 = (\tau_{1}, \tau_{2}) 
+      \end{gather*}
+    \end{enumerate}
+
+    We can get the values of \(\tau\) and \(\tau_3\) in terms of \(\tau_1\) and
+    \(\tau_2\) by looking at intermediate steps we took during unification.
+  \end{solution}
+
+  Write down an expression for the argument and return types of \lstinline|swap|
+  in terms of the type variables \(\tau_1\) and \(\tau_2\).
+
+  \begin{solution}
+    Argument type: \(\tau = (\tau_2, \tau_1)\) \\
+
+    Return type: \(\tau_3 = (\tau_1, \tau_2)\)
+  \end{solution}
+\end{exercise}

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

+\documentclass[a4paper]{article}
+
+\input{../macro}
+
+\ifdefined\ANSWERS
+  \if\ANSWERS1
+    \printanswers
+  \fi
+\else
+  \def\ANSWERS{0}
+\fi
+
+\DeclareMathOperator{\half}{half}
+\newcommand{\num}{\ensuremath{\mathbf{num}}}
+
+\DeclareMathOperator{\first}{first}
+\DeclareMathOperator{\follow}{follow}
+\DeclareMathOperator{\nullable}{nullable}
+\newcommand{\eof}{\ensuremath{\mathbf{EOF}}}
+
+\newcommand{\ifAns}[1]{%
+  \ifthenelse{\boolean{showanswers}}
+    {\textcolor{red}{#1}}
+    {\phantom{#1}}
+}
+
+\title{CS 320 \\ Computer Language Processing\\Review Exercises}
+\author{}
+\date{April 02, 2025}
+
+\begin{document}
+\maketitle
+
+\textcolor{red}{Note: these questions are collected from previous exams, which
+are also available to you in full. Some solutions were not available in the
+previous exams, and were added later. The solutions have not been rigorously
+verified. Use them as a quick reference, but do not assume they are always the
+correct expected answer.}
+
+\input{ex/regex}
+\input{ex/cfg}
+\input{ex/ll1}
+\input{ex/types}
+
+\end{document}

info/exercises/src/macro.tex

+% macro.tex
+% common to all exercises
+
+\usepackage[dvipsnames]{xcolor}
+\usepackage{amsmath, amssymb}
+\usepackage{xspace}
+\usepackage[colorlinks]{hyperref}
+\usepackage{tabularx}
+\usepackage{multicol}
+
+% for drawing
+\usepackage{tikz}
+\usetikzlibrary{automata, arrows, shapes, positioning}
+
+\usepackage{forest}
+
+\usepackage{bussproofs, bussproofs-extra}
+
+% for code
+\usepackage{listings}
+
+\definecolor{dkgreen}{rgb}{0,0.6,0}
+\definecolor{gray}{rgb}{0.5,0.5,0.5}
+\definecolor{mauve}{rgb}{0.58,0,0.82}
+
+\lstdefinestyle{scalaStyle}{
+  frame=tb,
+  language=scala,
+  aboveskip=3mm,
+  belowskip=3mm,
+  showstringspaces=false,
+  columns=flexible,
+  basicstyle=\small\ttfamily,
+  numbers=none,
+  numberstyle=\tiny\color{gray},
+  keywordstyle=\color{blue},
+  commentstyle=\color{dkgreen},
+  stringstyle=\color{mauve},
+  frame=none,
+  breaklines=true,
+  breakatwhitespace=true,
+  tabsize=2,
+}
+
+\lstset{style=scalaStyle}
+
+% lstinline in math mode
+% https://tex.stackexchange.com/a/127018
+
+\usepackage{letltxmacro}
+\newcommand*{\SavedLstInline}{}
+\LetLtxMacro\SavedLstInline\lstinline
+\DeclareRobustCommand*{\lstinline}{%
+  \ifmmode
+    \let\SavedBGroup\bgroup
+    \def\bgroup{%
+      \let\bgroup\SavedBGroup
+      \hbox\bgroup
+    }%
+  \fi
+  \SavedLstInline
+}
+
+% for exercises
+
+\newcounter{exercisenum}
+\newcommand{\theexercise}{\arabic{exercisenum}}
+
+\usepackage{marginnote}
+\newenvironment{exercise}[1]{\refstepcounter{exercisenum}\paragraph*{Exercise \theexercise}{\reversemarginpar\marginnote{#1}}}{}
+
+\usepackage{verbatim}
+
+\usepackage{ifthen}
+\newboolean{showanswers}
+\setboolean{showanswers}{false}
+\newcommand{\printanswers}{\setboolean{showanswers}{true}}
+\newcommand\suppress[1]{} 
+
+\newcommand\ite[3]{\ifthenelse{\boolean{#1}}%
+{#2\suppress{#3}}%
+{\suppress{#2}#3}}
+
+
+\newenvironment{solution}{%
+    \ite{showanswers}{\paragraph*{Solution}}{\expandafter\comment}
+}{%
+    \ite{showanswers}{\hfill\(\square\)}{\expandafter\endcomment}
+}
+
+\newcommand{\note}[1]{\hfill #1}
+
+\sloppy
+
+%% actual macros
+
+% meta
+\newcommand{\todo}[1]{\textcolor{red}{[Todo: #1]}}
+
+\newcommand{\fbowtie}{\mathrel \blacktriangleright \joinrel \mathrel \blacktriangleleft}
+
+\newcommand{\easy}{\ensuremath{\bigstar}\xspace}
+\newcommand{\hard}{\small\ensuremath{\fbowtie}\xspace}
+
+% real
+\newcommand{\naturals}{\mathbb{N}}
+\newcommand{\booleans}{\mathbb{B}}
+
+\usepackage{bussproofs}
+
+\usepackage{pifont}
+\newcommand{\cmark}{\ding{51}}
+\newcommand{\xmark}{\ding{55}}

info/grading.md

+# Grading Policy
+
+The grade is based on a midterm (30%) as well as team project work (70%).
+
+The project work is done in groups of 2-3 people (no individual groups; the goal is in part to learn how to work together).
+The work has many aspects: the implementation in [Scala](https://www.scala-lang.org/) of aspects of an interpreter and compiler (labs 1 to 5) and Lab 6, which is an open project. There will be no written exam at the _end_ of the semester and no exam in the exam period. Here are the weights of the milestones in the overall course grade:
+
+  * Midterm exam: 30% (see [the archive of past exams](past-exams/); note that we will have fewer multiple-choice questions this time)
+  * 10% Lab 1
+  * 10% Lab 2
+  * 10% Lab 3 (First team work statement to be sent afterwards)
+  * 10% Lab 4
+  * 10% Lab 5
+  * 20% Lab 6 (Compiler extension, customized, the final team work statement)
+
+After the deadline for the submitted lab has passed, you are allowed to discuss the lab with other group members and with teaching staff, so that you can correct it and continue to use your code in subsequent labs.
+
+Please note that, after the lab deadline, we reserve the right to ask you to explain any code that you submitted for the lab. You need to understand all the code submitted, regardless whether you or another group member wrote it. We will let you know in advance when you need to be present in the labs or exercises for such oral explanations on your laptop. Taking this into account, you are welcome to write and submit comments explaining what your code does.
+
+To monitor whether everyone is doing their share of work and help ensure that group members work together, we ask each student to submit via email their teamwork statement, twice during the semester: once right after Lab 3 is due, and once at the end of the semester. Please read carefully the [Teamwork Statements](teamwork.md) email instructions.
+
+For the final Lab 6, each group will need to do their own project (based on our suggestions or your own ideas that you check with the teaching staff). Each member of the group must present the project in a slot in one of the last two weeks of the semester and answer questions. The presentation part of of each person will be graded individually and includes answers to questions (a person not presenting will be given a 0 points for the presentation part of the Compiler extension lab). The final report on the project will need to handed in after the end of the semester but the students are encouraged to complete it during the semester as this is a continuous control course.