From 972748e0afd33687c91facc552999c2470575540 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?=E6=9D=BE=E6=B5=A6=20=E7=9F=A5=E4=B9=9F=20Matsuura=20Tomoy?= =?UTF-8?q?a?= Date: Thu, 11 Jul 2024 03:36:56 +0000 Subject: [PATCH] wriwriwriting --- src/lambdammm_vm_structure.pdf | Bin 0 -> 20037 bytes src/lambdammm_vm_structure.svg | 1731 ++++++++++++++++++++++++++++++++ src/main.tex | 45 +- src/syntax.tex | 1 + src/typing.tex | 9 +- 5 files changed, 1777 insertions(+), 9 deletions(-) create mode 100644 src/lambdammm_vm_structure.pdf create mode 100644 src/lambdammm_vm_structure.svg diff --git a/src/lambdammm_vm_structure.pdf b/src/lambdammm_vm_structure.pdf new file mode 100644 index 0000000000000000000000000000000000000000..3002f00f36ed2003d9a0eac0d69f65554608baa9 GIT binary patch literal 20037 zcmd741yo(hwl*5vo#3)@cXxMp5AGV=3GPm?puycOxC96UcX#(-!5<`@?({i*&$;9O z$9V4rSgUH5>{YY&n)9n~R)s`fSd@l=mIa!m?x_3@ni)V3ur;uN=H>>_NgLakI+_7k zo<)k#004ka)ZEI^*#7x$rSE7gY;0(2WDL#A3+>=&Z>(<(?V2{Etrd+k^Va)BcPv^8 zWP$fuN)NOWgUlC6qE_TC5Y6w*PQ1K&FwZ3kc~dv@q-0`gVrH(1+E2Zby0 zrv}He(~-K~_EOf!K}jwx+mm7+1spHp&lYRqOt5ZhGByGh~XqXQ%Kt>69OK zo(feq>STsz+FxCX-9HuVFGasAzV+JLw>|Kg)WoBC>Xm|ZUUlkarm(oz|F9}#9cK|S zE&M3-P=Lm>`+eK`{fCGr5#7RLHBmNBi}zk-4)Jl4tW(b)yyD%cI^(&tfH2iu(%v?{ zx4*r%cd%Xm=v?#Qc;!7lWxTfz_nngNRyzEC7 zHU<5LigfdYYE0!3Gp}=ggA+bptKj)2(E(ChFPGh+?)5OKsbIWi;14CPfC_^o8KSB-ug*3k`-O8Rd{ zkalp%$qnHkW%(f&nA)$^WG24K-QH-G>li989#{rR4D9F-f*gCw>sgUay!@}N$}8^hAE3CxU@ghByMUIbR9(RV%t)H%u7iVdeB@C* zd418+)ne}?ryrcj7LM>9R&U5pIvJsEm5)2jz8LNy5%>2T7j0ar%N6c4eZ{!lX6t(+ z9D*WQ-w*=tQ{Ie!q^AWCgqdR6(Z&B*HB4!XNe6a6GW_6Om1BF1Z<}Fr%*SUb&Nbc= z57-0~hbf1eAQYV64mdYaDo@q5{<_?5u6g#K|E=@qNaA@((pm|VB=;Q z%^j}$7Wm^Nd^IfP2e-p3!Y<}MrY*Z6Cr>DI3xv0~t5f&K_xJ-2y|)A_;4n08Lw@!` zD<)QF)-ln+g>XwuIKYD9oM@!cvME^RLBYNsTv;D!T7l%I5tAq~hJYY4wwrh7Dvg{i zrO&LQI6xvx^G(mSg-G9*?#=OQ+E+u{k=BEfYR$>cnD`4H2+Pg{J=pt?gv#3!9tf%D) zOBK%uxx*m}IAjYd2#7nw0-WmIY_@q-z_AR_hXJCaK_=x|5k;h~T@nOcl~)UBu|)ku z_|k@cOgd}H1(LE>!)9mhVvE_rLv|GC97I{r?B_Z5u(=;*;RIS1=sw}|O_zp#wdL&s zE+#rs%Q7>cVWb5LhYyLf5h;=D-eEShqf$UY>PkV+TNg<49~GR53}&#;7cx_ye#hU! zi$Fv~@CHBABjOY2qaA;Pb=LBSu(teKM1(s7Y{Z;R>P>?9tukiHei9=X;EU<~Ej;PV0p(#jx1wLmFE%Z;S&MT>*d`G0eh3 z37t;tme8>BdoX5Uo#`QaDP&$P`bpPXh0wx=SRqNz#+bSFYGTv+&s$;8TB30r;Eg`0 zPdIO~P{)mu@xROJ5WDA^^GbmNkXsdHKRWWyScCe6y$@6El0Ir7w`VNaEEr?bt@$EF zB2chvBG6R`Xp#q0uPD{%pYUtOh!KvavK9jsc6y(7wPWw?gW?7=trKarZcHpjLsC#Jpq@lSFY*;`7 zI{XZVL+;|bt*WJ@@tApy_RDMbkDk8ogbxGRNMd;^M7K{LH(5ZS69=V7&ttqhy~-5* zlf^#QDoXjHj8X+>=e_D26)#c*&p#VeWMB`(?h#M$K?}}i^1E^ypZa#5##mJk>afRT z$c1!U4Za7~WC?NC)Mb%Sj6(Pty|%J&GmG2NIemh8otfaayAHaNqcok}-Il8Y-}`A> zqlx2vkCLuhmmF+H1y5G*fnmi{s; zM%rGG$rj#yKLy*`u&<17gx{{Nzjr}(wumk$gl#u58_}tF#5q7Uh-sicUfKO?x z;J~RTeABMbZ8vxXH0SVLU%~E3ASm30X?h0A#g3vq_-&2s2-Gc8u2`nP2>;JkF~$t7 zUO<;;@bV=)JWEQoJB;?=12vLEP@fzK7(k{p^0q;TFy$Sx*Gm=8Z}kAf<8rl_!Qn<| z76tExWz~FczMXGh9h5&-eCR6(WC)EgQljfyezV_1?SCq3L{nyJLSaGC{pgdZT#7k4)ICe+QKc)Rt6CUYNU-FasE;p>!Sp@$*25cW?pY(HEO zuQz@S9VEt!X%(=@P{I@)Y~7tBA3BZ^%7Am_7$7&tqolfE?F%%oJ!wDWo$<#EH|%ZZ z{-$bPSiRISpJ~EAVbn_Q_u86~mw8!$1r8gMF_r$nvCO!u4{In566Tj>o*hdYXn)v-WiTmz%MS88emgE(%+c-KO58(Z4;HkSC3iQjExrYf; z#th_D=iFSXSyH2k8``}YolO;ck=}{|@(<%GJua7yH@5e-cXS>e-j=oZEh%|DWk-}h z46e5MVUQ6aR^m7A${rsC_RCqIYVJv!!-KC?zZLE_E=m$3>872o;ZKJfF!zB^L;qZy8C zv}L?yDnIkcjvWcT>$->CjbA))JflJJkO3-EkIN=&*S;D!xFp0*X#{7Nd|4DC9?z{{ z0uYw(cVa(uPM-?0gfbh!fRVMb4K}EmkUU_}RHr?83W|E3=0S_SRXCTMaNH2XI}*uS zb4HoKoTME+6__R(M5OFB1&K5Gq#voaUjYjgFZWf zt5tGVqFdnucYFaBUjZZtZ}zGOeRhmVF8%8N6&8a!o|`yw-T-bcyEY`sZjL4=9#8{o zfOBRtENZ`(lZ+u-?aM(n1Xo3Q$Y8)l6H0w!8domLAi<57Pug#1M4Z6*^g*=WwX9kCA`eeBnE~uAm7;l%#o|=pu zb#IgvRAgc{_?p^lH7=c$rVKiY%Z5vQ${)I;-+S@OujBQ7)ruaZ9gpZB#WBXGrOM+Y z_XWaHry!AWkNw6EpBO&Ai82|Gw@ik=k<8l0@HYR7CK4~9Ff5_?HCr01`bPF)hl<^? zo4~{f)xlawx>J>z7eWq?aTl(q^_Yl09D5TL|Gd8 zHRF6kKiCq0ZyYpOl0YvQDJMpcB2=3?FhBq7n}}k#l9q_Llzs*P%{~!iQrQ4%jYY>KcwGLh;QNqK3c?WJ~*5~R5di8U<)C=^Yf zCn{XpH)np3YYUgwEMM8q(Egrw6m)+xn8yX^0DrcqHMqcchhYqb8wGE;nRO}07vL2y zvw$IK!bU$<9!Y7p=W%zwD=d|Yf_+ku0jkau0dB4UGf!a8$pYvI@fwL6c4?Hni=p>F zyor9xduG$V>s^|cDZZnARL%TUDYu1e>duw7d5%a~K9#=CIi_t+6SjS&6nc;=ke*4@ zf_}rE=Bj$ddSRb^nu0VNyJ@u_pi6vUO?E#ki5yc5@tU9Po|%74!sL5^Vz!P;b<`B< zD0JqHJd!uoSdnr$S%l*_{uwLAkq4^-bsoL9otc))E^!iJKmtbqMU}RKNFZ578A-L< z)kAF<-TpK(7;x?Pg1B~HeQzd$G37I>>ZmFf;aSbs@}~x-MjfS>0@d|LT+$Xa zv9Q8D_WB`$8T?(AwX}&L62-3~j=qVn@EYhG&}yL~*GFRRNslErg;IP|fJ@JoO;O8! zVkn-#oab^+M`i+4t!f!l_e<&|<6%l+k-niM3l6rTgt-BG*6kxwXBG@N#??3I72CJK zV-yI}X#+A-r~oZaViHOeN*x;odS-M#kKPlzHcSxi`Oc%6#nuDKV1K~$cQ0ZIpDF{n98U&$uK^*1_O0~k z;&>k+dSNJO>25+Q-|=30(n>3eyTK%Eb?gIj10_N#x>-xES?Y}jT8+*Y7o%>ah2&r- zg0mUfFx`iGv5qfO$#vJ~oR5Q3GH!UiS~t_5co2#{WKghz3{|Vv#5fe%+(smaSvX85 z>Gnx#kfkY2f05=H2tEiBNYeUlbGg|CFOAP7oQgk5Gh>!<9>{23{(chbIM*hXhd?#g z*C9bd|0bgojjWS?nH@?O-7`CaZy?w!`!Y~8e?bQOg!87_-?A;(I~>TdsJu3c#u$97 z11T@rBCOengS<|Fi>$~Y6McSNcaGE&#D|{Ra>!1JGG7%2kjqN5DS#9VMWT~unq+7u zRVu{FDaUSdbYD#gBg&X(MZoshhj4t_P^l{22WqnE(blga=0*t|N`aWq`i@@ki=t{e zFjt7R0?9;n^&Ps6n4CbUdO2p+x=&8$JXn9dkjX$Vc_u0JQNEBd*i?WBMF}mvx3EUt z)LX5tBV!W$HyxjB{ZHEwvu9ULg3uA;zDAn z`f$+vG2Rvkt)y@#7(Gg?+pa2{Ho3%Dt2nhl3_Y&)-0}e9ZkJFh1o0W5QHKV^Avm=mxs$`Ly0Y0 z`y+1Og}G9FYlTmf+pY47;ek-=5(G-Lj|WLJI-jN1nE?d!r&Ym^&KA@GL$=&4u!QRE zv{q!9#70GT6Mnnj%oki|GK-(UEaKRUp^a^f{vey4Q!g~t3pe$0e`cqc+2~ncD!gQw z{$#O!@Kz$Oj$%rV&zu#2oBKuZ{Etqb{y77n6A}P00O$<$pRdnM)^ownE1jsVjpJ{% zO=#$8=mD(1n6Q@)OlTOMMQr~nVgRuJT|`gA0O0r~dhY%C_m8J!pnn$sBHNVR?2G|) zat0Pkj@CaO`VaPvf#FwMI#~e2j}lRHdk04V^B?K|Ov&*KF~D@uqk^uswy&eju$m(a zL*i;?vqLH_^<+;5JDN+zg*{x8#&RzAHM@|g=d*+@aH51sJrN#uFaf}&;vpb}l2)Zh zsw##cuK8iZinPf;Z{qnSHF49^g5mAeGQ=YoL)_RlOj9$}MiFeU7>q}j3t00tanK?h z^pd$Yk0z$tIpton%g;3bp9CZAM?q;!v3eC{+iD} zSxJT$rt*KLC0}Ofrv@1S3=GWl?0+LFw=~`CuxH$SY~LaS1m5+CtoH(|1A_wj0ceq1 zh%-Kl#KxJ$){;vSk|=~K7bUK%bKuCV3n`NA5X)K>gceAoHC8F*ACaRfv1JfDTalP^ zq|_HFu_k?Bmfzg>kPlw7zaJ_TBKDzc^Iq~Y#LXw1Jh&dM) zxj!dENPnDx$;==Sz9%N=`g)IR`Y_zOc^(kp<6n{{CWp_}^tfLWjfBjA^3jIVd3|w= zY_j5F1LxL{juwxj_H?1OqyZ6mFo&)=1b*p!9%1!6bCggx*~qfn;rn8E93Rxa74Ekd zkBABnXN&|xO6=a-o7r4)Fc2&Xg6rNmcXBJptkIYdXZ(HIaiDk$iqE2CJr(%f) zd*)lDFC<`JjeST8b$%V!;s>Kbmp$VdSm;(_5lM~0Nna;DDS>{#>?lWti#451U@@KD z3zy7pGnzaH=#naPab4_ONw`Q{#95o#oD;wyGV!25T|kE4yBL|%@MZoc2=&- zhVdsIc?6|o-bVRQ|cknsKx`p zi7={z${Ly)|MX!ZFo5+9 z8mwPnZJf0u-^Qt$1fFv-fo!dT8OJEF`>04azr>YB2wKuC0g^ZxBV^NSdsKS}VZMa| zg6pg^h7kH@>2H8a{Ka-bPfsv*yT#(#L<#7PeEL?5`G@y)NG4JQ(iiXR2rA(P-e9)~ zjc{I+8iM7ch$rWu_0HN*qZQgAMMBJWQYTF3tOYO&e2dZVM>RsSCllryJk}v?V+p!{ z9j9lgUWttS4j@1*4$lZW2f+dE#uYGf`G)z})a7fr-kWMtDq@wfA{b_9%anBK1Qf{o zVW$$tBPa|6>J!zxg%-adgSvtR`#1^1jrv10M!!y4FygnYR9D2>%gS>6hvrTTzzUYm z>MRriVO$&Q{Je!VSeA4t3oy7)(Vt&e_lCuCW|QKC2M%?np^k(*X{MLwckaPYo96^h zTaR)2)2%4p*3FdNsMaZ{8N=OKXK=O(MNEH5Yu$#xu^K`)9-^csmS_{D0g1Q6)zI!e z!R%9k$4TyQ8@et<%&D%8G@Hp+WkJXgqC$=`aM^%QEN5aRX6OG_4LWG-% znz~83x^jIN~z*I!>%)rv=tQx^}{zz`Chl#8TnB$pK*?5jXd_W z4Lla7x!rSfHb(V~&h*}X;G4jY6aCg%x~_YA32bL;^q8m6*@^_6l5msy^$;WN&3hjz zyuj=?SCp4wvHNcgyU}`#d8|u6_gf%4e#~>J@p+r8DG2VH@-D~-U+I?V6FP6NbtPEZ zq~h2Za0__7yTXZSS zX`dMj1#^Iq15p7)G3Nbm`#HLB3c=x(h42C^TQ)Vshf2ANV?WD-L@z0aE>XRbiz*PV zM}{?;lBA{)U#LmB3iD2G2<~-Mh@>h3qcFSq+OFHEETrPx5S7$Hd626q zU=-7q{Au{R2ZE#1$kpvbYt51lg!_ZCcvLM5YkeefJW)|^@1%IOohvaGE{8Vx*XSMt zqH{@UxpCxEOG1%vJ<#iMRtY^a)luB1Uma$sVmwI>D$DF0QTW+_{(ez_a{pr#yQJ^R zao|8)o&BP*-%Z_Hev5COc^3ym#H6AvFBPnvTIXaY78=-)!%uA`aQr^&1FqR8zl?sh zSmm>P#>!e|S=?r&h3lR4j3_Ox`TQe4l5wOO5@Pgp)YMO+LMNPeCF;Cp)d5@|W!%QB zpqzU59Jo?HOf@iZ^G%O<=xY4sNiRA3}kDU=aeBe zkgKNii?lY?r&`WFp6+zD14_7>1Y5#Rt_RL$VanaIE6}yi{VddNb9Lk5)=O0a0RI~PZWFgHslDG_2W?Uo~-`L771$yBw59grw_0m$K9=FqZOAXI(zOANeXCEv6N)ypEWM~8S&6|}i zlabAYphVEr8Md9`4wLFWqVCYNRDNlof|_3xFcGs6;}8=b0|AH@Ea%S%q^Db~CykzO z>fOPcXTDw>+AgQ5NQ-bCIx`zg>Gv6i9Lol2nmiQO-e2HpYL@%faDDT^h9ZRNOK1a{ z()osY-pbVY+7g49&jLq^t(Ex6K>qDVxJ#!DVReghWi3N58ZQT(H)8G|V=$!~OA~v| z_@zIUKp3U<_by%JMGmSnidJ`dC=ZoUAix>zN^#B4CqK=*zShNGzbQb{);G52P&0Db zO@OQcP6|{^F{PwUEms?Jq+J!CFdc!ieKOcf3hp&GICS0PD-?D~d<^q8;kkP_IX6;? zq9d(6kVx}%N~tB*SZq*R_l6-32}Jf(+K9l-!BW-ePgt&p^hfR~ZYNEdRYqo(yi&k-saM;ioZBd4|nIgRi3Y6uJ zV?o~nhtAjG*#Jc&c6?Z)V8ZN9?a@r!@4j|*7nZ>lZ&tYN*^{_hi15tuHfO7}Hv}?v z*kW9|4^Fjn>XDU_(X0KFI8(MbE49^3I2IB|eP5Cgi3c6_xa#E~gHC!)@YFNEgqvoP z2`WR>Z%Q_?>a4ENjE^l8jAQ2_KsVN`nF7JpsN=0!D%!apmRn_fZkpZ_py6?jH(S?p zDOVsZS7lg#xQkEeYXh8*1yp3_@cIaOkdBe%uh4nA9!pG4pj^;R>&9D>2taU05D!`4 zew^f_UTL#wv1EzVcL+-VGF70$p%CnDaX&~l-R5xzL!I=v9X0MV5!-%4@xWca zo5{4vXXhr(I2hZnzI~1yL~+Q)_S!Dm4hH*-b0gKaE~OgtQ$%iYI^MQbQ>K?vm-S|& zw9>_Xfw*U@{IXWq=~&hdK^xP(37hxQ2Ulh~*124mHZbZ6$TJ>?(?Ocn?^#A;4xwf= zds-$FuQjYX-%XfKW8tVfrJd~P>w+kzu;)b_i3T1~rHxcicsb0rbye7|s)i1zh8lb| zbNfo(8}UsJh!Hp?2q!qrUps*Nl^d!(*f;6`jXax36=hMyzP`LLmy&K zr4y1>vI&p_)9JX@fmN7pQ|2NT&t$0VfTPkC2zC*rDgKj|F6}l>Dmjl_0TT+x^=iE% zElH}@JX6#N@6He#8~o*HG+%{7FHs<{Ooi#^E_m|=?|8i>rT*heOjxW>-X~O|YJ${P z4!5csRFs|wESu$JH;Jl6qZX*gDpyzPUVXIH+G^8P;mRfUS~;5ndlAX{P%%rf`sUHo zLLv+In_YsVrdG_Vcf}B5S7YzT0Xmqt@SH09xE4;jBf|>$GrXQOkaBAp>)XX8)oNY# zTCH&l-*CA$@#<>>X)pE&n;u82PnDILXJ&O3soLIu=HUbG%p72u84|mazC`F}38?tI|PI<_LXzwoM%K_ZKh=;pK^hE3D#kJw}Fx zte6bbBnvf>k!5jORFk;J3k~wO1GaZHiUWo*UUl9?pRW~cJ%hylUSrx=gwV+9_LzCwno~rn(Oufp+a#Lc#^gHy&@o&NX_$(yqQ9DoVEshvX z9j_EdzQ0!Nna3+$Ur?G?S(z5aWhj1vipM#*M`=J}M!vjEj-cdt-DuB%1pRLNd{9jK70;vR4ce?xKgTXW>~_*&LvsOE((XE7-s zsYX63i`|tZ-s1Q63&6g|s?q9c;+qAWOBcoM1w(4+((YY1)42=F_12$EnPZ})RJA_R zr&%?V9EDk}jGXFO^7mjB#wEckB+8Ox*bKd@gXXFmC`Ux?F|~?PEt zwqDsq)kH){@4vwd-jS-N7|h{%U$>>a{I=4O$+zBI=9p^ZvvU!akrZ zXCY9s`ve|rRP)q3RXE9#lYEsB%WQeA4n+}`asyT^M{|=&6WhCTZST@0OVz=nMcV27 znn)g=&u9(Jd9xD}v&`)k>Wgf25*~fQ)x5gSW}bAG2&NB@ho|4)L>)M<&I5ZtJ#7+b zInFdTq{Q2oyYnE>Ts-v(QGfL?yp~sc%02>H-k`ZgeO!C=D zwdLXCaC@BI{zk_W$J54^zU;xR^@!VKTUBCt)`oQN>_WHPXSfZ&>H_3hLqCC)usBs| zOePuXsPnTZZb^4n}^i6mxiUn(%iEIj5 z7A#V!`5KWjF2j%)*5OQod%!-|lXZ`9_q+sFNnT_XGxP{ocs$piPR7{Uo!ZvCJ`MSW z9Um0Pj@`+nQ}Pr{I>Bxn+qY`uEy{luE7R*WFj65A-G5KEJJ?8-$#841hsvYm&iC-D zp_7VQ{+p@#X+);LlV;patL^^gd~)O)o0Rg3B)6fjiiFwM4oaqhC^g|-3-H|4J__tn zx0rhf@s~5ZLU}|3EyvsESo7LqOp+Fqbkh-G!A2F^mnFGY71dE+H7NsEC3!oRU$0|h zcBVTxRM+jw?}gdDe|Umoo!Jy6EA#a!BB`;`6#a~`m{Zs(&cYprg(m_R{V_;Pp*yE= zO=0qs+`<+0Pcf~>OFH#PVqm_CEnhr77XSR($I5n_%S%Y-^IBV#&Xrl8lBu`*4404R zT^0Jttnzv08)jbO-Xxj5+*!V^)b|L3mCo^=@BCipn8k)^ijdb3<<0qSgRzl~61dfA?3B2I$da}w9g&^i zA|`ly@ced#Y)6No$KvSKO(AOWvV0G5yh=|SUgc>vdHS;%mMn&H2k0YtEnz+hJZj9f zD=_-!8|V0Ata%h`d<7QS$XVV0KAA-E&~d@I)M(n2=~_;I!s?O*cEEdljev8a`w`+T zpl1vTCMz%O4kAf;t#e6fz4j^YX}rIS_5QrQT%XXx6wauVRwduO zWplMWHzW5?ARC2q>=wMkdFBzPXvP5zr%3c2oV4RTVh>Wq{of~hCdY5QXB2IpYN-%U z5vX}Mcvt%beXEZ^(+6;yO9_}CT6raesO|g zTH`U$OF_;9VKSa6>;f6AbxF(Ie+@!AO#t5W>LU5LZ&u}Oj7JG%l(>VLVeu8k-U?{Z zTc+G8`H_BtGPigDODmGN9(u0oJ(%Q*Vzjy6V+%~X)rpA!2`0!DNp$lWFguC4si z?o7n*#=ej2ScKClh3}((t)x~%t*gjH$zP>sCdO24dFPT%Hx7E=Nx`ghv=@_Q4*H&U& zy*@rdgcuGGQGL77p}0rsRbL7hzn99S$6>{b|akeV2EvOD!dAD|Ir z66ZdyAZp5G5esGFn&)jW6AXI?h$?r&MH8@BAg%XeWPs%&Ws1bG2-&40jGW~Ft}+Ap zD>`TpBXH9Uo(ht*$O21C!l=JJRd+nLP;aTSRV@Y_K`UOpkq2Cv+_E@2#p3|C;dCtx zZCbL|7+RtaR!;VO9=A!^IE|rpFfs3X0){n?&i;pp!mka@&jA5ehQA_248I~rzio78 z_%puqUw1m|#CO^((8C6uxI^PM3+eZLEQO^9hCLz)wic=3c}Fvr;@iuLx)alo+23yF zi-+u;e=|WWq9WI~v%zg$@BT%K`^==zTsEa*kVdQ?B(q@d5bHyJV=LdDPs>F~QP_9K zb{kKQ;SGaN!>ScqTTX*6cc(-&AU;gf^ZPEcX$3b{_>a8ltDH;ImyvYbw)L#R{xaN& zj(m5QYCif}Mc>bo2ky+9`OxM}dou3^>c@6)CBvlF59Y;&A3RMarY<|3H(cqt3+PVF z5Wdj&`gpOX+e(?~pc{U=YPM&{hl#Xj2!xXE!aF4K4*s5Q2in&qQ>GoUM^1sRWPoFk zc8b@6ZbA=3?lP0}-jhlv;OX%V`oHMd@X~d+7?8X+L^X-!rt#qDDBG81g>eUOFNU;;eFdLG)fY-vxc(M27XSsgN;_bq8AsVLvxA$%BHZT^QZ$;-t55q4r`{xgcm z@DkkndwlLCEGTU3U}$e{=V)vHGXnQ4lGV3<4&G^shzn`TQi&T|IU75g8|up%I~o63 zMO5F~+{z6={%0xRrI_Mpxs|@D1AvL~&&q;=wyppz01XGr^JWZY_U8~52Rj>pfu4;G zp!1`WgrmNdxuJlKsg*H+{)a@s!O-|QWXZwuvzM2Le96-=GBEup7t*&AH#RplbNtcG z50R3iv9&6I{b&1^jQFq2%P^le`x`R?7+ykeioXRdf2r!_z4;lle5w4iKPLmnA5lzY zdnefQ zSee-Ytn4fRHbzDO8$I*0bzuOou)Ua@7s<~yFFmodG5oB<`W!%hZu5M7ZuK+uQuC$V z-#>{Sz(W5bVPRqeuy8Q_?as*Y{Cv-!^3pTokI!LYcpk@dik;=T=F8K+ls>nj2QV=` zOP+gTdNy`HN}khfEH6*+B4uW$|M_Klo=0018}pab9DpBY@%QOwc&YyD9rzWJ{xh8Y zk9P9+&?_T7EB)UhuVpGyR@f@2t+u@NO4x@I27N}z+$b}u$XuWnie`bD5LQ%0MX2J% z!vIN?DVwxHB&1^b82)cTU_=44@)RL(RIJqb*vt&#k&}|6VUlPts;`SdVW!Ec`6IjC z3RnS!&J$l?}T_A+y zj%`ulYcH!m9MDd;0kbNV(5gIYn6=4n@eBQ;b4QLi_ew;v~;3hw?0J8H6H z2%>L@P#dX%J&gZ4{AfR#gw2#gG>(BtH-Wk0)@rPh2}BGBAif6(icOEGQ6S0=S%2pS zJ-K|>E3CY7Xj&(6ur4u>&ZQlZ)kO}H4>5#_(HNQ3vM4v*!#i2dBRlS3-LPofbhXS@kf9#AjE9*&x1hX zAkH^C`@V&bXz+EM0S9M67PMg{kGRPi_W%y7Tn@i9PvI4)`tkv00vb%d2Pr2c35f|3 zL_x?30E~{6uv;Br_vX+s;iM5NCmy=IXmK*U&!Nu%WNb&>zK88A-a$^X0sb>R-X4qZ^{X++1zTEI6psWf;D)G z@1)hn_v+gb2N7N-oK`1>1^nGwu6RA+C(<2JrTMSbpjowqiHv|E4hnlpRjWTM@5vCE zTO^tcsZy8aP9;*-C)hKg6(@2O%`w}Su6lKj9<>xX4;GtefJXPY5hwLAc2>^ot2<%x zSB4XCXiZx&@R+vf&tCdj?7-v~A83v(XD}Te`4xX4&G*#F>&Gwa;YxiNJ;WA6GOPLO z4}zL+?8He>wy=hJL@DnS2OeQ+qTC`%Z>hM+1lMI=6J=( zjM^A=`RU07!sk2k9Q;;*Idqje`dwOPna!zrY`Je$5RS|-UOA1`#;8A=Gt_a>1l z*k+(z)K+24`<*L&J8~hmO8aevLLkCWblbW%ttU+pt))Z(H-L>JYi)VZY!$p4w!q z0hsxY_-}ZV-=$RX_041;X^ssceIX6DWJUYZgQ?=Owx4~j-P*PLc)8%8+Va3ae4PJ@ zEJ(Pn^gDgmvW}Ca*Egb%OCjv(_u)OozJfh{Gg}E%BnRl12@Wa$uFD_#`9qhCj2wTe z^2G=JQsrNc`Y$K?!#}<_=AYn2LPJhe{r?=i{IMJ9xx4=#VV4)*^}91;{CywMUpo1r z38i1)MMy&UMJq4GKe5MO0Oo(x(Q_LmH-~2gC1GP?`_kPDI#M(?HGkf%_Kf)io;Ria zgnBQ&QO@4T*!~5vkV_anLo{xZhN-7xM zBTWxkN3-q=fPi==EPP2;v#WQzI1WJ4Myg0#-u=Od>?@x_b~p zu$YBWkWr8&Kgwgl-D}3+n=q^*R3koQlXqg|kn_#%JJ=3_f&}0P^*o<#ZNcAZ+2I-C z(d`N87iS`lVP;Ip_~gFP%_H0;L-=^u@B0vUj`|>*yYNnv%30ECH<60Xyucnp^8pg-nZHvTM16r`&?!w&{ zPF496WKclR)eK$k2ZaGlh7HrDswuePa1>4f}bCpUa`C<^Wf99d*$pZV=W@>~Xt^6A~m4MRUkGDHjbmZOhW=1lohF3Z>IB z@)rWD0$KCZ#Q>AO^Y6g!xa%nB;8>;7yOGEHqN12?WP7i*2xZ;@U;e;b7qYr+L9$}9TP`THRiI4*PlB+#WcSuXT>bLvIs9L7F0uc zj9k4?v!hf9iP|K``4S&w-S87 zE$ZRA$B3yP7Cp&4-XD-&eI9Qm(3;TuXrm-H%WgI|tBMOZt8uq(?9a7$d@Z7u>diVe zOIncg1)a^^V+QOfdsx0!<3e~bs+LRjpiuL5H+QrDvd?A`J(*0v2#!KrB&%ki$$^$w zJ>FIln&uj@D16J+xh;Jsp+zgV#;D+z1wRIMNkcnwCLqM^uxjUWj1rDxCHn@hbvS9v zwB-UH{l3*xvzw4*y-RmkR;4C&Lvx#WVZ&;_Ep!j{wvoA27f4Tk)zdm_*sE+1BZ8Rf z^+EA&wj9TJ%tU)mX)xA~ajVqUp5^Tt&o|KG3g(fHidSgR1Dd%TRxk@dPuX!R&^`-s zPiqK5_~(Zp&JkV#D`(@jXzk&L>qJ_-d%=d3Pv?-=H?#3FTTj=s2|j#RR{~f;7PPfW zm@~jh;ynTI*IWIgncPFOABu3OT2gb$-|ti|L3b}4RH1dnP4bMrH|EMZrH6H5BqpG~ zGy?M(NzA1qG0v4fF%#X7?VZTch}5N7!x+pZR7?bqLvgj08JH6us3VTbQ?x`B%jp>_ ze9K57JgXE|DHi$e6-;3++_i)T!Dyx@X-fK@y)lXoMH02t(j3ggm%~8Xq%_IwL>mgF zgkaLNytK=H4K)aT4TgbN1^{8ocnWiFfGM33V>ztoM@>)rD1|TYVkw ztr09T4jm7ml9Ece-8}r-4w)Cs*kUBk{q9=|;T97@)}lMYmhvLlyB#ebH@8NEBN|nb z``oV&Ob52nR9kf?`!p`x;dn<*GO*2|K;*~Rt}wc2g0+HN2v4#{PPNVUE8oVd`3gh5 zbQ_0C?68|v8@ny0Pz2oUk_?z;GnT>H4xP=o(-GnuS6c)v_*&$G2(#2|Qv?aS{zm?@l0$b;UmcL

e) zbu$wdT)X4U@EqtpkNY8oZH~7DUe*|=Gq-PjvW-$1dr^lg>GeUH*?!uYwB#zj z8%IH7*Kz3szX$lMdm4+d>B!2vPZtYn?E$AkC{3V#bu?y-8pk4mYAi^nlDv+bC)Sz> zDOWCMP2he?>CqoZE>gF%Vm{gvF;ED@j3+0?PCPkBV;jzI$NQ9$QX#Vhnjy3f zyU4=9vS8`J1wu_w*<`WsPQ^;X!5vvPubsq?KFk@%R-TSl+pgR#pS0R8pDef`z5*r} z5H+*1QMK0TP&1h}JKFdhnnKhHam?@tDPDpyG1Ggu@U0^BWCA(Rll8irnj37huO}Er z`a9YKronVh4LuVV-AoR`=_JyOj4tNjICc-g?W(kM8@bbfOUOd#)cTaCg3sL+=^5Y* zhqyqkC2pEMJu?<KR0vfab3bX7Qu;?82JZDtaW?rjs z<5!K~LCD-lGQmaGL4yNT%r9OeZnkcYxdpJX@>7#W<7i2cxu7UZSVSDz@N@Q7yJ<)) zDpGZ_JJe3%G)4~fWZUj|n>00Qb+HVjHy+EQR!hnj`pe7^{TpvxxoM+~v~CW~yp#P3QW; z!3CJPp!+CR*Xr}wu~*;u;Ih+IYv)xoaa*=r?WA27OMzCG4kPZzq{Vm>GLkaRMNg=8 zb^A=@h;S0xqC?QZ(^b&hvB-yzN+M+4AaoG+5De6SMcBl-#4ZM2VG*S|@m|bb?Hk!z z<*>w6A~p8mz|wn`#ZC58>`FzFyMH(BKi+{q7W%9le?}>oUigt;3;kcO%U>(Re|la1 z<}qVBExKPKS>DjN3qo%v93Uf(WN)c9P?M=*#a@d1g9#Gk8>3wO4A2M%fylnWi zpfNAl#1{0y@%tHM-(cBd7V_nDuDQ$x} zs=dl;pCy36(sSW+8Bt{`xadHl=vH8XW54*e_&K)(6UosRp)B65e^8*ZVck>$vOrNy zPKuQ?Ev~9R2weG6;iK=o6f^XfhYz;OCr1@)AIpVlzMx)C>o#4+(=#&U+_il-wqKzd*)y6Qx@_1}zy zOf=8)DMG}c>&Gyc8WFQ&%@XpwaN2dk^?dkjI2LjliS^a?hDiLz#Z&tck867J0T|To zG@=}CN~w^I8Z|_ZIZAXOM6M0Ez4iaI@^IdNC;$r^8GIPAT>JZDKGN6JM@uZN7 zLubh0p1h{Dyo?Jh0>bU3U(S`u2{l U_Rnfz;CPN+LX(h)$caM#KeUb|{Qv*} literal 0 HcmV?d00001 diff --git a/src/lambdammm_vm_structure.svg b/src/lambdammm_vm_structure.svg new file mode 100644 index 0000000..1652cb8 --- /dev/null +++ b/src/lambdammm_vm_structure.svg @@ -0,0 +1,1731 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + Virtual Machine + + + Program Counter + + + + State_Ptr + + + + Audio Driver + + + + Call Stack + + + + + + + + ... + + + + State Storage + + + + Closure Storage + + + + + + + + + Base Pointer + + + + + + + State Position + + + + State for self 1 + + Ring Buffer for delay 1 + + State for self 2 + + Ring Buffer for delay 2 + + + + ... + + + + + + + + + + + + Program + + Function Prototype0 + + Static Variables + + + ... + + + + + ... + Function Prototype1 + + + + + + OP + + + + A + + + + B + + + + C + + + + + + + + + Upvalue List + + + Program + State Size + + + N1 + N2 + + + + + + Open Closure + + Function Prototype + + + State Storage + + Upvalues + Negative Offset of Stack: N1 + Negative Offset of Stack: N2 + + + State Position + + + + + ` + + + + + + + + + + + Escaped Closure + + Function Prototype + + + State Storage + + Upvalues + + State Position + + + + Closed Upvalue 1 + Closed Upvalue 2 + + + + + + Somewhere on the Heap Memory (Maybe Shared with other closures) + + + + diff --git a/src/main.tex b/src/main.tex index 66682dd..265d273 100644 --- a/src/main.tex +++ b/src/main.tex @@ -208,10 +208,14 @@ Currently, it has been proved that BDA can be converted to a general-purpose fun Also, Kronos\cite{norilo2015} and W-calculus\cite{arias2021} are examples of attempts at lambda-calculus-based abstraction, while being influenced by Faust. Kronos is based on the theoretical foundation of System-$F\omega$, a lambda computation in which the type itself is the object of the lambda abstraction (a function can be defined that computes the type and returns a new type). The W-calculus limits the systems it represents to linear time-invariant ones and defines a more formal semantics, aiming at automatic proofs of the linearlity and an identity of graph topologies. -Previously, the author designed a programming language for music \textit{mimium} \cite{Matsuura2021}. It adds the basic operations of delay and feedback to lambda-calculus, signal processing can be expressed concisely while having a syntax close to that of general-purpose programming languages. +Previously, the author designed a programming language for music \textit{mimium} \cite{matsuura2021a}. It adds the basic operations of delay and feedback to lambda-calculus, signal processing can be expressed concisely while having a syntax close to that of general-purpose programming languages(especially, the syntax of mimium is designed to be looks like Rust language). In this paper, we present the syntax and semantics of a computational model: \lambdammm, which is an intermediate representation of mimium based on W-calculus. We also propose a virtual machine and its instruction set for efficient execution of this computational model. +One of the previous issues with mimium was the inability to compile the codes which contains a combination of recursive or higher-order functions and stateful functions because the compiler can not be determine the data size of the internal state of the signal processing. + +In this paper, the syntax and semantics of \lambdammm, a superset of the W-calculus-based call-by-value simply-typed lambda calculus are explained, as a computation model that is supposed to be an intermediate representation of mimium. Also a virtual machine and its instruction set are proposed to execute this computation model practically. Based on this model, it is possible to describe and execute generative signal processing in mimium. + \section{Syntax} \label{sec:syntax} @@ -292,7 +296,7 @@ VM Instructions for \lambdammm differs from Lua VM in the following respects. \end{enumerate} -Instructions in \lambdammm VM are 32bit tagged-union data that has up to 3 operands. Currently, a bit width for tag and each operands are all 8 bit\footnote[1]{Reason for this is easy to implemented on \textrm{enum} data structure on Rust, a host language of the latest mimium compiler.}. +Instructions in \lambdammm VM are 32bit tagged-union data that has up to 3 operands. Currently, a bit width for tag and each operands are all 8 bit\footnote[1]{Reason for this is that it is easy to implemented on \textrm{enum} data structure on Rust, a host language of the latest mimium compiler. Operands bitwidth and alignment may be changed in the future.}. The VM of \lambdammm is a register machine like the Lua VM(after version 5, although the VM has no real register but the register number simply means the offset index of call stack from the base pointer at the point of execution of the VM). The first operand of most instructions is the register number in which to store the result of the calculation. @@ -313,18 +317,24 @@ SETUPVALUE & A B & U(B) := R(A) \\ GETSTATE & A & R(A) := SPtr[SPos] \\ SETSTATE & A & Sptr[SPos] := R(A) \\ SHIFTSTATE & sAx & SPos += sAx \\ +DELAY & A B & R(A) := update\_ringbuffer(SPtr[SPos],R(B)) \\ JMP & sAx & PC +=sAx \\ JMPIFNEG & A sBx & if (R(A)<0) then PC += sBx \\ -CALL & A B C & R(A), ... ,R(A+C-2) := program.functions[R(A)](R(A+1),...,R(A+B-1)) \\ -CALLCLS & A B C & Sptr := vm.closures[R(A)].Sptr; \\ -\ & \ & R(A), ... ,R(A+C-2) := vm.closures[R(A)].fnproto(R(A+1),...,R(A+B-1)); \\ -\ & \ & Sptr := global\_sptr \\ +CALL & A B C & R(A),...,R(A+C-2) := program.functions[R(A)](R(A+1),...,R(A+B-1)) \\ +CALLCLS & A B C & Sptr := vm.closures[R(A)].Sptr \\ +\ & \ & R(A),...,R(A+C-2) := vm.closures[R(A)].fnproto(R(A+1),...,R(A+B-1)) \\ +\ & \ & Sptr := vm.global\_sptr \\ +CLOSURE & A Bx & vm.closures.push(closure(program.functions[R(Bx)])) \\ + & & R(A) := vm.closures.length - 1 \\ +CLOSE & A & close stack variables up to R(A)\\ RETURN & A B & return R(A), R(A+1)...,R(A+B-2) \\ ADDF & A B C & R(A) := R(B) as float + R(C) as float\\ SUBF & A B C & R(A) := R(B) as float - R(C) as float\\ MULF & A B C & R(A) := R(B) as float * R(C) as float\\ DIVF & A B C & R(A) := R(B) as float / R(C) as float\\ -\multicolumn{3}{l}{ +ADDF & A B C & R(A) := R(B) as int + R(C) as in \\ +\ & +\multicolumn{2}{l}{ \textit{...Other basic arithmetics continues for each primitive types...} } \end{tabular} @@ -354,6 +364,25 @@ SETSTATE 2 // store to self RETURN 3 1 \end{lstlisting} +\subsection{Overview of the VM structure} +\label{sec:vmstructure} + + +The overview of a data structure of the VM, program and the instantiated closure for \lambdammm is shown in \ref{fig:vmstructure}. In addition to the normal call stack, the VM has a storage area for managing internal state data for feedback and delay. + +This storage area is accompanied by data indicating the position from which the internal state is retrieved by the \texttt{GETSTATE} / \texttt{SETSTATE} instructions. This position is modified by \texttt{SHIFTSTATE} operation. The the actual data in the memory area are statically layed out at compile time by analyzing function calls that include references to self, delay and the functions which will call such statefull functions recursively. + +However, in the case of higher-order functions that receive a function as an argument and return another function, the layout of the internal state of the receiving function is unknown at the compilation, so an internal state storage area is created for each instantiated closure separately from the global storage area held by the VM itself. The VM switches the \texttt{State\_Ptr}, which points the internal state storage to be used, at each closure call, to the storage area on the closure, and returns a pointer pointing to the global storage area each time the closure context ends. + +Instantiated closures also hold the storage area of Upvalues. Until the closure exits the context of the parent function (Open Closure), Upvalues holds a negative offset on the stack at the current execution. Because this offset value can be determined at compile time, stored in the function prototype in the program. + +When the closure escapes from the original function with \texttt{RETURN} instruction, inserted \texttt{CLOSE} instruction before the return, which causes, Actual upvalues are moved from stack to somewhere on the heap memory. This Upvalue may be referenced from multiple locations when using nested closures, and some form of garbage collection needed to free memory after it is no longer referred. + +\begin{figure*}[ht] + \centerline{\includegraphics[width=\hsize]{lambdammm_vm_structure}} + \caption{\label{fig:vmstructure}{\it Overview of the virtual machine, program and instantiated closures for \lambdammm.}} +\end{figure*} + \section{Discussion} \label{sec:discussion} @@ -365,7 +394,7 @@ Because mimium treats functions that have internal states which change over time An example is the higher-order function \texttt{filterbank}, which duplicates \texttt{filter} function \texttt{N} times parametrically, and mix them together. Listing.\ref{lst:filterbank_bad} is an example of an incorrect code, and Listing.\ref{lst:filterbank_good} is an example of the code that behave correctly. The difference between Listing.\ref{lst:filterbank_bad} and Listing.\ref{lst:filterbank_good} is that the recursive calls in the filterbank function are written directly in the inner function to be returned, and the recursive calls in the filterbank function are written with \texttt{let} binding out of the inner function\footnote[2]{In the previous specification of mimium in \cite{matsuura2021a}, the binding of new variable and destructive assignment were the same syntax(\texttt{x = a}) but the syntax for the variable binding has changed to use \texttt{let} keyword.}. Similarly, in the \texttt{dsp} function that will be called by the audio driver, the difference is whether the filterbank function is executed inside \texttt{dsp} or bound with \texttt{let} once in the global context. -In the case of normal functional language, if all the functions used in a composition do not contain destructive assignments, the calculation process will not change even if the variable bound by let is manually replaced with its term(Beta reduction), as in the conversion from Listing.\ref{lst:filterbank_good} to Listing.\ref{lst:filterbank_bad}. +In the case of normal functional language, if all the functions used in a composition do not contain destructive assignments, the calculation process will not change even if the variable bound by \texttt{let} is manually replaced with its term(beta reduction), as in the conversion from Listing.\ref{lst:filterbank_good} to Listing.\ref{lst:filterbank_bad}. But in mimium, there are two major stages of evaluation: the code is evaluated in the global environment (finalization of the signal processing graph) at first, then the dsp function is repeatedly executed (actual signal processing), and the function may involve implicit internal state updates. Therefore, even though the code does not include destructive assignments, the recursive execution of the \texttt{filterbank} function is performed only once in Listing.\ref{lst:filterbank_good} for the evaluation of the global environment, whereas in Listing.\ref{lst:filterbank_bad}, every sample the dsp function is executed, the recursive function is executed and a closure is generated. Since the initialization of the internal state in the closure is performed at the time of closure allocation, in the example of Listing\ref{lst:filterbank_bad}, the internal state of the closure after the evaluation of \texttt{filterbank} is reset at each time step. diff --git a/src/syntax.tex b/src/syntax.tex index 1ef2c61..2aa08b4 100644 --- a/src/syntax.tex +++ b/src/syntax.tex @@ -44,6 +44,7 @@ e \; ::=& \ x &x \in {v_p} \ & [value]\\ |& \ let\; x = e_1\; in\; e_2 & & [let]\\ |& \ fix \; x.e & & [fixpoint]\\ |& \ e_1 \; e_2 & & [app]\\ + |& \ if\; (e_c)\; e_t\; else\; e_e \; & & [if] \\ |& \ delay\; n \; e_1 \; e_2 &n \in \mathbb{N}\ & [delay]\\ |& \ feed \; x.e & & [feed]\\ %%|& \quad (e_1,e_2) \quad & [product]\\ diff --git a/src/typing.tex b/src/typing.tex index a1ea6f5..988bb50 100644 --- a/src/typing.tex +++ b/src/typing.tex @@ -15,13 +15,20 @@ \end{equation*}\textrm{T-DELAY} \end{minipage}\\ - \begin{minipage}[t]{0.45\hsize} + \begin{minipage}[t]{0.4\hsize} \centering \begin{equation*} \frac{\Gamma, x : \tau_p \vdash e: \tau_p }{\Gamma \vdash feed\ x.e:\tau_p} \end{equation*}\textrm{T-FEED} \end{minipage}& + \begin{minipage}[t]{0.45\hsize} + \centering + \begin{equation*} + \frac{ \Gamma \vdash e_c : R\ \Gamma \vdash e_t:\tau\ \Gamma \vdash e_e:\tau }{\Gamma \vdash if\ (e_c)\ e_t\ e_e\ : \tau} + \end{equation*}\textrm{T-IF} + \end{minipage}\\ + \end{tabular} \caption{\label{fig:typing}{\it Typing rules for lambda abstraction and feed abstraction in $\lambda_{mmm}$.}} \end{figure} \ No newline at end of file