Mercurial > hg > Papers > 2021 > soto-prosym
changeset 10:60d4617eac84
fix slide intro
| author | soto <soto@cr.ie.u-ryukyu.ac.jp> |
|---|---|
| date | Thu, 06 Jan 2022 13:59:12 +0900 |
| parents | e02e29a614c9 |
| children | 8a97e69f8615 |
| files | MindMap/slide.html slide/slide.md |
| diffstat | 2 files changed, 507 insertions(+), 411 deletions(-) [+] |
line wrap: on
line diff
--- a/MindMap/slide.html Thu Jan 06 11:18:27 2022 +0900 +++ b/MindMap/slide.html Thu Jan 06 13:59:12 2022 +0900 @@ -9,7 +9,7 @@ * @size 16:9 1280px 720px * @size 4:3 960px 720px */div#p>svg>foreignObject>section{-ms-text-size-adjust:100%;-webkit-text-size-adjust:100%;word-wrap:break-word;background-color:#fff;color:#24292f;font-family:-apple-system,BlinkMacSystemFont,Segoe UI,Helvetica,Arial,sans-serif,Apple Color Emoji,Segoe UI Emoji;font-size:16px;line-height:1.5;margin:0}div#p>svg>foreignObject>section{--marpit-root-font-size:16px}div#p>svg>foreignObject>section .octicon{fill:currentColor;display:inline-block;vertical-align:text-bottom}div#p>svg>foreignObject>section h1:hover .anchor .octicon-link:before,div#p>svg>foreignObject>section h2:hover .anchor .octicon-link:before,div#p>svg>foreignObject>section h3:hover .anchor .octicon-link:before,div#p>svg>foreignObject>section h4:hover .anchor .octicon-link:before,div#p>svg>foreignObject>section h5:hover .anchor .octicon-link:before,div#p>svg>foreignObject>section h6:hover .anchor .octicon-link:before{background-color:currentColor;content:" ";display:inline-block;height:16px;-webkit-mask-image:url('data:image/svg+xml;charset=utf-8,<svg xmlns="http://www.w3.org/2000/svg" viewBox="0 0 16 16" aria-hidden="true"><path fill-rule="evenodd" d="M7.775 3.275a.75.75 0 0 0 1.06 1.06l1.25-1.25a2 2 0 1 1 2.83 2.83l-2.5 2.5a2 2 0 0 1-2.83 0 .75.75 0 0 0-1.06 1.06 3.5 3.5 0 0 0 4.95 0l2.5-2.5a3.5 3.5 0 0 0-4.95-4.95l-1.25 1.25zm-4.69 9.64a2 2 0 0 1 0-2.83l2.5-2.5a2 2 0 0 1 2.83 0 .75.75 0 0 0 1.06-1.06 3.5 3.5 0 0 0-4.95 0l-2.5 2.5a3.5 3.5 0 0 0 4.95 4.95l1.25-1.25a.75.75 0 0 0-1.06-1.06l-1.25 1.25a2 2 0 0 1-2.83 0z"/></svg>');mask-image:url('data:image/svg+xml;charset=utf-8,<svg xmlns="http://www.w3.org/2000/svg" viewBox="0 0 16 16" aria-hidden="true"><path fill-rule="evenodd" d="M7.775 3.275a.75.75 0 0 0 1.06 1.06l1.25-1.25a2 2 0 1 1 2.83 2.83l-2.5 2.5a2 2 0 0 1-2.83 0 .75.75 0 0 0-1.06 1.06 3.5 3.5 0 0 0 4.95 0l2.5-2.5a3.5 3.5 0 0 0-4.95-4.95l-1.25 1.25zm-4.69 9.64a2 2 0 0 1 0-2.83l2.5-2.5a2 2 0 0 1 2.83 0 .75.75 0 0 0 1.06-1.06 3.5 3.5 0 0 0-4.95 0l-2.5 2.5a3.5 3.5 0 0 0 4.95 4.95l1.25-1.25a.75.75 0 0 0-1.06-1.06l-1.25 1.25a2 2 0 0 1-2.83 0z"/></svg>');width:16px}div#p>svg>foreignObject>section details,div#p>svg>foreignObject>section figcaption,div#p>svg>foreignObject>section figure{display:block}div#p>svg>foreignObject>section summary{display:list-item}div#p>svg>foreignObject>section a{background-color:transparent;color:#0969da;text-decoration:none}div#p>svg>foreignObject>section a:active,div#p>svg>foreignObject>section a:hover{outline-width:0}div#p>svg>foreignObject>section abbr[title]{border-bottom:none;-webkit-text-decoration:underline dotted;text-decoration:underline dotted}div#p>svg>foreignObject>section b,div#p>svg>foreignObject>section strong{font-weight:600}div#p>svg>foreignObject>section dfn{font-style:italic}div#p>svg>foreignObject>section h1{border-bottom:1px solid #d8dee4;font-size:2em;font-weight:600;margin:.67em 0;padding-bottom:.3em}div#p>svg>foreignObject>section mark{background-color:#ff0;color:#24292f}div#p>svg>foreignObject>section small{font-size:90%}div#p>svg>foreignObject>section sub,div#p>svg>foreignObject>section sup{font-size:75%;line-height:0;position:relative;vertical-align:baseline}div#p>svg>foreignObject>section sub{bottom:-.25em}div#p>svg>foreignObject>section sup{top:-.5em}div#p>svg>foreignObject>section img{background-color:#fff;border-style:none;box-sizing:content-box;max-width:100%}div#p>svg>foreignObject>section code,div#p>svg>foreignObject>section kbd,div#p>svg>foreignObject>section pre,div#p>svg>foreignObject>section samp{font-family:monospace,monospace;font-size:1em}div#p>svg>foreignObject>section figure{margin:1em 40px}div#p>svg>foreignObject>section hr{background:transparent;background-color:#d0d7de;border:0;box-sizing:content-box;height:.25em;margin:24px 0;overflow:hidden;padding:0}div#p>svg>foreignObject>section [type=reset],div#p>svg>foreignObject>section [type=submit],div#p>svg>foreignObject>section html [type=button]{-webkit-appearance:button}div#p>svg>foreignObject>section [type=button]::-moz-focus-inner,div#p>svg>foreignObject>section [type=reset]::-moz-focus-inner,div#p>svg>foreignObject>section [type=submit]::-moz-focus-inner{border-style:none;padding:0}div#p>svg>foreignObject>section [type=button]:-moz-focusring,div#p>svg>foreignObject>section [type=reset]:-moz-focusring,div#p>svg>foreignObject>section [type=submit]:-moz-focusring{outline:1px dotted ButtonText}div#p>svg>foreignObject>section [type=checkbox],div#p>svg>foreignObject>section [type=radio]{box-sizing:border-box;padding:0}div#p>svg>foreignObject>section [type=number]::-webkit-inner-spin-button,div#p>svg>foreignObject>section [type=number]::-webkit-outer-spin-button{height:auto}div#p>svg>foreignObject>section [type=search]{-webkit-appearance:textfield;outline-offset:-2px}div#p>svg>foreignObject>section [type=search]::-webkit-search-cancel-button,div#p>svg>foreignObject>section [type=search]::-webkit-search-decoration{-webkit-appearance:none}div#p>svg>foreignObject>section ::-webkit-input-placeholder{color:inherit;opacity:.54}div#p>svg>foreignObject>section ::-webkit-file-upload-button{-webkit-appearance:button;font:inherit}div#p>svg>foreignObject>section a:hover{text-decoration:underline}div#p>svg>foreignObject>section hr:after,div#p>svg>foreignObject>section hr:before{content:"";display:table}div#p>svg>foreignObject>section hr:after{clear:both}div#p>svg>foreignObject>section table{border-collapse:collapse;border-spacing:0;display:block;max-width:100%;overflow:auto;width:-webkit-max-content;width:-moz-max-content;width:max-content}div#p>svg>foreignObject>section td,div#p>svg>foreignObject>section th{padding:0}div#p>svg>foreignObject>section details summary{cursor:pointer}div#p>svg>foreignObject>section details:not([open])>:not(summary){display:none!important}div#p>svg>foreignObject>section kbd{background-color:#f6f8fa;border:1px solid rgba(175,184,193,.2);border-radius:6px;box-shadow:inset 0 -1px 0 rgba(175,184,193,.2);color:#24292f;display:inline-block;font:11px ui-monospace,SFMono-Regular,SF Mono,Menlo,Consolas,Liberation Mono,monospace;line-height:10px;padding:3px 5px;vertical-align:middle}div#p>svg>foreignObject>section h1,div#p>svg>foreignObject>section h2,div#p>svg>foreignObject>section h3,div#p>svg>foreignObject>section h4,div#p>svg>foreignObject>section h5,div#p>svg>foreignObject>section h6{font-weight:600;line-height:1.25;margin-bottom:16px;margin-top:24px}div#p>svg>foreignObject>section h2{border-bottom:1px solid #d8dee4;font-size:1.5em;font-weight:600;padding-bottom:.3em}div#p>svg>foreignObject>section h3{font-size:1.25em;font-weight:600}div#p>svg>foreignObject>section h4{font-size:1em;font-weight:600}div#p>svg>foreignObject>section h5{font-size:.875em;font-weight:600}div#p>svg>foreignObject>section h6{color:#57606a;font-size:.85em;font-weight:600}div#p>svg>foreignObject>section p{margin-bottom:10px;margin-top:0}div#p>svg>foreignObject>section blockquote{border-left:.25em solid #d0d7de;color:#57606a;margin:0;padding:0 1em}div#p>svg>foreignObject>section ol,div#p>svg>foreignObject>section ul{margin-bottom:0;margin-top:0;padding-left:2em}div#p>svg>foreignObject>section ol ol,div#p>svg>foreignObject>section ul ol{list-style-type:lower-roman}div#p>svg>foreignObject>section ol ol ol,div#p>svg>foreignObject>section ol ul ol,div#p>svg>foreignObject>section ul ol ol,div#p>svg>foreignObject>section ul ul ol{list-style-type:lower-alpha}div#p>svg>foreignObject>section dd{margin-left:0}div#p>svg>foreignObject>section code,div#p>svg>foreignObject>section pre,div#p>svg>foreignObject>section tt{font-family:ui-monospace,SFMono-Regular,SF Mono,Menlo,Consolas,Liberation Mono,monospace;font-size:12px}div#p>svg>foreignObject>section pre{word-wrap:normal;margin-bottom:0;margin-top:0}div#p>svg>foreignObject>section :-ms-input-placeholder{color:#6e7781;opacity:1}div#p>svg>foreignObject>section ::-moz-placeholder{color:#6e7781;opacity:1}div#p>svg>foreignObject>section ::placeholder{color:#6e7781;opacity:1}div#p>svg>foreignObject>section .pl-c{color:#6e7781}div#p>svg>foreignObject>section .pl-c1,div#p>svg>foreignObject>section .pl-s .pl-v{color:#0550ae}div#p>svg>foreignObject>section .pl-e,div#p>svg>foreignObject>section .pl-en{color:#8250df}div#p>svg>foreignObject>section .pl-s .pl-s1,div#p>svg>foreignObject>section .pl-smi{color:#24292f}div#p>svg>foreignObject>section .pl-ent{color:#116329}div#p>svg>foreignObject>section .pl-k{color:#cf222e}div#p>svg>foreignObject>section .pl-pds,div#p>svg>foreignObject>section .pl-s,div#p>svg>foreignObject>section .pl-s .pl-pse .pl-s1,div#p>svg>foreignObject>section .pl-sr,div#p>svg>foreignObject>section .pl-sr .pl-cce,div#p>svg>foreignObject>section .pl-sr .pl-sra,div#p>svg>foreignObject>section .pl-sr .pl-sre{color:#0a3069}div#p>svg>foreignObject>section .pl-smw,div#p>svg>foreignObject>section .pl-v{color:#953800}div#p>svg>foreignObject>section .pl-bu{color:#82071e}div#p>svg>foreignObject>section .pl-ii{background-color:#82071e;color:#f6f8fa}div#p>svg>foreignObject>section .pl-c2{background-color:#cf222e;color:#f6f8fa}div#p>svg>foreignObject>section .pl-sr .pl-cce{color:#116329;font-weight:700}div#p>svg>foreignObject>section .pl-ml{color:#3b2300}div#p>svg>foreignObject>section .pl-mh,div#p>svg>foreignObject>section .pl-mh .pl-en,div#p>svg>foreignObject>section .pl-ms{color:#0550ae;font-weight:700}div#p>svg>foreignObject>section .pl-mi{color:#24292f;font-style:italic}div#p>svg>foreignObject>section .pl-mb{color:#24292f;font-weight:700}div#p>svg>foreignObject>section .pl-md{background-color:#ffebe9;color:#82071e}div#p>svg>foreignObject>section .pl-mi1{background-color:#dafbe1;color:#116329}div#p>svg>foreignObject>section .pl-mc{background-color:#ffd8b5;color:#953800}div#p>svg>foreignObject>section .pl-mi2{background-color:#0550ae;color:#eaeef2}div#p>svg>foreignObject>section .pl-mdr{color:#8250df;font-weight:700}div#p>svg>foreignObject>section .pl-ba{color:#57606a}div#p>svg>foreignObject>section .pl-sg{color:#8c959f}div#p>svg>foreignObject>section .pl-corl{color:#0a3069;text-decoration:underline}div#p>svg>foreignObject>section [data-catalyst]{display:block}div#p>svg>foreignObject>section g-emoji{font-family:Apple Color Emoji,Segoe UI Emoji,Segoe UI Symbol;font-size:1em;font-style:normal!important;font-weight:400;line-height:1;vertical-align:-.075em}div#p>svg>foreignObject>section g-emoji img{height:1em;width:1em}div#p>svg>foreignObject>section:after,div#p>svg>foreignObject>section:before{ - /* content:""; */display:table}div#p>svg>foreignObject>section:after{clear:both}div#p>svg>foreignObject>section>:first-child{margin-top:0!important}div#p>svg>foreignObject>section>:last-child{margin-bottom:0!important}div#p>svg>foreignObject>section a:not([href]){color:inherit;text-decoration:none}div#p>svg>foreignObject>section .absent{color:#cf222e}div#p>svg>foreignObject>section .anchor{float:left;line-height:1;margin-left:-20px;padding-right:4px}div#p>svg>foreignObject>section .anchor:focus{outline:none}div#p>svg>foreignObject>section blockquote,div#p>svg>foreignObject>section details,div#p>svg>foreignObject>section dl,div#p>svg>foreignObject>section ol,div#p>svg>foreignObject>section p,div#p>svg>foreignObject>section pre,div#p>svg>foreignObject>section table,div#p>svg>foreignObject>section ul{margin-bottom:16px;margin-top:0}div#p>svg>foreignObject>section blockquote>:first-child{margin-top:0}div#p>svg>foreignObject>section blockquote>:last-child{margin-bottom:0}div#p>svg>foreignObject>section sup>a:before{content:"["}div#p>svg>foreignObject>section sup>a:after{content:"]"}div#p>svg>foreignObject>section h1 .octicon-link,div#p>svg>foreignObject>section h2 .octicon-link,div#p>svg>foreignObject>section h3 .octicon-link,div#p>svg>foreignObject>section h4 .octicon-link,div#p>svg>foreignObject>section h5 .octicon-link,div#p>svg>foreignObject>section h6 .octicon-link{color:#24292f;vertical-align:middle;visibility:hidden}div#p>svg>foreignObject>section h1:hover .anchor,div#p>svg>foreignObject>section h2:hover .anchor,div#p>svg>foreignObject>section h3:hover .anchor,div#p>svg>foreignObject>section h4:hover .anchor,div#p>svg>foreignObject>section h5:hover .anchor,div#p>svg>foreignObject>section h6:hover .anchor{text-decoration:none}div#p>svg>foreignObject>section h1:hover .anchor .octicon-link,div#p>svg>foreignObject>section h2:hover .anchor .octicon-link,div#p>svg>foreignObject>section h3:hover .anchor .octicon-link,div#p>svg>foreignObject>section h4:hover .anchor .octicon-link,div#p>svg>foreignObject>section h5:hover .anchor .octicon-link,div#p>svg>foreignObject>section h6:hover .anchor .octicon-link{visibility:visible}div#p>svg>foreignObject>section h1 code,div#p>svg>foreignObject>section h1 tt,div#p>svg>foreignObject>section h2 code,div#p>svg>foreignObject>section h2 tt,div#p>svg>foreignObject>section h3 code,div#p>svg>foreignObject>section h3 tt,div#p>svg>foreignObject>section h4 code,div#p>svg>foreignObject>section h4 tt,div#p>svg>foreignObject>section h5 code,div#p>svg>foreignObject>section h5 tt,div#p>svg>foreignObject>section h6 code,div#p>svg>foreignObject>section h6 tt{font-size:inherit;padding:0 .2em}div#p>svg>foreignObject>section ol.no-list,div#p>svg>foreignObject>section ul.no-list{list-style-type:none;padding:0}div#p>svg>foreignObject>section ol[type="1"]{list-style-type:decimal}div#p>svg>foreignObject>section ol[type=a]{list-style-type:lower-alpha}div#p>svg>foreignObject>section ol[type=i]{list-style-type:lower-roman}div#p>svg>foreignObject>section div>ol:not([type]){list-style-type:decimal}div#p>svg>foreignObject>section ol ol,div#p>svg>foreignObject>section ol ul,div#p>svg>foreignObject>section ul ol,div#p>svg>foreignObject>section ul ul{margin-bottom:0;margin-top:0}div#p>svg>foreignObject>section li>p{margin-top:16px}div#p>svg>foreignObject>section li+li{margin-top:.25em}div#p>svg>foreignObject>section dl{padding:0}div#p>svg>foreignObject>section dl dt{font-size:1em;font-style:italic;font-weight:600;margin-top:16px;padding:0}div#p>svg>foreignObject>section dl dd{margin-bottom:16px;padding:0 16px}div#p>svg>foreignObject>section table th{font-weight:600}div#p>svg>foreignObject>section table td,div#p>svg>foreignObject>section table th{border:1px solid #d0d7de;padding:6px 13px}div#p>svg>foreignObject>section table tr{background-color:#fff;border-top:1px solid #d8dee4}div#p>svg>foreignObject>section table tr:nth-child(2n){background-color:#f6f8fa}div#p>svg>foreignObject>section table img{background-color:transparent}div#p>svg>foreignObject>section img[align=right]{padding-left:20px}div#p>svg>foreignObject>section img[align=left]{padding-right:20px}div#p>svg>foreignObject>section .emoji{background-color:transparent;max-width:none;vertical-align:text-top}div#p>svg>foreignObject>section span.frame,div#p>svg>foreignObject>section span.frame>span{display:block;overflow:hidden}div#p>svg>foreignObject>section span.frame>span{border:1px solid #d0d7de;float:left;margin:13px 0 0;padding:7px;width:auto}div#p>svg>foreignObject>section span.frame span img{display:block;float:left}div#p>svg>foreignObject>section span.frame span span{clear:both;color:#24292f;display:block;padding:5px 0 0}div#p>svg>foreignObject>section span.align-center{clear:both;display:block;overflow:hidden}div#p>svg>foreignObject>section span.align-center>span{display:block;margin:13px auto 0;overflow:hidden;text-align:center}div#p>svg>foreignObject>section span.align-center span img{margin:0 auto;text-align:center}div#p>svg>foreignObject>section span.align-right{clear:both;display:block;overflow:hidden}div#p>svg>foreignObject>section span.align-right>span{display:block;margin:13px 0 0;overflow:hidden;text-align:right}div#p>svg>foreignObject>section span.align-right span img{margin:0;text-align:right}div#p>svg>foreignObject>section span.float-left{display:block;float:left;margin-right:13px;overflow:hidden}div#p>svg>foreignObject>section span.float-left span{margin:13px 0 0}div#p>svg>foreignObject>section span.float-right{display:block;float:right;margin-left:13px;overflow:hidden}div#p>svg>foreignObject>section span.float-right>span{display:block;margin:13px auto 0;overflow:hidden;text-align:right}div#p>svg>foreignObject>section code,div#p>svg>foreignObject>section tt{background-color:rgba(175,184,193,.2);border-radius:6px;font-size:85%;margin:0;padding:.2em .4em}div#p>svg>foreignObject>section code br,div#p>svg>foreignObject>section tt br{display:none}div#p>svg>foreignObject>section del code{text-decoration:inherit}div#p>svg>foreignObject>section pre code{font-size:100%}div#p>svg>foreignObject>section pre>code{background:transparent;border:0;margin:0;padding:0;white-space:pre;word-break:normal}div#p>svg>foreignObject>section .highlight{margin-bottom:16px}div#p>svg>foreignObject>section .highlight pre{margin-bottom:0;word-break:normal}div#p>svg>foreignObject>section pre{background-color:#f6f8fa;border-radius:6px;font-size:85%;line-height:1.45;overflow:auto;padding:16px}div#p>svg>foreignObject>section pre code,div#p>svg>foreignObject>section pre tt{word-wrap:normal;background-color:transparent;border:0;display:inline;line-height:inherit;margin:0;max-width:auto;overflow:visible;padding:0}div#p>svg>foreignObject>section .csv-data td,div#p>svg>foreignObject>section .csv-data th{font-size:12px;line-height:1;overflow:hidden;padding:5px;text-align:left;white-space:nowrap}div#p>svg>foreignObject>section .csv-data .blob-num{background:#fff;border:0;padding:10px 8px 9px;text-align:right}div#p>svg>foreignObject>section .csv-data tr{border-top:0}div#p>svg>foreignObject>section .csv-data th{background:#f6f8fa;border-top:0;font-weight:600}div#p>svg>foreignObject>section .footnotes{border-top:1px solid #d0d7de;color:#57606a;font-size:12px}div#p>svg>foreignObject>section div#p>svg>foreignObject>section section.footnotes{--marpit-root-font-size:12px}div#p>svg>foreignObject>section .footnotes ol{padding-left:16px}div#p>svg>foreignObject>section .footnotes li{position:relative}div#p>svg>foreignObject>section .footnotes li:target:before{border:2px solid #0969da;border-radius:6px;bottom:-8px;content:"";left:-24px;pointer-events:none;position:absolute;right:-8px;top:-8px}div#p>svg>foreignObject>section .footnotes li:target{color:#24292f}div#p>svg>foreignObject>section .footnotes .data-footnote-backref g-emoji{font-family:monospace}div#p>svg>foreignObject>section [hidden]{display:none!important}div#p>svg>foreignObject>section ::-webkit-calendar-picker-indicator{filter:invert(50%)}div#p>svg>foreignObject>section .hljs{background:#fff;color:#333;display:block;overflow-x:auto;padding:.5em}div#p>svg>foreignObject>section .hljs-comment,div#p>svg>foreignObject>section .hljs-meta{color:#969896}div#p>svg>foreignObject>section .hljs-emphasis,div#p>svg>foreignObject>section .hljs-quote,div#p>svg>foreignObject>section .hljs-strong,div#p>svg>foreignObject>section .hljs-template-variable,div#p>svg>foreignObject>section .hljs-variable{color:#df5000}div#p>svg>foreignObject>section .hljs-keyword,div#p>svg>foreignObject>section .hljs-selector-tag,div#p>svg>foreignObject>section .hljs-type{color:#d73a49}div#p>svg>foreignObject>section .hljs-attribute,div#p>svg>foreignObject>section .hljs-bullet,div#p>svg>foreignObject>section .hljs-literal,div#p>svg>foreignObject>section .hljs-symbol{color:#0086b3}div#p>svg>foreignObject>section .hljs-name,div#p>svg>foreignObject>section .hljs-section{color:#63a35c}div#p>svg>foreignObject>section .hljs-tag{color:#333}div#p>svg>foreignObject>section .hljs-attr,div#p>svg>foreignObject>section .hljs-selector-attr,div#p>svg>foreignObject>section .hljs-selector-class,div#p>svg>foreignObject>section .hljs-selector-id,div#p>svg>foreignObject>section .hljs-selector-pseudo,div#p>svg>foreignObject>section .hljs-title{color:#6f42c1}div#p>svg>foreignObject>section .hljs-addition{background-color:#eaffea;color:#55a532}div#p>svg>foreignObject>section .hljs-deletion{background-color:#ffecec;color:#bd2c00}div#p>svg>foreignObject>section .hljs-link{text-decoration:underline}div#p>svg>foreignObject>section .hljs-number{color:#005cc5}div#p>svg>foreignObject>section .hljs-string{color:#032f62}div#p>svg>foreignObject>section svg[data-marp-fitting=svg]{max-height:563px}div#p>svg>foreignObject>section h1{color:#246;font-size:1.6em}div#p>svg>foreignObject>section h1,div#p>svg>foreignObject>section h2{border-bottom:none}div#p>svg>foreignObject>section h2{font-size:1.3em}div#p>svg>foreignObject>section h3{font-size:1.1em}div#p>svg>foreignObject>section h4{font-size:1.05em}div#p>svg>foreignObject>section h5{font-size:1em}div#p>svg>foreignObject>section h6{font-size:.9em}div#p>svg>foreignObject>section h1 strong,div#p>svg>foreignObject>section h2 strong,div#p>svg>foreignObject>section h3 strong,div#p>svg>foreignObject>section h4 strong,div#p>svg>foreignObject>section h5 strong,div#p>svg>foreignObject>section h6 strong{color:#48c;font-weight:inherit}div#p>svg>foreignObject>section hr{height:0;padding-top:.25em}div#p>svg>foreignObject>section pre{border:1px solid #999;line-height:1.15;overflow:visible}div#p>svg>foreignObject>section pre code svg[data-marp-fitting=svg]{max-height:529px}div#p>svg>foreignObject>section footer,div#p>svg>foreignObject>section header{color:hsla(0,0%,40%,.75);font-size:18px;left:30px;margin:0;position:absolute}div#p>svg>foreignObject>section header{top:21px}div#p>svg>foreignObject>section footer{bottom:21px}div#p>svg>foreignObject>section{align-items:stretch;background:#fff;display:flex;flex-flow:column nowrap;font-size:29px;height:720px;justify-content:center;padding:78.5px;width:1280px}div#p>svg>foreignObject>section{--marpit-root-font-size:29px}div#p>svg>foreignObject>section>:last-child,div#p>svg>foreignObject>section[data-footer]>:nth-last-child(2){margin-bottom:0}div#p>svg>foreignObject>section>:first-child,div#p>svg>foreignObject>section>header:first-child+*{margin-top:0}div#p>svg>foreignObject>section:after{bottom:21px;color:#777;font-size:24px;padding:0;position:absolute;right:30px}div#p>svg>foreignObject>section:after{--marpit-root-font-size:24px}div#p>svg>foreignObject>section.invert{background-color:#222;color:#e6eaf0}div#p>svg>foreignObject>section.invert:after{color:#999}div#p>svg>foreignObject>section.invert img{background-color:transparent}div#p>svg>foreignObject>section.invert a{color:#50b3ff}div#p>svg>foreignObject>section.invert h1{color:#a3c5e7}div#p>svg>foreignObject>section.invert h2,div#p>svg>foreignObject>section.invert h3,div#p>svg>foreignObject>section.invert h4,div#p>svg>foreignObject>section.invert h5{color:#ebeff5}div#p>svg>foreignObject>section.invert blockquote,div#p>svg>foreignObject>section.invert h6{border-color:#3d3f43;color:#939699}div#p>svg>foreignObject>section.invert h1 strong,div#p>svg>foreignObject>section.invert h2 strong,div#p>svg>foreignObject>section.invert h3 strong,div#p>svg>foreignObject>section.invert h4 strong,div#p>svg>foreignObject>section.invert h5 strong,div#p>svg>foreignObject>section.invert h6 strong{color:#7bf}div#p>svg>foreignObject>section.invert hr{background-color:#3d3f43}div#p>svg>foreignObject>section.invert footer,div#p>svg>foreignObject>section.invert header{color:hsla(0,0%,60%,.75)}div#p>svg>foreignObject>section.invert code,div#p>svg>foreignObject>section.invert kbd{background-color:#111}div#p>svg>foreignObject>section.invert kbd{border-color:#666;box-shadow:inset 0 -1px 0 #555;color:#e6eaf0}div#p>svg>foreignObject>section.invert table tr{background-color:#12181d;border-color:#60657b}div#p>svg>foreignObject>section.invert table tr:nth-child(2n){background-color:#1b2024}div#p>svg>foreignObject>section.invert table td,div#p>svg>foreignObject>section.invert table th{border-color:#5b5e61}div#p>svg>foreignObject>section.invert pre{background-color:#0a0e12;border-color:#777}div#p>svg>foreignObject>section.invert pre code{background-color:transparent}div#p>svg>foreignObject>section[data-color] h1,div#p>svg>foreignObject>section[data-color] h2,div#p>svg>foreignObject>section[data-color] h3,div#p>svg>foreignObject>section[data-color] h4,div#p>svg>foreignObject>section[data-color] h5,div#p>svg>foreignObject>section[data-color] h6{color:currentColor}div#p>svg>foreignObject>section{width:1280px;height:720px}div#p>svg>foreignObject>section{background-color:#FFFFFF;font-size:28px;color:#4b4b4b;font-family:"Droid Sans Mono","Hiragino Maru Gothic ProN";background-image:url("logo.svg");background-position:right 3% bottom 2%;background-repeat:no-repeat;background-attachment:5%;background-size:20% auto}div#p>svg>foreignObject>section{--marpit-root-font-size:28px}div#p>svg>foreignObject>section.title h1{color:#808db5;text-align:center}div#p>svg>foreignObject>section.title p{bottom:25%;width:100%;position:absolute;font-size:25px;color:#4b4b4b;background:linear-gradient(transparent 90%,#ffcc00 0%)}div#p>svg>foreignObject>section.slide h1{width:95%;color:white;background-color:#808db5;position:absolute;left:50px;top:35px}div#p>svg>foreignObject>section[data-marpit-advanced-background=background]{columns:initial!important;display:block!important;padding:0!important}div#p>svg>foreignObject>section[data-marpit-advanced-background=background]:after,div#p>svg>foreignObject>section[data-marpit-advanced-background=background]:before,div#p>svg>foreignObject>section[data-marpit-advanced-background=content]:after,div#p>svg>foreignObject>section[data-marpit-advanced-background=content]:before{display:none!important}div#p>svg>foreignObject>section[data-marpit-advanced-background=background]>div[data-marpit-advanced-background-container]{all:initial;display:flex;flex-direction:row;height:100%;overflow:hidden;width:100%}div#p>svg>foreignObject>section[data-marpit-advanced-background=background]>div[data-marpit-advanced-background-container][data-marpit-advanced-background-direction=vertical]{flex-direction:column}div#p>svg>foreignObject>section[data-marpit-advanced-background=background][data-marpit-advanced-background-split]>div[data-marpit-advanced-background-container]{width:var(--marpit-advanced-background-split,50%)}div#p>svg>foreignObject>section[data-marpit-advanced-background=background][data-marpit-advanced-background-split=right]>div[data-marpit-advanced-background-container]{margin-left:calc(100% - var(--marpit-advanced-background-split, 50%))}div#p>svg>foreignObject>section[data-marpit-advanced-background=background]>div[data-marpit-advanced-background-container]>figure{all:initial;background-position:center;background-repeat:no-repeat;background-size:cover;flex:auto;margin:0}div#p>svg>foreignObject>section[data-marpit-advanced-background=content],div#p>svg>foreignObject>section[data-marpit-advanced-background=pseudo]{background:transparent!important}div#p>svg>foreignObject>section[data-marpit-advanced-background=pseudo],div#p>svg[data-marpit-svg]>foreignObject[data-marpit-advanced-background=pseudo]{pointer-events:none!important}div#p>svg>foreignObject>section[data-marpit-advanced-background-split]{width:100%;height:100%}</style></head><body><div class="bespoke-marp-osc"><button data-bespoke-marp-osc="prev" tabindex="-1" title="Previous slide">Previous slide</button><span data-bespoke-marp-osc="page"></span><button data-bespoke-marp-osc="next" tabindex="-1" title="Next slide">Next slide</button><button data-bespoke-marp-osc="fullscreen" tabindex="-1" title="Toggle fullscreen (f)">Toggle fullscreen</button><button data-bespoke-marp-osc="presenter" tabindex="-1" title="Open presenter view (p)">Open presenter view</button></div><div id="p"><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="1" data-paginate="true" data-class="title" data-theme="default" data-style="section { + /* content:""; */display:table}div#p>svg>foreignObject>section:after{clear:both}div#p>svg>foreignObject>section>:first-child{margin-top:0!important}div#p>svg>foreignObject>section>:last-child{margin-bottom:0!important}div#p>svg>foreignObject>section a:not([href]){color:inherit;text-decoration:none}div#p>svg>foreignObject>section .absent{color:#cf222e}div#p>svg>foreignObject>section .anchor{float:left;line-height:1;margin-left:-20px;padding-right:4px}div#p>svg>foreignObject>section .anchor:focus{outline:none}div#p>svg>foreignObject>section blockquote,div#p>svg>foreignObject>section details,div#p>svg>foreignObject>section dl,div#p>svg>foreignObject>section ol,div#p>svg>foreignObject>section p,div#p>svg>foreignObject>section pre,div#p>svg>foreignObject>section table,div#p>svg>foreignObject>section ul{margin-bottom:16px;margin-top:0}div#p>svg>foreignObject>section blockquote>:first-child{margin-top:0}div#p>svg>foreignObject>section blockquote>:last-child{margin-bottom:0}div#p>svg>foreignObject>section sup>a:before{content:"["}div#p>svg>foreignObject>section sup>a:after{content:"]"}div#p>svg>foreignObject>section h1 .octicon-link,div#p>svg>foreignObject>section h2 .octicon-link,div#p>svg>foreignObject>section h3 .octicon-link,div#p>svg>foreignObject>section h4 .octicon-link,div#p>svg>foreignObject>section h5 .octicon-link,div#p>svg>foreignObject>section h6 .octicon-link{color:#24292f;vertical-align:middle;visibility:hidden}div#p>svg>foreignObject>section h1:hover .anchor,div#p>svg>foreignObject>section h2:hover .anchor,div#p>svg>foreignObject>section h3:hover .anchor,div#p>svg>foreignObject>section h4:hover .anchor,div#p>svg>foreignObject>section h5:hover .anchor,div#p>svg>foreignObject>section h6:hover .anchor{text-decoration:none}div#p>svg>foreignObject>section h1:hover .anchor .octicon-link,div#p>svg>foreignObject>section h2:hover .anchor .octicon-link,div#p>svg>foreignObject>section h3:hover .anchor .octicon-link,div#p>svg>foreignObject>section h4:hover .anchor .octicon-link,div#p>svg>foreignObject>section h5:hover .anchor .octicon-link,div#p>svg>foreignObject>section h6:hover .anchor .octicon-link{visibility:visible}div#p>svg>foreignObject>section h1 code,div#p>svg>foreignObject>section h1 tt,div#p>svg>foreignObject>section h2 code,div#p>svg>foreignObject>section h2 tt,div#p>svg>foreignObject>section h3 code,div#p>svg>foreignObject>section h3 tt,div#p>svg>foreignObject>section h4 code,div#p>svg>foreignObject>section h4 tt,div#p>svg>foreignObject>section h5 code,div#p>svg>foreignObject>section h5 tt,div#p>svg>foreignObject>section h6 code,div#p>svg>foreignObject>section h6 tt{font-size:inherit;padding:0 .2em}div#p>svg>foreignObject>section ol.no-list,div#p>svg>foreignObject>section ul.no-list{list-style-type:none;padding:0}div#p>svg>foreignObject>section ol[type="1"]{list-style-type:decimal}div#p>svg>foreignObject>section ol[type=a]{list-style-type:lower-alpha}div#p>svg>foreignObject>section ol[type=i]{list-style-type:lower-roman}div#p>svg>foreignObject>section div>ol:not([type]){list-style-type:decimal}div#p>svg>foreignObject>section ol ol,div#p>svg>foreignObject>section ol ul,div#p>svg>foreignObject>section ul ol,div#p>svg>foreignObject>section ul ul{margin-bottom:0;margin-top:0}div#p>svg>foreignObject>section li>p{margin-top:16px}div#p>svg>foreignObject>section li+li{margin-top:.25em}div#p>svg>foreignObject>section dl{padding:0}div#p>svg>foreignObject>section dl dt{font-size:1em;font-style:italic;font-weight:600;margin-top:16px;padding:0}div#p>svg>foreignObject>section dl dd{margin-bottom:16px;padding:0 16px}div#p>svg>foreignObject>section table th{font-weight:600}div#p>svg>foreignObject>section table td,div#p>svg>foreignObject>section table th{border:1px solid #d0d7de;padding:6px 13px}div#p>svg>foreignObject>section table tr{background-color:#fff;border-top:1px solid #d8dee4}div#p>svg>foreignObject>section table tr:nth-child(2n){background-color:#f6f8fa}div#p>svg>foreignObject>section table img{background-color:transparent}div#p>svg>foreignObject>section img[align=right]{padding-left:20px}div#p>svg>foreignObject>section img[align=left]{padding-right:20px}div#p>svg>foreignObject>section .emoji{background-color:transparent;max-width:none;vertical-align:text-top}div#p>svg>foreignObject>section span.frame,div#p>svg>foreignObject>section span.frame>span{display:block;overflow:hidden}div#p>svg>foreignObject>section span.frame>span{border:1px solid #d0d7de;float:left;margin:13px 0 0;padding:7px;width:auto}div#p>svg>foreignObject>section span.frame span img{display:block;float:left}div#p>svg>foreignObject>section span.frame span span{clear:both;color:#24292f;display:block;padding:5px 0 0}div#p>svg>foreignObject>section span.align-center{clear:both;display:block;overflow:hidden}div#p>svg>foreignObject>section span.align-center>span{display:block;margin:13px auto 0;overflow:hidden;text-align:center}div#p>svg>foreignObject>section span.align-center span img{margin:0 auto;text-align:center}div#p>svg>foreignObject>section span.align-right{clear:both;display:block;overflow:hidden}div#p>svg>foreignObject>section span.align-right>span{display:block;margin:13px 0 0;overflow:hidden;text-align:right}div#p>svg>foreignObject>section span.align-right span img{margin:0;text-align:right}div#p>svg>foreignObject>section span.float-left{display:block;float:left;margin-right:13px;overflow:hidden}div#p>svg>foreignObject>section span.float-left span{margin:13px 0 0}div#p>svg>foreignObject>section span.float-right{display:block;float:right;margin-left:13px;overflow:hidden}div#p>svg>foreignObject>section span.float-right>span{display:block;margin:13px auto 0;overflow:hidden;text-align:right}div#p>svg>foreignObject>section code,div#p>svg>foreignObject>section tt{background-color:rgba(175,184,193,.2);border-radius:6px;font-size:85%;margin:0;padding:.2em .4em}div#p>svg>foreignObject>section code br,div#p>svg>foreignObject>section tt br{display:none}div#p>svg>foreignObject>section del code{text-decoration:inherit}div#p>svg>foreignObject>section pre code{font-size:100%}div#p>svg>foreignObject>section pre>code{background:transparent;border:0;margin:0;padding:0;white-space:pre;word-break:normal}div#p>svg>foreignObject>section .highlight{margin-bottom:16px}div#p>svg>foreignObject>section .highlight pre{margin-bottom:0;word-break:normal}div#p>svg>foreignObject>section pre{background-color:#f6f8fa;border-radius:6px;font-size:85%;line-height:1.45;overflow:auto;padding:16px}div#p>svg>foreignObject>section pre code,div#p>svg>foreignObject>section pre tt{word-wrap:normal;background-color:transparent;border:0;display:inline;line-height:inherit;margin:0;max-width:auto;overflow:visible;padding:0}div#p>svg>foreignObject>section .csv-data td,div#p>svg>foreignObject>section .csv-data th{font-size:12px;line-height:1;overflow:hidden;padding:5px;text-align:left;white-space:nowrap}div#p>svg>foreignObject>section .csv-data .blob-num{background:#fff;border:0;padding:10px 8px 9px;text-align:right}div#p>svg>foreignObject>section .csv-data tr{border-top:0}div#p>svg>foreignObject>section .csv-data th{background:#f6f8fa;border-top:0;font-weight:600}div#p>svg>foreignObject>section .footnotes{border-top:1px solid #d0d7de;color:#57606a;font-size:12px}div#p>svg>foreignObject>section div#p>svg>foreignObject>section section.footnotes{--marpit-root-font-size:12px}div#p>svg>foreignObject>section .footnotes ol{padding-left:16px}div#p>svg>foreignObject>section .footnotes li{position:relative}div#p>svg>foreignObject>section .footnotes li:target:before{border:2px solid #0969da;border-radius:6px;bottom:-8px;content:"";left:-24px;pointer-events:none;position:absolute;right:-8px;top:-8px}div#p>svg>foreignObject>section .footnotes li:target{color:#24292f}div#p>svg>foreignObject>section .footnotes .data-footnote-backref g-emoji{font-family:monospace}div#p>svg>foreignObject>section [hidden]{display:none!important}div#p>svg>foreignObject>section ::-webkit-calendar-picker-indicator{filter:invert(50%)}div#p>svg>foreignObject>section .hljs{background:#fff;color:#333;display:block;overflow-x:auto;padding:.5em}div#p>svg>foreignObject>section .hljs-comment,div#p>svg>foreignObject>section .hljs-meta{color:#969896}div#p>svg>foreignObject>section .hljs-emphasis,div#p>svg>foreignObject>section .hljs-quote,div#p>svg>foreignObject>section .hljs-strong,div#p>svg>foreignObject>section .hljs-template-variable,div#p>svg>foreignObject>section .hljs-variable{color:#df5000}div#p>svg>foreignObject>section .hljs-keyword,div#p>svg>foreignObject>section .hljs-selector-tag,div#p>svg>foreignObject>section .hljs-type{color:#d73a49}div#p>svg>foreignObject>section .hljs-attribute,div#p>svg>foreignObject>section .hljs-bullet,div#p>svg>foreignObject>section .hljs-literal,div#p>svg>foreignObject>section .hljs-symbol{color:#0086b3}div#p>svg>foreignObject>section .hljs-name,div#p>svg>foreignObject>section .hljs-section{color:#63a35c}div#p>svg>foreignObject>section .hljs-tag{color:#333}div#p>svg>foreignObject>section .hljs-attr,div#p>svg>foreignObject>section .hljs-selector-attr,div#p>svg>foreignObject>section .hljs-selector-class,div#p>svg>foreignObject>section .hljs-selector-id,div#p>svg>foreignObject>section .hljs-selector-pseudo,div#p>svg>foreignObject>section .hljs-title{color:#6f42c1}div#p>svg>foreignObject>section .hljs-addition{background-color:#eaffea;color:#55a532}div#p>svg>foreignObject>section .hljs-deletion{background-color:#ffecec;color:#bd2c00}div#p>svg>foreignObject>section .hljs-link{text-decoration:underline}div#p>svg>foreignObject>section .hljs-number{color:#005cc5}div#p>svg>foreignObject>section .hljs-string{color:#032f62}div#p>svg>foreignObject>section svg[data-marp-fitting=svg]{max-height:563px}div#p>svg>foreignObject>section h1{color:#246;font-size:1.6em}div#p>svg>foreignObject>section h1,div#p>svg>foreignObject>section h2{border-bottom:none}div#p>svg>foreignObject>section h2{font-size:1.3em}div#p>svg>foreignObject>section h3{font-size:1.1em}div#p>svg>foreignObject>section h4{font-size:1.05em}div#p>svg>foreignObject>section h5{font-size:1em}div#p>svg>foreignObject>section h6{font-size:.9em}div#p>svg>foreignObject>section h1 strong,div#p>svg>foreignObject>section h2 strong,div#p>svg>foreignObject>section h3 strong,div#p>svg>foreignObject>section h4 strong,div#p>svg>foreignObject>section h5 strong,div#p>svg>foreignObject>section h6 strong{color:#48c;font-weight:inherit}div#p>svg>foreignObject>section hr{height:0;padding-top:.25em}div#p>svg>foreignObject>section pre{border:1px solid #999;line-height:1.15;overflow:visible}div#p>svg>foreignObject>section pre code svg[data-marp-fitting=svg]{max-height:529px}div#p>svg>foreignObject>section footer,div#p>svg>foreignObject>section header{color:hsla(0,0%,40%,.75);font-size:18px;left:30px;margin:0;position:absolute}div#p>svg>foreignObject>section header{top:21px}div#p>svg>foreignObject>section footer{bottom:21px}div#p>svg>foreignObject>section{align-items:stretch;background:#fff;display:flex;flex-flow:column nowrap;font-size:29px;height:720px;justify-content:center;padding:78.5px;width:1280px}div#p>svg>foreignObject>section{--marpit-root-font-size:29px}div#p>svg>foreignObject>section>:last-child,div#p>svg>foreignObject>section[data-footer]>:nth-last-child(2){margin-bottom:0}div#p>svg>foreignObject>section>:first-child,div#p>svg>foreignObject>section>header:first-child+*{margin-top:0}div#p>svg>foreignObject>section:after{bottom:21px;color:#777;font-size:24px;padding:0;position:absolute;right:30px}div#p>svg>foreignObject>section:after{--marpit-root-font-size:24px}div#p>svg>foreignObject>section.invert{background-color:#222;color:#e6eaf0}div#p>svg>foreignObject>section.invert:after{color:#999}div#p>svg>foreignObject>section.invert img{background-color:transparent}div#p>svg>foreignObject>section.invert a{color:#50b3ff}div#p>svg>foreignObject>section.invert h1{color:#a3c5e7}div#p>svg>foreignObject>section.invert h2,div#p>svg>foreignObject>section.invert h3,div#p>svg>foreignObject>section.invert h4,div#p>svg>foreignObject>section.invert h5{color:#ebeff5}div#p>svg>foreignObject>section.invert blockquote,div#p>svg>foreignObject>section.invert h6{border-color:#3d3f43;color:#939699}div#p>svg>foreignObject>section.invert h1 strong,div#p>svg>foreignObject>section.invert h2 strong,div#p>svg>foreignObject>section.invert h3 strong,div#p>svg>foreignObject>section.invert h4 strong,div#p>svg>foreignObject>section.invert h5 strong,div#p>svg>foreignObject>section.invert h6 strong{color:#7bf}div#p>svg>foreignObject>section.invert hr{background-color:#3d3f43}div#p>svg>foreignObject>section.invert footer,div#p>svg>foreignObject>section.invert header{color:hsla(0,0%,60%,.75)}div#p>svg>foreignObject>section.invert code,div#p>svg>foreignObject>section.invert kbd{background-color:#111}div#p>svg>foreignObject>section.invert kbd{border-color:#666;box-shadow:inset 0 -1px 0 #555;color:#e6eaf0}div#p>svg>foreignObject>section.invert table tr{background-color:#12181d;border-color:#60657b}div#p>svg>foreignObject>section.invert table tr:nth-child(2n){background-color:#1b2024}div#p>svg>foreignObject>section.invert table td,div#p>svg>foreignObject>section.invert table th{border-color:#5b5e61}div#p>svg>foreignObject>section.invert pre{background-color:#0a0e12;border-color:#777}div#p>svg>foreignObject>section.invert pre code{background-color:transparent}div#p>svg>foreignObject>section[data-color] h1,div#p>svg>foreignObject>section[data-color] h2,div#p>svg>foreignObject>section[data-color] h3,div#p>svg>foreignObject>section[data-color] h4,div#p>svg>foreignObject>section[data-color] h5,div#p>svg>foreignObject>section[data-color] h6{color:currentColor}div#p>svg>foreignObject>section{width:1280px;height:720px}div#p>svg>foreignObject>section{background-color:#FFFFFF;font-size:28px;color:#4b4b4b;font-family:"Droid Sans Mono","Hiragino Maru Gothic ProN";background-image:url("logo.svg");background-position:right 3% bottom 2%;background-repeat:no-repeat;background-attachment:5%;background-size:20% auto}div#p>svg>foreignObject>section{--marpit-root-font-size:28px}div#p>svg>foreignObject>section.title h1{color:#808db5;text-align:center}div#p>svg>foreignObject>section.title p{bottom:25%;width:100%;position:absolute;font-size:25px;color:#4b4b4b;background:linear-gradient(transparent 90%,#ffcc00 0%)}div#p>svg>foreignObject>section.slide h1{width:95%;color:white;background-color:#808db5;position:absolute;left:50px;top:35px}div#p>svg>foreignObject>section.fig_cg p{top:300px;text-align:center}div#p>svg>foreignObject>section[data-marpit-advanced-background=background]{columns:initial!important;display:block!important;padding:0!important}div#p>svg>foreignObject>section[data-marpit-advanced-background=background]:after,div#p>svg>foreignObject>section[data-marpit-advanced-background=background]:before,div#p>svg>foreignObject>section[data-marpit-advanced-background=content]:after,div#p>svg>foreignObject>section[data-marpit-advanced-background=content]:before{display:none!important}div#p>svg>foreignObject>section[data-marpit-advanced-background=background]>div[data-marpit-advanced-background-container]{all:initial;display:flex;flex-direction:row;height:100%;overflow:hidden;width:100%}div#p>svg>foreignObject>section[data-marpit-advanced-background=background]>div[data-marpit-advanced-background-container][data-marpit-advanced-background-direction=vertical]{flex-direction:column}div#p>svg>foreignObject>section[data-marpit-advanced-background=background][data-marpit-advanced-background-split]>div[data-marpit-advanced-background-container]{width:var(--marpit-advanced-background-split,50%)}div#p>svg>foreignObject>section[data-marpit-advanced-background=background][data-marpit-advanced-background-split=right]>div[data-marpit-advanced-background-container]{margin-left:calc(100% - var(--marpit-advanced-background-split, 50%))}div#p>svg>foreignObject>section[data-marpit-advanced-background=background]>div[data-marpit-advanced-background-container]>figure{all:initial;background-position:center;background-repeat:no-repeat;background-size:cover;flex:auto;margin:0}div#p>svg>foreignObject>section[data-marpit-advanced-background=content],div#p>svg>foreignObject>section[data-marpit-advanced-background=pseudo]{background:transparent!important}div#p>svg>foreignObject>section[data-marpit-advanced-background=pseudo],div#p>svg[data-marpit-svg]>foreignObject[data-marpit-advanced-background=pseudo]{pointer-events:none!important}div#p>svg>foreignObject>section[data-marpit-advanced-background-split]{width:100%;height:100%}</style></head><body><div class="bespoke-marp-osc"><button data-bespoke-marp-osc="prev" tabindex="-1" title="Previous slide">Previous slide</button><span data-bespoke-marp-osc="page"></span><button data-bespoke-marp-osc="next" tabindex="-1" title="Next slide">Next slide</button><button data-bespoke-marp-osc="fullscreen" tabindex="-1" title="Toggle fullscreen (f)">Toggle fullscreen</button><button data-bespoke-marp-osc="presenter" tabindex="-1" title="Open presenter view (p)">Open presenter view</button></div><div id="p"><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="1" data-paginate="true" data-class="title" data-theme="default" data-style="section { background-color: #FFFFFF; font-size: 28px; color: #4b4b4b; @@ -43,7 +43,12 @@ left: 50px; top: 35px; } -" data-heading-divider="1" class="title" data-marpit-pagination="1" data-marpit-pagination-total="26" style="--paginate:true;--class:title;--theme:default;--style:section { + +section.fig_cg p { + top: 300px; + text-align: center; +} +" data-heading-divider="1" class="title" data-marpit-pagination="1" data-marpit-pagination-total="24" style="--paginate:true;--class:title;--theme:default;--style:section { background-color: #FFFFFF; font-size: 28px; color: #4b4b4b; @@ -77,6 +82,11 @@ left: 50px; top: 35px; } + +section.fig_cg p { + top: 300px; + text-align: center; +} ;--heading-divider:1;" data-size="16:9"> <h1>Gears Agda による <br /> Left Learning Red Black Tree の検証</h1> @@ -116,7 +126,12 @@ left: 50px; top: 35px; } -" data-heading-divider="1" class="slide" data-marpit-pagination="2" data-marpit-pagination-total="26" style="--paginate:true;--class:slide;--theme:default;--style:section { + +section.fig_cg p { + top: 300px; + text-align: center; +} +" data-heading-divider="1" class="slide" data-marpit-pagination="2" data-marpit-pagination-total="24" style="--paginate:true;--class:slide;--theme:default;--style:section { background-color: #FFFFFF; font-size: 28px; color: #4b4b4b; @@ -150,6 +165,11 @@ left: 50px; top: 35px; } + +section.fig_cg p { + top: 300px; + text-align: center; +} ;--heading-divider:1;" data-size="16:9"> <h1>証明を用いてプログラムの信頼性の向上を目指す</h1> @@ -202,7 +222,12 @@ left: 50px; top: 35px; } -" data-heading-divider="1" class="slide" data-marpit-pagination="3" data-marpit-pagination-total="26" style="--paginate:true;--class:slide;--theme:default;--style:section { + +section.fig_cg p { + top: 300px; + text-align: center; +} +" data-heading-divider="1" class="slide" data-marpit-pagination="3" data-marpit-pagination-total="24" style="--paginate:true;--class:slide;--theme:default;--style:section { background-color: #FFFFFF; font-size: 28px; color: #4b4b4b; @@ -236,6 +261,11 @@ left: 50px; top: 35px; } + +section.fig_cg p { + top: 300px; + text-align: center; +} ;--heading-divider:1;" data-size="16:9"> <h1>CbC について</h1> <ul> @@ -283,7 +313,12 @@ left: 50px; top: 35px; } -" data-heading-divider="1" class="slide" data-marpit-pagination="4" data-marpit-pagination-total="26" style="--paginate:true;--class:slide;--theme:default;--style:section { + +section.fig_cg p { + top: 300px; + text-align: center; +} +" data-heading-divider="1" class="slide" data-marpit-pagination="4" data-marpit-pagination-total="24" style="--paginate:true;--class:slide;--theme:default;--style:section { background-color: #FFFFFF; font-size: 28px; color: #4b4b4b; @@ -317,6 +352,11 @@ left: 50px; top: 35px; } + +section.fig_cg p { + top: 300px; + text-align: center; +} ;--heading-divider:1;" data-size="16:9"> <h1>Agda の基本</h1> <ul> @@ -378,7 +418,12 @@ left: 50px; top: 35px; } -" data-heading-divider="1" class="slide" data-marpit-pagination="5" data-marpit-pagination-total="26" style="--paginate:true;--class:slide;--theme:default;--style:section { + +section.fig_cg p { + top: 300px; + text-align: center; +} +" data-heading-divider="1" class="slide" data-marpit-pagination="5" data-marpit-pagination-total="24" style="--paginate:true;--class:slide;--theme:default;--style:section { background-color: #FFFFFF; font-size: 28px; color: #4b4b4b; @@ -412,11 +457,16 @@ left: 50px; top: 35px; } + +section.fig_cg p { + top: 300px; + text-align: center; +} ;--heading-divider:1;" data-size="16:9"> <h1>Agda の基本 record</h1> <ul> <li>2つのものが同時に存在すること</li> -<li>Record 型とはオブジェクトあるいは構造体のようなもの</li> +<li>Record 型とはオブジェクトあるいは構造体</li> </ul> <pre><code><svg data-marp-fitting="svg" data-marp-fitting-code><foreignObject><span data-marp-fitting-svg-content><span data-marp-fitting-svg-content-wrap>record Env : Set where field @@ -424,9 +474,12 @@ vari : N open Env </span></span></foreignObject></svg></code></pre> -<p>記述する際の基本的な例を以下に挙げる</p> +<p>型に対応する値の導入(intro)</p> <pre><code><svg data-marp-fitting="svg" data-marp-fitting-code><foreignObject><span data-marp-fitting-svg-content><span data-marp-fitting-svg-content-wrap>record {varx = zero ; vary = suc zero} </span></span></foreignObject></svg></code></pre> +<p>record の値のアクセス(elim)</p> +<pre><code><svg data-marp-fitting="svg" data-marp-fitting-code><foreignObject><span data-marp-fitting-svg-content><span data-marp-fitting-svg-content-wrap>(env : Env) → varx env +</span></span></foreignObject></svg></code></pre> </section> </foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="6" data-paginate="true" data-class="slide" data-theme="default" data-style="section { background-color: #FFFFFF; @@ -462,7 +515,12 @@ left: 50px; top: 35px; } -" data-heading-divider="1" class="slide" data-marpit-pagination="6" data-marpit-pagination-total="26" style="--paginate:true;--class:slide;--theme:default;--style:section { + +section.fig_cg p { + top: 300px; + text-align: center; +} +" data-heading-divider="1" class="slide" data-marpit-pagination="6" data-marpit-pagination-total="24" style="--paginate:true;--class:slide;--theme:default;--style:section { background-color: #FFFFFF; font-size: 28px; color: #4b4b4b; @@ -496,6 +554,11 @@ left: 50px; top: 35px; } + +section.fig_cg p { + top: 300px; + text-align: center; +} ;--heading-divider:1;" data-size="16:9"> <h1>Agda の基本 data</h1> <ul> @@ -546,7 +609,12 @@ left: 50px; top: 35px; } -" data-heading-divider="1" class="slide" data-marpit-pagination="7" data-marpit-pagination-total="26" style="--paginate:true;--class:slide;--theme:default;--style:section { + +section.fig_cg p { + top: 300px; + text-align: center; +} +" data-heading-divider="1" class="slide" data-marpit-pagination="7" data-marpit-pagination-total="24" style="--paginate:true;--class:slide;--theme:default;--style:section { background-color: #FFFFFF; font-size: 28px; color: #4b4b4b; @@ -580,6 +648,11 @@ left: 50px; top: 35px; } + +section.fig_cg p { + top: 300px; + text-align: center; +} ;--heading-divider:1;" data-size="16:9"> <h1>Agda の基本 短縮記法</h1> <ul> @@ -637,7 +710,12 @@ left: 50px; top: 35px; } -" data-heading-divider="1" class="slide" data-marpit-pagination="8" data-marpit-pagination-total="26" style="--paginate:true;--class:slide;--theme:default;--style:section { + +section.fig_cg p { + top: 300px; + text-align: center; +} +" data-heading-divider="1" class="slide" data-marpit-pagination="8" data-marpit-pagination-total="24" style="--paginate:true;--class:slide;--theme:default;--style:section { background-color: #FFFFFF; font-size: 28px; color: #4b4b4b; @@ -671,6 +749,11 @@ left: 50px; top: 35px; } + +section.fig_cg p { + top: 300px; + text-align: center; +} ;--heading-divider:1;" data-size="16:9"> <h1>Gears Agda の記法</h1> <ul> @@ -723,7 +806,12 @@ left: 50px; top: 35px; } -" data-heading-divider="1" class="slide" data-marpit-pagination="9" data-marpit-pagination-total="26" style="--paginate:true;--class:slide;--theme:default;--style:section { + +section.fig_cg p { + top: 300px; + text-align: center; +} +" data-heading-divider="1" class="slide" data-marpit-pagination="9" data-marpit-pagination-total="24" style="--paginate:true;--class:slide;--theme:default;--style:section { background-color: #FFFFFF; font-size: 28px; color: #4b4b4b; @@ -757,6 +845,11 @@ left: 50px; top: 35px; } + +section.fig_cg p { + top: 300px; + text-align: center; +} ;--heading-divider:1;" data-size="16:9"> <h1>Gears Agda と Gears CbC の対応 x</h1> <ul> @@ -771,7 +864,7 @@ </li> </ul> </section> -</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="10" data-paginate="true" data-class="slide" data-theme="default" data-style="section { +</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="10" data-paginate="true" data-class="fig_cg" data-theme="default" data-style="section { background-color: #FFFFFF; font-size: 28px; color: #4b4b4b; @@ -805,7 +898,12 @@ left: 50px; top: 35px; } -" data-heading-divider="1" class="slide" data-marpit-pagination="10" data-marpit-pagination-total="26" style="--paginate:true;--class:slide;--theme:default;--style:section { + +section.fig_cg p { + top: 300px; + text-align: center; +} +" data-heading-divider="1" class="fig_cg" data-marpit-pagination="10" data-marpit-pagination-total="24" style="--paginate:true;--class:fig_cg;--theme:default;--style:section { background-color: #FFFFFF; font-size: 28px; color: #4b4b4b; @@ -839,13 +937,17 @@ left: 50px; top: 35px; } + +section.fig_cg p { + top: 300px; + text-align: center; +} ;--heading-divider:1;" data-size="16:9"> <h1>Normal level と Meta Level を用いた信頼性の向上</h1> -<p>CbCのプログラムの実行部分は以下の2つから構成される</p> <ul> +<li>CbCのプログラムの実行部分は以下の2つから構成される</li> <li>Normal Level は軽量継続で関数型プログラミングとなる <ul> -<li>atomicってなんだろう</li> <li>ポインタの操作はここでは行わず Meta Level にて行う</li> </ul> </li> @@ -859,6 +961,8 @@ </ul> </li> </ul> + +<p><img src="meta_cg_dg.svg" alt="" style="height:500px;" /></p> </section> </foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="11" data-paginate="true" data-class="slide" data-theme="default" data-style="section { background-color: #FFFFFF; @@ -894,7 +998,12 @@ left: 50px; top: 35px; } -" data-heading-divider="1" class="slide" data-marpit-pagination="11" data-marpit-pagination-total="26" style="--paginate:true;--class:slide;--theme:default;--style:section { + +section.fig_cg p { + top: 300px; + text-align: center; +} +" data-heading-divider="1" class="slide" data-marpit-pagination="11" data-marpit-pagination-total="24" style="--paginate:true;--class:slide;--theme:default;--style:section { background-color: #FFFFFF; font-size: 28px; color: #4b4b4b; @@ -928,9 +1037,30 @@ left: 50px; top: 35px; } + +section.fig_cg p { + top: 300px; + text-align: center; +} ;--heading-divider:1;" data-size="16:9"> -<h1>s</h1> -<div src="meta-cg-dg.pdf"> </div> +<h1>Gears Agda と Hoare Logic</h1> + +<p>C.A.R Hoare, R.W Floyd が考案</p> +<ul> +<li>Pre Condition → Command → Post Condition</li> +</ul> +<p>Gears Agda による Command の例</p> +<pre><code><svg data-marp-fitting="svg" data-marp-fitting-code><foreignObject><span data-marp-fitting-svg-content><span data-marp-fitting-svg-content-wrap>{-# TERMINATING #-} +whileLoop : {l : Level} {t : Set l} → Env → (Code : Env → t) → t +whileLoop env next with lt 0 (varn env) +whileLoop env next | false = next env +whileLoop env next | true = whileLoop (record {varn = (varn env) - 1 ; vari = (vari env) + 1}) next +</span></span></foreignObject></svg></code></pre> +<ul> +<li><code>{-# TERMINATING #-}</code></li> +<li>with 文</li> +<li>型と値</li> +</ul> </section> </foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="12" data-paginate="true" data-class="slide" data-theme="default" data-style="section { background-color: #FFFFFF; @@ -966,7 +1096,12 @@ left: 50px; top: 35px; } -" data-heading-divider="1" class="slide" data-marpit-pagination="12" data-marpit-pagination-total="26" style="--paginate:true;--class:slide;--theme:default;--style:section { + +section.fig_cg p { + top: 300px; + text-align: center; +} +" data-heading-divider="1" class="slide" data-marpit-pagination="12" data-marpit-pagination-total="24" style="--paginate:true;--class:slide;--theme:default;--style:section { background-color: #FFFFFF; font-size: 28px; color: #4b4b4b; @@ -1000,19 +1135,32 @@ left: 50px; top: 35px; } + +section.fig_cg p { + top: 300px; + text-align: center; +} ;--heading-divider:1;" data-size="16:9"> -<h1>Hoare Logic について</h1> +<h1>Gears Agda による検証の例（検証付き実装）</h1> <ul> -<li>Hoare Logic とは C.A.R Hoare, R.W Floyd が考案したプログラムの検証の手法</li> -<li>「プログラムの事前条件 (P) が成立しているときコマンド (C) 実行して停止すると事後条件 (Q) が成り立つ」というもの +<li>先ほど実装した while program に対して証明を付ける</li> +<li>loop を接続する Meta Gear も用意する</li> +</ul> +<pre><code><svg data-marp-fitting="svg" data-marp-fitting-code><foreignObject><span data-marp-fitting-svg-content><span data-marp-fitting-svg-content-wrap>TerminatingLoopS : {l : Level} {t : Set l} ( Index : Set ) + → {Invraiant : Index → Set } → ( reduce : Index → N) + → (loop : (r : Index) → Invraiant r + → (next : (r1 : Index) → Invraiant r1 → reduce r1 < reduce r → t ) → t) + → (r : Index) → (p : Invraiant r) → t +</span></span></foreignObject></svg></code></pre> <ul> -<li>CbC の実行を継続するという性質に非常に相性が良い</li> +<li>入力として仕様の証明を受け取る</li> +<li>出力として次の関数に仕様の証明を渡す</li> +<li>Hoare Conditionがプログラムの開始から停止するまで接続されていれば証明は完成 +<ul> +<li>Meta Gear にて証明を値としてあたえているため</li> </ul> </li> </ul> -<p>pre/post condition を Gears Agda では Meta Input Data Gear として<br /> -プログラム中に遷移させていくことで、プログラムが終始仕様に沿った動きをしている<br /> -ことを検証する</p> </section> </foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="13" data-paginate="true" data-class="slide" data-theme="default" data-style="section { background-color: #FFFFFF; @@ -1048,7 +1196,12 @@ left: 50px; top: 35px; } -" data-heading-divider="1" class="slide" data-marpit-pagination="13" data-marpit-pagination-total="26" style="--paginate:true;--class:slide;--theme:default;--style:section { + +section.fig_cg p { + top: 300px; + text-align: center; +} +" data-heading-divider="1" class="slide" data-marpit-pagination="13" data-marpit-pagination-total="24" style="--paginate:true;--class:slide;--theme:default;--style:section { background-color: #FFFFFF; font-size: 28px; color: #4b4b4b; @@ -1082,21 +1235,25 @@ left: 50px; top: 35px; } + +section.fig_cg p { + top: 300px; + text-align: center; +} ;--heading-divider:1;" data-size="16:9"> -<h1>Gears Agda による検証の例（実装）</h1> +<h1>test との違い</h1> <ul> -<li>while program の検証を例に挙げる +<li>test では実数を与えた際の出力が仕様に沿ったものであるかを検証する <ul> -<li>以下は実装部分のコードとなる</li> +<li>コーナーケースで仕様に沿った動きをしていない場合を考慮できない</li> +</ul> +</li> +<li>今回の定理証明を用いた証明では実数を必要としない +<ul> +<li>そのため、入力の型の範囲全てに対して仕様を満たしているか検証できる</li> </ul> </li> </ul> -<pre><code><svg data-marp-fitting="svg" data-marp-fitting-code><foreignObject><span data-marp-fitting-svg-content><span data-marp-fitting-svg-content-wrap>{-# TERMINATING #-} -whileLoop : {l : Level} {t : Set l} → Env → (Code : Env → t) → t -whileLoop env next with lt 0 (varn env) -whileLoop env next | false = next env -whileLoop env next | true = whileLoop (record {varn = (varn env) - 1 ; vari = (vari env) + 1}) next -</span></span></foreignObject></svg></code></pre> </section> </foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="14" data-paginate="true" data-class="slide" data-theme="default" data-style="section { background-color: #FFFFFF; @@ -1132,7 +1289,12 @@ left: 50px; top: 35px; } -" data-heading-divider="1" class="slide" data-marpit-pagination="14" data-marpit-pagination-total="26" style="--paginate:true;--class:slide;--theme:default;--style:section { + +section.fig_cg p { + top: 300px; + text-align: center; +} +" data-heading-divider="1" class="slide" data-marpit-pagination="14" data-marpit-pagination-total="24" style="--paginate:true;--class:slide;--theme:default;--style:section { background-color: #FFFFFF; font-size: 28px; color: #4b4b4b; @@ -1166,26 +1328,22 @@ left: 50px; top: 35px; } + +section.fig_cg p { + top: 300px; + text-align: center; +} ;--heading-divider:1;" data-size="16:9"> -<h1>Gears Agda による検証の例（検証付き実装）</h1> +<h1>Gears Agda による BinaryTree の実装</h1> <ul> -<li>先ほど実装した while program に対して証明を付ける</li> -<li>loop を接続する Meta Gear も用意する</li> -</ul> -<pre><code><svg data-marp-fitting="svg" data-marp-fitting-code><foreignObject><span data-marp-fitting-svg-content><span data-marp-fitting-svg-content-wrap>TerminatingLoopS : {l : Level} {t : Set l} ( Index : Set ) - → {Invraiant : Index → Set } → ( reduce : Index → N) - → (loop : (r : Index) → Invraiant r - → (next : (r1 : Index) → Invraiant r1 → reduce r1 < reduce r → t ) → t) - → (r : Index) → (p : Invraiant r) → t -</span></span></foreignObject></svg></code></pre> +<li>Agdaが変数への再代入を許していないためそのままでは木構造を実装できない <ul> -<li>入力として仕様の証明を受け取る</li> -<li>出力として次の関数に仕様の証明を渡す</li> -<li>Hoare Conditionがプログラムの開始から停止するまで接続されていれば証明は完成 -<ul> -<li>Meta Gear にて証明を値としてあたえているため</li> +<li>木構造を辿る際に現在いるノード以下の木構造をそのまま stack に格納する</li> +<li>replace / delete などの操作を行った後に stack を参照し Tree を再構築する</li> +<li>CbCへの変換の時に問題になりそうな予感</li> </ul> </li> +<li>ここの説明いらないかも？</li> </ul> </section> </foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="15" data-paginate="true" data-class="slide" data-theme="default" data-style="section { @@ -1222,7 +1380,12 @@ left: 50px; top: 35px; } -" data-heading-divider="1" class="slide" data-marpit-pagination="15" data-marpit-pagination-total="26" style="--paginate:true;--class:slide;--theme:default;--style:section { + +section.fig_cg p { + top: 300px; + text-align: center; +} +" data-heading-divider="1" class="slide" data-marpit-pagination="15" data-marpit-pagination-total="24" style="--paginate:true;--class:slide;--theme:default;--style:section { background-color: #FFFFFF; font-size: 28px; color: #4b4b4b; @@ -1256,20 +1419,21 @@ left: 50px; top: 35px; } + +section.fig_cg p { + top: 300px; + text-align: center; +} ;--heading-divider:1;" data-size="16:9"> -<h1>test との違い</h1> -<ul> -<li>test では実数を与えた際の出力が仕様に沿ったものであるかを検証する -<ul> -<li>コーナーケースで仕様に沿った動きをしていない場合を考慮できない</li> -</ul> -</li> -<li>今回の定理証明を用いた証明では実数を必要としない -<ul> -<li>そのため、入力の型の範囲全てに対して仕様を満たしているか検証できる</li> -</ul> -</li> -</ul> +<h1>Gears Agda による BinaryTree の実装 find node</h1> +<pre><code><svg data-marp-fitting="svg" data-marp-fitting-code><foreignObject><span data-marp-fitting-svg-content><span data-marp-fitting-svg-content-wrap>find : {n m : Level} {A : Set n} {t : Set m} → (env : Env A ) + → (next : (env : Env A ) → t ) → (exit : (env : Env A ) → t ) → t +find key leaf st _ exit = exit leaf st +find key (node key₁ v1 tree tree₁) st next exit with <-cmp key key₁ +find key n st _ exit | tri≈ ¬a b ¬c = exit n st +find key n@(node key₁ v1 tree tree₁) st next _ | tri< a ¬b ¬c = next tree (n ∷ st) +find key n@(node key₁ v1 tree tree₁) st next _ | tri> ¬a ¬b c = next tree₁ (n ∷ st) +</span></span></foreignObject></svg></code></pre> </section> </foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="16" data-paginate="true" data-class="slide" data-theme="default" data-style="section { background-color: #FFFFFF; @@ -1305,7 +1469,12 @@ left: 50px; top: 35px; } -" data-heading-divider="1" class="slide" data-marpit-pagination="16" data-marpit-pagination-total="26" style="--paginate:true;--class:slide;--theme:default;--style:section { + +section.fig_cg p { + top: 300px; + text-align: center; +} +" data-heading-divider="1" class="slide" data-marpit-pagination="16" data-marpit-pagination-total="24" style="--paginate:true;--class:slide;--theme:default;--style:section { background-color: #FFFFFF; font-size: 28px; color: #4b4b4b; @@ -1339,18 +1508,29 @@ left: 50px; top: 35px; } + +section.fig_cg p { + top: 300px; + text-align: center; +} ;--heading-divider:1;" data-size="16:9"> -<h1>Gears Agda による BinaryTree の実装</h1> -<ul> -<li>Agdaが変数への再代入を許していないためそのままでは木構造を実装できない -<ul> -<li>木構造を辿る際に現在いるノード以下の木構造をそのまま stack に格納する</li> -<li>replace / delete などの操作を行った後に stack を参照し Tree を再構築する</li> -<li>CbCへの変換の時に問題になりそうな予感</li> -</ul> -</li> -<li>ここの説明いらないかも？</li> -</ul> +<h1>Gears Agda による BinaryTree の実装 replace node</h1> +<pre><code><svg data-marp-fitting="svg" data-marp-fitting-code><foreignObject><span data-marp-fitting-svg-content><span data-marp-fitting-svg-content-wrap>replace : {n m : Level} {A : Set n} {t : Set m} + → (key : N) → (value : A) → bt A → List (bt A) + → (next : N → A → bt A → List (bt A) → t ) + → (exit : bt A → t) → t +replace key value repl [] next exit = exit repl -- can't happen +replace key value repl (leaf ∷ []) next exit = exit repl +replace key value repl (node key₁ value₁ left right ∷ []) next exit with <-cmp key key₁ +... | tri< a ¬b ¬c = exit (node key₁ value₁ repl right ) +... | tri≈ ¬a b ¬c = exit (node key₁ value left right ) +... | tri> ¬a ¬b c = exit (node key₁ value₁ left repl ) +replace key value repl (leaf ∷ st) next exit = next key value repl st +replace key value repl (node key₁ value₁ left right ∷ st) next exit with <-cmp key key₁ +... | tri< a ¬b ¬c = next key value (node key₁ value₁ repl right ) st +... | tri≈ ¬a b ¬c = next key value (node key₁ value left right ) st +... | tri> ¬a ¬b c = next key value (node key₁ value₁ left repl ) st +</span></span></foreignObject></svg></code></pre> </section> </foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="17" data-paginate="true" data-class="slide" data-theme="default" data-style="section { background-color: #FFFFFF; @@ -1386,7 +1566,12 @@ left: 50px; top: 35px; } -" data-heading-divider="1" class="slide" data-marpit-pagination="17" data-marpit-pagination-total="26" style="--paginate:true;--class:slide;--theme:default;--style:section { + +section.fig_cg p { + top: 300px; + text-align: center; +} +" data-heading-divider="1" class="slide" data-marpit-pagination="17" data-marpit-pagination-total="24" style="--paginate:true;--class:slide;--theme:default;--style:section { background-color: #FFFFFF; font-size: 28px; color: #4b4b4b; @@ -1420,15 +1605,14 @@ left: 50px; top: 35px; } + +section.fig_cg p { + top: 300px; + text-align: center; +} ;--heading-divider:1;" data-size="16:9"> -<h1>Gears Agda による BinaryTree の実装 find node</h1> -<pre><code><svg data-marp-fitting="svg" data-marp-fitting-code><foreignObject><span data-marp-fitting-svg-content><span data-marp-fitting-svg-content-wrap>find : {n m : Level} {A : Set n} {t : Set m} → (env : Env A ) - → (next : (env : Env A ) → t ) → (exit : (env : Env A ) → t ) → t -find key leaf st _ exit = exit leaf st -find key (node key₁ v1 tree tree₁) st next exit with <-cmp key key₁ -find key n st _ exit | tri≈ ¬a b ¬c = exit n st -find key n@(node key₁ v1 tree tree₁) st next _ | tri< a ¬b ¬c = next tree (n ∷ st) -find key n@(node key₁ v1 tree tree₁) st next _ | tri> ¬a ¬b c = next tree₁ (n ∷ st) +<h1>Gears Agda による BinaryTree の実装 loop connecter</h1> +<pre><code><svg data-marp-fitting="svg" data-marp-fitting-code><foreignObject><span data-marp-fitting-svg-content><span data-marp-fitting-svg-content-wrap> </span></span></foreignObject></svg></code></pre> </section> </foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="18" data-paginate="true" data-class="slide" data-theme="default" data-style="section { @@ -1465,7 +1649,12 @@ left: 50px; top: 35px; } -" data-heading-divider="1" class="slide" data-marpit-pagination="18" data-marpit-pagination-total="26" style="--paginate:true;--class:slide;--theme:default;--style:section { + +section.fig_cg p { + top: 300px; + text-align: center; +} +" data-heading-divider="1" class="slide" data-marpit-pagination="18" data-marpit-pagination-total="24" style="--paginate:true;--class:slide;--theme:default;--style:section { background-color: #FFFFFF; font-size: 28px; color: #4b4b4b; @@ -1499,24 +1688,20 @@ left: 50px; top: 35px; } + +section.fig_cg p { + top: 300px; + text-align: center; +} ;--heading-divider:1;" data-size="16:9"> -<h1>Gears Agda による BinaryTree の実装 replace node</h1> -<pre><code><svg data-marp-fitting="svg" data-marp-fitting-code><foreignObject><span data-marp-fitting-svg-content><span data-marp-fitting-svg-content-wrap>replace : {n m : Level} {A : Set n} {t : Set m} - → (key : N) → (value : A) → bt A → List (bt A) - → (next : N → A → bt A → List (bt A) → t ) - → (exit : bt A → t) → t -replace key value repl [] next exit = exit repl -- can't happen -replace key value repl (leaf ∷ []) next exit = exit repl -replace key value repl (node key₁ value₁ left right ∷ []) next exit with <-cmp key key₁ -... | tri< a ¬b ¬c = exit (node key₁ value₁ repl right ) -... | tri≈ ¬a b ¬c = exit (node key₁ value left right ) -... | tri> ¬a ¬b c = exit (node key₁ value₁ left repl ) -replace key value repl (leaf ∷ st) next exit = next key value repl st -replace key value repl (node key₁ value₁ left right ∷ st) next exit with <-cmp key key₁ -... | tri< a ¬b ¬c = next key value (node key₁ value₁ repl right ) st -... | tri≈ ¬a b ¬c = next key value (node key₁ value left right ) st -... | tri> ¬a ¬b c = next key value (node key₁ value₁ left repl ) st -</span></span></foreignObject></svg></code></pre> +<h1>Gears Agda による Binary Tree の検証 Invariant</h1> +<p>具体的な例を一つ挙げて、Invariantの説明を行う</p> +<ul> +<li>Binary Tree の性質である、左の子のkeyは親より小さく、<br /> +右の子のkeyは親より大きいことを検証</li> +<li>Stack に格納されているTreeはその次のStackの減少列になっているか</li> +<li>Tree を正しく入れ替えられているか</li> +</ul> </section> </foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="19" data-paginate="true" data-class="slide" data-theme="default" data-style="section { background-color: #FFFFFF; @@ -1552,7 +1737,12 @@ left: 50px; top: 35px; } -" data-heading-divider="1" class="slide" data-marpit-pagination="19" data-marpit-pagination-total="26" style="--paginate:true;--class:slide;--theme:default;--style:section { + +section.fig_cg p { + top: 300px; + text-align: center; +} +" data-heading-divider="1" class="slide" data-marpit-pagination="19" data-marpit-pagination-total="24" style="--paginate:true;--class:slide;--theme:default;--style:section { background-color: #FFFFFF; font-size: 28px; color: #4b4b4b; @@ -1586,9 +1776,30 @@ left: 50px; top: 35px; } + +section.fig_cg p { + top: 300px; + text-align: center; +} ;--heading-divider:1;" data-size="16:9"> -<h1>Gears Agda による BinaryTree の実装 loop connecter</h1> -<pre><code><svg data-marp-fitting="svg" data-marp-fitting-code><foreignObject><span data-marp-fitting-svg-content><span data-marp-fitting-svg-content-wrap> +<h1>Gears Agda による Binary Tree の検証 Invariant</h1> +<ul> +<li>Tree Invariant</li> +</ul> +<pre><code><svg data-marp-fitting="svg" data-marp-fitting-code><foreignObject><span data-marp-fitting-svg-content><span data-marp-fitting-svg-content-wrap>data treeInvariant {n : Level} {A : Set n} : (tree : bt A) → Set n where + t-leaf : treeInvariant leaf + t-single : (key : N) → (value : A) → treeInvariant (node key value leaf leaf) + t-right : {key key₁ : N} → {value value₁ : A} → {t₁ t₂ : bt A} → (key < key₁) + → treeInvariant (node key₁ value₁ t₁ t₂) + → treeInvariant (node key value leaf (node key₁ value₁ t₁ t₂)) + t-left : {key key₁ : N} → {value value₁ : A} → {t₁ t₂ : bt A} → (key < key₁) + → treeInvariant (node key value t₁ t₂) + → treeInvariant (node key₁ value₁ (node key value t₁ t₂) leaf ) + t-node : {key key₁ key₂ : N} → {value value₁ value₂ : A} + → {t₁ t₂ t₃ t₄ : bt A} → (key < key₁) → (key₁ < key₂) + → treeInvariant (node key value t₁ t₂) + → treeInvariant (node key₂ value₂ t₃ t₄) + → treeInvariant (node key₁ value₁ (node key value t₁ t₂) (node key₂ value₂ t₃ t₄)) </span></span></foreignObject></svg></code></pre> </section> </foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="20" data-paginate="true" data-class="slide" data-theme="default" data-style="section { @@ -1625,7 +1836,12 @@ left: 50px; top: 35px; } -" data-heading-divider="1" class="slide" data-marpit-pagination="20" data-marpit-pagination-total="26" style="--paginate:true;--class:slide;--theme:default;--style:section { + +section.fig_cg p { + top: 300px; + text-align: center; +} +" data-heading-divider="1" class="slide" data-marpit-pagination="20" data-marpit-pagination-total="24" style="--paginate:true;--class:slide;--theme:default;--style:section { background-color: #FFFFFF; font-size: 28px; color: #4b4b4b; @@ -1659,15 +1875,26 @@ left: 50px; top: 35px; } + +section.fig_cg p { + top: 300px; + text-align: center; +} ;--heading-divider:1;" data-size="16:9"> <h1>Gears Agda による Binary Tree の検証 Invariant</h1> -<p>具体的な例を一つ挙げて、Invariantの説明を行う</p> <ul> -<li>Binary Tree の性質である、左の子のkeyは親より小さく、<br /> -右の子のkeyは親より大きいことを検証</li> -<li>Stack に格納されているTreeはその次のStackの減少列になっているか</li> -<li>Tree を正しく入れ替えられているか</li> +<li>Stack Invariant</li> </ul> +<pre><code><svg data-marp-fitting="svg" data-marp-fitting-code><foreignObject><span data-marp-fitting-svg-content><span data-marp-fitting-svg-content-wrap>data stackInvariant {n : Level} {A : Set n} (key : N) : (top orig : bt A) + → (stack : List (bt A)) → Set n where + s-single : {tree0 : bt A} → stackInvariant key tree0 tree0 (tree0 ∷ []) + s-right : {tree tree0 tree₁ : bt A} → {key₁ : N } → {v1 : A } → {st : List (bt A)} + → key₁ < key → stackInvariant key (node key₁ v1 tree₁ tree) tree0 st + → stackInvariant key tree tree0 (tree ∷ st) + s-left : {tree₁ tree0 tree : bt A} → {key₁ : N } → {v1 : A } → {st : List (bt A)} + → key < key₁ → stackInvariant key (node key₁ v1 tree₁ tree) tree0 st + → stackInvariant key tree₁ tree0 (tree₁ ∷ st) +</span></span></foreignObject></svg></code></pre> </section> </foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="21" data-paginate="true" data-class="slide" data-theme="default" data-style="section { background-color: #FFFFFF; @@ -1703,7 +1930,12 @@ left: 50px; top: 35px; } -" data-heading-divider="1" class="slide" data-marpit-pagination="21" data-marpit-pagination-total="26" style="--paginate:true;--class:slide;--theme:default;--style:section { + +section.fig_cg p { + top: 300px; + text-align: center; +} +" data-heading-divider="1" class="slide" data-marpit-pagination="21" data-marpit-pagination-total="24" style="--paginate:true;--class:slide;--theme:default;--style:section { background-color: #FFFFFF; font-size: 28px; color: #4b4b4b; @@ -1737,25 +1969,26 @@ left: 50px; top: 35px; } + +section.fig_cg p { + top: 300px; + text-align: center; +} ;--heading-divider:1;" data-size="16:9"> <h1>Gears Agda による Binary Tree の検証 Invariant</h1> <ul> -<li>Tree Invariant</li> +<li>Replace Invariant</li> </ul> -<pre><code><svg data-marp-fitting="svg" data-marp-fitting-code><foreignObject><span data-marp-fitting-svg-content><span data-marp-fitting-svg-content-wrap>data treeInvariant {n : Level} {A : Set n} : (tree : bt A) → Set n where - t-leaf : treeInvariant leaf - t-single : (key : N) → (value : A) → treeInvariant (node key value leaf leaf) - t-right : {key key₁ : N} → {value value₁ : A} → {t₁ t₂ : bt A} → (key < key₁) - → treeInvariant (node key₁ value₁ t₁ t₂) - → treeInvariant (node key value leaf (node key₁ value₁ t₁ t₂)) - t-left : {key key₁ : N} → {value value₁ : A} → {t₁ t₂ : bt A} → (key < key₁) - → treeInvariant (node key value t₁ t₂) - → treeInvariant (node key₁ value₁ (node key value t₁ t₂) leaf ) - t-node : {key key₁ key₂ : N} → {value value₁ value₂ : A} - → {t₁ t₂ t₃ t₄ : bt A} → (key < key₁) → (key₁ < key₂) - → treeInvariant (node key value t₁ t₂) - → treeInvariant (node key₂ value₂ t₃ t₄) - → treeInvariant (node key₁ value₁ (node key value t₁ t₂) (node key₂ value₂ t₃ t₄)) +<pre><code><svg data-marp-fitting="svg" data-marp-fitting-code><foreignObject><span data-marp-fitting-svg-content><span data-marp-fitting-svg-content-wrap>data replacedTree {n : Level} {A : Set n} (key : N) (value : A) : (before after : bt A) → Set n where + r-leaf : replacedTree key value leaf (node key value leaf leaf) + r-node : {value₁ : A} → {t t₁ : bt A} + → replacedTree key value (node key value₁ t t₁) (node key value t t₁) + r-right : {k : N } {v1 : A} → {t t1 t2 : bt A} + → k < key → replacedTree key value t2 t + → replacedTree key value (node k v1 t1 t2) (node k v1 t1 t) + r-left : {k : N } {v1 : A} → {t t1 t2 : bt A} + → key < k → replacedTree key value t1 t + → replacedTree key value (node k v1 t1 t2) (node k v1 t t2) </span></span></foreignObject></svg></code></pre> </section> </foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="22" data-paginate="true" data-class="slide" data-theme="default" data-style="section { @@ -1792,7 +2025,12 @@ left: 50px; top: 35px; } -" data-heading-divider="1" class="slide" data-marpit-pagination="22" data-marpit-pagination-total="26" style="--paginate:true;--class:slide;--theme:default;--style:section { + +section.fig_cg p { + top: 300px; + text-align: center; +} +" data-heading-divider="1" class="slide" data-marpit-pagination="22" data-marpit-pagination-total="24" style="--paginate:true;--class:slide;--theme:default;--style:section { background-color: #FFFFFF; font-size: 28px; color: #4b4b4b; @@ -1826,20 +2064,18 @@ left: 50px; top: 35px; } + +section.fig_cg p { + top: 300px; + text-align: center; +} ;--heading-divider:1;" data-size="16:9"> -<h1>Gears Agda による Binary Tree の検証 Invariant</h1> -<ul> -<li>Stack Invariant</li> -</ul> -<pre><code><svg data-marp-fitting="svg" data-marp-fitting-code><foreignObject><span data-marp-fitting-svg-content><span data-marp-fitting-svg-content-wrap>data stackInvariant {n : Level} {A : Set n} (key : N) : (top orig : bt A) - → (stack : List (bt A)) → Set n where - s-single : {tree0 : bt A} → stackInvariant key tree0 tree0 (tree0 ∷ []) - s-right : {tree tree0 tree₁ : bt A} → {key₁ : N } → {v1 : A } → {st : List (bt A)} - → key₁ < key → stackInvariant key (node key₁ v1 tree₁ tree) tree0 st - → stackInvariant key tree tree0 (tree ∷ st) - s-left : {tree₁ tree0 tree : bt A} → {key₁ : N } → {v1 : A } → {st : List (bt A)} - → key < key₁ → stackInvariant key (node key₁ v1 tree₁ tree) tree0 st - → stackInvariant key tree₁ tree0 (tree₁ ∷ st) +<h1>Gears Agda による Binary Tree の検証</h1> +<p>Binary Tree の実装に対して上述した3つのInvariantを<br /> +Meta Data Gear として渡しながら実行できるように記述する</p> +<pre><code><svg data-marp-fitting="svg" data-marp-fitting-code><foreignObject><span data-marp-fitting-svg-content><span data-marp-fitting-svg-content-wrap>findP : {n m : Level} {A : Set n} {t : Set m} → (env : Env A) + → treeInvariant env ∧ stackInvariant env + → (exit : (env : Env A) → treeInvariant env ∧ stackInvariant env → t ) → t </span></span></foreignObject></svg></code></pre> </section> </foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="23" data-paginate="true" data-class="slide" data-theme="default" data-style="section { @@ -1876,7 +2112,12 @@ left: 50px; top: 35px; } -" data-heading-divider="1" class="slide" data-marpit-pagination="23" data-marpit-pagination-total="26" style="--paginate:true;--class:slide;--theme:default;--style:section { + +section.fig_cg p { + top: 300px; + text-align: center; +} +" data-heading-divider="1" class="slide" data-marpit-pagination="23" data-marpit-pagination-total="24" style="--paginate:true;--class:slide;--theme:default;--style:section { background-color: #FFFFFF; font-size: 28px; color: #4b4b4b; @@ -1910,22 +2151,19 @@ left: 50px; top: 35px; } + +section.fig_cg p { + top: 300px; + text-align: center; +} ;--heading-divider:1;" data-size="16:9"> -<h1>Gears Agda による Binary Tree の検証 Invariant</h1> +<h1>今後の研究方針</h1> <ul> -<li>Replace Invariant</li> +<li>現在は Binary Tree の検証までしか行えていないが、<br /> +今回定義した条件はそのまま Red Black Tree の検証に使用できるはず</li> +<li>今後は Gears Agda による実装と条件の追加をおこなう</li> +<li>モデル検査</li> </ul> -<pre><code><svg data-marp-fitting="svg" data-marp-fitting-code><foreignObject><span data-marp-fitting-svg-content><span data-marp-fitting-svg-content-wrap>data replacedTree {n : Level} {A : Set n} (key : N) (value : A) : (before after : bt A) → Set n where - r-leaf : replacedTree key value leaf (node key value leaf leaf) - r-node : {value₁ : A} → {t t₁ : bt A} - → replacedTree key value (node key value₁ t t₁) (node key value t t₁) - r-right : {k : N } {v1 : A} → {t t1 t2 : bt A} - → k < key → replacedTree key value t2 t - → replacedTree key value (node k v1 t1 t2) (node k v1 t1 t) - r-left : {k : N } {v1 : A} → {t t1 t2 : bt A} - → key < k → replacedTree key value t1 t - → replacedTree key value (node k v1 t1 t2) (node k v1 t t2) -</span></span></foreignObject></svg></code></pre> </section> </foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="24" data-paginate="true" data-class="slide" data-theme="default" data-style="section { background-color: #FFFFFF; @@ -1961,50 +2199,12 @@ left: 50px; top: 35px; } -" data-heading-divider="1" class="slide" data-marpit-pagination="24" data-marpit-pagination-total="26" style="--paginate:true;--class:slide;--theme:default;--style:section { - background-color: #FFFFFF; - font-size: 28px; - color: #4b4b4b; - font-family: "Droid Sans Mono", "Hiragino Maru Gothic ProN"; - background-image: url("logo.svg"); - background-position: right 3% bottom 2%; - background-repeat: no-repeat; - background-attachment: 5%; - background-size: 20% auto; + +section.fig_cg p { + top: 300px; + text-align: center; } - - section.title h1 { - color: #808db5; - text-align: center; - } - - section.title p { - bottom: 25%; - width: 100%; - position: absolute; - font-size: 25px; - color: #4b4b4b; - background: linear-gradient(transparent 90%, #ffcc00 0%); - } - -section.slide h1 { - width: 95%; - color: white; - background-color: #808db5; - position: absolute; - left: 50px; - top: 35px; -} -;--heading-divider:1;" data-size="16:9"> -<h1>Gears Agda による Binary Tree の検証</h1> -<p>Binary Tree の実装に対して上述した3つのInvariantを<br /> -Meta Data Gear として渡しながら実行できるように記述する</p> -<pre><code><svg data-marp-fitting="svg" data-marp-fitting-code><foreignObject><span data-marp-fitting-svg-content><span data-marp-fitting-svg-content-wrap>findP : {n m : Level} {A : Set n} {t : Set m} → (env : Env A) - → treeInvariant env ∧ stackInvariant env - → (exit : (env : Env A) → treeInvariant env ∧ stackInvariant env → t ) → t -</span></span></foreignObject></svg></code></pre> -</section> -</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="25" data-paginate="true" data-class="slide" data-theme="default" data-style="section { +" data-heading-divider="1" class="slide" data-marpit-pagination="24" data-marpit-pagination-total="24" style="--paginate:true;--class:slide;--theme:default;--style:section { background-color: #FFFFFF; font-size: 28px; color: #4b4b4b; @@ -2038,116 +2238,10 @@ left: 50px; top: 35px; } -" data-heading-divider="1" class="slide" data-marpit-pagination="25" data-marpit-pagination-total="26" style="--paginate:true;--class:slide;--theme:default;--style:section { - background-color: #FFFFFF; - font-size: 28px; - color: #4b4b4b; - font-family: "Droid Sans Mono", "Hiragino Maru Gothic ProN"; - background-image: url("logo.svg"); - background-position: right 3% bottom 2%; - background-repeat: no-repeat; - background-attachment: 5%; - background-size: 20% auto; -} - section.title h1 { - color: #808db5; - text-align: center; - } - - section.title p { - bottom: 25%; - width: 100%; - position: absolute; - font-size: 25px; - color: #4b4b4b; - background: linear-gradient(transparent 90%, #ffcc00 0%); - } - -section.slide h1 { - width: 95%; - color: white; - background-color: #808db5; - position: absolute; - left: 50px; - top: 35px; -} -;--heading-divider:1;" data-size="16:9"> -<h1>今後の研究方針</h1> -<ul> -<li>現在は Binary Tree の検証までしか行えていないが、<br /> -今回定義した条件はそのまま Red Black Tree の検証に使用できるはず</li> -<li>今後は Gears Agda による実装と条件の追加をおこなう</li> -<li>モデル検査</li> -</ul> -</section> -</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="26" data-paginate="true" data-class="slide" data-theme="default" data-style="section { - background-color: #FFFFFF; - font-size: 28px; - color: #4b4b4b; - font-family: "Droid Sans Mono", "Hiragino Maru Gothic ProN"; - background-image: url("logo.svg"); - background-position: right 3% bottom 2%; - background-repeat: no-repeat; - background-attachment: 5%; - background-size: 20% auto; -} - - section.title h1 { - color: #808db5; - text-align: center; - } - - section.title p { - bottom: 25%; - width: 100%; - position: absolute; - font-size: 25px; - color: #4b4b4b; - background: linear-gradient(transparent 90%, #ffcc00 0%); - } - -section.slide h1 { - width: 95%; - color: white; - background-color: #808db5; - position: absolute; - left: 50px; - top: 35px; -} -" data-heading-divider="1" class="slide" data-marpit-pagination="26" data-marpit-pagination-total="26" style="--paginate:true;--class:slide;--theme:default;--style:section { - background-color: #FFFFFF; - font-size: 28px; - color: #4b4b4b; - font-family: "Droid Sans Mono", "Hiragino Maru Gothic ProN"; - background-image: url("logo.svg"); - background-position: right 3% bottom 2%; - background-repeat: no-repeat; - background-attachment: 5%; - background-size: 20% auto; -} - - section.title h1 { - color: #808db5; - text-align: center; - } - - section.title p { - bottom: 25%; - width: 100%; - position: absolute; - font-size: 25px; - color: #4b4b4b; - background: linear-gradient(transparent 90%, #ffcc00 0%); - } - -section.slide h1 { - width: 95%; - color: white; - background-color: #808db5; - position: absolute; - left: 50px; - top: 35px; +section.fig_cg p { + top: 300px; + text-align: center; } ;--heading-divider:1;" data-size="16:9"> <h1>まとめ</h1> @@ -2165,8 +2259,8 @@ <p>condition を テンプレみたいに作ってかきやすくする話</p> </section> <script>!function(){"use strict";const t="marpitSVGPolyfill:setZoomFactor,",e=Symbol();let r,o;function n(n){const i="object"==typeof n&&n.target||document,a="object"==typeof n?n.zoom:n;window[e]||(Object.defineProperty(window,e,{configurable:!0,value:!0}),window.addEventListener("message",(({data:e,origin:r})=>{if(r===window.origin)try{if(e&&"string"==typeof e&&e.startsWith(t)){const[,t]=e.split(","),r=Number.parseFloat(t);Number.isNaN(r)||(o=r)}}catch(t){console.error(t)}})));let l=!1;Array.from(i.querySelectorAll("svg[data-marpit-svg]"),(t=>{var e,n,i,s;t.style.transform||(t.style.transform="translateZ(0)");const c=a||o||t.currentScale||1;r!==c&&(r=c,l=c);const d=t.getBoundingClientRect(),{length:u}=t.children;for(let r=0;r<u;r+=1){const o=t.children[r],a=o.getScreenCTM();if(a){const t=null!==(n=null===(e=o.x)||void 0===e?void 0:e.baseVal.value)&&void 0!==n?n:0,r=null!==(s=null===(i=o.y)||void 0===i?void 0:i.baseVal.value)&&void 0!==s?s:0,l=o.firstElementChild,{style:u}=l;u.transformOrigin||(u.transformOrigin=`${-t}px ${-r}px`),u.transform=`scale(${c}) matrix(${a.a}, ${a.b}, ${a.c}, ${a.d}, ${a.e-d.left}, ${a.f-d.top}) translateZ(0.0001px)`}}})),!1!==l&&Array.from(i.querySelectorAll("iframe"),(({contentWindow:e})=>{null==e||e.postMessage(`${t}${l}`,"null"===window.origin?"*":window.origin)}))}r=1,o=void 0;const i=(t,e,r)=>{if(t.getAttribute(e)!==r)return t.setAttribute(e,r),!0};function a({once:t=!1,target:e=document}={}){const r="Apple Computer, Inc."===navigator.vendor?[n]:[];let o=!t;const a=()=>{for(const t of r)t({target:e});!function(t=document){Array.from(t.querySelectorAll('svg[data-marp-fitting="svg"]'),(t=>{var e;const r=t.firstChild,o=r.firstChild,{scrollWidth:n,scrollHeight:a}=o;let l,s=1;if(t.hasAttribute("data-marp-fitting-code")&&(l=null===(e=t.parentElement)||void 0===e?void 0:e.parentElement),t.hasAttribute("data-marp-fitting-math")&&(l=t.parentElement),l){const t=getComputedStyle(l),e=Math.ceil(l.clientWidth-parseFloat(t.paddingLeft||"0")-parseFloat(t.paddingRight||"0"));e&&(s=e)}const c=Math.max(n,s),d=Math.max(a,1),u=`0 0 ${c} ${d}`;i(r,"width",`${c}`),i(r,"height",`${d}`),i(t,"preserveAspectRatio",getComputedStyle(t).getPropertyValue("--preserve-aspect-ratio")||"xMinYMin meet"),i(t,"viewBox",u)&&t.classList.toggle("__reflow__")}))}(e),o&&window.requestAnimationFrame(a)};return a(),()=>{o=!1}}const l=Symbol(),s=document.currentScript;((t=document)=>{if("undefined"==typeof window)throw new Error("Marp Core's browser script is valid only in browser context.");if(t[l])return t[l];const e=a({target:t}),r=()=>{e(),delete t[l]};Object.defineProperty(t,l,{configurable:!0,value:r})})(s?s.getRootNode():document)}(); -</script></foreignObject></svg></div><div class="bespoke-marp-note" data-index="1" tabindex="0"><p>研究目的</p></div><div class="bespoke-marp-note" data-index="13" tabindex="0"><p>コードの解説 -あとで…</p></div><div class="bespoke-marp-note" data-index="16" tabindex="0"><p>findは全部書いても大丈夫そう</p></div><div class="bespoke-marp-note" data-index="17" tabindex="0"><p>これは途中省略してよさそう</p></div><div class="bespoke-marp-note" data-index="20" tabindex="0"><p>コードの解説 +</script></foreignObject></svg></div><div class="bespoke-marp-note" data-index="1" tabindex="0"><p>研究目的</p></div><div class="bespoke-marp-note" data-index="11" tabindex="0"><p>コードの解説 +あとで…</p></div><div class="bespoke-marp-note" data-index="14" tabindex="0"><p>findは全部書いても大丈夫そう</p></div><div class="bespoke-marp-note" data-index="15" tabindex="0"><p>これは途中省略してよさそう</p></div><div class="bespoke-marp-note" data-index="18" tabindex="0"><p>コードの解説 省略した方がたぶん絶対良い right と left なんかはほとんど対照的なので省略とかでよさそう あとは、木構造の仕様を満たすためにData型になっている説明があるとよさそう</p></div><script>/*!! License: https://unpkg.com/@marp-team/marp-cli@1.5.0/lib/bespoke.js.LICENSE.txt */
--- a/slide/slide.md Thu Jan 06 11:18:27 2022 +0900 +++ b/slide/slide.md Thu Jan 06 13:59:12 2022 +0900 @@ -41,6 +41,11 @@ top: 35px; } + section.fig_cg p { + top: 300px; + text-align: center; + } + --- <!-- headingDivider: 1 --> @@ -87,7 +92,7 @@ # Agda の基本 record - 2つのものが同時に存在すること -- Record 型とはオブジェクトあるいは構造体のようなもの +- Record 型とはオブジェクトあるいは構造体 ``` record Env : Set where field @@ -96,101 +101,21 @@ open Env ``` -記述する際の基本的な例を以下に挙げる +型に対応する値の導入(intro) ``` record {varx = zero ; vary = suc zero} ``` - - -# Agda の基本 data -- 一つでも存在すること -- どちらかが成り立つ型を Data 型 で書く -``` -data bt {n : Level} (A : Set n) : Set n where - leaf : bt A - node : (key : N) → (value : A) → (left : bt A ) → (right : bt A ) → bt A -``` - -記述する際の基本的な例を以下に挙げる -``` -datasample : bt → N -datasample leaf = zero -datasample (node key value left right) = suc zero +record の値のアクセス(elim) ``` - - - -# Agda の基本 短縮記法 -- with を使用することでその変数のパターンマッチすることもできる -``` -patternmatch-default : Env → N -patternmatch-default record { varn = zero ; vari = i } = i -patternmatch-default record { varn = suc n ; vari = i } = patternmatch-default record { varn = n ; vari = suc i } -``` - -``` -patternmatch-extraction : env → N -patternmatch-extraction env with varn env -patternmatch-extraction zero = vari env -patternmatch-extraction suc n = patternmatch-extraction record { varn = n ; vari = suc (vari env) } -``` -- ... | `を使用することで関数の定義部分を省略できる -``` -patternmatch-extraction' : env → N -patternmatch-extraction' env with varn env -... | zero = vari env -... | suc n = patternmatch-default' record { varn = n ; vari = suc (vari env) } +(env : Env) → varx env ``` # Gears Agda の記法 -- Agda では関数の再帰呼び出しが可能であるが、CbC で再起処理を実装しても値は帰って来ない - - Agda で実装を行う際には再帰呼び出しを行わないようにする。 -``` -plus-com : {l : Level} {t : Set l} → Env → (next : Env → t) → (exit : Env → t) → t -plus-com env next exit with vary env -... | zero = exit (record { varx = varx env ; vary = vary env }) -... | suc y = next (record { varx = suc (varx env) ; vary = y }) -``` -- `→ t` で Set に遷移させるようにし、この後に関数が続くことと、関数を tail call していることで Continuation を定義している - - -# Gears Agda と Gears CbC の対応 x -- 証明のしやすいGears Agda で実装を行いながらContext単位で同時に検証も行う - -- Gears Agda は検証向きの実装となり、CbCでは高速な実行向きとなる -- Gears Agda での検証がCbCによる高速な実行の信頼性となる - -# Normal level と Meta Level を用いた信頼性の向上 -CbCのプログラムの実行部分は以下の2つから構成される -- Normal Level は軽量継続で関数型プログラミングとなる - - atomicってなんだろう - - ポインタの操作はここでは行わず Meta Level にて行う -- Meta Level では信頼性を保証するために必要な計算を行う - - メモリやCPUなどの資源管理 - - context - - 証明 - - 並列実行（他のプロセスとの干渉） - - monad - -# s - - -# Hoare Logic について -- Hoare Logic とは C.A.R Hoare, R.W Floyd が考案したプログラムの検証の手法 -- 「プログラムの事前条件 (P) が成立しているときコマンド (C) 実行して停止すると事後条件 (Q) が成り立つ」というもの - - CbC の実行を継続するという性質に非常に相性が良い - -pre/post condition を Gears Agda では Meta Input Data Gear として -プログラム中に遷移させていくことで、プログラムが終始仕様に沿った動きをしている -ことを検証する - - - -# Gears Agda による検証の例（実装） -- while program の検証を例に挙げる - - 以下は実装部分のコードとなる +Gears Agda では CbC と対応させるためにすべてLoopで記述する +loopは`→ t`の形式で表現する +再起呼び出しは使わない(構文的には禁止していないので注意が必要) ``` {-# TERMINATING #-} whileLoop : {l : Level} {t : Set l} → Env → (Code : Env → t) → t @@ -198,11 +123,74 @@ whileLoop env next | false = next env whileLoop env next | true = whileLoop (record {varn = (varn env) - 1 ; vari = (vari env) + 1}) next ``` +- t を返すで継続を表す(tは呼び出し時に任意に指定してもよい. testに使える) +- tail call により light weight continuation を定義している + + +# Gears Agda と Gears CbC の対応 +Gears Agda +- 証明向きの記述 +- Hoare Condition を含む + +Gears CbC +- 実行向きの記述 +- メモリ管理, 並列実行を含む + +Context +- processに相当する +- Code Gear 単位で並列実行 -# Gears Agda による検証の例（検証付き実装） -- 先ほど実装した while program に対して証明を付ける -- loop を接続する Meta Gear も用意する +# Normal level と Meta Level を用いた信頼性の向上 +Normal Level +- 軽量継続 +- Code Gear 単位で関数型プログラミングとなる +- atomic(Code Gear 自体の実行は割り込まれない) +- ポインタの操作は含まれない + +Meta Level +- メモリやCPUなどの資源管理, ポインタ操作 +- Hoare Condition と証明 +- Contextによる並列実行 +- monadに相当するData構造 + +# +<!-- class: fig_cg --> + + +# Gears Agda と Hoare Logic +<!-- class: slide --> +C.A.R Hoare, R.W Floyd が考案 +- Pre Condition → Command → Post Condition + +Gears Agda による Command の例 +``` +{-# TERMINATING #-} +whileLoop : {l : Level} {t : Set l} → Env → (Code : Env → t) → t +whileLoop env next with lt 0 (varn env) +whileLoop env next | false = next env +whileLoop env next | true = whileLoop (record {varn = (varn env) - 1 ; vari = (vari env) + 1}) next +``` +- `{-# TERMINATING #-}` +- with 文 +- 型と値 + +# Gears Agda の Pre Condition Post Condition +``` +whileLoopSeg : {l : Level} {t : Set l} → {c10 : N } → (env : Env) → (varn env + vari env ≡ c10) + → (next : (e1 : Env )→ varn e1 + vari e1 ≡ c10 → varn e1 < varn env → t) + → (exit : (e1 : Env )→ vari e1 ≡ c10 → t) → t +``` +- Terminatingを避けるためにloopを分割 +- `varn env + vari env ≡ c10` が Pre Condition +- `varn e1 + vari e1 ≡ c10` が Post Condition +- `varn e1 < varn env → t` が停止を保証する減少列 + +これは命題なので証明を与えてPre ConditionからPost Conditionを導出する必要がある +証明は値として次のCodeGearに渡される + +# Loop の接続 +分割したloopを接続するMeta Code Gearを作成する ``` TerminatingLoopS : {l : Level} {t : Set l} ( Index : Set ) → {Invraiant : Index → Set } → ( reduce : Index → N) @@ -210,15 +198,29 @@ → (next : (r1 : Index) → Invraiant r1 → reduce r1 < reduce r → t ) → t) → (r : Index) → (p : Invraiant r) → t ``` -- 入力として仕様の証明を受け取る -- 出力として次の関数に仕様の証明を渡す -- Hoare Conditionがプログラムの開始から停止するまで接続されていれば証明は完成 - - Meta Gear にて証明を値としてあたえているため +- IndexはLoop変数 +- Invariantはloop変数の不変条件 +- loopに接続するCode Gearを与える +- reduceは停止性を保証する減少列 + +これを一般的に証明することができている -<!-- -コードの解説 -あとで… ---> +# 実際のloopの接続 +証明したい性質を以下のように記述する +``` +whileTestSpec1 : (c10 : N) → (e1 : Env ) → vari e1 ≡ c10 → ⊤ +whileTestSpec1 _ _ x = tt +``` +loopをTerminatingLoopSで接続して仕様記述に繋げる +``` +proofGearsTermS : {c10 : N} → ⊤ +proofGearsTermS {c10} = whileTest' {_} {_} {c10} (λ n p → conversion1 n p (λ n1 p1 → + TerminatingLoopS Env (λ env → varn env)(λ n2 p2 loop → whileLoopSeg {_} {_} {c10} n2 p2 loop + (λ ne pe → whileTestSpec1 c10 ne pe)) n1 p1 )) +``` +- conversion1は +- whileLoopSeg +- ⊤ # test との違い - test では実数を与えた際の出力が仕様に沿ったものであるかを検証する