diff --git a/beamer/lc-beamer/example.tex b/beamer/lc-beamer/example.tex index f3ee859..621463c 100644 --- a/beamer/lc-beamer/example.tex +++ b/beamer/lc-beamer/example.tex @@ -271,23 +271,23 @@ image-write "out.png" im3 \begin{frame}{Coercions: (In-)Coherence with Transitivity} \begin{itemize} - \item<1-> Common example: coerce \texttt{Int -> Real} + \item<1-> Common example: coerce \texttt{Int -> Float} (subsumption \(\mathbb{N} \subset \mathbb{R}\)) \begin{itemize} - \item \texttt{Int -> Real} + \item \texttt{Int -> Float} \item \texttt{Int -> String} - \item \texttt{Real -> String} + \item \texttt{Float -> String} \end{itemize} \item<2-> transitivity creates two extensionally \emph{different} coercion paths: \begin{itemize} \item \texttt{Int -> String} (3 -> "3") - \item \texttt{Int -> Real -> String} (3 -> "3.0") + \item \texttt{Int -> Float -> String} (3 -> "3.0") \end{itemize} \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} \item value ranges (e.g. map int to unit interval [0,1]) \item multiple quantization functions (linear, exponential, \dots) @@ -342,17 +342,21 @@ image-write "out.png" im3 \end{frame} \begin{frame}{Morphisms} -\framesubtitle{Coherence} \begin{block}{Morphism Condition} Assume\\ \(\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{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} }\)\\ + \vskip1cm then it holds that:\\ \(\forall x:\typeterminal{\metavariable{\sigma}\sim\metavariable{\sigma_1}},\quad \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{frame} diff --git a/beamer/lc-beamer/morphisms.dot b/beamer/lc-beamer/morphisms.dot new file mode 100644 index 0000000..1d798bd --- /dev/null +++ b/beamer/lc-beamer/morphisms.dot @@ -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_σ"]; +} + + diff --git a/beamer/lc-beamer/morphisms.png b/beamer/lc-beamer/morphisms.png new file mode 100644 index 0000000..a05e3ae Binary files /dev/null and b/beamer/lc-beamer/morphisms.png differ