add image for morphism condition

This commit is contained in:
Michael Sippel 2024-09-24 10:28:14 +02:00
parent 7f45198cd1
commit 3adeebc8eb
3 changed files with 27 additions and 6 deletions

View file

@ -271,23 +271,23 @@ image-write "out.png" im3
\begin{frame}{Coercions: (In-)Coherence with Transitivity} \begin{frame}{Coercions: (In-)Coherence with Transitivity}
\begin{itemize} \begin{itemize}
\item<1-> Common example: coerce \texttt{Int -> Real} \item<1-> Common example: coerce \texttt{Int -> Float}
(subsumption \(\mathbb{N} \subset \mathbb{R}\)) (subsumption \(\mathbb{N} \subset \mathbb{R}\))
\begin{itemize} \begin{itemize}
\item \texttt{Int -> Real} \item \texttt{Int -> Float}
\item \texttt{Int -> String} \item \texttt{Int -> String}
\item \texttt{Real -> String} \item \texttt{Float -> String}
\end{itemize} \end{itemize}
\item<2-> transitivity creates two extensionally \emph{different} coercion paths: \item<2-> transitivity creates two extensionally \emph{different} coercion paths:
\begin{itemize} \begin{itemize}
\item \texttt{Int -> String} (3 -> "3") \item \texttt{Int -> String} (3 -> "3")
\item \texttt{Int -> Real -> String} (3 -> "3.0") \item \texttt{Int -> Float -> String} (3 -> "3.0")
\end{itemize} \end{itemize}
\item<3-> Subsumptive interpretation is misleading! \item<3-> Subsumptive interpretation is misleading!
\item<3-> \texttt{Int -> Real} is not as unambiguous as it might seem. \item<3-> \texttt{Int -> Float} is not as unambiguous as it might seem.
\begin{itemize} \begin{itemize}
\item value ranges (e.g. map int to unit interval [0,1]) \item value ranges (e.g. map int to unit interval [0,1])
\item multiple quantization functions (linear, exponential, \dots) \item multiple quantization functions (linear, exponential, \dots)
@ -342,17 +342,21 @@ image-write "out.png" im3
\end{frame} \end{frame}
\begin{frame}{Morphisms} \begin{frame}{Morphisms}
\framesubtitle{Coherence}
\begin{block}{Morphism Condition} \begin{block}{Morphism Condition}
Assume\\ Assume\\
\(\metavariable{m_\sigma} : \typeterminal{\metavariable{\sigma} \sim \metavariable{\sigma_1} \rightarrow_\text{morph} \metavariable{\sigma} \sim \metavariable{\sigma_2}}\)\\ \(\metavariable{m_\sigma} : \typeterminal{\metavariable{\sigma} \sim \metavariable{\sigma_1} \rightarrow_\text{morph} \metavariable{\sigma} \sim \metavariable{\sigma_2}}\)\\
\(\metavariable{m_\tau} : \typeterminal{\metavariable{\tau} \sim \metavariable{\tau_1} \rightarrow_\text{morph} \metavariable{\tau} \sim \metavariable{\tau_2}}\)\\ \(\metavariable{m_\tau} : \typeterminal{\metavariable{\tau} \sim \metavariable{\tau_1} \rightarrow_\text{morph} \metavariable{\tau} \sim \metavariable{\tau_2}}\)\\
\(\metavariable{f_1} : \typeterminal{\metavariable{\sigma} \sim \metavariable{\sigma_1} \rightarrow \metavariable{\tau} \sim \metavariable{\tau_1} }\)\\ \(\metavariable{f_1} : \typeterminal{\metavariable{\sigma} \sim \metavariable{\sigma_1} \rightarrow \metavariable{\tau} \sim \metavariable{\tau_1} }\)\\
\(\metavariable{f_2} : \typeterminal{\metavariable{\sigma} \sim \metavariable{\sigma_2} \rightarrow \metavariable{\tau} \sim \metavariable{\tau_2} }\)\\ \(\metavariable{f_2} : \typeterminal{\metavariable{\sigma} \sim \metavariable{\sigma_2} \rightarrow \metavariable{\tau} \sim \metavariable{\tau_2} }\)\\
\vskip1cm
then it holds that:\\ then it holds that:\\
\(\forall x:\typeterminal{\metavariable{\sigma}\sim\metavariable{\sigma_1}},\quad \(\forall x:\typeterminal{\metavariable{\sigma}\sim\metavariable{\sigma_1}},\quad
\metavariable{m_\tau}(\metavariable{f_1} x) = \metavariable{f_2} (\metavariable{m_\sigma} x) \) \metavariable{m_\tau}(\metavariable{f_1} x) = \metavariable{f_2} (\metavariable{m_\sigma} x) \)
\vskip-4.5cm
\hfill\includegraphics[width=0.3\textwidth]{morphisms.png}
\end{block} \end{block}
\end{frame} \end{frame}

View file

@ -0,0 +1,17 @@
digraph Morphisms {
node [fontcolor=blue];
edge [fontcolor=red];
sigma1 [label="σ ~ σ1", shape=plaintext];
sigma2 [label="σ ~ σ2", shape=plaintext];
tau1 [label="τ ~ τ1", shape=plaintext];
tau2 [label="τ ~ τ2", shape=plaintext];
sigma1 -> tau1 [label="f_1"];
sigma2 -> tau2 [label="f_2"];
tau1 -> tau2 [label="m_τ"];
sigma1 -> sigma2 [label="m_σ"];
}

Binary file not shown.

After

Width:  |  Height:  |  Size: 9 KiB