[FMFP] Interpreters

2026-04-28 16:19:23 +02:00 · 2026-03-26 17:19:27 +01:00
parent bca4434c3c
commit e7f688c1b7
12 changed files with 224 additions and 81 deletions
@@ -13,76 +13,3 @@ Or the same as a natural deduction rule:
        \infer2[$m$ not free in $\Gamma, P$]{\Gamma \vdash \forall n \in \N. P}
    \end{prooftree}
 \]
-
-
-\subsubsection{Induction over the natural numbers}
-In Haskell, we can also define all the natural numbers using
-\mint{haskell}+data Nat = Zero | Succ Nat deriving (Eq, Ord, Show)+
-
-Thus the natural numbers are (isomorphic to) the set
-\[
-    \texttt{Nat} = \{ \texttt{Zero}, \texttt{Succ Zero}, \texttt{Succ (Succ Zero)}, \ldots \}
-\]
-
-The data type provides two crucial rules for constructing members of \texttt{Nat}:
-\begin{itemize}
-    \item $\texttt{Zero} \in \texttt{Nat}$
-    \item If $x \in \texttt{Nat}$, then $\texttt{Succ} x \in \texttt{Nat}$
-\end{itemize}
-
-The induction stated as a natural deduction rule:
-\[
-    \begin{prooftree}
-        \hypo{\Gamma \vdash P[n \mapsto \texttt{Zero}]}
-        \hypo{\Gamma, P[n \mapsto m] \vdash P[n \mapsto \texttt{Succ}\ m]}
-        \infer2[$m$ not free in $\Gamma, P$]{\Gamma \vdash \forall n \in \texttt{Nat}. P}
-    \end{prooftree}
-\]
-
-
-\subsubsection{Lists}
-A possible data type for lists in Haskell is:
-\mint{haskell}+data L t = Nil | Cons t (L t)+
-
-A natural deduction rule for induction over lists is:
-\[
-    \begin{prooftree}
-        \hypo{\Gamma \vdash P[xs \mapsto \texttt{Nil}]}
-        \hypo{\Gamma, P[xs \mapsto ys] \vdash P[xs \mapsto \texttt{Cons}\ y\ ys]}
-        \infer2[$y$, $ys$ not free in $\Gamma, P$]{\Gamma \vdash \forall xs \in \texttt{L}\ t. P}
-    \end{prooftree}
-\]
-
-
-\subsubsection{Trees}
-A possible data type for trees in Haskell is:
-\mint{haskell}+data Tree t = Leaf | Node t (Tree t) (Tree t)+
-
-A natural deduction rule for induction over trees is:
-\[
-    \begin{prooftree}
-        \hypo{\Gamma \vdash P[x \mapsto \texttt{Leaf}]}
-        \hypo{\Gamma, P[x \mapsto l] \vdash P[xs \mapsto \texttt{Node}\ a\ l\ r]}
-        \infer2[$a$, $l$, $r$ not free in $\Gamma, P$]{\Gamma \vdash \forall x \in \texttt{Tree}\ t. P}
-    \end{prooftree}
-\]
-
-
-\subsubsection{Structural Induction}
-Induction is based on the structure of terms
-\mint{haskell}+data T t = Leaf t | Node1 (T t) | Node2 t (T t) (T t)+
-
-\shade{blue}{Base Case} $T_0 = \{ \texttt{Leaf}\ a \divider a \in t \}$
-
-\shade{green}{Step Case} $T_i = T_{i - 1} \cup \{ \texttt{Node1}\ s \divider s \in T_{i - 1} \} \cup \{ \texttt{Node2}\ a\ l\ r \divider a \in t \text{ and } l, r \in T_{i - 1} \}$
-
-A natural deduction rule structural induction is:
-\[
-    \begin{prooftree}
-        \hypo{\Gamma \vdash P[x \mapsto \texttt{Leaf}\ a]}
-        \hypo{\Gamma, P[x \mapsto s] \vdash P[xs \mapsto \texttt{Node1}\ s]}
-        \hypo{\Gamma, P[x \mapsto l], P[x \mapsto r] \vdash P[ \mapsto \texttt{Node2}\ a\ l\ r]}
-        \infer3[$(*)$]{\Gamma \vdash \forall x \in \texttt{T}\ t. P}
-    \end{prooftree}
-\]
-(*) $a$, $l$, $r$, $s$ not free in $\Gamma, P$
@@ -0,0 +1,23 @@
+\subsubsection{Induction over the natural numbers}
+In Haskell, we can also define all the natural numbers using
+\mint{haskell}+data Nat = Zero | Succ Nat deriving (Eq, Ord, Show)+
+
+Thus the natural numbers are (isomorphic to) the set
+\[
+    \texttt{Nat} = \{ \texttt{Zero}, \texttt{Succ Zero}, \texttt{Succ (Succ Zero)}, \ldots \}
+\]
+
+The data type provides two crucial rules for constructing members of \texttt{Nat}:
+\begin{itemize}
+    \item $\texttt{Zero} \in \texttt{Nat}$
+    \item If $x \in \texttt{Nat}$, then $\texttt{Succ} x \in \texttt{Nat}$
+\end{itemize}
+
+The induction stated as a natural deduction rule:
+\[
+    \begin{prooftree}
+        \hypo{\Gamma \vdash P[n \mapsto \texttt{Zero}]}
+        \hypo{\Gamma, P[n \mapsto m] \vdash P[n \mapsto \texttt{Succ}\ m]}
+        \infer2[$m$ not free in $\Gamma, P$]{\Gamma \vdash \forall n \in \texttt{Nat}. P}
+    \end{prooftree}
+\]
@@ -0,0 +1,12 @@
+\subsubsection{Lists}
+A possible data type for lists in Haskell is:
+\mint{haskell}+data L t = Nil | Cons t (L t)+
+
+A natural deduction rule for induction over lists is:
+\[
+    \begin{prooftree}
+        \hypo{\Gamma \vdash P[xs \mapsto \texttt{Nil}]}
+        \hypo{\Gamma, P[xs \mapsto ys] \vdash P[xs \mapsto \texttt{Cons}\ y\ ys]}
+        \infer2[$y$, $ys$ not free in $\Gamma, P$]{\Gamma \vdash \forall xs \in \texttt{L}\ t. P}
+    \end{prooftree}
+\]
@@ -0,0 +1,12 @@
+\subsubsection{Trees}
+A possible data type for trees in Haskell is:
+\mint{haskell}+data Tree t = Leaf | Node t (Tree t) (Tree t)+
+
+A natural deduction rule for induction over trees is:
+\[
+    \begin{prooftree}
+        \hypo{\Gamma \vdash P[x \mapsto \texttt{Leaf}]}
+        \hypo{\Gamma, P[x \mapsto l] \vdash P[xs \mapsto \texttt{Node}\ a\ l\ r]}
+        \infer2[$a$, $l$, $r$ not free in $\Gamma, P$]{\Gamma \vdash \forall x \in \texttt{Tree}\ t. P}
+    \end{prooftree}
+\]
@@ -0,0 +1,18 @@
+\subsubsection{Structural Induction}
+Induction is based on the structure of terms
+\mint{haskell}+data T t = Leaf t | Node1 (T t) | Node2 t (T t) (T t)+
+
+\shade{blue}{Base Case} $T_0 = \{ \texttt{Leaf}\ a \divider a \in t \}$
+
+\shade{green}{Step Case} $T_i = T_{i - 1} \cup \{ \texttt{Node1}\ s \divider s \in T_{i - 1} \} \cup \{ \texttt{Node2}\ a\ l\ r \divider a \in t \text{ and } l, r \in T_{i - 1} \}$
+
+A natural deduction rule structural induction is:
+\[
+    \begin{prooftree}
+        \hypo{\Gamma \vdash P[x \mapsto \texttt{Leaf}\ a]}
+        \hypo{\Gamma, P[x \mapsto s] \vdash P[xs \mapsto \texttt{Node1}\ s]}
+        \hypo{\Gamma, P[x \mapsto l], P[x \mapsto r] \vdash P[ \mapsto \texttt{Node2}\ a\ l\ r]}
+        \infer3[$(*)$]{\Gamma \vdash \forall x \in \texttt{T}\ t. P}
+    \end{prooftree}
+\]
+(*) $a$, $l$, $r$, $s$ not free in $\Gamma, P$
@@ -0,0 +1,7 @@
+\newpage
+\subsection{Interpreters}
+Interpreters are prevalent in programming languages, database systems, text processors, HDLs, search engines, etc.
+
+They are in concept very simple, as they perform three steps read, evaluate, print.
+
+The implementation of one however is not trivial by any stretch of the imagination.
@@ -0,0 +1,52 @@
+\subsubsection{Read step}
+During this step, text is turned from text into a more easily handlable format
+
+
+\paragraph{Lexical Analysis}
+During lexical analysis, the input is turned into tokens.
+For example: The source code is \texttt{position := initial + rate + 60}
+
+The translation is:
+\begin{multicols}{2}
+    \begin{enumerate}
+        \item Identifier \texttt{position}
+        \item Assignment symbol \texttt{:=}
+        \item Identifier \texttt{initial}
+        \item Addition symbol \texttt{+}
+        \item Identifier \texttt{rate}
+        \item Addition symbol \texttt{+}
+        \item Number \texttt{60}
+    \end{enumerate}
+\end{multicols}
+
+It also removes whitespaces and comments
+
+
+\paragraph{Parsing}
+The tokens are then turned into an abstract syntax tree.
+
+The syntax is specified by a grammar such as:
+\begin{align*}
+    Expr   & ::= Identifier \divider Number \divider Expr\; \texttt{`+`}\; Expr \\
+    Assign & ::= Identifier\; \texttt{`:=`}\; Expr
+\end{align*}
+
+This can also be represented as a haskell type:
+\begin{code}{haskell}
+    data Expr = Identifier Ident | Number Num | Plus Expr Expr
+    data Assign = Assignment Ident Expr
+    type Ident = String
+    type Num = Int
+\end{code}
+
+Since some to be parsed statements are more complex to parse, we may do combinatory parsing.
+
+This is much more powerful as it can handle ambiguous grammars typically found in real programming languages.
+
+We can use for example these parser combinators:
+
+\newpage
+\inputcode{haskell}{code/10_parser.hs}
+
+These are just some of the functions defined.
+You can find a full mini-haskell and lambda-calculus parser on CodeExpert (at the time of writing this that was the case at least)
@@ -0,0 +1,3 @@
+\newpage
+\subsection{Evaluation}
+Evaluation is then done using tree traversal as we have already seen in the haskell section.