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

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

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

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

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

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

info/exercises/src/macro.tex

+% 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

info/labs/lab01/examples/Hanoi.amy

+object Hanoi
+	
+  def solve(n : Int(32)) : Int(32) = {
+    if (n < 1) { 
+      error("can't solve Hanoi for less than 1 plate")
+    } else {
+      if (n == 1) {
+        1
+      } else {
+        2 * solve(n - 1) + 1
+      }
+    }
+  }
+
+  Std.printString("Hanoi for 4 plates: " ++ Std.intToString(solve(4)))
+end Hanoi
\ No newline at end of file

labs/amy-specification/Hello1.scala → info/labs/lab01/examples/Hello.amy

-object Hello 
+object Hello
   Std.printString("Hello " ++ "world!")
 end Hello

info/labs/lab01/examples/HelloInt.amy

+object HelloInt
+  Std.printString("What is your name?");
+  val name: String = Std.readString();
+  Std.printString("Hello " ++ name ++ "! And how old are you?");
+  val age: Int(32) = Std.readInt();
+  Std.printString(Std.intToString(age) ++ " years old then.")
+end HelloInt

info/labs/lab01/examples/Printing.amy

+object Printing
+  Std.printInt(0); Std.printInt(-222); Std.printInt(42);
+  Std.printBoolean(true); Std.printBoolean(false);
+  Std.printString(Std.digitToString(0));
+  Std.printString(Std.digitToString(5));
+  Std.printString(Std.digitToString(9));
+  Std.printString(Std.intToString(0));
+  Std.printString(Std.intToString(-111));
+  Std.printString(Std.intToString(22));
+  Std.printString("Hello " ++ "world!");
+  Std.printString("" ++ "")
+end Printing

info/labs/lab01/examples/TestLists.amy

+object TestLists 
+  val l: L.List = L.Cons(5, L.Cons(-5, L.Cons(-1, L.Cons(0, L.Cons(10, L.Nil())))));
+  Std.printString(L.toString(L.concat(L.Cons(1, L.Cons(2, L.Nil())), L.Cons(3, L.Nil()))));
+  Std.printInt(L.sum(l));
+  Std.printString(L.toString(L.mergeSort(l)))
+end TestLists

info/labs/lab01/lab01-README.md

