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{\(n_1, n_2\) are integer values}
+            \AxiomC{\(n_1 = n_2\)}
+            \BinaryInfC{\(n_1 == n_2 \leadsto true\)}
+            \DisplayProof \\
+            %
+            \AxiomC{\(n_1, n_2\) are integer values}
+            \AxiomC{\(n_1 \neq n_2\)}
+            \BinaryInfC{\(n_1 == n_2 \leadsto false\)}
+            \DisplayProof
+          \end{gather*}
+        \item Addition:
+          \begin{gather*}
+            \AxiomC{\(t_1 \leadsto t_1'\)}
+            \UnaryInfC{\(t_1 + t_2 \leadsto t_1' + t_2\)}
+            \DisplayProof \\
+            %
+            \AxiomC{\(n\) is an integer value}
+            \AxiomC{\(t_2 \leadsto t_2'\)}
+            \BinaryInfC{\(n + t_2 \leadsto n + t_2'\)}
+            \DisplayProof \\
+            %
+            \AxiomC{\(n_1, n_2\) are integer values}
+            \AxiomC{\(n_1 + n_2 = k\)}
+            \BinaryInfC{\(n_1 + n_2 \leadsto k\)}
+            \DisplayProof
+          \end{gather*}
+        \item Conjunction:
+          \begin{gather*}
+            \AxiomC{\(t_1 \leadsto t_1'\)}
+            \UnaryInfC{\(t_1 ~\&\& ~t_2 \leadsto t_1' ~\&\& ~t_2\)}
+            \DisplayProof \\
+            %
+            \AxiomC{}
+            \UnaryInfC{\(true ~\&\&~ t \leadsto t\)}
+            \DisplayProof \\
+            %
+            \AxiomC{}
+            \UnaryInfC{\(false ~\&\&~ t \leadsto false\)}
+            \DisplayProof
+          \end{gather*}
+        \item Conditionals:
+          \begin{gather*}
+            \AxiomC{\(t_1 \leadsto t_1'\)}
+            \UnaryInfC{\(if ~(t_1) ~t_2 ~else ~t_3 \leadsto if ~(t_1') ~t_2 ~else ~t_3\)}
+            \DisplayProof \\
+            %
+            \AxiomC{}
+            \UnaryInfC{\(if ~(true) ~t_2 ~else ~t_3 \leadsto t_2\)}
+            \DisplayProof \\
+            %
+            \AxiomC{}
+            \UnaryInfC{\(if ~(false) ~t_2 ~else ~t_3 \leadsto t_3\)}
+            \DisplayProof
+          \end{gather*}
+        \item Function call:
+          \begin{gather*}
+            \alwaysNoLine
+            \AxiomC{\(b_0\) is the body of \(f\)}
+            \UnaryInfC{\((x_1, \ldots, x_n)\) are parameters of \(f\)}
+            \UnaryInfC{\(b_0[x_1 := t_1] \to b_1 \quad \ldots \quad b_{n-1}[x_n := t_n] \to b_n\)}
+            \alwaysSingleLine
+            \UnaryInfC{\(f(t_1, \ldots, t_n) \leadsto b_n\)}
+            \DisplayProof
+          \end{gather*}
+      \end{itemize}
+
+      \item Evaluations:
+      \begin{enumerate}
+        \item \(sum(2) \leadsto 3\):
+          \begin{align*}
+            &sum(2)\\
+            &\leadsto if ~(2 == 0) ~ then ~ 0 ~ else ~ 2 + sum(2 + (-1))\\
+            &\leadsto if ~(false) ~ then ~ 0 ~ else ~ 2 + sum(2 + (-1))\\
+            &\leadsto 2 + sum(2 + (-1))\\
+            &\leadsto 2 + if ~((2 + (-1)) == 0) ~ then ~ 0 ~ else ~ 1 + sum(2 + (-1))\\
+            &\leadsto 2 + if ~(1 == 0) ~ then ~ 0 ~ else ~ 1 + sum(2 + (-1))\\
+            &\leadsto 2 + if ~(false) ~ then ~ 0 ~ else ~ 1 + sum(2 + (-1) + (-1))\\
+            &\leadsto 2 + (1 + sum(2 + (-1) + (-1)))\\
+            & \ldots \\
+            &\leadsto 2 + (1 + 0) \\
+            &\leadsto 2 + 1 \\
+            &\leadsto 3
+          \end{align*}
+        \item \(sum(sum(0)) \leadsto 0\):
+        \begin{align*}
+          &sum(sum(0))\\
+          &\leadsto if ~(sum(0) == 0) ~ then ~ 0 ~ else ~ 0 + sum(sum(0) + (-1))\\
+          &\leadsto \ldots \textit{(expand \(sum(0)\) in the conditional)} \\
+          &\leadsto if ~(0 == 0) ~ then ~ 0 ~ else ~ 0 + sum(sum(0) + (-1))\\
+          &\leadsto if ~(true) ~ then ~ 0 ~ else ~ 0 + sum(sum(0) + (-1))\\
+          &\leadsto 0
+        \end{align*}
+        \item \(if ~(1 == 2) ~ then ~ 3 ~ else ~ 4 \leadsto 4\).
+        \item \(rec() \leadsto rec()\) (infinite loop).
+        \item \(default(false, rec()) \leadsto 0\).
+      \end{enumerate}
+
+      Under call-by-value-semantics, the structure of the evaluations would be
+      different. In \(sum(sum(0))\), we would evaluate the inner \(sum(0)\) to
+      \(0\) before evaluating the outer \(sum(\cdot)\). In \(default(false,
+      rec())\), we would need to evaluate \(rec()\), which would lead to an
+      infinite loop.
+    \end{enumerate}
+        
+  \end{solution}
+  
+\end{exercise}

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

+
+% perform actual type derivation of some terms
+
+\begin{exercise}{}
+
+  Consider the following type system for a language with integers, conditionals, pairs, and
+  functions:
+
+  \allowdisplaybreaks
+  \addtolength{\jot}{0.5em}
+  \begin{gather*}
+    \AxiomC{\(n\) is an integer literal}
+    \UnaryInfC{\(\Gamma \vdash n : \lstinline|Int|\)}
+    \DisplayProof \quad
+    % variable
+    \AxiomC{\(x : \tau \in \Gamma\)}
+    \UnaryInfC{\(\Gamma \vdash x : \tau\)}
+    \DisplayProof \\
+    %
+    % addition
+    \AxiomC{\(\Gamma \vdash e_1 : \lstinline|Int|\)}
+    \AxiomC{\(\Gamma \vdash e_2 : \lstinline|Int|\)}
+    \BinaryInfC{\(\Gamma \vdash e_1 + e_2 : \lstinline|Int|\)}
+    \DisplayProof \\
+    %
+    % multiplication
+    \AxiomC{\(\Gamma \vdash e_1 : \lstinline|Int|\)}
+    \AxiomC{\(\Gamma \vdash e_2 : \lstinline|Int|\)}
+    \BinaryInfC{\(\Gamma \vdash e_1 \times e_2 : \lstinline|Int|\)}
+    \DisplayProof \\
+    %
+    % booleans
+    \AxiomC{\(b\) is a boolean literal}
+    \UnaryInfC{\(\Gamma \vdash b : \lstinline|Bool|\)}
+    \DisplayProof \quad
+    \AxiomC{\(\Gamma \vdash e : \lstinline|Bool|\)}
+    \UnaryInfC{\(\Gamma \vdash \lstinline|not e| : \lstinline|Bool|\)}
+    \DisplayProof \\
+    % boolean ops
+    \AxiomC{\(\Gamma \vdash e_1 : \lstinline|Bool|\)}
+    \AxiomC{\(\Gamma \vdash e_2 : \lstinline|Bool|\)}
+    \BinaryInfC{\(\Gamma \vdash e_1 \land e_2 : \lstinline|Bool|\)}
+    \DisplayProof
+    \quad
+    \AxiomC{\(\Gamma \vdash e_1 : \lstinline|Bool|\)}
+    \AxiomC{\(\Gamma \vdash e_2 : \lstinline|Bool|\)}
+    \BinaryInfC{\(\Gamma \vdash e_1 \lor e_2 : \lstinline|Bool|\)}
+    \DisplayProof \\
+    %
+    % conditionals
+    \AxiomC{\(\Gamma \vdash e_1 : \lstinline|Bool|\)}
+    \AxiomC{\(\Gamma \vdash e_2 : \tau\)}
+    \AxiomC{\(\Gamma \vdash e_3 : \tau\)}
+    \TrinaryInfC{\(\Gamma \vdash if ~e_1~ then ~e_2~ else ~e_3 : \tau\)}
+    \DisplayProof \\
+    % pairs
+    \AxiomC{\(\Gamma \vdash e_1 : \tau_1\)}
+    \AxiomC{\(\Gamma \vdash e_2 : \tau_2\)}
+    \BinaryInfC{\(\Gamma \vdash (e_1, e_2) : (\tau_1, \tau_2)\)}
+    \DisplayProof \\
+    %
+    % projections
+    \AxiomC{\(\Gamma \vdash e : (\tau_1, \tau_2)\)}
+    \UnaryInfC{\(\Gamma \vdash fst(e) : \tau_1\)}
+    \DisplayProof
+    \quad
+    \AxiomC{\(\Gamma \vdash e : (\tau_1, \tau_2)\)}
+    \UnaryInfC{\(\Gamma \vdash snd(e) : \tau_2\)}
+    \DisplayProof \\
+    %
+    % function
+    \AxiomC{\(\Gamma \oplus \{x : \tau_1\} \vdash e : \tau_2\)}
+    \UnaryInfC{\(\Gamma \vdash x \Rightarrow e : \tau_1 \to \tau_2\)}
+    \DisplayProof \quad
+    %
+    % application
+    \AxiomC{\(\Gamma \vdash e_1 : \tau_1 \to \tau_2\)}
+    \AxiomC{\(\Gamma \vdash e_2 : \tau_1\)}
+    \BinaryInfC{\(\Gamma \vdash e_1 e_2 : \tau_2\)}
+    \DisplayProof
+    %
+  \end{gather*}
+
+  \pagebreak
+
+  \begin{enumerate}
+    \item Given the following type derivation with type variables \(\tau_1,
+    \ldots, \tau_5\), choose the correct options:
+    \begin{equation*}
+      \AxiomC{\((x, \tau_4) \in \Gamma\)}
+      \UnaryInfC{\(\Gamma \vdash x: \tau_4\)}
+      \UnaryInfC{\(\Gamma \vdash fst(x): \tau_3\)}
+      \AxiomC{\((x, \tau_4) \in \Gamma\)}
+      \UnaryInfC{\(\Gamma \vdash x: \tau_4\)}
+      \UnaryInfC{\(\Gamma \vdash snd(x): \tau_5\)}
+      \BinaryInfC{\(\Gamma \vdash fst(x)(snd(x)) : \tau_2\)}
+      \UnaryInfC{\(\Gamma' \vdash x \Rightarrow fst(x)(snd(x)): \tau_1\)}
+      \DisplayProof
+    \end{equation*}
+
+    \begin{enumerate}
+      \item There are no valid assignments to the type variables such that the
+      above derivation is valid.
+      \item In all valid derivations, \(\tau_2 = \tau_5\).
+      \item There are \emph{no} valid derivations where \(\tau_2 = \lstinline|Int|\).
+      \item In all valid derivations, \(\tau_4 = (\tau_3, \tau_5)\).
+      \item In all valid derivations, \(\tau_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 \num(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 \\
+  % 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/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 you receive your points for the submitted lab, 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.

info/labs/.gitignore

+# sbt compilation output
+target/
+project/target
+# Compiler output and nodejs modules
+compiler/**/*.html
+compiler/**/*.wat
+compiler/**/*.wasm
+compiler/**/*.js
+compiler/node_modules
+compiler/package-lock.json
+# Latex output
+*.out
+*.aux
+*.log
+*.nav
+*.snm
+*.toc
+*.vrb
+# Vim
+*.swp
+# IntelliJ
+.idea
+# VSCode
+.vscode
+# tester
+tester/repos
+# Metals & Bloop
+.bsp/
+.bloop/
+.metals/
+metals.sbt

info/labs/lab01/amyi.sh

+#!/bin/bash
+# Script similar in structure to amytc.sh, see explanations there.
+if [ $# -eq 0 ]; then
+    echo "Usage: amyi Prog1.amy Prog2.amy ... ProgN.amy"
+    exit 1
+fi
+echo Intepreting: $*
+AMYJAR=target/scala-3.5.2/amyc-assembly-1.7.jar
+if test -r "${AMYJAR}"; then
+    echo "Reusing existing jar: ${AMYJAR}"
+else
+    sbt assembly
+fi
+java -jar ${AMYJAR} --interpret library/Std.amy library/Option.amy library/List.amy $*

info/labs/lab01/amytc.sh

+#!/bin/bash
+# The above line tells the operating system to use the 
+# bash shell interpreter to execute the commands in this file.
+# the hash sign, '#' means that characters following it are comments
+if [ $# -eq 0 ]; then # script is called with 0 parameters
+    # output short usage instructions on the command line
+    echo "Usage: amytc.sh Prog1.amy Prog2.amy ... ProgN.amy"
+    echo "Example invocation:"
+    echo "./amytc.sh examples/Arithmetic.amy"
+
+    echo "Example output:"
+    echo "  Type checking: examples/Arithmetic.amy"
+    echo "  Reusing existing jar: target/scala-3.5.2/amyc-assembly-1.7.jar"
+    echo "  Type checking successful!"
+    # Now, terminate the script with an error exit code 1:
+    exit 1
+fi
+# print progress message. $* denotes all arguments
+echo Type checking: $*
+# jar file is a zip file containing .class files of our interpreter/compiler
+# sbt generates the file in this particular place.
+AMYJAR=target/scala-3.5.2/amyc-assembly-1.7.jar
+# You can copy this file into test.zip and run unzip test.zip to see inside
+if test -r "${AMYJAR}"; then
+    # jar file exists, so we just reuse it
+    echo "Reusing existing jar: ${AMYJAR}"
+    # Note that we do not check if scala sources changed!
+    # Hence, our jar file can be old
+else
+    # If there is no jar file, we invoke `sbt assembly` to create it
+    sbt assembly
+fi
+# We should have the jar file now, so we invoke it
+# java starts the Java Virtual Machine. 
+# Here, it will unpack the jar file and find META-INF/MANIFEST.MF file
+# which specifies the main class of the jar file (entry point).
+# java will execute `public static void main` method of that class.
+java -jar ${AMYJAR} --type-check library/Std.amy library/Option.amy library/List.amy $*
+# Here, we ask amy to only type check the give files. 
+# We always provide standard library files as well as 
+# the explicitly files explicit given to the script (denoted $*)

info/labs/lab01/build.sbt

+version := "1.7"
+organization := "ch.epfl.lara"
+scalaVersion := "3.5.2"
+assembly / test := {}
+name := "amyc"
+
+Compile / scalaSource := baseDirectory.value / "src"
+scalacOptions ++= Seq("-feature")
+
+Test / scalaSource := baseDirectory.value / "test" / "scala"
+Test / parallelExecution := false
+libraryDependencies += "com.novocode" % "junit-interface" % "0.11" % "test"
+libraryDependencies += "org.apache.commons" % "commons-lang3" % "3.4" % "test"
+testOptions += Tests.Argument(TestFrameworks.JUnit, "-v")
+
+

info/labs/lab01/examples/Arithmetic.amy

+object Arithmetic
+  def pow(b: Int(32), e: Int(32)): Int(32) = {
+    if (e == 0) { 1 }
+    else {
+      if (e % 2 == 0) {
+        val rec: Int(32) = pow(b, e/2);
+        rec * rec
+      } else {
+        b * pow(b, e - 1)
+      }
+    }
+  }
+
+  def gcd(a: Int(32), b: Int(32)): Int(32) = {
+    if (a == 0 || b == 0) {
+      a + b
+    } else {
+      if (a < b) {
+        gcd(a, b % a)
+      } else {
+        gcd(a % b, b)
+      }
+    }
+  }
+
+  Std.printInt(pow(0, 10));
+  Std.printInt(pow(1, 5));
+  Std.printInt(pow(2, 10));
+  Std.printInt(pow(3, 3));
+  Std.printInt(gcd(0, 10));
+  Std.printInt(gcd(17, 99)); // 1
+  Std.printInt(gcd(16, 46)); // 2
+  Std.printInt(gcd(222, 888)) // 222
+end Arithmetic

info/labs/lab01/examples/Factorial.amy

+object Factorial
+  def fact(i: Int(32)): Int(32) = {
+    if (i < 2) { 1 }
+    else { 
+      val rec: Int(32) = fact(i-1);
+      i * rec
+    }
+  }
+
+  Std.printString("5! = "  ++ Std.intToString(fact(5)));
+  Std.printString("10! = " ++ Std.intToString(fact(10)))
+end Factorial