From dea5a6fbe4e3abf1c354f678189236423d489a54 Mon Sep 17 00:00:00 2001 From: Francesco Mecca Date: Tue, 30 Jun 2020 19:31:56 +0200 Subject: [PATCH] traces --- ...31ca755ec4bd798a690ed9350f68282bc11561.png | Bin 0 -> 1251 bytes ...cc44285208b6cf43ee96ac8e9f497e5f3191eb.png | Bin 0 -> 1384 bytes ...120fd1e8cd49ab0dab3ef97353929c15f4113a.png | Bin 0 -> 3467 bytes ...279e548f036c71f2640c10d3ac4556f571c8a3.png | Bin 0 -> 1364 bytes ...b96ab92fcbc42081a14294cafc9655d64124a1.png | Bin 0 -> 3593 bytes ...cddde4a95b736a274897266cb27c5b8a348b6f.png | Bin 0 -> 965 bytes ...6a52e070f6e7a9d353e2fb281d3431b02bdb3c.png | Bin 0 -> 1251 bytes ...f6cd40efd8589318c49e230274945c079c4ca8.png | Bin 0 -> 787 bytes ...2675337cc8345e6e71ecbfd98a2bd044cb53a2.png | Bin 0 -> 1404 bytes ...82b4110fb7414eb8af69a9211cfb2808fe4dd5.png | Bin 0 -> 1643 bytes ...705f10cbe564234adb81cafa072109c3faf2f5.png | Bin 0 -> 1080 bytes ...7c518e2def2cbaf55d84c945bd0b86d59e7037.png | Bin 0 -> 1823 bytes ...786361c751a1a74c01c332e65e4854d7be80e6.png | Bin 0 -> 633 bytes ...a68b35299cd5b8f2f8555b5b61d0f0803f6778.png | Bin 0 -> 550 bytes ...56f2a20f6be4475ef3496e1a2eb5e99cd0c727.png | Bin 0 -> 3452 bytes ...02030f255196914ab3a21c0b5eb83072e92d47.png | Bin 0 -> 1551 bytes ...429dea9befffee656ac9fc36b1df8509d3c7ff.png | Bin 0 -> 377 bytes ...116a10855bae8a6d0cb304a27220822ddaedb4.png | Bin 0 -> 329 bytes ...449751cf9a5061cafa5f18d30c08dbe8c20a11.png | Bin 0 -> 965 bytes ...43bcd039f21e4dbb99e46d60f3f9cf9f5c1311.png | Bin 0 -> 1929 bytes tesi/tesi_unicode.org | 127 ++++++++++-------- tesi/traces/example0.trace | 4 +- tesi/traces/example3.lambda | 18 +++ tesi/traces/example3.ml | 11 ++ tesi/traces/example3.trace | 46 +++++++ tesi/traces/example6.lambda | 70 ++++++++++ tesi/traces/example6.ml | 11 ++ tesi/traces/example9.lambda | 5 + tesi/traces/example9.ml | 9 ++ tesi/traces/example9.trace | 18 +++ tesi/traces/example9bis.lambda | 9 ++ tesi/traces/example9bis.ml | 6 + tesi/traces/example9bis.trace | 15 +++ tesi/traces/guards2.lambda | 7 + tesi/traces/guards2.ml | 8 ++ tesi/traces/guards2.trace | 24 ++++ 36 files changed, 332 insertions(+), 56 deletions(-) create mode 100644 tesi/ltximg/org-ltximg_1031ca755ec4bd798a690ed9350f68282bc11561.png create mode 100644 tesi/ltximg/org-ltximg_15cc44285208b6cf43ee96ac8e9f497e5f3191eb.png create mode 100644 tesi/ltximg/org-ltximg_20120fd1e8cd49ab0dab3ef97353929c15f4113a.png create mode 100644 tesi/ltximg/org-ltximg_25279e548f036c71f2640c10d3ac4556f571c8a3.png create mode 100644 tesi/ltximg/org-ltximg_38b96ab92fcbc42081a14294cafc9655d64124a1.png create mode 100644 tesi/ltximg/org-ltximg_41cddde4a95b736a274897266cb27c5b8a348b6f.png create mode 100644 tesi/ltximg/org-ltximg_5c6a52e070f6e7a9d353e2fb281d3431b02bdb3c.png create mode 100644 tesi/ltximg/org-ltximg_72f6cd40efd8589318c49e230274945c079c4ca8.png create mode 100644 tesi/ltximg/org-ltximg_8c2675337cc8345e6e71ecbfd98a2bd044cb53a2.png create mode 100644 tesi/ltximg/org-ltximg_8e82b4110fb7414eb8af69a9211cfb2808fe4dd5.png create mode 100644 tesi/ltximg/org-ltximg_96705f10cbe564234adb81cafa072109c3faf2f5.png create mode 100644 tesi/ltximg/org-ltximg_a07c518e2def2cbaf55d84c945bd0b86d59e7037.png create mode 100644 tesi/ltximg/org-ltximg_a4786361c751a1a74c01c332e65e4854d7be80e6.png create mode 100644 tesi/ltximg/org-ltximg_bea68b35299cd5b8f2f8555b5b61d0f0803f6778.png create mode 100644 tesi/ltximg/org-ltximg_c356f2a20f6be4475ef3496e1a2eb5e99cd0c727.png create mode 100644 tesi/ltximg/org-ltximg_ca02030f255196914ab3a21c0b5eb83072e92d47.png create mode 100644 tesi/ltximg/org-ltximg_cc429dea9befffee656ac9fc36b1df8509d3c7ff.png create mode 100644 tesi/ltximg/org-ltximg_d3116a10855bae8a6d0cb304a27220822ddaedb4.png create mode 100644 tesi/ltximg/org-ltximg_ee449751cf9a5061cafa5f18d30c08dbe8c20a11.png create mode 100644 tesi/ltximg/org-ltximg_f243bcd039f21e4dbb99e46d60f3f9cf9f5c1311.png create mode 100644 tesi/traces/example3.lambda create mode 100644 tesi/traces/example3.ml create mode 100644 tesi/traces/example3.trace create mode 100644 tesi/traces/example6.lambda create mode 100644 tesi/traces/example6.ml create mode 100644 tesi/traces/example9.lambda create mode 100644 tesi/traces/example9.ml create mode 100644 tesi/traces/example9.trace create mode 100644 tesi/traces/example9bis.lambda create mode 100644 tesi/traces/example9bis.ml create mode 100644 tesi/traces/example9bis.trace create mode 100644 tesi/traces/guards2.lambda create mode 100644 tesi/traces/guards2.ml create mode 100644 tesi/traces/guards2.trace diff --git a/tesi/ltximg/org-ltximg_1031ca755ec4bd798a690ed9350f68282bc11561.png b/tesi/ltximg/org-ltximg_1031ca755ec4bd798a690ed9350f68282bc11561.png new file mode 100644 index 0000000000000000000000000000000000000000..a624488ea883d17c18e568204ba09424755ba92a GIT binary patch literal 1251 zcmV<91RVQ`P)o+!00009a7bBm000ie z000ie0hKEb8vpe5n9ojAK@`RbVJ+nWu;m4``T`Um0MR{v#5GVLac4zb zBNg4sKesA{xK-M?HKE|z0Ev5ApTHj;a~$W+ozA`GCTM6Ha%SfH&iT%nx#v#l>ACt` zz6y-q9lO@wpGeol$2eih__lLoi+DGcz}Dc^DoZxpA{-P5z_9zyeCX zKicg?X*Qb&9EC&_Cpc4)M6`9j-gv_vJEiDk2u8u_3{IYv`O4~AI#-vF6<9!E>BL`1 zt+EzLYJchca`3fdwjr2~PW*s;zF@XJPN6yUbEB&?59&ysR@bzKQDR0jAqBK5kVpwV zuVee@=rC)M2oRmUYy*4KZnby;Tm42=hF}z|#@n5}r2YT&^kld+QhBm0-<{frt<81O zst*dKiPNc}#h9F$US4{(IHdRlepoh&S zbmb;B!gskFk*E@#eMg7Qlaph<+glr|6%obatyb$Smm6S`B@@HOuU22}*4`D1xATP| zjN#H9jtH*Q1IF@F1r`SQa(U5QQoB}rZ?U#F*W0ajqp=TWCAY?PhwAU`*5=BK_+g0d zf!qK_RHVAaV3jk+QN~`JpQRb_BtYbz!O%oTZMb7&_m`hmbSbJ~aPay<^-;$nh=;%; z11=PX_G&xAiU##3PO|yPLls_pOQdI){USS7=8sNZNz_`ajG-NZu1;+rBp3Hn8Ph^p;eCnexD z#FQRYu{o98sN`96Vu1N?qjV048Z6v^#jVKvZNd2vd8SWhOp%s(&Q`8 z>-pjP^$#$~UAfXToITH}0iv@ArcN-<0y^~*MP);D26Yl83fW<#`#447Dw<%3NGDN* z5$Ly0wwV*AuS*sL!Hi~NVE|AdT@}3bmrbQc)@0xi&ng27N@Nf8t)#1_$Ux@;L!P*m zA?a`yza4*Ph)p=lTU3J}okhU8<-saooPLp^p`$_Lh)^g_>Viu|OJrPv9Yw|wB}%ML zZ8jvSws6e9?2~8JL}p=YXun8LXikhiyLjV^D|x=1C(r51Qw0AZ@aT6QWsUA3a&Gio zD!xl2EvkUj|pY z%F;9W0n0^jraaG2Hb2E$^%sF(=oVgwe*KO5Cjiz@e&KqEY=r-|t5c5|BuvLLAq46v4zu9P{N%%k?A6)V>ty}O=ePo3x98Bp|Ts1KLNS_X4Fzaza0Po N002ovPDHLkV1foe5n89yURTRc2>e^2K0G!7TH!!%7m2Le4u)5Kh2(^1) zN)t6P)Kb^ArMd+QZp9AOtxzo%@~d-goYuTdVE={a+L~{@UpC0|S+^IdSscO8$G~oWL9=O8!})Me^@|@Zq)g zSNFH>A3F5nE5jpizV-IsTU&SUZaBQtP)@*@N2ktA{P6vE)^liRWT0NZckg%G`IOqp zk{&+Ntk>)7YipGf|EE@a`Pi}Bw|}XG$~!01CR7@8fCc1P3P0ZZ+47^=Xk@l0Z>OR1 zapHSe#7JiSXXh4d^J%x!B)xd~^R&cwOT9GOa870pR>(i2nGX$*tghVDCI-!uW8=0b zZ>OR1apHTH+e?-e3wmSYPCPvDqzoV;T42~mLDN3kYdb+wYE7r}QyQ_=l^d+TG^|A> z&<4H}=D>w~u!wJ1TG(vUK~K%!tGKk-wM#IKTko5TI>+7A42C2khtCCIdCEWoRU7$Ji4;I5;wApvL_DAYqNQ@+uf|!2kE(b<+Ajbp;$w6^PgRBUu!mB zYGem7hK65dwXLr`)|v=2(^FDM@o%*zC1&v5Zhsk|t}b5cb$hF;5B81O`of>R9@Dmb zy?v%NNgSHwHdr6TD5EVy@Ra2%=l;ow(-b6LDuA8NEt&z1pb2(#^o^PGQ?@@(P+Q1_)?HQ6Kx4#SDFsNmeKZCg3r9KdfUh|f8X5v)@H)k ze{BAxXJV~VXr#N3gThUs0TdhcHJTkL%@#foP%;qK6zu2{-_lMSF+h=yYGNM+G%S-C z9UMtz6dlxN#EFP;l}5n90m>uQO(Rq_9NNADK64+d zV=<#iwWh)e-a&14H`Ql;eioaGt3Y{VzZoLF5(6YY5H=$%nbbvUb`Z0Ww)Np>B0lu6 z9m7)@BHxLz@$s>D=waOux!3KUZk=T#qO4N&Z4he*G<0)glo%ZxNg1VVBG@4v4h~RI zI$0W|>U21?HF%){KJys$G=7bDQA-+`Fok-)l*H)4hqI=2>x%*#+<2%=Vo=Y}E9i`A zf`TDSP@P$7^5WWB^?Bs~hjkh)b?i3@3fD%8PJl_B~{ zT9^@oY9hobOv&UqlmUStSMn49kD=`-(3iP`twvr8o-hU+`6sVLr1P%3CDT?WtUN6h zMB{@3Qc=nlv0|;^=ul|^IT;ncB+9`7vZ3h`SN~l%90h#lFmbR#{_*WZ8Eyjn*1RHHs)f?OkFOtr@Y35_|7iv#NwzHDYfq8kDM5Ycxi*wIW_SO6=XD zRl5x@V*A>D-#_sEaMwBaoO_?=-gD2nDJJ)HuhMbSk&%&I)z^cWl97>r{q6GuDSqo5 z4p`)GLmQ-L^N@^;q5F@JKb2qr|4vrbhiRH4$ahK{(k-mm`e+2jqH=KTNlAm1D*3PH z93wX-XgDI7GgeHD-WlB`XVErtA*-#*G3CS1rX~hDA6U z9PE>uA;7K6(5;J@fOT08ZX~Js4y%%eY0$!oid!}9YL~txQHRQ;A!TmvhZli6YY|_u z-lN5gjgw^4>MivaEFan~44YG@w|@A3pgWhV^(S`BCL$)^P1>C_W5dr5UP6AhzyC5j z8y?{fqk1M)Tl*FLpeMCe{Yzs@b@f&qo5XObYDIwx=PdvAN3CR9LH& zV>{V+a&{bp#0MQMdwQHcWz)|N<%b+gZrYmzGU3VnkN+TG;b>B<#ys(F^skWY^Hx%G z7u8X|p!b?)dA!71mc)K<{Q5N+;OalLiZ;*Tx3+nuyY@1~klE=|?B(eM?44bj2>~@* zGjXK2zYIUMJ}j1BoIF+1c@Mt83)Se-6Ca=PI!?b0Xm!0Wa?^>^`jwCeMvJYn+-#Zn znI_)nQ%_p5%sWwiaOZMGj)q%tR_J^W0HyKQ>vg#6q7;1(ZN{%dt6=T$M!2k`-vhRlo#Pn)Mr>|l;N z)_|o{a4d)vG~-2BM&(g)ObW*fR4}X0!3=|c+zB=g94#4A>Q$g?VuBo!pX7Q!7z|5z z-XfRoY-1{Lov;7)9a4${l8MDO^yZEM0Z0kSg=!zp?9T^fjAKhrX~Zd7Jw;%)9WOi0 zbG$1>%dEb$hvl+<-B)c1deu$fB@zmFkib@`pU$q{P`_5$a8*JM^+2|@Mp;H8OBldu zB3P##rg&PL;;uVjo+gw_;XucJ6c4G0q+ha$PZm=GIv1nsJ(Kue6NJudX64^KRy)gi zeVE3Nw+Vw}K&w*WQ8@!~phM&51!V;mtSD`Njf%UM0!W)qTrvdH%^8lOU4YQ8AhYCY zdROfPPby@x5g<}ICJn|DX~Z5i0ATazfn;!4;?wk5e(MgSDX z#S|MaU}Om~{Fc%^;mPSfBknI*95EsJ^4T~mRNtE)@b62;kK|By@h08_erEqHR;llp z8Xa(wrvw4;*3tAp^c~%)HX!E*>clj&$&5Kd=b$IARO+U1QIprm0(GCU5s5NfoxYGaiz#)S5Nl+}!el ztuA>M(HoQT(wBi-m#%{x;MOX6z{B%$D<@_Kb}!?rSg-#|6emEy$z(7$Tj=uY}j+$e4e2>qBwQzmRqVFWDio1c@!r7bwP$;U_ z#i-mb{nI|3ZZf~lWKo`nc|6l}K)xSsF=zcz%&xA=5%zIyVBp8dg-fXWQ9fLD$n+J{4{J0Bqs4wo-A9 zRSj)&TJ%T}6|a3fa31G;B_En)27)GLY=TdtXVeQ*_u||t944qo>s-PTUlVxZ{;~QP z;mX3aN`T3>L?jCI(Q$YnUGsrTOB(AgupYDkMNpT3J0jLqB+EW6RTv~?<$}zd=@y%^ z#wPULKd>7Ex;8LbhVz-;p`%LjwihUS19dOY(c)#Y@qNI8lFV+@0Sa`Xe{T`vs*9`r zU@Zlc;PuoeLH#btM%`n95ckj6L1Wqq zCYYXSd8)&?q&NK1{og_Hl@GRHz0Q23xSLHF$CyhVqt?yEM%?@Mg@DM@uK8n|A}Y=g z#zBfyNk-9#ot^WurL2gdK=aJc}AXMW*+u1~(u^uw=@_SFgv&o-V0^NHReE)sC z^(diW%KClO(&ul1$tvF0$neB(fo&a?fqnHA)1Y`G4je1r^h}rywQ8 zzy-0eccp8Tn+g~brmn#)r0HzMpje8PlNU_X!2?{)_-&J=f0Cv=@-`!5 zNTqpNf#V_#G&x5i(~+qM-!7s?V$juTs-g>x&{H4tbPx_KPM6_3%!rPudvH(AsAn50 zkC_KO0Ua1Wx60uk<@ArWMCj5ztcWJ+!5O$z_CNdE;g%&(SRHM2uexeY%WXS`tL-Jw zQ62`G1Y*C_toJcSP#2Z!C=WrK*@oc3nx$;IujVOTtco}|#7&3xt|A)uxDMdBv^wiXS8BP|R*%)IgzXC% zRy!X`WhWOlp+il(d&04C*P22Wl~Gv8)_mHsEX$SMOFE=~btv_3JV`HN5 zWeTC(vXQFO-fGCzL2GECZ>{Bu@@`tF9I(xmZ))H+DUZ(|zpyGw?qty2o-h~ufzk%% z`#s%Dln53)o2@Na><#_CAzDxvwiA6EGE6Ba%RZ6VI|PCJk0Y^?Ixu>0jY$C-BpJjCPjhsI=M5P*wZx0Ct*G)o|8>^$NV zP33ID&Yc((=Eq)UtiTd*Arfd$D!%%&CSa2-@~psMe+-*T=HNrRvw!#Gk<8yR0T4i; z*KrKnagsJ|Nm0wXy0yIGsrtBuq`|seQA5RW$e(_eK)TMsJ40rA;%#w^wd<8JMw-fR zoO&nCg{8KEN)(x$@_e0*X5*KjwfhZGnjBAw>I8EqsXw5e zfZ3l=4dtptARK;qz2rhbugOVHOCh4!7>n&}?Wl3_y5Xo46`9O8)*HUEh0nt?x~4j~ ztICvQRU-SiZ_IU&cKID5cb&yc!?=_WjQ&TIrZah-B%{6Y3(GzgJSw51ZI}6bVM&o! zQ4BbPy6fe@H^uPSCc>2gSDS6#w#egPEvqI(d=Asa&Y#|61(^6CFGNy3op60M+#N!O z-U$arHixK>eh#!y5t69z*S{2WG8c~c-GLA-5mZGM#P8szI><+wpZ9Mz1(RiJha4pb ztdI68A1xf=CTenR9J-07dquO3g8!vh6CnI+w(9U&v)I?}L=Vr+Z4~LctYhyZ`e!(^ z&_Dc^`2dcv9s8LK^|Gty!^i*$>2LRM(^&mof+Za-=MHX&q8ss+N_0owjdOmNa2BiX z2_r3b-wOs+szKVnMdq?JMjPf1&5iKQ8x?d=nL%t6RT#%N*aS}Q^o9rQk{&D(tR=<8>{FV zQ_jOlQ7PCVA4D#>dZ9W`)76@K%1+sAGwes%asK%IHxqp(4L#pq+yl2nuy?bBi z+pENL-?%4c=ephQ&v$N%$x9Ol=!@<4vS>m=PEN9>5Q;8C3*=%eLLs^A!W~4*@!}k( zyuh*S+`<=&=g-P>^F~v^iEwo0jaAQ+A;O2J&k&IZLDwhCW0n1Jz|Njq{AKwr$mNq$ z9_Ov&c|eMrHT4N`)nZOyyY*|xkb@V}=)({vS^3YJf*x9zEs*QxN-iXq5h$Q~PS@wz z<9~WRGTgWC#g7^v-)LTS-9zjF!gTe>%TfWNcbw6O!9z8qdvpF&C1Gy1kOV4~ z2O8eo>@l5F;4#HFN4QpnD4~7-0mx-2!l*MUvJx!fDnrgv$6Ha?vuV-}{wqPO za7epS=3C`h54X}}Dk(L#TrWZ8icgO9PnR#zxy3(9>cI2v$r=&lREWkpE?IE)#18@u z>HNayv@3~X(x`KSi3R`STtX)tq{v=qftxhOTUAI?Ro;1pQG!x%TyB&s8p#;} z6V8*_{PZ=*G*SGk(pmHUHU9xhD4TK*u~q7Q6f%h%f(<>TX3nZ9^mK?x*Tt<`LocU9 zXuv2XFGBZ%t*)Q)FCi`-*vrL*?G8jbkfsi&kY>`TbApqs{70rhxHL^cvbI1T$!8(C zY*it5KE5s?usy52C%p>x^}ZtLMc`G!*9-1I95rEFW<_Aub*EGnQnFlT*(zoUs$QeA zGFbqjc_~yT5Q;Zs4hHQ|{K#?VtwDh*kW@d{3|Z4xh>J@pFhvjMYN0NgR2ye31TvCF zof80L=vcN6>+K1CA>g5bMvzd1fT#}8}@8}-NQ?{2$Qc(_Q12{a~il3+NT6ifh- ze5$N>crM#plcue1uO67RLtv=?)QnD4<{K!<4jf8r!hF8=~i WrhwJ3F&67)vB4JA|Eqfq@f^f?G2%FwURk zFd);(zN8oV>Ljpvqa1t~7`WR0F2+<@F6asP9U5+QIe>9B*O7F^j<=IlJgKp3I6+ENVpsXqP?!&*+b` zgxajR6qrDNBq;No0lPuKkrxg*%N)nPJ<9X#I}&gka7fP9SuStTKlaRhysfwM)n|O% z?P#iA@pt2${sISKw`#`Qb^bQhl361kHZgsX&`};R3yt1G3gopc6 z>h3JRnRvHu7)1P1>gnY*HM&(np{Tyd==F%hd?zD#Q3^ZEiOL>m)$0>=!1#`^JTaVu zxVnE~(o(7G8}N`B57y4;qD&2~S9O~XQ>;!nZcDa`QpQrEgfAAIL(D9=!5M!0bXsjy z1}*`RnxDAkm90B?RPZ+?uDm9k5V_-gh!vS;3jUMOJ-3@+P@NJZ^l#`7zPH{mr(Q zfx-SxQc|q9edMu+I|gaO^v(Hr+uwgD=#R6jYj<8wPB<6m5+=<(CaL^~oXv9@{_9FPWj%j>(jNhDNU^a9M?B>gQOx%y8oA=>sjh~yyp!L7rHAee;Pbc178hC zb7VKWe?QBq!;;V`506<~K^i=W{_{3q(_p6HbWoi~)DRgfd2KudHAka9#%fqFqg%Q( zteJgD+LTIw8DENzbcs{oOh+im02jso7OgM$JG|O+$4LvgfDb2%n7~d^0<~r&&E&fy zh2~7{Czac|$)w1`6u0Lw58IGs#RTfW88Jd493WM2CcleGQn8&A1`sC|DL{~2%#8}% z8@vvQE&=>Az@-|#r1~m{m$$QMH5Tj*b{Mz?qGKYx%9Q@Qj*Q zg3%?^cpEjf_i{#wrt%irv6K~z1BWR10aKzt5j!c&FWOqlIr+B8saxbE#O-%ViE!l! z6z7ogQg}UC#sOnG@wryLFhrJ@#htrN>Kslu%-@YukVSe?UP}eCS!mHFes!|Y5dDuWj1ud9*7Gi0=mCCEDU67YcL^8q%)Ml70}_=C91DIW@|X>RXYjB_ z%}N|}KZH9q4eg4;(B&~8QM4}LNd`Qlg2hDO1sksP(K1pW2QE|cyoM6bU~iRlV~q9R zhRw#j-rcfmWLI5Lt1`KHhPNwUb`?3oz44q~s+gBex%n~{NwHToT0sT_oQFC@AxXA= zHa0-ypfM1F;1N6{SjDUlXL{yvKv8tR|51uiteoO;id0k#`!wUmLmoq@EJ#xMrl2Dtki>0z3@&LNx zfN0EKfdCU({Yr9-5ew(RWurn~$56{v?$bGct?o)^Fibpir4QG6Xm_I{J5D_`Rm8xKx`46xEIer@ zlBQ?Ofd%0OjBog#+fJ7n%c2ycZvNtaI)D(8xYY}5yRZUiD<}e)3SQ!n34Cl<(p?q9 zvi(YLe6adwThnH(!bgED@(=ML`m|tw*yO|qj{4f2wb0NhlaQ6R-8#}%(0WI&m5^RR zwoGx(=H{nMCf*>e?V;qBnYs0`ZchpgLynWs539#%rxy-ERBN267T!ngid3yutN3ix$uCQ+};`(kE9tUeJ-Y!&)-+D`K+j~ z-(4-5y(Z$f-rgo}-{&qcIYJQ-tc{Y*WifX_a1aJUW;ospj#lFHdwttz7Q;IcgtKAIRLyI-96kQ4{~P z|72E2j3i*sR<1WLhNW6W&Y4q1_5SvKmAiH_FD<^DZO-Y+yr%c3NO`zj+O?#|;Z>I9 zRRTaUNobapJ1f;+EK|v{WlWT)QR>~cfmii5k0lVbP`ucc7=HaR< zE7-7@Mq~QMPiggRHZF%j-|);{k3RSnJ4b>;f04(SM+ox zZ9ynX*3VuIwIV-4r_*8qdQzOCHF6Ua#`7ZD}e z$WH}%PF(^|#R4TEGW$Mt?)#9n>HL4oN?&-UHE4^9vlp*=<-I~kyzgYXQ0KeXle>D$ zk^9Dg-QHU#hQ6u4yg~uLQ4 zP4F*8t2_JS#gFJWM%?}oohoh1fN`d`eY$&FBHU1XUkI!-KR%^H>kHbeUxsh^|9d`^ z4D6ZzTrq}}Q^}4x{QwNXk8}~ngVM4pWclt7C<>OvUHmJ-iJCX~&Y#m2dPZ>@*8S&t zc~Y!GQ|3s7Emu?30@r#Bm!53{Lmme<!?kV}n<+*?569Jk#nhsHZ2u+llaI;tlQ%S?qvlq&{?fl~G3=o$D(_Q@ hIsQjsD5mL{k<%bYa|d~I|KxASfHt*+R~oy7{Rhs5n=t?Y literal 0 HcmV?d00001 diff --git a/tesi/ltximg/org-ltximg_41cddde4a95b736a274897266cb27c5b8a348b6f.png b/tesi/ltximg/org-ltximg_41cddde4a95b736a274897266cb27c5b8a348b6f.png new file mode 100644 index 0000000000000000000000000000000000000000..aa26fbbe08b0df4bb45b1f28bdbe9ed78fa38f42 GIT binary patch literal 965 zcmV;$13LVPP)1X00009a7bBm000ie z000ie0hKEb8vp(6^N^rM|Cwo;%EXG{{TOaV~;nFSGWaDO335f^W%Gd-ouMTru!rk&S-$_ z?cBL&bhOUtk=|celwi(I8PjL)>s9w+r_&C_xjg5>|Jm=WlsaZ}^Zi~g8jE$>E%=rF zvPuKQT> z>{XtR=YyQV{w1KAb7RDrd)G|hZ9q^00D^n z(NI$n5x1#BZ^=hEtd)j$5Qs)Z?RJY2n}*O-944)zI;nIfvE_hJt5t`~Hx>jd(E+Da zT7|}A0Eet+m?mz57v;-7dXyphR?)ts{84hfR;_?av zbt>ea5E&zr&lhMZ(I*_|?tB(07m~D_p2vGf!kJ|nVX}!X%$|qf!%d`cw=y^6NUW}# zlo=5kKG9Gwo;sme9eQ5i#ROjjgC;{ql-yInBxp&4$`+SjNDSiI9t3^jS;`mGT)^c? zHKMVo$qAuRBJL1@9gD?gqbPgYMpN%N1yWiJ?LpAzQU}b{J8Ky5|M>obC*B34}Md n0%8;G#1V!V(u5H1>1O=~M3xtNP}5!m00000NkvXXu0mjfJT$%T literal 0 HcmV?d00001 diff --git a/tesi/ltximg/org-ltximg_5c6a52e070f6e7a9d353e2fb281d3431b02bdb3c.png b/tesi/ltximg/org-ltximg_5c6a52e070f6e7a9d353e2fb281d3431b02bdb3c.png new file mode 100644 index 0000000000000000000000000000000000000000..a624488ea883d17c18e568204ba09424755ba92a GIT binary patch literal 1251 zcmV<91RVQ`P)o+!00009a7bBm000ie z000ie0hKEb8vpe5n9ojAK@`RbVJ+nWu;m4``T`Um0MR{v#5GVLac4zb zBNg4sKesA{xK-M?HKE|z0Ev5ApTHj;a~$W+ozA`GCTM6Ha%SfH&iT%nx#v#l>ACt` zz6y-q9lO@wpGeol$2eih__lLoi+DGcz}Dc^DoZxpA{-P5z_9zyeCX zKicg?X*Qb&9EC&_Cpc4)M6`9j-gv_vJEiDk2u8u_3{IYv`O4~AI#-vF6<9!E>BL`1 zt+EzLYJchca`3fdwjr2~PW*s;zF@XJPN6yUbEB&?59&ysR@bzKQDR0jAqBK5kVpwV zuVee@=rC)M2oRmUYy*4KZnby;Tm42=hF}z|#@n5}r2YT&^kld+QhBm0-<{frt<81O zst*dKiPNc}#h9F$US4{(IHdRlepoh&S zbmb;B!gskFk*E@#eMg7Qlaph<+glr|6%obatyb$Smm6S`B@@HOuU22}*4`D1xATP| zjN#H9jtH*Q1IF@F1r`SQa(U5QQoB}rZ?U#F*W0ajqp=TWCAY?PhwAU`*5=BK_+g0d zf!qK_RHVAaV3jk+QN~`JpQRb_BtYbz!O%oTZMb7&_m`hmbSbJ~aPay<^-;$nh=;%; z11=PX_G&xAiU##3PO|yPLls_pOQdI){USS7=8sNZNz_`ajG-NZu1;+rBp3Hn8Ph^p;eCnexD z#FQRYu{o98sN`96Vu1N?qjV048Z6v^#jVKvZNd2vd8SWhOp%s(&Q`8 z>-pjP^$#$~UAfXToITH}0iv@ArcN-<0y^~*MP);D26Yl83fW<#`#447Dw<%3NGDN* z5$Ly0wwV*AuS*sL!Hi~NVE|AdT@}3bmrbQc)@0xi&ng27N@Nf8t)#1_$Ux@;L!P*m zA?a`yza4*Ph)p=lTU3J}okhU8<-saooPLp^p`$_Lh)^g_>Viu|OJrPv9Yw|wB}%ML zZ8jvSws6e9?2~8JL}p=YXun8LXikhiyLjV^D|x=1C(r51Qw0AZ@aT6QWsUA3a&Gio zD!xl2EvkUj|pY z%F;9W0n0^jraaG2Hb2E$^%sF(=oVgwe*KO5Cjiz@e&KqEY=r-|t5c5|BuvLLAq46v4zu9P{N%%k?A6)V>ty}O=ePo3x98Bp|Ts1KLNS_X4Fzaza0Po N002ovPDHLkV1foS*UQ6)az zaLZ_pNd8Inxv;(2*hV9tBw#fY27+( zHc#Ypbb;Mm-`t*@xcv|ia*FPbN>1bwl?qlO?{$}A^ zGC3H^==FbJ`=A<9C&yQyI~}8BdXvO>5GoH=m6GHM*awd4C?WRna{f(o+_DaDPvu3A zK>jnuk{Sx4rxdD3$bt4@)pgvYkxZN8FP>EehCtk(>~9y$^Lp`h0GVX7S1GSyq|m?J z+VHJ1FQgv{W^uWkGE$6>mGXTZ8RCc_t509<@9k!@*N6}yH!(>Hx_M8A;`{Lr0@4>k z>JOe_Az%tJSZB=P6pRQ`d?_jBfCUg$2yrBx(kt`dt|3Q)@42A)bx+Ks{(`3s$)8i> z1N%PVK=ZTn+av40QL0^L7id~#B|G8+t4T>$khmRGT zSj7;AIf9C0xkpBK(T|GI_4-prd`FE~<^^mbMe5nZIuoM-<0TN$Pn02asDj(u9L1RI$w;K%6v0kpjj& zaK=(VLKx%Jjt_@6U`QL{!_Wq7rAZJ9XQzPzVI&HWkbH-baH`}J9(s&tci-*K{gABK zIvsCj-;eM6&f7P0L#ed$_y1<#(C4Ec4h$6H;KM z;|=vuC$ZE?Az`V$=;p#Zu)hAdkOx<}Xuhs(kK_PKX=;tepJ8}bmTyzCVYaSSpJ5YP zkb8B1+r@;;Nx+*)9a2&=)92=E-y=+&pAj93BaY)#{WsYL#=_yxi%T5uQaxu)a$qAU z*yOWVzjbxtGRpYT*2Vtj?Fm`lisqZ;N9MyYcs>ItJv92oTBD(U3c*-yG%#1&V4=^j z!70c;P{eyH`eYZULnVFuFZjFAmI_Y{=xnBRpv%0o$ zxz%i~to*m9%|`PtTP;?4=|=rzbrL@eVFcI+MzYujEf`1LU|!( z$eut)R2L%fs}Tic_RU&tRuuq2L-mx6SR2g^QAP(p$nAcVef(p>2CW+r z-Itxg_1rdDl#P6kjE#?veFJ7n4bQD+^F;L&nv6n$MRby9RW4A|;CNrDYK4}0po#2cV3kTj@QJ@raf%%H;w*j1B9^kdqX$YjnH zDd!wM-g_wue7B8-j(4-9wjvOYK;C4YAy(u?)v7YpDILP~X(WrGoiDa>NelxT1%a&j zPVM)p7*I|n!NsZm+ftgE5pnURPEui{8e#&ItgqUJ32kBHHc3Jr*r|pB@-1@yp$<6G z@XdnpK_FW<6Le(Al6R7Ao>&B8G3+Rml!wqoYs=o-NJg^W`aXA_EbzpwAR!%Cef0RL zq((RoVG@IArjmej*FzpkvoaE33ML67%McUj3SI)t^T5s`p)KqzL+1G_fLt4-z!m%6 zeapMoJO8%l&Xc8HwI|_?54=g=V$IyDHINu26fHO-qtsVRQ5lA8oBCF$e%FO85^UJO z$TH-SAb)qClLeZk5=U~G^TWltEX}UWv#8t>@?QtgYMku55-aJXE6H+{pPK$oE^YY1 zbG$mi6+|+YF=La!t(0NwJ+d?6G8+Z&;!8XjhAfT!yUW86HZ({uU=zzQ><{v=e0QuY z2J}2;DHVC9O+CL+fJuJmIW@yDgjwZ;w4=7o80f=^r5B8J0{dU#TrWfwUde5nN4V1RTRfZESPT0WaYT1nXHC3x!?!0+X{2=8qIrrRi{^x(rz4y$W*F<9d-#=7=osV_h+1OZD@b2Av>awpFzb)GX{rMbCTtGz0>wRy>8a;i{JO%!1zk$7;&j)=6`8HvPg3kyXPIW}z*DqbSs z)Rl`F_rIrM{~Z}Qs=Plu`7s(DIs{hhyUFhz1|1!pAp?dr!6D$lbW8=aaF{XWwv0#H zj2Jr+Wf;E;vi;wD>+OzAXR-K8@Tj2=4o%X3tws(sG~{VaHd>oRU;n`L)gKB4U!v22 zzM9BKVM3ETer&YO^Q^ES?C$9;7K>k8IIn1%Ter{=CnhebCM2*y8#-Zq9 z+~&3C^Q#(Ob2>eqJ1etznPr5D8ko7e>rc(W7jXS#?I?u~@7=m}etuqdVJ`P+U9^E3 z$-ZZ;yjd=HA~hHBRxU*4Oh^J$L1_tyb&WdUg2*%Z_`Ba*H$`Pk224_XCG~rC;+hof3v)LnR zL*VY7-rk<)&`=AI%cau3{sFovXN!(&LZJz9(7r+lz%iJeozW1AK)h_i0?NU;M1aE=5<P?{>h)2Z0UcUyU56vSY zL(JfVBTsafx-6BvSw?p!b2!pvL9^08AF;4j_n^{Rd26}ciGXQ^l30?9<-H(Vgm%T7 zEePbXFR9FekmrYC)Q4q&bN#tag8zv@{c=cmJuLc^=Vj*7T^Nduv zSH!a+>RCQCF(!UcI2aE~TlJtuWkD0c#B^&sn$Q{#9Q~E4<73-yw~L8xHrsh`X8!Yk z^XAQirl#FJ?d?&2fZnt51CfZo&Htkv7#t2xra8E2Rm*qI#}oFEeBQ09J$Bq?{ztK> zT5{bR?<*Dx5zETEIp&uZQ>yg{W8)W@!I-b(tiK#0O-S5guXArqQO zU8*|_Zq42?$0Y9B^bMUsTdQnI`h$ffNxj&^o*DHGB7_4m84?ACwV3P+LL!_EQ7NuB zuV1PAc;eE=`lr=ZM`kR`dY;XwRs|gI-n-u)Kl3%8*U7D|Eo2i-RaJ%1AT2HX+u9Dw zNut|4e)4p5XyEh4x<=W-gerZz@_|=RJ2PK$-^e$cpu5eCbgu61*t7Ht!D14D3Q}LR z;zFe$Ye)oah*Gx$0TwTAwsQj6EO(U)`|aARr4vn1}#RvpE1I z+^~d6WxAAiiJP7P(To+XWLzisfSz(uItKm zqzJ86D{`mZ#n-$B*{Z_!idG$m`Ms#;=Vs3J_41zVJbLr`v_c?MF5c9dG9cs~bn-6q z5=L#z8X@qC^WMW)EL}IpHmH{fA$0$61ykfy^k-Hc#;$j8G>hOC6C+Pb4mo zR8p2mOi&tm*JaBoNwnmG$|{wsnbTU}}A_Fgdv_BRP3hH~`xai0~OtOsG3E`jCx?6_G#j2uB{2 z2{tq$S&`b;6aa!&O?5qmZlJ%RSyuj*djGO2mBl4E2=+7(kGsa@Kme{oA7QuuSNK4q z%4U|SxXKH`<5jEWd(41hMjAHzuazri0YNY(%Y#EB*-ToiSOYOb`>VXE)Sv-jmvu*^ yTHC862%&Ol;je%MVH=uZNXLLjASC*~bNdCIn_0k;VOu`{0000RA>e5nN3VwRTRgGvX)`Trt(;cn|A2NE{s6e2EmwUOr(^( zl$JzI40KA@2%=l*P!pqxl_|QF4$*}gQy#dni-sZT!X_rn7?a{kf5T}`F8956=f3xF zObui*IrrZ4@jvIDd(OQ>M@PQD-rm5iVC0q2XS%xFJSVIF?+9ebf$<9$|MQq+fDL9v z{&Y?U?$;iC@%d+sMm<)~=`+Pbp|G>PEvuZdci(&eR^{tQ2ao#upMPm+`1Lp5{OjOg zZ?6_B9-ZVQk560_*`A)B=lc8a-TO7lmfuiRXUmzlFJ1oW#~)0#!NK9KLgC@V-^|G; zl+GMdD+fH?|GT5(g>&a(H`h~xu(cUBMvn`53pYQx@u|f@w*9>Ii#f@#W$P1u*cKL- zRTkwA!90f4L@I)##YUPUCR%g;38k}zG@1jR?jKk5+6)`-1o=~*er8}J@5At}B{(=V zyji_tPBOeOF=@^u(XefYTe`Yg-Eg$KJciUnDq_8|W;((#tJQW>X)u{7_9P{n1Yyma z!*R`o|xHRPK774gRRZ5K_bYTM~gcpt%HwV6PdZc`{2v9b+(po!Oe_RWgPzY z&UZQqK@zAet0FQoI<^yr!lvJces1Vc2yRW*Ozec(qhBe85UnPiB} z#=F~1(=rIEL5QS~%4)1fW)4JQxI=;aZ<=bp`G6Tc!`+tg{$?2xy#|nFy#O5%> z28$G}Kxp)&1(0NydFe0!;3I7Ks7>CqF00Har$ep(67Fc1Qz;9B3Bxl8j*yBKHEMcf z<$wjlAt*~4H+3W};ehQ3f*ZC&P~m~RlL0mRqYoE#mZPQgetlnQH-Qq`ccWgXmJ25( z*%CQy%|{+uG=yuVSt-vJvo++xsihtMt?(|kEFK*?45>%(EG;b{LU*E#sH{bh4gOsV zS@a`9D73xMLo_C$90siSmIEB2hsRoH7vO=POEox^hkfN zg35D3h8W{H&Sm{{u_za4e!4)9mUfizTBAanj|4T%W@DXvLW&~Iw+dQPK88?>LL5>3 zQKI>DEUzRrfhfPu5Crlh&3rgQJRRk2ru-0WO2^*g2^7+< zwPQ1jAcu+`qQ4U14x#3SU@9@`CCkT-vP|M&j*fuEiB*H2v+X8O2) zSXIi?5P3rzp~3o_@YL+XCIMk%fWh0teC7Ix3lHVI`MdVvubT8OUJF-C*ZsxebO#|- zNZlSea=;b_Brz+Z{b$*UQ5eUGab1QdV0-}?p8)9EQi$DpU)OqBi->D0 z+O>$fHHz*PNViQK?7H!gbkB@W(BJUkmlI7@#D$Z|$^U%!>xsqQ!I%4-|8x8I9Ry;9 z@F5<*Z2VNhh@$_2@sziJaJ;><2e4%xTy55%IFre?nhn(&74-GnO2^!SlkV7$-5q5E zX6F{lrFFp4@@g0a<;^0PfLzzTY5TV1t8qH>5#4k;o68s0R+b_=)PTECDM>`S|L~nm zy7#w8?d0r&I-{b*;lZ!#-?R@q#f@?l2`(XtU8*%RJ3qXSfh-V!4il*oz-T&?ZTtNe zfY+9LrL(LOD0B!nzF(SC7E4}u-iG{i8VrdJ>Am~av zv;(c?)zRUBdPsSm4ik3vD&M1aP%$K^o-8EJRDmRPmJuKcddH6guCSzusE83L7=aaK z(whgVJy<%Rk*Nz*kl~7qa7S9LM%-~Q%J3i7s%SQ?6(DsTWGX~{UkW+?#rbJ180M(- zxYysxdi@j@8JphHP=k~=(G9wsxR*`RfB@J}I0*v40%oB^d)FWJSnT4wZcD!eJ5B;I zBA|mJ&u#)}G(>XXZ2Q;30?XRURnG^+{#&5zK>^c1`xu}?e$v)u@~X9Cb~_A0vZpTu zlr%gbW1FRQyT-QG8(^KMXKgVk@}>}+Ox_bJ!`A5u(>Cj0@?kEP)5j!#UOC2>U}le`$a>3wmbl`J!CK>K$M-{eyD zzVIL_&ofsj({5y$$5VNKCnU zqR8r90i8o=%4zNHAP@H-;V#RKEPEcSmfkzC36tv^0yg}H=RMg0Hp15+D;x^zR*4z5 oO%#1^Y+v?{eaY(gn&C3Y2|W>GPsHmy;6k2KUO zN^6hWe6-)c;QPakAMUyFy1VC|i!nCT0a3A20RRAyo-Pyy008H&bzTahYmQ=r23-qE zFI{V20D!jhF9B0UX*sTq#r2>XW`4lUY`ZvfOXjb|lLZG|4aZA6owX8$rD<;@vQK#; zB=TeAD+DJ6VSR6)riv*gB`6p>?*2H7WOtDs+=iho6`7tUC?<2dFmfaFGx=v|rj(#` z_ba7%%8v2lrrTEHf9BlgeTQ3QY#mWq9jZ?%hp%h`bAyjmd<`8OhOcH0PEd4*M@P+B z*^2ciC>tljl|(-1T+QA065roUJi>atGG*#0O4KJ;4!5 z*B`rBwFG$Wr|C?WH=HGRaFCIaZQ0bU4rGoKIPP)<27L|II_hYvYkgW(xm`BXDktTw z?AmYIn9uJ?G{42c-uD$fZ9G98rRKNVU`fZ-i1k`*VNCw=-}h#poe_kn1*A|{+34pN z|J|i7S3QiLT)9${$KhxOob9d7Xj8QX)RA_Zc>>bhI z(kEIVyR2@}O3vyijjIz@I!L5FB!K-6;9&Z7qK}#4Nmzcd3%i{OtQ)K>SBvId`F81h z*~UWU`g5oag;`7#y0V>ny|PH-UIb?wn3zKgCgg*paRsYsLOS;z2qa_LZ6nbXu_DG9 z3Y+}a(|()pVq(P?T;m;CX%iDwy;lz$ii(S&NiK)mg5AmbNf+zGp@$1SKQE<}%4n#m zscS1VH}&PNaVS;Lv#naHLn6&a*S!W5*F{3WvTm203>9*G@*(C=}O0yTpJGl-bUUtcSQ9be$ERF~hgQbZFY<*PwT$vmP~dHmt|?xO8!IHa5{Zw@?xx>+08810kytp8|VDq4HF(xt)eYqjpi=MR{)c2 zs!6yjCCIHnV`4X@_`_QGeM1+X#}~+`=RAx|OS-+__(Znfzq;p#E*UjGJH*^s;%8}a zEA)a_6US*!NePX57j)9U=4~hfG0_E|JYcU=hPo}Fk7?9Eo$Jg-PHO86AjxM^5l*x} z-?&TU%F`Qh$)-71f+?+Q1kb}C#Bsy`+yfM-_O#s>%`giZYPT@hIJF)kZJ6%{UWNO@ z3LZg<)9y=V5tB;hdC;HoN|GN~tIbRfkrX7=b}N#DII^*N<+EW%_@IOJkjH1yEP@)f zJ1AJYNuMRt1M_Gs>iI2qiDF67Y}0;0@Pa6mo+hD3dK#>!o^E=ccXtbhcpE~)oR?(6 zyOqbSGSN1SFg=4!&Jn>&<|FqpD6$i>$MX;ZKOJb#$6d z8asETQnHv6C-s~(zRe*&wdJUB>xV$tz4r-&T};9?`~{h4unK!R=?Dw6hejBi#(LjG z6jL2G#`Pvo5O6bsV3H@L+`QO>U+n*+Zg7Vgt9M5#|VfX912Ug!&Y zKf2s>u#FOfJE$H1O0Bu75iT5+uSBp99C|iizBR_bQ&Bh+DjW0}8hGc@L4ZAa$hlOy zF5KSrX_B1WL|QfE{Nm&!%+yduKZ$|sU}NS;8IkekU_?pzyi`IJ8$;H0>$tu7V+dW3 zmnbPHRVDO!kCS$ypQ>V`sS$$s73CmoNsgoQOv3+3(-Qv}d^v{-rlRwe_P6jNv4o#U zB-sMQSo0IpvE`Hnucl3*vYFfqJ$!9#ip-z!DFap+eDxpcn2z2SBUy6IJ?^)~#fEhQ zoTt5)MJVzYTX^w+XI7;IbY#W(pu|SUU}ZybQ4!>!m?pZ(zkjL%-bxhN8@?eqQvd0L z1>E0xJl2Nc9ifxy~yp6(ZpHqZ&nCfmqI zAn#a{+A7zoX=fZ9M(I%vwg`FL8Nfs({v{&{c=Re0GU3ZENkV9R9_usJQziF~GU>L@ zaGwqR8YI0L&c%!KP)7(q^QH=YcZ3(ftCKZO<{rqDWCpQeDxAq=aIevQF?=Lsk)RJH z@s!|k&(GMddJU4XdTg>Hn?|fqpEq&&agQRs%2Ec)2MGO5aNKx>1v+6g>y=HR2l4M0 zj)af-FHFL{QrF7OTKUlcGVN3vN#W@4eK@3t&XLDXhxjLs`PQWuAy8Ml?oGzo`=6Q7 z+*UgOwPNv~j{6cPDi{j*``ArCJH*2nkvK>-crh}mOnXV3Mf zmCE#|5B|g2I|#je6eg`^&-Vo}pwZlvO`=eED|Bi+9B;f`S-pG=W;);zqjqd6eS zh46Y_^-tPP1S>6;M(xj3){M?eE)^et5I&8;Y;kO1AzMVeFL?+oo%5r+4&iY1=cDHx zb`T4nI`GkLIKLIi>nK$znf;@*w)$lsu_}1Py%}l}j6ofYPtho6N@G4blkMYP z=k&##t$y5AKH8ug9ogfi@cr3cGaTfwEuQEtDzZ`FLzX?4fi(P&&1yF>s@;g^+oX+r)7&y-X<-v0){84EV17>Xs8+0cCAEEc zi5F~1jt-DacTmO3hwG&Jy=Ny{c~bP9hUH|OFJ|05j=HI5pN8|s^TB9WRh#yKsAn$D zKR(h-NYxlyk?=&`vMXcpUS03~oWax!$dLFD=O~059c}fM*1R?Kn>(~)L)cAz-;VLe zHjGN_<%+TNysjrV`ROQGWO+@F3%8h6LaJFf8ElB~F56h&;_k*o+N72}GCY#(ocvD< zMp=Vc#Wwk&IWQ}?4vKLeOc{2Zb4uhFcfg;3(JdZQ+jIN18&`Xv?W$4EAZ zaRxV|G>LlcmX-AvlCA}N0M}R%K0F`J+k9dmc%$~$;qr&pKSq6Pk6)&XtZQ4QU=&6o zt^k@y9|HojQ>LWM(wqzZ8hC&w!oqiUYs8{_MA#0BsW4mJw9tJ1u*AyYc2K65($>+g`i(QpMeJ?b>gGx)EQy zVdPWQwYc79;qiQf*#We+=dTDx?;<;{10fK}^P`Bm>@8rpwY{KAMt`$!`O1)i5Me zI4F^0&q}Xxn5ChZ)lWLzGP6JI(JIQ5{3$K8$M2UDBIdcgtcU;cW1GO~EI76LCcUWm z0J(d9DugJE_Bk7QO1R#wu2;c7++i$ooPp)B{}5tH_# zQ+uhl^6gzbC*i7%d!8$e55^Xd*Dzhz8Vx8j`~FPaS!4?fX92Rphk*j}gFR#%d`L{L z;$I7|_q<-Bro|hU%ku&0iMgE4o!7VQmumG&x}}eGEW*usbhVODW99#MzMk@u9LFaV zikk9&Eu@BrQhM}5WlQS}eE{B7(v0u0U^$19GMf_90a%dzn&EWc-0_bTQ KLO*IchW`(*Aaf%C literal 0 HcmV?d00001 diff --git a/tesi/ltximg/org-ltximg_ca02030f255196914ab3a21c0b5eb83072e92d47.png b/tesi/ltximg/org-ltximg_ca02030f255196914ab3a21c0b5eb83072e92d47.png new file mode 100644 index 0000000000000000000000000000000000000000..24ab60193f9b3b29641da1ae00c4bfbcea04a304 GIT binary patch literal 1551 zcmV+q2JrcbP)e5m(OclRTRfZEZCJZ*^P@jlU1i+o0qECl}Y>qY7{{c zOw;U}OcGE*8rupYNX)bfieQ@Bt+ms*s1+3Ys z;Qyb7<25;TMsa^~_B#U*@W%(a$B|;Hc$mm za}Hzp-hSuZp5DG{^>=eV(3?wl@ppAs1{8$yBvZ-Y(2wND7H<4psrZ5fI{Btt3ZjCa zKK|&#F3$@_P~#(mL)B{at1FjPvp2U7J}Z~6sm2mGf5}wphws0$^l_HEcR!R)Khl&V z`Bu8}ekX)|m}6XcB=VOKr=j3Y11tehXcfG} zj2A#@WU;EVT%HXu&O$hfLYDB)IlU^dSFZ z^)JPyB?DWLa0$aq<5pB{*O^TJ47IaMbJ|-^Bu^;oz&*5*iHO z+hF*4-!BvQ;BLR}Oppi6?K~{6!C0D2F*=A zo1;c0bXmupEnXFz!6T=;amenl5gO@*e9Fw>sAc1eQU={hAudrEtY2+r7LmcAR1w@2 zjmZIE2<0bB2}lKRh9#7lj_j5r8f<`Vnh{FdNVL#mLme>&iTihGC{7bIa#PsY1X~>k zcBrFd7vv2NkQt@*0OGS{|9izji7I|U zZWs4%{48$E?Pb}XmmA6b-R2!&vYQ+I_bhe-`yUrH&u&0s{@DNk002ovPDHLkV1mp$ B;i3Ql literal 0 HcmV?d00001 diff --git a/tesi/ltximg/org-ltximg_cc429dea9befffee656ac9fc36b1df8509d3c7ff.png b/tesi/ltximg/org-ltximg_cc429dea9befffee656ac9fc36b1df8509d3c7ff.png new file mode 100644 index 0000000000000000000000000000000000000000..019d01b06ac39b6aec646b618a1ccb90d56c41f0 GIT binary patch literal 377 zcmV-<0fzpGP)P000XJ0ssI21(mU+00009a7bBm000ie z000ie0hKEb8vpW)Nud7{hvR7Vj4<}8lWzgOBXLZcyJ$x7A>3)HwCEK zz`*dshxYGr-cjVfwa$^zZj?)ZV-@BSKkET z`uPXg+dHDE0SZE7fyy9kpmuqA1(4v~`%fTp5E5wZ-u;Ima`3oARs$CVDub}0B0y@* z`b|Jn;I={7Ky|>thBykV8lW;PvC-Q<38)9^NCpO|B@7He5uo=Wjzv=g6a@MUE(=kE zh0M(_gopwSg|ji$#l`#ydA2oVGT X$diWma~#u(00000NkvXXu0mjfr}>VP literal 0 HcmV?d00001 diff --git a/tesi/ltximg/org-ltximg_d3116a10855bae8a6d0cb304a27220822ddaedb4.png b/tesi/ltximg/org-ltximg_d3116a10855bae8a6d0cb304a27220822ddaedb4.png new file mode 100644 index 0000000000000000000000000000000000000000..0027ad4e0c5e47900675af63ad7a957ffc07ddfa GIT binary patch literal 329 zcmV-P0k-~$P)gn3@Cyh$d~hEqylLYGh@`!}NSbNJ-dxcEePTmd8M{DpJCau_Z$ zY#5+o30Nk<{R52EhYubM?UV`k3@U>Wm{tu841t2c>J(C`PM+A0ss@x-hflqV=C@Jq b&<+6r8KPe&eTPB*00000NkvXXu0mjf@wbE) literal 0 HcmV?d00001 diff --git a/tesi/ltximg/org-ltximg_ee449751cf9a5061cafa5f18d30c08dbe8c20a11.png b/tesi/ltximg/org-ltximg_ee449751cf9a5061cafa5f18d30c08dbe8c20a11.png new file mode 100644 index 0000000000000000000000000000000000000000..aa26fbbe08b0df4bb45b1f28bdbe9ed78fa38f42 GIT binary patch literal 965 zcmV;$13LVPP)1X00009a7bBm000ie z000ie0hKEb8vp(6^N^rM|Cwo;%EXG{{TOaV~;nFSGWaDO335f^W%Gd-ouMTru!rk&S-$_ z?cBL&bhOUtk=|celwi(I8PjL)>s9w+r_&C_xjg5>|Jm=WlsaZ}^Zi~g8jE$>E%=rF zvPuKQT> z>{XtR=YyQV{w1KAb7RDrd)G|hZ9q^00D^n z(NI$n5x1#BZ^=hEtd)j$5Qs)Z?RJY2n}*O-944)zI;nIfvE_hJt5t`~Hx>jd(E+Da zT7|}A0Eet+m?mz57v;-7dXyphR?)ts{84hfR;_?av zbt>ea5E&zr&lhMZ(I*_|?tB(07m~D_p2vGf!kJ|nVX}!X%$|qf!%d`cw=y^6NUW}# zlo=5kKG9Gwo;sme9eQ5i#ROjjgC;{ql-yInBxp&4$`+SjNDSiI9t3^jS;`mGT)^c? zHKMVo$qAuRBJL1@9gD?gqbPgYMpN%N1yWiJ?LpAzQU}b{J8Ky5|M>obC*B34}Md n0%8;G#1V!V(u5H1>1O=~M3xtNP}5!m00000NkvXXu0mjfJT$%T literal 0 HcmV?d00001 diff --git a/tesi/ltximg/org-ltximg_f243bcd039f21e4dbb99e46d60f3f9cf9f5c1311.png b/tesi/ltximg/org-ltximg_f243bcd039f21e4dbb99e46d60f3f9cf9f5c1311.png new file mode 100644 index 0000000000000000000000000000000000000000..b05f23b1af5f94bf2f496884a1dcce8a099442a7 GIT binary patch literal 1929 zcmV;42X^?0P)e5noUzwM-+z9avk6oFsxH0gX^SV%r?Oxx>b>^RS0Vd zlC=Rf+aT&T2_Ji%naVaLgIT8>stEo3b&!6$VR=>X6Zd-4hSXup%MH9yySMMpRZ+$WZMyZy#vZqLl_ws(xvYQEmv>sT{Rj8&`b zw>ajwdQaLGnY-KF$J^xmv-E(I-cdZ?+T0+p(m+*VGxU1kOj}ohGJauc?I~g^T$~*s z%mhTx^j&?>g)Y6{0Mv0EMOd#gL-iC#nF)ZMb9`LD7#~63qy!VPsrvNW4- z!2E2|0|%HpU%J^*``!J_1=>f%@Rn`=Wc3FKtA6MqEP)&SHA}j53GFN_(lA41MUstJ zk#M#*H^{X~bSk4n3g)YsSpY@6Dqr^z0mde#0=xYIU4E%B>ec-(`BrU<@oGu*K-8q+6T6RI68r2E@eV)#vML zzyiVYNCf3`puw7`nwwj&rYANxe@&Zave-_nq*k+$?oCfI`WXdh*JKY&)`HOKm@0+d zG&Ji~tHtw!h^Z?QdAeBo+NJX0=Z$SvOS`=jKTdn2aXN4*Z)yhU;QpjcK$1WygC}`Q zJ9R)zV0KZnUV)8I)5F*gaJZkrl(yiDp+DdKMJxioHFbxx^nj`WY+cx52neb^7$1(& zhB5t~h}hCVq)IeySl09w<4A7~8Zf@`)u0GP0O++zd~C2@Ha*4k!o(sXikrvdkDpWD zC7SJ|RpGnJ%#O#O0_|POo0?0LlQoWy?+@0k#49~J%0KAkrR4pQ%0S|QVB%G{1t1@g z3q^aFadgbJCV{hLLju@ozwz1(mPz2Mf81mWac^Y3f}XrL)-sqvTPPO>bE~V5peaO| zC+zY_lu#jg02mw^+CF?jK&STv&wHu>$Wjg;AG+uDK&Ph|CjO6CKV@3i)?Y&S;gCD$ z=kBt~Gp8nT*cObl)a&e!afl}hI3W{NbAXkaJP9l<^PCOfdi^Ubvdk#;vokk2I3U8J zQlVgp%LR&(tt)fNyOcXMYQb(PRxfFTUYeu|h|KLJ0D{VJ(&JML zdnqt25h3~dtV|bG5~kS_jY2Atr7_$C=@TLN03-c)<;@k^LdusuDdC&8n1>830%JsS z75~v=I{P3P3za-m5W7K~;V78k>GE+f4KTfw_(Ta=!x#a$%fG!SgiZZJ`$D&2(TTXyzf)7P(51-U!#_YBim}0=1DQVd0iS!bVjZ zmY(9|Dz(0*87G}$3%R|wGdF0a8Xs-|vhLHlmondo zwbAS@nkHg=k1-|QT-+8S+P5ZaL|`$3q{~|r()9e#hZPPx-fU9trG~IDa0@Hf5q71R4wqy z8MoZu*UV_Iwj_8Ii)Q+q2qM5-P;dSHFaW5@x<9N2UG7ntf0oIV3Yh-^C=}J+m<~?m P00000NkvXXu0mjfy|JF| literal 0 HcmV?d00001 diff --git a/tesi/tesi_unicode.org b/tesi/tesi_unicode.org index c44dfc9..1e8ca0d 100644 --- a/tesi/tesi_unicode.org +++ b/tesi/tesi_unicode.org @@ -1879,7 +1879,7 @@ for content equality. {\EquivTEX S \Failure \Failure \emptyqueue} \\ \infer - {\trel {t_S} {t_T}} + {\progrel {t_S} {t_T}} {\EquivTEX S {\Leaf {t_S}} {\Leaf {t_T}} \emptyqueue} \end{mathpar} @@ -1966,24 +1966,24 @@ is empty. {D_S} {\Guard {e_T} {D_0} {D_1}} {(e_S = b), G}} \end{mathpar} -Our equivalence-checking algorithm $\EquivTEX S {C_S} {C_T} G$ is +Our equivalence-checking algorithm is a exactly decision procedure for the provability of the judgment -$(\EquivTEX S {C_S} {C_T} G)$, defined by the previous inference rules. +$\EquivTEX S {C_S} {C_T}$, defined by the previous inference rules. Running a program tₛ or its translation 〚tₛ〛 against an input vₛ produces as a result /r/ in the following way: -| ( 〚tₛ〛ₛ(vₛ) ≡ Cₛ(vₛ) ) → r +| ( 〚tₛ〛ₛ(vₛ) ≡ Dₛ(vₛ) ) → r | tₛ(vₛ) → r Likewise -| ( 〚tₜ〛ₜ(vₜ) ≡ Cₜ(vₜ) ) → r +| ( 〚tₜ〛ₜ(vₜ) ≡ Dₜ(vₜ) ) → r | tₜ(vₜ) → r | result r ::= guard list * (Match blackbox \vert{} NoMatch \vert{} Absurd) | guard ::= blackbox. Having defined equivalence between two inputs of which one is expressed in the source language and the other in the target language, -vₛ ≃ vₜ, we can define the equivalence between a couple of programs or +$\vrel {v_S} {v_T}$, we can define the equivalence between a couple of programs or a couple of decision trees -| tₛ ≃ tₜ := ∀vₛ≃vₜ, tₛ(vₛ) = tₜ(vₜ) -| Cₛ ≃ Cₜ := ∀vₛ≃vₜ, Cₛ(vₛ) = Cₜ(vₜ) +| $\progrel {t_S} {t_T} := \forall \vrel {v_S} {v_T}, t_S(v_S) = t_T(v_T)$ +| $D_S \approx D_T := \forall \vrel {v_S} {v_T}, D_S(v_S) = D_T(v_T)$ The result of the proposed equivalence algorithm is /Yes/ or /No(vₛ, vₜ)/. In particular, in the negative case, vₛ and vₜ are a couple of possible counter examples for which the decision trees produce a @@ -1991,19 +1991,19 @@ different result. \\ In the presence of guards we can say that two results are equivalent modulo the guards queue, written /r₁ ≃gs r₂/, when: -| (gs₁, r₁) ≃gs (gs₂, r₂) ⇔ (gs₁, r₁) = (gs₂ ++ gs, r₂) -We say that Cₜ covers the input space /S/, written -/covers(Cₜ, S)/ when every value vₛ∈S is a valid input to the -decision tree Cₜ. (TODO: rephrase) +| (gs₁, r₁) ≃_{gs} (gs₂, r₂) ⇔ (gs₁, r₁) = (gs₂ +++ gs, r₂) +We say that Dₜ covers the input space /S/, written +/covers(Dₜ, S)/ when every value vₛ∈S is a valid input to the +decision tree Dₜ. (TODO: rephrase) Given an input space /S/ and a couple of decision trees, where -the target decision tree Cₜ covers the input space /S/ we can define equivalence: -| equiv(S, Cₛ, Cₜ, gs) = Yes ∧ covers(Cₜ, S) → ∀vₛ≃vₜ ∈ S, Cₛ(vₛ) ≃gs Cₜ(vₜ) +the target decision tree Dₜ covers the input space /S/ we can define equivalence: +| $equiv(S, C_S, C_T, gs) = Yes \wedge covers(C_T, S) \to \forall \vrel {v_S} {v_T} \in S, C_S(v_S) \simeq_{gs} C_T(v_T)$ Similarly we say that a couple of decision trees in the presence of an input space /S/ are /not/ equivalent in the following way: -| equiv(S, Cₛ, Cₜ, gs) = No(vₛ,vₜ) ∧ covers(Cₜ, S) → vₛ≃vₜ ∈ S ∧ Cₛ(vₛ) ≠gs Cₜ(vₜ) +| $equiv(S, C_S, C_T, gs) = No(v_S, v_T) \wedge covers(C_T, S) \to \vrel {v_S} {v_T} \in S \wedge C_S(v_S) \ne_{gs} C_T(v_T)$ Corollary: For a full input space /S/, that is the universe of the target program: -| equiv(S, 〚tₛ〛ₛ, 〚tₜ〛ₜ, ∅) = Yes ⇔ tₛ ≃ tₜ +| $equiv(S, \llbracket t_S \rrbracket{_S}, \llbracket t_T \rrbracket{_T}, \emptyset) = Yes \Leftrightarrow \progrel {t_S} {t_T}$ \begin{comment} @@ -2012,35 +2012,35 @@ TODO: put ^i∈I where needed \subsubsection{The trimming lemma} The trimming lemma allows to reduce the size of a decision tree given an accessor /a/ → π relation (TODO: expand) -| ∀vₜ ∈ (a→π), Cₜ(vₜ) = C_{t/a→π}(vₜ) +| ∀vₜ ∈ (a→π), Dₜ(vₜ) = D_{t/a→π}(vₜ) We prove this by induction on Cₜ: -- Cₜ = Leaf_{bb}: when the decision tree is a leaf terminal, the result of trimming on a Leaf is the Leaf itself +- Dₜ = Leaf_{bb}: when the decision tree is a leaf terminal, the result of trimming on a Leaf is the Leaf itself | Leaf_{bb/a→π}(v) = Leaf_{bb}(v) - The same applies to Failure terminal | Failure_{/a→π}(v) = Failure(v) -- When Cₜ = Switch(b, (π→Cᵢ)ⁱ)_{/a→π} then we look at the accessor - /a/ of the subtree Cᵢ and we define πᵢ' = πᵢ if a≠b else πᵢ∩π Trimming +- When Dₜ = Switch(b, (π→Dᵢ)ⁱ)_{/a→π} then we look at the accessor + /a/ of the subtree Dᵢ and we define πᵢ' = πᵢ if a≠b else πᵢ∩π Trimming a switch node yields the following result: - | Switch(b, (π→Cᵢ)^{i∈I})_{/a→π} := Switch(b, (π'ᵢ→C_{i/a→π})^{i∈I}) + | Switch(b, (π→Dᵢ)^{i∈I})_{/a→π} := Switch(b, (π'ᵢ→D_{i/a→π})^{i∈I}) \begin{comment} TODO: understand how to properly align lists check that every list is aligned \end{comment} For the trimming lemma we have to prove that running the value vₜ against -the decision tree Cₜ is the same as running vₜ against the tree -C_{trim} that is the result of the trimming operation on Cₜ -| Cₜ(vₜ) = C_{trim}(vₜ) = Switch(b, (πᵢ'→C_{i/a→π})^{i∈I})(vₜ) +the decision tree Dₜ is the same as running vₜ against the tree +D_{trim} that is the result of the trimming operation on Dₜ +| Dₜ(vₜ) = D_{trim}(vₜ) = Switch(b, (πᵢ'→D_{i/a→π})^{i∈I})(vₜ) We can reason by first noting that when vₜ∉(b→πᵢ)ⁱ the node must be a Failure node. In the case where ∃k \vert{} vₜ∈(b→πₖ) then we can prove that -| C_{k/a→π}(vₜ) = Switch(b, (πᵢ'→C_{i/a→π})^{i∈I})(vₜ) +| D_{k/a→π}(vₜ) = Switch(b, (πᵢ'→D_{i/a→π})^{i∈I})(vₜ) because when a ≠ b then πₖ'= πₖ and this means that vₜ∈πₖ' while when a = b then πₖ'=(πₖ∩π) and vₜ∈πₖ' because: - by the hypothesis, vₜ∈π - we are in the case where vₜ∈πₖ So vₜ ∈ πₖ' and by induction -| Cₖ(vₜ) = C_{k/a→π}(vₜ) -We also know that ∀vₜ∈(b→πₖ) → Cₜ(vₜ) = Cₖ(vₜ) +| Dₖ(vₜ) = D_{k/a→π}(vₜ) +We also know that ∀vₜ∈(b→πₖ) → Dₜ(vₜ) = Dₖ(vₜ) By putting together the last two steps, we have proven the trimming lemma. @@ -2056,21 +2056,21 @@ Covering lemma: \subsubsection{Equivalence checking} The equivalence checking algorithm takes as parameters an input space -/S/, a source decision tree /Cₛ/ and a target decision tree /Cₜ/: -| equiv(S, Cₛ, Cₜ) → Yes \vert{} No(vₛ, vₜ) +/S/, a source decision tree /Dₛ/ and a target decision tree /Dₜ/: +| equiv(S, Dₛ, Dₜ) → Yes \vert{} No(vₛ, vₜ) \\ -When the algorithm returns Yes and the input space is covered by /Cₛ/ +When the algorithm returns Yes and the input space is covered by /Dₛ/ we can say that the couple of decision trees are the same for every couple of source value /vₛ/ and target value /vₜ/ that are equivalent. \begin{comment} Define "covered" Is it correct to say the same? How to correctly distinguish in words ≃ and = ? \end{comment} -| equiv(S, Cₛ, Cₜ) = Yes and cover(Cₜ, S) → ∀ vₛ ≃ vₜ∈S ∧ Cₛ(vₛ) = Cₜ(vₜ) +| equiv(S, Dₛ, Dₜ) = Yes and cover(Dₜ, S) → ∀ vₛ ≃ vₜ∈S ∧ Dₛ(vₛ) = Dₜ(vₜ) In the case where the algorithm returns No we have at least a couple of counter example values vₛ and vₜ for which the two decision trees outputs a different result. -| equiv(S, Cₛ, Cₜ) = No(vₛ,vₜ) and cover(Cₜ, S) → ∀ vₛ ≃ vₜ∈S ∧ Cₛ(vₛ) ≠ Cₜ(vₜ) +| equiv(S, Dₛ, Cₜ) = No(vₛ,vₜ) and cover(Dₜ, S) → ∀ vₛ ≃ vₜ∈S ∧ Dₛ(vₛ) ≠ Dₜ(vₜ) We define the following | Forall(Yes) = Yes | Forall(Yes::l) = Forall(l) @@ -2092,9 +2092,9 @@ I start numbering from zero to leave the numbers as they were on the blackboard, I think the unreachable case should go at the end. \end{comment} 0. in case of unreachable: -| Cₛ(vₛ) = Absurd(Unreachable) ≠ Cₜ(vₜ) ∀vₛ,vₜ +| Dₛ(vₛ) = Absurd(Unreachable) ≠ Dₜ(vₜ) ∀vₛ,vₜ 1. In the case of an empty input space - | equiv(∅, Cₛ, Cₜ) := Yes + | equiv(∅, Dₛ, Dₜ) := Yes and that is trivial to prove because there is no pair of values (vₛ, vₜ) that could be tested against the decision trees. In the other subcases S is always non-empty. @@ -2102,48 +2102,46 @@ I think the unreachable case should go at the end. |equiv(S, Failure, Failure) := Yes Given that ∀v, Failure(v) = Failure, the statement holds. 3. When we have a Leaf or a Failure at the left side: - | equiv(S, Failure as Cₛ, Switch(a, (πᵢ → Cₜᵢ)^{i∈I})) := Forall(equiv( S∩a→π(kᵢ)), Cₛ, Cₜᵢ)^{i∈I}) - | equiv(S, Leaf bbₛ as Cₛ, Switch(a, (πᵢ → Cₜᵢ)^{i∈I})) := Forall(equiv( S∩a→π(kᵢ)), Cₛ, Cₜᵢ)^{i∈I}) + | equiv(S, Failure as Dₛ, Switch(a, (πᵢ → Dₜᵢ)^{i∈I})) := Forall(equiv( S∩a→π(kᵢ)), Dₛ, Dₜᵢ)^{i∈I}) + | equiv(S, Leaf bbₛ as Dₛ, Switch(a, (πᵢ → Dₜᵢ)^{i∈I})) := Forall(equiv( S∩a→π(kᵢ)), Dₛ, Dₜᵢ)^{i∈I}) Our algorithm either returns Yes for every sub-input space Sᵢ := S∩(a→π(kᵢ)) and subtree Cₜᵢ - | equiv(Sᵢ, Cₛ, Cₜᵢ) = Yes ∀i - or we have a counter example vₛ, vₜ for which - | vₛ≃vₜ∈Sₖ ∧ cₛ(vₛ) ≠ Cₜₖ(vₜ) - then because - | vₜ∈(a→πₖ) → Cₜ(vₜ) = Cₜₖ(vₜ) , - | vₛ≃vₜ∈S ∧ Cₛ(vₛ)≠Cₜ(vₜ) - we can say that + | equiv(Sᵢ, Dₛ, Dₜᵢ) = Yes ∀i + or we have a counter example v_S, v_T for which + | $\vrel {v_S} {v_T \in S_k} \wedge D_S(v_S) \ne D_{Tk}(v_T)$ + then because $v_T \in (a \to \pi_k) \to D_T(v_T) = D_{Tk}(v_T)$ and $\vrel v_S {v_T \in S} \wedge D_S(v_S) \ne D_T(v_T)$ we can say that | equiv(Sᵢ, Cₛ, Cₜᵢ) = No(vₛ, vₜ) for some minimal k∈I 4. When we have a Switch on the right we define π_{fallback} as the domain of values not covered but the union of the constructors kᵢ | $\pi_{fallback} = \neg\bigcup\limits_{i\in I}\pi(k_i)$ Our algorithm proceeds by trimming - | equiv(S, Switch(a, (kᵢ → Cₛᵢ)^{i∈I}, C_{sf}), Cₜ) := - | Forall(equiv( S∩(a→π(kᵢ)^{i∈I}), Cₛᵢ, C_{t/a→π(kᵢ)})^{i∈I} +++ equiv(S∩(a→πₙ), Cₛ, C_{a→π_{fallback}})) + | equiv(S, Switch(a, (kᵢ → Dₛᵢ)^{i∈I}, D_{sf}), Dₜ) := + | Forall(equiv( S∩(a→π(kᵢ)^{i∈I}), Dₛᵢ, D_{t/a→π(kᵢ)})^{i∈I} +++ equiv(S∩(a→πₙ), Dₛ, D_{a→π_{fallback}})) The statement still holds and we show this by first analyzing the /Yes/ case: - | Forall(equiv( S∩(a→π(kᵢ)^{i∈I}), Cₛᵢ, C_{t/a→π(kᵢ)})^{i∈I} = Yes + | Forall(equiv( S∩(a→π(kᵢ)^{i∈I}), Dₛᵢ, D_{t/a→π(kᵢ)})^{i∈I} = Yes The constructor k is either included in the set of constructors kᵢ: - | k \vert k∈(kᵢ)ⁱ ∧ Cₛ(vₛ) = Cₛᵢ(vₛ) + | k \vert k∈(kᵢ)ⁱ ∧ Dₛ(vₛ) = Dₛᵢ(vₛ) We also know that - | (1) Cₛᵢ(vₛ) = C_{t/a→πᵢ}(vₜ) - | (2) C_{T/a→πᵢ}(vₜ) = Cₜ(vₜ) + | (1) Dₛᵢ(vₛ) = D_{t/a→πᵢ}(vₜ) + | (2) D_{T/a→πᵢ}(vₜ) = Dₜ(vₜ) (1) is true by induction and (2) is a consequence of the trimming lemma. Putting everything together: - | Cₛ(vₛ) = Cₛᵢ(vₛ) = C_{T/a→πᵢ}(vₜ) = Cₜ(vₜ) + | Dₛ(vₛ) = Dₛᵢ(vₛ) = D_{T/a→πᵢ}(vₜ) = Dₜ(vₜ) When the k∉(kᵢ)ⁱ [TODO] The auxiliary Forall function returns /No(vₛ, vₜ)/ when, for a minimum k, - | equiv(Sₖ, Cₛₖ, C_{T/a→πₖ} = No(vₛ, vₜ) + | equiv(Sₖ, Dₛₖ, D_{T/a→πₖ} = No(vₛ, vₜ) Then we can say that - | Cₛₖ(vₛ) ≠ C_{t/a→πₖ}(vₜ) + | Dₛₖ(vₛ) ≠ D_{t/a→πₖ}(vₜ) that is enough for proving that - | Cₛₖ(vₛ) ≠ (C_{t/a→πₖ}(vₜ) = Cₜ(vₜ)) + | Dₛₖ(vₛ) ≠ (D_{t/a→πₖ}(vₜ) = Dₜ(vₜ)) * Examples In this section we discuss some examples given as input and output of -the prototype tool. +the prototype tool. Source and target files are taken from the +internship git repository\cite{internship}. ;; include_file example0.ml We can see from this first source file the usage of the /observe/ @@ -2154,6 +2152,23 @@ The prototype tool states that the compilation was successful and the two programs are equivalent. ;; include_file example0.trace +The following example shows how the prototype handles ADT. +;; include_file example3.ml +;; include_file example3.lambda +;; include_file example3.trace +This trivial pattern matching code shows how guards are handled. +;; include_file guards2.ml +;; include_file guards2.lambda +;; include_file guards2.trace +The following source code shows the usage of the OCaml refutation +clause. +;; include_file example9.ml +;; include_file example9.lambda +;; include_file example9.trace +In this example the tool correctly handles /Failure/ nodes on both decision trees. +;; include_file example9bis.ml +;; include_file example9bis.lambda +;; include_file example9bis.trace \begin{thebibliography}{9} \bibitem{cpp_pat} @@ -2240,4 +2255,8 @@ https://github.com/janestreet/ocaml-compiler-libs \bibitem{menhir} Régis-Gianas, François Pottier Yann. \textit{Menhir Reference Manual}. + +\bibitem{internship} +https://github.com/FraMecca/inria-internship + \end{thebibliography} diff --git a/tesi/traces/example0.trace b/tesi/traces/example0.trace index 1f0d6da..cd860ae 100644 --- a/tesi/traces/example0.trace +++ b/tesi/traces/example0.trace @@ -1,4 +1,4 @@ -Target program constraint tree +Target program decision tree Switch ({ var=AcAdd(-2 AcRoot=param/82); dom=Int [-inf; -1] [3; +inf] v Tag _; }) = Leaf=VConstant:5 Switch ({ var=AcAdd(-2 AcRoot=param/82); dom=Int [0; 2]; }) = @@ -12,7 +12,7 @@ Switch ({ var=AcAdd(-2 AcRoot=param/82); dom=Int [0; 2]; }) = Fallback=None -Source program constraint tree +Source program decision tree Switch AcRoot:{ Int 3 -> Leaf='Int 3 ' diff --git a/tesi/traces/example3.lambda b/tesi/traces/example3.lambda new file mode 100644 index 0000000..fee7a34 --- /dev/null +++ b/tesi/traces/example3.lambda @@ -0,0 +1,18 @@ +(setglobal Example3! + (let + (a/85 = + (function t/86 + (switch* t/86 + case int 0: (observe 3) + case tag 0: + (let (*match*/90 =a (field 0 t/86)) + (catch + (if (!= *match*/90 1) + (if (!= *match*/90 2) (exit 1) (apply (observe 1) 2)) + (apply (observe 1) 1)) + with (1) (apply (observe 1) 0a))) + case tag 1: + (let (*match*/91 =a (field 0 t/86)) + (if (!= *match*/91 0) (apply (observe 2) 1a) + (apply (observe 2) 0a)))))) + (makeblock 0 a/85))) diff --git a/tesi/traces/example3.ml b/tesi/traces/example3.ml new file mode 100644 index 0000000..63dbca1 --- /dev/null +++ b/tesi/traces/example3.ml @@ -0,0 +1,11 @@ +external observe : 'a -> 'b = "observe" + +type t = K1 of int | K2 of bool | K3 + +let a = fun t -> match t with + | K1 1 -> observe 1 1 + | K1 2 -> observe 1 2 + | K1 _ -> observe 1 () + | K2 true -> observe 2 true + | K2 false -> observe 2 false + | K3 -> observe 3 diff --git a/tesi/traces/example3.trace b/tesi/traces/example3.trace new file mode 100644 index 0000000..3a177bc --- /dev/null +++ b/tesi/traces/example3.trace @@ -0,0 +1,46 @@ +Target program decision tree +Switch ({ var=AcRoot=t/86; dom=Int 0; }) = + Leaf=VConstant:3 +Switch ({ var=AcRoot=t/86; dom=Tag 0; }) = + Switch ({ var=AcField(0 AcRoot=t/86); dom=Int [-inf; 0] [2; +inf] v Tag _; }) = + Switch ({ var=AcField(0 AcRoot=t/86); dom=Int [-inf; 1] [3; +inf] v Tag _; }) = + Leaf=VConstant:1, VConstant:0 + Switch ({ var=AcField(0 AcRoot=t/86); dom=Int 2; }) = + Leaf=VConstant:1, VConstant:2 + Fallback=None + Switch ({ var=AcField(0 AcRoot=t/86); dom=Int 1; }) = + Leaf=VConstant:1, VConstant:1 + Fallback=None +Switch ({ var=AcRoot=t/86; dom=Tag 1; }) = + Switch ({ var=AcField(0 AcRoot=t/86); dom=Int [-inf; -1] [1; +inf] v Tag _; }) = + Leaf=VConstant:2, VConstant:1 + Switch ({ var=AcField(0 AcRoot=t/86); dom=Int 0; }) = + Leaf=VConstant:2, VConstant:0 + Fallback=None +Fallback=None + +Source program decision tree +Switch AcRoot:{ + Variant K2 -> + Switch AcRoot.0:{ + Bool false -> + Leaf='Int 2 Bool false ' + + Bool true -> + Leaf='Int 2 Bool true ' + } Fallback: Unreachable + + Variant K1 -> + Switch AcRoot.0:{ + Int 2 -> + Leaf='Int 1 Int 2 ' + + Int 1 -> + Leaf='Int 1 Int 1 ' + } Fallback: Leaf='Int 1 Unit ' + + Variant K3 -> + Leaf='Int 3 ' +} Fallback: Unreachable + +The two programs are equivalent. \ No newline at end of file diff --git a/tesi/traces/example6.lambda b/tesi/traces/example6.lambda new file mode 100644 index 0000000..ce901f5 --- /dev/null +++ b/tesi/traces/example6.lambda @@ -0,0 +1,70 @@ +(setglobal Example6! + (let + (mm/81 = + (function x/89 + (catch + (if x/89 + (let (*match*/92 =a (field 0 x/89)) + (if *match*/92 + (let + (x/83 =a (field 0 *match*/92) + x/86 =a (field 0 x/83) + *match*/93 =a (field 0 x/86)) + (catch + (if (!= *match*/93 1) (exit 2) + (let (*match*/94 =a (field 1 x/86)) + (if (!= *match*/94 2) (exit 2) + (let (x/82 =a (field 1 x/83)) + (catch + (if (!= x/82 2) (exit 3) + (let (*match*/95 =a (field 1 *match*/92)) + (if *match*/95 (exit 1) + (let (*match*/96 =a (field 1 x/89)) + (catch + (if *match*/96 (exit 4) + (observe + [0: [0: [0: [0: 1 2] 2] 0a] 0a])) + with (4) + (observe [0: [0: [0: 1 2] 2] 0a])))))) + with (3) + (let (*match*/97 =a (field 1 *match*/92)) + (if *match*/97 (exit 1) + (let (*match*/98 =a (field 1 x/89)) + (observe + (makeblock 0 + (makeblock 0 (*,int) [0: 1 2] x/82) + 0a)))))))))) + with (2) + (let (*match*/100 =a (field 1 *match*/92)) + (if *match*/100 (exit 1) + (let + (z/88 =a (field 1 x/89) + y/87 =a (field 1 x/83) + *match*/99 =a (field 1 x/86)) + (catch + (if z/88 + (let (*match*/101 =a (field 0 z/88)) + (if *match*/101 + (let + (*match*/102 =a (field 1 *match*/101)) + (if *match*/102 (exit 5) + (let (*match*/103 =a (field 1 z/88)) + (if *match*/103 (exit 5) + (let + (x/84 =a x/83 + y/85 =a (field 0 *match*/101)) + (observe + (makeblock 0 + (makeblock 0 x/84 y/85) 0a))))))) + (exit 5))) + (observe (makeblock 0 x/83 0a))) + with (5) + (observe + (makeblock 0 + (makeblock 0 (makeblock 0 (*,int) x/86 y/87) + z/88) + 0a)))))))) + (exit 1))) + (exit 1)) + with (1) (observe x/89)))) + (makeblock 0 mm/81))) diff --git a/tesi/traces/example6.ml b/tesi/traces/example6.ml new file mode 100644 index 0000000..6044120 --- /dev/null +++ b/tesi/traces/example6.ml @@ -0,0 +1,11 @@ +[@@@warning "-20"] +external observe : 'a -> 'b = "observe" + +let mm = function + | [(1, 2), 2]::[] -> observe ([(1, 2), 2]::[]) + | [(1, 2), 2]::_ -> observe [(1, 2), 2] + | [(1, 2), x]::_ -> observe [(1, 2), x] + | [x]::[] -> observe [x] + | [x]::[y]::[] -> observe [x, y] + | [x, y]::z -> observe [(x, y), z] + | x -> observe x diff --git a/tesi/traces/example9.lambda b/tesi/traces/example9.lambda new file mode 100644 index 0000000..96c593c --- /dev/null +++ b/tesi/traces/example9.lambda @@ -0,0 +1,5 @@ +(setglobal Example9! + (let + (test/81 = + (function param/82 (if (!= param/82 0) (observe 0) (observe 1)))) + (makeblock 0 test/81))) diff --git a/tesi/traces/example9.ml b/tesi/traces/example9.ml new file mode 100644 index 0000000..7b163ea --- /dev/null +++ b/tesi/traces/example9.ml @@ -0,0 +1,9 @@ +[@@@warning "-20"] +external observe : 'a -> 'b = "observe" + +let test = function + | true -> observe 0 + | false -> observe 1 + | _ -> . + (* Unreachable; if this annotation was incorrect, + the OCaml compiler would error at pattern-checking-time *) diff --git a/tesi/traces/example9.trace b/tesi/traces/example9.trace new file mode 100644 index 0000000..78619ed --- /dev/null +++ b/tesi/traces/example9.trace @@ -0,0 +1,18 @@ +Target program decision tree +Switch ({ var=AcRoot=param/82; dom=Int [-inf; -1] [1; +inf] v Tag _; }) = + Leaf=VConstant:0 +Switch ({ var=AcRoot=param/82; dom=Int 0; }) = + Leaf=VConstant:1 +Fallback=None + + +Source program decision tree +Switch AcRoot:{ + Bool false -> + Leaf='Int 1 ' + + Bool true -> + Leaf='Int 0 ' +} Fallback: Unreachable + +The two programs are equivalent. \ No newline at end of file diff --git a/tesi/traces/example9bis.lambda b/tesi/traces/example9bis.lambda new file mode 100644 index 0000000..5203342 --- /dev/null +++ b/tesi/traces/example9bis.lambda @@ -0,0 +1,9 @@ +(setglobal Example9bis! + (let + (test/81 = + (function param/82 + (catch (if (!= param/82 0) (observe 0) (exit 1)) with (1) + (raise + (makeblock 0 (global Match_failure/18!) + [0: "example9bis.ml" 4 11]))))) + (makeblock 0 test/81))) diff --git a/tesi/traces/example9bis.ml b/tesi/traces/example9bis.ml new file mode 100644 index 0000000..adf0901 --- /dev/null +++ b/tesi/traces/example9bis.ml @@ -0,0 +1,6 @@ +[@@@warning "-20"] +external observe : 'a -> 'b = "observe" + +let test = function + | true -> observe 0 + (* we expect a Match_failure node for 'false' in the lambda representation *) diff --git a/tesi/traces/example9bis.trace b/tesi/traces/example9bis.trace new file mode 100644 index 0000000..7afb94d --- /dev/null +++ b/tesi/traces/example9bis.trace @@ -0,0 +1,15 @@ +Target program decision tree +Switch ({ var=AcRoot=param/82; dom=Int [-inf; -1] [1; +inf] v Tag _; }) = + Leaf=VConstant:0 +Switch ({ var=AcRoot=param/82; dom=Int 0; }) = + Failure + Fallback=None + + +Source program decision tree +Switch AcRoot:{ + Bool true -> + Leaf='Int 0 ' +} Fallback: Failure + +The two programs are equivalent. diff --git a/tesi/traces/guards2.lambda b/tesi/traces/guards2.lambda new file mode 100644 index 0000000..2436972 --- /dev/null +++ b/tesi/traces/guards2.lambda @@ -0,0 +1,7 @@ +(setglobal Guards2! + (let + (ff/82 = + (function x/83 + (if (guard 0a) (observe 1) + (if (guard 1) (observe 2) (observe 3))))) + (makeblock 0 ff/82))) diff --git a/tesi/traces/guards2.ml b/tesi/traces/guards2.ml new file mode 100644 index 0000000..452e39e --- /dev/null +++ b/tesi/traces/guards2.ml @@ -0,0 +1,8 @@ +[@@@warning "-20"] +external observe : 'a -> 'b = "observe" +external guard : 'a -> 'b = "guard" + +let ff = function + | x when guard () -> observe 1 + | _ when guard 1 -> observe 2 + | _ -> observe 3 diff --git a/tesi/traces/guards2.trace b/tesi/traces/guards2.trace new file mode 100644 index 0000000..6b774fa --- /dev/null +++ b/tesi/traces/guards2.trace @@ -0,0 +1,24 @@ +Target program decision tree +Guard (VConstant:0): +guard(true) = + Leaf=VConstant:1 +guard(false) = + Guard (VConstant:1): + guard(true) = + Leaf=VConstant:2 + guard(false) = + Leaf=VConstant:3 + +Source program decision tree +Switch AcRoot:{ +} Fallback: Guard (Unit ) = + guard(true) = + Leaf='Int 1 ' + guard(false) = + Guard (Int 1 ) = + guard(true) = + Leaf='Int 2 ' + guard(false) = + Leaf='Int 3 ' + +The two programs are equivalent.