tomoyanonymous/ifc-2024-lambdammm
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

submission

Browse Source
This commit is contained in:
松浦 知也 Matsuura Tomoya
2024-07-12 12:47:33 +00:00
parent a6a3ddb641
commit 17e8fc8925
10 changed files with 2539 additions and 313 deletions
Download Patch File Download Diff File Expand all files Collapse all files

BIN
src/fbdelay_spos.pdf Normal file
View File

Binary file not shown.

381
src/fbdelay_spos.svg Normal file
View File

@@ -0,0 +1,381 @@
<?xml version="1.0" encoding="UTF-8" standalone="no"?>
<!-- Created with Inkscape (http://www.inkscape.org/) -->
<svg
width="58.050533mm"
height="65.004601mm"
viewBox="0 0 58.050533 65.004601"
version="1.1"
id="svg1"
sodipodi:docname="fbdelay_explain.svg"
inkscape:version="1.3 (0e150ed, 2023-07-21)"
inkscape:export-filename="lambdammm_vm_structure.pdf"
inkscape:export-xdpi="300"
inkscape:export-ydpi="300"
xmlns:inkscape="http://www.inkscape.org/namespaces/inkscape"
xmlns:sodipodi="http://sodipodi.sourceforge.net/DTD/sodipodi-0.dtd"
xmlns="http://www.w3.org/2000/svg"
xmlns:svg="http://www.w3.org/2000/svg">
<sodipodi:namedview
id="namedview1"
pagecolor="#ffffff"
bordercolor="#000000"
borderopacity="0.25"
inkscape:showpageshadow="2"
inkscape:pageopacity="0.0"
inkscape:pagecheckerboard="0"
inkscape:deskcolor="#d1d1d1"
inkscape:document-units="mm"
inkscape:zoom="1.410082"
inkscape:cx="278.3526"
inkscape:cy="212.75358"
inkscape:window-width="1440"
inkscape:window-height="783"
inkscape:window-x="0"
inkscape:window-y="25"
inkscape:window-maximized="0"
inkscape:current-layer="layer1" />
<defs
id="defs1">
<marker
style="overflow:visible"
id="ArrowTriangleStylized"
refX="0"
refY="0"
orient="auto-start-reverse"
inkscape:stockid="Stylized triangle arrow"
markerWidth="1"
markerHeight="1"
viewBox="0 0 1 1"
inkscape:isstock="true"
inkscape:collect="always"
preserveAspectRatio="xMidYMid">
<path
transform="scale(0.5)"
style="fill:context-stroke;fill-rule:evenodd;stroke:context-stroke;stroke-width:1pt"
d="m 6,0 c -3,1 -7,3 -9,5 0,0 0,-4 2,-5 -2,-1 -2,-5 -2,-5 2,2 6,4 9,5 z"
id="path4" />
</marker>
<rect
x="37.223606"
y="23.78175"
width="113.7388"
height="18.611803"
id="rect76" />
<rect
x="37.223606"
y="23.78175"
width="115.3563"
height="39.639271"
id="rect78" />
<rect
x="37.223606"
y="23.78175"
width="113.7388"
height="18.611803"
id="rect81" />
<rect
x="37.223606"
y="23.78175"
width="115.3563"
height="39.639271"
id="rect82" />
<marker
style="overflow:visible"
id="ArrowTriangleStylized-7"
refX="0"
refY="0"
orient="auto-start-reverse"
inkscape:stockid="Stylized triangle arrow"
markerWidth="1"
markerHeight="1"
viewBox="0 0 1 1"
inkscape:isstock="true"
inkscape:collect="always"
preserveAspectRatio="xMidYMid">
<path
transform="scale(0.5)"
style="fill:context-stroke;fill-rule:evenodd;stroke:context-stroke;stroke-width:1pt"
d="m 6,0 c -3,1 -7,3 -9,5 0,0 0,-4 2,-5 -2,-1 -2,-5 -2,-5 2,2 6,4 9,5 z"
id="path4-6" />
</marker>
<marker
style="overflow:visible"
id="ArrowTriangleStylized-9"
refX="0"
refY="0"
orient="auto-start-reverse"
inkscape:stockid="Stylized triangle arrow"
markerWidth="1"
markerHeight="1"
viewBox="0 0 1 1"
inkscape:isstock="true"
inkscape:collect="always"
preserveAspectRatio="xMidYMid">
<path
transform="scale(0.5)"
style="fill:context-stroke;fill-rule:evenodd;stroke:context-stroke;stroke-width:1pt"
d="m 6,0 c -3,1 -7,3 -9,5 0,0 0,-4 2,-5 -2,-1 -2,-5 -2,-5 2,2 6,4 9,5 z"
id="path4-3" />
</marker>
<marker
style="overflow:visible"
id="ArrowTriangleStylized-8"
refX="0"
refY="0"
orient="auto-start-reverse"
inkscape:stockid="Stylized triangle arrow"
markerWidth="1"
markerHeight="1"
viewBox="0 0 1 1"
inkscape:isstock="true"
inkscape:collect="always"
preserveAspectRatio="xMidYMid">
<path
transform="scale(0.5)"
style="fill:context-stroke;fill-rule:evenodd;stroke:context-stroke;stroke-width:1pt"
d="m 6,0 c -3,1 -7,3 -9,5 0,0 0,-4 2,-5 -2,-1 -2,-5 -2,-5 2,2 6,4 9,5 z"
id="path4-0" />
</marker>
<rect
x="37.223606"
y="23.78175"
width="113.7388"
height="18.611803"
id="rect76-9-0" />
<rect
x="37.223606"
y="23.78175"
width="113.7388"
height="18.611803"
id="rect76-9-0-2" />
<rect
x="37.223606"
y="23.78175"
width="113.7388"
height="18.611803"
id="rect76-9-0-2-5" />
<rect
x="37.223606"
y="23.78175"
width="113.7388"
height="18.611803"
id="rect76-9-0-2-5-4" />
<rect
x="37.223606"
y="23.78175"
width="113.7388"
height="18.611803"
id="rect76-9-0-2-5-4-9" />
</defs>
<rect
style="fill:#ffffff;stroke:#000000;stroke-width:0.1;stroke-linejoin:round;stroke-dasharray:none;stroke-dashoffset:0;stroke-opacity:1"
id="rect111"
width="57.950535"
height="64.904602"
x="0.050000031"
y="0.050000437" />
<g
inkscape:label="Layer 1"
inkscape:groupmode="layer"
id="layer1"
transform="translate(-6.9040643,-8.6871612)">
<g
id="g75"
transform="translate(-3.0441009,-61.517576)">
<rect
style="fill-opacity:0;stroke:#000000;stroke-width:0.238248;stroke-dasharray:none;stroke-opacity:1"
id="rect77"
width="31.672922"
height="23.205704"
x="15.724542"
y="80.38961" />
<text
xml:space="preserve"
transform="matrix(0.26458333,0,0,0.26458333,6.1877822,74.420715)"
id="text77"
style="font-style:normal;font-variant:normal;font-weight:normal;font-stretch:normal;font-size:13.3333px;font-family:'Helvetica Neue';-inkscape-font-specification:'Helvetica Neue, Normal';font-variant-ligatures:normal;font-variant-caps:normal;font-variant-numeric:normal;font-variant-east-asian:normal;word-spacing:0px;white-space:pre;shape-inside:url(#rect78);display:inline;fill:#000000;fill-opacity:1;fill-rule:nonzero"><tspan
x="37.222656"
y="36.34345"
id="tspan2">Ring Buffer for &#10;</tspan><tspan
x="37.222656"
y="53.010076"
id="tspan3">delay 1</tspan></text>
<rect
style="fill-opacity:0;stroke:#000000;stroke-width:0.238248;stroke-dasharray:none;stroke-opacity:1"
id="rect79"
width="31.672922"
height="5.0172825"
x="15.724542"
y="103.57951" />
<text
xml:space="preserve"
transform="matrix(0.26458333,0,0,0.26458333,5.9738008,97.610619)"
id="text79"
style="font-style:normal;font-variant:normal;font-weight:normal;font-stretch:normal;font-size:13.3333px;font-family:'Helvetica Neue';-inkscape-font-specification:'Helvetica Neue, Normal';font-variant-ligatures:normal;font-variant-caps:normal;font-variant-numeric:normal;font-variant-east-asian:normal;word-spacing:0px;white-space:pre;shape-inside:url(#rect81);display:inline;fill:#000000;fill-opacity:1;fill-rule:nonzero"><tspan
x="37.222656"
y="36.353868"
id="tspan5">State for <tspan
style="font-style:italic"
id="tspan4">self </tspan>2</tspan></text>
<rect
style="fill-opacity:0;stroke:#000000;stroke-width:0.238248;stroke-dasharray:none;stroke-opacity:1"
id="rect80"
width="31.672922"
height="23.205704"
x="15.724542"
y="108.62543" />
<text
xml:space="preserve"
transform="matrix(0.26458333,0,0,0.26458333,6.1877822,102.65654)"
id="text80"
style="font-style:normal;font-variant:normal;font-weight:normal;font-stretch:normal;font-size:13.3333px;font-family:'Helvetica Neue';-inkscape-font-specification:'Helvetica Neue, Normal';font-variant-ligatures:normal;font-variant-caps:normal;font-variant-numeric:normal;font-variant-east-asian:normal;word-spacing:0px;white-space:pre;shape-inside:url(#rect82);display:inline;fill:#000000;fill-opacity:1;fill-rule:nonzero"><tspan
x="37.222656"
y="36.34345"
id="tspan6">Ring Buffer for &#10;</tspan><tspan
x="37.222656"
y="53.010076"
id="tspan7">delay 2</tspan></text>
<text
xml:space="preserve"
style="font-size:2.11667px;font-family:'Hiragino Mincho ProN';-inkscape-font-specification:'Hiragino Mincho ProN';word-spacing:0px;fill:#000000;stroke:none;stroke-width:0.264999;stroke-linejoin:round;stroke-dasharray:none;stroke-dashoffset:0;stroke-opacity:1"
x="60.299187"
y="94.177162"
id="text106"><tspan
sodipodi:role="line"
id="tspan106"
style="stroke-width:0.265"
x="60.299187"
y="94.177162"></tspan></text>
<rect
style="fill-opacity:0;stroke:#000000;stroke-width:0.238248;stroke-dasharray:none;stroke-opacity:1"
id="rect75"
width="31.672922"
height="5.0172825"
x="15.724542"
y="75.343689" />
<text
xml:space="preserve"
transform="matrix(0.26458333,0,0,0.26458333,5.9738009,69.374792)"
id="text75"
style="font-style:normal;font-variant:normal;font-weight:normal;font-stretch:normal;font-size:13.3333px;font-family:'Helvetica Neue';-inkscape-font-specification:'Helvetica Neue, Normal';font-variant-ligatures:normal;font-variant-caps:normal;font-variant-numeric:normal;font-variant-east-asian:normal;word-spacing:0px;white-space:pre;shape-inside:url(#rect76);display:inline;fill:#000000;fill-opacity:1;fill-rule:nonzero"><tspan
x="37.222656"
y="36.353868"
id="tspan9">State for <tspan
style="font-style:italic"
id="tspan8">self </tspan>1</tspan></text>
<g
id="g107"
transform="translate(-1.0263305)">
<circle
style="fill:#ffffff;stroke:#000000;stroke-width:0.1;stroke-linejoin:round;stroke-dasharray:none;stroke-dashoffset:0;stroke-opacity:1"
id="path107-6"
cx="45.614277"
cy="80.701118"
r="1.4569392" />
<text
xml:space="preserve"
transform="matrix(0.26458333,0,0,0.26458333,35.226816,73.158862)"
id="text75-9-9"
style="font-style:normal;font-variant:normal;font-weight:normal;font-stretch:normal;font-size:8px;font-family:'Helvetica Neue';-inkscape-font-specification:'Helvetica Neue, Normal';font-variant-ligatures:normal;font-variant-caps:normal;font-variant-numeric:normal;font-variant-east-asian:normal;word-spacing:0px;white-space:pre;shape-inside:url(#rect76-9-0);display:inline;fill:#000000;fill-opacity:1;fill-rule:nonzero"><tspan
x="37.222656"
y="31.318589"
id="tspan10">1</tspan></text>
</g>
<g
id="g108">
<circle
style="fill:#ffffff;stroke:#000000;stroke-width:0.1;stroke-linejoin:round;stroke-dasharray:none;stroke-dashoffset:0;stroke-opacity:1"
id="path107-6-3"
cx="49.632725"
cy="80.862404"
r="1.4569392" />
<text
xml:space="preserve"
transform="matrix(0.26458333,0,0,0.26458333,39.243713,73.315375)"
id="text75-9-9-0"
style="font-style:normal;font-variant:normal;font-weight:normal;font-stretch:normal;font-size:8px;font-family:'Helvetica Neue';-inkscape-font-specification:'Helvetica Neue, Normal';font-variant-ligatures:normal;font-variant-caps:normal;font-variant-numeric:normal;font-variant-east-asian:normal;word-spacing:0px;white-space:pre;shape-inside:url(#rect76-9-0-2);display:inline;fill:#000000;fill-opacity:1;fill-rule:nonzero"><tspan
x="37.222656"
y="31.318589"
id="tspan11">2</tspan></text>
</g>
<g
id="g109">
<circle
style="fill:#ffffff;stroke:#000000;stroke-width:0.1;stroke-linejoin:round;stroke-dasharray:none;stroke-dashoffset:0;stroke-opacity:1"
id="path107-6-3-1"
cx="53.939831"
cy="94.022964"
r="1.4569392" />
<text
xml:space="preserve"
transform="matrix(0.26458333,0,0,0.26458333,43.50265,86.487746)"
id="text75-9-9-0-4"
style="font-style:normal;font-variant:normal;font-weight:normal;font-stretch:normal;font-size:8px;font-family:'Helvetica Neue';-inkscape-font-specification:'Helvetica Neue, Normal';font-variant-ligatures:normal;font-variant-caps:normal;font-variant-numeric:normal;font-variant-east-asian:normal;word-spacing:0px;white-space:pre;shape-inside:url(#rect76-9-0-2-5);display:inline;fill:#000000;fill-opacity:1;fill-rule:nonzero"><tspan
x="37.222656"
y="31.318589"
id="tspan12">3</tspan></text>
</g>
<g
id="g111"
transform="translate(-1.3554851,-0.21179455)">
<circle
style="fill:#ffffff;stroke:#000000;stroke-width:0.1;stroke-linejoin:round;stroke-dasharray:none;stroke-dashoffset:0;stroke-opacity:1"
id="path107-6-3-3"
cx="44.845379"
cy="109.87311"
r="1.4569392" />
<text
xml:space="preserve"
transform="matrix(0.26458333,0,0,0.26458333,34.413789,102.32052)"
id="text75-9-9-0-4-3"
style="font-style:normal;font-variant:normal;font-weight:normal;font-stretch:normal;font-size:8px;font-family:'Helvetica Neue';-inkscape-font-specification:'Helvetica Neue, Normal';font-variant-ligatures:normal;font-variant-caps:normal;font-variant-numeric:normal;font-variant-east-asian:normal;word-spacing:0px;white-space:pre;shape-inside:url(#rect76-9-0-2-5-4);display:inline;fill:#000000;fill-opacity:1;fill-rule:nonzero"><tspan
x="37.222656"
y="31.318589"
id="tspan13">4</tspan></text>
</g>
<g
id="g110">
<circle
style="fill:#ffffff;stroke:#000000;stroke-width:0.1;stroke-linejoin:round;stroke-dasharray:none;stroke-dashoffset:0;stroke-opacity:1"
id="path107-6-3-5"
cx="60.29295"
cy="94.142822"
r="1.4569392" />
<text
xml:space="preserve"
transform="matrix(0.26458333,0,0,0.26458333,49.870157,86.582398)"
id="text75-9-9-0-4-3-1"
style="font-style:normal;font-variant:normal;font-weight:normal;font-stretch:normal;font-size:8px;font-family:'Helvetica Neue';-inkscape-font-specification:'Helvetica Neue, Normal';font-variant-ligatures:normal;font-variant-caps:normal;font-variant-numeric:normal;font-variant-east-asian:normal;word-spacing:0px;white-space:pre;shape-inside:url(#rect76-9-0-2-5-4-9);display:inline;fill:#000000;fill-opacity:1;fill-rule:nonzero"><tspan
x="37.222656"
y="31.318589"
id="tspan14">5</tspan></text>
</g>
</g>
<path
style="fill:none;stroke:#999999;stroke-width:0.264999;stroke-linejoin:round;stroke-dasharray:none;stroke-dashoffset:0;stroke-opacity:1;marker-end:url(#ArrowTriangleStylized)"
d="m 41.536022,16.880034 c 0,0 2.196051,0.971397 2.224392,2.401003 0.02917,1.471405 -2.276185,1.940972 -2.276185,1.940972"
id="path106"
sodipodi:nodetypes="csc" />
<path
style="fill:none;stroke:#999999;stroke-width:0.264999;stroke-linejoin:round;stroke-dasharray:none;stroke-dashoffset:0;stroke-opacity:1;marker-end:url(#ArrowTriangleStylized-8)"
d="m 41.169643,45.995892 c 0,0 2.196051,0.971397 2.224392,2.401003 0.02917,1.471405 -2.276185,1.940972 -2.276185,1.940972"
id="path106-0"
sodipodi:nodetypes="csc" />
<path
style="fill:none;stroke:#999999;stroke-width:0.264999;stroke-linejoin:round;stroke-dasharray:none;stroke-dashoffset:0;stroke-opacity:1;marker-end:url(#ArrowTriangleStylized-9)"
d="m 41.965409,15.643326 c 0,0 10.707847,1.039181 10.841541,14.510639 0.145801,14.691442 -11.365391,14.489066 -11.365391,14.489066"
id="path106-2"
sodipodi:nodetypes="csc" />
<path
style="fill:none;stroke:#999999;stroke-width:0.264999;stroke-linejoin:round;stroke-dasharray:none;stroke-dashoffset:0;stroke-opacity:1;marker-start:url(#ArrowTriangleStylized-8)"
d="m 42.90918,15.131599 c 0,0 12.375502,3.014503 12.509196,16.485961 0.145801,14.691442 -14.54125,19.953214 -14.54125,19.953214"
id="path106-2-7"
sodipodi:nodetypes="csc" />
<path
style="fill:none;stroke:#999999;stroke-width:0.264999;stroke-linejoin:round;stroke-dasharray:none;stroke-dashoffset:0;stroke-opacity:1;marker-end:url(#ArrowTriangleStylized-7)"
d="m 41.944461,21.265159 c 0,0 3.836439,0.08573 3.718899,-2.39661 -0.07451,-1.573548 -3.005988,-2.209014 -3.005988,-2.209014"
id="path106-8"
sodipodi:nodetypes="csc" />
</g>
</svg>
Side by Side

After

Width:  |  Height:  |  Size: 17 KiB

BIN
src/lambdammm_vm_structure.pdf
View File

Binary file not shown.

201
src/lambdammm_vm_structure.svg
View File

@@ -9,6 +9,9 @@
id="svg1"
sodipodi:docname="vmmodel.svg"
inkscape:version="1.3 (0e150ed, 2023-07-21)"
inkscape:export-filename="lambdammm_vm_structure.pdf"
inkscape:export-xdpi="300"
inkscape:export-ydpi="300"
xmlns:inkscape="http://www.inkscape.org/namespaces/inkscape"
xmlns:sodipodi="http://sodipodi.sourceforge.net/DTD/sodipodi-0.dtd"
xmlns:xlink="http://www.w3.org/1999/xlink"
@@ -24,15 +27,15 @@
inkscape:pagecheckerboard="0"
inkscape:deskcolor="#d1d1d1"
inkscape:document-units="mm"
inkscape:zoom="0.62112407"
inkscape:cx="477.36034"
inkscape:cy="323.60684"
inkscape:zoom="0.98354534"
inkscape:cx="417.36764"
inkscape:cy="219.61367"
inkscape:window-width="1440"
inkscape:window-height="783"
inkscape:window-x="0"
inkscape:window-y="25"
inkscape:window-maximized="0"
inkscape:current-layer="layer2" />
inkscape:current-layer="layer1" />
<defs
id="defs1">
<marker
@@ -651,6 +654,84 @@
d="m 6,0 c -3,1 -7,3 -9,5 0,0 0,-4 2,-5 -2,-1 -2,-5 -2,-5 2,2 6,4 9,5 z"
id="path4-9-4-0-7-0" />
</marker>
<marker
style="overflow:visible"
id="Dot-9"
refX="0"
refY="0"
orient="auto"
inkscape:stockid="Dot"
markerWidth="1"
markerHeight="1"
viewBox="0 0 1 1"
inkscape:isstock="true"
inkscape:collect="always"
preserveAspectRatio="xMidYMid">
<path
transform="scale(0.5)"
style="fill:context-stroke;fill-rule:evenodd;stroke:none"
d="M 5,0 C 5,2.76 2.76,5 0,5 -2.76,5 -5,2.76 -5,0 c 0,-2.76 2.3,-5 5,-5 2.76,0 5,2.24 5,5 z"
sodipodi:nodetypes="sssss"
id="path17-0" />
</marker>
<marker
style="overflow:visible"
id="ArrowTriangleStylized-4"
refX="0"
refY="0"
orient="auto-start-reverse"
inkscape:stockid="Stylized triangle arrow"
markerWidth="1"
markerHeight="1"
viewBox="0 0 1 1"
inkscape:isstock="true"
inkscape:collect="always"
preserveAspectRatio="xMidYMid">
<path
transform="scale(0.5)"
style="fill:context-stroke;fill-rule:evenodd;stroke:context-stroke;stroke-width:1pt"
d="m 6,0 c -3,1 -7,3 -9,5 0,0 0,-4 2,-5 -2,-1 -2,-5 -2,-5 2,2 6,4 9,5 z"
id="path4-02" />
</marker>
<marker
style="overflow:visible"
id="Dot-9-5"
refX="0"
refY="0"
orient="auto"
inkscape:stockid="Dot"
markerWidth="1"
markerHeight="1"
viewBox="0 0 1 1"
inkscape:isstock="true"
inkscape:collect="always"
preserveAspectRatio="xMidYMid">
<path
transform="scale(0.5)"
style="fill:context-stroke;fill-rule:evenodd;stroke:none"
d="M 5,0 C 5,2.76 2.76,5 0,5 -2.76,5 -5,2.76 -5,0 c 0,-2.76 2.3,-5 5,-5 2.76,0 5,2.24 5,5 z"
sodipodi:nodetypes="sssss"
id="path17-0-4" />
</marker>
<marker
style="overflow:visible"
id="ArrowTriangleStylized-4-9"
refX="0"
refY="0"
orient="auto-start-reverse"
inkscape:stockid="Stylized triangle arrow"
markerWidth="1"
markerHeight="1"
viewBox="0 0 1 1"
inkscape:isstock="true"
inkscape:collect="always"
preserveAspectRatio="xMidYMid">
<path
transform="scale(0.5)"
style="fill:context-stroke;fill-rule:evenodd;stroke:context-stroke;stroke-width:1pt"
d="m 6,0 c -3,1 -7,3 -9,5 0,0 0,-4 2,-5 -2,-1 -2,-5 -2,-5 2,2 6,4 9,5 z"
id="path4-02-0" />
</marker>
</defs>
<g
inkscape:groupmode="layer"
@@ -665,7 +746,7 @@
x="4.6246214"
y="-42.83358"
transform="translate(0.11223495,49.292931)"
inkscape:export-filename="lambdammm_vm_structure.pdf"
inkscape:export-filename="lambdammm_vm_structure.svg"
inkscape:export-xdpi="300"
inkscape:export-ydpi="300" />
</g>
@@ -711,14 +792,36 @@
id="tspan4">Program Counter</tspan></text>
</g>
<g
id="g26">
id="g26"
transform="translate(0,-4.2333333)">
<rect
style="fill-opacity:0;stroke:#000000;stroke-width:0.238248;stroke-dasharray:none;stroke-opacity:1"
id="rect10"
width="35.489555"
height="6.4485202"
height="16.800972"
x="13.816225"
y="74.628067" />
<rect
style="fill:none;fill-opacity:1;fill-rule:nonzero;stroke:#000000;stroke-width:0.0999997;stroke-dasharray:none;stroke-opacity:1"
id="rect7-4"
width="30.647167"
height="2.850651"
x="16.096413"
y="79.944267" />
<rect
style="fill:none;fill-opacity:1;fill-rule:nonzero;stroke:#000000;stroke-width:0.0999997;stroke-dasharray:none;stroke-opacity:1"
id="rect7-4-0"
width="30.647167"
height="2.850651"
x="16.024565"
y="83.821106" />
<rect
style="fill:none;fill-opacity:1;fill-rule:nonzero;stroke:#000000;stroke-width:0.0999997;stroke-dasharray:none;stroke-opacity:1"
id="rect7-4-0-9"
width="30.647167"
height="2.850651"
x="15.950636"
y="87.38607" />
<text
xml:space="preserve"
transform="matrix(0.26458333,0,0,0.26458333,5.5108554,69.374792)"
@@ -726,11 +829,11 @@
style="font-style:normal;font-variant:normal;font-weight:normal;font-stretch:normal;font-size:13.3333px;font-family:'Helvetica Neue';-inkscape-font-specification:'Helvetica Neue, Normal';font-variant-ligatures:normal;font-variant-caps:normal;font-variant-numeric:normal;font-variant-east-asian:normal;word-spacing:0px;white-space:pre;shape-inside:url(#rect12);display:inline;fill:#000000;fill-opacity:1;fill-rule:nonzero"><tspan
x="37.222656"
y="36.34345"
id="tspan5">State_Ptr</tspan></text>
id="tspan5">State_Ptr Stack</tspan></text>
</g>
<g
id="g27"
transform="translate(0,14.57944)">
transform="translate(0,20.400274)">
<rect
style="fill-opacity:0;stroke:#000000;stroke-width:0.238248;stroke-dasharray:none;stroke-opacity:1"
id="rect11"
@@ -754,7 +857,7 @@
style="fill-opacity:0;stroke:#000000;stroke-width:0.264951;stroke-dasharray:none;stroke-opacity:1"
id="rect5"
width="35.236588"
height="49.041969"
height="44.867596"
x="14.029625"
y="23.997538" />
<text
@@ -802,7 +905,7 @@
</g>
<text
xml:space="preserve"
transform="matrix(0.26458333,0,0,0.26458333,6.1655345,60.912806)"
transform="matrix(0.26458333,0,0,0.26458333,6.6947012,57.737807)"
id="text13"
style="font-style:normal;font-variant:normal;font-weight:normal;font-stretch:normal;font-size:13.3333px;font-family:'Helvetica Neue';-inkscape-font-specification:'Helvetica Neue, Normal';font-variant-ligatures:normal;font-variant-caps:normal;font-variant-numeric:normal;font-variant-east-asian:normal;text-align:center;word-spacing:0px;white-space:pre;shape-inside:url(#rect14);display:inline;fill:#000000;fill-opacity:1;fill-rule:nonzero"
x="4.4466538"
@@ -814,7 +917,7 @@
</g>
<g
id="g40"
transform="translate(0,14.674112)">
transform="translate(0,21.024116)">
<rect
style="fill-opacity:0;stroke:#000000;stroke-width:0.238248;stroke-dasharray:none;stroke-opacity:1"
id="rect40"
@@ -833,7 +936,7 @@
</g>
<g
id="g42"
transform="translate(0,8.0834752)">
transform="translate(0,14.433478)">
<rect
style="fill-opacity:0;stroke:#000000;stroke-width:0.238248;stroke-dasharray:none;stroke-opacity:1"
id="rect42"
@@ -895,7 +998,7 @@
id="tspan11">Base Pointer</tspan></text>
</g>
<path
style="fill:none;fill-opacity:1;stroke:#000000;stroke-width:0.3;stroke-dasharray:none;stroke-opacity:1;marker-start:url(#Dot-3);marker-end:url(#ArrowTriangleStylized-3)"
style="fill:none;fill-opacity:1;stroke:#999999;stroke-width:0.3;stroke-dasharray:none;stroke-opacity:1;marker-start:url(#Dot-3);marker-end:url(#ArrowTriangleStylized-3)"
d="m 44.061959,34.888436 c 3.286473,1.971324 2.705122,14.737485 -0.0015,17.163674"
id="path82-8"
sodipodi:nodetypes="cc" />
@@ -1003,7 +1106,7 @@
id="tspan20">delay 2</tspan></text>
</g>
<path
style="fill:none;fill-opacity:1;stroke:#000000;stroke-width:0.3;stroke-dasharray:none;stroke-opacity:1;marker-start:url(#Dot-5);marker-end:url(#ArrowTriangleStylized-7)"
style="fill:none;fill-opacity:1;stroke:#808080;stroke-width:0.3;stroke-dasharray:none;stroke-opacity:1;marker-start:url(#Dot-5);marker-end:url(#ArrowTriangleStylized-7)"
d="m 44.277061,67.646766 c 3.286473,1.971324 3.386797,5.194041 0.680135,7.62023"
id="path82-6"
sodipodi:nodetypes="cc" />
@@ -1023,37 +1126,47 @@
id="a67">
<path
style="fill:none;fill-opacity:1;fill-rule:nonzero;stroke:#000000;stroke-width:0.265;stroke-dasharray:0.265, 0.265;stroke-dashoffset:0"
d="M 49.282007,82.046004 52.352176,16.755578"
d="m 49.297931,88.399453 c 0,0 1.14395,-5.446449 1.469616,-17.177405 0.510946,-18.405009 1.682932,-54.620946 1.682932,-54.620946"
id="path50"
sodipodi:nodetypes="cc" />
sodipodi:nodetypes="csc" />
</a>
<path
style="fill:none;fill-opacity:1;fill-rule:nonzero;stroke:#000000;stroke-width:0.265;stroke-dasharray:0.265, 0.265;stroke-dashoffset:0"
d="m 49.333785,88.786127 3.084682,-3.447006"
d="m 49.277612,95.175188 c 0,0 0.686548,-3.818603 1.295437,-5.653587 0.479913,-1.446292 1.845418,-4.18248 1.845418,-4.18248"
id="path51"
sodipodi:nodetypes="cc" />
sodipodi:nodetypes="csc" />
<path
style="fill:none;fill-opacity:1;fill-rule:nonzero;stroke:#000000;stroke-width:0.265;stroke-dasharray:0.265, 0.265;stroke-dashoffset:0"
d="m 49.310755,96.679581 3.095344,14.043429"
d="m 49.293284,103.0306 c 0,0 1.258853,0.45685 1.834479,1.74544 1.169649,2.61836 1.278336,5.94697 1.278336,5.94697"
id="path52"
sodipodi:nodetypes="cc" />
sodipodi:nodetypes="csc" />
<path
style="fill:none;fill-opacity:1;fill-rule:nonzero;stroke:#000000;stroke-width:0.265;stroke-dasharray:0.265, 0.265;stroke-dashoffset:0"
d="m 49.307622,90.370628 3.097157,-3.585981"
d="m 49.307622,96.710034 c 0,0 1.395344,-2.06183 1.819571,-3.219118 0.783212,-2.136599 1.277586,-6.706269 1.277586,-6.706269"
id="path53"
sodipodi:nodetypes="cc" />
sodipodi:nodetypes="csc" />
<path
style="fill:none;fill-opacity:1;stroke:#000000;stroke-width:0.3;stroke-dasharray:none;stroke-opacity:1;marker-start:url(#Dot);marker-end:url(#ArrowTriangleStylized)"
d="m 45.487942,77.365342 c 3.286473,1.971324 3.386797,5.194041 0.680135,7.62023"
style="fill:none;fill-opacity:1;stroke:#999999;stroke-width:0.3;stroke-dasharray:none;stroke-opacity:1;marker-start:url(#Dot);marker-end:url(#ArrowTriangleStylized)"
d="m 44.420809,76.913151 c 3.286473,1.971324 4.078403,11.936302 1.371741,14.362491"
id="path82"
sodipodi:nodetypes="cc" />
<path
style="fill:none;fill-opacity:1;stroke:#999999;stroke-width:0.3;stroke-dasharray:none;stroke-opacity:1;marker-start:url(#Dot-9);marker-end:url(#ArrowTriangleStylized-4)"
d="M 44.406273,81.086527 C 45.873423,78.294486 49.365468,60.319412 49.993338,49.806698 51.071659,31.751864 49.213137,17.949357 53.945437,12.610023 59.863825,5.9324552 78.627725,7.3034404 91.645716,7.2692487 109.87104,7.22138 124.34365,9.570292 126.27112,24.968824"
id="path82-4"
sodipodi:nodetypes="csssc" />
<path
style="fill:none;fill-opacity:1;stroke:#999999;stroke-width:0.3;stroke-dasharray:none;stroke-opacity:1;marker-start:url(#Dot-9-5);marker-end:url(#ArrowTriangleStylized-4-9)"
d="m 44.464845,84.637831 c 6.933653,0.803446 14.513032,-1.504985 21.76889,-4.742326 10.501739,-4.685554 20.325762,-11.316999 26.533395,-13.275761 6.888343,-2.173554 35.35504,-1.596044 33.7397,8.488279"
id="path82-4-0"
sodipodi:nodetypes="cssc" />
<rect
style="fill:none;stroke:#000000;stroke-width:0.2;stroke-linejoin:round;stroke-dasharray:0.2, 0.2;stroke-dashoffset:0;stroke-opacity:1"
id="rect83"
width="2.2771528"
height="2.411103"
x="44.270527"
y="84.455582" />
x="43.801117"
y="90.557884" />
</g>
<g
id="g43"
@@ -1345,7 +1458,7 @@
style="font-style:normal;font-variant:normal;font-weight:normal;font-stretch:normal;font-size:8px;font-family:'Helvetica Neue';-inkscape-font-specification:'Helvetica Neue, Normal';font-variant-ligatures:normal;font-variant-caps:normal;font-variant-numeric:normal;font-variant-east-asian:normal;word-spacing:0px;white-space:pre;shape-inside:url(#rect63-2-5);display:inline;fill:#000000;fill-opacity:1;fill-rule:nonzero"><tspan
x="37.222656"
y="31.318589"
id="tspan31"> N1</tspan></text>
id="tspan31"> Local(N1)</tspan></text>
<text
xml:space="preserve"
transform="matrix(0.26458333,0,0,0.26458333,72.285667,66.187541)"
@@ -1353,7 +1466,7 @@
style="font-style:normal;font-variant:normal;font-weight:normal;font-stretch:normal;font-size:8px;font-family:'Helvetica Neue';-inkscape-font-specification:'Helvetica Neue, Normal';font-variant-ligatures:normal;font-variant-caps:normal;font-variant-numeric:normal;font-variant-east-asian:normal;word-spacing:0px;white-space:pre;shape-inside:url(#rect63-2-5-5);display:inline;fill:#000000;fill-opacity:1;fill-rule:nonzero"><tspan
x="37.222656"
y="31.318589"
id="tspan32"> N2</tspan></text>
id="tspan32"> Upvalue(N2)</tspan></text>
<rect
style="fill:none;fill-opacity:1;fill-rule:nonzero;stroke:#000000;stroke-width:0.158518;stroke-dasharray:none;stroke-opacity:1"
id="rect85"
@@ -1451,17 +1564,17 @@
style="font-style:normal;font-variant:normal;font-weight:normal;font-stretch:normal;font-size:8px;font-family:'Helvetica Neue';-inkscape-font-specification:'Helvetica Neue, Normal';font-variant-ligatures:normal;font-variant-caps:normal;font-variant-numeric:normal;font-variant-east-asian:normal;word-spacing:0px;white-space:pre;shape-inside:url(#rect63-2);display:inline;fill:#000000;fill-opacity:1;fill-rule:nonzero"><tspan
x="37.222656"
y="31.318589"
id="tspan41">Negative Offset of Stack: N1</tspan></text>
id="tspan41">Open(Local(N1))</tspan></text>
<text
xml:space="preserve"
transform="matrix(0.26458333,0,0,0.26458333,86.826022,48.365001)"
id="text62-8-4"
style="font-style:normal;font-variant:normal;font-weight:normal;font-stretch:normal;font-size:8px;font-family:'Helvetica Neue';-inkscape-font-specification:'Helvetica Neue, Normal';font-variant-ligatures:normal;font-variant-caps:normal;font-variant-numeric:normal;font-variant-east-asian:normal;word-spacing:0px;white-space:pre;shape-inside:url(#rect63-2-8);display:inline;fill:#000000;fill-opacity:1;fill-rule:nonzero"><tspan
style="font-style:normal;font-variant:normal;font-weight:normal;font-stretch:normal;font-size:8px;font-family:'Helvetica Neue';-inkscape-font-specification:'Helvetica Neue, Normal';font-variant-ligatures:normal;font-variant-caps:normal;font-variant-numeric:normal;font-variant-east-asian:normal;word-spacing:0px;white-space:pre;shape-inside:url(#rect63-2-8);display:inline;fill:#000000;fill-opacity:1;fill-rule:nonzero;stroke-width:1.00157;stroke-dasharray:none"><tspan
x="37.222656"
y="31.318589"
id="tspan42">Negative Offset of Stack: N2</tspan></text>
id="tspan42">Open(Upvalue(N2))</tspan></text>
<path
style="fill:none;fill-opacity:1;stroke:#000000;stroke-width:0.3;stroke-dasharray:none;stroke-opacity:1;marker-start:url(#Dot-53);marker-end:url(#ArrowTriangleStylized-73)"
style="fill:none;fill-opacity:1;stroke:#999999;stroke-width:0.3;stroke-dasharray:none;stroke-opacity:1;marker-start:url(#Dot-53);marker-end:url(#ArrowTriangleStylized-73)"
d="m 125.96588,31.161768 c 2.11058,1.215401 2.51044,3.884348 0.47572,4.966673"
id="path82-7"
sodipodi:nodetypes="cc" />
@@ -1521,18 +1634,18 @@
y="70.585785">`</tspan></text>
</g>
<path
style="fill:none;fill-opacity:1;stroke:#000000;stroke-width:0.3;stroke-dasharray:none;stroke-opacity:1;marker-start:url(#Dot-53-8);marker-end:url(#ArrowTriangleStylized-73-5)"
style="fill:none;fill-opacity:1;stroke:#999999;stroke-width:0.3;stroke-dasharray:none;stroke-opacity:1;marker-start:url(#Dot-53-8);marker-end:url(#ArrowTriangleStylized-73-5)"
d="m 127.2604,21.039801 c 6.88076,0.06629 7.75197,16.194647 12.03682,16.034697"
id="path82-7-3"
sodipodi:nodetypes="cc"
transform="translate(0,-1.0583331)" />
<path
style="fill:none;fill-opacity:1;stroke:#000000;stroke-width:0.3;stroke-dasharray:none;stroke-opacity:1;marker-start:url(#Dot-53-8-6);marker-end:url(#ArrowTriangleStylized-73-5-4)"
style="fill:none;fill-opacity:1;stroke:#999999;stroke-width:0.3;stroke-dasharray:none;stroke-opacity:1;marker-start:url(#Dot-53-8-6);marker-end:url(#ArrowTriangleStylized-73-5-4)"
d="m 127.03416,70.482277 c 6.88076,0.06629 7.75197,16.194647 12.03682,16.034697"
id="path82-7-3-2"
sodipodi:nodetypes="cc" />
<path
style="fill:none;fill-opacity:1;stroke:#000000;stroke-width:0.3;stroke-dasharray:none;stroke-opacity:1;marker-start:url(#Dot-53-8-6-2);marker-end:url(#ArrowTriangleStylized-73-5-4-4)"
style="fill:none;fill-opacity:1;stroke:#808080;stroke-width:0.3;stroke-dasharray:none;stroke-opacity:1;marker-start:url(#Dot-53-8-6-2);marker-end:url(#ArrowTriangleStylized-73-5-4-4)"
d="m 126.20557,101.62208 c 6.88076,0.0663 14.40531,-1.62056 18.69016,-1.46061"
id="path82-7-3-2-0"
sodipodi:nodetypes="cc" />
@@ -1542,15 +1655,15 @@
id="path82-7-3-2-0-1"
sodipodi:nodetypes="cc" />
<path
style="fill:none;fill-opacity:1;stroke:#000000;stroke-width:0.3;stroke-dasharray:none;stroke-opacity:1;marker-start:url(#Dot-53-8-6-2-9);marker-end:url(#ArrowTriangleStylized-73-5-4-4-6)"
style="fill:none;fill-opacity:1;stroke:#808080;stroke-width:0.3;stroke-dasharray:none;stroke-opacity:1;marker-start:url(#Dot-53-8-6-2-9);marker-end:url(#ArrowTriangleStylized-73-5-4-4-6)"
d="m 126.29113,105.36025 c 6.88076,0.0663 32.52893,-4.33765 37.47791,-5.27457"
id="path82-7-3-2-0-9"
sodipodi:nodetypes="cc" />
<path
style="fill:none;fill-opacity:1;fill-rule:nonzero;stroke:#000000;stroke-width:0.265;stroke-dasharray:0.265, 0.265;stroke-dashoffset:0"
d="M 85.598933,89.444775 92.62402,14.544544"
d="m 85.598933,89.444775 c 0,0 2.803803,-21.595554 3.908493,-33.281557 C 90.76286,42.882565 92.62402,14.544544 92.62402,14.544544"
id="path66"
sodipodi:nodetypes="cc" />
sodipodi:nodetypes="csc" />
<path
style="fill:none;fill-opacity:1;fill-rule:nonzero;stroke:#000000;stroke-width:0.265;stroke-dasharray:0.265, 0.265;stroke-dashoffset:0"
d="M 85.595644,94.030394 92.557996,59.61732"
@@ -1650,7 +1763,7 @@
x="95.99482"
y="34.241806" />
<path
style="fill:none;fill-opacity:1;stroke:#000000;stroke-width:0.3;stroke-dasharray:none;stroke-opacity:1;marker-start:url(#Dot-53-0);marker-end:url(#ArrowTriangleStylized-73-3)"
style="fill:none;fill-opacity:1;stroke:#999999;stroke-width:0.3;stroke-dasharray:none;stroke-opacity:1;marker-start:url(#Dot-53-0);marker-end:url(#ArrowTriangleStylized-73-3)"
d="m 126.32282,31.434325 c 2.11058,1.215401 2.51044,3.884348 0.47572,4.966673"
id="path82-7-9"
sodipodi:nodetypes="cc" />
@@ -1694,14 +1807,14 @@
</g>
<path
style="fill:none;fill-opacity:1;fill-rule:nonzero;stroke:#000000;stroke-width:0.265;stroke-dasharray:0.265, 0.265;stroke-dashoffset:0"
d="m 85.610338,99.391985 7.030045,10.463595"
d="m 85.610338,99.391985 c 0,0 2.866911,2.131555 3.901307,3.554605 1.486458,2.04497 3.128738,6.90899 3.128738,6.90899"
id="path74"
sodipodi:nodetypes="cc" />
sodipodi:nodetypes="csc" />
<path
style="fill:none;fill-opacity:1;fill-rule:nonzero;stroke:#000000;stroke-width:0.265;stroke-dasharray:0.265, 0.265;stroke-dashoffset:0"
d="M 85.577922,95.104433 92.560701,64.925064"
d="m 85.577922,95.104433 c 0,0 3.079266,-6.983269 4.041374,-10.659382 1.666028,-6.365715 2.941405,-19.519987 2.941405,-19.519987"
id="path75"
sodipodi:nodetypes="cc" />
sodipodi:nodetypes="csc" />
<text
xml:space="preserve"
transform="matrix(0.26458333,0,0,0.26458333,129.48565,101.11509)"
Side by Side Swipe Overlay

Before

Width:  |  Height:  |  Size: 74 KiB

After

Width:  |  Height:  |  Size: 78 KiB

392
src/main.md Normal file
View File

@@ -0,0 +1,392 @@
::: center
**ABSTRACT**
:::
This paper proposes $\lambda_{mmm}$:a call-by-value simply-typed lambda calculus-based intermediate representation of programming languages for music that deal with synchronous signal processing, as well as a virtual machine and instruction set to run $\lambda_{mmm}$. Digital signal processing can be represented with a syntax that incorporates the internal states of delay and feedback into the lambda calculus. $\lambda_{mmm}$is defined as a superset of the lambda calculus, which allows users to construct a generative signal processing graph and its execution in an identical semantics. On the other hand, due to its specification, a problem was found that when dealing with higher-order functions, the users have to determine whether they are executed in the global environment evaluation or in the DSP execution, and a solution was proposed by introducing multi-stage computation.
# Introduction {#sec:intro}
A number of programming languages for sound and music have been developed to date, but not many have strongly formalised semantics. One language that is both rigorously formalised and practical is Faust[@Orlarey2004], which combines blocks with inputs and outputs with five primitive operations - parallel, sequential, split, merge and recursive connection. By having basic arithmetics and delay as a primitive block, any type of signal processing can be written in Faust. In a later extension, macros based on a term rewriting system has introduced that allows the higher abstraction of systems with an arbitrary number of inputs and outputs[@graf2010].
This strong abstraction capability through formalisation enables Faust to be translated to various backends, such as C++ and Rust. On the other hand, BDA lacks theoretical and practical compatibility with common programming languages: although it is possible to call external C functions in Faust, the assumption is basically pure function calls without memory allocation and deallocation. Therefore, while it is easy to embed Faust in another language, it is not easy to call another language from Faust.
In addition, macros in Faust are independent as a term rewriting system that generates BDA based on pattern matching. Therefore, even though the distinction between real and integer types does not exist in BDA, the arguments for pattern matching implicitly required to be an integer, which causes compile errors. This implicit typing rules are not intuitice for novice users.
Proposing a computational model for signal processing that is based on the more generic computational models, such as the lambda calculus has the potential to interoperate between many different general-purpose languages, and also facilitate the appropriation of existing optimisation methods and the implementation of compilers and run-time.
Currently, it has been proved that BDA can be converted to a general-purpose functional language in the form of using Arrows, a higher-level abstraction of monads[@gaster2018]. But higher-order functions on general-purpose functional languages are often implemented on the basis of dynamic memory allocation and release, which makes it difficult to use them in host languages for the real-time signal processing.
Also, Kronos[@norilo2015] and W-calculus[@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 *mimium* [@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).
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 $\lambda_{mmm}$, a superset of the 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. Lastly, a space for optimization for running mimium using $\lambda_{mmm}$will be discussed.
# Syntax {#sec:syntax}
<figure id="fig:syntax_v">
<table>
<tbody>
<tr class="odd">
<td style="text-align: center;"><span class="math display">$$\begin{aligned}
\tau_p ::= &amp;\; R\ &amp;[real] \\
\ | &amp;\; N\ &amp;[nat] \\
\tau ::= &amp;\; \tau_p\ &amp; \\
\ | &amp;\; \tau \to \tau \ &amp;[function] \\
% |&amp;\quad \langle \tau \rangle
\end{aligned}$$</span> <span class="roman">Types</span></td>
<td style="text-align: center;"><span class="math display">$$\begin{aligned}
v_p \; ::=&amp; \ r \quad r \in \mathbb{R} \\
|&amp; \ n \quad n \in \mathbb{N}\\
v \; ::=&amp;\ v_p \\
|&amp; \ cls(\lambda\ x.e, E) \\
%%|&amp; \quad (e_1,e_2) \quad &amp; [product]\\
%%|&amp; \quad \pi_n e \quad n\in \mathbb{N},\; n&gt;0 \quad &amp; [project]\\
%%|&amp; \quad \langle e \rangle \quad &amp; [code] \\
%%|&amp; \quad \textasciitilde e \quad &amp; [escape]
\end{aligned}$$</span> <span class="roman">Values</span></td>
</tr>
<tr class="even">
<td colspan="2" style="text-align: center;"><span class="math display">$$\begin{aligned}
e \; ::=&amp; \ x &amp;x \in {v_p} \ &amp; [value]\\
|&amp; \ \lambda x.e &amp; &amp; [lambda]\\
|&amp; \ let\; x = e_1\; in\; e_2 &amp; &amp; [let]\\
|&amp; \ fix \; x.e &amp; &amp; [fixpoint]\\
|&amp; \ e_1 \; e_2 &amp; &amp; [app]\\
|&amp; \ if\; (e_c)\; e_t\; else\; e_e \; &amp; &amp; [if] \\
|&amp; \ delay\; n \; e_1 \; e_2 &amp;n \in \mathbb{N}\ &amp; [delay]\\
|&amp; \ feed \; x.e &amp; &amp; [feed]\\
|&amp; ... &amp; &amp; \\
%%|&amp; \quad (e_1,e_2) \quad &amp; [product]\\
%%|&amp; \quad \pi_n e \quad n\in \mathbb{N},\; n&gt;0 \quad &amp; [project]\\
%%|&amp; \quad \langle e \rangle \quad &amp; [code] \\
%%|&amp; \quad \textasciitilde e \quad &amp; [escape]
\end{aligned}$$</span> <span class="roman">Terms</span></td>
</tr>
</tbody>
</table>
<figcaption><span id="fig:syntax_v" label="fig:syntax_v"></span><span><em>Definition of Types, Values and Terms of the <span class="math inline"><em>λ</em><sub><em>m</em><em>m</em><em>m</em></sub></span>(Basic arithmetics are omitted).</em></span></figcaption>
</figure>
Definition of types and terms of the $\lambda_{mmm}$ are shown in Figure [1](#fig:syntax_v){reference-type="ref" reference="fig:syntax_v"}.
Two terms are added in addition to the usual simply-typed lambda calculus, $delay e_1 e_2$ that refers a previous value of $e_1$ to $e_2$ sample before, and $feed x.e$ abstraction that the user can refer the result of the evaluation of the $e$ one unit time before as $x$ during the evaluation of $e$ itself.
## Syntactic sugar of the feedback expression in mimium {#sec:mimium}
``` {#lst:onepole .Rust float="" floatplacement="H" label="lst:onepole" language="Rust" caption="\\it Example of the code of one-pole filter in mimium."}
fn onepole(x,g){
x*(1.0-g) + self*g
}
```
mimium by the author has a keyword $self$ that can be used in function definition, that refers to the previous return value of the function. The example code of the simple one-pole filter function is shown in Listing [\[lst:onepole\]](#lst:onepole){reference-type="ref" reference="lst:onepole"}. This code can be expressed in $\lambda_{mmm}$ as Figure [2](#fig:onepole){reference-type="ref" reference="fig:onepole"}.
<figure id="fig:onepole">
<p><span class="math display">$$\centering
\begin{aligned}
let\ &amp; onepole = \\
&amp; \ \lambda x. \lambda g.\ feed\ y.\ x *(1.0 - g) + y * g \ in\ ...
\end{aligned}$$</span></p>
<figcaption><span id="fig:onepole" label="fig:onepole"></span><span><em>Equivalent expression to Listing <a href="#lst:onepole" data-reference-type="ref" data-reference="lst:onepole">[lst:onepole]</a> in <span class="math inline"><em>λ</em><sub><em>m</em><em>m</em><em>m</em></sub></span>.</em></span></figcaption>
</figure>
## Typing Rule {#sec:typing}
<figure id="fig:typing">
<table>
<tbody>
<tr class="odd">
<td style="text-align: center;"><span class="math display">$$\frac{\Gamma, x:\tau_a \vdash e:\tau_b}{\Gamma \vdash \lambda x.e:\tau_a \to \tau_b }$$</span><span class="roman">T-LAMBDA</span></td>
<td style="text-align: center;"><span class="math display">$$\frac{ \Gamma \vdash e_1:N \quad \Gamma \vdash e_2:\tau }{\Gamma \vdash delay\ e_1\ e_2 : \tau}$$</span><span class="roman">T-DELAY</span></td>
</tr>
<tr class="even">
<td style="text-align: center;"><span class="math display">$$\frac{\Gamma, x : \tau_p \vdash e: \tau_p }{\Gamma \vdash feed\ x.e:\tau_p}$$</span><span class="roman">T-FEED</span></td>
<td style="text-align: center;"><span class="math display">$$\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}$$</span><span class="roman">T-IF</span></td>
</tr>
</tbody>
</table>
<figcaption><span id="fig:typing" label="fig:typing"></span><span><em>Excerpt of the typing rules for <span class="math inline"><em>λ</em><sub><em>m</em><em>m</em><em>m</em></sub></span>.</em></span></figcaption>
</figure>
Additional typing rules to usual simply-typed lambda calculus are shown in Figure [3](#fig:typing){reference-type="ref" reference="fig:typing"}.
As primitive types, there are a real number type to used in most of signal processing and a natural number type that is used to indice of delay.
In the W-calculus, a starting point of designing $\lambda_{mmm}$, function types can takes tuples of real numbers and return tuples of real numbers. This means that higher-order functions cannot be written. While this restriction is reasonable as a design choice for a language for signal processing since higher-order functions require data structures that require dynamic memory allocation, such as closures, for their implementation, it also lacks the generality of the lambda calculus.
In $\lambda_{mmm}$, the problem of memory allocation for closures is left to the implementation of the runtime in the Section[4](#sec:vm){reference-type="ref" reference="sec:vm"}, and higher-order functions are allowed. However, the $feed$ abstraction does not allow function types as its input and output. Allowing the return of function types in the $feed$ abstraction means that it is possible to define functions whose processing contents change time-to-time. While this may be interesting theoritically, there are currently no practical cases in real-world signal processing, and it is expected to further complicate implementations.
# Semantics {#sec:semantics}
::: figure*
----------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- -------------------------------------------------------------------------------------------------------------------------------------------------------------- -----------------------------------------------------------------------------------------------------------------------------------------------------------------
$$\frac{E^n \vdash e_1 \Downarrow v_1 \ n>v_1 \ E^{n-v_1} \vdash e_2 \Downarrow v_2}{E^n \vdash\ delay\ n\ e_1\ e_2 \Downarrow v_2}$$[E-DELAY]{.roman} $$\frac{}{E^n \vdash\ \lambda x.e \Downarrow cls(\lambda x.e , E^n) }$$[E-LAM]{.roman} $$\frac{ E^{n-1} \vdash e \Downarrow v_1\ E^n, x \mapsto v_1 \vdash e \Downarrow v_2 }{E^n, x \mapsto v_2\ \vdash\ feed\ x\ e \Downarrow v_1}$$[E-FEED]{.roman}
$$\frac{E^n \vdash e_c \Downarrow n \quad n > 0\ E^n \vdash e_t\ \Downarrow v\ }{E^n \vdash\ if (e_c)\ e_t\ else\ e_t \Downarrow v }$$[E-IFTRUE]{.roman} $$\frac{E^n \vdash e_c \Downarrow n \quad n \leqq0\ E^n \vdash e_e\ \Downarrow v\ }{E^n \vdash\ if (e_c)\ e_t\ else\ e_t \Downarrow v }$$[E-IFFALSE]{.roman}  
$$\frac{E^n \vdash e_1 \Downarrow cls(\lambda x_c.e_c, E^n_c) E^n \vdash e_2 \Downarrow v_2\ E^n_c,\ x_c \mapsto v_2 \vdash e_c \Downarrow v }{E^n \vdash\ e_1\ e_2 \Downarrow v }$$[E-APP]{.roman}
----------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- -------------------------------------------------------------------------------------------------------------------------------------------------------------- -----------------------------------------------------------------------------------------------------------------------------------------------------------------
:::
The excerpt of operational semantics of the $\lambda_{mmm}$is shown in Figure [\[fig:semantics\]](#fig:semantics){reference-type="ref" reference="fig:semantics"}. This big-step semantics is a conceptual explanation of the evaluation that, when the current time is $n$, the previous evaluation environment $t$ samples before can be referred to as $E^{n-t}$ , and that when the time \< 0, the evaluation of any term is evaluated to the default value of its type (0 for the numeric types).
Of course, if we tried to execute this semantics in a straightforward manner, we would have to redo the calculation from time 0 to the current time every sample, with saving all the variable environments at each sample. In practice, therefore, a virtual machine is defined that takes into account the internal memory space used by delay and feed, and the $\lambda_{mmm}$terms are converted into instructions for that machine before execution.
# VM Model and Instruction Set {#sec:vm}
A model for the virtual machine and its instruction set to run\
$\lambda_{mmm}$is based on Lua 5.0[@ierusalimschy2005].
When executing a computational model based on lambda calculus, the problem is how to handle a data structure called a closure that captures the variable environment where the inner function is defined, to refer the outer variables from the inner function context. If the dictionary data of names and values of variables are paired with inner function, implementation of the compiler(intepreter) is simple, but run-time performance is limited.
On the contrary, a runtime performance can be improved by performing a process called closure transformation (or lambda lifting), which analyses all the names of outer variables referred by the inner function and transforms the inner function by adding argument so that the variables can be referred explicitly, but the compiler implementation of the transformation is relatively complex.
The Lua VM takes an intermediate approach between these two by adding the VM instructions `GETUPVALUE` /\
`SETUPVALUE`, which allows the outer variables to be referenced dynamically at runtime. The implementation of compiler and VM using *Upvalue* is simpler than closure conversion, while at the same time preventing execution performance degradation, as outer variables can be referenced via the call stack rather than on the heap memory unless the closure object escapes from the context of the original function[@nystrom2021].
Also, Upvalue helps interoperations between other programming languages, as Lua can be easily embedded through C language API and when implementing external libraries in C, programmer can access to upvalues of Lua Runtime not only the stack values in C API.
## Instruction Set {#sec:instruction}
VM Instructions for $\lambda_{mmm}$differs from Lua VM in the following respects.
1. Since mimium is a statically typed language unlike Lua, instructions for basic arithmetics are provided for each type.
2. The call operation is separated into the normal function call and the call of closure to handle higher-order statefull functions(See [4.2](#sec:vmstructure){reference-type="ref" reference="sec:vmstructure"} for details).
3. If statements are realised by a combination of two instructions, `JMP` and `JMPIFNEG`, whereas the Lua VM uses a dedicated `TEST` instruction.
4. Instructions related to for loop, the `SELF` instruction used for object-oriented programming and the `TABLE`-related instructions for metadata references to variables are omitted in mimium as they are not used.
5. Instructions related to list-related data structures are also omitted in this paper, as the implementation of data structures such as tuples and arrays was omitted in the description of the $\lambda_{mmm}$in this paper.
Instructions in $\lambda_{mmm}$VM are 32bit data with operation tag and 3 operands. Currently, a bit width for the tag and each operands are all 8 bit[^1].
The VM of $\lambda_{mmm}$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 the 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 operation.
The list of instructions is shown in Figure [\[fig:instruction\]](#fig:instruction){reference-type="ref" reference="fig:instruction"} (basic arithmetic operations are partly omitted). The notation for the instruction follows the Lua VM paper [@ierusalimschy2005 p.13]. From left to right, the name of operation, a list of operands, and pseudo-code of the operation. When using each of the three operands as unsigned 8 bits, they are denoted as `A B C`. When used with a signed integer, prefix `s` is added, and when the two operand fields are used as one 16 bits, an suffix `x` is added. For example, when B and C are merged and treated as signed 16 bits, they are denoted as `sBx`.
In pseudo-code describing an functionality, `R(A)` means that data is moved in and out through the register (call stack) according to the numerical value of the operand `A`. `K(A)` means that it retrieves the `A`-th number in the static variable field of the compiled programm. `U(A)` means that referring `A`-th Upvalue of the current function.
In addition to Lua's Upvalue operation, 4 operations related to internal state variables over time, `GETSTATE`, `SETSTATE`,\
`SHIFTSTATE` and `DELAY` are added.
::: figure*
` `
------------ ---------------------------------------------------------------------- -------------------------------------------------------------------------
MOVE A B R(A) := R(B)
MOVECONST A B R(A) := K(B)
GETUPVALUE A B R(A) := U(B)
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 := 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
ADDF A B C R(A) := R(B) as int + R(C) as in
  *\...Other basic arithmetics continues for each primitive types\...*
------------ ---------------------------------------------------------------------- -------------------------------------------------------------------------
:::
## Overview of the VM structure {#sec:vmstructure}
The overview of a data structure of the VM, program and the instantiated closure for $\lambda_{mmm}$is shown in Figure [\[fig:vmstructure\]](#fig:vmstructure){reference-type="ref" reference="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 `GETSTATE` / `SETSTATE` instructions. This position is modified by\
`SHIFTSTATE` operation. The the actual data in the state storage memory are statically layed out at compile time by analyzing function calls that include references to `self`, call of `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 given 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 instance itself. The VM switches the `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 ongoing execution. Because this offset value can be determined at compile time, stored in the function prototype in the program. For instance, if the Upvalue indexes in the program were `[4,3]`, `GETUPVALUE 6 1` means that, take `3` from the upvalue indexes and get value from `R(-2)` (3-5) over the base pointer and store it to `R(6)`.
When the closure escapes from the original function with\
`RETURN` instruction, inserted `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.
::: figure*
![image](lambdammm_vm_structure.pdf){width="\\hsize"}
:::
## Compilation to the VM instructions
``` {#lst:bytecodes_onepole float="" floatplacement="H" label="lst:bytecodes_onepole" caption="\\it Compiled VM instructions of one-pole filter example in Listing \\ref{lst:onepole}"}
CONSTANTS:[1.0]
fn onepole(x,g) state_size:1
MOVECONST 2 0 // load 1.0
MOVE 3 1 // load g
SUBF 2 2 3 // 1.0 - g
MOVE 3 0 // load x
MULF 2 2 3 // x * (1.0-g)
GETSTATE 3 // load self
MOVE 4 1 // load g
MULF 3 3 4 // self * g
ADDF 2 2 3 // compute result
GETSTATE 3 // prepare return value
SETSTATE 2 // store to self
RETURN 3 1
```
Listing [\[lst:bytecodes_onepole\]](#lst:bytecodes_onepole){reference-type="ref" reference="lst:bytecodes_onepole"} shows an basic example when the mimium code in Listing [\[lst:onepole\]](#lst:onepole){reference-type="ref" reference="lst:onepole"} is compiled into VM bytecode. When `self` is referenced, the value is obtained with the `GETSTATE` instruction, and the internal state is updated by storing the return value with the\
`SETSTATE` instruction before returning the value with `RETURN` from the function. Here, the actual return value is obtained by the second `GETSTATE` instruction in order to return the initial value of the internal state when time=0.
For example, when a time counter is written as `| | {self + 1}`, it is the compiler's design choice whether the return value of time=0 should be 0 or 1 though the latter does not strictly follow the semantics E-FEED in Figure [\[fig:semantics\]](#fig:semantics){reference-type="ref" reference="fig:semantics"}. If the design is to return 1 when time = 0, the second `GETSTATE` instruction can be removed and the value for the `RETURN` instruction should be `R(2)`.
A more complex example code and its expected bytecode instructions are shown in Listing [\[lst:fbdelay\]](#lst:fbdelay){reference-type="ref" reference="lst:fbdelay"} and Listing [\[lst:bytecodes_fbdelay\]](#lst:bytecodes_fbdelay){reference-type="ref" reference="lst:bytecodes_fbdelay"}. The codes define delay with a feedback as `fbdelay`, the other function `twodelay` uses two feedback delay with different parameters, and `dsp` finally uses two `twodelay` function.
Each after the referring to `self` through `GETSTATE` instruction, or call to the other statefull function,\
`SHIFTSTATE` instruction inserted to move the `StatePtr` forward to prepare the next non-closure function call. Before exits function, `StatePtr` is reset to the same position as that the current function context has begun by `SHIFTSTATE` (A sum of the operand for `SHIFTSTATE` in a function must be always 0).
``` {#lst:fbdelay .Rust float="" floatplacement="H" label="lst:fbdelay" language="Rust" caption="\\it Example code that combines self and delay without closure call."}
fn fbdelay(x,fb,dtime){
x + delay(1000,self,dtime)*fb
}
fn twodelay(x,dtime){
fbdelay(x,dtime,0.7)
+fbdelay(x,dtime*2,0.8)
}
fn dsp(x){
twodelay(x,400)+twodelay(x,800)
}
```
``` {#lst:bytecodes_fbdelay float="" floatplacement="H" label="lst:bytecodes_fbdelay" caption="\\it Compiled VM instructions of one-pole filter example in Listing \\ref{lst:fbdelay}"}
CONSTANTS:[0.7,2,0.8,400,800,0,1]
fn fbdelay(x,fb,dtime) state_size:2
MOVE 3 0
GETSTATE 4
SHIFTSTATE 1
DELAY 4 2
MOVE 5 1
MULF 4 4 5
ADDF 3 3 4
SHIFTSTATE -1
GETSTATE 4
SETSTATE 3
RETURN 4 1
fn twodelay(x,dtime) state_size:4
MOVECONST 2 5 //load "fbdelay" prototype
MOVE 3 0
MOVE 4 1
MOVECONST 5 0 //load 0.7
CALL 2 3 1
SHIFTSTATE 2 //=state_size of fbdelay
MOVECONST 3 5 //load "fbdelay" prototype
MOVE 4 0
MOVECONST 5 1 //load 2
MULF 4 4 5
MOVECONST 5 0 //load 0.7
CALL 3 3 1
ADDF 3 3 4
SHIFTSTATE -2
RETURN 3 1
fn dsp (x)
MOVECONST 1 6 //load "twodelay prototype"
MOVE 2 0
MOVECONST 3 3 //load 400
CALL 1 2 1
SHIFTSTATE 4 //=state_size of twodelay
MOVECONST 2 6
MOVE 2 3 //load "twodelay prototype"
MOVE 3 0
MOVECONST 3 4 //load 400
CALL 2 2 1
ADD 1 1 2
SHIFTSTATE -4
RETURN 1 1
```
# Discussion : Different behaviour depending on the position of let binding {#sec:discussion}
Because mimium treats functions that have internal states which change over time, when higher-order functions are used, there is a counterintuitive behavior compared to general functional programming languages.
An example is the higher-order function `filterbank`, which duplicates `filter` function `N` times parametrically, and adds them together. Listing [\[lst:filterbank_bad\]](#lst:filterbank_bad){reference-type="ref" reference="lst:filterbank_bad"} is an example of an incorrect code, and Listing [\[lst:filterbank_good\]](#lst:filterbank_good){reference-type="ref" reference="lst:filterbank_good"} is an example of the code that behave correctly. The difference between Listing [\[lst:filterbank_bad\]](#lst:filterbank_bad){reference-type="ref" reference="lst:filterbank_bad"} and Listing [\[lst:filterbank_good\]](#lst:filterbank_good){reference-type="ref" reference="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 `let` binding out of the inner function[^2]. Similarly, in the `dsp` function that will be called by the audio driver in mimium, the difference is whether the filterbank function is executed inside `dsp` or bound with `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 [\[lst:filterbank_good\]](#lst:filterbank_good){reference-type="ref" reference="lst:filterbank_good"} to Listing [\[lst:filterbank_bad\]](#lst:filterbank_bad){reference-type="ref" reference="lst:filterbank_bad"}.
But in mimium, there are two major stages of evaluation, 0: the code is evaluated in the global environment (concretizing the signal processing graph) at first, and 1: 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 `filterbank` function is performed only once in Listing [\[lst:filterbank_good\]](#lst:filterbank_good){reference-type="ref" reference="lst:filterbank_good"} for the evaluation of the global environment, whereas in Listing [\[lst:filterbank_bad\]](#lst:filterbank_bad){reference-type="ref" reference="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[\[lst:filterbank_bad\]](#lst:filterbank_bad){reference-type="ref" reference="lst:filterbank_bad"}, the internal state of the closure after the evaluation of `filterbank` is reset at each time step.
``` {#lst:filterbank_bad .Rust float="" floatplacement="H" label="lst:filterbank_bad" language="Rust" caption="\\it Wrong example of the code that duplicate filter parametrically."}
fn bandpass(x,freq){
//...
}
fn filterbank(n,filter){
if (n>0){
|x,freq| filter(x,freq+n*100)
+ filterbank(n-1,filter)(x,freq)
}else{
0
}
}
fn dsp(){ //called by audio driver.
filterbank(3,bandpass)
}
```
``` {#lst:filterbank_good .Rust float="" floatplacement="H" label="lst:filterbank_good" language="Rust" caption="\\it Corrected example of the code that duplicate filter parametrically."}
fn filterbank(n,filter){
let next = filterbank(n-1,filter)
if (n>0){
|x,freq| filter(x,freq+n*100)
+ next(x,freq)
}else{
0
}
}
let myfilter = filterbank(3,bandpass)
fn dsp(){
myfilter(x,1000)
}
```
``` {#lst:filterbank_multi .Rust float="" floatplacement="H" label="lst:filterbank_multi" language="Rust" caption="\\it Example of filterbank function using multi-stage computation in a future specification of mimium."}
fn filterbank(n,filter){
.< if (n>0){
|x,freq| filter(x,freq+n*100)
+ ~filterbank(n-1,filter)(x,freq)
}else{
0
} >.
}
fn dsp(){
~filterbank(3,bandpass) (x,1000)
}
```
This means that the major compiler optimization techniques such as the constant folding and the function inlining can not simply be appropriated. Those optimizations should be done after the evaluation of a global context and before evaluating `dsp` function.
To solve this situation, introducing distinction whether the term should be used in global context evaluation(Stage 0) and in the actual signal processing(stage 1) in type system. This can be realized with Multi-Stage Computation[@Taha1997]. Listing [\[lst:filterbank_multi\]](#lst:filterbank_multi){reference-type="ref" reference="lst:filterbank_multi"} is the example of `filterbank` code using BER MetaOCaml's syntaxes `.<term>.` which will generate evaluated program used in a next stage, and `~term` which embed terms evaluated at the previous stage[@kiselyov2014a].
`filterbank` function is evaluated in stage 0 while embedding itself by using `~`.
This multi-stage computation code has a same semantics in a generative signal graph generation and execution of the signal processing, in contrast to that Faust have 2 different semantics of the term rewriting macro and BDA.
# Conclusion
[\[sec:conclusion\]](#sec:conclusion){reference-type="ref" reference="sec:conclusion"}
This paper proposed $\lambda_{mmm}$, an intermediate representation for the programming languages for music and signal processing with the virtual machine and instruction set to run it. $\lambda_{mmm}$enables to describe generative signal graph and its contents in a single syntax and semantics. However, user have to be responsible to write codes that does not create escapable closures during the dsp execution and this problem would be difficult to understand by novice users.
# Acknowledgments
This work was supported by JSPS KAKENHI (Grant No.\
JP19K21615). Also great thanks for many anonymous reviewers.
[^1]: Reason for this is that it is easy to implemented on `enum` data structure on Rust, a host language of the latest mimium compiler. Operands bitwidth and alignment may be changed in the future.
[^2]: In the previous specification of mimium in [@matsuura2021a], the binding of new variable and destructive assignment were the same syntax(`x = a`) but the syntax for the variable binding has changed to use `let` keyword.

BIN
src/main.pdf Normal file
View File

Binary file not shown.

295
src/main.tex
View File

@@ -184,29 +184,31 @@
\maketitle
\begin{abstract}
This paper proposes \lambdammm : a call-by-value simply-typed lambda calculus-based intermediate representation of programming languages for music that deal with synchronous signal processing, as well as a virtual machine and instruction set to run \lambdammm . Digital signal processing can be represented with a syntax that incorporates the internal states of delay and feedback into the lambda calculus. \lambdammm is a superset of the lambda calculus, which allows users to construct a generative signal processing graph and its execution in identical semantics. On the other hand, due to its specification, a problem was found that when dealing with higher-order functions, the users have to determine whether the execution is in the global environment evaluation or the DSP execution, and it is implied that the multi-stage computation would solve the issue.
This paper proposes \lambdammm : a call-by-value simply-typed lambda calculus-based intermediate representation of a programming language for music that deal with synchronous signal processing, as well as a virtual machine and instruction set to run \lambdammm . Digital signal processing can be represented with a syntax that incorporates the internal states of delay and feedback into the lambda calculus. \lambdammm\ is a superset of the lambda calculus, which allows users to construct a generative signal processing graph and its execution in identical semantics. On the other hand, due to its specification, a problem was found that when dealing with higher-order functions, the users have to determine whether the execution is in the global environment evaluation or the DSP execution, and it is implied that the multi-stage computation can solve the issue.
\end{abstract}
\section{Introduction}
\label{sec:intro}
Many programming languages for sound and music have been developed, but only a few have strongly formalized semantics. One language that is both rigorously formalized and practical is Faust\cite{Orlarey2004}, which combines blocks with inputs and outputs with five primitive operations - parallel, sequential, split, mergem and recursive connection. By having basic arithmetics and delay as a primitive block, any type of signal processing can be written in Faust. In a later extension, a macro based on a term rewriting system has been introduced, allowing the higher abstraction of systems with an arbitrary number of inputs and outputs\cite{graf2010}.
Many programming languages for sound and music have been developed, but only a few have strongly formalized semantics. One language that is both rigorously formalized and practical is Faust\cite{Orlarey2004}, which combines blocks with inputs and outputs with five primitive operations - parallel, sequential, split, merge, and recursive connection. By having basic arithmetics, conditional and delay as primitive blocks, any type of signal processing can be written in Faust. In a later extension, a macro based on a term rewriting system has been introduced, allowing users to parameterize blocks with an arbitrary number of inputs and outputs\cite{graf2010}.
This strong abstraction capability through formalization enables Faust to be translated to various backends, such as C++ and Rust. On the other hand, BDA lacks theoretical and practical compatibility with common programming languages. Although it is possible to call external C functions in Faust, those functions are assumed to be pure functions without a heap memory allocation and deallocation. Therefore, while it is easy to embed Faust in another language, it is not easy to call another language from Faust.
This strong abstraction capability through formalization enables Faust to be translated to various backends, such as C, C++, Rust and LLVM IR. On the other hand, BDA lacks theoretical and practical compatibility with common programming languages. Although it is possible to call external C functions in Faust, those functions are assumed to be pure functions without a heap memory allocation and deallocation. Therefore, while it is easy to embed Faust in another language, it is not easy to call another language from Faust.
In addition, macros in Faust are independent as a term rewriting system that generates BDA based on pattern matching. Therefore, even though the distinction between real and integer types does not exist in BDA, the arguments for pattern matching are implicitly required to be an integer, which causes compile errors. These implicit typing rules are not intuitive for novice users.
In addition, a macro for Faust is an independent term rewriting system that generates BDA based on a pattern matching. Therefore, the arguments for pattern matching are implicitly required to be an integer, which sometimes causes compile errors despite the distinction between real and integer types does not exist in BDA. These implicit typing rules are not intuitive for novice users.
Proposing a computational model for signal processing based on the more generic computational models, such as the lambda calculus has the potential to interoperate between many different general-purpose languages, and also facilitate the appropriation of existing optimisation methods and the implementation of compilers and run-time.
Proposing a computational model for signal processing based on the more generic computational models, such as a lambda calculus has the potential to interoperate between many different general purpose languages on run-time, and also facilitate the appropriation of existing optimization methods and the implementation of compilers and run-time.
Currently, it has been proved that BDA can be converted to a general-purpose functional language in the form of using Arrows, a higher-level abstraction of monads\cite{gaster2018}. However, higher-order functions on general-purpose functional languages are often implemented on the basis of dynamic memory allocation and release, which makes it difficult to use them in host languages for real-time signal processing.
Currently, it has been proved that BDA can be converted to a general-purpose functional language in the form of using arrow, a higher-level abstraction of monads\cite{gaster2018}. However, higher-order functions on general-purpose functional languages are often implemented on the basis of dynamic memory allocation and release, which makes it difficult to use them in host languages for real-time signal processing.
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 linearity and identity of graph topologies.
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 variation of lambda calculus in which the type itself can be abstractized (a function that takes the type as an input and returns a new type can be defined). In Kronos, a calculation of type corresponds to the signal graph generation and a calculation of value corresponds to the actual processing. A special primitive operation is only delay in Kronos, and the feedback routing can be represented as a recursive function application in a calculation of types.
Previously, the author designed a programming language for music \textit{mimium} \cite{matsuura2021a}. By adding basic operations of delay and feedback to lambda calculus, signal processing can be concisely expressed 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).
The W-calculus has feedback operation as a primitive, along with the access to the value of the variable in the past(= delay). W-calculus limits the systems so that can represents to linear-time-invariant such as filters and reverbrators and defines a more formal semantics, aiming at automatic proofs of the linearity and identity of graph topologies.
One of the previous issues with mimium was the inability to compile the codes, which contain a combination of recursive or higher-order functions and stateful functions because the compiler could not determine the data size of the internal state of the signal processing.
Previously, the author designed a programming language for music \textit{mimium} \cite{matsuura2021a}. By adding basic operations of delay and feedback to lambda calculus, signal processing can be concisely expressed 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, I propose the syntax and semantics of \lambdammm, a superset of the call-by-value simply-typed lambda calculus, as a computation model that is supposed to be an intermediate representation of mimium. Also, I propose a virtual machine and its instruction set to execute this computation model practically. Lastly, I discuss a space for optimization for running mimium using \lambdammm.
One of the previous issues with mimium was the inability to compile the codes, which contain a combination of recursive or higher-order functions with stateful functions that contains delay or feedback because the compiler could not determine the data size of the internal state of the signal processing.
In this paper, I propose a syntax and semantics of \lambdammm, an extended call-by-value simply-typed lambda calculus, as a computation model that is supposed to be an intermediate representation for mimium. Also, I propose a virtual machine and its instruction set based on Lua's VM, to execute this computation model practically. Lastly, I discuss the problem and the potential, one that the current \lambdammm\ that users have to care whether the calculation happens in a global context or an acutal signal processing, another that the run-time interoperation between the other programming languages can be easier than the existing DSP languages.
\section{Syntax}
@@ -214,21 +216,21 @@ In this paper, I propose the syntax and semantics of \lambdammm, a superset of t
\input{syntax.tex}
Definition of types and terms of the \lambdammm are shown in Figure \ref{fig:syntax_v}.
Definition of types and terms of the \lambdammm\ are shown in Figure \ref{fig:syntax_v}.
Two terms are added in addition to the usual simply-typed lambda calculus, $delay e_1 e_2 $ that refers a previous value of $e_1$ to $e_2$ sample before, and $feed x.e$ abstraction that the user can refer the result of the evaluation of the $e$ one unit time before as $x$ during the evaluation of $e$ itself.
Two terms are added in addition to the usual simply-typed lambda calculus, $delay\ n\ e_1\ e_2 $ that refers a previous value of $e_1$ to $e_2$ sample before (with maximum delay value $n$ to limit memory size to finite), and $feed\ x.e$ abstraction that the user can refer the result of the evaluation of the $e$ one unit time before as $x$ during the evaluation of $e$ itself.
\subsection{Syntactic sugar of the feedback expression in mimium}
\label{sec:mimium}
mimium by the author has a keyword $self$ that can be used in function definition, that refers to the previous return value of the function. The example code of the simple one-pole filter function that mixes input and last output signal so as to a sum of gains of input and feedback should be 1, is shown in Listing \ref{lst:onepole}. This code can be expressed in \lambdammm\ as Figure \ref{fig:onepole}.
\begin{lstlisting}[float,floatplacement=H,label=lst:onepole,language=Rust,caption=\it Example of the code of one-pole filter in mimium.]
fn onepole(x,g){
x*(1.0-g) + self*g
}
\end{lstlisting}
mimium by the author has a keyword $self$ that can be used in function definition, that refers to the previous return value of the function. The example code of the simple one-pole filter function is shown in Listing \ref{lst:onepole}. This code can be expressed in $\lambda_{mmm}$ as Figure \ref{fig:onepole}.
\begin{figure}[ht]
\begin{equation*}
\centering
@@ -247,60 +249,58 @@ mimium by the author has a keyword $self$ that can be used in function definitio
Additional typing rules to usual simply-typed lambda calculus are shown in Figure \ref{fig:typing}.
As primitive types, there are a real number type to used in most of signal processing and a natural number type that is used to indice of delay.
In the W-calculus, a starting point of designing \lambdammm, function types can takes tuples of real numbers and return tuples of real numbers. This means that higher-order functions cannot be written. While this restriction is reasonable as a design choice for a language for signal processing since higher-order functions require data structures that require dynamic memory allocation, such as closures, for their implementation, it also lacks the generality of the lambda calculus.
In \lambdammm, the problem of memory allocation for closures is left to the implementation of the runtime in the Section\ref{sec:vm}, and higher-order functions are allowed. However, the $feed$ abstraction does not allow function types as its input and output. Allowing the return of function types in the $feed$ abstraction means that it is possible to define functions whose processing contents change time-to-time. While this may be interesting theoritically, there are currently no practical cases in real-world signal processing, and it is expected to further complicate implementations.
As primitive types, there are a real number type to used in most of signal processing and a natural number type that is used for the indice of delay.
In the W-calculus, which is a direct inspiration to designing \lambdammm, function types can takes only tuples of real numbers and return tuples of real numbers. This means that higher-order functions cannot be written. While this restriction is reasonable as a design choice for a language for signal processing since higher-order functions require data structures that require dynamic memory allocation, such as closures, for their implementation, it also lacks the generality of the lambda calculus.
In \lambdammm, the problem of memory allocation for closures is left to the implementation of the runtime in the Section\ref{sec:vm}, and higher-order functions are allowed. However, the $feed$ abstraction does not allow function types as its input and output. Allowing the return of function types in the $feed$ abstraction means that it is possible to define functions whose processing contents may change time-to-time. While this may be interesting theoritically, there are currently no practical cases in real-world signal processing, and it is expected to further complicate implementations.
\section{Semantics}
\label{sec:semantics}
\input{semantics.tex}
The excerpt of operational semantics of the \lambdammm is shown in Figure \ref{fig:semantics}. This big-step semantics is a conceptual explanation of the evaluation that, when the current time is $n$, the previous evaluation environment $t$ samples before can be referred to as $E^{n-t}$ , and that when the time < 0, the evaluation of any term is evaluated to the default value of its type (0 for the numeric types).
The excerpt of operational semantics of the \lambdammm\ is shown in Figure \ref{fig:semantics}. This big-step semantics is a conceptual explanation of the evaluation that, when the current time is $n$, the previous evaluation environment $t$ samples before can be referred to as $E^{n-t}$ , and that when the time < 0, the evaluation of any term is evaluated to the default value of its type (0 for the numeric types).
Of course, if we tried to execute this semantics in a straightforward manner, we would have to redo the calculation from time 0 to the current time every sample, with saving all the variable environments at each sample. In practice, therefore, a virtual machine is defined that takes into account the internal memory space used by $delay$ and $feed$, and the \lambdammm terms are converted into instructions for that machine before execution.
Of course, if we tried to execute this semantics in a straightforward manner, we would have to redo the calculation from time 0 to the current time every sample, with saving all the variable environments at each sample. In practice, therefore, a virtual machine is defined that takes into account the internal memory space used by $delay$ and $feed$, and the \lambdammm\ terms are converted into instructions for that machine before execution.
\section{VM Model and Instruction Set}
\label{sec:vm}
A model for the virtual machine and its instruction set to run \\ \lambdammm is based on Lua 5.0\cite{ierusalimschy2005}.
A model for the virtual machine and its instruction set to run \\ \lambdammm\ is based on the VM for Lua version 5\cite{ierusalimschy2005}.
When executing a computational model based on lambda calculus, the problem is how to handle a data structure called a closure that captures the variable environment where the inner function is defined, to refer the outer variables from the inner function context. If the dictionary data of names and values of variables are paired with inner function, implementation of the compiler(intepreter) is simple, but run-time performance is limited.
When executing a computational model based on lambda calculus, the problem is how to handle a data structure called a closure that captures the variable environment where the inner function is defined, to refer the outer variables from the inner function context. If the dictionary data of names and values of variables are paired with inner function, implementation of the compiler (intepreter) is simple, but run-time performance is limited.
On the contrary, a runtime performance can be improved by performing a process called closure transformation (or lambda lifting), which analyses all the names of outer variables referred by the inner function and transforms the inner function by adding argument so that the variables can be referred explicitly, but the compiler implementation of the transformation is relatively complex.
The Lua VM takes an intermediate approach between these two by adding the VM instructions \texttt{GETUPVALUE} / \\ \texttt{SETUPVALUE}, which allows the outer variables to be referenced dynamically at runtime. The implementation of compiler and VM using \textit{Upvalue} is simpler than closure conversion, while at the same time preventing execution performance degradation, as outer variables can be referenced via the call stack rather than on the heap memory unless the closure object escapes from the context of the original function\cite{nystrom2021}.
The Lua VM takes an intermediate approach between these two by adding the VM instructions \texttt{GETUPVALUE} / \\ \texttt{SETUPVALUE}, which allows the outer variables to be referred dynamically at runtime. The implementation of compiler and VM using \textit{upvalue} is simpler than closure conversion, while at the same time preventing execution performance degradation, as outer variables can be referred via the call stack rather than on the heap memory unless the closure object escapes from the context of the original function\cite{nystrom2021}.
Also, Upvalue helps interoperations between other programming languages, as Lua can be easily embedded through C language API and when implementing external libraries in C, programmer can access to upvalues of Lua Runtime not only the stack values in C API.
Also, upvalue helps interoperations between other programming languages, as Lua can be easily embedded through C language API and when implementing external libraries in C, programmer can access to upvalues of Lua Runtime not only the stack values in C API.
\subsection{Instruction Set}
\label{sec:instruction}
VM Instructions for \lambdammm differs from Lua VM in the following respects.
VM Instructions for \lambdammm\ differs from the Lua VM in the following respects.
\begin{enumerate}
\item{Since mimium is a statically typed language unlike Lua, instructions for basic arithmetics are provided for each type.}
\item{The call operation is separated into the normal function call and the call of closure to handle higher-order statefull functions(See \ref{sec:vmstructure} for details). }
\item{If statements are realised by a combination of two instructions, \texttt{JMP} and \texttt{JMPIFNEG}, whereas the Lua VM uses a dedicated \texttt{TEST} instruction.}
\item{The call operation is separated into the normal function call and the call of closure due to its static typing similarly, and also to handle higher-order statefull functions(See \ref{sec:vmstructure} for details). }
\item{If statements are realised by a combination of two instructions, \texttt{JMP} and \texttt{JMPIFNEG}, whereas the Lua VM uses a dedicated \texttt{TEST} instructions.}
\item{Instructions related to for loop, the \texttt{SELF} instruction used for object-oriented programming and the \texttt{TABLE}-related instructions for metadata references to variables are omitted in mimium as they are not used.}
\item{Instructions related to list-related data structures are also omitted in this paper, as the implementation of data structures such as tuples and arrays was omitted in the description of the \lambdammm in this paper.}
\item{Instructions related to list-related data structures are also omitted in this paper, as the implementation of data structures such as tuples and arrays was omitted in the description of the \lambdammm\ in this paper.}
\end{enumerate}
Instructions in \lambdammm VM are 32bit data with operation tag and 3 operands. Currently, a bit width for the tag and each operands are all 8 bit\footnote[1]{Reason for this is that it is easy to implemented on \texttt{enum} data structure on Rust, a host language of the latest mimium compiler. Operands bitwidth and alignment may be changed in the future.}.
Instructions in \lambdammm\ VM are 32bit data with operation tag and 3 operands. Currently, a bit width for the tag and each operands are all 8 bit\footnote[1]{Reason for this is that it is easy to implemented on \texttt{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 the 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 operation.
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 the 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 operation.
The list of instructions is shown in Figure \ref{fig:instruction} (basic arithmetic operations are partly omitted). The notation for the instruction follows the Lua VM paper \cite[p.13]{ierusalimschy2005}. From left to right, the name of operation, a list of operands, and pseudo-code of the operation. When using each of the three operands as unsigned 8 bits, they are denoted as \texttt{A B C}. When used with a signed integer, prefix \texttt{s} is added, and when the two operand fields are used as one 16 bits, an suffix \texttt{x} is added. For example, when B and C are merged and treated as signed 16 bits, they are denoted as \texttt{sBx}.
In pseudo-code describing an functionality, \texttt{R(A)} means that data is moved in and out through the register (call stack) according to the numerical value of the operand \texttt{A}. \texttt{K(A)} means that it retrieves the \texttt{A}-th number in the static variable field of the compiled programm. \texttt{U(A)} means that referring \texttt{A}-th Upvalue of the current function.
In pseudo-code describing an functionality, \texttt{R(A)} means that data is moved in and out through the register (call stack) at the point of base pointer for current function + \texttt{A}. \texttt{K(A)} means that it retrieves the \texttt{A}-th number in the static variable field of the compiled program. \texttt{U(A)} means that referring \texttt{A}-th upvalue of the current function.
In addition to Lua's Upvalue operation, 4 operations related to internal state variables over time, \texttt{GETSTATE}, \texttt{SETSTATE}, \\ \texttt{SHIFTSTATE} and \texttt{DELAY} are added.
In addition to Lua's Upvalue operation, 4 operations related to internal state variables over time, \texttt{GETSTATE}, \texttt{SETSTATE}, \\ \texttt{SHIFTSTATE} and \texttt{DELAY} are added to compile $delay$ and $feed$ expressions.
\begin{figure*}[ht]
\tt
@@ -309,17 +309,25 @@ In addition to Lua's Upvalue operation, 4 operations related to internal state v
MOVE & A B & R(A) := R(B) \\
MOVECONST & A B & R(A) := K(B) \\
GETUPVALUE & A B & R(A) := U(B) \\
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)) \\
\multicolumn{3}{l}{
\textit{(SETUPVALUE does not exist)}
}\\
GETSTATE* & A & R(A) := SPtr[SPos] \\
SETSTATE* & A & SPtr[SPos] := R(A) \\
SHIFTSTATE* & sAx & SPos += sAx \\
DELAY* & A B C & R(A) := update\_ringbuffer(SPtr[SPos],R(B),R(C)) \\
\multicolumn{3}{l}{
\textit{ *((SPos,SPtr)= vm.closures[vm.statepos\_stack.top()].state }
}\\
\multicolumn{3}{l}{
\textit{\quad if vm.statepos\_stack is empty, use global state storage.)}
}\\
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 \\
CALLCLS & A B C & vm.statepos\_stack.push(R(A)) \\
\ & \ & R(A),...,R(A+C-2) := vm.closures[R(A)].fnproto(R(A+1),...,R(A+B-1)) \\
\ & \ & Sptr := vm.global\_sptr \\
\ & \ & vm.statepos\_stack.pop() \\
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)\\
@@ -328,7 +336,7 @@ 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\\
ADDF & A B C & R(A) := R(B) as int + R(C) as in \\
ADDI & A B C & R(A) := R(B) as int + R(C) as int \\
\ &
\multicolumn{2}{l}{
\textit{...Other basic arithmetics continues for each primitive types...}
@@ -340,15 +348,19 @@ ADDF & A B C & R(A) := R(B) as int + R(C) as in \\
\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 Figure \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.
The overview of a data structure of the virtual machine, the program and the instantiated closure for \lambdammm\ is shown in Figure \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 state storage memory are statically layed out at compile time by analyzing function calls that include references to \texttt{self}, call of \texttt{delay} and the functions which will call such statefull functions recursively.
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 back and forth. The actual data in the state storage memory are statically layed out at compile time by analyzing function calls that include references to \texttt{self}, call of \texttt{delay} and the functions which will call such statefull functions recursively. \texttt{DELAY} operation takes 2 inputs, B for an input and C for the delay time in samples.
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 given 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 instance 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.
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 given 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 instance itself. The VM have an another stack to keep the pointer to state storage. Each time \texttt{CALLCLS} used, VM pushes a pointer to the state storage of instantiated closure to the state stack and, at the end of the closure call, VM pops out the state pointer from the stack.
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 ongoing execution. Because this offset value can be determined at compile time, stored in the function prototype in the program. For instance, if the Upvalue indexes in the program were \texttt{[4,3]}, \texttt{GETUPVALUE 6 1} means that, take \texttt{3} from the upvalue indexes and get value from \texttt{R(-2)} (3-5) over the base pointer and store it to \texttt{R(6)}.
Instantiated closures also hold the storage area of upvalues. Until the closure exits the context of parent function (such a closure is called "Open Closure"), upvalues holds a negative offset on the stack at the ongoing execution. This offset value can be determined at compile time, the offset is stored in the function prototype in the program. Also, not only local variables, upvalue may refer to parent funtion's upvalue (this situation can happens when at least 3 functions are nested). So the array of upvalue indexes in the function prototype holds a pair of tag whether it is local stack value or further upvalue and its index (negative offset of stack or parent function's upvalue index).
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.
For instance, if the Upvalue indexes in the program were like \texttt{[upvalue(1),local(3)]}, \texttt{GETUPVALUE 6 1} means that, take \texttt{3} from the upvalue indexes 1 and get value from \texttt{R(-3)} over the base pointer and store it to \texttt{R(6)}.
When the closure escapes from the original function with \\ \texttt{RETURN} instruction, inserted \texttt{CLOSE} instruction \\ the \texttt{RETURN} instruction moves actual upvalues from the stack into somewhere on the heap memory. This upvalues may be referred from multiple locations when using nested closures, and some form of garbage collection needed to free memory after they are no longer referred.
In the current specification, the paradigm is call-by-value and reassignment expression does not exist, therefore, \texttt{SETUPVALUE} instruction does not exist in \lambdammm\ VM. This difference also make a difference to the implemention of open upvalue in the closure because the open upvalue should be shared memory cell which maybe recursively converted into memory cell of closed value when the \texttt{CLOSE} instruction is called.
\begin{figure*}[ht]
\centerline{\includegraphics[width=\hsize]{lambdammm_vm_structure}}
@@ -358,30 +370,31 @@ When the closure escapes from the original function with \\ \texttt{RETURN} inst
\subsection{Compilation to the VM instructions}
\begin{lstlisting}[float,floatplacement=H,label=lst:bytecodes_onepole,caption=\it Compiled VM instructions of one-pole filter example in Listing \ref{lst:onepole}]
CONSTANTS:[1.0]
fn onepole(x,g) state_size:1
MOVECONST 2 0 // load 1.0
MOVE 3 1 // load g
SUBF 2 2 3 // 1.0 - g
MOVE 3 0 // load x
MULF 2 2 3 // x * (1.0-g)
GETSTATE 3 // load self
MOVE 4 1 // load g
MULF 3 3 4 // self * g
ADDF 2 2 3 // compute result
GETSTATE 3 // prepare return value
SETSTATE 2 // store to self
RETURN 3 1
CONSTANTS:[1.0]
fn onepole(x,g) state_size:1
MOVECONST 2 0 // load 1.0
MOVE 3 1 // load g
SUBF 2 2 3 // 1.0 - g
MOVE 3 0 // load x
MULF 2 2 3 // x * (1.0-g)
GETSTATE 3 // load self
MOVE 4 1 // load g
MULF 3 3 4 // self * g
ADDF 2 2 3 // compute result
GETSTATE 3 // prepare return value
SETSTATE 2 // store to self
RETURN 3 1
\end{lstlisting}
Listing \ref{lst:bytecodes_onepole} shows an basic example when the mimium code in Listing \ref{lst:onepole} is compiled into VM bytecode. When \texttt{self} is referenced, the value is obtained with the \texttt{GETSTATE} instruction, and the internal state is updated by storing the return value with the \\ \texttt{SETSTATE} instruction before returning the value with \texttt{RETURN} from the function. Here, the actual return value is obtained by the second \texttt{GETSTATE} instruction in order to return the initial value of the internal state when time=0.
Listing \ref{lst:bytecodes_onepole} shows an basic example when the mimium code in Listing \ref{lst:onepole} is compiled into VM bytecode. When \texttt{self} is referred, the value is obtained with the \texttt{GETSTATE} instruction, and the internal state is updated by storing the return value with the \\ \texttt{SETSTATE} instruction before returning the value with \texttt{RETURN} from the function. Here, the actual return value is obtained by the second \texttt{GETSTATE} instruction in order to return the initial value of the internal state when time=0.
For example, when a time counter is written as \texttt{| | \{self + 1\}}, it is the compiler's design choice whether the return value of time=0 should be 0 or 1 though the latter does not strictly follow the semantics E-FEED in Figure \ref{fig:semantics}. If the design is to return 1 when time = 0, the second \texttt{GETSTATE} instruction can be removed and the value for the \texttt{RETURN} instruction should be \texttt{R(2)}.
A more complex example code and its expected bytecode instructions are shown in Listing \ref{lst:fbdelay} and Listing \ref{lst:bytecodes_fbdelay}. The codes define delay with a feedback as \texttt{fbdelay}, the other function \texttt{twodelay} uses two feedback delay with different parameters, and \texttt{dsp} finally uses two \texttt{twodelay} function.
Each after the referring to \texttt{self} through \texttt{GETSTATE} instruction, or call to the other statefull function, \\ \texttt{SHIFTSTATE} instruction inserted to move the \texttt{StatePtr} forward to prepare the next non-closure function call. Before exits function, \texttt{StatePtr} is reset to the same position as that the current function context has begun by \texttt{SHIFTSTATE} (A sum of the operand for \texttt{SHIFTSTATE} in a function must be always 0).
Each after the referring to \texttt{self} through \texttt{GETSTATE} instruction, or call to the other statefull function, \\ \texttt{SHIFTSTATE} instruction inserted to move the position of state storage forward to prepare the next non-closure function call. Before exiting function, the state position is reset to the same position as that the current function context has begun by \texttt{SHIFTSTATE} (A sum of the operand for \texttt{SHIFTSTATE} in a function must be always 0). Figure \ref{fig:fbdelay_spos} shows how the state position moves by \texttt{SHIFTSTATE} operations during the execution of \texttt{twodelay} function.
By describing an internal state as a relative position in the state storage, the state data can be expressed as a flat array, which makes the implementation of the compiler simple, not like a tree structure that need to analyze a call tree from the root to generate as in the previous implementation of mimium. This is similar to upvalue makes the implementation of the compiler simpler by describing free variables as relative positions on the call stack.
\begin{lstlisting}[float,floatplacement=H,label=lst:fbdelay,language=Rust,caption=\it Example code that combines self and delay without closure call.]
fn fbdelay(x,fb,dtime){
@@ -396,20 +409,20 @@ fn dsp(x){
}
\end{lstlisting}
\begin{lstlisting}[float,floatplacement=H,label=lst:bytecodes_fbdelay,caption=\it Compiled VM instructions of one-pole filter example in Listing \ref{lst:fbdelay}]
\begin{lstlisting}[float,floatplacement=H,label=lst:bytecodes_fbdelay,caption=\it Compiled VM instructions of feedback delay example in Listing \ref{lst:fbdelay}]
CONSTANTS:[0.7,2,0.8,400,800,0,1]
fn fbdelay(x,fb,dtime) state_size:2
MOVE 3 0
GETSTATE 4
SHIFTSTATE 1
DELAY 4 2
MOVE 5 1
MULF 4 4 5
ADDF 3 3 4
SHIFTSTATE -1
GETSTATE 4
SETSTATE 3
RETURN 4 1
MOVE 3 0 //load x
GETSTATE 4 //load self
SHIFTSTATE 1 //shift Spos
DELAY 4 4 2 //delay(_,_,_)
MOVE 5 1 // load fb
MULF 4 4 5 //delayed val *fb
ADDF 3 3 4 // x+
SHIFTSTATE -1 //reset SPos
GETSTATE 4 //prepare result
SETSTATE 3 //store to self
RETURN 4 1 //return previous self
fn twodelay(x,dtime) state_size:4
MOVECONST 2 5 //load "fbdelay" prototype
@@ -444,20 +457,109 @@ SHIFTSTATE -4
RETURN 1 1
\end{lstlisting}
\begin{figure}[ht]
\centerline{\includegraphics[width=0.7\hsize]{fbdelay_spos}}
\caption{\label{fig:fbdelay_spos}{\it Image of how the state position moves while executing \texttt{twodelay} function in Listing \ref{lst:bytecodes_fbdelay}.}}
\end{figure}
\section{Discussion : Different behaviour depending on the position of let binding}
Listing \ref{lst:filterbank_good} shows an example of a higher-order function \\ \texttt{filterbank} that takes another function \texttt{filter} that takes an input and a frequency as an argument, duplicates \texttt{n} of filter, and adds them together. Note that 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. Also, because the semantics is call-by-value paradigm, reassignment syntax never be used in the current implementation.
The previous mimium compiler could not compile code that takes a function containing such a state as an argument because the tree of all internal states was statically determined at compile time, but the VM in the \lambdammm\ can manage it dynamically. Listing \ref{lst:bytecode_filterbank} shows translated VM instruction of the code. Recursive calls of the first line of code in \texttt{filterbank} and the functions given as arguments or obtained via upvalue like \texttt{filter} are called with the \texttt{CALLCLS} instruction instead of the \texttt{CALL} instruction. The \texttt{GETSTATE} and \texttt{SETSTATE} instructions are not used in this function because the internal state storage is switched when the \texttt{CALLCLS} is interpreted.
\begin{lstlisting}[float,floatplacement=H,label=lst:filterbank_good,language=Rust,caption=\it Example code that duplicates filter parametrically using a recursive function and closure.]
fn filterbank(n,filter){
let next = filterbank(n-1,filter)
if (n>0){
|x,freq| filter(x,freq+n*100)
+ next(x,freq)
}else{
|x,freq| 0
}
}
let myfilter = filterbank(3,bandpass)
fn dsp(){
myfilter(x,1000)
}
\end{lstlisting}
\begin{lstlisting}[float,floatplacement=H,label=lst:bytecode_filterbank,caption=\it Compiled VM instructions filterbank example in Listing \ref{lst:filterbank_good}]
CONSTANTS[100,1,0,2]
fn inner_then(x,freq)
//upvalue:[local(4),local(3),local(2),local(1)]
GETUPVALUE 3 2 //load filter
MOVE 4 0
MOVE 5 1
GETUPVALUE 6 1 //load n
ADDD 5 5 6
MOVECONST 6 0
MULF 5 5 6
CALLCLS 3 2 1 //call filter
GETUPVALUE 4 4 //load next
MOVE 5 0
MOVE 6 1
CALLCLS 4 2 1 //call next
ADDF 3 3 4
RETURN 3 1
fn inner_else(x,freq)
MOVECONST 2 2
RETURN 2 1
fn filterbank(n,filter)
MOVECONST 2 1 //load itself
MOVE 3 0 //load n
MOVECONST 4 1 //load 1
SUBF 3 3 4
MOVECONST 4 2 //load inner_then
CALLCLS 2 2 1 //recursive call
MOVE 3 0
MOVECONST 4 2 //load 0
SUBF 3 3 4
JMPIFNEG 3 2
MOVECONST 3 2 //load inner_then
CLOSURE 3 3 //load inner_lambda
JMP 2
MOVECONST 3 3 //load inner_else
CLOSURE 3 3
CLOSE 2
RETURN 3 1
\end{lstlisting}
\section{Discussion}
\label{sec:discussion}
Because mimium treats functions that have internal states which change over time, when higher-order functions are used, there is a counterintuitive behavior compared to general functional programming languages.
As seen in the example of the filterbank, in \lambdammm, signal graph can be parametrically generated in an evaluation of global context, compared to that Faust uses a term-rewriting macro and Kronos uses a type-level computation as in the Table \ref{tab:comparison}.
An example is the higher-order function \texttt{filterbank}, which duplicates \texttt{filter} function \texttt{N} times parametrically, and adds 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 in mimium, the difference is whether the filterbank function is executed inside \texttt{dsp} or bound with \texttt{let} once in the global context.
The ability to describe both the generation of parametric signal processing and its content in a single semantics will make it easier for novice users to understand the mechanism of the language. Also, the single semantics may facilitate run-time interoperation with other general-purpose languages.
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}.
On the other hand, there is the problem that the single semantics causes \lambdammm\ to behave differently from the behavior expected in a normal lambda calculus.
\begin{table}[ht]
\centering
\begin{tabular*}{\textwidth}{|c|c|c|}\cline{1-3}
\ & Parametric Signal Graph & Actual DSP \\\cline{1-3}
Faust & Term Rewriting Macro & BDA \\\cline{1-3}
Kronos & Type-level Computation & Value Evaluation\\\cline{1-3}
\lambdammm& \begin{tabular}{ll}Evaluation in \\ Global Context\end{tabular} & \begin{tabular}{ll}Evaluation of \\\texttt{dsp} Function\end{tabular} \\\cline{1-3}
\end{tabular*}
\caption{\label{tab:comparison}{\it Comparison of the way of signal graph generation and actual signal processing between Faust, Kronos and \lambdammm.}}
\end{table}
\subsection{Different behaviour depending on the location of let binding}
\label{sec:letbinding}
By having functions that have internal states which change over time in mimium, when higher-order functions are used, there is a counterintuitive behavior compared to general functional programming languages.
Listing \ref{lst:filterbank_bad} is an example of the incorrect code slightly modified from the filterbank example in Listing \ref{lst:filterbank_good}. The difference between Listing \ref{lst:filterbank_good} and Listing \ref{lst:filterbank_bad} is that the recursive calls in the filterbank function are written directly, or once bound with \texttt{let} expression out of the inner function. Similarly, in the \texttt{dsp} function that will be called by the audio driver in mimium, 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 \texttt{let} were 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, 0: the code is evaluated in the global environment (concretizing the signal processing graph) at first, and 1: 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.
\begin{lstlisting}[float,floatplacement=H,label=lst:filterbank_bad,language=Rust,caption=\it Wrong example of the code that duplicate filter parametrically.]
fn bandpass(x,freq){
//...
}
@@ -466,7 +568,7 @@ fn filterbank(n,filter){
|x,freq| filter(x,freq+n*100)
+ filterbank(n-1,filter)(x,freq)
}else{
0
|x,freq| 0
}
}
fn dsp(){ //called by audio driver.
@@ -474,28 +576,14 @@ fn dsp(){ //called by audio driver.
}
\end{lstlisting}
\begin{lstlisting}[float,floatplacement=H,label=lst:filterbank_good,language=Rust,caption=\it Corrected example of the code that duplicate filter parametrically.]
fn filterbank(n,filter){
let next = filterbank(n-1,filter)
if (n>0){
|x,freq| filter(x,freq+n*100)
+ next(x,freq)
}else{
0
}
}
let myfilter = filterbank(3,bandpass)
fn dsp(){
myfilter(x,1000)
}
\end{lstlisting}
\begin{lstlisting}[float,floatplacement=H,label=lst:filterbank_multi,language=Rust,caption=\it Example of filterbank function using multi-stage computation in a future specification of mimium.]
fn filterbank(n,filter){
.< if (n>0){
|x,freq| filter(x,freq+n*100)
+ ~filterbank(n-1,filter)(x,freq)
}else{
0
|x,freq| 0
} >.
}
fn dsp(){
@@ -503,23 +591,26 @@ fn dsp(){
}
\end{lstlisting}
This means that the major compiler optimization techniques such as the constant folding and the function inlining can not simply be appropriated for mimium. Those optimizations should be done after the evaluation of a global context and before evaluating \texttt{dsp} function.
This means that the major compiler optimization techniques such as the constant folding and the function inlining can not simply be appropriated. Those optimizations should be done after the evaluation of a global context and before evaluating \texttt{dsp} function.
To solve this situation, introducing distinction whether the term should be used in global context evaluation (stage 0) and in the actual signal processing (stage 1) in type system. This can be realized with Multi-Stage Computation\cite{Taha1997}. Listing \ref{lst:filterbank_multi} is the example of \texttt{filterbank} code using BER MetaOCaml's syntaxes \texttt{.<term>.} which will generate evaluated program to be used in a next stage, and \texttt{\textasciitilde term} which embed terms evaluated at the previous stage\cite{kiselyov2014a}.
To solve this situation, introducing distinction whether the term should be used in global context evaluation(Stage 0) and in the actual signal processing(stage 1) in type system. This can be realized with Multi-Stage Computation\cite{Taha1997}. Listing \ref{lst:filterbank_multi} is the example of \texttt{filterbank} code using BER MetaOCaml's syntaxes \texttt{.<term>.} which will generate evaluated program used in a next stage, and \texttt{\textasciitilde term} which embed terms evaluated at the previous stage\cite{kiselyov2014a}.
\texttt{filterbank} function is evaluated in stage 0 while embedding itself by using \texttt{\textasciitilde}. This multi-stage computation code still has a same semantics in a generative signal graph generation and execution of the signal processing, in contrast to that Faust and Kronos.
\texttt{filterbank} function is evaluated in stage 0 while embedding itself by using \texttt{\textasciitilde}.
\subsection{A possibility of the foreign statefull function call}
This multi-stage computation code has a same semantics in a generative signal graph generation and execution of the signal processing, in contrast to that Faust have 2 different semantics of the term rewriting macro and BDA.
The data structure of closure in \lambdammm\ is a combination of functions and internal states, as shown in Figure 3. The fact that\\ \texttt{filterbank} samples do not require any special handling of internal states also means that external signal processor (Unit Generator: UGen) such as oscillators and filters written in C or C++, for example, can be called from mimium in the same way as normal closure calls, and it is even possible to parametrically duplicate and combine external UGens. This is an advantage that is difficult to implement in Faust and other similar languages, but easy to implement on \lambdammm\ paradigm.
However currently, mimium is based on sample-by-sample processing and cannot handle buffer-by-buffer value passing. Since most native unit generators perform processing on a buffer-by-buffer basis, there are not many cases where external UGens are utilized in practice for now. However, in the \lambdammm, only $feed$ terms need to be processed sample-by-sample, so it is possible to distinguish functions that can only process one sample at a time from functions that can process concurrently at the type level. As the Multi-rate specification is being considered in Faust\cite{jouvelotDependentVectorTypes2011}, it may be possible to read/write buffer between an external Unit Generator by having the compiler automatically determine the parts that can be processed as buffer-by-buffer.
\section{Conclusion}
\label{sec:conclusion}
This paper proposed \lambdammm , an intermediate representation for the programming languages for music and signal processing with the virtual machine and instruction set to run it. \lambdammm enables to describe generative signal graph and its contents in a single syntax and semantics. However, user have to be responsible to write codes that does not create escapable closures during the dsp execution and this problem would be difficult to understand by novice users.
This paper proposed \lambdammm , an intermediate representation for the programming languages for music and signal processing with the virtual machine and instruction set to run it. \lambdammm\ enables to describe generative signal graph and its contents in a single syntax and semantics. However, user have to be responsible to write codes that does not create escapable closures during the iterative execution of DSP, which will be difficult to understand for novice users.
In this paper, the translation from \lambdammm\ terms from VM instructions is explained by just showing examples of the code and its expected result of instructions as well as the semantics of VM is presented with pseudo-code of the behaviour. More formal semantics and translation process should be considered along with an introduction of the multi-stage computation.
I hope that this research will lead to more general representations of music and sound on the digital computer and more connections between the theory of languages for music and more general programming language theory.
\section{Acknowledgments}

10
src/ref.bib
View File

@@ -143,3 +143,13 @@
isbn = {978-3-319-07151-0},
language = {en}
}
@article{jouvelotDependentVectorTypes2011,
title = {Dependent Vector Types for Data Structuring in Multirate {{Faust}}},
author = {Jouvelot, Pierre and Orlarey, Yann},
year = {2011},
journal = {Computer Languages, Systems \& Structures},
volume = {37},
number = {3},
pages = {113--131},
publisher = {Elsevier}
}

8
src/semantics.tex
View File

@@ -5,7 +5,7 @@
\begin{minipage}[b]{5.5cm}
\centering
\begin{equation*}
\frac{E^n \vdash e_1 \Downarrow v_1 \ n>v_1 \ E^{n-v_1} \vdash e_2 \Downarrow v_2}{E^n \vdash\ delay\ n\ e_1\ e_2 \Downarrow v_2}
\frac{E^n \vdash e_2 \Downarrow v_d \ n>v_d \ E^{n-v_d} \vdash e_1 \Downarrow v}{E^n \vdash\ delay\ n\ e_1\ e_2 \Downarrow v}
\end{equation*}\textrm{E-DELAY}
\end{minipage} &
\begin{minipage}[b]{5.5cm}
@@ -17,21 +17,21 @@
\begin{minipage}[b]{5.5cm}
\centering
\begin{equation*}
\frac{ E^{n-1} \vdash e \Downarrow v_1\ E^n, x \mapsto v_1 \vdash e \Downarrow v_2 }{E^n, x \mapsto v_2\ \vdash\ feed\ x\ e \Downarrow v_1}
\frac{ E^{n-1} \vdash e \Downarrow v_f\ E^n, x \mapsto v_f \vdash e \Downarrow v }{E^n \vdash\ feed\ x.e \Downarrow v}
\end{equation*}\textrm{E-FEED}
\end{minipage}
\\
\begin{minipage}[b]{5.5cm}
\centering
\begin{equation*}
\frac{E^n \vdash e_c \Downarrow n \quad n > 0\ E^n \vdash e_t\ \Downarrow v\ }{E^n \vdash\ if (e_c)\ e_t\ else\ e_t \Downarrow v }
\frac{E^n \vdash e_c \Downarrow n \quad n > 0\ E^n \vdash e_t\ \Downarrow v\ }{E^n \vdash\ if (e_c)\ e_t\ else\ e_e \Downarrow v }
\end{equation*}\textrm{E-IFTRUE}
\end{minipage}
&
\begin{minipage}[b]{5.5cm}
\centering
\begin{equation*}
\frac{E^n \vdash e_c \Downarrow n \quad n \leqq0\ E^n \vdash e_e\ \Downarrow v\ }{E^n \vdash\ if (e_c)\ e_t\ else\ e_t \Downarrow v }
\frac{E^n \vdash e_c \Downarrow n \quad n \leqq0\ E^n \vdash e_e\ \Downarrow v\ }{E^n \vdash\ if (e_c)\ e_t\ else\ e_e \Downarrow v }
\end{equation*}\textrm{E-IFFALSE}
\end{minipage}
&

1449
src/vmmodel.svg
View File

File diff suppressed because it is too large Load Diff
Side by Side Swipe Overlay

Before

Width:  |  Height:  |  Size: 27 KiB

After

Width:  |  Height:  |  Size: 79 KiB