+# Amy Lab 01: Interpreter
+
+Below you will find the instructions for the first lab assignment in which you will get to know and implement an interpreter for the Amy language.
+
+## Logistics
+
+As a reminder, the labs are done in groups of 2-3, please register on Moodle if not already done.
+
+We advice you to create a private git repository to track your work and collaborate.
+
+The labs are graded through Moodle assignments, similarly to Software Construction (CS-214) that you might have taken. You will have to submit your `.scala` files on Moodle and you will receive automatically a grade and feedback. You submit as many times as you want, only the last submission will be taken into account. The tests are the same as the ones you will receive for each lab, we do not use any hidden tests.
+
+For this first lab, you can download the initial project scaffold from this folder.
+
+## Part 1: Your first Amy programs
+
+Write two example Amy programs each make sure that they typecheck (see [Type check examples](#type-check-examples)). Put them under `/examples`. Please be creative when writing your programs: they should be nontrivial and not reproduce the functionality of the examples in the `/library` and `/examples` directories of the repository. Of course you are welcome to browse these directories for inspiration.
+
+Remember that you will use these programs in the remaining of the semester to test your compiler, so don't make them too trivial! Try to test many features of the language.
+
+If you have questions about how a feature of Amy works, you can always look at the [Amy Specification](../amy-specification/AmySpec.md). It's a good idea to keep a local copy of this document handy -- it will be your reference for whenever you are asked to implement an aspect of the Amy language throughout this semester.
+
+### Type check examples
+
+You can use the provided Frontend to type check your programs. To do so, run the provided bash script:
+
+```bash.sh
+./amytc.sh examples/your_program.amy
+```
+
+This will run the compiler frontend up to type checking and report either `Type checking successful!` or an error message. If you get an error message, you should fix the error before moving on to the next step.
+
+Please examine the bash scipt amytc.sh and its comments in your editor to understand how it works. Do not modify it.
+
+#### Troubleshooting
+
+- Your project must compile before you call the `amytc.sh` script.
+- If you get unexpected errors or behaviour, try to delete the `target/scala-3.5.2/amyc-assembly-1.7.jar` and retry.
+
+## Part 2: An Interpreter for Amy
+
+The main task of the first lab is to write an interpreter for Amy.
+
+### Interpreters
+
+The way to execute programs you have mostly seen so far is compilation to some kind of low-level code (bytecode for a virtual machine such as Java's; native binary code in case of languages such as C). An alternative way to execute programs is interpretation. According to Wikipedia, "an interpreter is a computer program that directly executes, i.e. performs, instructions written in a programming or scripting language, without previously compiling them into a machine language program". In other words, your interpreter is supposed to directly look at the code and *interpret* its meaning. For example, when encountering a call to the 'printString' function, your interpreter should print its argument on the standard output. This is the way Python is executing your code.
+
+### The general structure of the Interpreter
+
+The skeleton of the assignment is provided by us as an `sbt` project. See the [Implementation skeleton](#implementation-skeleton) section for more details.
+
+You will modify the `Interpreter.scala` file.
+
+In `Main.scala` you find the main method which is the entry point to your program. After processing the command line arguments of the interpreter, the main method creates a Pipeline, which contains the different stages of the compiler which you will implement in the future labs. The Pipeline will first call the Amy frontend, which will parse the source program into an abstract syntax tree (AST) and check it for correctness according to the [Amy Specification](../amy-specification/AmySpec.md), and then passes the result to the Interpreter.
+
+The AST abstracts away uninteresting things of the program (e.g. parentheses, whitespace, operator precedence...) and keeps the essential structure of the program. It describes the structure of programs recursively. For example, here you have the description of a module in Amy:
+
+`Module ::= **object** Id Definition* Expr? **end** Id`
+
+and in the implementation we find a class:
+
+`case class ModuleDef(name: Identifier, defs: List[ClassOrFunDef], optExpr: Option[Expr]) extends Definition`
+
+A comparison of the implementation of ASTs in Java (as shown in the book) and Scala is instructive.
+
+You can find the source code of the AST in the [TreeModule.scala](./src/amyc/ast/TreeModule.scala).
+
+### The Interpreter class
+
+Now let's delve into `Interpreter.scala`. This file currently only contains a partial implementation, and it is your task to complete it! The entrypoint into the interpreter is `interpret`, which takes an expression as input and executes its meaning. The main loop at the end of the class will just take the modules in order and interpret their expression, if present.
+
+`interpret` returns a `Value`, which is a type that represents a value that an Amy expression can produce. Value is inherited by classes which represent the different types of values present in Amy (`Int(32)`, `Booleans`, `Unit`, `String` and ADT values). `Value` has convenience methods to cast to `Int(32)`, `Boolean` and `String` (`as*`). Remember we can always call these methods safely when we know the types of an expression (e.g. the operands of an addition), since we know that the program type-checks.
+
+`interpret` takes an additional implicit parameter as an argument, which is a mapping from variables to values (in the interpreted language). In Scala, when an implicit parameter is expected, the compiler will look in the scope for some binding of the correct type and pass it automatically. This way we do not have to pass the same mapping over and over to all recursive calls to `interpret`. Be aware, however, that there are some cases when you need to change the `locals` parameter! Think carefully about when you have to do so.
+
+A few final notes:
+
+- You can print program output straight to the console.
+- You can assume the input programs are valid. This is guaranteed by the Amy frontend.
+- To find constructors and functions in the program, you have to search in the `SymbolTable` passed along with the program. To do so, use the three helper methods provided in the interpreter:
+  - `isConstrutor` will return whether the `Identifier` argument is a type constructor in the program
+  - `findFunctionOwner` will return the module which contains the given `Identifier`, which has to be a function in the program. E.g. if you give it the `printInt` function of the `Std` module, you will get the string `"Std"`.
+  - `findFunction` will return the function definition given a pair of Strings representing the module containing the function, and the function name. The return value is of type `FunDef` (see [the AST definitions](./src/amyc/ast/TreeModule.scala)).
+- When comparing Strings by reference, compare the two `StringValue`s directly and not the underlying Strings. The reason is that the JVM may return true when comparing Strings by equality when it is not expected (it has to do with JVM constant pools).
+- Some functions contained in the `Std` module are built-in in the language, i.e. they are hard-coded in the interpreter because they cannot be implemented in Amy otherwise. An example of a built-in function is `printString`. When you implement the interpreter for function calls, you should first check if the function is built-in, and if so, use the implementation provided in the `builtIns` map in the interpreter.
+- When a program fails (e.g. due to a call to `error` or a match fail), you should call the dedicated method in the Context: `ctx.reporter.fatal`.
+
+### Implementation skeleton
+
+You can get the project scaffold from [this folder](.).
+
+- `src/amyc/interpreter/Interpreter.scala` contains the partially implemented interpreter
+- `src/amyc/Main.scala` contains the `main` method which runs the interpreter on the input files
+- The `library` directory contains library definitions you can use in your Amy programs.
+- The `examples` directory contains some example programs on which you can try your implementation. Remember that most of them also use library files from `/library`. This should also contain the programs you wrote in Part 1.
+- `lib/amy-frontend-1.7.jar` contains the frontend of the compiler as a library, allowing you directly work with type-checked ASTs of input programs. You need this to be able to extract the AST from your source code to interpret it, as you did not implement this part of the compiler yet. This is also what allowed you to type check programs in part 1. **Note**: You are only allowed to use this binary code to link against your interpreter.
+
+You will have to complete the interpreter by implementing the missing methods (marked with the placeholder `???`).
+
+### Testing
+
+When you are done, use sbt to try some of your programs from Part 1:
+
+```bash
+  $ sbt
+  > run library/Std.amy examples/Hello.amy
+  Hello world!
+```
+
+You can also run your interpreter with the `amyi.sh` script in a similar way as you did with the type checker:
+
+```bash
+  $ ./amyi.sh examples/Hello.amy
+  Hello world!
+```
+
+**Note**: if you use this method, you have to delete `target/scala-3.5.2/amyc-assembly-1.7.jar` before running the script when you modified your interpreter. Otherwise, the script will reuse the previously compiled version of the interpreter and your new modifications would not be taken into account. Therefore this method is more recommended for testing multiple amy programs, rather than testing your interpreter while you are developing it.
+
+There is also testing infrastructure under `/test`. To add your own tests, you have to add your testcases under `/test/resources/interpreter/passing`
+and the expected output under `/test/resources/interpreter/outputs`.
+Then, you have to add the name of the new test in `InterpreterTests`, similarly to the examples given.
+To allow a test to also use the standard library (e.g., `Std.printString`), you can copy `Std.scala` from `library/Std.scala` to `/test/resources/interpreter/passing`.
+
+For example, to add a test that expects only "Hello world" to be printed, you can add `/test/resources/interpreter/passing/Hello.amy` containing:
+
+```scala
+object Hello 
+  Std.printString("Hello world") 
+end Hello
+```
+
+and `/test/resources/interpreter/outputs/Hello.txt` containing
+
+```text
+Hello world
+
+```
+
+(with a newline in the end!).
+
+You will also have to add a line to `/test/scala/amyc/test/InterpreterTests.scala`:  `@Test def testHello = shouldOutput(List("Std", "Hello"), "Hello")`. This will pass both files `Std.amy` and `Hello.amy` as inputs of the test. When you now run `test` from sbt, you should see the additional test case (called `testHello`).
+
+The tests provided originally in `test/` are the ones used to grade your work on Moodle. Please note that the grade returned by the grader on Moodle is what you will get for the lab. Therefore you should submit regularly on Moodle to validate your progress. Also, if tests pass locally but not on the grader, the grader is the one that counts so submit your work regularly and check the feedback in case of discrepancies.
+
+### Deliverables
+
+You should submit the following files on Moodle:
+
+- `Interpreter.scala` with your implementation of the interpreter
+
+Deadline: **07.03.2025 23:59:59**
+
+#### Related documentation
+
+- End of Chapter 1 in the Tiger Book presents a similar problem for another mini-language. A comparison of the implementation of ASTs in Java (as shown in the book) and Scala is instructive.