From 3adeebc8eb8b5eb1d80e8e56398e6b3b9c8cf0bd Mon Sep 17 00:00:00 2001 From: Michael Sippel Date: Tue, 24 Sep 2024 10:28:14 +0200 Subject: [PATCH] add image for morphism condition --- beamer/lc-beamer/example.tex | 16 ++++++++++------ beamer/lc-beamer/morphisms.dot | 17 +++++++++++++++++ beamer/lc-beamer/morphisms.png | Bin 0 -> 9201 bytes 3 files changed, 27 insertions(+), 6 deletions(-) create mode 100644 beamer/lc-beamer/morphisms.dot create mode 100644 beamer/lc-beamer/morphisms.png 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 0000000000000000000000000000000000000000..a05e3ae959718e6d39dc13bd9b2d491283d8cc99 GIT binary patch literal 9201 zcmbt)WmuF^*Y3ao(nztG!oM3 zw|UQXegDpn^B(xYF!RiM_Otie>yEV})Kuh%@aga&5D1a{OKA=8cMt->;K0QJubx0A ziNPNn6Gb^`$iLg)yicWx5XgOqy!11KN7kP?Pi@5U&7J+zA$T5c*-{Fupsau5NBg6+ z)kxh8`i!*jR>U%K%a7rO)&@{LYCf*$qONHm>HQaqjmK<_7p$rxrE^YQe z`Vl9=gNN!mxTFyS&%<9LsGds~{6Am9=gh|!(D^j}UAK6|jldFPzRU2zYDyV zicmeh0Aj}A13kU7cd@8+2nD9F-si?Y=xw-`)rlz>tm&e;sJiLI`R%45! zBP_owQc>TG0R-brS8eawu+(d+{V_RSe>{xE39XRM-{s|9v5XnY0s`c?BzG_|0~U=I zcXW&?E81H`jrH!)%CDBelEWiNa~3=bmu=?S@J32iqjGaPJL^uZPVMiD(~G(jrwQU& ze#fHW!_;oV-9N_G)5madkYXM8mDLcMF)x>Xow7e$rSoM9(SukCH@4!aB5Sr(ck@7I z>?`JG5enMjD`l14q#9Dw%1?lM)isdi93FCYl+3LBsLMawJU=gIvbQ1d@UTo#mf4Cf zvTmY#jYmzrbUxD@SjMBv|+M+T=PN=TIC_~9E zIR7LIzCZYxe{iJU6WVS6vrB4mO*zj@amn-r6O-|Z1dMQFdJHZ=MTM!Dipi#mA9sf& zcxiovK%6Nn>&-b2;T=Yca`bR!S13_ev0{K8kFAfl_x6;0ScW+ahIMnubX@DYOBj8x z`cqYC^lgqc4gc4P_P^=66|g>%dl+j(Q3ex(+f2fI4!%$$(@&-h{bMA3FD%VwieQ{k zDJ*PksPPizy88ODfuk^D#>lfX4~D0HdR*gdykmWl&9(zc9HLIkSoX6m7_VNvsvbgh z1z;FOs~a~(r@)YJwkNrRgM+&k77T4 zO9B@7-1O?~pykab8INHHVXNMyf1-k-;=#psZO_C6rS5y%v5Tu{QgGSg)M|a*7 zm`*`r0R+r(SZ*%U^XJdwpPz0{;v*X@KTp@A65`_nqNsVds$dW`1S0so-LLMsIYut6 znjb%XVz9Y&9=V9U(V2H+qqn5F$Fk zuAy`RQW~0<>(TOH`pD=&obTh~PHRK7HIEw_8^#ned-Qoec<=y&QQWP!!}k(y{eykpiSS->af*h9#%PVcxb18UX(Frg zGGl3=dZFyn{3q{Ocd;MXh!o`ClM{6Qi!jH-HRbA@P{UUiBRMjsyK@JFyq$Rt3mxq% zG=iLp+_RnjOx3y{&=s1MaNmnJ^G=)-wT4gGlNA`AcqO@01j*|9Ht)~5FXV&hUY#GT z#tLM@qoaFUUDiG1_$-@D%k!(MV4|X;iy&-pTpY=s=!CPITWDb+^U2Q79`VS}1uTk0 z)!Ox#=H}*S8-;Nma-?QU-66OH1TRcX9`3Q@L=9*_RdXbsIXc3xuC9!XjX#UWvhVKh zT8@_xVPax}yJ#a)=(IoBGeV5khSIYV!%NlJ>x@2Q+Aef3ZfGQXrt*)VAnNg0}z`&sH{rlSo12F(z5dE2LB`0B$6f7%_j7(3bT^r5}TU<0UH8VSi zMLCwi=#Y)(MCdps5^-_yd39^ki=$1rkdO=*7Z_#OK*3vPx!A?!FHt!4l`Z@!DJf}u zD4f@|1~FM#3{DG2>$w4`)T0e7_Y?8r_)vnGPHw_*7gi$^OrPWAwa>?pWEm*e>ngBo zp`*<x>=jYRHu9YngX`-Z}ZiL~{SbzUQ{QVCExVW)}Z6RWASl_at3JTUq zI=t|Q10b`~lvq)6u?$O$GGvYB!zONSZdG-4bz7uNPfQ4nY-gG>hBvM}(R%u{AAQp6 zl{15_xb=~ZR!*{tR0%1(hOx1X;wFn-Z`%uBnt(NE@&703wl}YT99~}D-Pr6pZ2tQ< z7J#_X@>jzhhH;kv+6r8|K6#(kS&ZDXovwTPD})__TPdjf0dr|d3P~5A2rU!WwVH+- z9dB{6nORueAt51w>AoiM?HCx8oP6oIBknpN|rLQRleye6rosB_%cW)H%=k zSo&DhF`#}#5>@5tf~FHRs&X(y^B9=IL{jU2HqzS6B-Mu!(b9{?*Z1~jV5h_1^0j8w z6VcOf!AxP|nf1J#6l+h-2~qC5xS+^OEAP%U+bHp*HeO$zRx;%)rZ()UAB+05n4c5* z2t@;+E>+EKkd2|MHycbTXEL7PT%zv!5>j6WN9R02!FXcpS(RxT>y2%{KSDoz7`#-f zN)WO+seE`}E)M_D$-VXrxi{Z!V=-ba@$+=vJFc~*1tHmee%Rea&HdeDhLXlZ$1<~+ z4wS)XpzI#ADV=O#N8cmT)`rY|gsz}5PIocvW^gNI0J#5hAXw?`gP!i$P?_!-EO{Pn zMAnu|@>kKxL390Y9xpF1J8u2pi0Pb~R@13a)6fWPwwW^7`cYn2V-KDB*}5~uty{rV z)25$OvTjlSjq0^K93fPNV?pt;r6o_R*5GU{(?RgY0QJJGyc<-D_^hnx$1ZD#r_Sex zy$JfD)v!t)OLb(04$Z{b@wS$avQSkh{Yn%SclT0H7%3BzVd0(#6(WVR3fYWbC>M9T ziTBv0wkNwA+a^RN;1i;BUZ->JW7WDMV!oYph!lk^F;{#iC#U`6<5fl(xO36I&tKD9 zhG6Z~T6liAj@q05)Z%$)9#g75rLMzS@4TvTwDXg^rlzL75LY$^^WqpPY>!oA;QLsD zhj{vvuBcWem6n6&zw6VnHdmXrT18Edz1VR%d3pKUwFQY@Atxxn<$aZJp=#_Agku&) zLidPJi+zB2Z%((-Xe3ua*pnYcMHNkSZ)iFIqq`mKkg7bXl~Wx9u!#i(1W=${bVFSG zbP#(oxXp~n?Xi<|Ov#ArRUkrhY3 zDFHtIC>WGdh9KTx3U{JuhAUomXmVm^W)zd(8HRwxw;v+~5UE1hE?ozVnwoc%*morv zge|@?ROx;oj$?Y7V%z45om`xCdokGcX=1LNd+d5cX?#%U)+|Ye5*+XuC`KM$Ua$S{ zYH<2qv|mYSn#D=_zDdLmNKU3KQO%8=sMKQSg zY=CHY`aJ*PozQ@T9t?xWGf(jzF{w;g#lefF=e0#b(#V41GBdepW z2?9PozKx%aYrKPdJT+%A*C@3iW z$m!sB{{2$I>j-yjY>YvJHZ(jOHyV)IgM$M~9{AbD7_*@LY}zaSIsOcytFkh7QE_q9 z_GC40tP&d=+sb;bf63gJ2^wKr8Zp zD8WnlTnSH1a&mGCYU&lRMYKP z{`s)Kzb_T>z;ILlAqNMC{sHn(Mp;%Y;RSKJGPSQD&Cl$5%y*Q2E48K%5)B?Ob+i4u( zqzDBg8)~!|F}TvrS2F@E{Osy*3Ivivk~q~#D|7E%u8TlV}F|NNz2aGUso*?jAS7|5w^CrLIP^^KR$%Pq9Zj3 z_|pji2}B=ljvEpRgrc}*)l&eqNJ>fR9vdSCv{%;G^;Gl$T|&PpE52XV=w` zvXGtNfd)L%j_P@l)PJk4`6EgECuFTS?vg|GS|GpIFx}h&8U=tvZcj}3O9OTLgK0m9 zd2{WsS*og-!fE@9H3`*?wKyXL1n1d}cUM0ijW`v%yDLlg*w03(xO?3rTZ6pK0wl-= z#L|&f*9={F4EBxRWkPKy4izuX)&%tV^RrdvK=AKmHS~22*40(OYodcfU-0i+`tEtdNZ&n(@Nv* zDJTIoK7Hr)1;z&l0(#x^^R95x=i3-v=uktQq5+T9$o(hetTguOkVQ0+(T&eiEkC69 z3kHz#A3xUp#)8Pn&85m1y2v|2C(GE;ru=BxI395c{&#$N%Z~SohD7}&P~1p(O2Pv> zS$%QejQaUchJH_6O7{Jo)`@GS1806W)Eg`1kE-y<5Aa*Y@0**LaCS_#Htr*z2bzz! zI|bD<`J3)!I?!A$-C5fHtDs056+UW*UNl0(xM?r1-JK36EU>YopLp#5-JVI38OYVL zbGB-Py{iiS(u+Id(5`;aY(E#Em>TTVdoPm)4r%eCq!Ct{rgy!O*#Bt}5P>&ZNp0l7 zyMvC2Bzw;rN;IyF=GG1HzgE=Fb#tXWH8@HyFR$A*)YbUcUNpecj7%-glbW`)AI;m@ z)uf!zUvFsWRUMz83=hBSHe3N`W!MIbd`}Wf%$>^bel>EF6(xl5|4q+y2thQX#8>T7mFQ-> zL2ZRdgiAT2vVh51xPcMF|yItZ5d2M25ROprMFz1q;qDaKd;<-TF1B2sz?Hr@X5g{_Zs5)kL`F@0M@vg9OTv>3D6BO` zIg9A`u!x8VM`!15py8KxcfX0pKBMI`!P;HujB9BTomYP|U^$2h0iXvkjt)H7t+;OS zyB518Dgb~9nIyB^8M67e8nPa{;PCM9gvZ9p)*5{B=;Ol$Quu5o?y2MI0Oi+JbhH20 zG7xF6{g9YW$T}Dhqg90$ zchz#N09!&r!b5JUdt>nLy!YPc{(d~b5Pmbt)S8)@EnV()_61@S7+G5nh!a!G8d9Yz z;Q)#R{HgoZJahLoOaREqe)2kon+;IRtGDo7G(ZAMOW866tpfA%?t_tNsHhMJ1_ki} z&=edk{nfHblZ+hz^t$;-P7I*P5}tp9-5EZSGcZJ7UHSZn;C53cukr#49<0RL15~}I z+!z-&Hnw)NHD&v!PsVn3!{WqRh?Guk9UWtU;J5GN6A*azjnMGkN!L^ZSITuI{rq|KwKHRRgvAFQZBP0wiFXt#x&McWYM_7Mb&-0D)^YgdlHonVfYjXYrE`^%_50813GCf+%mF%XPWhD2h zg>r_VG4LzR49_kvkxk+Ce}2*0EacRC9S18_{EN%Gk7i(`tu)N7uhFL!ca}c9dwnVJ z-i8|3A#f@t-l6e1{WIk8*Wv0p`f3)=sF$E-m^*Zwo3AowJ^lALRe|&7CR#^_&+Sjf zn{fncbs)LwSr86PK%j9ss^WB_o*AW>%Ab<_WqR&o^zp_6TMOmfZ`x82)X$&MEG&GJ z)%2*fwdmqf8!8|$(PU)7{ubu=hgpKPe9Om0AZ~>8B<{M!Z)r zaQKXSLjP0EURRBNBdpQGnD=LzZY4jvoY-{Vf#8s&__!@CErFWbHa6Q@`5st?YWgVK zzF5YWnv7Zr3P?Km8}|K$f0%n6Tz{IlZtdY)OP1;1S(wTiTSjZ^ewBqtW`r>rY@c3mAj^>a$ zqIY^U-z+RW9d8A^>2#G58DU(dBVbH7_i@TcjI3a!@kbX>5XKG;alk@A0qkvGu>{11 zU<0i5LuTeB5KdfWRY4)R*uGG#UmmzF70ARha;iV}s_242ReQmDW9&#KgK$Tvqs)p6p@&d0pZr~y5{~;bI;39zN z<@;VKTb$g;zd+&P_t2nladEruF!=<$u0~q9-k<{p9_9m*^*}^~8Zav;Bq=HB7H2kQ znz^p7ubaj80K~uapMIaBgJ) zW=3+XR;Qou@3l2+?l6D^z!~83o$Kwz!VkgB6mbYGEiIjN{$U0>6vd|t{!C!6)Lsc* zcm7^oEuT|l4Jjyi2uz}~8PJ8*Tio5PNhSpIsG$f#gEX2nq=adA;TU18JkqnS8ccnmgL*?+TpIGbOm9336uV{39Id;Dph0v-xp<=<3o7NO^63EF_aI{p4i z3V1{6Id;n6DpH>)anSGv#AliL;1CBYF|fR}xef(o5melkqj?yy437grE1-j2NnSqU zbtu@4 zjIO_K3XWaemI5Sp-fNp1BrBqAy+Rn&v(YB2S685?2pDF_?{PLvWWz>4bv3t%i3#Wm zssBmvQ(pc3JJ0iQP1JRZf>LJCvcKSkh{Jqvb~Yo(XSSb$jg5^7iHT6qzv(ZL|512* zI-oj~^uIqvQ2v*zJ3(xHfO7G4;q8!8o~KLRi#vH1s`KUlIS|m*>LN8&6Hv+J`1jHN z5r^Xr&FBZ-#T{5uI3g|uCcAjydY_L})c+n>vD6;bY%=`AdGD^_OespO9F{zmDD{n5 z+Os|XK`LyB*D>b24>{0u+86N^V+&-YZo61FZ6a#L;Os#B_L*wjv|hG20f{S}5Lpga ztAxNg{RLqME-P!m*3HxY{%$Y-ksPUC?|J)vHp!oMIyMh$>Jd)QU=q<|PSs#c%<=_o zoZU;ok+OZe%S#2} zbmx@W&vD+!#6>}8nlLIp)|uKlXN%uCyTG)Wgj`<&@IVI-JPeFc{!_ZNM^a@#L`a7v zDu#)N*EQ2DB^z3oKbH?xLttH<(5q?VO3PaFYWYaO9q)r?B4Cd~nW20I4IAOb#cJ_? zsbiEB$y0>Ele{xsmR^hzX-ZxB#<)1={+30tj6LJ_y4>80rT6ax!ouwNP0cWZ?mz`B zFkRN#8T=L@`vY8{ud>Y=mS3;}qkGry!KPN*rswI|wZGJj@%7(jXG1Nc=zZAS%L$M$ z4|H{x90UT}}mVoXgv!SToCH%6l?kNa$Q zaPgM1E4K79g)x}?^^Q+@b#Z(y%1>PA_&F7cOwIAV8}JF<;*keT8Lnr)RMV+h@T>IO z%gCg+YeadaE1pWFQXz| J^V}%#e*kkTmBj!6 literal 0 HcmV?d00001