paper: subtype relation

This commit is contained in:
Michael Sippel 2024-08-08 13:19:17 +02:00
parent 06dba1f348
commit b8e8543813
Signed by: senvas
GPG key ID: F96CF119C34B64A6

View file

@ -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}\).