Mercurial > hg > Papers > 2021 > soto-prosym
changeset 12:62e56d73f104
WIP カンペを追加 14ページまで
| author | soto <soto@cr.ie.u-ryukyu.ac.jp> |
|---|---|
| date | Fri, 07 Jan 2022 00:58:07 +0900 |
| parents | 8a97e69f8615 |
| children | 76c3378c61dc |
| files | MindMap/slide.html MindMap/slide.pdf slide/note.md slide/slide.md |
| diffstat | 4 files changed, 962 insertions(+), 454 deletions(-) [+] |
line wrap: on
line diff
--- a/MindMap/slide.html Thu Jan 06 16:57:53 2022 +0900 +++ b/MindMap/slide.html Fri Jan 07 00:58:07 2022 +0900 @@ -48,7 +48,7 @@ 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 { +" data-heading-divider="1" class="title" data-marpit-pagination="1" data-marpit-pagination-total="28" style="--paginate:true;--class:title;--theme:default;--style:section { background-color: #FFFFFF; font-size: 28px; color: #4b4b4b; @@ -131,7 +131,7 @@ 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 { +" data-heading-divider="1" class="slide" data-marpit-pagination="2" data-marpit-pagination-total="28" style="--paginate:true;--class:slide;--theme:default;--style:section { background-color: #FFFFFF; font-size: 28px; color: #4b4b4b; @@ -227,7 +227,7 @@ 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 { +" data-heading-divider="1" class="slide" data-marpit-pagination="3" data-marpit-pagination-total="28" style="--paginate:true;--class:slide;--theme:default;--style:section { background-color: #FFFFFF; font-size: 28px; color: #4b4b4b; @@ -318,7 +318,7 @@ 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 { +" data-heading-divider="1" class="slide" data-marpit-pagination="4" data-marpit-pagination-total="28" style="--paginate:true;--class:slide;--theme:default;--style:section { background-color: #FFFFFF; font-size: 28px; color: #4b4b4b; @@ -360,12 +360,8 @@ ;--heading-divider:1;" data-size="16:9"> <h1>Agda の基本</h1> <ul> -<li>Agdaとは定理証明支援器であり、関数型言語である</li> -<li>Agdaでの関数は、最初に型について定義した後に、関数を定義する事で記述できる -<ul> -<li>これが Curry-Howard 対応となる</li> -</ul> -</li> +<li>Agdaとは定理証明支援器であり、関数型言語</li> +<li>Agdaでの関数は、最初に型について定義した後に、関数を定義する事で記述する</li> <li>型の定義部分で、入力と出力の型を定義できる <ul> <li>input → output のようになる</li> @@ -377,12 +373,6 @@ </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>sample1 : (A : Set ) → Set -sample1 a = a - -sample2 : (A : Set ) → (B : Set ) → Set -sample2 a b = b -</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="5" data-paginate="true" data-class="slide" data-theme="default" data-style="section { background-color: #FFFFFF; @@ -423,7 +413,7 @@ 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 { +" data-heading-divider="1" class="slide" data-marpit-pagination="5" data-marpit-pagination-total="28" style="--paginate:true;--class:slide;--theme:default;--style:section { background-color: #FFFFFF; font-size: 28px; color: #4b4b4b; @@ -464,10 +454,7 @@ } ;--heading-divider:1;" data-size="16:9"> <h1>Agda の基本 record</h1> -<ul> -<li>2つのものが同時に存在すること</li> -<li>Record 型とはオブジェクトあるいは構造体</li> -</ul> +<p>オブジェクトあるいは構造体</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 Env : Set where field varn : N @@ -520,202 +507,7 @@ 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; - 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>Agda の基本 data</h1> -<ul> -<li>一つでも存在すること</li> -<li>どちらかが成り立つ型を Data 型 で書く</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 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 -</span></span></foreignObject></svg></code></pre> -<p>記述する際の基本的な例を以下に挙げる</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>datasample : bt → N -datasample leaf = zero -datasample (node key value left right) = suc zero -</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="7" 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; -} - -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; - 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>Agda の基本 短縮記法</h1> -<ul> -<li>with を使用することでその変数のパターンマッチすることもできる</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>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 } -</span></span></foreignObject></svg></code></pre> -<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>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) } -</span></span></foreignObject></svg></code></pre> -<ul> -<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>patternmatch-extraction' : env → N -patternmatch-extraction' env with varn env -... | zero = vari env -... | suc n = patternmatch-default' record { varn = n ; vari = suc (vari 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="8" 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; -} - -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 { +" data-heading-divider="1" class="slide" data-marpit-pagination="6" data-marpit-pagination-total="28" style="--paginate:true;--class:slide;--theme:default;--style:section { background-color: #FFFFFF; font-size: 28px; color: #4b4b4b; @@ -756,23 +548,21 @@ } ;--heading-divider:1;" data-size="16:9"> <h1>Gears Agda の記法</h1> -<ul> -<li>Agda では関数の再帰呼び出しが可能であるが、CbC で再起処理を実装しても値は帰って来ない -<ul> -<li>Agda で実装を行う際には再帰呼び出しを行わないようにする。</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>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 }) +<p>Gears Agda では CbC と対応させるためにすべてLoopで記述する<br /> +loopは<code>→ t</code>の形式で表現する<br /> +再帰呼び出しは使わない(構文的には禁止していないので注意が必要)</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>→ t</code> で Set に遷移させるようにし、この後に関数が続くことと、関数を tail call していることで Continuation を定義している</li> +<li>t を返すことで継続を表す(tは呼び出し時に任意に指定してもよい. testに使える)</li> +<li>tail call により light weight continuation を定義している</li> </ul> </section> -</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="9" 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="7" data-paginate="true" data-class="slide" data-theme="default" data-style="section { background-color: #FFFFFF; font-size: 28px; color: #4b4b4b; @@ -811,7 +601,7 @@ 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 { +" data-heading-divider="1" class="slide" data-marpit-pagination="7" data-marpit-pagination-total="28" style="--paginate:true;--class:slide;--theme:default;--style:section { background-color: #FFFFFF; font-size: 28px; color: #4b4b4b; @@ -851,20 +641,24 @@ text-align: center; } ;--heading-divider:1;" data-size="16:9"> -<h1>Gears Agda と Gears CbC の対応 x</h1> +<h1>Gears Agda と Gears CbC の対応</h1> +<p>Gears Agda</p> +<ul> +<li>証明向きの記述</li> +<li>Hoare Condition を含む</li> +</ul> +<p>Gears CbC</p> <ul> -<li> -<p>証明のしやすいGears Agda で実装を行いながらContext単位で同時に検証も行う</p> -</li> -<li> -<p>Gears Agda は検証向きの実装となり、CbCでは高速な実行向きとなる</p> -</li> -<li> -<p>Gears Agda での検証がCbCによる高速な実行の信頼性となる</p> -</li> +<li>実行向きの記述</li> +<li>メモリ管理, 並列実行を含む</li> +</ul> +<p>Context</p> +<ul> +<li>processに相当する</li> +<li>Code Gear 単位で並列実行</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="fig_cg" data-theme="default" data-style="section { +</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="8" data-paginate="true" data-class="slide" data-theme="default" data-style="section { background-color: #FFFFFF; font-size: 28px; color: #4b4b4b; @@ -903,7 +697,7 @@ 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 { +" data-heading-divider="1" class="slide" data-marpit-pagination="8" data-marpit-pagination-total="28" style="--paginate:true;--class:slide;--theme:default;--style:section { background-color: #FFFFFF; font-size: 28px; color: #4b4b4b; @@ -944,27 +738,22 @@ } ;--heading-divider:1;" data-size="16:9"> <h1>Normal level と Meta Level を用いた信頼性の向上</h1> -<ul> -<li>CbCのプログラムの実行部分は以下の2つから構成される</li> -<li>Normal Level は軽量継続で関数型プログラミングとなる -<ul> -<li>ポインタの操作はここでは行わず Meta Level にて行う</li> -</ul> -</li> -<li>Meta Level では信頼性を保証するために必要な計算を行う +<p>Normal Level</p> <ul> -<li>メモリやCPUなどの資源管理</li> -<li>context</li> -<li>証明</li> -<li>並列実行（他のプロセスとの干渉）</li> -<li>monad</li> +<li>軽量継続</li> +<li>Code Gear 単位で関数型プログラミングとなる</li> +<li>atomic(Code Gear 自体の実行は割り込まれない)</li> +<li>ポインタの操作は含まれない</li> </ul> -</li> +<p>Meta Level</p> +<ul> +<li>メモリやCPUなどの資源管理, ポインタ操作</li> +<li>Hoare Condition と証明</li> +<li>Contextによる並列実行</li> +<li>monadに相当するData構造</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 { +</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="9" data-paginate="true" data-class="fig_cg" data-theme="default" data-style="section { background-color: #FFFFFF; font-size: 28px; color: #4b4b4b; @@ -1003,7 +792,90 @@ 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 { +" data-heading-divider="1" class="fig_cg" data-marpit-pagination="9" data-marpit-pagination-total="28" style="--paginate:true;--class:fig_cg;--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> + +<p><img src="meta_cg_dg.svg" alt="" style="height:700px;" /></p> +</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 { + 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; +} +" data-heading-divider="1" class="slide" data-marpit-pagination="10" data-marpit-pagination-total="28" style="--paginate:true;--class:slide;--theme:default;--style:section { background-color: #FFFFFF; font-size: 28px; color: #4b4b4b; @@ -1062,6 +934,99 @@ <li>型と値</li> </ul> </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; + 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; +} +" data-heading-divider="1" class="slide" data-marpit-pagination="11" data-marpit-pagination-total="28" 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>Gears Agda の Pre Condition Post Condition</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>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 +</span></span></foreignObject></svg></code></pre> +<ul> +<li>Terminatingを避けるためにloopを分割</li> +<li><code>varn env + vari env ≡ c10</code> が Pre Condition</li> +<li><code>varn e1 + vari e1 ≡ c10</code> が Post Condition</li> +<li><code>varn e1 < varn env → t</code> が停止を保証する減少列</li> +</ul> +<p>これは命題なので証明を与えてPre ConditionからPost Conditionを導出する必要がある<br /> +証明は値として次のCodeGearに渡される</p> +</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; font-size: 28px; @@ -1101,7 +1066,7 @@ 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 { +" data-heading-divider="1" class="slide" data-marpit-pagination="12" data-marpit-pagination-total="28" style="--paginate:true;--class:slide;--theme:default;--style:section { background-color: #FFFFFF; font-size: 28px; color: #4b4b4b; @@ -1141,11 +1106,8 @@ text-align: center; } ;--heading-divider:1;" data-size="16:9"> -<h1>Gears Agda による検証の例（検証付き実装）</h1> -<ul> -<li>先ほど実装した while program に対して証明を付ける</li> -<li>loop を接続する Meta Gear も用意する</li> -</ul> +<h1>Loop の接続</h1> +<p>分割したloopを接続するMeta Code 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>TerminatingLoopS : {l : Level} {t : Set l} ( Index : Set ) → {Invraiant : Index → Set } → ( reduce : Index → N) → (loop : (r : Index) → Invraiant r @@ -1153,14 +1115,12 @@ → (r : Index) → (p : Invraiant r) → t </span></span></foreignObject></svg></code></pre> <ul> -<li>入力として仕様の証明を受け取る</li> -<li>出力として次の関数に仕様の証明を渡す</li> -<li>Hoare Conditionがプログラムの開始から停止するまで接続されていれば証明は完成 -<ul> -<li>Meta Gear にて証明を値としてあたえているため</li> +<li>IndexはLoop変数</li> +<li>Invariantはloop変数の不変条件</li> +<li>loopに接続するCode Gearを与える</li> +<li>reduceは停止性を保証する減少列</li> </ul> -</li> -</ul> +<p>これを一般的に証明することができている</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; @@ -1201,7 +1161,103 @@ 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 { +" data-heading-divider="1" class="slide" data-marpit-pagination="13" data-marpit-pagination-total="28" 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>実際のloopの接続</h1> +<p>証明したい性質を以下のように記述する</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>whileTestSpec1 : (c10 : N) → (e1 : Env ) → vari e1 ≡ c10 → ⊤ +whileTestSpec1 _ _ x = tt +</span></span></foreignObject></svg></code></pre> +<p>loopをTerminatingLoopSで接続して仕様記述に繋げる</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>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 )) +</span></span></foreignObject></svg></code></pre> +<ul> +<li>conversion1はPre Condition をPost Conditionに変換する</li> +<li>whileLoopSeg</li> +<li>⊤</li> +</ul> +</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; + 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; +} +" data-heading-divider="1" class="slide" data-marpit-pagination="14" data-marpit-pagination-total="28" style="--paginate:true;--class:slide;--theme:default;--style:section { background-color: #FFFFFF; font-size: 28px; color: #4b4b4b; @@ -1255,7 +1311,7 @@ </li> </ul> </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 { +</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 { background-color: #FFFFFF; font-size: 28px; color: #4b4b4b; @@ -1294,7 +1350,7 @@ 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 { +" data-heading-divider="1" class="slide" data-marpit-pagination="15" data-marpit-pagination-total="28" style="--paginate:true;--class:slide;--theme:default;--style:section { background-color: #FFFFFF; font-size: 28px; color: #4b4b4b; @@ -1335,105 +1391,16 @@ } ;--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> -</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 { - 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; -} -" 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; - 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>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 +<p>CbCと並行した実装をするため、Stackを明示した実装をする</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>find : {n m : Level} {A : Set n} {t : Set m} → (key : ℕ) → (tree : bt A ) → List (bt A) + → (next : bt A → List (bt A) → t ) → (exit : bt A → List (bt 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> +<p>置き換えるnodeまでTreeを辿り、Stackに逆順にTreeを積んでいく</p> </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; @@ -1474,7 +1441,7 @@ 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 { +" data-heading-divider="1" class="slide" data-marpit-pagination="16" data-marpit-pagination-total="28" style="--paginate:true;--class:slide;--theme:default;--style:section { background-color: #FFFFFF; font-size: 28px; color: #4b4b4b; @@ -1515,6 +1482,7 @@ } ;--heading-divider:1;" data-size="16:9"> <h1>Gears Agda による BinaryTree の実装 replace node</h1> +<p>置き換えたnodeをStackを解消しながらTreeを再構成する</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>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 ) @@ -1571,7 +1539,7 @@ 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 { +" data-heading-divider="1" class="slide" data-marpit-pagination="17" data-marpit-pagination-total="28" style="--paginate:true;--class:slide;--theme:default;--style:section { background-color: #FFFFFF; font-size: 28px; color: #4b4b4b; @@ -1611,9 +1579,19 @@ 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> -</span></span></foreignObject></svg></code></pre> +<h1>Binary Tree の3種類の Invariant</h1> +<p>Tree Invariant</p> +<ul> +<li>Binary Tree が Key の順序に沿って構成されていることを表すData構造</li> +</ul> +<p>Stack Invariant</p> +<ul> +<li>Stackが木の昇順に構成されていることを表す</li> +</ul> +<p>Replace Tree</p> +<ul> +<li>2つの木の1つのnodeが入れ替わっていることを示す</li> +</ul> </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 { background-color: #FFFFFF; @@ -1654,7 +1632,7 @@ 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 { +" data-heading-divider="1" class="slide" data-marpit-pagination="18" data-marpit-pagination-total="28" style="--paginate:true;--class:slide;--theme:default;--style:section { background-color: #FFFFFF; font-size: 28px; color: #4b4b4b; @@ -1694,14 +1672,26 @@ text-align: center; } ;--heading-divider:1;" data-size="16:9"> -<h1>Gears Agda による Binary Tree の検証 Invariant</h1> -<p>具体的な例を一つ挙げて、Invariantの説明を行う</p> +<h1>Tree Invariant</h1> <ul> -<li>Binary Tree の性質である、左の子のkeyは親より小さく、<br /> -右の子のkeyは親より大きいことを検証</li> -<li>Stack に格納されているTreeはその次のStackの減少列になっているか</li> -<li>Tree を正しく入れ替えられているか</li> +<li>Invariant というよりも可能な Binary Tree 全体の集合を表す型</li> +<li>制約付きのBinary Tree</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="19" data-paginate="true" data-class="slide" data-theme="default" data-style="section { background-color: #FFFFFF; @@ -1742,7 +1732,7 @@ 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 { +" data-heading-divider="1" class="slide" data-marpit-pagination="19" data-marpit-pagination-total="28" style="--paginate:true;--class:slide;--theme:default;--style:section { background-color: #FFFFFF; font-size: 28px; color: #4b4b4b; @@ -1782,24 +1772,21 @@ text-align: center; } ;--heading-divider:1;" data-size="16:9"> -<h1>Gears Agda による Binary Tree の検証 Invariant</h1> +<h1>Stack Invariant</h1> <ul> -<li>Tree Invariant</li> +<li>StackにはTreeを辿った履歴が残っている</li> +<li>辿り方はKeyの値に依存する</li> +<li>実際のStackよりも豊富な情報を持っている</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 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="20" data-paginate="true" data-class="slide" data-theme="default" data-style="section { @@ -1841,7 +1828,7 @@ 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 { +" data-heading-divider="1" class="slide" data-marpit-pagination="20" data-marpit-pagination-total="28" style="--paginate:true;--class:slide;--theme:default;--style:section { background-color: #FFFFFF; font-size: 28px; color: #4b4b4b; @@ -1881,19 +1868,20 @@ text-align: center; } ;--heading-divider:1;" data-size="16:9"> -<h1>Gears Agda による Binary Tree の検証 Invariant</h1> +<h1>Replace Tree</h1> <ul> -<li>Stack Invariant</li> +<li>木の特定のnodeが正しく置き換えられているか</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) +<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="21" data-paginate="true" data-class="slide" data-theme="default" data-style="section { @@ -1935,7 +1923,7 @@ 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 { +" data-heading-divider="1" class="slide" data-marpit-pagination="21" data-marpit-pagination-total="28" style="--paginate:true;--class:slide;--theme:default;--style:section { background-color: #FFFFFF; font-size: 28px; color: #4b4b4b; @@ -1975,20 +1963,17 @@ text-align: center; } ;--heading-divider:1;" data-size="16:9"> -<h1>Gears Agda による Binary Tree の検証 Invariant</h1> -<ul> -<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 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) +<h1>find の Hoare Condition</h1> +<p>findPでは treeInvariant をつかって stackInvariant を生成する<br /> +停止性を証明する木の深さの不等式も証明する</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} → (key : ℕ) → (tree tree0 : bt A ) → (stack : List (bt A)) + → treeInvariant tree ∧ stackInvariant key tree tree0 stack + → (next : (tree1 : bt A) → (stack : List (bt A)) + → treeInvariant tree1 ∧ stackInvariant key tree1 tree0 stack + → bt-depth tree1 < bt-depth tree → t ) + → (exit : (tree1 : bt A) → (stack : List (bt A)) + → treeInvariant tree1 ∧ stackInvariant key tree1 tree0 stack + → (tree1 ≡ leaf ) ∨ ( node-key tree1 ≡ just key ) → 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="22" data-paginate="true" data-class="slide" data-theme="default" data-style="section { @@ -2030,7 +2015,7 @@ 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 { +" data-heading-divider="1" class="slide" data-marpit-pagination="22" data-marpit-pagination-total="28" style="--paginate:true;--class:slide;--theme:default;--style:section { background-color: #FFFFFF; font-size: 28px; color: #4b4b4b; @@ -2070,12 +2055,19 @@ text-align: center; } ;--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 +<h1>Hoare Condition の拡張</h1> +<p>testなどでは仮定が入ることがある<br /> +Hoare Conditionを拡張可能な部分があるrecordで定義する<br /> +Cが拡張される部分で, これはDataの継続に相当する<br /> +Code Gear に継続があるように 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>record findPR {n : Level} {A : Set n} (key : ℕ) (tree : bt A ) (stack : List (bt A)) + (C : ℕ → bt A → List (bt A) → Set n) : Set n where + field + tree0 : bt A + ti0 : treeInvariant tree0 + ti : treeInvariant tree + si : stackInvariant key tree tree0 stack + ci : C key tree stack -- data continuation </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 { @@ -2117,7 +2109,383 @@ 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 { +" data-heading-divider="1" class="slide" data-marpit-pagination="23" data-marpit-pagination-total="28" 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> +<p>拡張部分はrecord findPC で定義する<br /> +拡張部分の推論はrecord findExt で定義する</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 findPC {n : Level} {A : Set n} (value : A) (key1 : ℕ) (tree : bt A ) (stack : List (bt A)) : Set n where + field + tree1 : bt A + ci : replacedTree key1 value tree1 tree + +record findExt {n : Level} {A : Set n} (key : ℕ) (C : ℕ → bt A → List (bt A) → Set n) : Set (Level.suc n) where + field + c1 : {key₁ : ℕ} {tree tree₁ : bt A } {st : List (bt A)} {v1 : A} + → findPR key (node key₁ v1 tree tree₁) st C → key < key₁ → C key tree (tree ∷ st) + c2 : {key₁ : ℕ} {tree tree₁ : bt A } {st : List (bt A)} {v1 : A} + → findPR key (node key₁ v1 tree tree₁) st C → key > key₁ → C key tree₁ (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="24" 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; +} + +section.fig_cg p { + top: 300px; + text-align: center; +} +" data-heading-divider="1" class="slide" data-marpit-pagination="24" data-marpit-pagination-total="28" 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>replade Node の Invariant</h1> +<p>repraceTree は置き換えるべきnodeが実行時に決まるので関数を挟んだInvariantになる</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>child-replaced : {n : Level} {A : Set n} (key : ℕ) (tree : bt A) → bt A +child-replaced key leaf = leaf +child-replaced key (node key₁ value left right) with <-cmp key key₁ +... | tri< a ¬b ¬c = left +... | tri≈ ¬a b ¬c = node key₁ value left right +... | tri> ¬a ¬b c = right + +record replacePR {n : Level} {A : Set n} (key : ℕ) (value : A) (tree repl : bt A ) + (stack : List (bt A)) (C : bt A → bt A → List (bt A) → Set n) : Set n where + field + tree0 : bt A + ti : treeInvariant tree0 + si : stackInvariant key tree tree0 stack + ri : replacedTree key value (child-replaced key tree ) repl + ci : C tree repl stack -- data continuation +</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 { + 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; +} +" data-heading-divider="1" class="slide" data-marpit-pagination="25" data-marpit-pagination-total="28" 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> +<p>insertしたkeyをfindすると元の値が取れてくることを証明する<br /> +insertTreeSpec0が仕様<br /> +conteinsTreeがtestコードかつ証明になっている<br /> +証明の詳細はコードのHoara condition の証明に入っている</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>insertTreeSpec0 : {n : Level} {A : Set n} → (tree : bt A) → (value : A) + → top-value tree ≡ just value → ⊤ +insertTreeSpec0 _ _ _ = tt + +containsTree : {n : Level} {A : Set n} → (tree tree1 : bt A) → (key : ℕ) → (value : A) + → treeInvariant tree1 → replacedTree key value tree1 tree → ⊤ +containsTree {n} {A} tree tree1 key value P RT = + TerminatingLoopS (bt A ∧ List (bt A) ) + {λ p → findPR key (proj1 p) (proj2 p) (findPC value ) } (λ p → bt-depth (proj1 p)) + ⟪ tree , tree ∷ [] ⟫ ? + $ λ p P loop → findPPC1 key value (proj1 p) (proj2 p) P (λ t s P1 lt → loop ⟪ t , s ⟫ P1 lt ) + $ λ t1 s1 P2 found? → insertTreeSpec0 t1 value (lemma6 t1 s1 found? P2) +</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="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; +} + +section.fig_cg p { + top: 300px; + text-align: center; +} +" data-heading-divider="1" class="slide" data-marpit-pagination="26" data-marpit-pagination-total="28" 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>replace Tree の性質</h1> +<p>Replace Tree 自体は Tree に特定の値が入っていることを示すData構造になっている<br /> +これをHoare条件として持ち歩くことにより、Binary Treeの詳細に立ち入らず何が入っているかを指定できる</p> +<p>これにより木を用いるプログラムでの証明を記述できる<br /> +insert Tree や Find Node の停止性も証明されている</p> +</section> +</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="27" 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; +} + +section.fig_cg p { + top: 300px; + text-align: center; +} +" data-heading-divider="1" class="slide" data-marpit-pagination="27" data-marpit-pagination-total="28" style="--paginate:true;--class:slide;--theme:default;--style:section { background-color: #FFFFFF; font-size: 28px; color: #4b4b4b; @@ -2159,13 +2527,25 @@ ;--heading-divider:1;" data-size="16:9"> <h1>今後の研究方針</h1> <ul> -<li>現在は Binary Tree の検証までしか行えていないが、<br /> -今回定義した条件はそのまま Red Black Tree の検証に使用できるはず</li> -<li>今後は Gears Agda による実装と条件の追加をおこなう</li> +<li>Deleteの実装</li> +<li>Red Black Tree の実装 +<ul> +<li>今回定義した条件はそのまま Red Black Tree の検証に使用できるはず</li> +</ul> +</li> +<li>Contextを用いた並列実行時のプログラムの正しさの証明 +<ul> +<li>synchronized queue</li> +<li>concurrent tree</li> +</ul> +</li> +<li>xv.6への適用</li> <li>モデル検査</li> </ul> +<p>読めない間は待っている<br /> +tree</p> </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 { +</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="28" data-paginate="true" data-class="slide" data-theme="default" data-style="section { background-color: #FFFFFF; font-size: 28px; color: #4b4b4b; @@ -2204,7 +2584,7 @@ top: 300px; text-align: center; } -" data-heading-divider="1" class="slide" data-marpit-pagination="24" data-marpit-pagination-total="24" style="--paginate:true;--class:slide;--theme:default;--style:section { +" data-heading-divider="1" class="slide" data-marpit-pagination="28" data-marpit-pagination-total="28" style="--paginate:true;--class:slide;--theme:default;--style:section { background-color: #FFFFFF; font-size: 28px; color: #4b4b4b; @@ -2248,20 +2628,26 @@ <ul> <li>Gears Agda にて Binary Tree を検証することができた <ul> -<li>Gears Agda における Termination を使用しない実装の仕方を確率した</li> +<li>Gears Agda における Termination を使用しない実装の仕方を確立した</li> <li>Hoare Logic による検証もできるようになった</li> <li>今後は Red Black Tree の検証をすすめる</li> </ul> </li> <li>モデル検査をしたい</li> </ul> -<p>英語版も欲しい</p> -<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="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>コードの解説 +</script></foreignObject></svg></div><div class="bespoke-marp-note" data-index="1" tabindex="0"><p>研究目的</p></div><div class="bespoke-marp-note" data-index="3" tabindex="0"><p>``` +sample1 : (A : Set ) → Set +sample1 a = a + +sample2 : (A : Set ) → (B : Set ) → Set +sample2 a b = b +```</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="17" tabindex="0"><p>t-leaf はコンストラクタ + + +コードの解説 省略した方がたぶん絶対良い right と left なんかはほとんど対照的なので省略とかでよさそう -あとは、木構造の仕様を満たすためにData型になっている説明があるとよさそう</p></div><script>/*!! License: https://unpkg.com/@marp-team/marp-cli@1.5.0/lib/bespoke.js.LICENSE.txt */ +あとは、木構造の仕様を満たすためにData型になっている説明があるとよさそう</p></div><div class="bespoke-marp-note" data-index="18" tabindex="0"><p>Keyの比較が入っているから</p></div><div class="bespoke-marp-note" data-index="27" tabindex="0"><p>英語版も欲しい</p></div><script>/*!! License: https://unpkg.com/@marp-team/marp-cli@1.5.0/lib/bespoke.js.LICENSE.txt */ !function(){"use strict";const e=document.body,t=(...e)=>history.replaceState(...e),n="presenter",r="next",o=["",n,r],a="data-bespoke-marp-",i=(e,{protocol:t,host:n,pathname:r,hash:o}=location)=>{const a=e.toString();return`${t}//${n}${r}${a?"?":""}${a}${o}`},s=()=>e.dataset.bespokeView,l=e=>new URLSearchParams(location.search).get(e),c=(e,n={})=>{var r;const o={location,setter:t,...n},a=new URLSearchParams(o.location.search);for(const t of Object.keys(e)){const n=e[t];"string"==typeof n?a.set(t,n):a.delete(t)}try{o.setter({...null!==(r=window.history.state)&&void 0!==r?r:{}},"",i(a,o.location))}catch(e){console.error(e)}},d=(()=>{const e="bespoke-marp";try{return localStorage.setItem(e,e),localStorage.removeItem(e),!0}catch(e){return!1}})(),f=e=>{try{return localStorage.getItem(e)}catch(e){return null}},u=(e,t)=>{try{return localStorage.setItem(e,t),!0}catch(e){return!1}},m=e=>{try{return localStorage.removeItem(e),!0}catch(e){return!1}},g=(e,t)=>{const n="aria-hidden";t?e.setAttribute(n,"true"):e.removeAttribute(n)},p=e=>{e.parent.classList.add("bespoke-marp-parent"),e.slides.forEach((e=>e.classList.add("bespoke-marp-slide"))),e.on("activate",(t=>{const n="bespoke-marp-active",r=t.slide,o=r.classList,a=!o.contains(n);if(e.slides.forEach((e=>{e.classList.remove(n),g(e,!0)})),o.add(n),g(r,!1),a){const e=`${n}-ready`;o.add(e),document.body.clientHeight,o.remove(e)}}))},v=e=>{let t=0,n=0;Object.defineProperty(e,"fragments",{enumerable:!0,value:e.slides.map((e=>[null,...e.querySelectorAll("[data-marpit-fragment]")]))});const r=r=>void 0!==e.fragments[t][n+r],o=(r,o)=>{t=r,n=o,e.fragments.forEach(((e,t)=>{e.forEach(((e,n)=>{if(null==e)return;const i=t<r||t===r&&n<=o;e.setAttribute(`${a}fragment`,(i?"":"in")+"active");const s=`${a}current-fragment`;t===r&&n===o?e.setAttribute(s,"current"):e.removeAttribute(s)}))})),e.fragmentIndex=o;const i={slide:e.slides[r],index:r,fragments:e.fragments[r],fragmentIndex:o};e.fire("fragment",i)};e.on("next",(({fragment:a=!0})=>{if(a){if(r(1))return o(t,n+1),!1;const a=t+1;e.fragments[a]&&o(a,0)}else{const r=e.fragments[t].length;if(n+1<r)return o(t,r-1),!1;const a=e.fragments[t+1];a&&o(t+1,a.length-1)}})),e.on("prev",(({fragment:a=!0})=>{if(r(-1)&&a)return o(t,n-1),!1;const i=t-1;e.fragments[i]&&o(i,e.fragments[i].length-1)})),e.on("slide",(({index:t,fragment:n})=>{let r=0;if(void 0!==n){const o=e.fragments[t];if(o){const{length:e}=o;r=-1===n?e-1:Math.min(Math.max(n,0),e-1)}}o(t,r)})),o(0,0)},h=document,y=()=>!(!h.fullscreenEnabled&&!h.webkitFullscreenEnabled),x=()=>!(!h.fullscreenElement&&!h.webkitFullscreenElement),w=e=>{e.fullscreen=()=>{y()&&(async()=>{return x()?null===(e=h.exitFullscreen||h.webkitExitFullscreen)||void 0===e?void 0:e.call(h):((e=h.body)=>{var t;return null===(t=e.requestFullscreen||e.webkitRequestFullscreen)||void 0===t?void 0:t.call(e)})();var e})()},document.addEventListener("keydown",(t=>{"f"!==t.key&&"F11"!==t.key||t.altKey||t.ctrlKey||t.metaKey||!y()||(e.fullscreen(),t.preventDefault())}))},b="bespoke-marp-inactive",k=(e=2e3)=>({parent:t,fire:n})=>{const r=t.classList,o=e=>n(`marp-${e?"":"in"}active`);let a;const i=()=>{a&&clearTimeout(a),a=setTimeout((()=>{r.add(b),o()}),e),r.contains(b)&&(r.remove(b),o(!0))};for(const e of["mousedown","mousemove","touchend"])document.addEventListener(e,i);setTimeout(i,0)},E=["AUDIO","BUTTON","INPUT","SELECT","TEXTAREA","VIDEO"],L=e=>{e.parent.addEventListener("keydown",(e=>{if(!e.target)return;const t=e.target;(E.includes(t.nodeName)||"true"===t.contentEditable)&&e.stopPropagation()}))},$=e=>{window.addEventListener("load",(()=>{for(const t of e.slides){const e=t.querySelector("[data-marp-fitting]")?"":"hideable";t.setAttribute(`${a}load`,e)}}))},P=({interval:e=250}={})=>t=>{document.addEventListener("keydown",(e=>{if(" "===e.key&&e.shiftKey)t.prev();else if("ArrowLeft"===e.key||"ArrowUp"===e.key||"PageUp"===e.key)t.prev({fragment:!e.shiftKey});else if(" "!==e.key||e.shiftKey)if("ArrowRight"===e.key||"ArrowDown"===e.key||"PageDown"===e.key)t.next({fragment:!e.shiftKey});else if("End"===e.key)t.slide(t.slides.length-1,{fragment:-1});else{if("Home"!==e.key)return;t.slide(0)}else t.next();e.preventDefault()}));let n,r,o=0;t.parent.addEventListener("wheel",(a=>{let i=!1;const s=(e,t)=>{e&&(i=i||((e,t)=>((e,t)=>{const n="X"===t?"Width":"Height";return e[`client${n}`]<e[`scroll${n}`]})(e,t)&&((e,t)=>{const{overflow:n}=e,r=e[`overflow${t}`];return"auto"===n||"scroll"===n||"auto"===r||"scroll"===r})(getComputedStyle(e),t))(e,t)),(null==e?void 0:e.parentElement)&&s(e.parentElement,t)};if(0!==a.deltaX&&s(a.target,"X"),0!==a.deltaY&&s(a.target,"Y"),i)return;a.preventDefault();const l=Math.sqrt(a.deltaX**2+a.deltaY**2);if(void 0!==a.wheelDelta){if(void 0===a.webkitForce&&Math.abs(a.wheelDelta)<40)return;if(a.deltaMode===a.DOM_DELTA_PIXEL&&l<4)return}else if(a.deltaMode===a.DOM_DELTA_PIXEL&&l<12)return;r&&clearTimeout(r),r=setTimeout((()=>{n=0}),e);const c=Date.now()-o<e,d=l<=n;if(n=l,c||d)return;let f;(a.deltaX>0||a.deltaY>0)&&(f="next"),(a.deltaX<0||a.deltaY<0)&&(f="prev"),f&&(t[f](),o=Date.now())}))},S=(e=".bespoke-marp-osc")=>{const t=document.querySelector(e);if(!t)return()=>{};const n=(e,n)=>{t.querySelectorAll(`[${a}osc=${JSON.stringify(e)}]`).forEach(n)};return y()||n("fullscreen",(e=>e.style.display="none")),d||n("presenter",(e=>{e.disabled=!0,e.title="Presenter view is disabled due to restricted localStorage."})),e=>{t.addEventListener("click",(t=>{if(t.target instanceof HTMLElement){const{bespokeMarpOsc:n}=t.target.dataset;n&&t.target.blur();const r={fragment:!t.shiftKey};"next"===n?e.next(r):"prev"===n?e.prev(r):"fullscreen"===n?null==e||e.fullscreen():"presenter"===n&&e.openPresenterView()}})),e.parent.appendChild(t),e.on("activate",(({index:t})=>{n("page",(n=>n.textContent=`Page ${t+1} of ${e.slides.length}`))})),e.on("fragment",(({index:t,fragments:r,fragmentIndex:o})=>{n("prev",(e=>e.disabled=0===t&&0===o)),n("next",(n=>n.disabled=t===e.slides.length-1&&o===r.length-1))})),e.on("marp-active",(()=>g(t,!1))),e.on("marp-inactive",(()=>g(t,!0))),y()&&(e=>{for(const t of["","webkit"])h.addEventListener(t+"fullscreenchange",e)})((()=>n("fullscreen",(e=>e.classList.toggle("exit",y()&&x())))))}},I=e=>{window.addEventListener("message",(t=>{if(t.origin!==window.origin)return;const[n,r]=t.data.split(":");if("navigate"===n){const[t,n]=r.split(",");let o=Number.parseInt(t,10),a=Number.parseInt(n,10)+1;a>=e.fragments[o].length&&(o+=1,a=0),e.slide(o,{fragment:a})}}))};var T=["area","base","br","col","command","embed","hr","img","input","keygen","link","meta","param","source","track","wbr"];let A=e=>String(e).replace(/[&<>"']/g,(e=>`&${C[e]};`)),C={"&":"amp","<":"lt",">":"gt",'"':"quot","'":"apos"},N="dangerouslySetInnerHTML",K={className:"class",htmlFor:"for"},O={};function D(e,t){let n=[],r="";t=t||{};for(let e=arguments.length;e-- >2;)n.push(arguments[e]);if("function"==typeof e)return t.children=n.reverse(),e(t);if(e){if(r+="<"+e,t)for(let e in t)!1!==t[e]&&null!=t[e]&&e!==N&&(r+=` ${K[e]?K[e]:A(e)}="${A(t[e])}"`);r+=">"}if(-1===T.indexOf(e)){if(t[N])r+=t[N].__html;else for(;n.length;){let e=n.pop();if(e)if(e.pop)for(let t=e.length;t--;)n.push(e[t]);else r+=!0===O[e]?e:A(e)}r+=e?`</${e}>`:""}return O[r]=!0,r}const M=({children:e})=>D(null,null,...e),q="bespoke-marp-presenter-",_={container:`${q}container`,next:`${q}next`,nextContainer:`${q}next-container`,noteContainer:`${q}note-container`,infoContainer:`${q}info-container`,infoPage:`${q}info-page`,infoPageText:`${q}info-page-text`,infoPagePrev:`${q}info-page-prev`,infoPageNext:`${q}info-page-next`,infoTime:`${q}info-time`,infoTimer:`${q}info-timer`},U=e=>{const{title:t}=document;document.title="[Presenter view]"+(t?` - ${t}`:"");const n={},r=e=>(n[e]=n[e]||document.querySelector(`.${e}`),n[e]);document.body.appendChild((e=>{const t=document.createElement("div");return t.className=_.container,t.appendChild(e),t.insertAdjacentHTML("beforeend",D(M,null,D("div",{class:_.nextContainer},D("iframe",{class:_.next,src:"?view=next"})),D("div",{class:_.noteContainer}),D("div",{class:_.infoContainer},D("div",{class:_.infoPage},D("button",{class:_.infoPagePrev,tabindex:"-1",title:"Previous"},"Previous"),D("span",{class:_.infoPageText}),D("button",{class:_.infoPageNext,tabindex:"-1",title:"Next"},"Next")),D("time",{class:_.infoTime,title:"Current time"}),D("div",{class:_.infoTimer})))),t})(e.parent)),(e=>{r(_.nextContainer).addEventListener("click",(()=>e.next()));const t=r(_.next),n=(o=t,(e,t)=>{var n;return null===(n=o.contentWindow)||void 0===n?void 0:n.postMessage(`navigate:${e},${t}`,"null"===window.origin?"*":window.origin)});var o;t.addEventListener("load",(()=>{r(_.nextContainer).classList.add("active"),n(e.slide(),e.fragmentIndex),e.on("fragment",(({index:e,fragmentIndex:t})=>n(e,t)))}));const a=document.querySelectorAll(".bespoke-marp-note");a.forEach((e=>{e.addEventListener("keydown",(e=>e.stopPropagation())),r(_.noteContainer).appendChild(e)})),e.on("activate",(()=>a.forEach((t=>t.classList.toggle("active",t.dataset.index==e.slide()))))),e.on("activate",(({index:t})=>{r(_.infoPageText).textContent=`${t+1} / ${e.slides.length}`}));const i=r(_.infoPagePrev),s=r(_.infoPageNext);i.addEventListener("click",(t=>{i.blur(),e.prev({fragment:!t.shiftKey})})),s.addEventListener("click",(t=>{s.blur(),e.next({fragment:!t.shiftKey})})),e.on("fragment",(({index:t,fragments:n,fragmentIndex:r})=>{i.disabled=0===t&&0===r,s.disabled=t===e.slides.length-1&&r===n.length-1}));const l=()=>r(_.infoTime).textContent=(new Date).toLocaleTimeString();l(),setInterval(l,250)})(e)},V=e=>{if(!(e=>e.syncKey&&"string"==typeof e.syncKey)(e))throw new Error("The current instance of Bespoke.js is invalid for Marp bespoke presenter plugin.");Object.defineProperties(e,{openPresenterView:{enumerable:!0,value:X},presenterUrl:{enumerable:!0,get:F}}),d&&document.addEventListener("keydown",(t=>{"p"!==t.key||t.altKey||t.ctrlKey||t.metaKey||(t.preventDefault(),e.openPresenterView())}))};function X(){const{max:e,floor:t}=Math,n=e(t(.85*window.innerWidth),640),r=e(t(.85*window.innerHeight),360);return window.open(this.presenterUrl,q+this.syncKey,`width=${n},height=${r},menubar=no,toolbar=no`)}function F(){const e=new URLSearchParams(location.search);return e.set("view","presenter"),e.set("sync",this.syncKey),i(e)}const B=e=>{const t=s();return t===r&&e.appendChild(document.createElement("span")),{"":V,[n]:U,[r]:I}[t]},R=e=>{e.on("activate",(t=>{document.querySelectorAll(".bespoke-progress-parent > .bespoke-progress-bar").forEach((n=>{n.style.flexBasis=100*t.index/(e.slides.length-1)+"%"}))}))},j=e=>{const t=Number.parseInt(e,10);return Number.isNaN(t)?null:t},H=(e={})=>{const t={history:!0,...e};return e=>{let n=!0;const r=e=>{const t=n;try{return n=!0,e()}finally{n=t}},o=(t={fragment:!0})=>{((t,n)=>{const{min:r,max:o}=Math,{fragments:a,slides:i}=e,s=o(0,r(t,i.length-1)),l=o(0,r(n||0,a[s].length-1));s===e.slide()&&l===e.fragmentIndex||e.slide(s,{fragment:l})})((j(location.hash.slice(1))||1)-1,t.fragment?j(l("f")||""):null)};e.on("fragment",(({index:e,fragmentIndex:r})=>{n||c({f:0===r||r.toString()},{location:{...location,hash:`#${e+1}`},setter:(...e)=>t.history?history.pushState(...e):history.replaceState(...e)})})),setTimeout((()=>{o(),window.addEventListener("hashchange",(()=>r((()=>{o({fragment:!1}),c({f:void 0})})))),window.addEventListener("popstate",(()=>{n||r((()=>o()))})),n=!1}),0)}},Y=(e={})=>{var n;const r=e.key||(null===(n=window.history.state)||void 0===n?void 0:n.marpBespokeSyncKey)||Math.random().toString(36).slice(2),o=`bespoke-marp-sync-${r}`;var a;a={marpBespokeSyncKey:r},c({},{setter:(e,...n)=>t({...e,...a},...n)});const i=()=>{const e=f(o);return e?JSON.parse(e):Object.create(null)},s=e=>{const t=i(),n={...t,...e(t)};return u(o,JSON.stringify(n)),n},l=()=>{window.removeEventListener("pageshow",l),s((e=>({reference:(e.reference||0)+1})))};return e=>{l(),Object.defineProperty(e,"syncKey",{value:r,enumerable:!0});let t=!0;setTimeout((()=>{e.on("fragment",(e=>{t&&s((()=>({index:e.index,fragmentIndex:e.fragmentIndex})))}))}),0),window.addEventListener("storage",(n=>{if(n.key===o&&n.oldValue&&n.newValue){const r=JSON.parse(n.oldValue),o=JSON.parse(n.newValue);if(r.index!==o.index||r.fragmentIndex!==o.fragmentIndex)try{t=!1,e.slide(o.index,{fragment:o.fragmentIndex})}finally{t=!0}}}));const n=()=>{const{reference:e}=i();void 0===e||e<=1?m(o):s((()=>({reference:e-1})))};window.addEventListener("pagehide",(e=>{e.persisted&&window.addEventListener("pageshow",l),n()})),e.on("destroy",n)}},{PI:J,abs:W,sqrt:z,atan2:G}=Math,Q={passive:!0},Z=({slope:e=-.7,swipeThreshold:t=30}={})=>n=>{let r;const o=n.parent,a=e=>{const t=o.getBoundingClientRect();return{x:e.pageX-(t.left+t.right)/2,y:e.pageY-(t.top+t.bottom)/2}};o.addEventListener("touchstart",(({touches:e})=>{r=1===e.length?a(e[0]):void 0}),Q),o.addEventListener("touchmove",(e=>{if(r)if(1===e.touches.length){e.preventDefault();const t=a(e.touches[0]),n=t.x-r.x,o=t.y-r.y;r.delta=z(W(n)**2+W(o)**2),r.radian=G(n,o)}else r=void 0})),o.addEventListener("touchend",(o=>{if(r){if(r.delta&&r.delta>=t&&r.radian){const t=(r.radian-e+J)%(2*J)-J;n[t<0?"next":"prev"](),o.stopPropagation()}r=void 0}}),Q)},ee="_tA",te=e=>{const t=document.documentTransition;if(!t)return;let n;e._tP=!1;const r=(n,{back:r,cond:o})=>a=>{const i=e.slides[e.slide()].querySelector("section[data-transition]");if(!i)return!0;const s=document.querySelector(".bespoke-marp-osc"),l=s?[s]:void 0;if(e._tP){if(a._tA){e._tP=!1;try{t.start({sharedElements:l}).catch((()=>{}))}catch(e){}return!0}}else{if(!o(a))return!0;e._tP=t.prepare({rootTransition:a.back||r?i.dataset.transitionBack:i.dataset.transition,sharedElements:l}).then((()=>n(a))).catch((()=>n(a)))}return!1};e.on("prev",r((t=>e.prev({...t,[ee]:!0})),{back:!0,cond:e=>{var t;return e.index>0&&!((null===(t=e.fragment)||void 0===t||t)&&n.fragmentIndex>0)}})),e.on("next",r((t=>e.next({...t,[ee]:!0})),{cond:t=>t.index+1<e.slides.length&&!(n.fragmentIndex+1<n.fragments.length)})),setTimeout((()=>{e.on("slide",r((t=>e.slide(t.index,{...t,[ee]:!0})),{cond:t=>{const n=e.slide();return t.index!==n&&(t.back=t.index<n,!0)}}))}),0),e.on("fragment",(e=>{n=e}))};let ne;const re=()=>(void 0===ne&&(ne="wakeLock"in navigator&&navigator.wakeLock),ne),oe=async()=>{const e=re();if(e)try{return await e.request("screen")}catch(e){console.warn(e)}return null},ae=async()=>{if(!re())return;let e;const t=()=>{e&&"visible"===document.visibilityState&&oe()};for(const e of["visibilitychange","fullscreenchange"])document.addEventListener(e,t);return e=await oe(),e};((t=document.getElementById("p"))=>{(()=>{const t=l("view");e.dataset.bespokeView=t===r||t===n?t:""})();const a=(e=>{const t=l(e);return c({[e]:void 0}),t})("sync")||void 0;var i,d,f,u,m,g,h,y,x,b,E,I;i=t,d=((...e)=>{const t=o.findIndex((e=>s()===e));return e.map((([e,n])=>e[t]&&n)).filter((e=>e))})([[1,1,0],Y({key:a})],[[1,1,1],B(t)],[[1,1,0],L],[[1,1,1],p],[[1,0,0],k()],[[1,1,1],$],[[1,1,1],H({history:!1})],[[1,1,0],P()],[[1,1,0],w],[[1,0,0],R],[[1,1,0],Z()],[[1,0,0],S()],[[1,0,0],te],[[1,1,1],v],[[1,1,0],ae]),u=1===(i.parent||i).nodeType?i.parent||i:document.querySelector(i.parent||i),m=[].filter.call("string"==typeof i.slides?u.querySelectorAll(i.slides):i.slides||u.children,(function(e){return"SCRIPT"!==e.nodeName})),g={},h=function(e,t){return(t=t||{}).index=m.indexOf(e),t.slide=e,t},b=function(e,t){m[e]&&(f&&x("deactivate",h(f,t)),f=m[e],x("activate",h(f,t)))},E=function(e,t){var n=m.indexOf(f)+e;x(e>0?"next":"prev",h(f,t))&&b(n,t)},I={off:y=function(e,t){g[e]=(g[e]||[]).filter((function(e){return e!==t}))},on:function(e,t){return(g[e]||(g[e]=[])).push(t),y.bind(null,e,t)},fire:x=function(e,t){return(g[e]||[]).reduce((function(e,n){return e&&!1!==n(t)}),!0)},slide:function(e,t){if(!arguments.length)return m.indexOf(f);x("slide",h(m[e],t))&&b(e,t)},next:E.bind(null,1),prev:E.bind(null,-1),parent:u,slides:m,destroy:function(e){x("destroy",h(f,e)),g={}}},(d||[]).forEach((function(e){e(I)})),f||b(0)})()}();</script></body></html> \ No newline at end of file
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/slide/note.md Fri Jan 07 00:58:07 2022 +0900 @@ -0,0 +1,122 @@ +<!--カンペだよ--> + +# タイトル + +Gears Agdaにおける +Left Learning Red Black Tree の検証について + +琉球大学 並列信頼研究室の上地が発表します + +# 目的 +そのまま読む + +# CbC +もそのまま読む + +# Agda +もそのまま読む + +# Agda の基本 +Agda の基本となる型の１つである Data 型について説明します + +record Env とあるところで Env という Record 型を定義 +することを示しています + +そしてその中にvarnとvariがあり、その型が自然数であることを定義しています + +次に、記述する際の導入が以下のようになり +varxに0を、variに1を定義しています + +導入後は変数 スペース record名でその中身にアクセスできます + +# Gears Agda の記法 +何と対応しているからLoopで記述するんだっけ + +Agdaの構文的に禁止していないので再帰呼び出しは使用しないよう注意が必要です + +以下がwhile loopのノーマルレベルでの記述になります + +まず型の方で +Envを受け取り、Codeを受け取り、 +tを返すといった流れになっています + +このCodeはEnvを受け取った後にｔを返すというものです + +次に、入力を env next で受け取っています + +このcodeは後で再び説明するので、withの方はおいておいてください + +パターンマッチの方で、false trueの場合をかんがえています +これはfalseの場合はnextにenvを渡します +nextはenvを受け取ってtを返すので正しいです +これがtを返すことでこの後も関数が続くこと、継続を示します + + +# Gears Agdaと Gears CbCの対応 +そのまま読むでよさそう +Contextだけ調べた方がよいかも + + +# Normal levelと～ +今回検証に使用するHoare Conditionと証明も Meta levelです + +画像はよなおせ + +# Hoare logic +プログラム が事前条件 P に関して停止し、停止後には必ず事後条件 Q が成り立つならば、プログラム S は、事前条件 P と事後条件 Q とに関して正当（correct）であるという + +簡単な例としてGears Agdaにてwhile loopを検証します + +以下のコードを詳細に説明します + +入力と出力に関しては前述しました +このたーみねーてぃんぐはこの関数が停止することを示しています +この実装ではagdaはloopが終了するのかわからず、コンパイルできないので +このあのてーとをつけて停止することを明示します + +with文は引数であたえられた値を展開します。 +今回はその値をパターンマッチしています。 + +これがless than で0とvarnを比較しています + +このwhileloopは、 +varnがこれからループする回数で、variがループした回数になります + +なので、これが0になると終了し次の関数であるnextに遷移し +0でないならループする回数varxから今回分の１引いて +variには今回分の1を足したものをEnvとしてもう一度関数を実行するという記述になっています + +# post condition +先ほど実装したノーマルレベルなwhile loopに対して +事前条件となるPre / Post Condition を追加した実装をします + +そのまえにterminatingが付いていると停止性の証明をしたことにはならないので～ + + +このconditionはループしたい回数は +これからループする回数とループした回数の和と等しいというものです + +exitのPostConditionもつけるべきだな… + +# loopの接続 +loopが前のページのWhile LoopSeg だな + +loopの部分の証明のみだな + +# 実際のloopの接続 +最終的にはループした回数が入力のループしたい回数と一致していることを +証明したいので以下のようになります + +で、前回のものは最初から構造体（record）に値が格納されている状態から始まっていたので +proofGearsTermS では、入力が自然数で、recordの定義から検証を行っている + +そしてそれを行っているのが最初の関数であるwhileTest'で +ここでvarnが入力c10と一致し、variが0であることを証明している + +次の関数であるversionでは、whileTest'のrecord定義時のConditionから +loop時のconditionを生成しています + +# testとの違い +そのまま読むよ + +Condition
--- a/slide/slide.md Thu Jan 06 16:57:53 2022 +0900 +++ b/slide/slide.md Fri Jan 07 00:58:07 2022 +0900 @@ -76,7 +76,6 @@ # Agda の基本 - Agdaとは定理証明支援器であり、関数型言語 - Agdaでの関数は、最初に型について定義した後に、関数を定義する事で記述する - - これが Curry-Howard 対応となる - 型の定義部分で、入力と出力の型を定義できる - input → output のようになる - 関数の定義は = を用いて行う @@ -104,11 +103,11 @@ 型に対応する値の導入(intro) ``` -record {varx = zero ; vary = suc zero} +record {varn = zero ; vari = suc zero} ``` record の値のアクセス(elim) ``` -(env : Env) → varx env +(env : Env) → varn env ``` @@ -116,7 +115,7 @@ # Gears Agda の記法 Gears Agda では CbC と対応させるためにすべてLoopで記述する loopは`→ t`の形式で表現する -再起呼び出しは使わない(構文的には禁止していないので注意が必要) +再帰呼び出しは使わない(構文的には禁止していないので注意が必要) ``` {-# TERMINATING #-} whileLoop : {l : Level} {t : Set l} → Env → (Code : Env → t) → t @@ -174,7 +173,6 @@ ``` - `{-# TERMINATING #-}` - with 文 -- 型と値 # Gears Agda の Pre Condition Post Condition ``` @@ -220,7 +218,6 @@ (λ ne pe → whileTestSpec1 c10 ne pe)) n1 p1 )) ``` - conversion1はPre Condition をPost Conditionに変換する -- whileLoopSeg - ⊤ # test との違い @@ -445,14 +442,17 @@ - Red Black Tree の実装 - 今回定義した条件はそのまま Red Black Tree の検証に使用できるはず - Contextを用いた並列実行時のプログラムの正しさの証明 - - syncronized queue - - concarent tree + - synchronized queue + - concurrent tree - xv.6への適用 - モデル検査 +読めない間は待っている +tree + # まとめ - Gears Agda にて Binary Tree を検証することができた - - Gears Agda における Termination を使用しない実装の仕方を確率した + - Gears Agda における Termination を使用しない実装の仕方を確立した - Hoare Logic による検証もできるようになった - 今後は Red Black Tree の検証をすすめる - モデル検査をしたい