From b8e8543813690a43eaa6624d35fe52c4d929fc6c Mon Sep 17 00:00:00 2001
From: Michael Sippel <micha@fragmental.art>
Date: Thu, 8 Aug 2024 13:19:17 +0200
Subject: [PATCH] paper: subtype relation

---
 paper/main.tex | 58 ++++++++++++++++++++++++++++++++++++++++++++++----
 1 file changed, 54 insertions(+), 4 deletions(-)

diff --git a/paper/main.tex b/paper/main.tex
index e4335db..3577d3c 100644
--- a/paper/main.tex
+++ b/paper/main.tex
@@ -448,14 +448,64 @@ LNF is reached by exhaustive application of \(\rightarrow_\text{distribute}\).
 PNF reached by exhaustive application of \(\rightarrow_\text{condense}\).
 \end{definition}
 
-\begin{definition}[Syntactic Subtyping]
-\todo{}
+\subsubsection{Subtype Relations}
+
+We define two relations: first the syntatic subtype relation \(\leq\) and second the semantic subtype relation \(\precsim\).
+
+\begin{definition}[Syntactic Subtype (\(\tau_1\leq\tau_2\))]
+\begin{mathpar}
+\inferrule[S-Refl]{	
+	\metavariable{\tau} \equiv \metavariable{\tau'}
+}{
+	\metavariable{\tau} \leq \metavariable{\tau'}
+}
+
+\inferrule[S-Syntactic]{
+	\metavariable{\sigma} \leq \metavariable{\tau}
+}{
+	\metavariable{\sigma'} \typeterminal{\sim} \metavariable{\sigma} \leq \metavariable{\tau}
+}
+\end{mathpar}
 \end{definition}
 
-\begin{definition}[Semantic Subtyping]
-\todo{}
+\begin{definition}[Semantic Subtype (\(\tau_1\precsim\tau_2\))]
+\begin{mathpar}
+
+\inferrule[S-Refl]{	
+	\metavariable{\tau} \equiv \metavariable{\tau'}
+}{
+	\metavariable{\tau} \precsim \metavariable{\tau'}
+}
+
+\inferrule[S-Syntactic]{
+	\metavariable{\sigma} \precsim \metavariable{\tau}
+}{
+	\metavariable{\sigma'} \typeterminal{\sim} \metavariable{\sigma} \precsim \metavariable{\tau}
+}
+
+\inferrule[S-Semantic]{
+	\metavariable{\sigma} \equiv \metavariable{\tau}
+}{
+	\metavariable{\sigma} \typeterminal{\sim} \metavariable{\sigma'} \precsim \metavariable{\tau} \typeterminal{\sim} \metavariable{\tau'}
+}
+
+
+\end{mathpar}
 \end{definition}
 
+
+\begin{example}[Syntactic \& Semantic Subtypes]$\\$
+
+\begin{enumerate}
+\item \typeterminal{ <Digit 10> \(\sim\) Char \( \quad \leq \quad \) Char }\\
+.. is a \emph{syntactic subtype}, because the representation of \typeterminal{<Digit 10>} is \emph{embedded} into \typeterminal{Char}.\\
+
+\item \typeterminal{ <Digit 10> \(\sim\) Char \( \quad \precsim \quad \) <Digit 10> \(\sim\) machine.UInt64}\\
+.. is a \emph{semantic subtype}, because the \typeterminal{Char} based representation can be transformed into a representation based on \typeterminal{machine.UInt64},
+while preserving its semantics.
+\end{enumerate}
+\end{example}
+
 \subsubsection{Inference of Expression Types}
 
 The type-context \(\Gamma = \{ \metavariable{x_1} : \metavariable{\tau_1} , \quad \metavariable{x_2} : \metavariable{\tau_2} , \quad \ldots \}\) is a finite mapping from variables \(\metavariable{x_i} \in \exprvars\) to ground types \(\metavariable{\tau_i} \in \typenonterm{\emptyset}\).