diff options
Diffstat (limited to 'doc/talks')
| -rw-r--r-- | doc/talks/2023-01-18-tocatta/Makefile | 12 | ||||
| -rw-r--r-- | doc/talks/2023-01-18-tocatta/assets/lattice1.svg | 433 | ||||
| -rw-r--r-- | doc/talks/2023-01-18-tocatta/assets/lattice2.svg | 514 | ||||
| -rw-r--r-- | doc/talks/2023-01-18-tocatta/assets/lattice3.svg | 515 | ||||
| -rw-r--r-- | doc/talks/2023-01-18-tocatta/assets/lattice4.svg | 525 | ||||
| -rw-r--r-- | doc/talks/2023-01-18-tocatta/assets/lattice5.svg | 536 | ||||
| -rw-r--r-- | doc/talks/2023-01-18-tocatta/assets/lattice6.svg | 553 | ||||
| -rw-r--r-- | doc/talks/2023-01-18-tocatta/assets/lattice7.svg | 581 | ||||
| -rw-r--r-- | doc/talks/2023-01-18-tocatta/assets/lattice8.svg | 587 | ||||
| -rw-r--r-- | doc/talks/2023-01-18-tocatta/assets/lattice9.svg | 587 | ||||
| -rw-r--r-- | doc/talks/2023-01-18-tocatta/assets/latticeA.svg | 587 | ||||
| -rw-r--r-- | doc/talks/2023-01-18-tocatta/assets/latticeB.svg | 598 | ||||
| -rw-r--r-- | doc/talks/2023-01-18-tocatta/assets/latticeC.svg | 598 | ||||
| -rw-r--r-- | doc/talks/2023-01-18-tocatta/talk.pdf | bin | 2594434 -> 2643346 bytes | |||
| -rw-r--r-- | doc/talks/2023-01-18-tocatta/talk.tex | 43 |
15 files changed, 6658 insertions, 11 deletions
diff --git a/doc/talks/2023-01-18-tocatta/Makefile b/doc/talks/2023-01-18-tocatta/Makefile index 4a967d24..a1f76e15 100644 --- a/doc/talks/2023-01-18-tocatta/Makefile +++ b/doc/talks/2023-01-18-tocatta/Makefile @@ -4,6 +4,18 @@ ASSETS=assets/consistent_hashing_1.pdf \ assets/consistent_hashing_4.pdf \ assets/garage_tables.pdf \ assets/consensus.pdf_tex \ + assets/lattice1.pdf_tex \ + assets/lattice2.pdf_tex \ + assets/lattice3.pdf_tex \ + assets/lattice4.pdf_tex \ + assets/lattice5.pdf_tex \ + assets/lattice6.pdf_tex \ + assets/lattice7.pdf_tex \ + assets/lattice8.pdf_tex \ + assets/lattice9.pdf_tex \ + assets/latticeA.pdf_tex \ + assets/latticeB.pdf_tex \ + assets/latticeC.pdf_tex \ assets/deuxfleurs.pdf talk.pdf: talk.tex $(ASSETS) diff --git a/doc/talks/2023-01-18-tocatta/assets/lattice1.svg b/doc/talks/2023-01-18-tocatta/assets/lattice1.svg new file mode 100644 index 00000000..8bfa5aa7 --- /dev/null +++ b/doc/talks/2023-01-18-tocatta/assets/lattice1.svg @@ -0,0 +1,433 @@ +<?xml version="1.0" encoding="UTF-8" standalone="no"?> +<!-- Created with Inkscape (http://www.inkscape.org/) --> + +<svg + width="1000" + height="400" + viewBox="0 0 264.58333 105.83333" + version="1.1" + id="svg5" + inkscape:version="1.2.2 (b0a8486541, 2022-12-01)" + sodipodi:docname="lattice1.svg" + 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="namedview7" + pagecolor="#ffffff" + bordercolor="#666666" + borderopacity="1.0" + inkscape:showpageshadow="2" + inkscape:pageopacity="0.0" + inkscape:pagecheckerboard="0" + inkscape:deskcolor="#d1d1d1" + inkscape:document-units="mm" + showgrid="false" + inkscape:zoom="1.0419012" + inkscape:cx="445.81962" + inkscape:cy="222.66987" + inkscape:window-width="1920" + inkscape:window-height="999" + inkscape:window-x="0" + inkscape:window-y="0" + inkscape:window-maximized="1" + inkscape:current-layer="layer2" /> + <defs + id="defs2"> + <marker + style="overflow:visible" + id="Arrow2" + refX="0" + refY="0" + orient="auto-start-reverse" + inkscape:stockid="Arrow2" + markerWidth="7.6999998" + markerHeight="5.5999999" + viewBox="0 0 7.7 5.6" + inkscape:isstock="true" + inkscape:collect="always" + preserveAspectRatio="xMidYMid"> + <path + transform="scale(0.7)" + d="M -2,-4 9,0 -2,4 c 2,-2.33 2,-5.66 0,-8 z" + style="fill:context-stroke;fill-rule:evenodd;stroke:none" + id="arrow2L" /> + </marker> + <marker + style="overflow:visible" + id="Arrow2-9" + refX="0" + refY="0" + orient="auto-start-reverse" + inkscape:stockid="Arrow2" + markerWidth="7.6999998" + markerHeight="5.5999999" + viewBox="0 0 7.7 5.6" + inkscape:isstock="true" + inkscape:collect="always" + preserveAspectRatio="xMidYMid"> + <path + transform="scale(0.7)" + d="M -2,-4 9,0 -2,4 c 2,-2.33 2,-5.66 0,-8 z" + style="fill:context-stroke;fill-rule:evenodd;stroke:none" + id="arrow2L-1" /> + </marker> + <marker + style="overflow:visible" + id="Arrow2-9-7" + refX="0" + refY="0" + orient="auto-start-reverse" + inkscape:stockid="Arrow2" + markerWidth="7.6999998" + markerHeight="5.5999999" + viewBox="0 0 7.7 5.6" + inkscape:isstock="true" + inkscape:collect="always" + preserveAspectRatio="xMidYMid"> + <path + transform="scale(0.7)" + d="M -2,-4 9,0 -2,4 c 2,-2.33 2,-5.66 0,-8 z" + style="fill:context-stroke;fill-rule:evenodd;stroke:none" + id="arrow2L-1-0" /> + </marker> + <marker + style="overflow:visible" + id="Arrow2-93" + refX="0" + refY="0" + orient="auto-start-reverse" + inkscape:stockid="Arrow2" + markerWidth="7.6999998" + markerHeight="5.5999999" + viewBox="0 0 7.7 5.6" + inkscape:isstock="true" + inkscape:collect="always" + preserveAspectRatio="xMidYMid"> + <path + transform="scale(0.7)" + d="M -2,-4 9,0 -2,4 c 2,-2.33 2,-5.66 0,-8 z" + style="fill:context-stroke;fill-rule:evenodd;stroke:none" + id="arrow2L-6" /> + </marker> + <marker + style="overflow:visible" + id="Arrow2-9-7-2" + refX="0" + refY="0" + orient="auto-start-reverse" + inkscape:stockid="Arrow2" + markerWidth="7.6999998" + markerHeight="5.5999999" + viewBox="0 0 7.7 5.6" + inkscape:isstock="true" + inkscape:collect="always" + preserveAspectRatio="xMidYMid"> + <path + transform="scale(0.7)" + d="M -2,-4 9,0 -2,4 c 2,-2.33 2,-5.66 0,-8 z" + style="fill:context-stroke;fill-rule:evenodd;stroke:none" + id="arrow2L-1-0-6" /> + </marker> + <marker + style="overflow:visible" + id="Arrow2-93-1" + refX="0" + refY="0" + orient="auto-start-reverse" + inkscape:stockid="Arrow2" + markerWidth="7.6999998" + markerHeight="5.5999999" + viewBox="0 0 7.7 5.6" + inkscape:isstock="true" + inkscape:collect="always" + preserveAspectRatio="xMidYMid"> + <path + transform="scale(0.7)" + d="M -2,-4 9,0 -2,4 c 2,-2.33 2,-5.66 0,-8 z" + style="fill:context-stroke;fill-rule:evenodd;stroke:none" + id="arrow2L-6-8" /> + </marker> + <marker + style="overflow:visible" + id="Arrow2-9-75" + refX="0" + refY="0" + orient="auto-start-reverse" + inkscape:stockid="Arrow2" + markerWidth="7.6999998" + markerHeight="5.5999999" + viewBox="0 0 7.7 5.6" + inkscape:isstock="true" + inkscape:collect="always" + preserveAspectRatio="xMidYMid"> + <path + transform="scale(0.7)" + d="M -2,-4 9,0 -2,4 c 2,-2.33 2,-5.66 0,-8 z" + style="fill:context-stroke;fill-rule:evenodd;stroke:none" + id="arrow2L-1-9" /> + </marker> + <marker + style="overflow:visible" + id="Arrow2-9-75-2" + refX="0" + refY="0" + orient="auto-start-reverse" + inkscape:stockid="Arrow2" + markerWidth="7.6999998" + markerHeight="5.5999999" + viewBox="0 0 7.7 5.6" + inkscape:isstock="true" + inkscape:collect="always" + preserveAspectRatio="xMidYMid"> + <path + transform="scale(0.7)" + d="M -2,-4 9,0 -2,4 c 2,-2.33 2,-5.66 0,-8 z" + style="fill:context-stroke;fill-rule:evenodd;stroke:none" + id="arrow2L-1-9-8" /> + </marker> + <marker + style="overflow:visible" + id="Arrow2-9-75-7" + refX="0" + refY="0" + orient="auto-start-reverse" + inkscape:stockid="Arrow2" + markerWidth="7.6999998" + markerHeight="5.5999999" + viewBox="0 0 7.7 5.6" + inkscape:isstock="true" + inkscape:collect="always" + preserveAspectRatio="xMidYMid"> + <path + transform="scale(0.7)" + d="M -2,-4 9,0 -2,4 c 2,-2.33 2,-5.66 0,-8 z" + style="fill:context-stroke;fill-rule:evenodd;stroke:none" + id="arrow2L-1-9-3" /> + </marker> + <marker + style="overflow:visible" + id="Arrow2-9-75-7-1" + refX="0" + refY="0" + orient="auto-start-reverse" + inkscape:stockid="Arrow2" + markerWidth="7.6999998" + markerHeight="5.5999999" + viewBox="0 0 7.7 5.6" + inkscape:isstock="true" + inkscape:collect="always" + preserveAspectRatio="xMidYMid"> + <path + transform="scale(0.7)" + d="M -2,-4 9,0 -2,4 c 2,-2.33 2,-5.66 0,-8 z" + style="fill:context-stroke;fill-rule:evenodd;stroke:none" + id="arrow2L-1-9-3-2" /> + </marker> + <marker + style="overflow:visible" + id="Arrow2-93-1-4" + refX="0" + refY="0" + orient="auto-start-reverse" + inkscape:stockid="Arrow2" + markerWidth="7.6999998" + markerHeight="5.5999999" + viewBox="0 0 7.7 5.6" + inkscape:isstock="true" + inkscape:collect="always" + preserveAspectRatio="xMidYMid"> + <path + transform="scale(0.7)" + d="M -2,-4 9,0 -2,4 c 2,-2.33 2,-5.66 0,-8 z" + style="fill:context-stroke;fill-rule:evenodd;stroke:none" + id="arrow2L-6-8-7" /> + </marker> + <marker + style="overflow:visible" + id="Arrow2-9-7-2-8" + refX="0" + refY="0" + orient="auto-start-reverse" + inkscape:stockid="Arrow2" + markerWidth="7.6999998" + markerHeight="5.5999999" + viewBox="0 0 7.7 5.6" + inkscape:isstock="true" + inkscape:collect="always" + preserveAspectRatio="xMidYMid"> + <path + transform="scale(0.7)" + d="M -2,-4 9,0 -2,4 c 2,-2.33 2,-5.66 0,-8 z" + style="fill:context-stroke;fill-rule:evenodd;stroke:none" + id="arrow2L-1-0-6-4" /> + </marker> + </defs> + <g + inkscape:label="Layer 1" + inkscape:groupmode="layer" + id="layer1" + sodipodi:insensitive="true"> + <rect + style="fill:#ffffff;stroke:none;stroke-width:1;stop-color:#000000" + id="rect288" + width="209.84705" + height="104.42732" + x="0.77790999" + y="0.93738818" /> + </g> + <g + inkscape:groupmode="layer" + id="layer2" + inkscape:label="Layer 2"> + <text + xml:space="preserve" + style="font-size:8.46667px;line-height:1.25;font-family:sans-serif;text-align:center;text-anchor:middle;stroke-width:0.264583;fill:#000000" + x="164.56372" + y="99.307442" + id="text951"><tspan + sodipodi:role="line" + id="tspan949" + style="stroke-width:0.264583;fill:#000000" + x="164.56372" + y="99.307442">$\{\}$</tspan></text> + <text + xml:space="preserve" + style="font-size:8.46667px;line-height:1.25;font-family:sans-serif;text-align:center;text-anchor:middle;stroke-width:0.264583;fill:#000000" + x="164.56372" + y="13.151893" + id="text1005"><tspan + sodipodi:role="line" + id="tspan1003" + style="stroke-width:0.264583;fill:#000000" + x="164.56372" + y="13.151893">$\{a,b,c\}$</tspan></text> + <g + id="g1175" + transform="translate(51.996784,3.5774043)"> + <text + xml:space="preserve" + style="font-size:8.46667px;line-height:1.25;font-family:sans-serif;text-align:center;text-anchor:middle;stroke-width:0.264583;fill:#000000" + x="49.27084" + y="67.008698" + id="text1009"><tspan + sodipodi:role="line" + id="tspan1007" + style="stroke-width:0.264583;fill:#000000" + x="49.27084" + y="67.008698">$\{a\}$</tspan></text> + <text + xml:space="preserve" + style="font-size:8.46667px;line-height:1.25;font-family:sans-serif;text-align:center;text-anchor:middle;stroke-width:0.264583;fill:#000000" + x="112.90984" + y="67.017166" + id="text1009-3"><tspan + sodipodi:role="line" + id="tspan1007-6" + style="stroke-width:0.264583;fill:#000000" + x="112.90984" + y="67.017166">$\{b\}$</tspan></text> + <text + xml:space="preserve" + style="font-size:8.46667px;line-height:1.25;font-family:sans-serif;text-align:center;text-anchor:middle;stroke-width:0.264583;fill:#000000" + x="176.20593" + y="67.008698" + id="text1009-7"><tspan + sodipodi:role="line" + id="tspan1007-5" + style="stroke-width:0.264583;fill:#000000" + x="176.20593" + y="67.008698">$\{c\}$</tspan></text> + </g> + <g + id="g1183" + transform="translate(51.996784,1.0317046)"> + <text + xml:space="preserve" + style="font-size:8.46667px;line-height:1.25;font-family:sans-serif;text-align:center;text-anchor:middle;stroke-width:0.264583;fill:#000000" + x="112.90984" + y="40.841526" + id="text1117"><tspan + sodipodi:role="line" + id="tspan1115" + style="stroke-width:0.264583;fill:#000000" + x="112.90984" + y="40.841526">$\{a,c\}$</tspan></text> + <text + xml:space="preserve" + style="font-size:8.46667px;line-height:1.25;font-family:sans-serif;text-align:center;text-anchor:middle;stroke-width:0.264583;fill:#000000" + x="49.27084" + y="40.841526" + id="text1117-3"><tspan + sodipodi:role="line" + id="tspan1115-5" + style="stroke-width:0.264583;fill:#000000" + x="49.27084" + y="40.841526">$\{a,b\}$</tspan></text> + <text + xml:space="preserve" + style="font-size:8.46667px;line-height:1.25;font-family:sans-serif;text-align:center;text-anchor:middle;stroke-width:0.264583;fill:#000000" + x="176.20593" + y="40.841526" + id="text1117-6"><tspan + sodipodi:role="line" + id="tspan1115-2" + style="stroke-width:0.264583;fill:#000000" + x="176.20593" + y="40.841526">$\{b,c\}$</tspan></text> + </g> + <path + style="fill:none;stroke:#000000;stroke-width:0.5;stroke-linecap:butt;stroke-linejoin:miter;stroke-dasharray:none;stroke-opacity:1;marker-end:url(#Arrow2)" + d="M 153.33622,90.367682 118.34198,73.428915" + id="path1300" /> + <path + style="fill:none;stroke:#000000;stroke-width:0.5;stroke-linecap:butt;stroke-linejoin:miter;stroke-dasharray:none;stroke-opacity:1;marker-end:url(#Arrow2-9)" + d="M 177.46016,90.367682 212.4544,73.428915" + id="path1300-2" /> + <path + style="fill:none;stroke:#000000;stroke-width:0.5;stroke-linecap:butt;stroke-linejoin:miter;stroke-dasharray:none;stroke-opacity:1;marker-end:url(#Arrow2-93)" + d="M 153.33622,61.655656 118.34198,44.716889" + id="path1300-0" /> + <path + style="fill:none;stroke:#000000;stroke-width:0.5;stroke-linecap:butt;stroke-linejoin:miter;stroke-dasharray:none;stroke-opacity:1;marker-end:url(#Arrow2-9-7)" + d="M 177.46016,61.655656 212.4544,44.716889" + id="path1300-2-6" /> + <path + style="fill:none;stroke:#000000;stroke-width:0.5;stroke-linecap:butt;stroke-linejoin:miter;stroke-dasharray:none;stroke-opacity:1;marker-end:url(#Arrow2-93-1)" + d="M 118.34198,61.655656 153.33622,44.716889" + id="path1300-0-7" /> + <path + style="fill:none;stroke:#000000;stroke-width:0.5;stroke-linecap:butt;stroke-linejoin:miter;stroke-dasharray:none;stroke-opacity:1;marker-end:url(#Arrow2-9-7-2)" + d="M 212.4544,61.655656 177.46016,44.716889" + id="path1300-2-6-9" /> + <path + style="fill:none;stroke:#000000;stroke-width:0.5;stroke-linecap:butt;stroke-linejoin:miter;stroke-dasharray:none;stroke-opacity:1;marker-end:url(#Arrow2-93-1-4)" + d="M 118.34198,34.227412 153.33622,17.288645" + id="path1300-0-7-5" /> + <path + style="fill:none;stroke:#000000;stroke-width:0.5;stroke-linecap:butt;stroke-linejoin:miter;stroke-dasharray:none;stroke-opacity:1;marker-end:url(#Arrow2-9-7-2-8)" + d="M 212.4544,34.227412 177.46016,17.288645" + id="path1300-2-6-9-0" /> + <path + style="fill:none;stroke:#000000;stroke-width:0.5;stroke-linecap:butt;stroke-linejoin:miter;stroke-dasharray:none;stroke-opacity:1;marker-end:url(#Arrow2-9-75)" + d="m 228.52843,61.091809 0.33313,-12.554874 m -0.33313,12.554874 0.33313,-12.554874" + id="path1300-2-2" + sodipodi:nodetypes="cc" /> + <path + style="fill:none;stroke:#000000;stroke-width:0.5;stroke-linecap:butt;stroke-linejoin:miter;stroke-dasharray:none;stroke-opacity:1;marker-end:url(#Arrow2-9-75-2)" + d="m 101.90418,61.091809 0.33313,-12.554874 m -0.33313,12.554874 0.33313,-12.554874" + id="path1300-2-2-9" + sodipodi:nodetypes="cc" /> + <path + style="fill:none;stroke:#000000;stroke-width:0.5;stroke-linecap:butt;stroke-linejoin:miter;stroke-dasharray:none;stroke-opacity:1;marker-end:url(#Arrow2-9-75-7)" + d="m 165.29305,89.571762 0.33313,-12.554874 m -0.33313,12.554874 0.33313,-12.554874" + id="path1300-2-2-6" + sodipodi:nodetypes="cc" /> + <path + style="fill:none;stroke:#000000;stroke-width:0.5;stroke-linecap:butt;stroke-linejoin:miter;stroke-dasharray:none;stroke-opacity:1;marker-end:url(#Arrow2-9-75-7-1)" + d="m 165.29305,32.445235 0.33313,-12.554874 m -0.33313,12.554874 0.33313,-12.554874" + id="path1300-2-2-6-9" + sodipodi:nodetypes="cc" /> + </g> +</svg> diff --git a/doc/talks/2023-01-18-tocatta/assets/lattice2.svg b/doc/talks/2023-01-18-tocatta/assets/lattice2.svg new file mode 100644 index 00000000..adcd92cb --- /dev/null +++ b/doc/talks/2023-01-18-tocatta/assets/lattice2.svg @@ -0,0 +1,514 @@ +<?xml version="1.0" encoding="UTF-8" standalone="no"?> +<!-- Created with Inkscape (http://www.inkscape.org/) --> + +<svg + width="1000" + height="400" + viewBox="0 0 264.58333 105.83333" + version="1.1" + id="svg5" + inkscape:version="1.2.2 (b0a8486541, 2022-12-01)" + sodipodi:docname="lattice2.svg" + 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="namedview7" + pagecolor="#ffffff" + bordercolor="#666666" + borderopacity="1.0" + inkscape:showpageshadow="2" + inkscape:pageopacity="0.0" + inkscape:pagecheckerboard="0" + inkscape:deskcolor="#d1d1d1" + inkscape:document-units="mm" + showgrid="false" + inkscape:zoom="1.0419012" + inkscape:cx="384.39345" + inkscape:cy="227.46879" + inkscape:window-width="1920" + inkscape:window-height="999" + inkscape:window-x="0" + inkscape:window-y="0" + inkscape:window-maximized="1" + inkscape:current-layer="layer2" /> + <defs + id="defs2"> + <marker + style="overflow:visible" + id="Arrow2" + refX="0" + refY="0" + orient="auto-start-reverse" + inkscape:stockid="Arrow2" + markerWidth="7.6999998" + markerHeight="5.5999999" + viewBox="0 0 7.7 5.6" + inkscape:isstock="true" + inkscape:collect="always" + preserveAspectRatio="xMidYMid"> + <path + transform="scale(0.7)" + d="M -2,-4 9,0 -2,4 c 2,-2.33 2,-5.66 0,-8 z" + style="fill:context-stroke;fill-rule:evenodd;stroke:none" + id="arrow2L" /> + </marker> + <marker + style="overflow:visible" + id="Arrow2-9" + refX="0" + refY="0" + orient="auto-start-reverse" + inkscape:stockid="Arrow2" + markerWidth="7.6999998" + markerHeight="5.5999999" + viewBox="0 0 7.7 5.6" + inkscape:isstock="true" + inkscape:collect="always" + preserveAspectRatio="xMidYMid"> + <path + transform="scale(0.7)" + d="M -2,-4 9,0 -2,4 c 2,-2.33 2,-5.66 0,-8 z" + style="fill:context-stroke;fill-rule:evenodd;stroke:none" + id="arrow2L-1" /> + </marker> + <marker + style="overflow:visible" + id="Arrow2-9-7" + refX="0" + refY="0" + orient="auto-start-reverse" + inkscape:stockid="Arrow2" + markerWidth="7.6999998" + markerHeight="5.5999999" + viewBox="0 0 7.7 5.6" + inkscape:isstock="true" + inkscape:collect="always" + preserveAspectRatio="xMidYMid"> + <path + transform="scale(0.7)" + d="M -2,-4 9,0 -2,4 c 2,-2.33 2,-5.66 0,-8 z" + style="fill:context-stroke;fill-rule:evenodd;stroke:none" + id="arrow2L-1-0" /> + </marker> + <marker + style="overflow:visible" + id="Arrow2-93" + refX="0" + refY="0" + orient="auto-start-reverse" + inkscape:stockid="Arrow2" + markerWidth="7.6999998" + markerHeight="5.5999999" + viewBox="0 0 7.7 5.6" + inkscape:isstock="true" + inkscape:collect="always" + preserveAspectRatio="xMidYMid"> + <path + transform="scale(0.7)" + d="M -2,-4 9,0 -2,4 c 2,-2.33 2,-5.66 0,-8 z" + style="fill:context-stroke;fill-rule:evenodd;stroke:none" + id="arrow2L-6" /> + </marker> + <marker + style="overflow:visible" + id="Arrow2-9-7-2" + refX="0" + refY="0" + orient="auto-start-reverse" + inkscape:stockid="Arrow2" + markerWidth="7.6999998" + markerHeight="5.5999999" + viewBox="0 0 7.7 5.6" + inkscape:isstock="true" + inkscape:collect="always" + preserveAspectRatio="xMidYMid"> + <path + transform="scale(0.7)" + d="M -2,-4 9,0 -2,4 c 2,-2.33 2,-5.66 0,-8 z" + style="fill:context-stroke;fill-rule:evenodd;stroke:none" + id="arrow2L-1-0-6" /> + </marker> + <marker + style="overflow:visible" + id="Arrow2-93-1" + refX="0" + refY="0" + orient="auto-start-reverse" + inkscape:stockid="Arrow2" + markerWidth="7.6999998" + markerHeight="5.5999999" + viewBox="0 0 7.7 5.6" + inkscape:isstock="true" + inkscape:collect="always" + preserveAspectRatio="xMidYMid"> + <path + transform="scale(0.7)" + d="M -2,-4 9,0 -2,4 c 2,-2.33 2,-5.66 0,-8 z" + style="fill:context-stroke;fill-rule:evenodd;stroke:none" + id="arrow2L-6-8" /> + </marker> + <marker + style="overflow:visible" + id="Arrow2-9-75" + refX="0" + refY="0" + orient="auto-start-reverse" + inkscape:stockid="Arrow2" + markerWidth="7.6999998" + markerHeight="5.5999999" + viewBox="0 0 7.7 5.6" + inkscape:isstock="true" + inkscape:collect="always" + preserveAspectRatio="xMidYMid"> + <path + transform="scale(0.7)" + d="M -2,-4 9,0 -2,4 c 2,-2.33 2,-5.66 0,-8 z" + style="fill:context-stroke;fill-rule:evenodd;stroke:none" + id="arrow2L-1-9" /> + </marker> + <marker + style="overflow:visible" + id="Arrow2-9-75-2" + refX="0" + refY="0" + orient="auto-start-reverse" + inkscape:stockid="Arrow2" + markerWidth="7.6999998" + markerHeight="5.5999999" + viewBox="0 0 7.7 5.6" + inkscape:isstock="true" + inkscape:collect="always" + preserveAspectRatio="xMidYMid"> + <path + transform="scale(0.7)" + d="M -2,-4 9,0 -2,4 c 2,-2.33 2,-5.66 0,-8 z" + style="fill:context-stroke;fill-rule:evenodd;stroke:none" + id="arrow2L-1-9-8" /> + </marker> + <marker + style="overflow:visible" + id="Arrow2-9-75-7" + refX="0" + refY="0" + orient="auto-start-reverse" + inkscape:stockid="Arrow2" + markerWidth="7.6999998" + markerHeight="5.5999999" + viewBox="0 0 7.7 5.6" + inkscape:isstock="true" + inkscape:collect="always" + preserveAspectRatio="xMidYMid"> + <path + transform="scale(0.7)" + d="M -2,-4 9,0 -2,4 c 2,-2.33 2,-5.66 0,-8 z" + style="fill:context-stroke;fill-rule:evenodd;stroke:none" + id="arrow2L-1-9-3" /> + </marker> + <marker + style="overflow:visible" + id="Arrow2-9-75-7-1" + refX="0" + refY="0" + orient="auto-start-reverse" + inkscape:stockid="Arrow2" + markerWidth="7.6999998" + markerHeight="5.5999999" + viewBox="0 0 7.7 5.6" + inkscape:isstock="true" + inkscape:collect="always" + preserveAspectRatio="xMidYMid"> + <path + transform="scale(0.7)" + d="M -2,-4 9,0 -2,4 c 2,-2.33 2,-5.66 0,-8 z" + style="fill:context-stroke;fill-rule:evenodd;stroke:none" + id="arrow2L-1-9-3-2" /> + </marker> + <marker + style="overflow:visible" + id="Arrow2-93-1-4" + refX="0" + refY="0" + orient="auto-start-reverse" + inkscape:stockid="Arrow2" + markerWidth="7.6999998" + markerHeight="5.5999999" + viewBox="0 0 7.7 5.6" + inkscape:isstock="true" + inkscape:collect="always" + preserveAspectRatio="xMidYMid"> + <path + transform="scale(0.7)" + d="M -2,-4 9,0 -2,4 c 2,-2.33 2,-5.66 0,-8 z" + style="fill:context-stroke;fill-rule:evenodd;stroke:none" + id="arrow2L-6-8-7" /> + </marker> + <marker + style="overflow:visible" + id="Arrow2-9-7-2-8" + refX="0" + refY="0" + orient="auto-start-reverse" + inkscape:stockid="Arrow2" + markerWidth="7.6999998" + markerHeight="5.5999999" + viewBox="0 0 7.7 5.6" + inkscape:isstock="true" + inkscape:collect="always" + preserveAspectRatio="xMidYMid"> + <path + transform="scale(0.7)" + d="M -2,-4 9,0 -2,4 c 2,-2.33 2,-5.66 0,-8 z" + style="fill:context-stroke;fill-rule:evenodd;stroke:none" + id="arrow2L-1-0-6-4" /> + </marker> + </defs> + <g + inkscape:label="Layer 1" + inkscape:groupmode="layer" + id="layer1" + sodipodi:insensitive="true"> + <rect + style="fill:#ffffff;stroke:none;stroke-width:1;stop-color:#000000" + id="rect288" + width="209.84705" + height="104.42732" + x="0.77790999" + y="0.93738818" /> + </g> + <g + inkscape:groupmode="layer" + id="layer2" + inkscape:label="Layer 2"> + <text + xml:space="preserve" + style="font-size:8.46667px;line-height:1.25;font-family:sans-serif;text-align:center;text-anchor:middle;stroke-width:0.264583;fill:#000000" + x="164.56372" + y="99.307442" + id="text951"><tspan + sodipodi:role="line" + id="tspan949" + style="stroke-width:0.264583;fill:#000000" + x="164.56372" + y="99.307442">$\{\}$</tspan></text> + <text + xml:space="preserve" + style="font-size:8.46667px;line-height:1.25;font-family:sans-serif;text-align:center;text-anchor:middle;stroke-width:0.264583;fill:#000000" + x="164.56372" + y="13.151893" + id="text1005"><tspan + sodipodi:role="line" + id="tspan1003" + style="stroke-width:0.264583;fill:#000000" + x="164.56372" + y="13.151893">$\{a,b,c\}$</tspan></text> + <g + id="g1175" + transform="translate(51.996784,3.5774043)"> + <text + xml:space="preserve" + style="font-size:8.46667px;line-height:1.25;font-family:sans-serif;text-align:center;text-anchor:middle;stroke-width:0.264583;fill:#000000" + x="49.27084" + y="67.008698" + id="text1009"><tspan + sodipodi:role="line" + id="tspan1007" + style="stroke-width:0.264583;fill:#000000" + x="49.27084" + y="67.008698">$\{a\}$</tspan></text> + <text + xml:space="preserve" + style="font-size:8.46667px;line-height:1.25;font-family:sans-serif;text-align:center;text-anchor:middle;stroke-width:0.264583;fill:#000000" + x="112.90984" + y="67.017166" + id="text1009-3"><tspan + sodipodi:role="line" + id="tspan1007-6" + style="stroke-width:0.264583;fill:#000000" + x="112.90984" + y="67.017166">$\{b\}$</tspan></text> + <text + xml:space="preserve" + style="font-size:8.46667px;line-height:1.25;font-family:sans-serif;text-align:center;text-anchor:middle;stroke-width:0.264583;fill:#000000" + x="176.20593" + y="67.008698" + id="text1009-7"><tspan + sodipodi:role="line" + id="tspan1007-5" + style="stroke-width:0.264583;fill:#000000" + x="176.20593" + y="67.008698">$\{c\}$</tspan></text> + </g> + <g + id="g1183" + transform="translate(51.996784,1.0317046)" + style="fill:#000000"> + <text + xml:space="preserve" + style="font-size:8.46667px;line-height:1.25;font-family:sans-serif;text-align:center;text-anchor:middle;stroke-width:0.264583;fill:#000000" + x="112.90984" + y="40.841526" + id="text1117"><tspan + sodipodi:role="line" + id="tspan1115" + style="stroke-width:0.264583;fill:#000000" + x="112.90984" + y="40.841526">$\{a,c\}$</tspan></text> + <text + xml:space="preserve" + style="font-size:8.46667px;line-height:1.25;font-family:sans-serif;text-align:center;text-anchor:middle;stroke-width:0.264583;fill:#000000" + x="49.27084" + y="40.841526" + id="text1117-3"><tspan + sodipodi:role="line" + id="tspan1115-5" + style="stroke-width:0.264583;fill:#000000" + x="49.27084" + y="40.841526">$\{a,b\}$</tspan></text> + <text + xml:space="preserve" + style="font-size:8.46667px;line-height:1.25;font-family:sans-serif;text-align:center;text-anchor:middle;stroke-width:0.264583;fill:#000000" + x="176.20593" + y="40.841526" + id="text1117-6"><tspan + sodipodi:role="line" + id="tspan1115-2" + style="stroke-width:0.264583;fill:#000000" + x="176.20593" + y="40.841526">$\{b,c\}$</tspan></text> + </g> + <path + style="fill:none;stroke:#000000;stroke-width:0.5;stroke-linecap:butt;stroke-linejoin:miter;stroke-dasharray:none;stroke-opacity:1;marker-end:url(#Arrow2)" + d="M 153.33622,90.367682 118.34198,73.428915" + id="path1300" /> + <path + style="fill:none;stroke:#000000;stroke-width:0.5;stroke-linecap:butt;stroke-linejoin:miter;stroke-dasharray:none;stroke-opacity:1;marker-end:url(#Arrow2-9)" + d="M 177.46016,90.367682 212.4544,73.428915" + id="path1300-2" /> + <path + style="fill:none;stroke:#000000;stroke-width:0.5;stroke-linecap:butt;stroke-linejoin:miter;stroke-dasharray:none;stroke-opacity:1;marker-end:url(#Arrow2-93)" + d="M 153.33622,61.655656 118.34198,44.716889" + id="path1300-0" /> + <path + style="fill:none;stroke:#000000;stroke-width:0.5;stroke-linecap:butt;stroke-linejoin:miter;stroke-dasharray:none;stroke-opacity:1;marker-end:url(#Arrow2-9-7)" + d="M 177.46016,61.655656 212.4544,44.716889" + id="path1300-2-6" /> + <path + style="fill:none;stroke:#000000;stroke-width:0.5;stroke-linecap:butt;stroke-linejoin:miter;stroke-dasharray:none;stroke-opacity:1;marker-end:url(#Arrow2-93-1)" + d="M 118.34198,61.655656 153.33622,44.716889" + id="path1300-0-7" /> + <path + style="fill:none;stroke:#000000;stroke-width:0.5;stroke-linecap:butt;stroke-linejoin:miter;stroke-dasharray:none;stroke-opacity:1;marker-end:url(#Arrow2-9-7-2)" + d="M 212.4544,61.655656 177.46016,44.716889" + id="path1300-2-6-9" /> + <path + style="fill:none;stroke:#000000;stroke-width:0.5;stroke-linecap:butt;stroke-linejoin:miter;stroke-dasharray:none;stroke-opacity:1;marker-end:url(#Arrow2-93-1-4)" + d="M 118.34198,34.227412 153.33622,17.288645" + id="path1300-0-7-5" /> + <path + style="fill:none;stroke:#000000;stroke-width:0.5;stroke-linecap:butt;stroke-linejoin:miter;stroke-dasharray:none;stroke-opacity:1;marker-end:url(#Arrow2-9-7-2-8)" + d="M 212.4544,34.227412 177.46016,17.288645" + id="path1300-2-6-9-0" /> + <path + style="fill:none;stroke:#000000;stroke-width:0.5;stroke-linecap:butt;stroke-linejoin:miter;stroke-dasharray:none;stroke-opacity:1;marker-end:url(#Arrow2-9-75)" + d="m 228.52843,61.091809 0.33313,-12.554874 m -0.33313,12.554874 0.33313,-12.554874" + id="path1300-2-2" + sodipodi:nodetypes="cc" /> + <path + style="fill:none;stroke:#000000;stroke-width:0.5;stroke-linecap:butt;stroke-linejoin:miter;stroke-dasharray:none;stroke-opacity:1;marker-end:url(#Arrow2-9-75-2)" + d="m 101.90418,61.091809 0.33313,-12.554874 m -0.33313,12.554874 0.33313,-12.554874" + id="path1300-2-2-9" + sodipodi:nodetypes="cc" /> + <path + style="fill:none;stroke:#000000;stroke-width:0.5;stroke-linecap:butt;stroke-linejoin:miter;stroke-dasharray:none;stroke-opacity:1;marker-end:url(#Arrow2-9-75-7)" + d="m 165.29305,89.571762 0.33313,-12.554874 m -0.33313,12.554874 0.33313,-12.554874" + id="path1300-2-2-6" + sodipodi:nodetypes="cc" /> + <path + style="fill:none;stroke:#000000;stroke-width:0.5;stroke-linecap:butt;stroke-linejoin:miter;stroke-dasharray:none;stroke-opacity:1;marker-end:url(#Arrow2-9-75-7-1)" + d="m 165.29305,32.445235 0.33313,-12.554874 m -0.33313,12.554874 0.33313,-12.554874" + id="path1300-2-2-6-9" + sodipodi:nodetypes="cc" /> + <circle + style="fill:#ff0000;stroke:none;stroke-width:0.499999;stroke-dasharray:none;stop-color:#000000" + id="path3663" + cx="147.35568" + cy="95.24971" + r="2.7302806" /> + <circle + style="fill:#008000;stroke:none;stroke-width:0.499999;stroke-dasharray:none;stop-color:#000000" + id="path3663-3" + cx="139.48744" + cy="95.24971" + r="2.7302806" /> + <circle + style="fill:#800080;stroke:none;stroke-width:0.499999;stroke-dasharray:none;stop-color:#000000" + id="path3663-6" + cx="131.61919" + cy="95.24971" + r="2.7302806" /> + <circle + style="fill:#ff0000;stroke:none;stroke-width:0.499999;stroke-dasharray:none;stop-color:#000000" + id="path3663-1" + cx="18.004833" + cy="39.402473" + r="2.7302806" /> + <circle + style="fill:#008000;stroke:none;stroke-width:0.499999;stroke-dasharray:none;stop-color:#000000" + id="path3663-3-0" + cx="18.004833" + cy="30.371933" + r="2.7302806" /> + <circle + style="fill:#800080;stroke:none;stroke-width:0.499999;stroke-dasharray:none;stop-color:#000000" + id="path3663-6-6" + cx="18.004833" + cy="21.341394" + r="2.7302806" /> + <text + xml:space="preserve" + style="font-size:8.46667px;line-height:1.25;font-family:sans-serif;stroke-width:0.264583;fill:#000000" + x="6.9525447" + y="13.702217" + id="text3707"><tspan + sodipodi:role="line" + id="tspan3705" + style="stroke-width:0.264583;fill:#000000" + x="6.9525447" + y="13.702217">$write(\{a\})$:</tspan></text> + <text + xml:space="preserve" + style="font-size:8.46667px;line-height:1.25;font-family:sans-serif;fill:#999999;stroke-width:0.264583" + x="23.457415" + y="24.042637" + id="text3750"><tspan + sodipodi:role="line" + id="tspan3748" + style="fill:#999999;stroke-width:0.264583" + x="23.457415" + y="24.042637">$\not\sqsupseteq \{a\}$</tspan></text> + <text + xml:space="preserve" + style="font-size:8.46667px;line-height:1.25;font-family:sans-serif;fill:#999999;stroke-width:0.264583" + x="23.457415" + y="33.02087" + id="text3750-3"><tspan + sodipodi:role="line" + id="tspan3748-2" + style="fill:#999999;stroke-width:0.264583" + x="23.457415" + y="33.02087">$\not\sqsupseteq \{a\}$</tspan></text> + <text + xml:space="preserve" + style="font-size:8.46667px;line-height:1.25;font-family:sans-serif;fill:#999999;stroke-width:0.264583" + x="23.457415" + y="41.972523" + id="text3750-0"><tspan + sodipodi:role="line" + id="tspan3748-6" + style="fill:#999999;stroke-width:0.264583" + x="23.457415" + y="41.972523">$\not\sqsupseteq \{a\}$</tspan></text> + </g> +</svg> diff --git a/doc/talks/2023-01-18-tocatta/assets/lattice3.svg b/doc/talks/2023-01-18-tocatta/assets/lattice3.svg new file mode 100644 index 00000000..640dc468 --- /dev/null +++ b/doc/talks/2023-01-18-tocatta/assets/lattice3.svg @@ -0,0 +1,515 @@ +<?xml version="1.0" encoding="UTF-8" standalone="no"?> +<!-- Created with Inkscape (http://www.inkscape.org/) --> + +<svg + width="1000" + height="400" + viewBox="0 0 264.58333 105.83333" + version="1.1" + id="svg5" + inkscape:version="1.2.2 (b0a8486541, 2022-12-01)" + sodipodi:docname="lattice3.svg" + 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="namedview7" + pagecolor="#ffffff" + bordercolor="#666666" + borderopacity="1.0" + inkscape:showpageshadow="2" + inkscape:pageopacity="0.0" + inkscape:pagecheckerboard="0" + inkscape:deskcolor="#d1d1d1" + inkscape:document-units="mm" + showgrid="false" + inkscape:zoom="1.4734708" + inkscape:cx="324.06479" + inkscape:cy="168.98876" + inkscape:window-width="1920" + inkscape:window-height="999" + inkscape:window-x="0" + inkscape:window-y="0" + inkscape:window-maximized="1" + inkscape:current-layer="layer2" /> + <defs + id="defs2"> + <marker + style="overflow:visible" + id="Arrow2" + refX="0" + refY="0" + orient="auto-start-reverse" + inkscape:stockid="Arrow2" + markerWidth="7.6999998" + markerHeight="5.5999999" + viewBox="0 0 7.7 5.6" + inkscape:isstock="true" + inkscape:collect="always" + preserveAspectRatio="xMidYMid"> + <path + transform="scale(0.7)" + d="M -2,-4 9,0 -2,4 c 2,-2.33 2,-5.66 0,-8 z" + style="fill:context-stroke;fill-rule:evenodd;stroke:none" + id="arrow2L" /> + </marker> + <marker + style="overflow:visible" + id="Arrow2-9" + refX="0" + refY="0" + orient="auto-start-reverse" + inkscape:stockid="Arrow2" + markerWidth="7.6999998" + markerHeight="5.5999999" + viewBox="0 0 7.7 5.6" + inkscape:isstock="true" + inkscape:collect="always" + preserveAspectRatio="xMidYMid"> + <path + transform="scale(0.7)" + d="M -2,-4 9,0 -2,4 c 2,-2.33 2,-5.66 0,-8 z" + style="fill:context-stroke;fill-rule:evenodd;stroke:none" + id="arrow2L-1" /> + </marker> + <marker + style="overflow:visible" + id="Arrow2-9-7" + refX="0" + refY="0" + orient="auto-start-reverse" + inkscape:stockid="Arrow2" + markerWidth="7.6999998" + markerHeight="5.5999999" + viewBox="0 0 7.7 5.6" + inkscape:isstock="true" + inkscape:collect="always" + preserveAspectRatio="xMidYMid"> + <path + transform="scale(0.7)" + d="M -2,-4 9,0 -2,4 c 2,-2.33 2,-5.66 0,-8 z" + style="fill:context-stroke;fill-rule:evenodd;stroke:none" + id="arrow2L-1-0" /> + </marker> + <marker + style="overflow:visible" + id="Arrow2-93" + refX="0" + refY="0" + orient="auto-start-reverse" + inkscape:stockid="Arrow2" + markerWidth="7.6999998" + markerHeight="5.5999999" + viewBox="0 0 7.7 5.6" + inkscape:isstock="true" + inkscape:collect="always" + preserveAspectRatio="xMidYMid"> + <path + transform="scale(0.7)" + d="M -2,-4 9,0 -2,4 c 2,-2.33 2,-5.66 0,-8 z" + style="fill:context-stroke;fill-rule:evenodd;stroke:none" + id="arrow2L-6" /> + </marker> + <marker + style="overflow:visible" + id="Arrow2-9-7-2" + refX="0" + refY="0" + orient="auto-start-reverse" + inkscape:stockid="Arrow2" + markerWidth="7.6999998" + markerHeight="5.5999999" + viewBox="0 0 7.7 5.6" + inkscape:isstock="true" + inkscape:collect="always" + preserveAspectRatio="xMidYMid"> + <path + transform="scale(0.7)" + d="M -2,-4 9,0 -2,4 c 2,-2.33 2,-5.66 0,-8 z" + style="fill:context-stroke;fill-rule:evenodd;stroke:none" + id="arrow2L-1-0-6" /> + </marker> + <marker + style="overflow:visible" + id="Arrow2-93-1" + refX="0" + refY="0" + orient="auto-start-reverse" + inkscape:stockid="Arrow2" + markerWidth="7.6999998" + markerHeight="5.5999999" + viewBox="0 0 7.7 5.6" + inkscape:isstock="true" + inkscape:collect="always" + preserveAspectRatio="xMidYMid"> + <path + transform="scale(0.7)" + d="M -2,-4 9,0 -2,4 c 2,-2.33 2,-5.66 0,-8 z" + style="fill:context-stroke;fill-rule:evenodd;stroke:none" + id="arrow2L-6-8" /> + </marker> + <marker + style="overflow:visible" + id="Arrow2-9-75" + refX="0" + refY="0" + orient="auto-start-reverse" + inkscape:stockid="Arrow2" + markerWidth="7.6999998" + markerHeight="5.5999999" + viewBox="0 0 7.7 5.6" + inkscape:isstock="true" + inkscape:collect="always" + preserveAspectRatio="xMidYMid"> + <path + transform="scale(0.7)" + d="M -2,-4 9,0 -2,4 c 2,-2.33 2,-5.66 0,-8 z" + style="fill:context-stroke;fill-rule:evenodd;stroke:none" + id="arrow2L-1-9" /> + </marker> + <marker + style="overflow:visible" + id="Arrow2-9-75-2" + refX="0" + refY="0" + orient="auto-start-reverse" + inkscape:stockid="Arrow2" + markerWidth="7.6999998" + markerHeight="5.5999999" + viewBox="0 0 7.7 5.6" + inkscape:isstock="true" + inkscape:collect="always" + preserveAspectRatio="xMidYMid"> + <path + transform="scale(0.7)" + d="M -2,-4 9,0 -2,4 c 2,-2.33 2,-5.66 0,-8 z" + style="fill:context-stroke;fill-rule:evenodd;stroke:none" + id="arrow2L-1-9-8" /> + </marker> + <marker + style="overflow:visible" + id="Arrow2-9-75-7" + refX="0" + refY="0" + orient="auto-start-reverse" + inkscape:stockid="Arrow2" + markerWidth="7.6999998" + markerHeight="5.5999999" + viewBox="0 0 7.7 5.6" + inkscape:isstock="true" + inkscape:collect="always" + preserveAspectRatio="xMidYMid"> + <path + transform="scale(0.7)" + d="M -2,-4 9,0 -2,4 c 2,-2.33 2,-5.66 0,-8 z" + style="fill:context-stroke;fill-rule:evenodd;stroke:none" + id="arrow2L-1-9-3" /> + </marker> + <marker + style="overflow:visible" + id="Arrow2-9-75-7-1" + refX="0" + refY="0" + orient="auto-start-reverse" + inkscape:stockid="Arrow2" + markerWidth="7.6999998" + markerHeight="5.5999999" + viewBox="0 0 7.7 5.6" + inkscape:isstock="true" + inkscape:collect="always" + preserveAspectRatio="xMidYMid"> + <path + transform="scale(0.7)" + d="M -2,-4 9,0 -2,4 c 2,-2.33 2,-5.66 0,-8 z" + style="fill:context-stroke;fill-rule:evenodd;stroke:none" + id="arrow2L-1-9-3-2" /> + </marker> + <marker + style="overflow:visible" + id="Arrow2-93-1-4" + refX="0" + refY="0" + orient="auto-start-reverse" + inkscape:stockid="Arrow2" + markerWidth="7.6999998" + markerHeight="5.5999999" + viewBox="0 0 7.7 5.6" + inkscape:isstock="true" + inkscape:collect="always" + preserveAspectRatio="xMidYMid"> + <path + transform="scale(0.7)" + d="M -2,-4 9,0 -2,4 c 2,-2.33 2,-5.66 0,-8 z" + style="fill:context-stroke;fill-rule:evenodd;stroke:none" + id="arrow2L-6-8-7" /> + </marker> + <marker + style="overflow:visible" + id="Arrow2-9-7-2-8" + refX="0" + refY="0" + orient="auto-start-reverse" + inkscape:stockid="Arrow2" + markerWidth="7.6999998" + markerHeight="5.5999999" + viewBox="0 0 7.7 5.6" + inkscape:isstock="true" + inkscape:collect="always" + preserveAspectRatio="xMidYMid"> + <path + transform="scale(0.7)" + d="M -2,-4 9,0 -2,4 c 2,-2.33 2,-5.66 0,-8 z" + style="fill:context-stroke;fill-rule:evenodd;stroke:none" + id="arrow2L-1-0-6-4" /> + </marker> + </defs> + <g + inkscape:label="Layer 1" + inkscape:groupmode="layer" + id="layer1" + sodipodi:insensitive="true"> + <rect + style="fill:#ffffff;stroke:none;stroke-width:1;stop-color:#000000" + id="rect288" + width="209.84705" + height="104.42732" + x="0.77790999" + y="0.93738818" /> + </g> + <g + inkscape:groupmode="layer" + id="layer2" + inkscape:label="Layer 2"> + <text + xml:space="preserve" + style="font-size:8.46667px;line-height:1.25;font-family:sans-serif;text-align:center;text-anchor:middle;stroke-width:0.264583;fill:#000000" + x="164.56372" + y="99.307442" + id="text951"><tspan + sodipodi:role="line" + id="tspan949" + style="stroke-width:0.264583;fill:#000000" + x="164.56372" + y="99.307442">$\{\}$</tspan></text> + <text + xml:space="preserve" + style="font-size:8.46667px;line-height:1.25;font-family:sans-serif;text-align:center;text-anchor:middle;stroke-width:0.264583;fill:#000000" + x="164.56372" + y="13.151893" + id="text1005"><tspan + sodipodi:role="line" + id="tspan1003" + style="stroke-width:0.264583;fill:#000000" + x="164.56372" + y="13.151893">$\{a,b,c\}$</tspan></text> + <g + id="g1175" + transform="translate(51.996784,3.5774043)" + style="fill:#000000"> + <text + xml:space="preserve" + style="font-size:8.46667px;line-height:1.25;font-family:sans-serif;text-align:center;text-anchor:middle;stroke-width:0.264583;fill:#000000" + x="49.27084" + y="67.008698" + id="text1009"><tspan + sodipodi:role="line" + id="tspan1007" + style="stroke-width:0.264583;fill:#000000" + x="49.27084" + y="67.008698">$\{a\}$</tspan></text> + <text + xml:space="preserve" + style="font-size:8.46667px;line-height:1.25;font-family:sans-serif;text-align:center;text-anchor:middle;stroke-width:0.264583;fill:#000000" + x="112.90984" + y="67.017166" + id="text1009-3"><tspan + sodipodi:role="line" + id="tspan1007-6" + style="stroke-width:0.264583;fill:#000000" + x="112.90984" + y="67.017166">$\{b\}$</tspan></text> + <text + xml:space="preserve" + style="font-size:8.46667px;line-height:1.25;font-family:sans-serif;text-align:center;text-anchor:middle;stroke-width:0.264583;fill:#000000" + x="176.20593" + y="67.008698" + id="text1009-7"><tspan + sodipodi:role="line" + id="tspan1007-5" + style="stroke-width:0.264583;fill:#000000" + x="176.20593" + y="67.008698">$\{c\}$</tspan></text> + </g> + <g + id="g1183" + transform="translate(51.996784,1.0317046)" + style="fill:#000000"> + <text + xml:space="preserve" + style="font-size:8.46667px;line-height:1.25;font-family:sans-serif;text-align:center;text-anchor:middle;stroke-width:0.264583;fill:#000000" + x="112.90984" + y="40.841526" + id="text1117"><tspan + sodipodi:role="line" + id="tspan1115" + style="stroke-width:0.264583;fill:#000000" + x="112.90984" + y="40.841526">$\{a,c\}$</tspan></text> + <text + xml:space="preserve" + style="font-size:8.46667px;line-height:1.25;font-family:sans-serif;text-align:center;text-anchor:middle;stroke-width:0.264583;fill:#000000" + x="49.27084" + y="40.841526" + id="text1117-3"><tspan + sodipodi:role="line" + id="tspan1115-5" + style="stroke-width:0.264583;fill:#000000" + x="49.27084" + y="40.841526">$\{a,b\}$</tspan></text> + <text + xml:space="preserve" + style="font-size:8.46667px;line-height:1.25;font-family:sans-serif;text-align:center;text-anchor:middle;stroke-width:0.264583;fill:#000000" + x="176.20593" + y="40.841526" + id="text1117-6"><tspan + sodipodi:role="line" + id="tspan1115-2" + style="stroke-width:0.264583;fill:#000000" + x="176.20593" + y="40.841526">$\{b,c\}$</tspan></text> + </g> + <path + style="fill:none;stroke:#000000;stroke-width:0.5;stroke-linecap:butt;stroke-linejoin:miter;stroke-dasharray:none;stroke-opacity:1;marker-end:url(#Arrow2)" + d="M 153.33622,90.367682 118.34198,73.428915" + id="path1300" /> + <path + style="fill:none;stroke:#000000;stroke-width:0.5;stroke-linecap:butt;stroke-linejoin:miter;stroke-dasharray:none;stroke-opacity:1;marker-end:url(#Arrow2-9)" + d="M 177.46016,90.367682 212.4544,73.428915" + id="path1300-2" /> + <path + style="fill:none;stroke:#000000;stroke-width:0.5;stroke-linecap:butt;stroke-linejoin:miter;stroke-dasharray:none;stroke-opacity:1;marker-end:url(#Arrow2-93)" + d="M 153.33622,61.655656 118.34198,44.716889" + id="path1300-0" /> + <path + style="fill:none;stroke:#000000;stroke-width:0.5;stroke-linecap:butt;stroke-linejoin:miter;stroke-dasharray:none;stroke-opacity:1;marker-end:url(#Arrow2-9-7)" + d="M 177.46016,61.655656 212.4544,44.716889" + id="path1300-2-6" /> + <path + style="fill:none;stroke:#000000;stroke-width:0.5;stroke-linecap:butt;stroke-linejoin:miter;stroke-dasharray:none;stroke-opacity:1;marker-end:url(#Arrow2-93-1)" + d="M 118.34198,61.655656 153.33622,44.716889" + id="path1300-0-7" /> + <path + style="fill:none;stroke:#000000;stroke-width:0.5;stroke-linecap:butt;stroke-linejoin:miter;stroke-dasharray:none;stroke-opacity:1;marker-end:url(#Arrow2-9-7-2)" + d="M 212.4544,61.655656 177.46016,44.716889" + id="path1300-2-6-9" /> + <path + style="fill:none;stroke:#000000;stroke-width:0.5;stroke-linecap:butt;stroke-linejoin:miter;stroke-dasharray:none;stroke-opacity:1;marker-end:url(#Arrow2-93-1-4)" + d="M 118.34198,34.227412 153.33622,17.288645" + id="path1300-0-7-5" /> + <path + style="fill:none;stroke:#000000;stroke-width:0.5;stroke-linecap:butt;stroke-linejoin:miter;stroke-dasharray:none;stroke-opacity:1;marker-end:url(#Arrow2-9-7-2-8)" + d="M 212.4544,34.227412 177.46016,17.288645" + id="path1300-2-6-9-0" /> + <path + style="fill:none;stroke:#000000;stroke-width:0.5;stroke-linecap:butt;stroke-linejoin:miter;stroke-dasharray:none;stroke-opacity:1;marker-end:url(#Arrow2-9-75)" + d="m 228.52843,61.091809 0.33313,-12.554874 m -0.33313,12.554874 0.33313,-12.554874" + id="path1300-2-2" + sodipodi:nodetypes="cc" /> + <path + style="fill:none;stroke:#000000;stroke-width:0.5;stroke-linecap:butt;stroke-linejoin:miter;stroke-dasharray:none;stroke-opacity:1;marker-end:url(#Arrow2-9-75-2)" + d="m 101.90418,61.091809 0.33313,-12.554874 m -0.33313,12.554874 0.33313,-12.554874" + id="path1300-2-2-9" + sodipodi:nodetypes="cc" /> + <path + style="fill:none;stroke:#000000;stroke-width:0.5;stroke-linecap:butt;stroke-linejoin:miter;stroke-dasharray:none;stroke-opacity:1;marker-end:url(#Arrow2-9-75-7)" + d="m 165.29305,89.571762 0.33313,-12.554874 m -0.33313,12.554874 0.33313,-12.554874" + id="path1300-2-2-6" + sodipodi:nodetypes="cc" /> + <path + style="fill:none;stroke:#000000;stroke-width:0.5;stroke-linecap:butt;stroke-linejoin:miter;stroke-dasharray:none;stroke-opacity:1;marker-end:url(#Arrow2-9-75-7-1)" + d="m 165.29305,32.445235 0.33313,-12.554874 m -0.33313,12.554874 0.33313,-12.554874" + id="path1300-2-2-6-9" + sodipodi:nodetypes="cc" /> + <circle + style="fill:#ff0000;stroke:none;stroke-width:0.499999;stroke-dasharray:none;stop-color:#000000" + id="path3663" + cx="147.35568" + cy="95.24971" + r="2.7302806" /> + <circle + style="fill:#008000;stroke:none;stroke-width:0.499999;stroke-dasharray:none;stop-color:#000000" + id="path3663-3" + cx="139.48744" + cy="95.24971" + r="2.7302806" /> + <circle + style="fill:#800080;stroke:none;stroke-width:0.499999;stroke-dasharray:none;stop-color:#000000" + id="path3663-6" + cx="119.58919" + cy="67.645035" + r="2.7302806" /> + <circle + style="fill:#ff0000;stroke:none;stroke-width:0.499999;stroke-dasharray:none;stop-color:#000000" + id="path3663-1" + cx="18.004833" + cy="39.402473" + r="2.7302806" /> + <circle + style="fill:#008000;stroke:none;stroke-width:0.499999;stroke-dasharray:none;stop-color:#000000" + id="path3663-3-0" + cx="18.004833" + cy="30.371933" + r="2.7302806" /> + <circle + style="fill:#800080;stroke:none;stroke-width:0.499999;stroke-dasharray:none;stop-color:#000000" + id="path3663-6-6" + cx="18.004833" + cy="21.341394" + r="2.7302806" /> + <text + xml:space="preserve" + style="font-size:8.46667px;line-height:1.25;font-family:sans-serif;stroke-width:0.264583;fill:#000000" + x="6.9525447" + y="13.702217" + id="text3707"><tspan + sodipodi:role="line" + id="tspan3705" + style="stroke-width:0.264583;fill:#000000" + x="6.9525447" + y="13.702217">$write(\{a\})$:</tspan></text> + <text + xml:space="preserve" + style="font-size:8.46667px;line-height:1.25;font-family:sans-serif;fill:#000000;stroke-width:0.264583" + x="23.457415" + y="24.042637" + id="text3750"><tspan + sodipodi:role="line" + id="tspan3748" + style="fill:#000000;stroke-width:0.264583" + x="23.457415" + y="24.042637">$\sqsupseteq \{a\} \to$ OK</tspan></text> + <text + xml:space="preserve" + style="font-size:8.46667px;line-height:1.25;font-family:sans-serif;fill:#999999;stroke-width:0.264583" + x="23.457415" + y="33.02087" + id="text3750-3"><tspan + sodipodi:role="line" + id="tspan3748-2" + style="fill:#999999;stroke-width:0.264583" + x="23.457415" + y="33.02087">$\not\sqsupseteq \{a\}$</tspan></text> + <text + xml:space="preserve" + style="font-size:8.46667px;line-height:1.25;font-family:sans-serif;fill:#999999;stroke-width:0.264583" + x="23.457415" + y="41.972523" + id="text3750-0"><tspan + sodipodi:role="line" + id="tspan3748-6" + style="fill:#999999;stroke-width:0.264583" + x="23.457415" + y="41.972523">$\not\sqsupseteq \{a\}$</tspan></text> + </g> +</svg> diff --git a/doc/talks/2023-01-18-tocatta/assets/lattice4.svg b/doc/talks/2023-01-18-tocatta/assets/lattice4.svg new file mode 100644 index 00000000..b2a99e28 --- /dev/null +++ b/doc/talks/2023-01-18-tocatta/assets/lattice4.svg @@ -0,0 +1,525 @@ +<?xml version="1.0" encoding="UTF-8" standalone="no"?> +<!-- Created with Inkscape (http://www.inkscape.org/) --> + +<svg + width="1000" + height="400" + viewBox="0 0 264.58333 105.83333" + version="1.1" + id="svg5" + inkscape:version="1.2.2 (b0a8486541, 2022-12-01)" + sodipodi:docname="lattice4.svg" + 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="namedview7" + pagecolor="#ffffff" + bordercolor="#666666" + borderopacity="1.0" + inkscape:showpageshadow="2" + inkscape:pageopacity="0.0" + inkscape:pagecheckerboard="0" + inkscape:deskcolor="#d1d1d1" + inkscape:document-units="mm" + showgrid="false" + inkscape:zoom="0.73673541" + inkscape:cx="287.07728" + inkscape:cy="294.54265" + inkscape:window-width="1920" + inkscape:window-height="999" + inkscape:window-x="0" + inkscape:window-y="0" + inkscape:window-maximized="1" + inkscape:current-layer="layer2" /> + <defs + id="defs2"> + <marker + style="overflow:visible" + id="Arrow2" + refX="0" + refY="0" + orient="auto-start-reverse" + inkscape:stockid="Arrow2" + markerWidth="7.6999998" + markerHeight="5.5999999" + viewBox="0 0 7.7 5.6" + inkscape:isstock="true" + inkscape:collect="always" + preserveAspectRatio="xMidYMid"> + <path + transform="scale(0.7)" + d="M -2,-4 9,0 -2,4 c 2,-2.33 2,-5.66 0,-8 z" + style="fill:context-stroke;fill-rule:evenodd;stroke:none" + id="arrow2L" /> + </marker> + <marker + style="overflow:visible" + id="Arrow2-9" + refX="0" + refY="0" + orient="auto-start-reverse" + inkscape:stockid="Arrow2" + markerWidth="7.6999998" + markerHeight="5.5999999" + viewBox="0 0 7.7 5.6" + inkscape:isstock="true" + inkscape:collect="always" + preserveAspectRatio="xMidYMid"> + <path + transform="scale(0.7)" + d="M -2,-4 9,0 -2,4 c 2,-2.33 2,-5.66 0,-8 z" + style="fill:context-stroke;fill-rule:evenodd;stroke:none" + id="arrow2L-1" /> + </marker> + <marker + style="overflow:visible" + id="Arrow2-9-7" + refX="0" + refY="0" + orient="auto-start-reverse" + inkscape:stockid="Arrow2" + markerWidth="7.6999998" + markerHeight="5.5999999" + viewBox="0 0 7.7 5.6" + inkscape:isstock="true" + inkscape:collect="always" + preserveAspectRatio="xMidYMid"> + <path + transform="scale(0.7)" + d="M -2,-4 9,0 -2,4 c 2,-2.33 2,-5.66 0,-8 z" + style="fill:context-stroke;fill-rule:evenodd;stroke:none" + id="arrow2L-1-0" /> + </marker> + <marker + style="overflow:visible" + id="Arrow2-93" + refX="0" + refY="0" + orient="auto-start-reverse" + inkscape:stockid="Arrow2" + markerWidth="7.6999998" + markerHeight="5.5999999" + viewBox="0 0 7.7 5.6" + inkscape:isstock="true" + inkscape:collect="always" + preserveAspectRatio="xMidYMid"> + <path + transform="scale(0.7)" + d="M -2,-4 9,0 -2,4 c 2,-2.33 2,-5.66 0,-8 z" + style="fill:context-stroke;fill-rule:evenodd;stroke:none" + id="arrow2L-6" /> + </marker> + <marker + style="overflow:visible" + id="Arrow2-9-7-2" + refX="0" + refY="0" + orient="auto-start-reverse" + inkscape:stockid="Arrow2" + markerWidth="7.6999998" + markerHeight="5.5999999" + viewBox="0 0 7.7 5.6" + inkscape:isstock="true" + inkscape:collect="always" + preserveAspectRatio="xMidYMid"> + <path + transform="scale(0.7)" + d="M -2,-4 9,0 -2,4 c 2,-2.33 2,-5.66 0,-8 z" + style="fill:context-stroke;fill-rule:evenodd;stroke:none" + id="arrow2L-1-0-6" /> + </marker> + <marker + style="overflow:visible" + id="Arrow2-93-1" + refX="0" + refY="0" + orient="auto-start-reverse" + inkscape:stockid="Arrow2" + markerWidth="7.6999998" + markerHeight="5.5999999" + viewBox="0 0 7.7 5.6" + inkscape:isstock="true" + inkscape:collect="always" + preserveAspectRatio="xMidYMid"> + <path + transform="scale(0.7)" + d="M -2,-4 9,0 -2,4 c 2,-2.33 2,-5.66 0,-8 z" + style="fill:context-stroke;fill-rule:evenodd;stroke:none" + id="arrow2L-6-8" /> + </marker> + <marker + style="overflow:visible" + id="Arrow2-9-75" + refX="0" + refY="0" + orient="auto-start-reverse" + inkscape:stockid="Arrow2" + markerWidth="7.6999998" + markerHeight="5.5999999" + viewBox="0 0 7.7 5.6" + inkscape:isstock="true" + inkscape:collect="always" + preserveAspectRatio="xMidYMid"> + <path + transform="scale(0.7)" + d="M -2,-4 9,0 -2,4 c 2,-2.33 2,-5.66 0,-8 z" + style="fill:context-stroke;fill-rule:evenodd;stroke:none" + id="arrow2L-1-9" /> + </marker> + <marker + style="overflow:visible" + id="Arrow2-9-75-2" + refX="0" + refY="0" + orient="auto-start-reverse" + inkscape:stockid="Arrow2" + markerWidth="7.6999998" + markerHeight="5.5999999" + viewBox="0 0 7.7 5.6" + inkscape:isstock="true" + inkscape:collect="always" + preserveAspectRatio="xMidYMid"> + <path + transform="scale(0.7)" + d="M -2,-4 9,0 -2,4 c 2,-2.33 2,-5.66 0,-8 z" + style="fill:context-stroke;fill-rule:evenodd;stroke:none" + id="arrow2L-1-9-8" /> + </marker> + <marker + style="overflow:visible" + id="Arrow2-9-75-7" + refX="0" + refY="0" + orient="auto-start-reverse" + inkscape:stockid="Arrow2" + markerWidth="7.6999998" + markerHeight="5.5999999" + viewBox="0 0 7.7 5.6" + inkscape:isstock="true" + inkscape:collect="always" + preserveAspectRatio="xMidYMid"> + <path + transform="scale(0.7)" + d="M -2,-4 9,0 -2,4 c 2,-2.33 2,-5.66 0,-8 z" + style="fill:context-stroke;fill-rule:evenodd;stroke:none" + id="arrow2L-1-9-3" /> + </marker> + <marker + style="overflow:visible" + id="Arrow2-9-75-7-1" + refX="0" + refY="0" + orient="auto-start-reverse" + inkscape:stockid="Arrow2" + markerWidth="7.6999998" + markerHeight="5.5999999" + viewBox="0 0 7.7 5.6" + inkscape:isstock="true" + inkscape:collect="always" + preserveAspectRatio="xMidYMid"> + <path + transform="scale(0.7)" + d="M -2,-4 9,0 -2,4 c 2,-2.33 2,-5.66 0,-8 z" + style="fill:context-stroke;fill-rule:evenodd;stroke:none" + id="arrow2L-1-9-3-2" /> + </marker> + <marker + style="overflow:visible" + id="Arrow2-93-1-4" + refX="0" + refY="0" + orient="auto-start-reverse" + inkscape:stockid="Arrow2" + markerWidth="7.6999998" + markerHeight="5.5999999" + viewBox="0 0 7.7 5.6" + inkscape:isstock="true" + inkscape:collect="always" + preserveAspectRatio="xMidYMid"> + <path + transform="scale(0.7)" + d="M -2,-4 9,0 -2,4 c 2,-2.33 2,-5.66 0,-8 z" + style="fill:context-stroke;fill-rule:evenodd;stroke:none" + id="arrow2L-6-8-7" /> + </marker> + <marker + style="overflow:visible" + id="Arrow2-9-7-2-8" + refX="0" + refY="0" + orient="auto-start-reverse" + inkscape:stockid="Arrow2" + markerWidth="7.6999998" + markerHeight="5.5999999" + viewBox="0 0 7.7 5.6" + inkscape:isstock="true" + inkscape:collect="always" + preserveAspectRatio="xMidYMid"> + <path + transform="scale(0.7)" + d="M -2,-4 9,0 -2,4 c 2,-2.33 2,-5.66 0,-8 z" + style="fill:context-stroke;fill-rule:evenodd;stroke:none" + id="arrow2L-1-0-6-4" /> + </marker> + </defs> + <g + inkscape:label="Layer 1" + inkscape:groupmode="layer" + id="layer1" + sodipodi:insensitive="true"> + <rect + style="fill:#ffffff;stroke:none;stroke-width:1;stop-color:#000000" + id="rect288" + width="209.84705" + height="104.42732" + x="0.77790999" + y="0.93738818" /> + </g> + <g + inkscape:groupmode="layer" + id="layer2" + inkscape:label="Layer 2"> + <text + xml:space="preserve" + style="font-size:8.46667px;line-height:1.25;font-family:sans-serif;text-align:center;text-anchor:middle;stroke-width:0.264583;fill:#000000" + x="164.56372" + y="99.307442" + id="text951"><tspan + sodipodi:role="line" + id="tspan949" + style="stroke-width:0.264583;fill:#000000" + x="164.56372" + y="99.307442">$\{\}$</tspan></text> + <text + xml:space="preserve" + style="font-size:8.46667px;line-height:1.25;font-family:sans-serif;text-align:center;text-anchor:middle;stroke-width:0.264583;fill:#000000" + x="164.56372" + y="13.151893" + id="text1005"><tspan + sodipodi:role="line" + id="tspan1003" + style="stroke-width:0.264583;fill:#000000" + x="164.56372" + y="13.151893">$\{a,b,c\}$</tspan></text> + <g + id="g1175" + transform="translate(51.996784,3.5774043)"> + <text + xml:space="preserve" + style="font-size:8.46667px;line-height:1.25;font-family:sans-serif;text-align:center;text-anchor:middle;stroke-width:0.264583;fill:#000000" + x="49.27084" + y="67.008698" + id="text1009"><tspan + sodipodi:role="line" + id="tspan1007" + style="stroke-width:0.264583;fill:#000000" + x="49.27084" + y="67.008698">$\{a\}$</tspan></text> + <text + xml:space="preserve" + style="font-size:8.46667px;line-height:1.25;font-family:sans-serif;text-align:center;text-anchor:middle;stroke-width:0.264583;fill:#000000" + x="112.90984" + y="67.017166" + id="text1009-3"><tspan + sodipodi:role="line" + id="tspan1007-6" + style="stroke-width:0.264583;fill:#000000" + x="112.90984" + y="67.017166">$\{b\}$</tspan></text> + <text + xml:space="preserve" + style="font-size:8.46667px;line-height:1.25;font-family:sans-serif;text-align:center;text-anchor:middle;stroke-width:0.264583;fill:#000000" + x="176.20593" + y="67.008698" + id="text1009-7"><tspan + sodipodi:role="line" + id="tspan1007-5" + style="stroke-width:0.264583;fill:#000000" + x="176.20593" + y="67.008698">$\{c\}$</tspan></text> + </g> + <g + id="g1183" + transform="translate(51.996784,1.0317046)" + style="fill:#000000"> + <text + xml:space="preserve" + style="font-size:8.46667px;line-height:1.25;font-family:sans-serif;text-align:center;text-anchor:middle;stroke-width:0.264583;fill:#000000" + x="112.90984" + y="40.841526" + id="text1117"><tspan + sodipodi:role="line" + id="tspan1115" + style="stroke-width:0.264583;fill:#000000" + x="112.90984" + y="40.841526">$\{a,c\}$</tspan></text> + <text + xml:space="preserve" + style="font-size:8.46667px;line-height:1.25;font-family:sans-serif;text-align:center;text-anchor:middle;stroke-width:0.264583;fill:#000000" + x="49.27084" + y="40.841526" + id="text1117-3"><tspan + sodipodi:role="line" + id="tspan1115-5" + style="stroke-width:0.264583;fill:#000000" + x="49.27084" + y="40.841526">$\{a,b\}$</tspan></text> + <text + xml:space="preserve" + style="font-size:8.46667px;line-height:1.25;font-family:sans-serif;text-align:center;text-anchor:middle;stroke-width:0.264583;fill:#000000" + x="176.20593" + y="40.841526" + id="text1117-6"><tspan + sodipodi:role="line" + id="tspan1115-2" + style="stroke-width:0.264583;fill:#000000" + x="176.20593" + y="40.841526">$\{b,c\}$</tspan></text> + </g> + <path + style="fill:none;stroke:#000000;stroke-width:0.5;stroke-linecap:butt;stroke-linejoin:miter;stroke-dasharray:none;stroke-opacity:1;marker-end:url(#Arrow2)" + d="M 153.33622,90.367682 118.34198,73.428915" + id="path1300" /> + <path + style="fill:none;stroke:#000000;stroke-width:0.5;stroke-linecap:butt;stroke-linejoin:miter;stroke-dasharray:none;stroke-opacity:1;marker-end:url(#Arrow2-9)" + d="M 177.46016,90.367682 212.4544,73.428915" + id="path1300-2" /> + <path + style="fill:none;stroke:#000000;stroke-width:0.5;stroke-linecap:butt;stroke-linejoin:miter;stroke-dasharray:none;stroke-opacity:1;marker-end:url(#Arrow2-93)" + d="M 153.33622,61.655656 118.34198,44.716889" + id="path1300-0" /> + <path + style="fill:none;stroke:#000000;stroke-width:0.5;stroke-linecap:butt;stroke-linejoin:miter;stroke-dasharray:none;stroke-opacity:1;marker-end:url(#Arrow2-9-7)" + d="M 177.46016,61.655656 212.4544,44.716889" + id="path1300-2-6" /> + <path + style="fill:none;stroke:#000000;stroke-width:0.5;stroke-linecap:butt;stroke-linejoin:miter;stroke-dasharray:none;stroke-opacity:1;marker-end:url(#Arrow2-93-1)" + d="M 118.34198,61.655656 153.33622,44.716889" + id="path1300-0-7" /> + <path + style="fill:none;stroke:#000000;stroke-width:0.5;stroke-linecap:butt;stroke-linejoin:miter;stroke-dasharray:none;stroke-opacity:1;marker-end:url(#Arrow2-9-7-2)" + d="M 212.4544,61.655656 177.46016,44.716889" + id="path1300-2-6-9" /> + <path + style="fill:none;stroke:#000000;stroke-width:0.5;stroke-linecap:butt;stroke-linejoin:miter;stroke-dasharray:none;stroke-opacity:1;marker-end:url(#Arrow2-93-1-4)" + d="M 118.34198,34.227412 153.33622,17.288645" + id="path1300-0-7-5" /> + <path + style="fill:none;stroke:#000000;stroke-width:0.5;stroke-linecap:butt;stroke-linejoin:miter;stroke-dasharray:none;stroke-opacity:1;marker-end:url(#Arrow2-9-7-2-8)" + d="M 212.4544,34.227412 177.46016,17.288645" + id="path1300-2-6-9-0" /> + <path + style="fill:none;stroke:#000000;stroke-width:0.5;stroke-linecap:butt;stroke-linejoin:miter;stroke-dasharray:none;stroke-opacity:1;marker-end:url(#Arrow2-9-75)" + d="m 228.52843,61.091809 0.33313,-12.554874 m -0.33313,12.554874 0.33313,-12.554874" + id="path1300-2-2" + sodipodi:nodetypes="cc" /> + <path + style="fill:none;stroke:#000000;stroke-width:0.5;stroke-linecap:butt;stroke-linejoin:miter;stroke-dasharray:none;stroke-opacity:1;marker-end:url(#Arrow2-9-75-2)" + d="m 101.90418,61.091809 0.33313,-12.554874 m -0.33313,12.554874 0.33313,-12.554874" + id="path1300-2-2-9" + sodipodi:nodetypes="cc" /> + <path + style="fill:none;stroke:#000000;stroke-width:0.5;stroke-linecap:butt;stroke-linejoin:miter;stroke-dasharray:none;stroke-opacity:1;marker-end:url(#Arrow2-9-75-7)" + d="m 165.29305,89.571762 0.33313,-12.554874 m -0.33313,12.554874 0.33313,-12.554874" + id="path1300-2-2-6" + sodipodi:nodetypes="cc" /> + <path + style="fill:none;stroke:#000000;stroke-width:0.5;stroke-linecap:butt;stroke-linejoin:miter;stroke-dasharray:none;stroke-opacity:1;marker-end:url(#Arrow2-9-75-7-1)" + d="m 165.29305,32.445235 0.33313,-12.554874 m -0.33313,12.554874 0.33313,-12.554874" + id="path1300-2-2-6-9" + sodipodi:nodetypes="cc" /> + <circle + style="fill:#ff0000;stroke:none;stroke-width:0.499999;stroke-dasharray:none;stop-color:#000000" + id="path3663" + cx="147.35568" + cy="95.24971" + r="2.7302806" /> + <circle + style="fill:#008000;stroke:none;stroke-width:0.499999;stroke-dasharray:none;stop-color:#000000" + id="path3663-3" + cx="126.08154" + cy="67.968384" + r="2.7302806" /> + <circle + style="fill:#800080;stroke:none;stroke-width:0.499999;stroke-dasharray:none;stop-color:#000000" + id="path3663-6" + cx="119.58919" + cy="67.645035" + r="2.7302806" /> + <circle + style="fill:#ff0000;stroke:none;stroke-width:0.499999;stroke-dasharray:none;stop-color:#000000" + id="path3663-1" + cx="18.004833" + cy="39.402473" + r="2.7302806" /> + <circle + style="fill:#008000;stroke:none;stroke-width:0.499999;stroke-dasharray:none;stop-color:#000000" + id="path3663-3-0" + cx="18.004833" + cy="30.371933" + r="2.7302806" /> + <circle + style="fill:#800080;stroke:none;stroke-width:0.499999;stroke-dasharray:none;stop-color:#000000" + id="path3663-6-6" + cx="18.004833" + cy="21.341394" + r="2.7302806" /> + <text + xml:space="preserve" + style="font-size:8.46667px;line-height:1.25;font-family:sans-serif;stroke-width:0.264583;fill:#000000" + x="6.9525447" + y="13.702217" + id="text3707"><tspan + sodipodi:role="line" + id="tspan3705" + style="stroke-width:0.264583;fill:#000000" + x="6.9525447" + y="13.702217">$write(\{a\})$:</tspan></text> + <text + xml:space="preserve" + style="font-size:8.46667px;line-height:1.25;font-family:sans-serif;fill:#000000;stroke-width:0.264583" + x="23.457415" + y="24.042637" + id="text3750"><tspan + sodipodi:role="line" + id="tspan3748" + style="fill:#000000;stroke-width:0.264583" + x="23.457415" + y="24.042637">$\sqsupseteq \{a\} \to$ OK</tspan></text> + <text + xml:space="preserve" + style="font-size:8.46667px;line-height:1.25;font-family:sans-serif;fill:#000000;stroke-width:0.264583" + x="23.457415" + y="33.02087" + id="text3750-3"><tspan + sodipodi:role="line" + id="tspan3748-2" + style="fill:#000000;stroke-width:0.264583" + x="23.457415" + y="33.02087">$\sqsupseteq \{a\} \to$ OK</tspan></text> + <text + xml:space="preserve" + style="font-size:8.46667px;line-height:1.25;font-family:sans-serif;fill:#999999;stroke-width:0.264583" + x="23.457415" + y="41.972523" + id="text3750-0"><tspan + sodipodi:role="line" + id="tspan3748-6" + style="fill:#999999;stroke-width:0.264583" + x="23.457415" + y="41.972523">$\not\sqsupseteq \{a\}$</tspan></text> + <text + xml:space="preserve" + style="font-size:8.46667px;line-height:1.25;font-family:sans-serif;fill:#000000;stroke-width:0.264583" + x="14.395845" + y="52.022549" + id="text4280"><tspan + sodipodi:role="line" + id="tspan4278" + style="fill:#000000;stroke-width:0.264583" + x="14.395845" + y="52.022549">return OK</tspan></text> + </g> +</svg> diff --git a/doc/talks/2023-01-18-tocatta/assets/lattice5.svg b/doc/talks/2023-01-18-tocatta/assets/lattice5.svg new file mode 100644 index 00000000..bc6b7195 --- /dev/null +++ b/doc/talks/2023-01-18-tocatta/assets/lattice5.svg @@ -0,0 +1,536 @@ +<?xml version="1.0" encoding="UTF-8" standalone="no"?> +<!-- Created with Inkscape (http://www.inkscape.org/) --> + +<svg + width="1000" + height="400" + viewBox="0 0 264.58333 105.83333" + version="1.1" + id="svg5" + inkscape:version="1.2.2 (b0a8486541, 2022-12-01)" + sodipodi:docname="lattice5.svg" + 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="namedview7" + pagecolor="#ffffff" + bordercolor="#666666" + borderopacity="1.0" + inkscape:showpageshadow="2" + inkscape:pageopacity="0.0" + inkscape:pagecheckerboard="0" + inkscape:deskcolor="#d1d1d1" + inkscape:document-units="mm" + showgrid="false" + inkscape:zoom="1.0419012" + inkscape:cx="276.89766" + inkscape:cy="254.34273" + inkscape:window-width="1920" + inkscape:window-height="999" + inkscape:window-x="0" + inkscape:window-y="0" + inkscape:window-maximized="1" + inkscape:current-layer="layer2" /> + <defs + id="defs2"> + <marker + style="overflow:visible" + id="Arrow2" + refX="0" + refY="0" + orient="auto-start-reverse" + inkscape:stockid="Arrow2" + markerWidth="7.6999998" + markerHeight="5.5999999" + viewBox="0 0 7.7 5.6" + inkscape:isstock="true" + inkscape:collect="always" + preserveAspectRatio="xMidYMid"> + <path + transform="scale(0.7)" + d="M -2,-4 9,0 -2,4 c 2,-2.33 2,-5.66 0,-8 z" + style="fill:context-stroke;fill-rule:evenodd;stroke:none" + id="arrow2L" /> + </marker> + <marker + style="overflow:visible" + id="Arrow2-9" + refX="0" + refY="0" + orient="auto-start-reverse" + inkscape:stockid="Arrow2" + markerWidth="7.6999998" + markerHeight="5.5999999" + viewBox="0 0 7.7 5.6" + inkscape:isstock="true" + inkscape:collect="always" + preserveAspectRatio="xMidYMid"> + <path + transform="scale(0.7)" + d="M -2,-4 9,0 -2,4 c 2,-2.33 2,-5.66 0,-8 z" + style="fill:context-stroke;fill-rule:evenodd;stroke:none" + id="arrow2L-1" /> + </marker> + <marker + style="overflow:visible" + id="Arrow2-9-7" + refX="0" + refY="0" + orient="auto-start-reverse" + inkscape:stockid="Arrow2" + markerWidth="7.6999998" + markerHeight="5.5999999" + viewBox="0 0 7.7 5.6" + inkscape:isstock="true" + inkscape:collect="always" + preserveAspectRatio="xMidYMid"> + <path + transform="scale(0.7)" + d="M -2,-4 9,0 -2,4 c 2,-2.33 2,-5.66 0,-8 z" + style="fill:context-stroke;fill-rule:evenodd;stroke:none" + id="arrow2L-1-0" /> + </marker> + <marker + style="overflow:visible" + id="Arrow2-93" + refX="0" + refY="0" + orient="auto-start-reverse" + inkscape:stockid="Arrow2" + markerWidth="7.6999998" + markerHeight="5.5999999" + viewBox="0 0 7.7 5.6" + inkscape:isstock="true" + inkscape:collect="always" + preserveAspectRatio="xMidYMid"> + <path + transform="scale(0.7)" + d="M -2,-4 9,0 -2,4 c 2,-2.33 2,-5.66 0,-8 z" + style="fill:context-stroke;fill-rule:evenodd;stroke:none" + id="arrow2L-6" /> + </marker> + <marker + style="overflow:visible" + id="Arrow2-9-7-2" + refX="0" + refY="0" + orient="auto-start-reverse" + inkscape:stockid="Arrow2" + markerWidth="7.6999998" + markerHeight="5.5999999" + viewBox="0 0 7.7 5.6" + inkscape:isstock="true" + inkscape:collect="always" + preserveAspectRatio="xMidYMid"> + <path + transform="scale(0.7)" + d="M -2,-4 9,0 -2,4 c 2,-2.33 2,-5.66 0,-8 z" + style="fill:context-stroke;fill-rule:evenodd;stroke:none" + id="arrow2L-1-0-6" /> + </marker> + <marker + style="overflow:visible" + id="Arrow2-93-1" + refX="0" + refY="0" + orient="auto-start-reverse" + inkscape:stockid="Arrow2" + markerWidth="7.6999998" + markerHeight="5.5999999" + viewBox="0 0 7.7 5.6" + inkscape:isstock="true" + inkscape:collect="always" + preserveAspectRatio="xMidYMid"> + <path + transform="scale(0.7)" + d="M -2,-4 9,0 -2,4 c 2,-2.33 2,-5.66 0,-8 z" + style="fill:context-stroke;fill-rule:evenodd;stroke:none" + id="arrow2L-6-8" /> + </marker> + <marker + style="overflow:visible" + id="Arrow2-9-75" + refX="0" + refY="0" + orient="auto-start-reverse" + inkscape:stockid="Arrow2" + markerWidth="7.6999998" + markerHeight="5.5999999" + viewBox="0 0 7.7 5.6" + inkscape:isstock="true" + inkscape:collect="always" + preserveAspectRatio="xMidYMid"> + <path + transform="scale(0.7)" + d="M -2,-4 9,0 -2,4 c 2,-2.33 2,-5.66 0,-8 z" + style="fill:context-stroke;fill-rule:evenodd;stroke:none" + id="arrow2L-1-9" /> + </marker> + <marker + style="overflow:visible" + id="Arrow2-9-75-2" + refX="0" + refY="0" + orient="auto-start-reverse" + inkscape:stockid="Arrow2" + markerWidth="7.6999998" + markerHeight="5.5999999" + viewBox="0 0 7.7 5.6" + inkscape:isstock="true" + inkscape:collect="always" + preserveAspectRatio="xMidYMid"> + <path + transform="scale(0.7)" + d="M -2,-4 9,0 -2,4 c 2,-2.33 2,-5.66 0,-8 z" + style="fill:context-stroke;fill-rule:evenodd;stroke:none" + id="arrow2L-1-9-8" /> + </marker> + <marker + style="overflow:visible" + id="Arrow2-9-75-7" + refX="0" + refY="0" + orient="auto-start-reverse" + inkscape:stockid="Arrow2" + markerWidth="7.6999998" + markerHeight="5.5999999" + viewBox="0 0 7.7 5.6" + inkscape:isstock="true" + inkscape:collect="always" + preserveAspectRatio="xMidYMid"> + <path + transform="scale(0.7)" + d="M -2,-4 9,0 -2,4 c 2,-2.33 2,-5.66 0,-8 z" + style="fill:context-stroke;fill-rule:evenodd;stroke:none" + id="arrow2L-1-9-3" /> + </marker> + <marker + style="overflow:visible" + id="Arrow2-9-75-7-1" + refX="0" + refY="0" + orient="auto-start-reverse" + inkscape:stockid="Arrow2" + markerWidth="7.6999998" + markerHeight="5.5999999" + viewBox="0 0 7.7 5.6" + inkscape:isstock="true" + inkscape:collect="always" + preserveAspectRatio="xMidYMid"> + <path + transform="scale(0.7)" + d="M -2,-4 9,0 -2,4 c 2,-2.33 2,-5.66 0,-8 z" + style="fill:context-stroke;fill-rule:evenodd;stroke:none" + id="arrow2L-1-9-3-2" /> + </marker> + <marker + style="overflow:visible" + id="Arrow2-93-1-4" + refX="0" + refY="0" + orient="auto-start-reverse" + inkscape:stockid="Arrow2" + markerWidth="7.6999998" + markerHeight="5.5999999" + viewBox="0 0 7.7 5.6" + inkscape:isstock="true" + inkscape:collect="always" + preserveAspectRatio="xMidYMid"> + <path + transform="scale(0.7)" + d="M -2,-4 9,0 -2,4 c 2,-2.33 2,-5.66 0,-8 z" + style="fill:context-stroke;fill-rule:evenodd;stroke:none" + id="arrow2L-6-8-7" /> + </marker> + <marker + style="overflow:visible" + id="Arrow2-9-7-2-8" + refX="0" + refY="0" + orient="auto-start-reverse" + inkscape:stockid="Arrow2" + markerWidth="7.6999998" + markerHeight="5.5999999" + viewBox="0 0 7.7 5.6" + inkscape:isstock="true" + inkscape:collect="always" + preserveAspectRatio="xMidYMid"> + <path + transform="scale(0.7)" + d="M -2,-4 9,0 -2,4 c 2,-2.33 2,-5.66 0,-8 z" + style="fill:context-stroke;fill-rule:evenodd;stroke:none" + id="arrow2L-1-0-6-4" /> + </marker> + </defs> + <g + inkscape:label="Layer 1" + inkscape:groupmode="layer" + id="layer1" + sodipodi:insensitive="true"> + <rect + style="fill:#ffffff;stroke:none;stroke-width:1;stop-color:#000000" + id="rect288" + width="209.84705" + height="104.42732" + x="0.77790999" + y="0.93738818" /> + </g> + <g + inkscape:groupmode="layer" + id="layer2" + inkscape:label="Layer 2"> + <text + xml:space="preserve" + style="font-size:8.46667px;line-height:1.25;font-family:sans-serif;text-align:center;text-anchor:middle;stroke-width:0.264583;fill:#000000" + x="164.56372" + y="99.307442" + id="text951"><tspan + sodipodi:role="line" + id="tspan949" + style="stroke-width:0.264583;fill:#000000" + x="164.56372" + y="99.307442">$\{\}$</tspan></text> + <text + xml:space="preserve" + style="font-size:8.46667px;line-height:1.25;font-family:sans-serif;text-align:center;text-anchor:middle;stroke-width:0.264583;fill:#000000" + x="164.56372" + y="13.151893" + id="text1005"><tspan + sodipodi:role="line" + id="tspan1003" + style="stroke-width:0.264583;fill:#000000" + x="164.56372" + y="13.151893">$\{a,b,c\}$</tspan></text> + <g + id="g1175" + transform="translate(51.996784,3.5774043)"> + <text + xml:space="preserve" + style="font-size:8.46667px;line-height:1.25;font-family:sans-serif;text-align:center;text-anchor:middle;stroke-width:0.264583;fill:#000000" + x="49.27084" + y="67.008698" + id="text1009"><tspan + sodipodi:role="line" + id="tspan1007" + style="stroke-width:0.264583;fill:#000000" + x="49.27084" + y="67.008698">$\{a\}$</tspan></text> + <text + xml:space="preserve" + style="font-size:8.46667px;line-height:1.25;font-family:sans-serif;text-align:center;text-anchor:middle;stroke-width:0.264583;fill:#000000" + x="112.90984" + y="67.017166" + id="text1009-3"><tspan + sodipodi:role="line" + id="tspan1007-6" + style="stroke-width:0.264583;fill:#000000" + x="112.90984" + y="67.017166">$\{b\}$</tspan></text> + <text + xml:space="preserve" + style="font-size:8.46667px;line-height:1.25;font-family:sans-serif;text-align:center;text-anchor:middle;stroke-width:0.264583;fill:#000000" + x="176.20593" + y="67.008698" + id="text1009-7"><tspan + sodipodi:role="line" + id="tspan1007-5" + style="stroke-width:0.264583;fill:#000000" + x="176.20593" + y="67.008698">$\{c\}$</tspan></text> + </g> + <g + id="g1183" + transform="translate(51.996784,1.0317046)" + style="fill:#000000"> + <text + xml:space="preserve" + style="font-size:8.46667px;line-height:1.25;font-family:sans-serif;text-align:center;text-anchor:middle;stroke-width:0.264583;fill:#000000" + x="112.90984" + y="40.841526" + id="text1117"><tspan + sodipodi:role="line" + id="tspan1115" + style="stroke-width:0.264583;fill:#000000" + x="112.90984" + y="40.841526">$\{a,c\}$</tspan></text> + <text + xml:space="preserve" + style="font-size:8.46667px;line-height:1.25;font-family:sans-serif;text-align:center;text-anchor:middle;stroke-width:0.264583;fill:#000000" + x="49.27084" + y="40.841526" + id="text1117-3"><tspan + sodipodi:role="line" + id="tspan1115-5" + style="stroke-width:0.264583;fill:#000000" + x="49.27084" + y="40.841526">$\{a,b\}$</tspan></text> + <text + xml:space="preserve" + style="font-size:8.46667px;line-height:1.25;font-family:sans-serif;text-align:center;text-anchor:middle;stroke-width:0.264583;fill:#000000" + x="176.20593" + y="40.841526" + id="text1117-6"><tspan + sodipodi:role="line" + id="tspan1115-2" + style="stroke-width:0.264583;fill:#000000" + x="176.20593" + y="40.841526">$\{b,c\}$</tspan></text> + </g> + <path + style="fill:none;stroke:#000000;stroke-width:0.5;stroke-linecap:butt;stroke-linejoin:miter;stroke-dasharray:none;stroke-opacity:1;marker-end:url(#Arrow2)" + d="M 153.33622,90.367682 118.34198,73.428915" + id="path1300" /> + <path + style="fill:none;stroke:#000000;stroke-width:0.5;stroke-linecap:butt;stroke-linejoin:miter;stroke-dasharray:none;stroke-opacity:1;marker-end:url(#Arrow2-9)" + d="M 177.46016,90.367682 212.4544,73.428915" + id="path1300-2" /> + <path + style="fill:none;stroke:#000000;stroke-width:0.5;stroke-linecap:butt;stroke-linejoin:miter;stroke-dasharray:none;stroke-opacity:1;marker-end:url(#Arrow2-93)" + d="M 153.33622,61.655656 118.34198,44.716889" + id="path1300-0" /> + <path + style="fill:none;stroke:#000000;stroke-width:0.5;stroke-linecap:butt;stroke-linejoin:miter;stroke-dasharray:none;stroke-opacity:1;marker-end:url(#Arrow2-9-7)" + d="M 177.46016,61.655656 212.4544,44.716889" + id="path1300-2-6" /> + <path + style="fill:none;stroke:#000000;stroke-width:0.5;stroke-linecap:butt;stroke-linejoin:miter;stroke-dasharray:none;stroke-opacity:1;marker-end:url(#Arrow2-93-1)" + d="M 118.34198,61.655656 153.33622,44.716889" + id="path1300-0-7" /> + <path + style="fill:none;stroke:#000000;stroke-width:0.5;stroke-linecap:butt;stroke-linejoin:miter;stroke-dasharray:none;stroke-opacity:1;marker-end:url(#Arrow2-9-7-2)" + d="M 212.4544,61.655656 177.46016,44.716889" + id="path1300-2-6-9" /> + <path + style="fill:none;stroke:#000000;stroke-width:0.5;stroke-linecap:butt;stroke-linejoin:miter;stroke-dasharray:none;stroke-opacity:1;marker-end:url(#Arrow2-93-1-4)" + d="M 118.34198,34.227412 153.33622,17.288645" + id="path1300-0-7-5" /> + <path + style="fill:none;stroke:#000000;stroke-width:0.5;stroke-linecap:butt;stroke-linejoin:miter;stroke-dasharray:none;stroke-opacity:1;marker-end:url(#Arrow2-9-7-2-8)" + d="M 212.4544,34.227412 177.46016,17.288645" + id="path1300-2-6-9-0" /> + <path + style="fill:none;stroke:#000000;stroke-width:0.5;stroke-linecap:butt;stroke-linejoin:miter;stroke-dasharray:none;stroke-opacity:1;marker-end:url(#Arrow2-9-75)" + d="m 228.52843,61.091809 0.33313,-12.554874 m -0.33313,12.554874 0.33313,-12.554874" + id="path1300-2-2" + sodipodi:nodetypes="cc" /> + <path + style="fill:none;stroke:#000000;stroke-width:0.5;stroke-linecap:butt;stroke-linejoin:miter;stroke-dasharray:none;stroke-opacity:1;marker-end:url(#Arrow2-9-75-2)" + d="m 101.90418,61.091809 0.33313,-12.554874 m -0.33313,12.554874 0.33313,-12.554874" + id="path1300-2-2-9" + sodipodi:nodetypes="cc" /> + <path + style="fill:none;stroke:#000000;stroke-width:0.5;stroke-linecap:butt;stroke-linejoin:miter;stroke-dasharray:none;stroke-opacity:1;marker-end:url(#Arrow2-9-75-7)" + d="m 165.29305,89.571762 0.33313,-12.554874 m -0.33313,12.554874 0.33313,-12.554874" + id="path1300-2-2-6" + sodipodi:nodetypes="cc" /> + <path + style="fill:none;stroke:#000000;stroke-width:0.5;stroke-linecap:butt;stroke-linejoin:miter;stroke-dasharray:none;stroke-opacity:1;marker-end:url(#Arrow2-9-75-7-1)" + d="m 165.29305,32.445235 0.33313,-12.554874 m -0.33313,12.554874 0.33313,-12.554874" + id="path1300-2-2-6-9" + sodipodi:nodetypes="cc" /> + <circle + style="fill:#ff0000;stroke:none;stroke-width:0.499999;stroke-dasharray:none;stop-color:#000000" + id="path3663" + cx="147.35568" + cy="95.24971" + r="2.7302806" /> + <circle + style="fill:#008000;stroke:none;stroke-width:0.499999;stroke-dasharray:none;stop-color:#000000" + id="path3663-3" + cx="126.08154" + cy="67.968384" + r="2.7302806" /> + <circle + style="fill:#800080;stroke:none;stroke-width:0.499999;stroke-dasharray:none;stop-color:#000000" + id="path3663-6" + cx="119.58919" + cy="67.645035" + r="2.7302806" /> + <circle + style="fill:#ff0000;stroke:none;stroke-width:0.499999;stroke-dasharray:none;stop-color:#000000" + id="path3663-1" + cx="18.004833" + cy="39.402473" + r="2.7302806" /> + <circle + style="fill:#008000;stroke:none;stroke-width:0.499999;stroke-dasharray:none;stop-color:#000000" + id="path3663-3-0" + cx="18.004833" + cy="30.371933" + r="2.7302806" /> + <circle + style="fill:#800080;stroke:none;stroke-width:0.499999;stroke-dasharray:none;stop-color:#000000" + id="path3663-6-6" + cx="18.004833" + cy="21.341394" + r="2.7302806" /> + <text + xml:space="preserve" + style="font-size:8.46667px;line-height:1.25;font-family:sans-serif;stroke-width:0.264583;fill:#000000" + x="6.9525447" + y="13.702217" + id="text3707"><tspan + sodipodi:role="line" + id="tspan3705" + style="stroke-width:0.264583;fill:#000000" + x="6.9525447" + y="13.702217">$write(\{a\})$:</tspan></text> + <text + xml:space="preserve" + style="font-size:8.46667px;line-height:1.25;font-family:sans-serif;fill:#000000;stroke-width:0.264583" + x="6.9525447" + y="65.261436" + id="text3707-1"><tspan + sodipodi:role="line" + id="tspan3705-5" + style="fill:#000000;stroke-width:0.264583" + x="6.9525447" + y="65.261436">$read()$:</tspan></text> + <text + xml:space="preserve" + style="font-size:8.46667px;line-height:1.25;font-family:sans-serif;fill:#000000;stroke-width:0.264583" + x="23.457415" + y="24.042637" + id="text3750"><tspan + sodipodi:role="line" + id="tspan3748" + style="fill:#000000;stroke-width:0.264583" + x="23.457415" + y="24.042637">$\sqsupseteq \{a\} \to$ OK</tspan></text> + <text + xml:space="preserve" + style="font-size:8.46667px;line-height:1.25;font-family:sans-serif;fill:#000000;stroke-width:0.264583" + x="23.457415" + y="33.02087" + id="text3750-3"><tspan + sodipodi:role="line" + id="tspan3748-2" + style="fill:#000000;stroke-width:0.264583" + x="23.457415" + y="33.02087">$\sqsupseteq \{a\} \to$ OK</tspan></text> + <text + xml:space="preserve" + style="font-size:8.46667px;line-height:1.25;font-family:sans-serif;fill:#999999;stroke-width:0.264583" + x="23.457415" + y="41.972523" + id="text3750-0"><tspan + sodipodi:role="line" + id="tspan3748-6" + style="fill:#999999;stroke-width:0.264583" + x="23.457415" + y="41.972523">$\not\sqsupseteq \{a\}$</tspan></text> + <text + xml:space="preserve" + style="font-size:8.46667px;line-height:1.25;font-family:sans-serif;fill:#000000;stroke-width:0.264583" + x="14.395845" + y="52.022549" + id="text4280"><tspan + sodipodi:role="line" + id="tspan4278" + style="fill:#000000;stroke-width:0.264583" + x="14.395845" + y="52.022549">return OK</tspan></text> + </g> +</svg> diff --git a/doc/talks/2023-01-18-tocatta/assets/lattice6.svg b/doc/talks/2023-01-18-tocatta/assets/lattice6.svg new file mode 100644 index 00000000..176b1715 --- /dev/null +++ b/doc/talks/2023-01-18-tocatta/assets/lattice6.svg @@ -0,0 +1,553 @@ +<?xml version="1.0" encoding="UTF-8" standalone="no"?> +<!-- Created with Inkscape (http://www.inkscape.org/) --> + +<svg + width="1000" + height="400" + viewBox="0 0 264.58333 105.83333" + version="1.1" + id="svg5" + inkscape:version="1.2.2 (b0a8486541, 2022-12-01)" + sodipodi:docname="lattice6.svg" + 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="namedview7" + pagecolor="#ffffff" + bordercolor="#666666" + borderopacity="1.0" + inkscape:showpageshadow="2" + inkscape:pageopacity="0.0" + inkscape:pagecheckerboard="0" + inkscape:deskcolor="#d1d1d1" + inkscape:document-units="mm" + showgrid="false" + inkscape:zoom="1.0419012" + inkscape:cx="277.85744" + inkscape:cy="254.34273" + inkscape:window-width="1920" + inkscape:window-height="999" + inkscape:window-x="0" + inkscape:window-y="0" + inkscape:window-maximized="1" + inkscape:current-layer="layer2" /> + <defs + id="defs2"> + <marker + style="overflow:visible" + id="Arrow2" + refX="0" + refY="0" + orient="auto-start-reverse" + inkscape:stockid="Arrow2" + markerWidth="7.6999998" + markerHeight="5.5999999" + viewBox="0 0 7.7 5.6" + inkscape:isstock="true" + inkscape:collect="always" + preserveAspectRatio="xMidYMid"> + <path + transform="scale(0.7)" + d="M -2,-4 9,0 -2,4 c 2,-2.33 2,-5.66 0,-8 z" + style="fill:context-stroke;fill-rule:evenodd;stroke:none" + id="arrow2L" /> + </marker> + <marker + style="overflow:visible" + id="Arrow2-9" + refX="0" + refY="0" + orient="auto-start-reverse" + inkscape:stockid="Arrow2" + markerWidth="7.6999998" + markerHeight="5.5999999" + viewBox="0 0 7.7 5.6" + inkscape:isstock="true" + inkscape:collect="always" + preserveAspectRatio="xMidYMid"> + <path + transform="scale(0.7)" + d="M -2,-4 9,0 -2,4 c 2,-2.33 2,-5.66 0,-8 z" + style="fill:context-stroke;fill-rule:evenodd;stroke:none" + id="arrow2L-1" /> + </marker> + <marker + style="overflow:visible" + id="Arrow2-9-7" + refX="0" + refY="0" + orient="auto-start-reverse" + inkscape:stockid="Arrow2" + markerWidth="7.6999998" + markerHeight="5.5999999" + viewBox="0 0 7.7 5.6" + inkscape:isstock="true" + inkscape:collect="always" + preserveAspectRatio="xMidYMid"> + <path + transform="scale(0.7)" + d="M -2,-4 9,0 -2,4 c 2,-2.33 2,-5.66 0,-8 z" + style="fill:context-stroke;fill-rule:evenodd;stroke:none" + id="arrow2L-1-0" /> + </marker> + <marker + style="overflow:visible" + id="Arrow2-93" + refX="0" + refY="0" + orient="auto-start-reverse" + inkscape:stockid="Arrow2" + markerWidth="7.6999998" + markerHeight="5.5999999" + viewBox="0 0 7.7 5.6" + inkscape:isstock="true" + inkscape:collect="always" + preserveAspectRatio="xMidYMid"> + <path + transform="scale(0.7)" + d="M -2,-4 9,0 -2,4 c 2,-2.33 2,-5.66 0,-8 z" + style="fill:context-stroke;fill-rule:evenodd;stroke:none" + id="arrow2L-6" /> + </marker> + <marker + style="overflow:visible" + id="Arrow2-9-7-2" + refX="0" + refY="0" + orient="auto-start-reverse" + inkscape:stockid="Arrow2" + markerWidth="7.6999998" + markerHeight="5.5999999" + viewBox="0 0 7.7 5.6" + inkscape:isstock="true" + inkscape:collect="always" + preserveAspectRatio="xMidYMid"> + <path + transform="scale(0.7)" + d="M -2,-4 9,0 -2,4 c 2,-2.33 2,-5.66 0,-8 z" + style="fill:context-stroke;fill-rule:evenodd;stroke:none" + id="arrow2L-1-0-6" /> + </marker> + <marker + style="overflow:visible" + id="Arrow2-93-1" + refX="0" + refY="0" + orient="auto-start-reverse" + inkscape:stockid="Arrow2" + markerWidth="7.6999998" + markerHeight="5.5999999" + viewBox="0 0 7.7 5.6" + inkscape:isstock="true" + inkscape:collect="always" + preserveAspectRatio="xMidYMid"> + <path + transform="scale(0.7)" + d="M -2,-4 9,0 -2,4 c 2,-2.33 2,-5.66 0,-8 z" + style="fill:context-stroke;fill-rule:evenodd;stroke:none" + id="arrow2L-6-8" /> + </marker> + <marker + style="overflow:visible" + id="Arrow2-9-75" + refX="0" + refY="0" + orient="auto-start-reverse" + inkscape:stockid="Arrow2" + markerWidth="7.6999998" + markerHeight="5.5999999" + viewBox="0 0 7.7 5.6" + inkscape:isstock="true" + inkscape:collect="always" + preserveAspectRatio="xMidYMid"> + <path + transform="scale(0.7)" + d="M -2,-4 9,0 -2,4 c 2,-2.33 2,-5.66 0,-8 z" + style="fill:context-stroke;fill-rule:evenodd;stroke:none" + id="arrow2L-1-9" /> + </marker> + <marker + style="overflow:visible" + id="Arrow2-9-75-2" + refX="0" + refY="0" + orient="auto-start-reverse" + inkscape:stockid="Arrow2" + markerWidth="7.6999998" + markerHeight="5.5999999" + viewBox="0 0 7.7 5.6" + inkscape:isstock="true" + inkscape:collect="always" + preserveAspectRatio="xMidYMid"> + <path + transform="scale(0.7)" + d="M -2,-4 9,0 -2,4 c 2,-2.33 2,-5.66 0,-8 z" + style="fill:context-stroke;fill-rule:evenodd;stroke:none" + id="arrow2L-1-9-8" /> + </marker> + <marker + style="overflow:visible" + id="Arrow2-9-75-7" + refX="0" + refY="0" + orient="auto-start-reverse" + inkscape:stockid="Arrow2" + markerWidth="7.6999998" + markerHeight="5.5999999" + viewBox="0 0 7.7 5.6" + inkscape:isstock="true" + inkscape:collect="always" + preserveAspectRatio="xMidYMid"> + <path + transform="scale(0.7)" + d="M -2,-4 9,0 -2,4 c 2,-2.33 2,-5.66 0,-8 z" + style="fill:context-stroke;fill-rule:evenodd;stroke:none" + id="arrow2L-1-9-3" /> + </marker> + <marker + style="overflow:visible" + id="Arrow2-9-75-7-1" + refX="0" + refY="0" + orient="auto-start-reverse" + inkscape:stockid="Arrow2" + markerWidth="7.6999998" + markerHeight="5.5999999" + viewBox="0 0 7.7 5.6" + inkscape:isstock="true" + inkscape:collect="always" + preserveAspectRatio="xMidYMid"> + <path + transform="scale(0.7)" + d="M -2,-4 9,0 -2,4 c 2,-2.33 2,-5.66 0,-8 z" + style="fill:context-stroke;fill-rule:evenodd;stroke:none" + id="arrow2L-1-9-3-2" /> + </marker> + <marker + style="overflow:visible" + id="Arrow2-93-1-4" + refX="0" + refY="0" + orient="auto-start-reverse" + inkscape:stockid="Arrow2" + markerWidth="7.6999998" + markerHeight="5.5999999" + viewBox="0 0 7.7 5.6" + inkscape:isstock="true" + inkscape:collect="always" + preserveAspectRatio="xMidYMid"> + <path + transform="scale(0.7)" + d="M -2,-4 9,0 -2,4 c 2,-2.33 2,-5.66 0,-8 z" + style="fill:context-stroke;fill-rule:evenodd;stroke:none" + id="arrow2L-6-8-7" /> + </marker> + <marker + style="overflow:visible" + id="Arrow2-9-7-2-8" + refX="0" + refY="0" + orient="auto-start-reverse" + inkscape:stockid="Arrow2" + markerWidth="7.6999998" + markerHeight="5.5999999" + viewBox="0 0 7.7 5.6" + inkscape:isstock="true" + inkscape:collect="always" + preserveAspectRatio="xMidYMid"> + <path + transform="scale(0.7)" + d="M -2,-4 9,0 -2,4 c 2,-2.33 2,-5.66 0,-8 z" + style="fill:context-stroke;fill-rule:evenodd;stroke:none" + id="arrow2L-1-0-6-4" /> + </marker> + </defs> + <g + inkscape:label="Layer 1" + inkscape:groupmode="layer" + id="layer1" + sodipodi:insensitive="true"> + <rect + style="fill:#ffffff;stroke:none;stroke-width:1;stop-color:#000000" + id="rect288" + width="209.84705" + height="104.42732" + x="0.77790999" + y="0.93738818" /> + </g> + <g + inkscape:groupmode="layer" + id="layer2" + inkscape:label="Layer 2"> + <text + xml:space="preserve" + style="font-size:8.46667px;line-height:1.25;font-family:sans-serif;text-align:center;text-anchor:middle;stroke-width:0.264583;fill:#000000" + x="164.56372" + y="99.307442" + id="text951"><tspan + sodipodi:role="line" + id="tspan949" + style="stroke-width:0.264583;fill:#000000" + x="164.56372" + y="99.307442">$\{\}$</tspan></text> + <text + xml:space="preserve" + style="font-size:8.46667px;line-height:1.25;font-family:sans-serif;text-align:center;text-anchor:middle;stroke-width:0.264583;fill:#000000" + x="164.56372" + y="13.151893" + id="text1005"><tspan + sodipodi:role="line" + id="tspan1003" + style="stroke-width:0.264583;fill:#000000" + x="164.56372" + y="13.151893">$\{a,b,c\}$</tspan></text> + <g + id="g1175" + transform="translate(51.996784,3.5774043)"> + <text + xml:space="preserve" + style="font-size:8.46667px;line-height:1.25;font-family:sans-serif;text-align:center;text-anchor:middle;stroke-width:0.264583;fill:#000000" + x="49.27084" + y="67.008698" + id="text1009"><tspan + sodipodi:role="line" + id="tspan1007" + style="stroke-width:0.264583;fill:#000000" + x="49.27084" + y="67.008698">$\{a\}$</tspan></text> + <text + xml:space="preserve" + style="font-size:8.46667px;line-height:1.25;font-family:sans-serif;text-align:center;text-anchor:middle;stroke-width:0.264583;fill:#000000" + x="112.90984" + y="67.017166" + id="text1009-3"><tspan + sodipodi:role="line" + id="tspan1007-6" + style="stroke-width:0.264583;fill:#000000" + x="112.90984" + y="67.017166">$\{b\}$</tspan></text> + <text + xml:space="preserve" + style="font-size:8.46667px;line-height:1.25;font-family:sans-serif;text-align:center;text-anchor:middle;stroke-width:0.264583;fill:#000000" + x="176.20593" + y="67.008698" + id="text1009-7"><tspan + sodipodi:role="line" + id="tspan1007-5" + style="stroke-width:0.264583;fill:#000000" + x="176.20593" + y="67.008698">$\{c\}$</tspan></text> + </g> + <g + id="g1183" + transform="translate(51.996784,1.0317046)" + style="fill:#000000"> + <text + xml:space="preserve" + style="font-size:8.46667px;line-height:1.25;font-family:sans-serif;text-align:center;text-anchor:middle;stroke-width:0.264583;fill:#000000" + x="112.90984" + y="40.841526" + id="text1117"><tspan + sodipodi:role="line" + id="tspan1115" + style="stroke-width:0.264583;fill:#000000" + x="112.90984" + y="40.841526">$\{a,c\}$</tspan></text> + <text + xml:space="preserve" + style="font-size:8.46667px;line-height:1.25;font-family:sans-serif;text-align:center;text-anchor:middle;stroke-width:0.264583;fill:#000000" + x="49.27084" + y="40.841526" + id="text1117-3"><tspan + sodipodi:role="line" + id="tspan1115-5" + style="stroke-width:0.264583;fill:#000000" + x="49.27084" + y="40.841526">$\{a,b\}$</tspan></text> + <text + xml:space="preserve" + style="font-size:8.46667px;line-height:1.25;font-family:sans-serif;text-align:center;text-anchor:middle;stroke-width:0.264583;fill:#000000" + x="176.20593" + y="40.841526" + id="text1117-6"><tspan + sodipodi:role="line" + id="tspan1115-2" + style="stroke-width:0.264583;fill:#000000" + x="176.20593" + y="40.841526">$\{b,c\}$</tspan></text> + </g> + <path + style="fill:none;stroke:#000000;stroke-width:0.5;stroke-linecap:butt;stroke-linejoin:miter;stroke-dasharray:none;stroke-opacity:1;marker-end:url(#Arrow2)" + d="M 153.33622,90.367682 118.34198,73.428915" + id="path1300" /> + <path + style="fill:none;stroke:#000000;stroke-width:0.5;stroke-linecap:butt;stroke-linejoin:miter;stroke-dasharray:none;stroke-opacity:1;marker-end:url(#Arrow2-9)" + d="M 177.46016,90.367682 212.4544,73.428915" + id="path1300-2" /> + <path + style="fill:none;stroke:#000000;stroke-width:0.5;stroke-linecap:butt;stroke-linejoin:miter;stroke-dasharray:none;stroke-opacity:1;marker-end:url(#Arrow2-93)" + d="M 153.33622,61.655656 118.34198,44.716889" + id="path1300-0" /> + <path + style="fill:none;stroke:#000000;stroke-width:0.5;stroke-linecap:butt;stroke-linejoin:miter;stroke-dasharray:none;stroke-opacity:1;marker-end:url(#Arrow2-9-7)" + d="M 177.46016,61.655656 212.4544,44.716889" + id="path1300-2-6" /> + <path + style="fill:none;stroke:#000000;stroke-width:0.5;stroke-linecap:butt;stroke-linejoin:miter;stroke-dasharray:none;stroke-opacity:1;marker-end:url(#Arrow2-93-1)" + d="M 118.34198,61.655656 153.33622,44.716889" + id="path1300-0-7" /> + <path + style="fill:none;stroke:#000000;stroke-width:0.5;stroke-linecap:butt;stroke-linejoin:miter;stroke-dasharray:none;stroke-opacity:1;marker-end:url(#Arrow2-9-7-2)" + d="M 212.4544,61.655656 177.46016,44.716889" + id="path1300-2-6-9" /> + <path + style="fill:none;stroke:#000000;stroke-width:0.5;stroke-linecap:butt;stroke-linejoin:miter;stroke-dasharray:none;stroke-opacity:1;marker-end:url(#Arrow2-93-1-4)" + d="M 118.34198,34.227412 153.33622,17.288645" + id="path1300-0-7-5" /> + <path + style="fill:none;stroke:#000000;stroke-width:0.5;stroke-linecap:butt;stroke-linejoin:miter;stroke-dasharray:none;stroke-opacity:1;marker-end:url(#Arrow2-9-7-2-8)" + d="M 212.4544,34.227412 177.46016,17.288645" + id="path1300-2-6-9-0" /> + <path + style="fill:none;stroke:#000000;stroke-width:0.5;stroke-linecap:butt;stroke-linejoin:miter;stroke-dasharray:none;stroke-opacity:1;marker-end:url(#Arrow2-9-75)" + d="m 228.52843,61.091809 0.33313,-12.554874 m -0.33313,12.554874 0.33313,-12.554874" + id="path1300-2-2" + sodipodi:nodetypes="cc" /> + <path + style="fill:none;stroke:#000000;stroke-width:0.5;stroke-linecap:butt;stroke-linejoin:miter;stroke-dasharray:none;stroke-opacity:1;marker-end:url(#Arrow2-9-75-2)" + d="m 101.90418,61.091809 0.33313,-12.554874 m -0.33313,12.554874 0.33313,-12.554874" + id="path1300-2-2-9" + sodipodi:nodetypes="cc" /> + <path + style="fill:none;stroke:#000000;stroke-width:0.5;stroke-linecap:butt;stroke-linejoin:miter;stroke-dasharray:none;stroke-opacity:1;marker-end:url(#Arrow2-9-75-7)" + d="m 165.29305,89.571762 0.33313,-12.554874 m -0.33313,12.554874 0.33313,-12.554874" + id="path1300-2-2-6" + sodipodi:nodetypes="cc" /> + <path + style="fill:none;stroke:#000000;stroke-width:0.5;stroke-linecap:butt;stroke-linejoin:miter;stroke-dasharray:none;stroke-opacity:1;marker-end:url(#Arrow2-9-75-7-1)" + d="m 165.29305,32.445235 0.33313,-12.554874 m -0.33313,12.554874 0.33313,-12.554874" + id="path1300-2-2-6-9" + sodipodi:nodetypes="cc" /> + <circle + style="fill:#ff0000;stroke:none;stroke-width:0.499999;stroke-dasharray:none;stop-color:#000000" + id="path3663" + cx="147.35568" + cy="95.24971" + r="2.7302806" /> + <circle + style="fill:#008000;stroke:none;stroke-width:0.499999;stroke-dasharray:none;stop-color:#000000" + id="path3663-3" + cx="126.08154" + cy="67.968384" + r="2.7302806" /> + <circle + style="fill:#800080;stroke:none;stroke-width:0.499999;stroke-dasharray:none;stop-color:#000000" + id="path3663-6" + cx="119.58919" + cy="67.645035" + r="2.7302806" /> + <circle + style="fill:#ff0000;stroke:none;stroke-width:0.499999;stroke-dasharray:none;stop-color:#000000" + id="path3663-1" + cx="18.004833" + cy="39.402473" + r="2.7302806" /> + <circle + style="fill:#008000;stroke:none;stroke-width:0.499999;stroke-dasharray:none;stop-color:#000000" + id="path3663-3-0" + cx="18.004833" + cy="30.371933" + r="2.7302806" /> + <circle + style="fill:#800080;stroke:none;stroke-width:0.499999;stroke-dasharray:none;stop-color:#000000" + id="path3663-6-6" + cx="18.004833" + cy="21.341394" + r="2.7302806" /> + <text + xml:space="preserve" + style="font-size:8.46667px;line-height:1.25;font-family:sans-serif;stroke-width:0.264583;fill:#000000" + x="6.9525447" + y="13.702217" + id="text3707"><tspan + sodipodi:role="line" + id="tspan3705" + style="stroke-width:0.264583;fill:#000000" + x="6.9525447" + y="13.702217">$write(\{a\})$:</tspan></text> + <text + xml:space="preserve" + style="font-size:8.46667px;line-height:1.25;font-family:sans-serif;fill:#000000;stroke-width:0.264583" + x="6.9525447" + y="65.261436" + id="text3707-1"><tspan + sodipodi:role="line" + id="tspan3705-5" + style="fill:#000000;stroke-width:0.264583" + x="6.9525447" + y="65.261436">$read()$:</tspan></text> + <text + xml:space="preserve" + style="font-size:8.46667px;line-height:1.25;font-family:sans-serif;fill:#000000;stroke-width:0.264583" + x="23.457415" + y="24.042637" + id="text3750"><tspan + sodipodi:role="line" + id="tspan3748" + style="fill:#000000;stroke-width:0.264583" + x="23.457415" + y="24.042637">$\sqsupseteq \{a\} \to$ OK</tspan></text> + <text + xml:space="preserve" + style="font-size:8.46667px;line-height:1.25;font-family:sans-serif;fill:#000000;stroke-width:0.264583" + x="23.457415" + y="33.02087" + id="text3750-3"><tspan + sodipodi:role="line" + id="tspan3748-2" + style="fill:#000000;stroke-width:0.264583" + x="23.457415" + y="33.02087">$\sqsupseteq \{a\} \to$ OK</tspan></text> + <text + xml:space="preserve" + style="font-size:8.46667px;line-height:1.25;font-family:sans-serif;fill:#999999;stroke-width:0.264583" + x="23.457415" + y="41.972523" + id="text3750-0"><tspan + sodipodi:role="line" + id="tspan3748-6" + style="fill:#999999;stroke-width:0.264583" + x="23.457415" + y="41.972523">$\not\sqsupseteq \{a\}$</tspan></text> + <circle + style="fill:#ff0000;stroke:none;stroke-width:0.499999;stroke-dasharray:none;stop-color:#000000" + id="path3663-6-6-4" + cx="18.004833" + cy="70.942116" + r="2.7302806" /> + <text + xml:space="preserve" + style="font-size:8.46667px;line-height:1.25;font-family:sans-serif;fill:#000000;stroke-width:0.264583" + x="23.457415" + y="73.643356" + id="text3750-7"><tspan + sodipodi:role="line" + id="tspan3748-65" + style="fill:#000000;stroke-width:0.264583" + x="23.457415" + y="73.643356">$\to \{\}$</tspan></text> + <text + xml:space="preserve" + style="font-size:8.46667px;line-height:1.25;font-family:sans-serif;fill:#000000;stroke-width:0.264583" + x="14.395845" + y="52.022549" + id="text4280"><tspan + sodipodi:role="line" + id="tspan4278" + style="fill:#000000;stroke-width:0.264583" + x="14.395845" + y="52.022549">return OK</tspan></text> + </g> +</svg> diff --git a/doc/talks/2023-01-18-tocatta/assets/lattice7.svg b/doc/talks/2023-01-18-tocatta/assets/lattice7.svg new file mode 100644 index 00000000..7ce8bda8 --- /dev/null +++ b/doc/talks/2023-01-18-tocatta/assets/lattice7.svg @@ -0,0 +1,581 @@ +<?xml version="1.0" encoding="UTF-8" standalone="no"?> +<!-- Created with Inkscape (http://www.inkscape.org/) --> + +<svg + width="1000" + height="400" + viewBox="0 0 264.58333 105.83333" + version="1.1" + id="svg5" + inkscape:version="1.2.2 (b0a8486541, 2022-12-01)" + sodipodi:docname="lattice7.svg" + 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="namedview7" + pagecolor="#ffffff" + bordercolor="#666666" + borderopacity="1.0" + inkscape:showpageshadow="2" + inkscape:pageopacity="0.0" + inkscape:pagecheckerboard="0" + inkscape:deskcolor="#d1d1d1" + inkscape:document-units="mm" + showgrid="false" + inkscape:zoom="1.0419012" + inkscape:cx="276.89766" + inkscape:cy="254.34273" + inkscape:window-width="1920" + inkscape:window-height="999" + inkscape:window-x="0" + inkscape:window-y="0" + inkscape:window-maximized="1" + inkscape:current-layer="layer2" /> + <defs + id="defs2"> + <marker + style="overflow:visible" + id="Arrow2" + refX="0" + refY="0" + orient="auto-start-reverse" + inkscape:stockid="Arrow2" + markerWidth="7.6999998" + markerHeight="5.5999999" + viewBox="0 0 7.7 5.6" + inkscape:isstock="true" + inkscape:collect="always" + preserveAspectRatio="xMidYMid"> + <path + transform="scale(0.7)" + d="M -2,-4 9,0 -2,4 c 2,-2.33 2,-5.66 0,-8 z" + style="fill:context-stroke;fill-rule:evenodd;stroke:none" + id="arrow2L" /> + </marker> + <marker + style="overflow:visible" + id="Arrow2-9" + refX="0" + refY="0" + orient="auto-start-reverse" + inkscape:stockid="Arrow2" + markerWidth="7.6999998" + markerHeight="5.5999999" + viewBox="0 0 7.7 5.6" + inkscape:isstock="true" + inkscape:collect="always" + preserveAspectRatio="xMidYMid"> + <path + transform="scale(0.7)" + d="M -2,-4 9,0 -2,4 c 2,-2.33 2,-5.66 0,-8 z" + style="fill:context-stroke;fill-rule:evenodd;stroke:none" + id="arrow2L-1" /> + </marker> + <marker + style="overflow:visible" + id="Arrow2-9-7" + refX="0" + refY="0" + orient="auto-start-reverse" + inkscape:stockid="Arrow2" + markerWidth="7.6999998" + markerHeight="5.5999999" + viewBox="0 0 7.7 5.6" + inkscape:isstock="true" + inkscape:collect="always" + preserveAspectRatio="xMidYMid"> + <path + transform="scale(0.7)" + d="M -2,-4 9,0 -2,4 c 2,-2.33 2,-5.66 0,-8 z" + style="fill:context-stroke;fill-rule:evenodd;stroke:none" + id="arrow2L-1-0" /> + </marker> + <marker + style="overflow:visible" + id="Arrow2-93" + refX="0" + refY="0" + orient="auto-start-reverse" + inkscape:stockid="Arrow2" + markerWidth="7.6999998" + markerHeight="5.5999999" + viewBox="0 0 7.7 5.6" + inkscape:isstock="true" + inkscape:collect="always" + preserveAspectRatio="xMidYMid"> + <path + transform="scale(0.7)" + d="M -2,-4 9,0 -2,4 c 2,-2.33 2,-5.66 0,-8 z" + style="fill:context-stroke;fill-rule:evenodd;stroke:none" + id="arrow2L-6" /> + </marker> + <marker + style="overflow:visible" + id="Arrow2-9-7-2" + refX="0" + refY="0" + orient="auto-start-reverse" + inkscape:stockid="Arrow2" + markerWidth="7.6999998" + markerHeight="5.5999999" + viewBox="0 0 7.7 5.6" + inkscape:isstock="true" + inkscape:collect="always" + preserveAspectRatio="xMidYMid"> + <path + transform="scale(0.7)" + d="M -2,-4 9,0 -2,4 c 2,-2.33 2,-5.66 0,-8 z" + style="fill:context-stroke;fill-rule:evenodd;stroke:none" + id="arrow2L-1-0-6" /> + </marker> + <marker + style="overflow:visible" + id="Arrow2-93-1" + refX="0" + refY="0" + orient="auto-start-reverse" + inkscape:stockid="Arrow2" + markerWidth="7.6999998" + markerHeight="5.5999999" + viewBox="0 0 7.7 5.6" + inkscape:isstock="true" + inkscape:collect="always" + preserveAspectRatio="xMidYMid"> + <path + transform="scale(0.7)" + d="M -2,-4 9,0 -2,4 c 2,-2.33 2,-5.66 0,-8 z" + style="fill:context-stroke;fill-rule:evenodd;stroke:none" + id="arrow2L-6-8" /> + </marker> + <marker + style="overflow:visible" + id="Arrow2-9-75" + refX="0" + refY="0" + orient="auto-start-reverse" + inkscape:stockid="Arrow2" + markerWidth="7.6999998" + markerHeight="5.5999999" + viewBox="0 0 7.7 5.6" + inkscape:isstock="true" + inkscape:collect="always" + preserveAspectRatio="xMidYMid"> + <path + transform="scale(0.7)" + d="M -2,-4 9,0 -2,4 c 2,-2.33 2,-5.66 0,-8 z" + style="fill:context-stroke;fill-rule:evenodd;stroke:none" + id="arrow2L-1-9" /> + </marker> + <marker + style="overflow:visible" + id="Arrow2-9-75-2" + refX="0" + refY="0" + orient="auto-start-reverse" + inkscape:stockid="Arrow2" + markerWidth="7.6999998" + markerHeight="5.5999999" + viewBox="0 0 7.7 5.6" + inkscape:isstock="true" + inkscape:collect="always" + preserveAspectRatio="xMidYMid"> + <path + transform="scale(0.7)" + d="M -2,-4 9,0 -2,4 c 2,-2.33 2,-5.66 0,-8 z" + style="fill:context-stroke;fill-rule:evenodd;stroke:none" + id="arrow2L-1-9-8" /> + </marker> + <marker + style="overflow:visible" + id="Arrow2-9-75-7" + refX="0" + refY="0" + orient="auto-start-reverse" + inkscape:stockid="Arrow2" + markerWidth="7.6999998" + markerHeight="5.5999999" + viewBox="0 0 7.7 5.6" + inkscape:isstock="true" + inkscape:collect="always" + preserveAspectRatio="xMidYMid"> + <path + transform="scale(0.7)" + d="M -2,-4 9,0 -2,4 c 2,-2.33 2,-5.66 0,-8 z" + style="fill:context-stroke;fill-rule:evenodd;stroke:none" + id="arrow2L-1-9-3" /> + </marker> + <marker + style="overflow:visible" + id="Arrow2-9-75-7-1" + refX="0" + refY="0" + orient="auto-start-reverse" + inkscape:stockid="Arrow2" + markerWidth="7.6999998" + markerHeight="5.5999999" + viewBox="0 0 7.7 5.6" + inkscape:isstock="true" + inkscape:collect="always" + preserveAspectRatio="xMidYMid"> + <path + transform="scale(0.7)" + d="M -2,-4 9,0 -2,4 c 2,-2.33 2,-5.66 0,-8 z" + style="fill:context-stroke;fill-rule:evenodd;stroke:none" + id="arrow2L-1-9-3-2" /> + </marker> + <marker + style="overflow:visible" + id="Arrow2-93-1-4" + refX="0" + refY="0" + orient="auto-start-reverse" + inkscape:stockid="Arrow2" + markerWidth="7.6999998" + markerHeight="5.5999999" + viewBox="0 0 7.7 5.6" + inkscape:isstock="true" + inkscape:collect="always" + preserveAspectRatio="xMidYMid"> + <path + transform="scale(0.7)" + d="M -2,-4 9,0 -2,4 c 2,-2.33 2,-5.66 0,-8 z" + style="fill:context-stroke;fill-rule:evenodd;stroke:none" + id="arrow2L-6-8-7" /> + </marker> + <marker + style="overflow:visible" + id="Arrow2-9-7-2-8" + refX="0" + refY="0" + orient="auto-start-reverse" + inkscape:stockid="Arrow2" + markerWidth="7.6999998" + markerHeight="5.5999999" + viewBox="0 0 7.7 5.6" + inkscape:isstock="true" + inkscape:collect="always" + preserveAspectRatio="xMidYMid"> + <path + transform="scale(0.7)" + d="M -2,-4 9,0 -2,4 c 2,-2.33 2,-5.66 0,-8 z" + style="fill:context-stroke;fill-rule:evenodd;stroke:none" + id="arrow2L-1-0-6-4" /> + </marker> + </defs> + <g + inkscape:label="Layer 1" + inkscape:groupmode="layer" + id="layer1" + sodipodi:insensitive="true"> + <rect + style="fill:#ffffff;stroke:none;stroke-width:1;stop-color:#000000" + id="rect288" + width="209.84705" + height="104.42732" + x="0.77790999" + y="0.93738818" /> + </g> + <g + inkscape:groupmode="layer" + id="layer2" + inkscape:label="Layer 2"> + <text + xml:space="preserve" + style="font-size:8.46667px;line-height:1.25;font-family:sans-serif;text-align:center;text-anchor:middle;stroke-width:0.264583;fill:#000000" + x="164.56372" + y="99.307442" + id="text951"><tspan + sodipodi:role="line" + id="tspan949" + style="stroke-width:0.264583;fill:#000000" + x="164.56372" + y="99.307442">$\{\}$</tspan></text> + <text + xml:space="preserve" + style="font-size:8.46667px;line-height:1.25;font-family:sans-serif;text-align:center;text-anchor:middle;stroke-width:0.264583;fill:#000000" + x="164.56372" + y="13.151893" + id="text1005"><tspan + sodipodi:role="line" + id="tspan1003" + style="stroke-width:0.264583;fill:#000000" + x="164.56372" + y="13.151893">$\{a,b,c\}$</tspan></text> + <g + id="g1175" + transform="translate(51.996784,3.5774043)"> + <text + xml:space="preserve" + style="font-size:8.46667px;line-height:1.25;font-family:sans-serif;text-align:center;text-anchor:middle;stroke-width:0.264583;fill:#000000" + x="49.27084" + y="67.008698" + id="text1009"><tspan + sodipodi:role="line" + id="tspan1007" + style="stroke-width:0.264583;fill:#000000" + x="49.27084" + y="67.008698">$\{a\}$</tspan></text> + <text + xml:space="preserve" + style="font-size:8.46667px;line-height:1.25;font-family:sans-serif;text-align:center;text-anchor:middle;stroke-width:0.264583;fill:#000000" + x="112.90984" + y="67.017166" + id="text1009-3"><tspan + sodipodi:role="line" + id="tspan1007-6" + style="stroke-width:0.264583;fill:#000000" + x="112.90984" + y="67.017166">$\{b\}$</tspan></text> + <text + xml:space="preserve" + style="font-size:8.46667px;line-height:1.25;font-family:sans-serif;text-align:center;text-anchor:middle;stroke-width:0.264583;fill:#000000" + x="176.20593" + y="67.008698" + id="text1009-7"><tspan + sodipodi:role="line" + id="tspan1007-5" + style="stroke-width:0.264583;fill:#000000" + x="176.20593" + y="67.008698">$\{c\}$</tspan></text> + </g> + <g + id="g1183" + transform="translate(51.996784,1.0317046)" + style="fill:#000000"> + <text + xml:space="preserve" + style="font-size:8.46667px;line-height:1.25;font-family:sans-serif;text-align:center;text-anchor:middle;stroke-width:0.264583;fill:#000000" + x="112.90984" + y="40.841526" + id="text1117"><tspan + sodipodi:role="line" + id="tspan1115" + style="stroke-width:0.264583;fill:#000000" + x="112.90984" + y="40.841526">$\{a,c\}$</tspan></text> + <text + xml:space="preserve" + style="font-size:8.46667px;line-height:1.25;font-family:sans-serif;text-align:center;text-anchor:middle;stroke-width:0.264583;fill:#000000" + x="49.27084" + y="40.841526" + id="text1117-3"><tspan + sodipodi:role="line" + id="tspan1115-5" + style="stroke-width:0.264583;fill:#000000" + x="49.27084" + y="40.841526">$\{a,b\}$</tspan></text> + <text + xml:space="preserve" + style="font-size:8.46667px;line-height:1.25;font-family:sans-serif;text-align:center;text-anchor:middle;stroke-width:0.264583;fill:#000000" + x="176.20593" + y="40.841526" + id="text1117-6"><tspan + sodipodi:role="line" + id="tspan1115-2" + style="stroke-width:0.264583;fill:#000000" + x="176.20593" + y="40.841526">$\{b,c\}$</tspan></text> + </g> + <path + style="fill:none;stroke:#000000;stroke-width:0.5;stroke-linecap:butt;stroke-linejoin:miter;stroke-dasharray:none;stroke-opacity:1;marker-end:url(#Arrow2)" + d="M 153.33622,90.367682 118.34198,73.428915" + id="path1300" /> + <path + style="fill:none;stroke:#000000;stroke-width:0.5;stroke-linecap:butt;stroke-linejoin:miter;stroke-dasharray:none;stroke-opacity:1;marker-end:url(#Arrow2-9)" + d="M 177.46016,90.367682 212.4544,73.428915" + id="path1300-2" /> + <path + style="fill:none;stroke:#000000;stroke-width:0.5;stroke-linecap:butt;stroke-linejoin:miter;stroke-dasharray:none;stroke-opacity:1;marker-end:url(#Arrow2-93)" + d="M 153.33622,61.655656 118.34198,44.716889" + id="path1300-0" /> + <path + style="fill:none;stroke:#000000;stroke-width:0.5;stroke-linecap:butt;stroke-linejoin:miter;stroke-dasharray:none;stroke-opacity:1;marker-end:url(#Arrow2-9-7)" + d="M 177.46016,61.655656 212.4544,44.716889" + id="path1300-2-6" /> + <path + style="fill:none;stroke:#000000;stroke-width:0.5;stroke-linecap:butt;stroke-linejoin:miter;stroke-dasharray:none;stroke-opacity:1;marker-end:url(#Arrow2-93-1)" + d="M 118.34198,61.655656 153.33622,44.716889" + id="path1300-0-7" /> + <path + style="fill:none;stroke:#000000;stroke-width:0.5;stroke-linecap:butt;stroke-linejoin:miter;stroke-dasharray:none;stroke-opacity:1;marker-end:url(#Arrow2-9-7-2)" + d="M 212.4544,61.655656 177.46016,44.716889" + id="path1300-2-6-9" /> + <path + style="fill:none;stroke:#000000;stroke-width:0.5;stroke-linecap:butt;stroke-linejoin:miter;stroke-dasharray:none;stroke-opacity:1;marker-end:url(#Arrow2-93-1-4)" + d="M 118.34198,34.227412 153.33622,17.288645" + id="path1300-0-7-5" /> + <path + style="fill:none;stroke:#000000;stroke-width:0.5;stroke-linecap:butt;stroke-linejoin:miter;stroke-dasharray:none;stroke-opacity:1;marker-end:url(#Arrow2-9-7-2-8)" + d="M 212.4544,34.227412 177.46016,17.288645" + id="path1300-2-6-9-0" /> + <path + style="fill:none;stroke:#000000;stroke-width:0.5;stroke-linecap:butt;stroke-linejoin:miter;stroke-dasharray:none;stroke-opacity:1;marker-end:url(#Arrow2-9-75)" + d="m 228.52843,61.091809 0.33313,-12.554874 m -0.33313,12.554874 0.33313,-12.554874" + id="path1300-2-2" + sodipodi:nodetypes="cc" /> + <path + style="fill:none;stroke:#000000;stroke-width:0.5;stroke-linecap:butt;stroke-linejoin:miter;stroke-dasharray:none;stroke-opacity:1;marker-end:url(#Arrow2-9-75-2)" + d="m 101.90418,61.091809 0.33313,-12.554874 m -0.33313,12.554874 0.33313,-12.554874" + id="path1300-2-2-9" + sodipodi:nodetypes="cc" /> + <path + style="fill:none;stroke:#000000;stroke-width:0.5;stroke-linecap:butt;stroke-linejoin:miter;stroke-dasharray:none;stroke-opacity:1;marker-end:url(#Arrow2-9-75-7)" + d="m 165.29305,89.571762 0.33313,-12.554874 m -0.33313,12.554874 0.33313,-12.554874" + id="path1300-2-2-6" + sodipodi:nodetypes="cc" /> + <path + style="fill:none;stroke:#000000;stroke-width:0.5;stroke-linecap:butt;stroke-linejoin:miter;stroke-dasharray:none;stroke-opacity:1;marker-end:url(#Arrow2-9-75-7-1)" + d="m 165.29305,32.445235 0.33313,-12.554874 m -0.33313,12.554874 0.33313,-12.554874" + id="path1300-2-2-6-9" + sodipodi:nodetypes="cc" /> + <circle + style="fill:#ff0000;stroke:none;stroke-width:0.499999;stroke-dasharray:none;stop-color:#000000" + id="path3663" + cx="147.35568" + cy="95.24971" + r="2.7302806" /> + <circle + style="fill:#008000;stroke:none;stroke-width:0.499999;stroke-dasharray:none;stop-color:#000000" + id="path3663-3" + cx="126.08154" + cy="67.968384" + r="2.7302806" /> + <circle + style="fill:#800080;stroke:none;stroke-width:0.499999;stroke-dasharray:none;stop-color:#000000" + id="path3663-6" + cx="119.58919" + cy="67.645035" + r="2.7302806" /> + <circle + style="fill:#ff0000;stroke:none;stroke-width:0.499999;stroke-dasharray:none;stop-color:#000000" + id="path3663-1" + cx="18.004833" + cy="39.402473" + r="2.7302806" /> + <circle + style="fill:#008000;stroke:none;stroke-width:0.499999;stroke-dasharray:none;stop-color:#000000" + id="path3663-3-0" + cx="18.004833" + cy="30.371933" + r="2.7302806" /> + <circle + style="fill:#800080;stroke:none;stroke-width:0.499999;stroke-dasharray:none;stop-color:#000000" + id="path3663-6-6" + cx="18.004833" + cy="21.341394" + r="2.7302806" /> + <text + xml:space="preserve" + style="font-size:8.46667px;line-height:1.25;font-family:sans-serif;stroke-width:0.264583;fill:#000000" + x="6.9525447" + y="13.702217" + id="text3707"><tspan + sodipodi:role="line" + id="tspan3705" + style="stroke-width:0.264583;fill:#000000" + x="6.9525447" + y="13.702217">$write(\{a\})$:</tspan></text> + <text + xml:space="preserve" + style="font-size:8.46667px;line-height:1.25;font-family:sans-serif;fill:#000000;stroke-width:0.264583" + x="6.9525447" + y="65.261436" + id="text3707-1"><tspan + sodipodi:role="line" + id="tspan3705-5" + style="fill:#000000;stroke-width:0.264583" + x="6.9525447" + y="65.261436">$read()$:</tspan></text> + <text + xml:space="preserve" + style="font-size:8.46667px;line-height:1.25;font-family:sans-serif;fill:#000000;stroke-width:0.264583" + x="23.457415" + y="24.042637" + id="text3750"><tspan + sodipodi:role="line" + id="tspan3748" + style="fill:#000000;stroke-width:0.264583" + x="23.457415" + y="24.042637">$\sqsupseteq \{a\} \to$ OK</tspan></text> + <text + xml:space="preserve" + style="font-size:8.46667px;line-height:1.25;font-family:sans-serif;fill:#000000;stroke-width:0.264583" + x="23.457415" + y="33.02087" + id="text3750-3"><tspan + sodipodi:role="line" + id="tspan3748-2" + style="fill:#000000;stroke-width:0.264583" + x="23.457415" + y="33.02087">$\sqsupseteq \{a\} \to$ OK</tspan></text> + <text + xml:space="preserve" + style="font-size:8.46667px;line-height:1.25;font-family:sans-serif;fill:#999999;stroke-width:0.264583" + x="23.457415" + y="41.972523" + id="text3750-0"><tspan + sodipodi:role="line" + id="tspan3748-6" + style="fill:#999999;stroke-width:0.264583" + x="23.457415" + y="41.972523">$\not\sqsupseteq \{a\}$</tspan></text> + <circle + style="fill:#ff0000;stroke:none;stroke-width:0.499999;stroke-dasharray:none;stop-color:#000000" + id="path3663-6-6-4" + cx="18.004833" + cy="70.942116" + r="2.7302806" /> + <text + xml:space="preserve" + style="font-size:8.46667px;line-height:1.25;font-family:sans-serif;fill:#000000;stroke-width:0.264583" + x="23.457415" + y="73.643356" + id="text3750-7"><tspan + sodipodi:role="line" + id="tspan3748-65" + style="fill:#000000;stroke-width:0.264583" + x="23.457415" + y="73.643356">$\to \{\}$</tspan></text> + <text + xml:space="preserve" + style="font-size:8.46667px;line-height:1.25;font-family:sans-serif;fill:#000000;stroke-width:0.264583" + x="14.395845" + y="52.022549" + id="text4280"><tspan + sodipodi:role="line" + id="tspan4278" + style="fill:#000000;stroke-width:0.264583" + x="14.395845" + y="52.022549">return OK</tspan></text> + <text + xml:space="preserve" + style="font-size:8.46667px;line-height:1.25;font-family:sans-serif;fill:#000000;stroke-width:0.264583" + x="14.395845" + y="92.005798" + id="text4280-3"><tspan + sodipodi:role="line" + id="tspan4278-7" + style="fill:#000000;stroke-width:0.264583" + x="14.395845" + y="92.005798">return $\{\}\sqcup\{a\}=\{a\}$</tspan></text> + <circle + style="fill:#800080;stroke:none;stroke-width:0.499999;stroke-dasharray:none;stop-color:#000000" + id="path3663-1-5" + cx="18.004833" + cy="81.007744" + r="2.7302806" /> + <text + xml:space="preserve" + style="font-size:8.46667px;line-height:1.25;font-family:sans-serif;fill:#000000;stroke-width:0.264583" + x="23.457415" + y="83.577797" + id="text3750-0-6"><tspan + sodipodi:role="line" + id="tspan3748-6-9" + style="fill:#000000;stroke-width:0.264583" + x="23.457415" + y="83.577797">$\to \{a\}$</tspan></text> + </g> +</svg> diff --git a/doc/talks/2023-01-18-tocatta/assets/lattice8.svg b/doc/talks/2023-01-18-tocatta/assets/lattice8.svg new file mode 100644 index 00000000..3bada791 --- /dev/null +++ b/doc/talks/2023-01-18-tocatta/assets/lattice8.svg @@ -0,0 +1,587 @@ +<?xml version="1.0" encoding="UTF-8" standalone="no"?> +<!-- Created with Inkscape (http://www.inkscape.org/) --> + +<svg + width="1000" + height="400" + viewBox="0 0 264.58333 105.83333" + version="1.1" + id="svg5" + inkscape:version="1.2.2 (b0a8486541, 2022-12-01)" + sodipodi:docname="lattice8.svg" + 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="namedview7" + pagecolor="#ffffff" + bordercolor="#666666" + borderopacity="1.0" + inkscape:showpageshadow="2" + inkscape:pageopacity="0.0" + inkscape:pagecheckerboard="0" + inkscape:deskcolor="#d1d1d1" + inkscape:document-units="mm" + showgrid="false" + inkscape:zoom="1.4734708" + inkscape:cx="451.65469" + inkscape:cy="272.14655" + inkscape:window-width="1920" + inkscape:window-height="999" + inkscape:window-x="0" + inkscape:window-y="0" + inkscape:window-maximized="1" + inkscape:current-layer="layer2" /> + <defs + id="defs2"> + <marker + style="overflow:visible" + id="Arrow2" + refX="0" + refY="0" + orient="auto-start-reverse" + inkscape:stockid="Arrow2" + markerWidth="7.6999998" + markerHeight="5.5999999" + viewBox="0 0 7.7 5.6" + inkscape:isstock="true" + inkscape:collect="always" + preserveAspectRatio="xMidYMid"> + <path + transform="scale(0.7)" + d="M -2,-4 9,0 -2,4 c 2,-2.33 2,-5.66 0,-8 z" + style="fill:context-stroke;fill-rule:evenodd;stroke:none" + id="arrow2L" /> + </marker> + <marker + style="overflow:visible" + id="Arrow2-9" + refX="0" + refY="0" + orient="auto-start-reverse" + inkscape:stockid="Arrow2" + markerWidth="7.6999998" + markerHeight="5.5999999" + viewBox="0 0 7.7 5.6" + inkscape:isstock="true" + inkscape:collect="always" + preserveAspectRatio="xMidYMid"> + <path + transform="scale(0.7)" + d="M -2,-4 9,0 -2,4 c 2,-2.33 2,-5.66 0,-8 z" + style="fill:context-stroke;fill-rule:evenodd;stroke:none" + id="arrow2L-1" /> + </marker> + <marker + style="overflow:visible" + id="Arrow2-9-7" + refX="0" + refY="0" + orient="auto-start-reverse" + inkscape:stockid="Arrow2" + markerWidth="7.6999998" + markerHeight="5.5999999" + viewBox="0 0 7.7 5.6" + inkscape:isstock="true" + inkscape:collect="always" + preserveAspectRatio="xMidYMid"> + <path + transform="scale(0.7)" + d="M -2,-4 9,0 -2,4 c 2,-2.33 2,-5.66 0,-8 z" + style="fill:context-stroke;fill-rule:evenodd;stroke:none" + id="arrow2L-1-0" /> + </marker> + <marker + style="overflow:visible" + id="Arrow2-93" + refX="0" + refY="0" + orient="auto-start-reverse" + inkscape:stockid="Arrow2" + markerWidth="7.6999998" + markerHeight="5.5999999" + viewBox="0 0 7.7 5.6" + inkscape:isstock="true" + inkscape:collect="always" + preserveAspectRatio="xMidYMid"> + <path + transform="scale(0.7)" + d="M -2,-4 9,0 -2,4 c 2,-2.33 2,-5.66 0,-8 z" + style="fill:context-stroke;fill-rule:evenodd;stroke:none" + id="arrow2L-6" /> + </marker> + <marker + style="overflow:visible" + id="Arrow2-9-7-2" + refX="0" + refY="0" + orient="auto-start-reverse" + inkscape:stockid="Arrow2" + markerWidth="7.6999998" + markerHeight="5.5999999" + viewBox="0 0 7.7 5.6" + inkscape:isstock="true" + inkscape:collect="always" + preserveAspectRatio="xMidYMid"> + <path + transform="scale(0.7)" + d="M -2,-4 9,0 -2,4 c 2,-2.33 2,-5.66 0,-8 z" + style="fill:context-stroke;fill-rule:evenodd;stroke:none" + id="arrow2L-1-0-6" /> + </marker> + <marker + style="overflow:visible" + id="Arrow2-93-1" + refX="0" + refY="0" + orient="auto-start-reverse" + inkscape:stockid="Arrow2" + markerWidth="7.6999998" + markerHeight="5.5999999" + viewBox="0 0 7.7 5.6" + inkscape:isstock="true" + inkscape:collect="always" + preserveAspectRatio="xMidYMid"> + <path + transform="scale(0.7)" + d="M -2,-4 9,0 -2,4 c 2,-2.33 2,-5.66 0,-8 z" + style="fill:context-stroke;fill-rule:evenodd;stroke:none" + id="arrow2L-6-8" /> + </marker> + <marker + style="overflow:visible" + id="Arrow2-9-75" + refX="0" + refY="0" + orient="auto-start-reverse" + inkscape:stockid="Arrow2" + markerWidth="7.6999998" + markerHeight="5.5999999" + viewBox="0 0 7.7 5.6" + inkscape:isstock="true" + inkscape:collect="always" + preserveAspectRatio="xMidYMid"> + <path + transform="scale(0.7)" + d="M -2,-4 9,0 -2,4 c 2,-2.33 2,-5.66 0,-8 z" + style="fill:context-stroke;fill-rule:evenodd;stroke:none" + id="arrow2L-1-9" /> + </marker> + <marker + style="overflow:visible" + id="Arrow2-9-75-2" + refX="0" + refY="0" + orient="auto-start-reverse" + inkscape:stockid="Arrow2" + markerWidth="7.6999998" + markerHeight="5.5999999" + viewBox="0 0 7.7 5.6" + inkscape:isstock="true" + inkscape:collect="always" + preserveAspectRatio="xMidYMid"> + <path + transform="scale(0.7)" + d="M -2,-4 9,0 -2,4 c 2,-2.33 2,-5.66 0,-8 z" + style="fill:context-stroke;fill-rule:evenodd;stroke:none" + id="arrow2L-1-9-8" /> + </marker> + <marker + style="overflow:visible" + id="Arrow2-9-75-7" + refX="0" + refY="0" + orient="auto-start-reverse" + inkscape:stockid="Arrow2" + markerWidth="7.6999998" + markerHeight="5.5999999" + viewBox="0 0 7.7 5.6" + inkscape:isstock="true" + inkscape:collect="always" + preserveAspectRatio="xMidYMid"> + <path + transform="scale(0.7)" + d="M -2,-4 9,0 -2,4 c 2,-2.33 2,-5.66 0,-8 z" + style="fill:context-stroke;fill-rule:evenodd;stroke:none" + id="arrow2L-1-9-3" /> + </marker> + <marker + style="overflow:visible" + id="Arrow2-9-75-7-1" + refX="0" + refY="0" + orient="auto-start-reverse" + inkscape:stockid="Arrow2" + markerWidth="7.6999998" + markerHeight="5.5999999" + viewBox="0 0 7.7 5.6" + inkscape:isstock="true" + inkscape:collect="always" + preserveAspectRatio="xMidYMid"> + <path + transform="scale(0.7)" + d="M -2,-4 9,0 -2,4 c 2,-2.33 2,-5.66 0,-8 z" + style="fill:context-stroke;fill-rule:evenodd;stroke:none" + id="arrow2L-1-9-3-2" /> + </marker> + <marker + style="overflow:visible" + id="Arrow2-93-1-4" + refX="0" + refY="0" + orient="auto-start-reverse" + inkscape:stockid="Arrow2" + markerWidth="7.6999998" + markerHeight="5.5999999" + viewBox="0 0 7.7 5.6" + inkscape:isstock="true" + inkscape:collect="always" + preserveAspectRatio="xMidYMid"> + <path + transform="scale(0.7)" + d="M -2,-4 9,0 -2,4 c 2,-2.33 2,-5.66 0,-8 z" + style="fill:context-stroke;fill-rule:evenodd;stroke:none" + id="arrow2L-6-8-7" /> + </marker> + <marker + style="overflow:visible" + id="Arrow2-9-7-2-8" + refX="0" + refY="0" + orient="auto-start-reverse" + inkscape:stockid="Arrow2" + markerWidth="7.6999998" + markerHeight="5.5999999" + viewBox="0 0 7.7 5.6" + inkscape:isstock="true" + inkscape:collect="always" + preserveAspectRatio="xMidYMid"> + <path + transform="scale(0.7)" + d="M -2,-4 9,0 -2,4 c 2,-2.33 2,-5.66 0,-8 z" + style="fill:context-stroke;fill-rule:evenodd;stroke:none" + id="arrow2L-1-0-6-4" /> + </marker> + </defs> + <g + inkscape:label="Layer 1" + inkscape:groupmode="layer" + id="layer1" + sodipodi:insensitive="true"> + <rect + style="fill:#ffffff;stroke:none;stroke-width:1;stop-color:#000000" + id="rect288" + width="209.84705" + height="104.42732" + x="0.77790999" + y="0.93738818" /> + </g> + <g + inkscape:groupmode="layer" + id="layer2" + inkscape:label="Layer 2"> + <text + xml:space="preserve" + style="font-size:8.46667px;line-height:1.25;font-family:sans-serif;text-align:center;text-anchor:middle;stroke-width:0.264583;fill:#000000" + x="164.56372" + y="99.307442" + id="text951"><tspan + sodipodi:role="line" + id="tspan949" + style="stroke-width:0.264583;fill:#000000" + x="164.56372" + y="99.307442">$\{\}$</tspan></text> + <text + xml:space="preserve" + style="font-size:8.46667px;line-height:1.25;font-family:sans-serif;text-align:center;text-anchor:middle;stroke-width:0.264583;fill:#000000" + x="164.56372" + y="13.151893" + id="text1005"><tspan + sodipodi:role="line" + id="tspan1003" + style="stroke-width:0.264583;fill:#000000" + x="164.56372" + y="13.151893">$\{a,b,c\}$</tspan></text> + <g + id="g1175" + transform="translate(51.996784,3.5774043)"> + <text + xml:space="preserve" + style="font-size:8.46667px;line-height:1.25;font-family:sans-serif;text-align:center;text-anchor:middle;stroke-width:0.264583;fill:#000000" + x="49.27084" + y="67.008698" + id="text1009"><tspan + sodipodi:role="line" + id="tspan1007" + style="stroke-width:0.264583;fill:#000000" + x="49.27084" + y="67.008698">$\{a\}$</tspan></text> + <text + xml:space="preserve" + style="font-size:8.46667px;line-height:1.25;font-family:sans-serif;text-align:center;text-anchor:middle;stroke-width:0.264583;fill:#000000" + x="112.90984" + y="67.017166" + id="text1009-3"><tspan + sodipodi:role="line" + id="tspan1007-6" + style="stroke-width:0.264583;fill:#000000" + x="112.90984" + y="67.017166">$\{b\}$</tspan></text> + <text + xml:space="preserve" + style="font-size:8.46667px;line-height:1.25;font-family:sans-serif;text-align:center;text-anchor:middle;stroke-width:0.264583;fill:#000000" + x="176.20593" + y="67.008698" + id="text1009-7"><tspan + sodipodi:role="line" + id="tspan1007-5" + style="stroke-width:0.264583;fill:#000000" + x="176.20593" + y="67.008698">$\{c\}$</tspan></text> + </g> + <g + id="g1183" + transform="translate(51.996784,1.0317046)" + style="fill:#000000"> + <text + xml:space="preserve" + style="font-size:8.46667px;line-height:1.25;font-family:sans-serif;text-align:center;text-anchor:middle;stroke-width:0.264583;fill:#000000" + x="112.90984" + y="40.841526" + id="text1117"><tspan + sodipodi:role="line" + id="tspan1115" + style="stroke-width:0.264583;fill:#000000" + x="112.90984" + y="40.841526">$\{a,c\}$</tspan></text> + <text + xml:space="preserve" + style="font-size:8.46667px;line-height:1.25;font-family:sans-serif;text-align:center;text-anchor:middle;stroke-width:0.264583;fill:#000000" + x="49.27084" + y="40.841526" + id="text1117-3"><tspan + sodipodi:role="line" + id="tspan1115-5" + style="stroke-width:0.264583;fill:#000000" + x="49.27084" + y="40.841526">$\{a,b\}$</tspan></text> + <text + xml:space="preserve" + style="font-size:8.46667px;line-height:1.25;font-family:sans-serif;text-align:center;text-anchor:middle;stroke-width:0.264583;fill:#000000" + x="176.20593" + y="40.841526" + id="text1117-6"><tspan + sodipodi:role="line" + id="tspan1115-2" + style="stroke-width:0.264583;fill:#000000" + x="176.20593" + y="40.841526">$\{b,c\}$</tspan></text> + </g> + <path + style="fill:none;stroke:#000000;stroke-width:0.5;stroke-linecap:butt;stroke-linejoin:miter;stroke-dasharray:none;stroke-opacity:1;marker-end:url(#Arrow2)" + d="M 153.33622,90.367682 118.34198,73.428915" + id="path1300" /> + <path + style="fill:none;stroke:#000000;stroke-width:0.5;stroke-linecap:butt;stroke-linejoin:miter;stroke-dasharray:none;stroke-opacity:1;marker-end:url(#Arrow2-9)" + d="M 177.46016,90.367682 212.4544,73.428915" + id="path1300-2" /> + <path + style="fill:none;stroke:#000000;stroke-width:0.5;stroke-linecap:butt;stroke-linejoin:miter;stroke-dasharray:none;stroke-opacity:1;marker-end:url(#Arrow2-93)" + d="M 153.33622,61.655656 118.34198,44.716889" + id="path1300-0" /> + <path + style="fill:none;stroke:#000000;stroke-width:0.5;stroke-linecap:butt;stroke-linejoin:miter;stroke-dasharray:none;stroke-opacity:1;marker-end:url(#Arrow2-9-7)" + d="M 177.46016,61.655656 212.4544,44.716889" + id="path1300-2-6" /> + <path + style="fill:none;stroke:#000000;stroke-width:0.5;stroke-linecap:butt;stroke-linejoin:miter;stroke-dasharray:none;stroke-opacity:1;marker-end:url(#Arrow2-93-1)" + d="M 118.34198,61.655656 153.33622,44.716889" + id="path1300-0-7" /> + <path + style="fill:none;stroke:#000000;stroke-width:0.5;stroke-linecap:butt;stroke-linejoin:miter;stroke-dasharray:none;stroke-opacity:1;marker-end:url(#Arrow2-9-7-2)" + d="M 212.4544,61.655656 177.46016,44.716889" + id="path1300-2-6-9" /> + <path + style="fill:none;stroke:#000000;stroke-width:0.5;stroke-linecap:butt;stroke-linejoin:miter;stroke-dasharray:none;stroke-opacity:1;marker-end:url(#Arrow2-93-1-4)" + d="M 118.34198,34.227412 153.33622,17.288645" + id="path1300-0-7-5" /> + <path + style="fill:none;stroke:#000000;stroke-width:0.5;stroke-linecap:butt;stroke-linejoin:miter;stroke-dasharray:none;stroke-opacity:1;marker-end:url(#Arrow2-9-7-2-8)" + d="M 212.4544,34.227412 177.46016,17.288645" + id="path1300-2-6-9-0" /> + <path + style="fill:none;stroke:#000000;stroke-width:0.5;stroke-linecap:butt;stroke-linejoin:miter;stroke-dasharray:none;stroke-opacity:1;marker-end:url(#Arrow2-9-75)" + d="m 228.52843,61.091809 0.33313,-12.554874 m -0.33313,12.554874 0.33313,-12.554874" + id="path1300-2-2" + sodipodi:nodetypes="cc" /> + <path + style="fill:none;stroke:#000000;stroke-width:0.5;stroke-linecap:butt;stroke-linejoin:miter;stroke-dasharray:none;stroke-opacity:1;marker-end:url(#Arrow2-9-75-2)" + d="m 101.90418,61.091809 0.33313,-12.554874 m -0.33313,12.554874 0.33313,-12.554874" + id="path1300-2-2-9" + sodipodi:nodetypes="cc" /> + <path + style="fill:none;stroke:#000000;stroke-width:0.5;stroke-linecap:butt;stroke-linejoin:miter;stroke-dasharray:none;stroke-opacity:1;marker-end:url(#Arrow2-9-75-7)" + d="m 165.29305,89.571762 0.33313,-12.554874 m -0.33313,12.554874 0.33313,-12.554874" + id="path1300-2-2-6" + sodipodi:nodetypes="cc" /> + <path + style="fill:none;stroke:#000000;stroke-width:0.5;stroke-linecap:butt;stroke-linejoin:miter;stroke-dasharray:none;stroke-opacity:1;marker-end:url(#Arrow2-9-75-7-1)" + d="m 165.29305,32.445235 0.33313,-12.554874 m -0.33313,12.554874 0.33313,-12.554874" + id="path1300-2-2-6-9" + sodipodi:nodetypes="cc" /> + <circle + style="fill:#ff0000;stroke:none;stroke-width:0.499999;stroke-dasharray:none;stop-color:#000000" + id="path3663" + cx="147.35568" + cy="95.24971" + r="2.7302806" /> + <circle + style="fill:#008000;stroke:none;stroke-width:0.499999;stroke-dasharray:none;stop-color:#000000" + id="path3663-3" + cx="126.08154" + cy="67.968384" + r="2.7302806" /> + <circle + style="fill:#800080;stroke:none;stroke-width:0.499999;stroke-dasharray:none;stop-color:#000000" + id="path3663-6" + cx="119.58919" + cy="67.645035" + r="2.7302806" /> + <circle + style="fill:#ff0000;stroke:none;stroke-width:0.499999;stroke-dasharray:none;stop-color:#000000" + id="path3663-1" + cx="18.004833" + cy="39.402473" + r="2.7302806" /> + <circle + style="fill:#008000;stroke:none;stroke-width:0.499999;stroke-dasharray:none;stop-color:#000000" + id="path3663-3-0" + cx="18.004833" + cy="30.371933" + r="2.7302806" /> + <circle + style="fill:#800080;stroke:none;stroke-width:0.499999;stroke-dasharray:none;stop-color:#000000" + id="path3663-6-6" + cx="18.004833" + cy="21.341394" + r="2.7302806" /> + <text + xml:space="preserve" + style="font-size:8.46667px;line-height:1.25;font-family:sans-serif;stroke-width:0.264583;fill:#000000" + x="6.9525447" + y="13.702217" + id="text3707"><tspan + sodipodi:role="line" + id="tspan3705" + style="stroke-width:0.264583;fill:#000000" + x="6.9525447" + y="13.702217">$write(\{a\})$:</tspan></text> + <text + xml:space="preserve" + style="font-size:8.46667px;line-height:1.25;font-family:sans-serif;fill:#000000;stroke-width:0.264583" + x="23.457415" + y="24.042637" + id="text3750"><tspan + sodipodi:role="line" + id="tspan3748" + style="fill:#000000;stroke-width:0.264583" + x="23.457415" + y="24.042637">$\sqsupseteq \{a\} \to$ OK</tspan></text> + <text + xml:space="preserve" + style="font-size:8.46667px;line-height:1.25;font-family:sans-serif;fill:#000000;stroke-width:0.264583" + x="23.457415" + y="33.02087" + id="text3750-3"><tspan + sodipodi:role="line" + id="tspan3748-2" + style="fill:#000000;stroke-width:0.264583" + x="23.457415" + y="33.02087">$\sqsupseteq \{a\} \to$ OK</tspan></text> + <text + xml:space="preserve" + style="font-size:8.46667px;line-height:1.25;font-family:sans-serif;fill:#999999;stroke-width:0.264583" + x="23.457415" + y="41.972523" + id="text3750-0"><tspan + sodipodi:role="line" + id="tspan3748-6" + style="fill:#999999;stroke-width:0.264583" + x="23.457415" + y="41.972523">$\not\sqsupseteq \{a\}$</tspan></text> + <text + xml:space="preserve" + style="font-size:8.46667px;line-height:1.25;font-family:sans-serif;fill:#000000;stroke-width:0.264583" + x="14.395845" + y="52.022549" + id="text4280"><tspan + sodipodi:role="line" + id="tspan4278" + style="fill:#000000;stroke-width:0.264583" + x="14.395845" + y="52.022549">return OK</tspan></text> + <circle + style="fill:#ff0000;stroke:none;stroke-width:0.499999;stroke-dasharray:none;stop-color:#000000" + id="path3663-1-4" + cx="18.004833" + cy="90.979645" + r="2.7302806" /> + <circle + style="fill:#008000;stroke:none;stroke-width:0.499999;stroke-dasharray:none;stop-color:#000000" + id="path3663-3-0-5" + cx="18.004833" + cy="81.949104" + r="2.7302806" /> + <circle + style="fill:#800080;stroke:none;stroke-width:0.499999;stroke-dasharray:none;stop-color:#000000" + id="path3663-6-6-2" + cx="18.004833" + cy="72.918564" + r="2.7302806" /> + <text + xml:space="preserve" + style="font-size:8.46667px;line-height:1.25;font-family:sans-serif;fill:#000000;stroke-width:0.264583" + x="6.9525447" + y="65.279381" + id="text3707-5"><tspan + sodipodi:role="line" + id="tspan3705-4" + style="fill:#000000;stroke-width:0.264583" + x="6.9525447" + y="65.279381">$write(\{b\})$:</tspan></text> + <text + xml:space="preserve" + style="font-size:8.46667px;line-height:1.25;font-family:sans-serif;fill:#999999;stroke-width:0.264583" + x="23.457415" + y="75.619804" + id="text3750-7"><tspan + sodipodi:role="line" + id="tspan3748-4" + style="fill:#999999;stroke-width:0.264583" + x="23.457415" + y="75.619804">$\not\sqsupseteq \{b\}$</tspan></text> + <text + xml:space="preserve" + style="font-size:8.46667px;line-height:1.25;font-family:sans-serif;fill:#999999;stroke-width:0.264583" + x="23.457415" + y="84.598038" + id="text3750-3-4"><tspan + sodipodi:role="line" + id="tspan3748-2-3" + style="fill:#999999;stroke-width:0.264583" + x="23.457415" + y="84.598038">$\not\sqsupseteq \{b\}$</tspan></text> + <text + xml:space="preserve" + style="font-size:8.46667px;line-height:1.25;font-family:sans-serif;fill:#999999;stroke-width:0.264583" + x="23.457415" + y="93.54969" + id="text3750-0-0"><tspan + sodipodi:role="line" + id="tspan3748-6-7" + style="fill:#999999;stroke-width:0.264583" + x="23.457415" + y="93.54969">$\not\sqsupseteq \{b\}$</tspan></text> + </g> +</svg> diff --git a/doc/talks/2023-01-18-tocatta/assets/lattice9.svg b/doc/talks/2023-01-18-tocatta/assets/lattice9.svg new file mode 100644 index 00000000..8b3c6585 --- /dev/null +++ b/doc/talks/2023-01-18-tocatta/assets/lattice9.svg @@ -0,0 +1,587 @@ +<?xml version="1.0" encoding="UTF-8" standalone="no"?> +<!-- Created with Inkscape (http://www.inkscape.org/) --> + +<svg + width="1000" + height="400" + viewBox="0 0 264.58333 105.83333" + version="1.1" + id="svg5" + inkscape:version="1.2.2 (b0a8486541, 2022-12-01)" + sodipodi:docname="lattice9.svg" + 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="namedview7" + pagecolor="#ffffff" + bordercolor="#666666" + borderopacity="1.0" + inkscape:showpageshadow="2" + inkscape:pageopacity="0.0" + inkscape:pagecheckerboard="0" + inkscape:deskcolor="#d1d1d1" + inkscape:document-units="mm" + showgrid="false" + inkscape:zoom="1.4734708" + inkscape:cx="451.65469" + inkscape:cy="272.14655" + inkscape:window-width="1920" + inkscape:window-height="999" + inkscape:window-x="0" + inkscape:window-y="0" + inkscape:window-maximized="1" + inkscape:current-layer="layer2" /> + <defs + id="defs2"> + <marker + style="overflow:visible" + id="Arrow2" + refX="0" + refY="0" + orient="auto-start-reverse" + inkscape:stockid="Arrow2" + markerWidth="7.6999998" + markerHeight="5.5999999" + viewBox="0 0 7.7 5.6" + inkscape:isstock="true" + inkscape:collect="always" + preserveAspectRatio="xMidYMid"> + <path + transform="scale(0.7)" + d="M -2,-4 9,0 -2,4 c 2,-2.33 2,-5.66 0,-8 z" + style="fill:context-stroke;fill-rule:evenodd;stroke:none" + id="arrow2L" /> + </marker> + <marker + style="overflow:visible" + id="Arrow2-9" + refX="0" + refY="0" + orient="auto-start-reverse" + inkscape:stockid="Arrow2" + markerWidth="7.6999998" + markerHeight="5.5999999" + viewBox="0 0 7.7 5.6" + inkscape:isstock="true" + inkscape:collect="always" + preserveAspectRatio="xMidYMid"> + <path + transform="scale(0.7)" + d="M -2,-4 9,0 -2,4 c 2,-2.33 2,-5.66 0,-8 z" + style="fill:context-stroke;fill-rule:evenodd;stroke:none" + id="arrow2L-1" /> + </marker> + <marker + style="overflow:visible" + id="Arrow2-9-7" + refX="0" + refY="0" + orient="auto-start-reverse" + inkscape:stockid="Arrow2" + markerWidth="7.6999998" + markerHeight="5.5999999" + viewBox="0 0 7.7 5.6" + inkscape:isstock="true" + inkscape:collect="always" + preserveAspectRatio="xMidYMid"> + <path + transform="scale(0.7)" + d="M -2,-4 9,0 -2,4 c 2,-2.33 2,-5.66 0,-8 z" + style="fill:context-stroke;fill-rule:evenodd;stroke:none" + id="arrow2L-1-0" /> + </marker> + <marker + style="overflow:visible" + id="Arrow2-93" + refX="0" + refY="0" + orient="auto-start-reverse" + inkscape:stockid="Arrow2" + markerWidth="7.6999998" + markerHeight="5.5999999" + viewBox="0 0 7.7 5.6" + inkscape:isstock="true" + inkscape:collect="always" + preserveAspectRatio="xMidYMid"> + <path + transform="scale(0.7)" + d="M -2,-4 9,0 -2,4 c 2,-2.33 2,-5.66 0,-8 z" + style="fill:context-stroke;fill-rule:evenodd;stroke:none" + id="arrow2L-6" /> + </marker> + <marker + style="overflow:visible" + id="Arrow2-9-7-2" + refX="0" + refY="0" + orient="auto-start-reverse" + inkscape:stockid="Arrow2" + markerWidth="7.6999998" + markerHeight="5.5999999" + viewBox="0 0 7.7 5.6" + inkscape:isstock="true" + inkscape:collect="always" + preserveAspectRatio="xMidYMid"> + <path + transform="scale(0.7)" + d="M -2,-4 9,0 -2,4 c 2,-2.33 2,-5.66 0,-8 z" + style="fill:context-stroke;fill-rule:evenodd;stroke:none" + id="arrow2L-1-0-6" /> + </marker> + <marker + style="overflow:visible" + id="Arrow2-93-1" + refX="0" + refY="0" + orient="auto-start-reverse" + inkscape:stockid="Arrow2" + markerWidth="7.6999998" + markerHeight="5.5999999" + viewBox="0 0 7.7 5.6" + inkscape:isstock="true" + inkscape:collect="always" + preserveAspectRatio="xMidYMid"> + <path + transform="scale(0.7)" + d="M -2,-4 9,0 -2,4 c 2,-2.33 2,-5.66 0,-8 z" + style="fill:context-stroke;fill-rule:evenodd;stroke:none" + id="arrow2L-6-8" /> + </marker> + <marker + style="overflow:visible" + id="Arrow2-9-75" + refX="0" + refY="0" + orient="auto-start-reverse" + inkscape:stockid="Arrow2" + markerWidth="7.6999998" + markerHeight="5.5999999" + viewBox="0 0 7.7 5.6" + inkscape:isstock="true" + inkscape:collect="always" + preserveAspectRatio="xMidYMid"> + <path + transform="scale(0.7)" + d="M -2,-4 9,0 -2,4 c 2,-2.33 2,-5.66 0,-8 z" + style="fill:context-stroke;fill-rule:evenodd;stroke:none" + id="arrow2L-1-9" /> + </marker> + <marker + style="overflow:visible" + id="Arrow2-9-75-2" + refX="0" + refY="0" + orient="auto-start-reverse" + inkscape:stockid="Arrow2" + markerWidth="7.6999998" + markerHeight="5.5999999" + viewBox="0 0 7.7 5.6" + inkscape:isstock="true" + inkscape:collect="always" + preserveAspectRatio="xMidYMid"> + <path + transform="scale(0.7)" + d="M -2,-4 9,0 -2,4 c 2,-2.33 2,-5.66 0,-8 z" + style="fill:context-stroke;fill-rule:evenodd;stroke:none" + id="arrow2L-1-9-8" /> + </marker> + <marker + style="overflow:visible" + id="Arrow2-9-75-7" + refX="0" + refY="0" + orient="auto-start-reverse" + inkscape:stockid="Arrow2" + markerWidth="7.6999998" + markerHeight="5.5999999" + viewBox="0 0 7.7 5.6" + inkscape:isstock="true" + inkscape:collect="always" + preserveAspectRatio="xMidYMid"> + <path + transform="scale(0.7)" + d="M -2,-4 9,0 -2,4 c 2,-2.33 2,-5.66 0,-8 z" + style="fill:context-stroke;fill-rule:evenodd;stroke:none" + id="arrow2L-1-9-3" /> + </marker> + <marker + style="overflow:visible" + id="Arrow2-9-75-7-1" + refX="0" + refY="0" + orient="auto-start-reverse" + inkscape:stockid="Arrow2" + markerWidth="7.6999998" + markerHeight="5.5999999" + viewBox="0 0 7.7 5.6" + inkscape:isstock="true" + inkscape:collect="always" + preserveAspectRatio="xMidYMid"> + <path + transform="scale(0.7)" + d="M -2,-4 9,0 -2,4 c 2,-2.33 2,-5.66 0,-8 z" + style="fill:context-stroke;fill-rule:evenodd;stroke:none" + id="arrow2L-1-9-3-2" /> + </marker> + <marker + style="overflow:visible" + id="Arrow2-93-1-4" + refX="0" + refY="0" + orient="auto-start-reverse" + inkscape:stockid="Arrow2" + markerWidth="7.6999998" + markerHeight="5.5999999" + viewBox="0 0 7.7 5.6" + inkscape:isstock="true" + inkscape:collect="always" + preserveAspectRatio="xMidYMid"> + <path + transform="scale(0.7)" + d="M -2,-4 9,0 -2,4 c 2,-2.33 2,-5.66 0,-8 z" + style="fill:context-stroke;fill-rule:evenodd;stroke:none" + id="arrow2L-6-8-7" /> + </marker> + <marker + style="overflow:visible" + id="Arrow2-9-7-2-8" + refX="0" + refY="0" + orient="auto-start-reverse" + inkscape:stockid="Arrow2" + markerWidth="7.6999998" + markerHeight="5.5999999" + viewBox="0 0 7.7 5.6" + inkscape:isstock="true" + inkscape:collect="always" + preserveAspectRatio="xMidYMid"> + <path + transform="scale(0.7)" + d="M -2,-4 9,0 -2,4 c 2,-2.33 2,-5.66 0,-8 z" + style="fill:context-stroke;fill-rule:evenodd;stroke:none" + id="arrow2L-1-0-6-4" /> + </marker> + </defs> + <g + inkscape:label="Layer 1" + inkscape:groupmode="layer" + id="layer1" + sodipodi:insensitive="true"> + <rect + style="fill:#ffffff;stroke:none;stroke-width:1;stop-color:#000000" + id="rect288" + width="209.84705" + height="104.42732" + x="0.77790999" + y="0.93738818" /> + </g> + <g + inkscape:groupmode="layer" + id="layer2" + inkscape:label="Layer 2"> + <text + xml:space="preserve" + style="font-size:8.46667px;line-height:1.25;font-family:sans-serif;text-align:center;text-anchor:middle;stroke-width:0.264583;fill:#000000" + x="164.56372" + y="99.307442" + id="text951"><tspan + sodipodi:role="line" + id="tspan949" + style="stroke-width:0.264583;fill:#000000" + x="164.56372" + y="99.307442">$\{\}$</tspan></text> + <text + xml:space="preserve" + style="font-size:8.46667px;line-height:1.25;font-family:sans-serif;text-align:center;text-anchor:middle;stroke-width:0.264583;fill:#000000" + x="164.56372" + y="13.151893" + id="text1005"><tspan + sodipodi:role="line" + id="tspan1003" + style="stroke-width:0.264583;fill:#000000" + x="164.56372" + y="13.151893">$\{a,b,c\}$</tspan></text> + <g + id="g1175" + transform="translate(51.996784,3.5774043)"> + <text + xml:space="preserve" + style="font-size:8.46667px;line-height:1.25;font-family:sans-serif;text-align:center;text-anchor:middle;stroke-width:0.264583;fill:#000000" + x="49.27084" + y="67.008698" + id="text1009"><tspan + sodipodi:role="line" + id="tspan1007" + style="stroke-width:0.264583;fill:#000000" + x="49.27084" + y="67.008698">$\{a\}$</tspan></text> + <text + xml:space="preserve" + style="font-size:8.46667px;line-height:1.25;font-family:sans-serif;text-align:center;text-anchor:middle;stroke-width:0.264583;fill:#000000" + x="112.90984" + y="67.017166" + id="text1009-3"><tspan + sodipodi:role="line" + id="tspan1007-6" + style="stroke-width:0.264583;fill:#000000" + x="112.90984" + y="67.017166">$\{b\}$</tspan></text> + <text + xml:space="preserve" + style="font-size:8.46667px;line-height:1.25;font-family:sans-serif;text-align:center;text-anchor:middle;stroke-width:0.264583;fill:#000000" + x="176.20593" + y="67.008698" + id="text1009-7"><tspan + sodipodi:role="line" + id="tspan1007-5" + style="stroke-width:0.264583;fill:#000000" + x="176.20593" + y="67.008698">$\{c\}$</tspan></text> + </g> + <g + id="g1183" + transform="translate(51.996784,1.0317046)" + style="fill:#000000"> + <text + xml:space="preserve" + style="font-size:8.46667px;line-height:1.25;font-family:sans-serif;text-align:center;text-anchor:middle;stroke-width:0.264583;fill:#000000" + x="112.90984" + y="40.841526" + id="text1117"><tspan + sodipodi:role="line" + id="tspan1115" + style="stroke-width:0.264583;fill:#000000" + x="112.90984" + y="40.841526">$\{a,c\}$</tspan></text> + <text + xml:space="preserve" + style="font-size:8.46667px;line-height:1.25;font-family:sans-serif;text-align:center;text-anchor:middle;stroke-width:0.264583;fill:#000000" + x="49.27084" + y="40.841526" + id="text1117-3"><tspan + sodipodi:role="line" + id="tspan1115-5" + style="stroke-width:0.264583;fill:#000000" + x="49.27084" + y="40.841526">$\{a,b\}$</tspan></text> + <text + xml:space="preserve" + style="font-size:8.46667px;line-height:1.25;font-family:sans-serif;text-align:center;text-anchor:middle;stroke-width:0.264583;fill:#000000" + x="176.20593" + y="40.841526" + id="text1117-6"><tspan + sodipodi:role="line" + id="tspan1115-2" + style="stroke-width:0.264583;fill:#000000" + x="176.20593" + y="40.841526">$\{b,c\}$</tspan></text> + </g> + <path + style="fill:none;stroke:#000000;stroke-width:0.5;stroke-linecap:butt;stroke-linejoin:miter;stroke-dasharray:none;stroke-opacity:1;marker-end:url(#Arrow2)" + d="M 153.33622,90.367682 118.34198,73.428915" + id="path1300" /> + <path + style="fill:none;stroke:#000000;stroke-width:0.5;stroke-linecap:butt;stroke-linejoin:miter;stroke-dasharray:none;stroke-opacity:1;marker-end:url(#Arrow2-9)" + d="M 177.46016,90.367682 212.4544,73.428915" + id="path1300-2" /> + <path + style="fill:none;stroke:#000000;stroke-width:0.5;stroke-linecap:butt;stroke-linejoin:miter;stroke-dasharray:none;stroke-opacity:1;marker-end:url(#Arrow2-93)" + d="M 153.33622,61.655656 118.34198,44.716889" + id="path1300-0" /> + <path + style="fill:none;stroke:#000000;stroke-width:0.5;stroke-linecap:butt;stroke-linejoin:miter;stroke-dasharray:none;stroke-opacity:1;marker-end:url(#Arrow2-9-7)" + d="M 177.46016,61.655656 212.4544,44.716889" + id="path1300-2-6" /> + <path + style="fill:none;stroke:#000000;stroke-width:0.5;stroke-linecap:butt;stroke-linejoin:miter;stroke-dasharray:none;stroke-opacity:1;marker-end:url(#Arrow2-93-1)" + d="M 118.34198,61.655656 153.33622,44.716889" + id="path1300-0-7" /> + <path + style="fill:none;stroke:#000000;stroke-width:0.5;stroke-linecap:butt;stroke-linejoin:miter;stroke-dasharray:none;stroke-opacity:1;marker-end:url(#Arrow2-9-7-2)" + d="M 212.4544,61.655656 177.46016,44.716889" + id="path1300-2-6-9" /> + <path + style="fill:none;stroke:#000000;stroke-width:0.5;stroke-linecap:butt;stroke-linejoin:miter;stroke-dasharray:none;stroke-opacity:1;marker-end:url(#Arrow2-93-1-4)" + d="M 118.34198,34.227412 153.33622,17.288645" + id="path1300-0-7-5" /> + <path + style="fill:none;stroke:#000000;stroke-width:0.5;stroke-linecap:butt;stroke-linejoin:miter;stroke-dasharray:none;stroke-opacity:1;marker-end:url(#Arrow2-9-7-2-8)" + d="M 212.4544,34.227412 177.46016,17.288645" + id="path1300-2-6-9-0" /> + <path + style="fill:none;stroke:#000000;stroke-width:0.5;stroke-linecap:butt;stroke-linejoin:miter;stroke-dasharray:none;stroke-opacity:1;marker-end:url(#Arrow2-9-75)" + d="m 228.52843,61.091809 0.33313,-12.554874 m -0.33313,12.554874 0.33313,-12.554874" + id="path1300-2-2" + sodipodi:nodetypes="cc" /> + <path + style="fill:none;stroke:#000000;stroke-width:0.5;stroke-linecap:butt;stroke-linejoin:miter;stroke-dasharray:none;stroke-opacity:1;marker-end:url(#Arrow2-9-75-2)" + d="m 101.90418,61.091809 0.33313,-12.554874 m -0.33313,12.554874 0.33313,-12.554874" + id="path1300-2-2-9" + sodipodi:nodetypes="cc" /> + <path + style="fill:none;stroke:#000000;stroke-width:0.5;stroke-linecap:butt;stroke-linejoin:miter;stroke-dasharray:none;stroke-opacity:1;marker-end:url(#Arrow2-9-75-7)" + d="m 165.29305,89.571762 0.33313,-12.554874 m -0.33313,12.554874 0.33313,-12.554874" + id="path1300-2-2-6" + sodipodi:nodetypes="cc" /> + <path + style="fill:none;stroke:#000000;stroke-width:0.5;stroke-linecap:butt;stroke-linejoin:miter;stroke-dasharray:none;stroke-opacity:1;marker-end:url(#Arrow2-9-75-7-1)" + d="m 165.29305,32.445235 0.33313,-12.554874 m -0.33313,12.554874 0.33313,-12.554874" + id="path1300-2-2-6-9" + sodipodi:nodetypes="cc" /> + <circle + style="fill:#ff0000;stroke:none;stroke-width:0.499999;stroke-dasharray:none;stop-color:#000000" + id="path3663" + cx="177.03145" + cy="67.991631" + r="2.7302806" /> + <circle + style="fill:#008000;stroke:none;stroke-width:0.499999;stroke-dasharray:none;stop-color:#000000" + id="path3663-3" + cx="126.08154" + cy="67.968384" + r="2.7302806" /> + <circle + style="fill:#800080;stroke:none;stroke-width:0.499999;stroke-dasharray:none;stop-color:#000000" + id="path3663-6" + cx="119.58919" + cy="67.645035" + r="2.7302806" /> + <circle + style="fill:#ff0000;stroke:none;stroke-width:0.499999;stroke-dasharray:none;stop-color:#000000" + id="path3663-1" + cx="18.004833" + cy="39.402473" + r="2.7302806" /> + <circle + style="fill:#008000;stroke:none;stroke-width:0.499999;stroke-dasharray:none;stop-color:#000000" + id="path3663-3-0" + cx="18.004833" + cy="30.371933" + r="2.7302806" /> + <circle + style="fill:#800080;stroke:none;stroke-width:0.499999;stroke-dasharray:none;stop-color:#000000" + id="path3663-6-6" + cx="18.004833" + cy="21.341394" + r="2.7302806" /> + <text + xml:space="preserve" + style="font-size:8.46667px;line-height:1.25;font-family:sans-serif;stroke-width:0.264583;fill:#000000" + x="6.9525447" + y="13.702217" + id="text3707"><tspan + sodipodi:role="line" + id="tspan3705" + style="stroke-width:0.264583;fill:#000000" + x="6.9525447" + y="13.702217">$write(\{a\})$:</tspan></text> + <text + xml:space="preserve" + style="font-size:8.46667px;line-height:1.25;font-family:sans-serif;fill:#000000;stroke-width:0.264583" + x="23.457415" + y="24.042637" + id="text3750"><tspan + sodipodi:role="line" + id="tspan3748" + style="fill:#000000;stroke-width:0.264583" + x="23.457415" + y="24.042637">$\sqsupseteq \{a\} \to$ OK</tspan></text> + <text + xml:space="preserve" + style="font-size:8.46667px;line-height:1.25;font-family:sans-serif;fill:#000000;stroke-width:0.264583" + x="23.457415" + y="33.02087" + id="text3750-3"><tspan + sodipodi:role="line" + id="tspan3748-2" + style="fill:#000000;stroke-width:0.264583" + x="23.457415" + y="33.02087">$\sqsupseteq \{a\} \to$ OK</tspan></text> + <text + xml:space="preserve" + style="font-size:8.46667px;line-height:1.25;font-family:sans-serif;fill:#999999;stroke-width:0.264583" + x="23.457415" + y="41.972523" + id="text3750-0"><tspan + sodipodi:role="line" + id="tspan3748-6" + style="fill:#999999;stroke-width:0.264583" + x="23.457415" + y="41.972523">$\not\sqsupseteq \{a\}$</tspan></text> + <text + xml:space="preserve" + style="font-size:8.46667px;line-height:1.25;font-family:sans-serif;fill:#000000;stroke-width:0.264583" + x="14.395845" + y="52.022549" + id="text4280"><tspan + sodipodi:role="line" + id="tspan4278" + style="fill:#000000;stroke-width:0.264583" + x="14.395845" + y="52.022549">return OK</tspan></text> + <circle + style="fill:#ff0000;stroke:none;stroke-width:0.499999;stroke-dasharray:none;stop-color:#000000" + id="path3663-1-4" + cx="18.004833" + cy="90.979645" + r="2.7302806" /> + <circle + style="fill:#008000;stroke:none;stroke-width:0.499999;stroke-dasharray:none;stop-color:#000000" + id="path3663-3-0-5" + cx="18.004833" + cy="81.949104" + r="2.7302806" /> + <circle + style="fill:#800080;stroke:none;stroke-width:0.499999;stroke-dasharray:none;stop-color:#000000" + id="path3663-6-6-2" + cx="18.004833" + cy="72.918564" + r="2.7302806" /> + <text + xml:space="preserve" + style="font-size:8.46667px;line-height:1.25;font-family:sans-serif;fill:#000000;stroke-width:0.264583" + x="6.9525447" + y="65.279381" + id="text3707-5"><tspan + sodipodi:role="line" + id="tspan3705-4" + style="fill:#000000;stroke-width:0.264583" + x="6.9525447" + y="65.279381">$write(\{b\})$:</tspan></text> + <text + xml:space="preserve" + style="font-size:8.46667px;line-height:1.25;font-family:sans-serif;fill:#999999;stroke-width:0.264583" + x="23.457415" + y="75.619804" + id="text3750-7"><tspan + sodipodi:role="line" + id="tspan3748-4" + style="fill:#999999;stroke-width:0.264583" + x="23.457415" + y="75.619804">$\not\sqsupseteq \{b\}$</tspan></text> + <text + xml:space="preserve" + style="font-size:8.46667px;line-height:1.25;font-family:sans-serif;fill:#999999;stroke-width:0.264583" + x="23.457415" + y="84.598038" + id="text3750-3-4"><tspan + sodipodi:role="line" + id="tspan3748-2-3" + style="fill:#999999;stroke-width:0.264583" + x="23.457415" + y="84.598038">$\not\sqsupseteq \{b\}$</tspan></text> + <text + xml:space="preserve" + style="font-size:8.46667px;line-height:1.25;font-family:sans-serif;fill:#000000;stroke-width:0.264583" + x="23.457415" + y="93.54969" + id="text3750-0-0"><tspan + sodipodi:role="line" + id="tspan3748-6-7" + style="fill:#000000;stroke-width:0.264583" + x="23.457415" + y="93.54969">$\sqsupseteq \{b\} \to$ OK</tspan></text> + </g> +</svg> diff --git a/doc/talks/2023-01-18-tocatta/assets/latticeA.svg b/doc/talks/2023-01-18-tocatta/assets/latticeA.svg new file mode 100644 index 00000000..400ccff8 --- /dev/null +++ b/doc/talks/2023-01-18-tocatta/assets/latticeA.svg @@ -0,0 +1,587 @@ +<?xml version="1.0" encoding="UTF-8" standalone="no"?> +<!-- Created with Inkscape (http://www.inkscape.org/) --> + +<svg + width="1000" + height="400" + viewBox="0 0 264.58333 105.83333" + version="1.1" + id="svg5" + inkscape:version="1.2.2 (b0a8486541, 2022-12-01)" + sodipodi:docname="latticeA.svg" + 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="namedview7" + pagecolor="#ffffff" + bordercolor="#666666" + borderopacity="1.0" + inkscape:showpageshadow="2" + inkscape:pageopacity="0.0" + inkscape:pagecheckerboard="0" + inkscape:deskcolor="#d1d1d1" + inkscape:document-units="mm" + showgrid="false" + inkscape:zoom="1.4734708" + inkscape:cx="450.97602" + inkscape:cy="272.14655" + inkscape:window-width="1920" + inkscape:window-height="999" + inkscape:window-x="0" + inkscape:window-y="0" + inkscape:window-maximized="1" + inkscape:current-layer="layer2" /> + <defs + id="defs2"> + <marker + style="overflow:visible" + id="Arrow2" + refX="0" + refY="0" + orient="auto-start-reverse" + inkscape:stockid="Arrow2" + markerWidth="7.6999998" + markerHeight="5.5999999" + viewBox="0 0 7.7 5.6" + inkscape:isstock="true" + inkscape:collect="always" + preserveAspectRatio="xMidYMid"> + <path + transform="scale(0.7)" + d="M -2,-4 9,0 -2,4 c 2,-2.33 2,-5.66 0,-8 z" + style="fill:context-stroke;fill-rule:evenodd;stroke:none" + id="arrow2L" /> + </marker> + <marker + style="overflow:visible" + id="Arrow2-9" + refX="0" + refY="0" + orient="auto-start-reverse" + inkscape:stockid="Arrow2" + markerWidth="7.6999998" + markerHeight="5.5999999" + viewBox="0 0 7.7 5.6" + inkscape:isstock="true" + inkscape:collect="always" + preserveAspectRatio="xMidYMid"> + <path + transform="scale(0.7)" + d="M -2,-4 9,0 -2,4 c 2,-2.33 2,-5.66 0,-8 z" + style="fill:context-stroke;fill-rule:evenodd;stroke:none" + id="arrow2L-1" /> + </marker> + <marker + style="overflow:visible" + id="Arrow2-9-7" + refX="0" + refY="0" + orient="auto-start-reverse" + inkscape:stockid="Arrow2" + markerWidth="7.6999998" + markerHeight="5.5999999" + viewBox="0 0 7.7 5.6" + inkscape:isstock="true" + inkscape:collect="always" + preserveAspectRatio="xMidYMid"> + <path + transform="scale(0.7)" + d="M -2,-4 9,0 -2,4 c 2,-2.33 2,-5.66 0,-8 z" + style="fill:context-stroke;fill-rule:evenodd;stroke:none" + id="arrow2L-1-0" /> + </marker> + <marker + style="overflow:visible" + id="Arrow2-93" + refX="0" + refY="0" + orient="auto-start-reverse" + inkscape:stockid="Arrow2" + markerWidth="7.6999998" + markerHeight="5.5999999" + viewBox="0 0 7.7 5.6" + inkscape:isstock="true" + inkscape:collect="always" + preserveAspectRatio="xMidYMid"> + <path + transform="scale(0.7)" + d="M -2,-4 9,0 -2,4 c 2,-2.33 2,-5.66 0,-8 z" + style="fill:context-stroke;fill-rule:evenodd;stroke:none" + id="arrow2L-6" /> + </marker> + <marker + style="overflow:visible" + id="Arrow2-9-7-2" + refX="0" + refY="0" + orient="auto-start-reverse" + inkscape:stockid="Arrow2" + markerWidth="7.6999998" + markerHeight="5.5999999" + viewBox="0 0 7.7 5.6" + inkscape:isstock="true" + inkscape:collect="always" + preserveAspectRatio="xMidYMid"> + <path + transform="scale(0.7)" + d="M -2,-4 9,0 -2,4 c 2,-2.33 2,-5.66 0,-8 z" + style="fill:context-stroke;fill-rule:evenodd;stroke:none" + id="arrow2L-1-0-6" /> + </marker> + <marker + style="overflow:visible" + id="Arrow2-93-1" + refX="0" + refY="0" + orient="auto-start-reverse" + inkscape:stockid="Arrow2" + markerWidth="7.6999998" + markerHeight="5.5999999" + viewBox="0 0 7.7 5.6" + inkscape:isstock="true" + inkscape:collect="always" + preserveAspectRatio="xMidYMid"> + <path + transform="scale(0.7)" + d="M -2,-4 9,0 -2,4 c 2,-2.33 2,-5.66 0,-8 z" + style="fill:context-stroke;fill-rule:evenodd;stroke:none" + id="arrow2L-6-8" /> + </marker> + <marker + style="overflow:visible" + id="Arrow2-9-75" + refX="0" + refY="0" + orient="auto-start-reverse" + inkscape:stockid="Arrow2" + markerWidth="7.6999998" + markerHeight="5.5999999" + viewBox="0 0 7.7 5.6" + inkscape:isstock="true" + inkscape:collect="always" + preserveAspectRatio="xMidYMid"> + <path + transform="scale(0.7)" + d="M -2,-4 9,0 -2,4 c 2,-2.33 2,-5.66 0,-8 z" + style="fill:context-stroke;fill-rule:evenodd;stroke:none" + id="arrow2L-1-9" /> + </marker> + <marker + style="overflow:visible" + id="Arrow2-9-75-2" + refX="0" + refY="0" + orient="auto-start-reverse" + inkscape:stockid="Arrow2" + markerWidth="7.6999998" + markerHeight="5.5999999" + viewBox="0 0 7.7 5.6" + inkscape:isstock="true" + inkscape:collect="always" + preserveAspectRatio="xMidYMid"> + <path + transform="scale(0.7)" + d="M -2,-4 9,0 -2,4 c 2,-2.33 2,-5.66 0,-8 z" + style="fill:context-stroke;fill-rule:evenodd;stroke:none" + id="arrow2L-1-9-8" /> + </marker> + <marker + style="overflow:visible" + id="Arrow2-9-75-7" + refX="0" + refY="0" + orient="auto-start-reverse" + inkscape:stockid="Arrow2" + markerWidth="7.6999998" + markerHeight="5.5999999" + viewBox="0 0 7.7 5.6" + inkscape:isstock="true" + inkscape:collect="always" + preserveAspectRatio="xMidYMid"> + <path + transform="scale(0.7)" + d="M -2,-4 9,0 -2,4 c 2,-2.33 2,-5.66 0,-8 z" + style="fill:context-stroke;fill-rule:evenodd;stroke:none" + id="arrow2L-1-9-3" /> + </marker> + <marker + style="overflow:visible" + id="Arrow2-9-75-7-1" + refX="0" + refY="0" + orient="auto-start-reverse" + inkscape:stockid="Arrow2" + markerWidth="7.6999998" + markerHeight="5.5999999" + viewBox="0 0 7.7 5.6" + inkscape:isstock="true" + inkscape:collect="always" + preserveAspectRatio="xMidYMid"> + <path + transform="scale(0.7)" + d="M -2,-4 9,0 -2,4 c 2,-2.33 2,-5.66 0,-8 z" + style="fill:context-stroke;fill-rule:evenodd;stroke:none" + id="arrow2L-1-9-3-2" /> + </marker> + <marker + style="overflow:visible" + id="Arrow2-93-1-4" + refX="0" + refY="0" + orient="auto-start-reverse" + inkscape:stockid="Arrow2" + markerWidth="7.6999998" + markerHeight="5.5999999" + viewBox="0 0 7.7 5.6" + inkscape:isstock="true" + inkscape:collect="always" + preserveAspectRatio="xMidYMid"> + <path + transform="scale(0.7)" + d="M -2,-4 9,0 -2,4 c 2,-2.33 2,-5.66 0,-8 z" + style="fill:context-stroke;fill-rule:evenodd;stroke:none" + id="arrow2L-6-8-7" /> + </marker> + <marker + style="overflow:visible" + id="Arrow2-9-7-2-8" + refX="0" + refY="0" + orient="auto-start-reverse" + inkscape:stockid="Arrow2" + markerWidth="7.6999998" + markerHeight="5.5999999" + viewBox="0 0 7.7 5.6" + inkscape:isstock="true" + inkscape:collect="always" + preserveAspectRatio="xMidYMid"> + <path + transform="scale(0.7)" + d="M -2,-4 9,0 -2,4 c 2,-2.33 2,-5.66 0,-8 z" + style="fill:context-stroke;fill-rule:evenodd;stroke:none" + id="arrow2L-1-0-6-4" /> + </marker> + </defs> + <g + inkscape:label="Layer 1" + inkscape:groupmode="layer" + id="layer1" + sodipodi:insensitive="true"> + <rect + style="fill:#ffffff;stroke:none;stroke-width:1;stop-color:#000000" + id="rect288" + width="209.84705" + height="104.42732" + x="0.77790999" + y="0.93738818" /> + </g> + <g + inkscape:groupmode="layer" + id="layer2" + inkscape:label="Layer 2"> + <text + xml:space="preserve" + style="font-size:8.46667px;line-height:1.25;font-family:sans-serif;text-align:center;text-anchor:middle;stroke-width:0.264583;fill:#000000" + x="164.56372" + y="99.307442" + id="text951"><tspan + sodipodi:role="line" + id="tspan949" + style="stroke-width:0.264583;fill:#000000" + x="164.56372" + y="99.307442">$\{\}$</tspan></text> + <text + xml:space="preserve" + style="font-size:8.46667px;line-height:1.25;font-family:sans-serif;text-align:center;text-anchor:middle;stroke-width:0.264583;fill:#000000" + x="164.56372" + y="13.151893" + id="text1005"><tspan + sodipodi:role="line" + id="tspan1003" + style="stroke-width:0.264583;fill:#000000" + x="164.56372" + y="13.151893">$\{a,b,c\}$</tspan></text> + <g + id="g1175" + transform="translate(51.996784,3.5774043)"> + <text + xml:space="preserve" + style="font-size:8.46667px;line-height:1.25;font-family:sans-serif;text-align:center;text-anchor:middle;stroke-width:0.264583;fill:#000000" + x="49.27084" + y="67.008698" + id="text1009"><tspan + sodipodi:role="line" + id="tspan1007" + style="stroke-width:0.264583;fill:#000000" + x="49.27084" + y="67.008698">$\{a\}$</tspan></text> + <text + xml:space="preserve" + style="font-size:8.46667px;line-height:1.25;font-family:sans-serif;text-align:center;text-anchor:middle;stroke-width:0.264583;fill:#000000" + x="112.90984" + y="67.017166" + id="text1009-3"><tspan + sodipodi:role="line" + id="tspan1007-6" + style="stroke-width:0.264583;fill:#000000" + x="112.90984" + y="67.017166">$\{b\}$</tspan></text> + <text + xml:space="preserve" + style="font-size:8.46667px;line-height:1.25;font-family:sans-serif;text-align:center;text-anchor:middle;stroke-width:0.264583;fill:#000000" + x="176.20593" + y="67.008698" + id="text1009-7"><tspan + sodipodi:role="line" + id="tspan1007-5" + style="stroke-width:0.264583;fill:#000000" + x="176.20593" + y="67.008698">$\{c\}$</tspan></text> + </g> + <g + id="g1183" + transform="translate(51.996784,1.0317046)" + style="fill:#000000"> + <text + xml:space="preserve" + style="font-size:8.46667px;line-height:1.25;font-family:sans-serif;text-align:center;text-anchor:middle;stroke-width:0.264583;fill:#000000" + x="112.90984" + y="40.841526" + id="text1117"><tspan + sodipodi:role="line" + id="tspan1115" + style="stroke-width:0.264583;fill:#000000" + x="112.90984" + y="40.841526">$\{a,c\}$</tspan></text> + <text + xml:space="preserve" + style="font-size:8.46667px;line-height:1.25;font-family:sans-serif;text-align:center;text-anchor:middle;stroke-width:0.264583;fill:#000000" + x="49.27084" + y="40.841526" + id="text1117-3"><tspan + sodipodi:role="line" + id="tspan1115-5" + style="stroke-width:0.264583;fill:#000000" + x="49.27084" + y="40.841526">$\{a,b\}$</tspan></text> + <text + xml:space="preserve" + style="font-size:8.46667px;line-height:1.25;font-family:sans-serif;text-align:center;text-anchor:middle;stroke-width:0.264583;fill:#000000" + x="176.20593" + y="40.841526" + id="text1117-6"><tspan + sodipodi:role="line" + id="tspan1115-2" + style="stroke-width:0.264583;fill:#000000" + x="176.20593" + y="40.841526">$\{b,c\}$</tspan></text> + </g> + <path + style="fill:none;stroke:#000000;stroke-width:0.5;stroke-linecap:butt;stroke-linejoin:miter;stroke-dasharray:none;stroke-opacity:1;marker-end:url(#Arrow2)" + d="M 153.33622,90.367682 118.34198,73.428915" + id="path1300" /> + <path + style="fill:none;stroke:#000000;stroke-width:0.5;stroke-linecap:butt;stroke-linejoin:miter;stroke-dasharray:none;stroke-opacity:1;marker-end:url(#Arrow2-9)" + d="M 177.46016,90.367682 212.4544,73.428915" + id="path1300-2" /> + <path + style="fill:none;stroke:#000000;stroke-width:0.5;stroke-linecap:butt;stroke-linejoin:miter;stroke-dasharray:none;stroke-opacity:1;marker-end:url(#Arrow2-93)" + d="M 153.33622,61.655656 118.34198,44.716889" + id="path1300-0" /> + <path + style="fill:none;stroke:#000000;stroke-width:0.5;stroke-linecap:butt;stroke-linejoin:miter;stroke-dasharray:none;stroke-opacity:1;marker-end:url(#Arrow2-9-7)" + d="M 177.46016,61.655656 212.4544,44.716889" + id="path1300-2-6" /> + <path + style="fill:none;stroke:#000000;stroke-width:0.5;stroke-linecap:butt;stroke-linejoin:miter;stroke-dasharray:none;stroke-opacity:1;marker-end:url(#Arrow2-93-1)" + d="M 118.34198,61.655656 153.33622,44.716889" + id="path1300-0-7" /> + <path + style="fill:none;stroke:#000000;stroke-width:0.5;stroke-linecap:butt;stroke-linejoin:miter;stroke-dasharray:none;stroke-opacity:1;marker-end:url(#Arrow2-9-7-2)" + d="M 212.4544,61.655656 177.46016,44.716889" + id="path1300-2-6-9" /> + <path + style="fill:none;stroke:#000000;stroke-width:0.5;stroke-linecap:butt;stroke-linejoin:miter;stroke-dasharray:none;stroke-opacity:1;marker-end:url(#Arrow2-93-1-4)" + d="M 118.34198,34.227412 153.33622,17.288645" + id="path1300-0-7-5" /> + <path + style="fill:none;stroke:#000000;stroke-width:0.5;stroke-linecap:butt;stroke-linejoin:miter;stroke-dasharray:none;stroke-opacity:1;marker-end:url(#Arrow2-9-7-2-8)" + d="M 212.4544,34.227412 177.46016,17.288645" + id="path1300-2-6-9-0" /> + <path + style="fill:none;stroke:#000000;stroke-width:0.5;stroke-linecap:butt;stroke-linejoin:miter;stroke-dasharray:none;stroke-opacity:1;marker-end:url(#Arrow2-9-75)" + d="m 228.52843,61.091809 0.33313,-12.554874 m -0.33313,12.554874 0.33313,-12.554874" + id="path1300-2-2" + sodipodi:nodetypes="cc" /> + <path + style="fill:none;stroke:#000000;stroke-width:0.5;stroke-linecap:butt;stroke-linejoin:miter;stroke-dasharray:none;stroke-opacity:1;marker-end:url(#Arrow2-9-75-2)" + d="m 101.90418,61.091809 0.33313,-12.554874 m -0.33313,12.554874 0.33313,-12.554874" + id="path1300-2-2-9" + sodipodi:nodetypes="cc" /> + <path + style="fill:none;stroke:#000000;stroke-width:0.5;stroke-linecap:butt;stroke-linejoin:miter;stroke-dasharray:none;stroke-opacity:1;marker-end:url(#Arrow2-9-75-7)" + d="m 165.29305,89.571762 0.33313,-12.554874 m -0.33313,12.554874 0.33313,-12.554874" + id="path1300-2-2-6" + sodipodi:nodetypes="cc" /> + <path + style="fill:none;stroke:#000000;stroke-width:0.5;stroke-linecap:butt;stroke-linejoin:miter;stroke-dasharray:none;stroke-opacity:1;marker-end:url(#Arrow2-9-75-7-1)" + d="m 165.29305,32.445235 0.33313,-12.554874 m -0.33313,12.554874 0.33313,-12.554874" + id="path1300-2-2-6-9" + sodipodi:nodetypes="cc" /> + <circle + style="fill:#ff0000;stroke:none;stroke-width:0.499999;stroke-dasharray:none;stop-color:#000000" + id="path3663" + cx="117.08417" + cy="38.792969" + r="2.7302806" /> + <circle + style="fill:#008000;stroke:none;stroke-width:0.499999;stroke-dasharray:none;stop-color:#000000" + id="path3663-3" + cx="126.08154" + cy="67.968384" + r="2.7302806" /> + <circle + style="fill:#800080;stroke:none;stroke-width:0.499999;stroke-dasharray:none;stop-color:#000000" + id="path3663-6" + cx="119.58919" + cy="67.645035" + r="2.7302806" /> + <circle + style="fill:#ff0000;stroke:none;stroke-width:0.499999;stroke-dasharray:none;stop-color:#000000" + id="path3663-1" + cx="18.004833" + cy="39.402473" + r="2.7302806" /> + <circle + style="fill:#008000;stroke:none;stroke-width:0.499999;stroke-dasharray:none;stop-color:#000000" + id="path3663-3-0" + cx="18.004833" + cy="30.371933" + r="2.7302806" /> + <circle + style="fill:#800080;stroke:none;stroke-width:0.499999;stroke-dasharray:none;stop-color:#000000" + id="path3663-6-6" + cx="18.004833" + cy="21.341394" + r="2.7302806" /> + <text + xml:space="preserve" + style="font-size:8.46667px;line-height:1.25;font-family:sans-serif;stroke-width:0.264583;fill:#000000" + x="6.9525447" + y="13.702217" + id="text3707"><tspan + sodipodi:role="line" + id="tspan3705" + style="stroke-width:0.264583;fill:#000000" + x="6.9525447" + y="13.702217">$write(\{a\})$:</tspan></text> + <text + xml:space="preserve" + style="font-size:8.46667px;line-height:1.25;font-family:sans-serif;fill:#000000;stroke-width:0.264583" + x="23.457415" + y="24.042637" + id="text3750"><tspan + sodipodi:role="line" + id="tspan3748" + style="fill:#000000;stroke-width:0.264583" + x="23.457415" + y="24.042637">$\sqsupseteq \{a\} \to$ OK</tspan></text> + <text + xml:space="preserve" + style="font-size:8.46667px;line-height:1.25;font-family:sans-serif;fill:#000000;stroke-width:0.264583" + x="23.457415" + y="33.02087" + id="text3750-3"><tspan + sodipodi:role="line" + id="tspan3748-2" + style="fill:#000000;stroke-width:0.264583" + x="23.457415" + y="33.02087">$\sqsupseteq \{a\} \to$ OK</tspan></text> + <text + xml:space="preserve" + style="font-size:8.46667px;line-height:1.25;font-family:sans-serif;fill:#000000;stroke-width:0.264583" + x="23.457415" + y="41.972523" + id="text3750-0"><tspan + sodipodi:role="line" + id="tspan3748-6" + style="fill:#000000;stroke-width:0.264583" + x="23.457415" + y="41.972523">$\sqsupseteq \{a\}$</tspan></text> + <text + xml:space="preserve" + style="font-size:8.46667px;line-height:1.25;font-family:sans-serif;fill:#000000;stroke-width:0.264583" + x="14.395845" + y="52.022549" + id="text4280"><tspan + sodipodi:role="line" + id="tspan4278" + style="fill:#000000;stroke-width:0.264583" + x="14.395845" + y="52.022549">return OK</tspan></text> + <circle + style="fill:#ff0000;stroke:none;stroke-width:0.499999;stroke-dasharray:none;stop-color:#000000" + id="path3663-1-4" + cx="18.004833" + cy="90.979645" + r="2.7302806" /> + <circle + style="fill:#008000;stroke:none;stroke-width:0.499999;stroke-dasharray:none;stop-color:#000000" + id="path3663-3-0-5" + cx="18.004833" + cy="81.949104" + r="2.7302806" /> + <circle + style="fill:#800080;stroke:none;stroke-width:0.499999;stroke-dasharray:none;stop-color:#000000" + id="path3663-6-6-2" + cx="18.004833" + cy="72.918564" + r="2.7302806" /> + <text + xml:space="preserve" + style="font-size:8.46667px;line-height:1.25;font-family:sans-serif;fill:#000000;stroke-width:0.264583" + x="6.9525447" + y="65.279381" + id="text3707-5"><tspan + sodipodi:role="line" + id="tspan3705-4" + style="fill:#000000;stroke-width:0.264583" + x="6.9525447" + y="65.279381">$write(\{b\})$:</tspan></text> + <text + xml:space="preserve" + style="font-size:8.46667px;line-height:1.25;font-family:sans-serif;fill:#999999;stroke-width:0.264583" + x="23.457415" + y="75.619804" + id="text3750-7"><tspan + sodipodi:role="line" + id="tspan3748-4" + style="fill:#999999;stroke-width:0.264583" + x="23.457415" + y="75.619804">$\not\sqsupseteq \{b\}$</tspan></text> + <text + xml:space="preserve" + style="font-size:8.46667px;line-height:1.25;font-family:sans-serif;fill:#999999;stroke-width:0.264583" + x="23.457415" + y="84.598038" + id="text3750-3-4"><tspan + sodipodi:role="line" + id="tspan3748-2-3" + style="fill:#999999;stroke-width:0.264583" + x="23.457415" + y="84.598038">$\not\sqsupseteq \{b\}$</tspan></text> + <text + xml:space="preserve" + style="font-size:8.46667px;line-height:1.25;font-family:sans-serif;fill:#000000;stroke-width:0.264583" + x="23.457415" + y="93.54969" + id="text3750-0-0"><tspan + sodipodi:role="line" + id="tspan3748-6-7" + style="fill:#000000;stroke-width:0.264583" + x="23.457415" + y="93.54969">$\sqsupseteq \{b\} \to$ OK</tspan></text> + </g> +</svg> diff --git a/doc/talks/2023-01-18-tocatta/assets/latticeB.svg b/doc/talks/2023-01-18-tocatta/assets/latticeB.svg new file mode 100644 index 00000000..06725d75 --- /dev/null +++ b/doc/talks/2023-01-18-tocatta/assets/latticeB.svg @@ -0,0 +1,598 @@ +<?xml version="1.0" encoding="UTF-8" standalone="no"?> +<!-- Created with Inkscape (http://www.inkscape.org/) --> + +<svg + width="1000" + height="400" + viewBox="0 0 264.58333 105.83333" + version="1.1" + id="svg5" + inkscape:version="1.2.2 (b0a8486541, 2022-12-01)" + sodipodi:docname="latticeB.svg" + 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="namedview7" + pagecolor="#ffffff" + bordercolor="#666666" + borderopacity="1.0" + inkscape:showpageshadow="2" + inkscape:pageopacity="0.0" + inkscape:pagecheckerboard="0" + inkscape:deskcolor="#d1d1d1" + inkscape:document-units="mm" + showgrid="false" + inkscape:zoom="1.4734708" + inkscape:cx="450.97602" + inkscape:cy="272.14655" + inkscape:window-width="1920" + inkscape:window-height="999" + inkscape:window-x="0" + inkscape:window-y="0" + inkscape:window-maximized="1" + inkscape:current-layer="layer2" /> + <defs + id="defs2"> + <marker + style="overflow:visible" + id="Arrow2" + refX="0" + refY="0" + orient="auto-start-reverse" + inkscape:stockid="Arrow2" + markerWidth="7.6999998" + markerHeight="5.5999999" + viewBox="0 0 7.7 5.6" + inkscape:isstock="true" + inkscape:collect="always" + preserveAspectRatio="xMidYMid"> + <path + transform="scale(0.7)" + d="M -2,-4 9,0 -2,4 c 2,-2.33 2,-5.66 0,-8 z" + style="fill:context-stroke;fill-rule:evenodd;stroke:none" + id="arrow2L" /> + </marker> + <marker + style="overflow:visible" + id="Arrow2-9" + refX="0" + refY="0" + orient="auto-start-reverse" + inkscape:stockid="Arrow2" + markerWidth="7.6999998" + markerHeight="5.5999999" + viewBox="0 0 7.7 5.6" + inkscape:isstock="true" + inkscape:collect="always" + preserveAspectRatio="xMidYMid"> + <path + transform="scale(0.7)" + d="M -2,-4 9,0 -2,4 c 2,-2.33 2,-5.66 0,-8 z" + style="fill:context-stroke;fill-rule:evenodd;stroke:none" + id="arrow2L-1" /> + </marker> + <marker + style="overflow:visible" + id="Arrow2-9-7" + refX="0" + refY="0" + orient="auto-start-reverse" + inkscape:stockid="Arrow2" + markerWidth="7.6999998" + markerHeight="5.5999999" + viewBox="0 0 7.7 5.6" + inkscape:isstock="true" + inkscape:collect="always" + preserveAspectRatio="xMidYMid"> + <path + transform="scale(0.7)" + d="M -2,-4 9,0 -2,4 c 2,-2.33 2,-5.66 0,-8 z" + style="fill:context-stroke;fill-rule:evenodd;stroke:none" + id="arrow2L-1-0" /> + </marker> + <marker + style="overflow:visible" + id="Arrow2-93" + refX="0" + refY="0" + orient="auto-start-reverse" + inkscape:stockid="Arrow2" + markerWidth="7.6999998" + markerHeight="5.5999999" + viewBox="0 0 7.7 5.6" + inkscape:isstock="true" + inkscape:collect="always" + preserveAspectRatio="xMidYMid"> + <path + transform="scale(0.7)" + d="M -2,-4 9,0 -2,4 c 2,-2.33 2,-5.66 0,-8 z" + style="fill:context-stroke;fill-rule:evenodd;stroke:none" + id="arrow2L-6" /> + </marker> + <marker + style="overflow:visible" + id="Arrow2-9-7-2" + refX="0" + refY="0" + orient="auto-start-reverse" + inkscape:stockid="Arrow2" + markerWidth="7.6999998" + markerHeight="5.5999999" + viewBox="0 0 7.7 5.6" + inkscape:isstock="true" + inkscape:collect="always" + preserveAspectRatio="xMidYMid"> + <path + transform="scale(0.7)" + d="M -2,-4 9,0 -2,4 c 2,-2.33 2,-5.66 0,-8 z" + style="fill:context-stroke;fill-rule:evenodd;stroke:none" + id="arrow2L-1-0-6" /> + </marker> + <marker + style="overflow:visible" + id="Arrow2-93-1" + refX="0" + refY="0" + orient="auto-start-reverse" + inkscape:stockid="Arrow2" + markerWidth="7.6999998" + markerHeight="5.5999999" + viewBox="0 0 7.7 5.6" + inkscape:isstock="true" + inkscape:collect="always" + preserveAspectRatio="xMidYMid"> + <path + transform="scale(0.7)" + d="M -2,-4 9,0 -2,4 c 2,-2.33 2,-5.66 0,-8 z" + style="fill:context-stroke;fill-rule:evenodd;stroke:none" + id="arrow2L-6-8" /> + </marker> + <marker + style="overflow:visible" + id="Arrow2-9-75" + refX="0" + refY="0" + orient="auto-start-reverse" + inkscape:stockid="Arrow2" + markerWidth="7.6999998" + markerHeight="5.5999999" + viewBox="0 0 7.7 5.6" + inkscape:isstock="true" + inkscape:collect="always" + preserveAspectRatio="xMidYMid"> + <path + transform="scale(0.7)" + d="M -2,-4 9,0 -2,4 c 2,-2.33 2,-5.66 0,-8 z" + style="fill:context-stroke;fill-rule:evenodd;stroke:none" + id="arrow2L-1-9" /> + </marker> + <marker + style="overflow:visible" + id="Arrow2-9-75-2" + refX="0" + refY="0" + orient="auto-start-reverse" + inkscape:stockid="Arrow2" + markerWidth="7.6999998" + markerHeight="5.5999999" + viewBox="0 0 7.7 5.6" + inkscape:isstock="true" + inkscape:collect="always" + preserveAspectRatio="xMidYMid"> + <path + transform="scale(0.7)" + d="M -2,-4 9,0 -2,4 c 2,-2.33 2,-5.66 0,-8 z" + style="fill:context-stroke;fill-rule:evenodd;stroke:none" + id="arrow2L-1-9-8" /> + </marker> + <marker + style="overflow:visible" + id="Arrow2-9-75-7" + refX="0" + refY="0" + orient="auto-start-reverse" + inkscape:stockid="Arrow2" + markerWidth="7.6999998" + markerHeight="5.5999999" + viewBox="0 0 7.7 5.6" + inkscape:isstock="true" + inkscape:collect="always" + preserveAspectRatio="xMidYMid"> + <path + transform="scale(0.7)" + d="M -2,-4 9,0 -2,4 c 2,-2.33 2,-5.66 0,-8 z" + style="fill:context-stroke;fill-rule:evenodd;stroke:none" + id="arrow2L-1-9-3" /> + </marker> + <marker + style="overflow:visible" + id="Arrow2-9-75-7-1" + refX="0" + refY="0" + orient="auto-start-reverse" + inkscape:stockid="Arrow2" + markerWidth="7.6999998" + markerHeight="5.5999999" + viewBox="0 0 7.7 5.6" + inkscape:isstock="true" + inkscape:collect="always" + preserveAspectRatio="xMidYMid"> + <path + transform="scale(0.7)" + d="M -2,-4 9,0 -2,4 c 2,-2.33 2,-5.66 0,-8 z" + style="fill:context-stroke;fill-rule:evenodd;stroke:none" + id="arrow2L-1-9-3-2" /> + </marker> + <marker + style="overflow:visible" + id="Arrow2-93-1-4" + refX="0" + refY="0" + orient="auto-start-reverse" + inkscape:stockid="Arrow2" + markerWidth="7.6999998" + markerHeight="5.5999999" + viewBox="0 0 7.7 5.6" + inkscape:isstock="true" + inkscape:collect="always" + preserveAspectRatio="xMidYMid"> + <path + transform="scale(0.7)" + d="M -2,-4 9,0 -2,4 c 2,-2.33 2,-5.66 0,-8 z" + style="fill:context-stroke;fill-rule:evenodd;stroke:none" + id="arrow2L-6-8-7" /> + </marker> + <marker + style="overflow:visible" + id="Arrow2-9-7-2-8" + refX="0" + refY="0" + orient="auto-start-reverse" + inkscape:stockid="Arrow2" + markerWidth="7.6999998" + markerHeight="5.5999999" + viewBox="0 0 7.7 5.6" + inkscape:isstock="true" + inkscape:collect="always" + preserveAspectRatio="xMidYMid"> + <path + transform="scale(0.7)" + d="M -2,-4 9,0 -2,4 c 2,-2.33 2,-5.66 0,-8 z" + style="fill:context-stroke;fill-rule:evenodd;stroke:none" + id="arrow2L-1-0-6-4" /> + </marker> + </defs> + <g + inkscape:label="Layer 1" + inkscape:groupmode="layer" + id="layer1" + sodipodi:insensitive="true"> + <rect + style="fill:#ffffff;stroke:none;stroke-width:1;stop-color:#000000" + id="rect288" + width="209.84705" + height="104.42732" + x="0.77790999" + y="0.93738818" /> + </g> + <g + inkscape:groupmode="layer" + id="layer2" + inkscape:label="Layer 2"> + <text + xml:space="preserve" + style="font-size:8.46667px;line-height:1.25;font-family:sans-serif;text-align:center;text-anchor:middle;stroke-width:0.264583;fill:#000000" + x="164.56372" + y="99.307442" + id="text951"><tspan + sodipodi:role="line" + id="tspan949" + style="stroke-width:0.264583;fill:#000000" + x="164.56372" + y="99.307442">$\{\}$</tspan></text> + <text + xml:space="preserve" + style="font-size:8.46667px;line-height:1.25;font-family:sans-serif;text-align:center;text-anchor:middle;stroke-width:0.264583;fill:#000000" + x="164.56372" + y="13.151893" + id="text1005"><tspan + sodipodi:role="line" + id="tspan1003" + style="stroke-width:0.264583;fill:#000000" + x="164.56372" + y="13.151893">$\{a,b,c\}$</tspan></text> + <g + id="g1175" + transform="translate(51.996784,3.5774043)"> + <text + xml:space="preserve" + style="font-size:8.46667px;line-height:1.25;font-family:sans-serif;text-align:center;text-anchor:middle;stroke-width:0.264583;fill:#000000" + x="49.27084" + y="67.008698" + id="text1009"><tspan + sodipodi:role="line" + id="tspan1007" + style="stroke-width:0.264583;fill:#000000" + x="49.27084" + y="67.008698">$\{a\}$</tspan></text> + <text + xml:space="preserve" + style="font-size:8.46667px;line-height:1.25;font-family:sans-serif;text-align:center;text-anchor:middle;stroke-width:0.264583;fill:#000000" + x="112.90984" + y="67.017166" + id="text1009-3"><tspan + sodipodi:role="line" + id="tspan1007-6" + style="stroke-width:0.264583;fill:#000000" + x="112.90984" + y="67.017166">$\{b\}$</tspan></text> + <text + xml:space="preserve" + style="font-size:8.46667px;line-height:1.25;font-family:sans-serif;text-align:center;text-anchor:middle;stroke-width:0.264583;fill:#000000" + x="176.20593" + y="67.008698" + id="text1009-7"><tspan + sodipodi:role="line" + id="tspan1007-5" + style="stroke-width:0.264583;fill:#000000" + x="176.20593" + y="67.008698">$\{c\}$</tspan></text> + </g> + <g + id="g1183" + transform="translate(51.996784,1.0317046)" + style="fill:#000000"> + <text + xml:space="preserve" + style="font-size:8.46667px;line-height:1.25;font-family:sans-serif;text-align:center;text-anchor:middle;stroke-width:0.264583;fill:#000000" + x="112.90984" + y="40.841526" + id="text1117"><tspan + sodipodi:role="line" + id="tspan1115" + style="stroke-width:0.264583;fill:#000000" + x="112.90984" + y="40.841526">$\{a,c\}$</tspan></text> + <text + xml:space="preserve" + style="font-size:8.46667px;line-height:1.25;font-family:sans-serif;text-align:center;text-anchor:middle;stroke-width:0.264583;fill:#000000" + x="49.27084" + y="40.841526" + id="text1117-3"><tspan + sodipodi:role="line" + id="tspan1115-5" + style="stroke-width:0.264583;fill:#000000" + x="49.27084" + y="40.841526">$\{a,b\}$</tspan></text> + <text + xml:space="preserve" + style="font-size:8.46667px;line-height:1.25;font-family:sans-serif;text-align:center;text-anchor:middle;stroke-width:0.264583;fill:#000000" + x="176.20593" + y="40.841526" + id="text1117-6"><tspan + sodipodi:role="line" + id="tspan1115-2" + style="stroke-width:0.264583;fill:#000000" + x="176.20593" + y="40.841526">$\{b,c\}$</tspan></text> + </g> + <path + style="fill:none;stroke:#000000;stroke-width:0.5;stroke-linecap:butt;stroke-linejoin:miter;stroke-dasharray:none;stroke-opacity:1;marker-end:url(#Arrow2)" + d="M 153.33622,90.367682 118.34198,73.428915" + id="path1300" /> + <path + style="fill:none;stroke:#000000;stroke-width:0.5;stroke-linecap:butt;stroke-linejoin:miter;stroke-dasharray:none;stroke-opacity:1;marker-end:url(#Arrow2-9)" + d="M 177.46016,90.367682 212.4544,73.428915" + id="path1300-2" /> + <path + style="fill:none;stroke:#000000;stroke-width:0.5;stroke-linecap:butt;stroke-linejoin:miter;stroke-dasharray:none;stroke-opacity:1;marker-end:url(#Arrow2-93)" + d="M 153.33622,61.655656 118.34198,44.716889" + id="path1300-0" /> + <path + style="fill:none;stroke:#000000;stroke-width:0.5;stroke-linecap:butt;stroke-linejoin:miter;stroke-dasharray:none;stroke-opacity:1;marker-end:url(#Arrow2-9-7)" + d="M 177.46016,61.655656 212.4544,44.716889" + id="path1300-2-6" /> + <path + style="fill:none;stroke:#000000;stroke-width:0.5;stroke-linecap:butt;stroke-linejoin:miter;stroke-dasharray:none;stroke-opacity:1;marker-end:url(#Arrow2-93-1)" + d="M 118.34198,61.655656 153.33622,44.716889" + id="path1300-0-7" /> + <path + style="fill:none;stroke:#000000;stroke-width:0.5;stroke-linecap:butt;stroke-linejoin:miter;stroke-dasharray:none;stroke-opacity:1;marker-end:url(#Arrow2-9-7-2)" + d="M 212.4544,61.655656 177.46016,44.716889" + id="path1300-2-6-9" /> + <path + style="fill:none;stroke:#000000;stroke-width:0.5;stroke-linecap:butt;stroke-linejoin:miter;stroke-dasharray:none;stroke-opacity:1;marker-end:url(#Arrow2-93-1-4)" + d="M 118.34198,34.227412 153.33622,17.288645" + id="path1300-0-7-5" /> + <path + style="fill:none;stroke:#000000;stroke-width:0.5;stroke-linecap:butt;stroke-linejoin:miter;stroke-dasharray:none;stroke-opacity:1;marker-end:url(#Arrow2-9-7-2-8)" + d="M 212.4544,34.227412 177.46016,17.288645" + id="path1300-2-6-9-0" /> + <path + style="fill:none;stroke:#000000;stroke-width:0.5;stroke-linecap:butt;stroke-linejoin:miter;stroke-dasharray:none;stroke-opacity:1;marker-end:url(#Arrow2-9-75)" + d="m 228.52843,61.091809 0.33313,-12.554874 m -0.33313,12.554874 0.33313,-12.554874" + id="path1300-2-2" + sodipodi:nodetypes="cc" /> + <path + style="fill:none;stroke:#000000;stroke-width:0.5;stroke-linecap:butt;stroke-linejoin:miter;stroke-dasharray:none;stroke-opacity:1;marker-end:url(#Arrow2-9-75-2)" + d="m 101.90418,61.091809 0.33313,-12.554874 m -0.33313,12.554874 0.33313,-12.554874" + id="path1300-2-2-9" + sodipodi:nodetypes="cc" /> + <path + style="fill:none;stroke:#000000;stroke-width:0.5;stroke-linecap:butt;stroke-linejoin:miter;stroke-dasharray:none;stroke-opacity:1;marker-end:url(#Arrow2-9-75-7)" + d="m 165.29305,89.571762 0.33313,-12.554874 m -0.33313,12.554874 0.33313,-12.554874" + id="path1300-2-2-6" + sodipodi:nodetypes="cc" /> + <path + style="fill:none;stroke:#000000;stroke-width:0.5;stroke-linecap:butt;stroke-linejoin:miter;stroke-dasharray:none;stroke-opacity:1;marker-end:url(#Arrow2-9-75-7-1)" + d="m 165.29305,32.445235 0.33313,-12.554874 m -0.33313,12.554874 0.33313,-12.554874" + id="path1300-2-2-6-9" + sodipodi:nodetypes="cc" /> + <circle + style="fill:#ff0000;stroke:none;stroke-width:0.499999;stroke-dasharray:none;stop-color:#000000" + id="path3663" + cx="117.08417" + cy="38.792969" + r="2.7302806" /> + <circle + style="fill:#008000;stroke:none;stroke-width:0.499999;stroke-dasharray:none;stop-color:#000000" + id="path3663-3" + cx="123.57843" + cy="39.100433" + r="2.7302806" /> + <circle + style="fill:#800080;stroke:none;stroke-width:0.499999;stroke-dasharray:none;stop-color:#000000" + id="path3663-6" + cx="119.58919" + cy="67.645035" + r="2.7302806" /> + <circle + style="fill:#ff0000;stroke:none;stroke-width:0.499999;stroke-dasharray:none;stop-color:#000000" + id="path3663-1" + cx="18.004833" + cy="39.402473" + r="2.7302806" /> + <circle + style="fill:#008000;stroke:none;stroke-width:0.499999;stroke-dasharray:none;stop-color:#000000" + id="path3663-3-0" + cx="18.004833" + cy="30.371933" + r="2.7302806" /> + <circle + style="fill:#800080;stroke:none;stroke-width:0.499999;stroke-dasharray:none;stop-color:#000000" + id="path3663-6-6" + cx="18.004833" + cy="21.341394" + r="2.7302806" /> + <text + xml:space="preserve" + style="font-size:8.46667px;line-height:1.25;font-family:sans-serif;stroke-width:0.264583;fill:#000000" + x="6.9525447" + y="13.702217" + id="text3707"><tspan + sodipodi:role="line" + id="tspan3705" + style="stroke-width:0.264583;fill:#000000" + x="6.9525447" + y="13.702217">$write(\{a\})$:</tspan></text> + <text + xml:space="preserve" + style="font-size:8.46667px;line-height:1.25;font-family:sans-serif;fill:#000000;stroke-width:0.264583" + x="23.457415" + y="24.042637" + id="text3750"><tspan + sodipodi:role="line" + id="tspan3748" + style="fill:#000000;stroke-width:0.264583" + x="23.457415" + y="24.042637">$\sqsupseteq \{a\} \to$ OK</tspan></text> + <text + xml:space="preserve" + style="font-size:8.46667px;line-height:1.25;font-family:sans-serif;fill:#000000;stroke-width:0.264583" + x="23.457415" + y="33.02087" + id="text3750-3"><tspan + sodipodi:role="line" + id="tspan3748-2" + style="fill:#000000;stroke-width:0.264583" + x="23.457415" + y="33.02087">$\sqsupseteq \{a\} \to$ OK</tspan></text> + <text + xml:space="preserve" + style="font-size:8.46667px;line-height:1.25;font-family:sans-serif;fill:#000000;stroke-width:0.264583" + x="23.457415" + y="41.972523" + id="text3750-0"><tspan + sodipodi:role="line" + id="tspan3748-6" + style="fill:#000000;stroke-width:0.264583" + x="23.457415" + y="41.972523">$\sqsupseteq \{a\}$</tspan></text> + <text + xml:space="preserve" + style="font-size:8.46667px;line-height:1.25;font-family:sans-serif;fill:#000000;stroke-width:0.264583" + x="14.395845" + y="52.022549" + id="text4280"><tspan + sodipodi:role="line" + id="tspan4278" + style="fill:#000000;stroke-width:0.264583" + x="14.395845" + y="52.022549">return OK</tspan></text> + <text + xml:space="preserve" + style="font-size:8.46667px;line-height:1.25;font-family:sans-serif;fill:#000000;stroke-width:0.264583" + x="14.395845" + y="102.48464" + id="text4280-8"><tspan + sodipodi:role="line" + id="tspan4278-8" + style="fill:#000000;stroke-width:0.264583" + x="14.395845" + y="102.48464">return OK</tspan></text> + <circle + style="fill:#ff0000;stroke:none;stroke-width:0.499999;stroke-dasharray:none;stop-color:#000000" + id="path3663-1-4" + cx="18.004833" + cy="90.979645" + r="2.7302806" /> + <circle + style="fill:#008000;stroke:none;stroke-width:0.499999;stroke-dasharray:none;stop-color:#000000" + id="path3663-3-0-5" + cx="18.004833" + cy="81.949104" + r="2.7302806" /> + <circle + style="fill:#800080;stroke:none;stroke-width:0.499999;stroke-dasharray:none;stop-color:#000000" + id="path3663-6-6-2" + cx="18.004833" + cy="72.918564" + r="2.7302806" /> + <text + xml:space="preserve" + style="font-size:8.46667px;line-height:1.25;font-family:sans-serif;fill:#000000;stroke-width:0.264583" + x="6.9525447" + y="65.279381" + id="text3707-5"><tspan + sodipodi:role="line" + id="tspan3705-4" + style="fill:#000000;stroke-width:0.264583" + x="6.9525447" + y="65.279381">$write(\{b\})$:</tspan></text> + <text + xml:space="preserve" + style="font-size:8.46667px;line-height:1.25;font-family:sans-serif;fill:#999999;stroke-width:0.264583" + x="23.457415" + y="75.619804" + id="text3750-7"><tspan + sodipodi:role="line" + id="tspan3748-4" + style="fill:#999999;stroke-width:0.264583" + x="23.457415" + y="75.619804">$\not\sqsupseteq \{b\}$</tspan></text> + <text + xml:space="preserve" + style="font-size:8.46667px;line-height:1.25;font-family:sans-serif;fill:#000000;stroke-width:0.264583" + x="23.457415" + y="84.598038" + id="text3750-3-4"><tspan + sodipodi:role="line" + id="tspan3748-2-3" + style="fill:#000000;stroke-width:0.264583" + x="23.457415" + y="84.598038">$\sqsupseteq \{b\} \to$ OK</tspan></text> + <text + xml:space="preserve" + style="font-size:8.46667px;line-height:1.25;font-family:sans-serif;fill:#000000;stroke-width:0.264583" + x="23.457415" + y="93.54969" + id="text3750-0-0"><tspan + sodipodi:role="line" + id="tspan3748-6-7" + style="fill:#000000;stroke-width:0.264583" + x="23.457415" + y="93.54969">$\sqsupseteq \{b\} \to$ OK</tspan></text> + </g> +</svg> diff --git a/doc/talks/2023-01-18-tocatta/assets/latticeC.svg b/doc/talks/2023-01-18-tocatta/assets/latticeC.svg new file mode 100644 index 00000000..c815af94 --- /dev/null +++ b/doc/talks/2023-01-18-tocatta/assets/latticeC.svg @@ -0,0 +1,598 @@ +<?xml version="1.0" encoding="UTF-8" standalone="no"?> +<!-- Created with Inkscape (http://www.inkscape.org/) --> + +<svg + width="1000" + height="400" + viewBox="0 0 264.58333 105.83333" + version="1.1" + id="svg5" + inkscape:version="1.2.2 (b0a8486541, 2022-12-01)" + sodipodi:docname="latticeC.svg" + 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="namedview7" + pagecolor="#ffffff" + bordercolor="#666666" + borderopacity="1.0" + inkscape:showpageshadow="2" + inkscape:pageopacity="0.0" + inkscape:pagecheckerboard="0" + inkscape:deskcolor="#d1d1d1" + inkscape:document-units="mm" + showgrid="false" + inkscape:zoom="1.4734708" + inkscape:cx="450.97602" + inkscape:cy="272.14655" + inkscape:window-width="1920" + inkscape:window-height="999" + inkscape:window-x="0" + inkscape:window-y="0" + inkscape:window-maximized="1" + inkscape:current-layer="layer2" /> + <defs + id="defs2"> + <marker + style="overflow:visible" + id="Arrow2" + refX="0" + refY="0" + orient="auto-start-reverse" + inkscape:stockid="Arrow2" + markerWidth="7.6999998" + markerHeight="5.5999999" + viewBox="0 0 7.7 5.6" + inkscape:isstock="true" + inkscape:collect="always" + preserveAspectRatio="xMidYMid"> + <path + transform="scale(0.7)" + d="M -2,-4 9,0 -2,4 c 2,-2.33 2,-5.66 0,-8 z" + style="fill:context-stroke;fill-rule:evenodd;stroke:none" + id="arrow2L" /> + </marker> + <marker + style="overflow:visible" + id="Arrow2-9" + refX="0" + refY="0" + orient="auto-start-reverse" + inkscape:stockid="Arrow2" + markerWidth="7.6999998" + markerHeight="5.5999999" + viewBox="0 0 7.7 5.6" + inkscape:isstock="true" + inkscape:collect="always" + preserveAspectRatio="xMidYMid"> + <path + transform="scale(0.7)" + d="M -2,-4 9,0 -2,4 c 2,-2.33 2,-5.66 0,-8 z" + style="fill:context-stroke;fill-rule:evenodd;stroke:none" + id="arrow2L-1" /> + </marker> + <marker + style="overflow:visible" + id="Arrow2-9-7" + refX="0" + refY="0" + orient="auto-start-reverse" + inkscape:stockid="Arrow2" + markerWidth="7.6999998" + markerHeight="5.5999999" + viewBox="0 0 7.7 5.6" + inkscape:isstock="true" + inkscape:collect="always" + preserveAspectRatio="xMidYMid"> + <path + transform="scale(0.7)" + d="M -2,-4 9,0 -2,4 c 2,-2.33 2,-5.66 0,-8 z" + style="fill:context-stroke;fill-rule:evenodd;stroke:none" + id="arrow2L-1-0" /> + </marker> + <marker + style="overflow:visible" + id="Arrow2-93" + refX="0" + refY="0" + orient="auto-start-reverse" + inkscape:stockid="Arrow2" + markerWidth="7.6999998" + markerHeight="5.5999999" + viewBox="0 0 7.7 5.6" + inkscape:isstock="true" + inkscape:collect="always" + preserveAspectRatio="xMidYMid"> + <path + transform="scale(0.7)" + d="M -2,-4 9,0 -2,4 c 2,-2.33 2,-5.66 0,-8 z" + style="fill:context-stroke;fill-rule:evenodd;stroke:none" + id="arrow2L-6" /> + </marker> + <marker + style="overflow:visible" + id="Arrow2-9-7-2" + refX="0" + refY="0" + orient="auto-start-reverse" + inkscape:stockid="Arrow2" + markerWidth="7.6999998" + markerHeight="5.5999999" + viewBox="0 0 7.7 5.6" + inkscape:isstock="true" + inkscape:collect="always" + preserveAspectRatio="xMidYMid"> + <path + transform="scale(0.7)" + d="M -2,-4 9,0 -2,4 c 2,-2.33 2,-5.66 0,-8 z" + style="fill:context-stroke;fill-rule:evenodd;stroke:none" + id="arrow2L-1-0-6" /> + </marker> + <marker + style="overflow:visible" + id="Arrow2-93-1" + refX="0" + refY="0" + orient="auto-start-reverse" + inkscape:stockid="Arrow2" + markerWidth="7.6999998" + markerHeight="5.5999999" + viewBox="0 0 7.7 5.6" + inkscape:isstock="true" + inkscape:collect="always" + preserveAspectRatio="xMidYMid"> + <path + transform="scale(0.7)" + d="M -2,-4 9,0 -2,4 c 2,-2.33 2,-5.66 0,-8 z" + style="fill:context-stroke;fill-rule:evenodd;stroke:none" + id="arrow2L-6-8" /> + </marker> + <marker + style="overflow:visible" + id="Arrow2-9-75" + refX="0" + refY="0" + orient="auto-start-reverse" + inkscape:stockid="Arrow2" + markerWidth="7.6999998" + markerHeight="5.5999999" + viewBox="0 0 7.7 5.6" + inkscape:isstock="true" + inkscape:collect="always" + preserveAspectRatio="xMidYMid"> + <path + transform="scale(0.7)" + d="M -2,-4 9,0 -2,4 c 2,-2.33 2,-5.66 0,-8 z" + style="fill:context-stroke;fill-rule:evenodd;stroke:none" + id="arrow2L-1-9" /> + </marker> + <marker + style="overflow:visible" + id="Arrow2-9-75-2" + refX="0" + refY="0" + orient="auto-start-reverse" + inkscape:stockid="Arrow2" + markerWidth="7.6999998" + markerHeight="5.5999999" + viewBox="0 0 7.7 5.6" + inkscape:isstock="true" + inkscape:collect="always" + preserveAspectRatio="xMidYMid"> + <path + transform="scale(0.7)" + d="M -2,-4 9,0 -2,4 c 2,-2.33 2,-5.66 0,-8 z" + style="fill:context-stroke;fill-rule:evenodd;stroke:none" + id="arrow2L-1-9-8" /> + </marker> + <marker + style="overflow:visible" + id="Arrow2-9-75-7" + refX="0" + refY="0" + orient="auto-start-reverse" + inkscape:stockid="Arrow2" + markerWidth="7.6999998" + markerHeight="5.5999999" + viewBox="0 0 7.7 5.6" + inkscape:isstock="true" + inkscape:collect="always" + preserveAspectRatio="xMidYMid"> + <path + transform="scale(0.7)" + d="M -2,-4 9,0 -2,4 c 2,-2.33 2,-5.66 0,-8 z" + style="fill:context-stroke;fill-rule:evenodd;stroke:none" + id="arrow2L-1-9-3" /> + </marker> + <marker + style="overflow:visible" + id="Arrow2-9-75-7-1" + refX="0" + refY="0" + orient="auto-start-reverse" + inkscape:stockid="Arrow2" + markerWidth="7.6999998" + markerHeight="5.5999999" + viewBox="0 0 7.7 5.6" + inkscape:isstock="true" + inkscape:collect="always" + preserveAspectRatio="xMidYMid"> + <path + transform="scale(0.7)" + d="M -2,-4 9,0 -2,4 c 2,-2.33 2,-5.66 0,-8 z" + style="fill:context-stroke;fill-rule:evenodd;stroke:none" + id="arrow2L-1-9-3-2" /> + </marker> + <marker + style="overflow:visible" + id="Arrow2-93-1-4" + refX="0" + refY="0" + orient="auto-start-reverse" + inkscape:stockid="Arrow2" + markerWidth="7.6999998" + markerHeight="5.5999999" + viewBox="0 0 7.7 5.6" + inkscape:isstock="true" + inkscape:collect="always" + preserveAspectRatio="xMidYMid"> + <path + transform="scale(0.7)" + d="M -2,-4 9,0 -2,4 c 2,-2.33 2,-5.66 0,-8 z" + style="fill:context-stroke;fill-rule:evenodd;stroke:none" + id="arrow2L-6-8-7" /> + </marker> + <marker + style="overflow:visible" + id="Arrow2-9-7-2-8" + refX="0" + refY="0" + orient="auto-start-reverse" + inkscape:stockid="Arrow2" + markerWidth="7.6999998" + markerHeight="5.5999999" + viewBox="0 0 7.7 5.6" + inkscape:isstock="true" + inkscape:collect="always" + preserveAspectRatio="xMidYMid"> + <path + transform="scale(0.7)" + d="M -2,-4 9,0 -2,4 c 2,-2.33 2,-5.66 0,-8 z" + style="fill:context-stroke;fill-rule:evenodd;stroke:none" + id="arrow2L-1-0-6-4" /> + </marker> + </defs> + <g + inkscape:label="Layer 1" + inkscape:groupmode="layer" + id="layer1" + sodipodi:insensitive="true"> + <rect + style="fill:#ffffff;stroke:none;stroke-width:1;stop-color:#000000" + id="rect288" + width="209.84705" + height="104.42732" + x="0.77790999" + y="0.93738818" /> + </g> + <g + inkscape:groupmode="layer" + id="layer2" + inkscape:label="Layer 2"> + <text + xml:space="preserve" + style="font-size:8.46667px;line-height:1.25;font-family:sans-serif;text-align:center;text-anchor:middle;stroke-width:0.264583;fill:#000000" + x="164.56372" + y="99.307442" + id="text951"><tspan + sodipodi:role="line" + id="tspan949" + style="stroke-width:0.264583;fill:#000000" + x="164.56372" + y="99.307442">$\{\}$</tspan></text> + <text + xml:space="preserve" + style="font-size:8.46667px;line-height:1.25;font-family:sans-serif;text-align:center;text-anchor:middle;stroke-width:0.264583;fill:#000000" + x="164.56372" + y="13.151893" + id="text1005"><tspan + sodipodi:role="line" + id="tspan1003" + style="stroke-width:0.264583;fill:#000000" + x="164.56372" + y="13.151893">$\{a,b,c\}$</tspan></text> + <g + id="g1175" + transform="translate(51.996784,3.5774043)"> + <text + xml:space="preserve" + style="font-size:8.46667px;line-height:1.25;font-family:sans-serif;text-align:center;text-anchor:middle;stroke-width:0.264583;fill:#000000" + x="49.27084" + y="67.008698" + id="text1009"><tspan + sodipodi:role="line" + id="tspan1007" + style="stroke-width:0.264583;fill:#000000" + x="49.27084" + y="67.008698">$\{a\}$</tspan></text> + <text + xml:space="preserve" + style="font-size:8.46667px;line-height:1.25;font-family:sans-serif;text-align:center;text-anchor:middle;stroke-width:0.264583;fill:#000000" + x="112.90984" + y="67.017166" + id="text1009-3"><tspan + sodipodi:role="line" + id="tspan1007-6" + style="stroke-width:0.264583;fill:#000000" + x="112.90984" + y="67.017166">$\{b\}$</tspan></text> + <text + xml:space="preserve" + style="font-size:8.46667px;line-height:1.25;font-family:sans-serif;text-align:center;text-anchor:middle;stroke-width:0.264583;fill:#000000" + x="176.20593" + y="67.008698" + id="text1009-7"><tspan + sodipodi:role="line" + id="tspan1007-5" + style="stroke-width:0.264583;fill:#000000" + x="176.20593" + y="67.008698">$\{c\}$</tspan></text> + </g> + <g + id="g1183" + transform="translate(51.996784,1.0317046)" + style="fill:#000000"> + <text + xml:space="preserve" + style="font-size:8.46667px;line-height:1.25;font-family:sans-serif;text-align:center;text-anchor:middle;stroke-width:0.264583;fill:#000000" + x="112.90984" + y="40.841526" + id="text1117"><tspan + sodipodi:role="line" + id="tspan1115" + style="stroke-width:0.264583;fill:#000000" + x="112.90984" + y="40.841526">$\{a,c\}$</tspan></text> + <text + xml:space="preserve" + style="font-size:8.46667px;line-height:1.25;font-family:sans-serif;text-align:center;text-anchor:middle;stroke-width:0.264583;fill:#000000" + x="49.27084" + y="40.841526" + id="text1117-3"><tspan + sodipodi:role="line" + id="tspan1115-5" + style="stroke-width:0.264583;fill:#000000" + x="49.27084" + y="40.841526">$\{a,b\}$</tspan></text> + <text + xml:space="preserve" + style="font-size:8.46667px;line-height:1.25;font-family:sans-serif;text-align:center;text-anchor:middle;stroke-width:0.264583;fill:#000000" + x="176.20593" + y="40.841526" + id="text1117-6"><tspan + sodipodi:role="line" + id="tspan1115-2" + style="stroke-width:0.264583;fill:#000000" + x="176.20593" + y="40.841526">$\{b,c\}$</tspan></text> + </g> + <path + style="fill:none;stroke:#000000;stroke-width:0.5;stroke-linecap:butt;stroke-linejoin:miter;stroke-dasharray:none;stroke-opacity:1;marker-end:url(#Arrow2)" + d="M 153.33622,90.367682 118.34198,73.428915" + id="path1300" /> + <path + style="fill:none;stroke:#000000;stroke-width:0.5;stroke-linecap:butt;stroke-linejoin:miter;stroke-dasharray:none;stroke-opacity:1;marker-end:url(#Arrow2-9)" + d="M 177.46016,90.367682 212.4544,73.428915" + id="path1300-2" /> + <path + style="fill:none;stroke:#000000;stroke-width:0.5;stroke-linecap:butt;stroke-linejoin:miter;stroke-dasharray:none;stroke-opacity:1;marker-end:url(#Arrow2-93)" + d="M 153.33622,61.655656 118.34198,44.716889" + id="path1300-0" /> + <path + style="fill:none;stroke:#000000;stroke-width:0.5;stroke-linecap:butt;stroke-linejoin:miter;stroke-dasharray:none;stroke-opacity:1;marker-end:url(#Arrow2-9-7)" + d="M 177.46016,61.655656 212.4544,44.716889" + id="path1300-2-6" /> + <path + style="fill:none;stroke:#000000;stroke-width:0.5;stroke-linecap:butt;stroke-linejoin:miter;stroke-dasharray:none;stroke-opacity:1;marker-end:url(#Arrow2-93-1)" + d="M 118.34198,61.655656 153.33622,44.716889" + id="path1300-0-7" /> + <path + style="fill:none;stroke:#000000;stroke-width:0.5;stroke-linecap:butt;stroke-linejoin:miter;stroke-dasharray:none;stroke-opacity:1;marker-end:url(#Arrow2-9-7-2)" + d="M 212.4544,61.655656 177.46016,44.716889" + id="path1300-2-6-9" /> + <path + style="fill:none;stroke:#000000;stroke-width:0.5;stroke-linecap:butt;stroke-linejoin:miter;stroke-dasharray:none;stroke-opacity:1;marker-end:url(#Arrow2-93-1-4)" + d="M 118.34198,34.227412 153.33622,17.288645" + id="path1300-0-7-5" /> + <path + style="fill:none;stroke:#000000;stroke-width:0.5;stroke-linecap:butt;stroke-linejoin:miter;stroke-dasharray:none;stroke-opacity:1;marker-end:url(#Arrow2-9-7-2-8)" + d="M 212.4544,34.227412 177.46016,17.288645" + id="path1300-2-6-9-0" /> + <path + style="fill:none;stroke:#000000;stroke-width:0.5;stroke-linecap:butt;stroke-linejoin:miter;stroke-dasharray:none;stroke-opacity:1;marker-end:url(#Arrow2-9-75)" + d="m 228.52843,61.091809 0.33313,-12.554874 m -0.33313,12.554874 0.33313,-12.554874" + id="path1300-2-2" + sodipodi:nodetypes="cc" /> + <path + style="fill:none;stroke:#000000;stroke-width:0.5;stroke-linecap:butt;stroke-linejoin:miter;stroke-dasharray:none;stroke-opacity:1;marker-end:url(#Arrow2-9-75-2)" + d="m 101.90418,61.091809 0.33313,-12.554874 m -0.33313,12.554874 0.33313,-12.554874" + id="path1300-2-2-9" + sodipodi:nodetypes="cc" /> + <path + style="fill:none;stroke:#000000;stroke-width:0.5;stroke-linecap:butt;stroke-linejoin:miter;stroke-dasharray:none;stroke-opacity:1;marker-end:url(#Arrow2-9-75-7)" + d="m 165.29305,89.571762 0.33313,-12.554874 m -0.33313,12.554874 0.33313,-12.554874" + id="path1300-2-2-6" + sodipodi:nodetypes="cc" /> + <path + style="fill:none;stroke:#000000;stroke-width:0.5;stroke-linecap:butt;stroke-linejoin:miter;stroke-dasharray:none;stroke-opacity:1;marker-end:url(#Arrow2-9-75-7-1)" + d="m 165.29305,32.445235 0.33313,-12.554874 m -0.33313,12.554874 0.33313,-12.554874" + id="path1300-2-2-6-9" + sodipodi:nodetypes="cc" /> + <circle + style="fill:#ff0000;stroke:none;stroke-width:0.499999;stroke-dasharray:none;stop-color:#000000" + id="path3663" + cx="117.08417" + cy="38.792969" + r="2.7302806" /> + <circle + style="fill:#008000;stroke:none;stroke-width:0.499999;stroke-dasharray:none;stop-color:#000000" + id="path3663-3" + cx="123.57843" + cy="39.100433" + r="2.7302806" /> + <circle + style="fill:#800080;stroke:none;stroke-width:0.499999;stroke-dasharray:none;stop-color:#000000" + id="path3663-6" + cx="130.27556" + cy="39.441635" + r="2.7302806" /> + <circle + style="fill:#ff0000;stroke:none;stroke-width:0.499999;stroke-dasharray:none;stop-color:#000000" + id="path3663-1" + cx="18.004833" + cy="39.402473" + r="2.7302806" /> + <circle + style="fill:#008000;stroke:none;stroke-width:0.499999;stroke-dasharray:none;stop-color:#000000" + id="path3663-3-0" + cx="18.004833" + cy="30.371933" + r="2.7302806" /> + <circle + style="fill:#800080;stroke:none;stroke-width:0.499999;stroke-dasharray:none;stop-color:#000000" + id="path3663-6-6" + cx="18.004833" + cy="21.341394" + r="2.7302806" /> + <text + xml:space="preserve" + style="font-size:8.46667px;line-height:1.25;font-family:sans-serif;stroke-width:0.264583;fill:#000000" + x="6.9525447" + y="13.702217" + id="text3707"><tspan + sodipodi:role="line" + id="tspan3705" + style="stroke-width:0.264583;fill:#000000" + x="6.9525447" + y="13.702217">$write(\{a\})$:</tspan></text> + <text + xml:space="preserve" + style="font-size:8.46667px;line-height:1.25;font-family:sans-serif;fill:#000000;stroke-width:0.264583" + x="23.457415" + y="24.042637" + id="text3750"><tspan + sodipodi:role="line" + id="tspan3748" + style="fill:#000000;stroke-width:0.264583" + x="23.457415" + y="24.042637">$\sqsupseteq \{a\} \to$ OK</tspan></text> + <text + xml:space="preserve" + style="font-size:8.46667px;line-height:1.25;font-family:sans-serif;fill:#000000;stroke-width:0.264583" + x="23.457415" + y="33.02087" + id="text3750-3"><tspan + sodipodi:role="line" + id="tspan3748-2" + style="fill:#000000;stroke-width:0.264583" + x="23.457415" + y="33.02087">$\sqsupseteq \{a\} \to$ OK</tspan></text> + <text + xml:space="preserve" + style="font-size:8.46667px;line-height:1.25;font-family:sans-serif;fill:#000000;stroke-width:0.264583" + x="23.457415" + y="41.972523" + id="text3750-0"><tspan + sodipodi:role="line" + id="tspan3748-6" + style="fill:#000000;stroke-width:0.264583" + x="23.457415" + y="41.972523">$\sqsupseteq \{a\}$</tspan></text> + <text + xml:space="preserve" + style="font-size:8.46667px;line-height:1.25;font-family:sans-serif;fill:#000000;stroke-width:0.264583" + x="14.395845" + y="52.022549" + id="text4280"><tspan + sodipodi:role="line" + id="tspan4278" + style="fill:#000000;stroke-width:0.264583" + x="14.395845" + y="52.022549">return OK</tspan></text> + <text + xml:space="preserve" + style="font-size:8.46667px;line-height:1.25;font-family:sans-serif;fill:#000000;stroke-width:0.264583" + x="14.395845" + y="102.48464" + id="text4280-8"><tspan + sodipodi:role="line" + id="tspan4278-8" + style="fill:#000000;stroke-width:0.264583" + x="14.395845" + y="102.48464">return OK</tspan></text> + <circle + style="fill:#ff0000;stroke:none;stroke-width:0.499999;stroke-dasharray:none;stop-color:#000000" + id="path3663-1-4" + cx="18.004833" + cy="90.979645" + r="2.7302806" /> + <circle + style="fill:#008000;stroke:none;stroke-width:0.499999;stroke-dasharray:none;stop-color:#000000" + id="path3663-3-0-5" + cx="18.004833" + cy="81.949104" + r="2.7302806" /> + <circle + style="fill:#800080;stroke:none;stroke-width:0.499999;stroke-dasharray:none;stop-color:#000000" + id="path3663-6-6-2" + cx="18.004833" + cy="72.918564" + r="2.7302806" /> + <text + xml:space="preserve" + style="font-size:8.46667px;line-height:1.25;font-family:sans-serif;fill:#000000;stroke-width:0.264583" + x="6.9525447" + y="65.279381" + id="text3707-5"><tspan + sodipodi:role="line" + id="tspan3705-4" + style="fill:#000000;stroke-width:0.264583" + x="6.9525447" + y="65.279381">$write(\{b\})$:</tspan></text> + <text + xml:space="preserve" + style="font-size:8.46667px;line-height:1.25;font-family:sans-serif;fill:#000000;stroke-width:0.264583" + x="23.457415" + y="75.619804" + id="text3750-7"><tspan + sodipodi:role="line" + id="tspan3748-4" + style="fill:#000000;stroke-width:0.264583" + x="23.457415" + y="75.619804">$\sqsupseteq \{b\}$</tspan></text> + <text + xml:space="preserve" + style="font-size:8.46667px;line-height:1.25;font-family:sans-serif;fill:#000000;stroke-width:0.264583" + x="23.457415" + y="84.598038" + id="text3750-3-4"><tspan + sodipodi:role="line" + id="tspan3748-2-3" + style="fill:#000000;stroke-width:0.264583" + x="23.457415" + y="84.598038">$\sqsupseteq \{b\} \to$ OK</tspan></text> + <text + xml:space="preserve" + style="font-size:8.46667px;line-height:1.25;font-family:sans-serif;fill:#000000;stroke-width:0.264583" + x="23.457415" + y="93.54969" + id="text3750-0-0"><tspan + sodipodi:role="line" + id="tspan3748-6-7" + style="fill:#000000;stroke-width:0.264583" + x="23.457415" + y="93.54969">$\sqsupseteq \{b\} \to$ OK</tspan></text> + </g> +</svg> diff --git a/doc/talks/2023-01-18-tocatta/talk.pdf b/doc/talks/2023-01-18-tocatta/talk.pdf Binary files differindex ba9bde3d..02f605e8 100644 --- a/doc/talks/2023-01-18-tocatta/talk.pdf +++ b/doc/talks/2023-01-18-tocatta/talk.pdf diff --git a/doc/talks/2023-01-18-tocatta/talk.tex b/doc/talks/2023-01-18-tocatta/talk.tex index ac9b4077..e789f597 100644 --- a/doc/talks/2023-01-18-tocatta/talk.tex +++ b/doc/talks/2023-01-18-tocatta/talk.tex @@ -494,8 +494,7 @@ \item \textbf{Linearizability} of all operations\\ (strongest consistency guarantee) \vspace{1em} - \item \textbf{Replicated state machines} that can implement - any sequential specification + \item Any sequential specification can be implemented as a \textbf{replicated state machine} \vspace{1em} \item \textbf{Costly}, the leader is a bottleneck; leader elections on failure take time @@ -515,7 +514,7 @@ \item \textbf{Operations have to commute}, i.e.~we can only implement CRDTs \vspace{1em} - \item \textbf{Fast}, no node is a bottleneck;\\ + \item \textbf{Fast}, no single bottleneck;\\ works the same with offline nodes \end{itemize} } \end{minipage} @@ -530,27 +529,29 @@ \vspace{2em} \hspace{1em} - \begin{minipage}{7cm} + \begin{minipage}{6.5cm} \underline{Consensus-based systems:} \vspace{1em} \textbf{Any sequential specification}\\~ + + \vspace{1em} + \textbf{Easier to program for}: just write your program as if it were sequential on a single machine + \end{minipage} \hfill - \begin{minipage}{7cm} + \begin{minipage}{6.5cm} \underline{Weakly consistent systems:} \vspace{1em} \textbf{CRDTs only}\\(conflict-free replicated data types) + + \vspace{1em} + Part of the complexity is \textbf{reported to the consumer of the API}\\~ \end{minipage} \hspace{1em} - - \vspace{3em} - \begin{center} - Part of the complexity is \textbf{reported to the consumer of the API} - \end{center} \end{frame} \begin{frame} @@ -663,7 +664,27 @@ \end{frame} \begin{frame} - \frametitle{Impact on performances} + \frametitle{Understanding CRDTs and quorums} + \begin{figure} + \centering + \def\svgwidth{.8\textwidth} + \only<1>{\import{assets/}{lattice1.pdf_tex}}% + \only<2>{\import{assets/}{lattice2.pdf_tex}}% + \only<3>{\import{assets/}{lattice3.pdf_tex}}% + \only<4>{\import{assets/}{lattice4.pdf_tex}}% + \only<5>{\import{assets/}{lattice5.pdf_tex}}% + \only<6>{\import{assets/}{lattice6.pdf_tex}}% + \only<7>{\import{assets/}{lattice7.pdf_tex}}% + \only<8>{\import{assets/}{lattice8.pdf_tex}}% + \only<9>{\import{assets/}{lattice9.pdf_tex}}% + \only<10>{\import{assets/}{latticeA.pdf_tex}}% + \only<11>{\import{assets/}{latticeB.pdf_tex}}% + \only<12>{\import{assets/}{latticeC.pdf_tex}}% + \end{figure} +\end{frame} + +\begin{frame} + \frametitle{Performance gains in practice} \begin{center} \includegraphics[width=.8\linewidth]{assets/endpoint-latency-dc.png} \end{center} |
