Mercurial > hg > Papers > 2019 > ryokka-sigss
changeset 3:100e82a436f6
modify mindmap
| author | ryokka |
|---|---|
| date | Sun, 16 Dec 2018 19:33:11 +0900 |
| parents | 81e2a6af901e |
| children | 8189d4b8f2ac |
| files | ryokka-sigss.mm |
| diffstat | 1 files changed, 75 insertions(+), 4 deletions(-) [+] |
line wrap: on
line diff
--- a/ryokka-sigss.mm Sun Dec 16 18:19:33 2018 +0900 +++ b/ryokka-sigss.mm Sun Dec 16 19:33:11 2018 +0900 @@ -1,4 +1,4 @@ -<map version="1.1.0"> +<map version="1.0.1"> <!-- To view this file, download free mind mapping software FreeMind from http://freemind.sourceforge.net --> <node CREATED="1542710800707" ID="ID_311099003" MODIFIED="1542710817736" TEXT="HoareLogic を用いた CbC の検証"> <node CREATED="1542710937504" ID="ID_569346512" MODIFIED="1542710954774" POSITION="right" TEXT="目次"> @@ -33,17 +33,88 @@ <node CREATED="1544604295278" ID="ID_1571024257" MODIFIED="1544604451101" TEXT="Curry Howard とか書いたほうがいい?"/> <node CREATED="1544604345175" ID="ID_1245079261" MODIFIED="1544604485703" TEXT="Agda での証明"/> </node> -</node> <node CREATED="1542710855615" ID="ID_633104128" MODIFIED="1544605442284" TEXT="GearsOSとAgda"> <node CREATED="1544603433154" ID="ID_1178446548" MODIFIED="1544603443456" TEXT="CbC について"/> <node CREATED="1544603444224" ID="ID_1582475028" MODIFIED="1544603454233" TEXT="CodeGear, DataGear"/> <node CREATED="1544603454927" ID="ID_1017938996" MODIFIED="1544604274110" TEXT="Agda での CodeGear, DataGear(継続渡し記述の説明も)"/> <node CREATED="1544604389725" ID="ID_1200091175" MODIFIED="1544604415749" TEXT="Agda での CbC の検証"/> </node> +<node CREATED="1544955510685" ID="ID_1378359833" MODIFIED="1544955531798" TEXT="等式変形の証明"> +<node CREATED="1544955536030" ID="ID_1351263237" MODIFIED="1544955550375" TEXT="x==y を証明したい"/> +<node CREATED="1544955552292" ID="ID_1396517005" MODIFIED="1544955578075" TEXT="Reasoning を 三つの ? でかく"/> +<node CREATED="1544955585146" ID="ID_569206138" MODIFIED="1544955596370" TEXT="二つ目を見ると前後に必要な式がわかる"/> +<node CREATED="1544955597250" ID="ID_1715686699" MODIFIED="1544955611283" TEXT="変形する式を羅列する"/> +<node CREATED="1544955612652" ID="ID_985696591" MODIFIED="1544955630412" TEXT="変形する推論規則(x==x1)"> +<node CREATED="1544955633523" ID="ID_1341233417" MODIFIED="1544955646711" TEXT="x1==y を証明すれば良い"/> +</node> +</node> +</node> <node CREATED="1542710864438" ID="ID_1474492130" MODIFIED="1542710910000" TEXT="HoareLogic"> -<node CREATED="1544603812282" ID="ID_1914859833" MODIFIED="1544603912739" TEXT="Agda での Hoare Logic の実装"/> -<node CREATED="1544603916933" ID="ID_912615419" MODIFIED="1544603949220" TEXT="CodeGear, DataGear を用いたスタイルと Hoare Logic"/> +<node CREATED="1544952943134" ID="ID_10179037" MODIFIED="1544952949971" TEXT="While Program"> +<node CREATED="1544952991409" ID="ID_596599032" MODIFIED="1544952997567" TEXT="Skip"/> +<node CREATED="1544952998071" ID="ID_1502092759" MODIFIED="1544953002143" TEXT="Abort"/> +<node CREATED="1544953002729" ID="ID_652512656" MODIFIED="1544953004935" TEXT="Seq"/> +<node CREATED="1544953005280" ID="ID_1999779347" MODIFIED="1544953009167" TEXT="PComm"/> +<node CREATED="1544953009656" ID="ID_143829516" MODIFIED="1544953010671" TEXT="If"/> +<node CREATED="1544953010967" ID="ID_1707380993" MODIFIED="1544953012496" TEXT="While"/> +</node> +<node CREATED="1544953033123" ID="ID_1125077236" MODIFIED="1544953048274" TEXT="PreCondition Command PostCondition"> +<node CREATED="1544953059289" ID="ID_554375384" MODIFIED="1544953065212" TEXT="HTProof"> +<node CREATED="1544953087539" ID="ID_500044924" MODIFIED="1544953091662" TEXT="SkipRule"/> +<node CREATED="1544953092210" ID="ID_1398126479" MODIFIED="1544953097342" TEXT="AbortRule"/> +<node CREATED="1544953097973" ID="ID_1347734292" MODIFIED="1544953100799" TEXT="SeqRule"/> +<node CREATED="1544953101143" ID="ID_810877387" MODIFIED="1544953114392" TEXT="PrimCommRule"/> +<node CREATED="1544953115159" ID="ID_1693437242" MODIFIED="1544953119888" TEXT="IfRule"/> +<node CREATED="1544953120428" ID="ID_403099872" MODIFIED="1544953122745" TEXT="WhileRule"/> +<node CREATED="1544953131201" ID="ID_1694881778" MODIFIED="1544953193197" TEXT="WeakningRule"/> +</node> +<node CREATED="1544953067155" ID="ID_991425650" MODIFIED="1544953077405" TEXT="Axiom "/> +<node CREATED="1544953078010" ID="ID_1967448460" MODIFIED="1544953082901" TEXT="Totology"/> +</node> +<node CREATED="1544953213492" ID="ID_1313761757" MODIFIED="1544953220280" TEXT="Example"/> +<node CREATED="1544954625664" ID="ID_856350466" MODIFIED="1544954638560" TEXT="証明の手順"> +<node CREATED="1544954639048" ID="ID_707405060" MODIFIED="1544954655114" TEXT="Programに沿ってルールを構築する"/> +<node CREATED="1544954656137" ID="ID_1099647645" MODIFIED="1544954693892" TEXT="While Program に相似なProgram の構築方法になる"/> +<node CREATED="1544954695449" ID="ID_167702231" MODIFIED="1544954726159" TEXT="ルールの Axiom 部分を ? とすると証明すべき論理式が得られる"/> +<node CREATED="1544954728375" ID="ID_733013199" MODIFIED="1544954791492" TEXT="証明をラムダこうとして構築する"/> +<node CREATED="1544954794025" ID="ID_1862482735" MODIFIED="1544954833648" TEXT="Invaliant のように PostCondition と PreCondition が合わない場合は"> +<node CREATED="1544954837647" ID="ID_605650861" MODIFIED="1544954853144" TEXT="WeakningRuleを使う"/> </node> +<node CREATED="1544954861191" ID="ID_1632760763" MODIFIED="1544954884779" TEXT="すべてが接続されると証明が終わる"/> +<node CREATED="1544954887674" ID="ID_49477826" MODIFIED="1544954897316" TEXT="停止性はここではまだ証明していない"> +<node CREATED="1544954900504" ID="ID_333078697" MODIFIED="1544954920046" TEXT="Agda では TERMINATING というアノテーションで抑制する"/> +</node> +</node> +<node CREATED="1544603916933" ID="ID_912615419" MODIFIED="1544953262787" TEXT="CodeGear, DataGear"> +<node CREATED="1544953301023" ID="ID_1936819038" MODIFIED="1544953341105" TEXT="add PreCondition to CodeGear Argument"/> +<node CREATED="1544953364369" ID="ID_1897331085" MODIFIED="1544953383252" TEXT="use Conversion CodeGear as a WeakningRule"/> +</node> +<node CREATED="1544953390779" ID="ID_1221989718" MODIFIED="1544953393861" TEXT="Example"/> +</node> +<node CREATED="1544953534749" ID="ID_757078127" MODIFIED="1544953544019" TEXT="比較と評価"> +<node CREATED="1544953548644" ID="ID_660804708" MODIFIED="1544953586327" TEXT="HoareLogic は Program の構造と証明が別"/> +<node CREATED="1544953593558" ID="ID_1222836750" MODIFIED="1544953605696" TEXT="停止性はまだ未実装"/> +<node CREATED="1544953607664" ID="ID_1418415681" MODIFIED="1544953624184" TEXT="CodeGear"> +<node CREATED="1544953624446" ID="ID_1333500913" MODIFIED="1544953647627" TEXT="Program と証明が対応してる"/> +<node CREATED="1544953649212" ID="ID_1043705676" MODIFIED="1544953685286" TEXT="while Program と違ってCodeGearの記述が自由"/> +<node CREATED="1544953687507" ID="ID_213969675" MODIFIED="1544953714064" TEXT="証明がメタ計算の入力と出力に対応する"/> +<node CREATED="1544953717022" ID="ID_960276791" MODIFIED="1544953734255" TEXT="入力がPreCondition で"/> +<node CREATED="1544953736673" ID="ID_13390002" MODIFIED="1544953757401" TEXT="継続の呼び出しが PostCondition になる"/> +</node> +<node CREATED="1544953777092" ID="ID_1972622252" MODIFIED="1544953797711" TEXT="CodeGearでHoareLogic を簡潔に記述できることがわかった"/> +</node> +<node CREATED="1544953399717" ID="ID_1659003334" MODIFIED="1544953407985" TEXT="将来の課題"> +<node CREATED="1544953411825" ID="ID_1766627105" MODIFIED="1544953435986" TEXT="HoareLogic 部分をメタ計算として記述"/> +<node CREATED="1544953456250" ID="ID_37105044" MODIFIED="1544953464613" TEXT="元の計算の記述を保存する"/> +<node CREATED="1544953465598" ID="ID_454238122" MODIFIED="1544953488516" TEXT="RedBlackTree"/> +<node CREATED="1544953489813" ID="ID_286112576" MODIFIED="1544953506149" TEXT="Synchronized Queue"> +<node CREATED="1544953803400" ID="ID_1363325581" MODIFIED="1544953823216" TEXT="並列プログラムを状態遷移に変換する"/> +<node CREATED="1544953824288" ID="ID_649570454" MODIFIED="1544953862724" TEXT="Temporal Logic なプロパティを状態遷移として記述する"/> +<node CREATED="1544953864581" ID="ID_1141579119" MODIFIED="1544953928385" TEXT="Omega Automaton の受理条件として証明する"/> +</node> +<node CREATED="1544953525955" ID="ID_796699968" MODIFIED="1544953529433" TEXT="GearsOS"/> +</node> +<node CREATED="1544952979891" ID="ID_1616071429" MODIFIED="1544952986481" TEXT="まとめ"/> </node> <node CREATED="1542710960435" ID="ID_167048397" MODIFIED="1542710984521" POSITION="right" TEXT="研究"/> </node>