Mercurial > hg > Papers > 2018 > nozomi-master
changeset 147:d7b8a5d1252f
remove file
| author | Nozomi Teruya <e125769@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sat, 06 Jan 2018 19:07:03 +0900 |
| parents | a2aaf1d0bf01 |
| children | cf9c3be20362 |
| files | index.mm paper/agda.tex paper/akasha.tex paper/atton-master.pdf paper/atton-master.tex paper/cbc-type.tex paper/cbc.tex paper/history.tex paper/nozomi-master.pdf paper/signature.pdf paper/sources.tex paper/src/AgdaBasics.agda paper/src/AgdaBool.agda paper/src/AgdaElem.agda paper/src/AgdaElemApply.agda paper/src/AgdaFunction.agda paper/src/AgdaId.agda paper/src/AgdaImplicitId.agda paper/src/AgdaImport.agda paper/src/AgdaInstance.agda paper/src/AgdaLambda.agda paper/src/AgdaModusPonens.agda paper/src/AgdaNPushNPop.agda paper/src/AgdaNPushNPopProof.agda paper/src/AgdaNat.agda paper/src/AgdaNot.agda paper/src/AgdaParameterizedModule.agda paper/src/AgdaPattern.agda paper/src/AgdaPlus.agda paper/src/AgdaProduct.agda paper/src/AgdaProp.agda paper/src/AgdaPushPop.agda paper/src/AgdaPushPopProof.agda paper/src/AgdaRecord.agda paper/src/AgdaRecordProj.agda paper/src/AgdaStack.agda paper/src/AgdaStackDS.agda paper/src/AgdaTypeClass.agda paper/src/AgdaWhere.agda paper/src/CodeSegment.agda paper/src/CodeSegments.agda paper/src/DataSegment.agda paper/src/Eq.Agda paper/src/Equiv.agda paper/src/Exec.agda paper/src/Goto.agda paper/src/Maybe.agda paper/src/MetaCodeSegment.agda paper/src/MetaDataSegment.agda paper/src/MetaMetaCodeSegment.agda paper/src/MetaMetaDataSegment.agda paper/src/Nat.agda paper/src/NatAdd.agda paper/src/NatAddSym.agda paper/src/PushPopType.agda paper/src/Reasoning.agda paper/src/SingleLinkedStack.cbc paper/src/ThreePlusOne.agda paper/src/akashaContext.h paper/src/akashaMeta.c paper/src/assert.c paper/src/atton-master-meta-sample.agda paper/src/atton-master-sample.agda paper/src/cbmc-assert.c paper/src/context.h paper/src/enumerate-inputs.c paper/src/expr-term.txt paper/src/factrial.cbc paper/src/getMinHeight.c paper/src/goto.cbc paper/src/initLLRBContext.c paper/src/insertCase2.c paper/src/meta.c paper/src/rbtreeContext.h paper/src/singleLinkedStack.c paper/src/stack-product.agda paper/src/stack-subtype-sample.agda paper/src/stack-subtype.agda paper/src/stack.h paper/src/struct-init.c paper/src/struct.c paper/src/stub.cbc paper/src/subtype.agda paper/src/type-cs.c paper/src/type-ds.h paper/src/type-mds.h paper/副本.pdf paper/正本.pdf paper/背表紙.pdf paper/表紙.pdf |
| diffstat | 90 files changed, 90 insertions(+), 3359 deletions(-) [+] |
line wrap: on
line diff
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/index.mm Sat Jan 06 19:07:03 2018 +0900 @@ -0,0 +1,90 @@ +<map version="1.0.1"> +<!-- To view this file, download free mind mapping software FreeMind from http://freemind.sourceforge.net --> +<node CREATED="1512456732213" ID="ID_890440834" MODIFIED="1512456746030" TEXT="分散フレームワークChristieの設計"> +<node CREATED="1512456770597" ID="ID_832101674" MODIFIED="1512456821597" POSITION="right" TEXT="研究目的"> +<node CREATED="1512457195813" ID="ID_1859750393" MODIFIED="1512457216791" TEXT="分散プログラミングの信頼性向上"/> +<node CREATED="1512457225372" ID="ID_835750853" MODIFIED="1512460412400" TEXT="CSとDSを用いたプログラミング"/> +<node CREATED="1512457217499" ID="ID_1872250590" MODIFIED="1512460453092" TEXT="Aliceを作成した"/> +<node CREATED="1512460509028" ID="ID_1810651531" MODIFIED="1512460680057" TEXT="シンプルに拡張性高く記述できる環境の必要性"/> +<node CREATED="1512460803818" ID="ID_1205467497" MODIFIED="1512460807420" TEXT="メタを実装した"/> +<node CREATED="1512457230570" ID="ID_1571884420" MODIFIED="1512460432675" TEXT="Aliceの成果と問題点"/> +<node CREATED="1512457235327" ID="ID_1111066763" MODIFIED="1512458999970" TEXT="Christieの設計しプロトタイプを実装する"/> +</node> +<node CREATED="1512456776555" ID="ID_106984894" MODIFIED="1512459010262" POSITION="left" TEXT="Aliceの問題点"> +<node CREATED="1512457149099" ID="ID_31182128" MODIFIED="1512457155410" TEXT="APIがわかりづらい"> +<node CREATED="1512457663036" ID="ID_402965930" MODIFIED="1512457671037" TEXT="create/setKey"/> +<node CREATED="1512457671366" ID="ID_1634916310" MODIFIED="1512457678862" TEXT="動的なsetKeyができる"/> +<node CREATED="1512464836716" ID="ID_403642153" MODIFIED="1512464843720" TEXT="asClassしないといけない"/> +<node CREATED="1512466981943" ID="ID_1385830591" MODIFIED="1512466994922" TEXT="asClassのとき指定する型がわからない"/> +</node> +<node CREATED="1512457314485" ID="ID_1266494639" MODIFIED="1512457341115" TEXT="DSMが複数立ち上げられない"> +<node CREATED="1512459427043" ID="ID_863203050" MODIFIED="1512459429904" TEXT="テストが煩雑になる"/> +<node CREATED="1512457341737" ID="ID_571695417" MODIFIED="1512459426250" TEXT="NAT超えを実装しようとしてできなかった"/> +<node CREATED="1512457353443" ID="ID_61410781" MODIFIED="1512459442824" TEXT="static抜こうとしたけど抜static抜こうとしたけど抜けなかった けなかった"/> +</node> +<node CREATED="1512457390756" ID="ID_1372747247" MODIFIED="1512457408748" TEXT="TopologyManagerのManagerが必要"/> +<node CREATED="1512459206943" ID="ID_1504699433" MODIFIED="1512459211178" TEXT="永続性"/> +</node> +<node CREATED="1512457158023" ID="ID_1273481367" MODIFIED="1512459029974" POSITION="left" TEXT="Christieの設計"> +<node CREATED="1512457188059" ID="ID_1851286703" MODIFIED="1512457417082" TEXT="APIの改善"> +<node CREATED="1512458193024" ID="ID_870262193" MODIFIED="1512458248476" TEXT="Annotationを用いたsetKey"> +<node CREATED="1512458258940" ID="ID_1086285716" MODIFIED="1512458274786" TEXT="DSMのkey指定がなくなる"/> +<node CREATED="1512461230211" ID="ID_1853592762" MODIFIED="1512461445296" TEXT="メタの指定もAnnotationでできる"/> +<node CREATED="1512964413666" ID="ID_1219010229" MODIFIED="1512964421366" TEXT="javassistはできなかった"/> +</node> +<node CREATED="1512457418327" ID="ID_1788593872" MODIFIED="1512458218403" TEXT="書き方の例題"/> +<node CREATED="1512458164522" ID="ID_138685590" MODIFIED="1512458171955" TEXT="メタでasClassする"/> +<node CREATED="1512457429330" ID="ID_1132035018" MODIFIED="1512457695521" TEXT="動的なsetKeyを禁止する"/> +</node> +<node CREATED="1512458309209" ID="ID_464367874" MODIFIED="1512458327907" TEXT="DSMを引数で持ち歩く"/> +</node> +<node CREATED="1512458305365" ID="ID_1754252786" MODIFIED="1512459031036" POSITION="left" TEXT="Christieの評価"> +<node CREATED="1512458338159" ID="ID_1323033547" MODIFIED="1512458346586" TEXT="シンプルさの測定"> +<node CREATED="1512461170115" ID="ID_487155475" MODIFIED="1512461173605" TEXT="実験内容"/> +<node CREATED="1512461176450" ID="ID_1204165433" MODIFIED="1512461179002" TEXT="実験結果"/> +</node> +<node CREATED="1512459099409" ID="ID_1147670794" MODIFIED="1512459107553" TEXT="他フレームワークとの比較"> +<node CREATED="1512469478718" ID="ID_104406562" MODIFIED="1512469482049" TEXT="Corba"/> +<node CREATED="1512469482527" ID="ID_1242782697" MODIFIED="1512469484085" TEXT="Akka"/> +<node CREATED="1512469526406" ID="ID_1909895355" MODIFIED="1512469534732" TEXT="Erlang"/> +</node> +</node> +<node CREATED="1512459160888" ID="ID_165563938" MODIFIED="1512459174383" POSITION="left" TEXT="まとめ"/> +<node CREATED="1512459155781" ID="ID_423223494" MODIFIED="1512459159181" POSITION="left" TEXT="今後の課題"> +<node CREATED="1512459602523" ID="ID_1145326867" MODIFIED="1512459609910" TEXT="分散環境での測定"/> +<node CREATED="1512459233979" ID="ID_1657764184" MODIFIED="1512459240435" TEXT="Gearsへの移行"/> +</node> +<node CREATED="1445921942785" ID="ID_1662142999" MODIFIED="1512459025026" POSITION="right" TEXT="Aliceの概要"> +<node CREATED="1445923082853" HGAP="26" ID="ID_1386409070" MODIFIED="1448709505560" TEXT="CSとDS" VSHIFT="5"> +<node CREATED="1445926774851" ID="ID_774091212" MODIFIED="1445926781353" TEXT="依存関係を記述"/> +<node CREATED="1445926781984" ID="ID_1384910420" MODIFIED="1445926789891" TEXT="InputDSとOutputDS"/> +<node CREATED="1445926819925" ID="ID_126605196" MODIFIED="1512456870345" TEXT="APIで操作する"/> +<node CREATED="1445926858144" ID="ID_754564617" MODIFIED="1445926887987" TEXT="依存関係がなければ並列実行可能"/> +<node CREATED="1445932275207" ID="ID_1944439207" MODIFIED="1445932284209" TEXT="DSはCSに専有される"/> +<node CREATED="1445931799886" ID="ID_1795589283" MODIFIED="1445931828202" TEXT="AliceはJavaで実装されているのでDSはJavaObject、CSはRannableThread"/> +<node CREATED="1448717629517" ID="ID_479450498" MODIFIED="1448717637105" TEXT="DSManager"> +<node CREATED="1448717637106" ID="ID_1945213625" MODIFIED="1448717640158" TEXT="Local"/> +<node CREATED="1448717640647" ID="ID_1642476151" MODIFIED="1448717643425" TEXT="Remote"/> +<node CREATED="1445923096032" ID="ID_208005271" MODIFIED="1448717653420" TEXT="DataSegmentAPI"> +<node CREATED="1445926561228" ID="ID_921169672" MODIFIED="1445926639024" TEXT="DSM名とkeyで指定"/> +<node CREATED="1445926570220" ID="ID_1391127764" MODIFIED="1445926628915" TEXT="put/update"/> +<node CREATED="1445926610739" ID="ID_1307715047" MODIFIED="1445933128813" TEXT="peek/take"/> +<node CREATED="1445932866707" ID="ID_1106088614" MODIFIED="1445932870391" TEXT="asClass()"/> +</node> +</node> +<node CREATED="1445933045088" ID="ID_297106986" MODIFIED="1448717652555" TEXT="CodeSegmentの記述方法"> +<node CREATED="1445933179322" ID="ID_910557017" MODIFIED="1445933194427" TEXT="例題のソースコードを記載"/> +<node CREATED="1445933073234" ID="ID_1603356267" MODIFIED="1445933074518" TEXT="CS を継承して記述 する"/> +<node CREATED="1445933075023" ID="ID_766309004" MODIFIED="1445933078655" TEXT="StartCS"/> +<node CREATED="1445933133409" ID="ID_1910313006" MODIFIED="1445933138694" TEXT="create/setKey"/> +</node> +</node> +<node CREATED="1512457018961" ID="ID_705249785" MODIFIED="1512457024443" TEXT="TopologyManager"> +<node CREATED="1512460319034" ID="ID_1389406658" MODIFIED="1512460327439" TEXT="静的"/> +<node CREATED="1512460312622" ID="ID_743788058" MODIFIED="1512460318405" TEXT="動的"/> +<node CREATED="1512460337913" ID="ID_149855751" MODIFIED="1512460343295" TEXT="KeepAlive"/> +<node CREATED="1513073343141" ID="ID_766143205" MODIFIED="1513073348346" TEXT="NAT超えできなかった"/> +</node> +</node> +</node> +</map>
--- a/paper/agda.tex Sat Jan 06 19:04:39 2018 +0900 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,629 +0,0 @@ -\chapter{証明支援系言語 Agda による証明手法} -\label{chapter:agda} -\ref{chapter:type}章ではCbCにおける CodeSegment と DataSegment が部分型で定義できることを示した。 - -型システムは Curry-Howard 同型対応により命題と型付きラムダ計算が一対一に対応する。 -依存型という型を持つ証明支援系言語 Agda を用いて型システムで証明が行なえることを示す。 - -% {{{ 依存型を持つ証明支援系言語 Agda - -\section{依存型を持つ証明支援系言語 Agda} -型システムを用いて証明を行なうことができる言語に Agda~\cite{agda} が存在する。 -Agda は依存型という強力な型システムを持っている。 -依存型とは型も第一級オブジェクトとする型システムであり、型の型や型を引数に取る関数、値を取って型を返す関数などが記述できる。 -この節では Agda の文法的な紹介を行なう~\cite{Norell:2009:DTP:1481861.1481862}~\cite{agda-documentation}。 - -Agda はインデントに意味を持つ言語であるため、インデントはきちんと揃える必要がある。 -また、非常に多くの記号を利用できる言語であり、スペースの有無は厳格にチェックされる。 -なお、 \verb/--/ の後はコメントである。 - -まず、Agda のプログラムを記述するファイルを作成する。 -Agda のプログラムは全てモジュール内部に記述されるため、まずはトップレベルにモジュールを定義する必要がある。 -トップレベルのモジュールはファイル名と同一となる。 -例えば \verb/AgdaBasics.agda/ を作成する時のモジュール名はリスト~\ref{src:agda-module}のように定義する。 - -\lstinputlisting[label=src:agda-module, caption=Agdaのモジュールの定義する] {src/AgdaBasics.agda.replaced} - -Agda における型指定は $:$ を用いて行なう。 -例えば、変数xが型Aを持つ、ということを表すには \verb/x : A/ と記述する。 - -データ型は Haskell や ML に似た代数的なデータ構造である。 -データ型の定義は \verb/data/ キーワードを用いる。 -\verb/data/キーワードの後に \verb/where/ 句を書きインデントを深くした後、値にコンストラクタとその型を列挙する。 -例えば Bool 型を定義するとリスト~\ref{src:agda-bool}のようになる。 -Bool はコンストラクタ \verb/true/ か \verb/false/ を持つデータ型である。 -Bool 自身の型は \verb/Set/ であり、これは Agda が組み込みで持つ「型の型」である。 -Set は階層構造を持ち、型の型の型を指定するには Set1 と書く。 - -\lstinputlisting[label=src:agda-bool, caption=Agdaにおけるデータ型 Bool の定義] {src/AgdaBool.agda.replaced} - - -関数の定義は Haskell に近い。 -関数名と型を記述した後に関数の本体を \verb/=/ の後に指定する。 -関数の型は $ \rightarrow $ を用いる。 -なお、$\rightarrow$に対しては糖衣構文 \verb/->/ も用意されている。 -例えば引数が型 \verb/A/ で返り値が型 \verb/B/ の関数は \verb/A -> B/ のように書ける。 -Bool 変数 \verb/x/ を取って true を返す関数 \verb/f/はリスト~\ref{src:agda-function}のようになる。 - -\lstinputlisting[label=src:agda-function, caption=Agda における関数定義] {src/AgdaFunction.agda.replaced} - -引数は変数名で受けることもできるが、具体的なコンストラクタを指定することでそのコンストラクタが渡された時の挙動を定義できる。 -これはパターンマッチと呼ばれ、コンストラクタで case 文を行なっているようなものである。 -例えば Bool 型の値を反転する \verb/not/ 関数を書くとリスト~\ref{src:agda-not}のようになる。 - -\lstinputlisting[label=src:agda-not, caption=Agdaにおける関数 not の定義] {src/AgdaNot.agda.replaced} - -パターンマッチは全てのコンストラクタのパターンを含まなくてはならない。 -例えば、Bool 型を受け取る関数で \verb/true/ の時の挙動のみを書くことはできない。 -なお、コンストラクタをいくつか指定した後に変数で受けると、変数が持ちうる値は指定した以外のコンストラクタとなる。 -例えばリスト~\ref{src:agda-pattern}の not は x には true しか入ることは無い。 -なお、マッチした値を変数として利用しない場合は \verb/_/ を用いて捨てることもできる。 - -\lstinputlisting[label=src:agda-pattern, caption=Agdaにおけるパターンマッチ] {src/AgdaPattern.agda.replaced} - -関数にはリテラルが存在し、関数名を定義せずともその場で生成することができる。 -これをラムダ式と呼び、\verb/\arg1 arg2 -> function body/ のように書く。 -例えば Bool 型の引数 \verb/b/ を取って not を適用する \verb/not-apply/ をラムダ式で書くとリスト~\ref{src:agda-lambda}のようになる。 -関数 \verb/not-apply/ をラムダ式を使わずに定義すると \verb/not-apply-2/ になるが、この二つの関数は同一の動作をする。 - -\lstinputlisting[label=src:agda-lambda, caption=Agda におけるラムダ式] {src/AgdaLambda.agda.replaced} - -Agda では特定の関数内のみで利用する関数を \verb/where/ 句で記述できる。 -これは関数内部の冗長な記述を省略するのに活用できる。 -スコープは \verb/where/句が存在する関数内部のみであるため、名前空間が汚染させることも無い。 -例えば自然数3つを取ってそれぞれ3倍して加算する関数 \verb/f/ を定義するとき、 \verb/where/ を使うとリスト~\ref{src:agda-where} のように書ける。 -これは \verb/f'/ と同様の動作をする。 -\verb/where/ 句は利用したい関数の末尾にインデント付きで \verb/where/ キーワードを記述し、改行の後インデントをして関数内部で利用する関数を定義する。 - -\lstinputlisting[label=src:agda-where, caption=Agda における where 句] {src/AgdaWhere.agda.replaced} - - -データ型のコンストラクタには自分自身の型を引数に取ることもできる(リスト~\ref{src:agda-nat})。 -自然数のコンストラクタは2つあり、片方は自然数ゼロ、片方は自然数を取って後続数を返すものである。 -例えば0 は \verb/zero/ であり、1 は \verb/suc zero/に、3は \verb/suc (suc (suc zero))/ に対応する。 - -\lstinputlisting[label=src:agda-nat, caption=Agdaにおける自然数の定義] {src/AgdaNat.agda.replaced} - -自然数に対する演算は再帰関数として定義できる。 -例えば自然数どうしの加算は二項演算子\verb/+/としてリスト~\ref{src:agda-plus}のように書ける。 - -この二項演算子は正確には中置関数である。 -前置や後置で定義できる部分を関数名に \verb/_/ として埋め込んでおくことで、関数を呼ぶ時にあたかも前置や後置演算子のように振る舞う。 -例えば \verb/!_/ 関数を定義すると \verb/! true/ のように利用でき、\verb/_~/ 関数を定義すると \verb/false ~/ のように利用できる。 - -また、Agda は再帰関数が停止するかを判定できる。 -この加算の二項演算子は左側がゼロに対しては明らかに停止する。 -左側が1以上の時の再帰時には \verb/suc n/ から \verb/n/へと減っているため、再帰で繰り返し減らすことでいつかは停止する。 -もし \verb/suc n/ のまま自分自身へと再帰した場合、Agda は警告を出す。 - -\lstinputlisting[label=src:agda-plus, caption=Agda における自然数の加算の定義] {src/AgdaPlus.agda.replaced} - -次に依存型について見ていく。 -依存型で最も基本的なものは関数型である。 -依存型を利用した関数は引数の型に依存して返す型を決定できる。 - -Agda で \verb/(x : A) -> B/ と書くと関数は型 A を持つx を受け取り、Bを返す。 -ここで B の中で x を扱っても良い。 -例えば任意の型に対する恒等関数はリスト~\ref{src:agda-id}のように書ける。 - -\lstinputlisting[label=src:agda-id, caption=依存型を持つ関数の定義] {src/AgdaId.agda.replaced} - -この恒等関数 \verb/identitiy/ は任意の型に適用可能である。 -実際に関数 \verb/identitiy/ を Nat へ適用した例が \verb/identitiy-zero/ である。 - -多相の恒等関数では型を明示的に指定せずとも \verb/zero/ に適用した場合の型は自明に \verb/Nat -> Nat/である。 -Agda はこのような推論をサポートしており、推論可能な引数は省略できる。 -推論によって解決される引数を暗黙的な引数(implicit arguments) と言い、記号 \verb/{}/ でくくる。 - -例えば、\verb/identitiy/ の対象とする型\verb/A/を暗黙的な引数として省略するとリスト~\ref{src:agda-implicit-id}のようになる。 -この恒等関数を利用する際は特定の型に属する値を渡すだけでその型が自動的に推論される。 -よって関数を利用する際は \verb/id-zero/ のように型を省略して良い。 -なお、関数の本体で暗黙的な引数を利用したい場合は \verb/{variableName}/ で束縛することもできる(\verb/id'/ 関数)。 -適用する場合も \verb/{}/でくくり、\verb/id-true/のように使用する。 - -\lstinputlisting[label=src:agda-implicit-id, caption=Agdaにおける暗黙的な引数を持つ関数] {src/AgdaImplicitId.agda.replaced} - -Agda には C における構造体に相当するレコード型も存在する。 -定義を行なう際は \verb/record/キーワードの後にレコード名、型、\verb/where/ の後に \verb/field/ キーワードを入れた後、フィールド名と型名を列挙する。 -例えば x と y の二つの自然数からなるレコード \verb/Point/ を定義するとリスト~\ref{src:agda-record}のようになる。 -レコードを構築する際は \verb/record/ キーワードの後の \verb/{}/ の内部に \verb/fieldName = value/ の形で値を列挙していく。 -複数の値を列挙する際は \verb/;/ で区切る。 - -\lstinputlisting[label=src:agda-record, caption=Agdaにおけるレコード型の定義] {src/AgdaRecord.agda.replaced} - -構築されたレコードから値を取得する際には \verb/RecordName.fieldName/ という名前の関数を適用する(リスト~\ref{src:agda-record-proj} 内2行目) 。 -なお、レコードにもパターンマッチが利用できる(リスト~\ref{src:agda-record-proj} 内5行目)。 -また、値を更新する際は \verb/record oldRecord {field = value ; ... }/ という構文を利用する。 -Point の中の x の値を5増やす関数 \verb/xPlus5/ はリスト~\ref{src:agda-record-proj}の 7,8行目のように書ける。 - -\lstinputlisting[label=src:agda-record-proj, caption=Agda におけるレコードの射影、パターンマッチ、値の更新] {src/AgdaRecordProj.agda.replaced} - -Agda における部分型のように振る舞う機能として Instance Arguments が存在する。 -これはとあるデータ型が、ある型と名前を持つ関数を持つことを保証する機能であり、Haskell における型クラスや Java におけるインターフェースに相当する。 -Agda における部分型の制約は、必要な関数を定義した record に相当し、その制約を保証するにはその record を instance として登録することになる。 -例えば、同じ型と比較することができる、という性質を表すとリスト~\ref{src:agda-type-class}のようになる。 -具体的にはとある型 A における中置関数 \verb/_==_/ を定義することに相当する。 - -\lstinputlisting[label=src:agda-type-class, caption=Agdaにおける部分型制約] {src/AgdaTypeClass.agda.replaced} - -ある型 T がこの部分型制約を満たすことを示すには、型 T でこのレコードを作成できることを示し、それを instance 構文で登録する。 -型Nat が Eq の上位型であることを記述するとリスト~\ref{src:agda-instance}のようになる。 - -\lstinputlisting[label=src:agda-instance, caption=Agdaにおける部分型関係の構築] {src/AgdaInstance.agda.replaced} - -これで \verb/Eq/ が要求される関数に対して Nat が適用できるようになる。 -例えば型 A の要素を持つ List A から要素を探してくる elem を定義する。 -部分型のインスタンスは \verb/{{}}/ 内部に名前と型名で記述する。 -なお、名前部分は必須である。 -仮に変数として受けても利用しない場合は \verb/_/ で捨てると良い。 -部分型として登録した record は関数本体において \verb/{{variableName}}/ という構文で変数に束縛できる。 - -\lstinputlisting[label=src:agda-use-instance, caption=Agdaにおける部分型を使う関数の定義] {src/AgdaElem.agda.replaced} - -この \verb/elem/ 関数はリスト~\ref{src:agda-elem-apply} のように利用できる。 -Nat型の要素を持つリストの内部に4が含まれるか確認している。 -この \verb/listHas4/ は \verb/true/ に評価される。 - -\lstinputlisting[label=src:agda-elem-apply, caption=部分型を持つ関数の適用] {src/AgdaElemApply.agda.replaced} - -最後にモジュールについて述べる。 -モジュールはほとんど名前空間として作用する。 -なお、依存型の解決はモジュールのインポート時に行なわれる。 -モジュールをインポートする時は \verb/import/ キーワードを指定する。 -また、インポートを行なう際に名前を別名に変更することもでき、その際は \verb/as/ キーワードを用いる。 -モジュールから特定の関数のみをインポートする場合は \verb/using/ キーワードを、関数の名前を変える時は \verb/renaming/キーワードを、特定の関数のみを隠す場合は \verb/hiding/ キーワードを用いる。 -なお、モジュールに存在する関数をトップレベルで用いる場合は \verb/open/ キーワードを使うことで展開できる。 -モジュールをインポートする例をリスト~\ref{src:agda-import}に示す。 - -\lstinputlisting[label=src:agda-import, caption=Agdaにおけるモジュールのインポート] {src/AgdaImport.agda.replaced} - -また、モジュールには値を渡すことができる。 -そのようなモジュールは Parameterized Module と呼ばれ、渡された値はそのモジュール内部で一貫して扱える。 -例えば要素の型と比較する二項演算子を使って並べ替えをするモジュール\verb/Sort/ を考える。 -そのモジュールは引数に型Aと二項演算子 \verb/</を取り、ソートする関数を提供する。 -\verb/Sort/モジュールを \verb/Nat/ と \verb/Bool/ で利用した例がリスト~\ref{src:agda-parameterized-module}である。 - -\lstinputlisting[label=src:agda-parameterized-module, caption=Agda における Parameterized Module] {src/AgdaParameterizedModule.agda.replaced} - -% }}} - -% {{{ Natural Deduction -\section{Natural Deduction} -\label{section:natural_deduction} -まず始めに証明を行なうためにNatural Deduction(自然演繹)を示す。 - -Natural Deduction は Gentzen によって作られた論理と、その証明システムである~\cite{Girard:1989:PT:64805}。 -命題変数と記号を用いた論理式で論理を記述し、推論規則により変形することで求める論理式を導く。 - -natural deduction において - -\begin{eqnarray} - \vdots \\ \nonumber - A \\ \nonumber -\end{eqnarray} - -と書いた時、最終的に命題Aを証明したことを意味する。 -証明は木構造で表わされ、葉の命題は仮定となる。 -仮定には dead か alive の2つの状態が存在する。 - -\begin{eqnarray} - \label{exp:a_implies_b} - A \\ \nonumber - \vdots \\ \nonumber - B \\ \nonumber -\end{eqnarray} - -式\ref{exp:a_implies_b}のように A を仮定して B を導いたとする。 -この時 A は alive な仮定であり、証明された B は A の仮定に依存していることを意味する。 - -ここで、推論規則により記号 $ \Rightarrow $ を導入する。 - -\begin{prooftree} - \AxiomC{[$ A $]} - \noLine - \UnaryInfC{ $ \vdots $} - \noLine - \UnaryInfC{ $ B $ } - \RightLabel{ $ \Rightarrow \mathcal{I} $} - \UnaryInfC{$ A \Rightarrow B $} -\end{prooftree} - -$ \Rightarrow \mathcal{I} $ を適用することで仮定 A は dead となり、新たな命題 $ A \Rightarrow B $ を導くことができる。 -A という仮定に依存して B を導く証明から、「A が存在すれば B が存在する」という証明を導いたこととなる。 -このように、仮定から始めて最終的に全ての仮定を dead とすることで、仮定に依存しない証明を導ける。 -なお、dead な仮定は \verb/[A]/ のように \verb/[]/ で囲んで書く。 - -alive な仮定を dead にすることができるのは $ \Rightarrow \mathcal{I} $ 規則のみである。 -それを踏まえ、 natural deduction には以下のような規則が存在する。 - -\begin{itemize} - \item Hypothesis - - 仮定。葉にある式が仮定となるため、論理式A を仮定する場合に以下のように書く。 - - $ A $ - - \item Introductions - - 導入。証明された論理式に対して記号を導入することで新たな証明を導く。 - - -\begin{prooftree} - \AxiomC{ $ \vdots $} - \noLine - \UnaryInfC{ $ A $ } - \AxiomC{ $ \vdots $} - \noLine - \UnaryInfC{ $ B $ } - \RightLabel{ $ \land \mathcal{I} $} - \BinaryInfC{$ A \land B $} -\end{prooftree} - -\begin{prooftree} - \AxiomC{ $ \vdots $} - \noLine - \UnaryInfC{ $ A $ } - \RightLabel{ $ \lor 1 \mathcal{I} $} - \UnaryInfC{$ A \lor B $} -\end{prooftree} - -\begin{prooftree} - \AxiomC{ $ \vdots $} - \noLine - \UnaryInfC{ $ B $ } - \RightLabel{ $ \lor 2 \mathcal{I} $} - \UnaryInfC{$ A \lor B $} -\end{prooftree} - -\begin{prooftree} - \AxiomC{[$ A $]} - \noLine - \UnaryInfC{ $ \vdots $} - \noLine - \UnaryInfC{ $ B $ } - \RightLabel{ $ \Rightarrow \mathcal{I} $} - \UnaryInfC{$ A \Rightarrow B $} -\end{prooftree} - -\item Eliminations - - 除去。ある論理記号で構成された証明から別の証明を導く。 - -\begin{prooftree} - \AxiomC{ $ \vdots $} - \noLine - \UnaryInfC{ $ A \land B $ } - \RightLabel{ $ \land 1 \mathcal{E} $} - \UnaryInfC{$ A $} -\end{prooftree} - -\begin{prooftree} - \AxiomC{ $ \vdots $} - \noLine - \UnaryInfC{ $ A \land B $ } - \RightLabel{ $ \land 2 \mathcal{E} $} - \UnaryInfC{$ B $} -\end{prooftree} - -\begin{prooftree} - \AxiomC{ $ \vdots $} - \noLine - \UnaryInfC{ $ A \lor B $ } - - \AxiomC{[$A$]} - \noLine - \UnaryInfC{ $ \vdots $} - \noLine - \UnaryInfC{ $ C $ } - - \AxiomC{[$B$]} - \noLine - \UnaryInfC{ $ \vdots $} - \noLine - \UnaryInfC{ $ C $ } - - \RightLabel{ $ \lor \mathcal{E} $} - \TrinaryInfC{ $ C $ } -\end{prooftree} - -\begin{prooftree} - \AxiomC{ $ \vdots $} - \noLine - \UnaryInfC{ $ A $ } - - \AxiomC{ $ \vdots $} - \noLine - \UnaryInfC{ $ A \Rightarrow B $ } - - \RightLabel{ $ \Rightarrow \mathcal{E} $} - \BinaryInfC{$ B $} -\end{prooftree} - -\end{itemize} - -記号 $ \lor, \land, \Rightarrow $ の導入の除去規則について述べた。 -natural deduction には他にも $ \forall, \exists, \bot $ といった記号が存在するが、ここでは解説を省略する。 - -それぞれの記号は以下のような意味を持つ -\begin{itemize} - \item $ \land $ - conjunction。2つの命題が成り立つことを示す。 - $ A \land B $ と記述すると、 A かつ B と考えることができる。 - - \item $ \lor $ - disjunction。2つの命題のうちどちらかが成り立つことを示す。 - $ A \lor B $ と記述すると、 A または B と考えることができる。 - - \item $ \Rightarrow $ - implication。左側の命題が成り立つ時、右側の命題が成り立つことを示す。 - $ A \Rightarrow B $ と記述すると、 A ならば B と考えることができる。 -\end{itemize} - -例として、natural deduction で三段論法を証明する。 -なお、三段論法とは「A は B であり、 B は C である。よって A は C である」といった文を示す。 - -\begin{prooftree} - \AxiomC{ $ [A] $ $_{(1)}$} - \AxiomC{ [$ (A \Rightarrow B) \land (B \Rightarrow C)$] $_{(2)}$ } - \RightLabel{ $ \land 1 \mathcal{E} $ } - \UnaryInfC{ $ (A \Rightarrow B) $ } - \RightLabel{ $ \Rightarrow \mathcal{E} $} - \BinaryInfC{ $ B $ } - - \AxiomC{ [$ (A \Rightarrow B) \land (B \Rightarrow C)$] $_{(2)}$ } - \RightLabel{ $ \land 2 \mathcal{E} $ } - \UnaryInfC{ $ (B \Rightarrow C) $ } - - \RightLabel{ $ \Rightarrow \mathcal{E} $} - \BinaryInfC{ $ C $ } - \RightLabel{ $ \Rightarrow \mathcal{I} _{(1)}$} - \UnaryInfC{ $ A \Rightarrow C $} - \RightLabel{ $ \Rightarrow \mathcal{I} _{(2)}$} - \UnaryInfC{ $ ((A \Rightarrow B) \land (B \Rightarrow C)) \Rightarrow (A \Rightarrow C) $} -\end{prooftree} - -まず、三段論法を論理式で表す。 - -「A は B であり、 B は C である。よって A は C である」 が証明するべき命題である。 -まず、「A は B であり」から、Aから性質Bが導けることが分かる。これが $ A \Rightarrow B $ となる。 -次に、「B は C である」から、Bから性質Cが導けることが分かる。これが $ B \Rightarrow C $ となる。 -そしてこの2つは同時に成り立つ。 -よって $ (A \Rightarrow B) \land (B \Rightarrow C)$ が仮定となる。 -この仮定が成り立つ時に「Aは Cである」を示せば良い。 -仮定と同じように「A は C である」は、 $ A \Rightarrow C $ と書けるため、証明するべき論理式は $ ((A \Rightarrow B) \land (B \Rightarrow C)) \Rightarrow (A \Rightarrow C) $ となる。 - -証明の手順はこうである。 -まず条件$ (A \Rightarrow B) \land (B \Rightarrow C)$とAの2つを仮定する。 -条件を $ \land 1 \mathcal{E} $ $ \land 2 \mathcal{E} $ により分解する。 -A と $ A \Rightarrow B$ から B を、 B と $ B \Rightarrow C $ から C を導く。 -ここで $ \Rightarrow \mathcal{I} $ により $ A \Rightarrow C $ を導く。 -この際に dead にする仮定は A である。 -数回仮定を dead にする際は $_{(1)} $ のように対応する \verb/[]/の記号に数値を付ける。 -これで残る alive な仮定は $ (A \Rightarrow B) \land (B \Rightarrow C)$ となり、これから $ A \Rightarrow C $ を導くことができたためにさらに $ \Rightarrow \mathcal{I} $ を適用する。 -結果、証明すべき論理式$ ((A \Rightarrow B) \land (B \Rightarrow C)) \Rightarrow (A \Rightarrow C) $ が導けたために証明終了となる。 - -% }}} - -% {{{ Curry-Howard Isomorphism -\section{Curry-Howard Isomorphism} -\label{section:curry_howard_isomorphism} -\ref{section:natural_deduction}節では Natural Deduction における証明手法について述べた。 -Natural Deduction はプログラム上では型付きのラムダ式として表現できる。 -これは Curry-Howard Isomorphism と呼ばれ、 Natural Deduction と型付き $ \lambda $ 計算が同じ構造であることを表している。 -Curry-Howard Isomorphism の概要を表~\ref{table:curry}に示す。 - -\begin{center} -\begin{table}[htbp] -\begin{tabular}{|c|c|} \hline - Natural Deduction & 型付き $ \lambda $ 計算 \\ \hline \hline - $ A $ & 型 A を持つ変数 x \\ \hline - $ A \Rightarrow B $ & 型 A を取り型 B の変数を返す関数 f \\ \hline - $ \Rightarrow \mathcal{I} $ & ラムダの抽象化 \\ \hline - $ \Rightarrow \mathcal{E} $ & 関数適用 \\ \hline - $ A \land B $ & 型 A と型 B の直積型 を持つ変数 x \\ \hline - $ \land \mathcal{I} $ & 型A,Bを持つ値から直積型へのコンストラクタ \\ \hline - $ \land 1 \mathcal{E} $ & 直積型からの型Aを取り出す射影fst \\ \hline - $ \land 2 \mathcal{E} $ & 直積型からの型Bを取り出す射影snd \\ \hline - $ A \lor B $ & 型 A と型 B の直和型 を持つ変数 x \\ \hline - $ \lor \mathcal{I} $ & 型A,Bの値から直和型へのコンストラクタ \\ \hline - $ \lor \mathcal{E} $ & 直和型から型Cの値を返す関数f \\ \hline -\end{tabular} -\caption{natural deuction と 型付き $ \lambda $ 計算との対応(Curry-Howard Isomorphism)} -\label{table:curry} -\end{table} -\end{center} - -型付きラムダ計算における命題は型に相当する。 -例えば恒等関数id の型は $ \text{A} \rightarrow \text{A}$ という型を持つが、これは「Aが成り立つならAが成り立つ」という命題と等しい。 -命題の仮定は引数となって表れ、証明はその型を導くための式となる。 - -例えば Natural Deduction における三段論法は $ ((A \Rightarrow B) \land (B \Rightarrow C)) \Rightarrow (A \Rightarrow C) $ という形をしていた。 -仮定は $ ((A \Rightarrow B) \land (B \Rightarrow C)) $ となる。 - -直積に対応する型には直積型が存在する。 -Agda において直積型に対応するデータ構造 \verb/Product/ を定義するとリスト~\ref{src:agda-product}のようになる。 -例えば \verb/Int/ 型と \verb/String/ 型を取る直積型は \verb/Int/ $ \times $ \verb/String/ 型となる。 -これは二つの型を取る型であり、Natural Deduction の $ \land $ に相当する。 - -直積型から値を射影する関数 \verb/fst/ と \verb/snd/ を定義する。 -これらは Natural Deduction における $ \land 1 \mathcal{E} $ と $ \land 2 \mathcal{E} $ に相当する。 - -なお、直積型は型Aを持つフィールド\verb/fst/と型Bを持つフィールド\verb/snd/を持つレコード型と考えても良い。 - -\lstinputlisting[label=src:agda-product, caption=Agda における直積型] {src/AgdaProduct.agda.replaced} - -三段論法の証明は 「1つの仮定から $ \land 1 \mathcal{E} $ と $ \land 2 \mathcal{E} $ を用いて仮定を二つ取り出し、それぞれに $ \Rightarrow \mathcal{E} $ を適用した後に仮定を $ \Rightarrow \mathcal{I}$ で dead にする」形であった。 - -$ \Rightarrow \mathcal{I}$ に対応するのは関数適用である。 -よってこの証明は「一つの変数から \verb/fst/ と \verb/snd/ を使って関数を二つ取り出し、それぞれを関数適用する」という形になる。 -これをラムダ式で書くとリスト~\ref{src:agda-modus-ponens}のようになる。 -仮定 $ (\text{A} \rightarrow \text{B}) \times (\text{B} \rightarrow \text{C}) $ と仮定 A から A $ \rightarrow $ C を導いている。 - -仮定に相当する変数 p の型は$ (\text{A} \rightarrow \text{B}) \times (\text{B} \rightarrow \text{C}) $ であり、p からそれぞれの命題を取り出す操作が \verb/fst/ と \verb/snd/ に相当する。 -\verb/fst p/ の型は $ (\text{A} \rightarrow \text{B}) $ であり、\verb/snd p/ の型は $ (\text{B} \rightarrow \text{C}) $ である。 -もう一つの仮定xの型は A なので、\verb/fst p/ を関数適用することで B が導ける。 -得られた B を \verb/snd p/ に適用することで最終的に C が導ける。 - -\lstinputlisting[label=src:agda-modus-ponens, caption=Agda における三段論法の証明] {src/AgdaModusPonens.agda.replaced} - -このように Agda では証明を記述することができる。 - -% }}} - -% {{{ Reasoning - -\section{Reasoning} -次に依存型を利用して等式の証明を記述していく。 - -例題として、自然数の加法の可換法則を示す。 -証明を行なうためにまずは自然数を定義する。 -今回用いる自然数の定義は以下のようなものである。 - -\begin{itemize} - \item 0 は自然数である - \item 任意の自然数には後続数が存在する - \item 0 はいかなる自然数の後続数でもない - \item 異なる自然数どうしの後続数は異なる ($ n \neq m \rightarrow S n \neq S m $) - \item 0がある性質を満たし、aがある性質を満たせばその後続数 S(n) も自然数である -\end{itemize} - -この定義は peano arithmetic における自然数の定義である。 - -Agda で自然数型 Nat を定義するとリスト \ref{src:agda-nat-2} のようになる。 - -\lstinputlisting[label=src:agda-nat-2, caption=Agda における自然数型 Nat の定義] {src/Nat.agda.replaced} - -自然数型 Nat は2つのコンストラクタを持つ。 - -\begin{itemize} - \item O - - 引数を持たないコンストラクタ。これが0に相当する。 - - \item S - - Nat を引数に取るコンストラクタ。これが後続数に相当する。 - -\end{itemize} - -よって、数値の 3 は \verb/S (S (S O))/ のように表現される。 -Sの個数が数値に対応する。 - -次に加算を定義する(リスト\ref{src:agda-nat-add})。 - -\lstinputlisting[label=src:agda-nat-add, caption=Agdaにおける自然数型に対する加算の定義] {src/NatAdd.agda.replaced} - -加算は中置関数 \verb/_+_/ として定義する。 -2つの Nat を取り、Natを返す。 -関数 \verb/_+_/ はパターンマッチにより処理を変える。 -0に対して m 加算する場合は m であり、 n の後続数に対して m 加算する場合は n に m 加算した数の後続数とする。 -S を左の数から右の数へ1つずつ再帰的に移していくような加算である。 - -例えば 3 + 1 といった計算は (S (S (S O))) + (S O) のように記述される。 -ここで 3 + 1 が 4と等しいことの証明を行なう。 - -等式の証明には agda の standard library における Relation.Binary.Core の定義を用いる。 - -\lstinputlisting[label=src:agda-equiv, caption= Relation.Binary.Core による等式を示す型 $ \equiv $] {src/Equiv.agda.replaced} -Agda において等式は、等式を示すデータ型 $ \equiv $ により定義される。 -$ \equiv $ は同じ両辺が同じ項に簡約される時にコンストラクタ refl で構築できる。 - -実際に 3 + 1 = 4 の証明は refl で構成できる(リスト\ref{src:agda-three-plus-one})。 - -\lstinputlisting[label=src:agda-three-plus-one, caption= Agda における 3 + 1 の結果が 4 と等しい証明] {src/ThreePlusOne.agda.replaced} - -3+1 という関数を定義し、その型として証明すべき式を記述し、証明を関数の定義として定義する。 -証明する式は \verb/(S (S (S O))) + (S O)≡(S (S (S (S O))))/ である。 -今回は \verb/_+_/ 関数の定義により \verb/ (S (S (S (S O)))) / に簡約されるためにコンストラクタ refl が証明となる。 - -$ \equiv $ によって証明する際、必ず同じ式に簡約されるとは限らないため、いくつかの操作が Relation.Binary.PropositionalEquality に定義されている。 - -\begin{itemize} - \item sym : $ x \equiv y \rightarrow y \equiv x $ - - 等式が証明できればその等式の左辺と右辺を反転しても等しい。 - - \item cong : $ f \rightarrow x \equiv y \rightarrow f x \equiv f y $ - - 証明した等式に同じ関数を与えても等式は保たれる。 - - \item trans : $ x \equiv y \rightarrow y \equiv z \rightarrow x \equiv z $ - - 2つの等式に表れた同じ項を用いて2つの等式を繋げた等式は等しい。 -\end{itemize} - -ではこれから nat の加法の交換法則を証明していく(リスト\ref{src:agda-nat-add-sym})。 - -\lstinputlisting[label=src:agda-nat-add-sym, caption= Agda における加法の交換法則の証明] {src/NatAddSym.agda.replaced} - -証明する式は $ n + m \equiv m + n $ である。 -n と m は Nat であるため、それぞれがコンストラクタ O か S により構成される。 -そのためにパターンは4通りある。 - -\begin{itemize} - \item n = O, m = O - - \verb/_+_/ の定義により、 O に簡約されるため refl で証明できる。 - - \item n = O, m = S m - - $ O + (S m) \equiv (S m) + O $ を証明することになる。 - この等式は \verb/_+_/ の定義により $ O + (S m) \equiv S (m + O) $ と変形できる。 - $ S (m + O) $ は $ m + O $ に S を加えたものであるため、 cong を用いて再帰的に \verb/addSym/ を実行することで証明できる。 - - この2つの証明はこのような意味を持つ。 - n が 0 であるとき、 m も 0 なら簡約により等式が成立する。 - n が 0 であり、 m が 0 でないとき、 m は後続数である。 - よって m が (S x) と書かれる時、 x は m の前の値である。 - 前の値による交換法則を用いてからその結果の後続数も \verb/_+_/ の定義により等しい。 - - ここで、 \verb/addSym/ に渡される m は1つ値が減っているため、最終的には n = 0, m = 0 である refl にまで簡約され、等式が得られる。 - - \item n = S n, m = O - - $ (S n) + O \equiv O + (S n) $ を証明する。 - この等式は \verb/_+_/ の定義により $ S (n + O) \equiv (S n) $ と変形できる。 - さらに変形すれば $ S (n + O) \equiv S (O + n) $ となる。 - よって \verb/addSym/ により O と n を変換した後に cong で S を加えることで証明ができる。 - - ここで、 $ O + n \equiv n $ は \verb/_+_/ の定義により自明であるが、$ n + O \equiv n $ をそのまま導出できないことに注意して欲しい。 - \verb/_+_/ の定義は左側の項から S を右側の項への移すだけであるため、右側の項への演算はしない。 - - \item n = S n, m = S m - - 3つのパターンは証明したが、このパターンは少々長くなるため別に解説することとする。 -\end{itemize} - -3 つのパターンにおいては refl や cong といった単純な項で証明を行なうことができた。 -しかし長い証明になると refl や cong といった式を trans で大量に繋げていく必要性がある。 -長い証明を分かりやすく記述するために $ \equiv $-Reasoning を用いる。 - -$ \equiv $-Reasoning では等式の左辺を begin の後に記述し、等式の変形を $ \equiv \langle expression \rangle $ に記述することで変形していく。 -最終的に等式の左辺を $ \blacksquare $ の項へと変形することで等式の証明が得られる。 - -自然数の加法の交換法則を $ \equiv $-Reasoning を用いて証明した例がリスト\ref{src:agda-reasoning}である。 -特に n と m が1以上である時の証明に注目する。 - -\lstinputlisting[label=src:agda-reasoning, caption= $ \equiv $ - Reasoning を用いた証明の例] {src/Reasoning.agda.replaced} - -まず \verb/ (S n) + (S m)/ は \verb/_+_/ の定義により \verb/ S (n + (S m)) / に等しい。 -よって refl で導かれる。 -なお、基本的に定義などで同じ項に簡約される時は refl によって記述することが多い。 - -次に \verb/S (n + (S m)) / に対して addSym を用いて交換し、 cong によって S を追加することで \verb/ S ((S m) + n) / を得る。 -これは、前3パターンにおいて + の右辺の項が 1以上であっても上手く交換法則が定義できたことを利用して項を変形している。 -このように同じ法則の中でも、違うパターンで証明できた部分を用いて別パターンの証明を行なうこともある。 - -最後に \verb/S ((S m) + n)/ から \verb/(S m) + (S n)/を得なくてはならない。 -しかし、 \verb/_+_/ の定義には右辺に対して S を移動する演算が含まれていない。 -よってこのままでは証明することができない。 -そのため、等式 $ S (m + n) \equiv m + (S n) $ を addToRight として定義する。 -addToRight はコンストラクタによる分岐を用いて証明できる。 -値が0であれば自明に成り立ち、1以上であれば再帰的に addToRight を適用することで任意の数に対して成り立つ。 -addToRight を用いることで \verb/S ((S m) + n)/ から \verb/(S m) + (S n)/を得られた。 -これで等式 $ (S m) + (S n) \equiv (S n) + (S m) $ の証明が完了した。 - -自然数に対する + の演算を考えた時にありえるコンストラクタの組み合せ4パターンのいずれかでも交換法則の等式が成り立つことが分かった。 -このように、Agda における等式の証明は、定義や等式を用いて右辺と左辺を同じ項に変形することで行なわれる。 - -% }}}
--- a/paper/akasha.tex Sat Jan 06 19:04:39 2018 +0900 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,256 +0,0 @@ -\chapter{メタ計算ライブラリ akasha における検証} -\label{chapter:akasha} -第~\ref{chapter:cbc}章では Continuation based C 言語の概要と、CbC で記述された GearsOS について述べた。 -GearsOS の持つメタ計算として、モデル検査的なアプローチで CodeGear の仕様を検証していく。 - -% {{{ モデル検査 -\section{モデル検査} -モデル検査とは、ソフトウェアの全ての状態において仕様が満たされるかを確認するものである。 -このモデル検査を行なうソフトウェアをモデル検査器と呼ぶ。 -モデルは検査器は、仕様の定義とその検証ができる。 -加えて、仕様を満たさない場合にはソフトウェアがどのような状態であったか反例を返す。 - -モデル検査器には Spin\cite{spin} やCBMC\cite{cbmc} などが存在する。 - -Spin は Promela と呼ばれる言語でモデルを記述し、その中に論理式として仕様を記述する。 -論理式は assert でモデルの内部に埋め込まれ、並列に実行してもその仕様が満たされるかをチェックする。 -また、Promela で記述されたモデルからC言語を生成することができる。 -しかし、Promela で記述されたモデルは元のC言語とはかなり異なる構文をしており、ユーザが記述する難易度が高い。 - -そこで、モデルを個別に記述せずに実装そのものを検査するアプローチがある。 -例えばモデル検査器 CBMC は C言語を直接検証できる。 -CBMC でも仕様は論理式で記述され、 assert と組み合わせる。 -C 言語の実行は通常の実行とは異なり、記号実行という形で実行される。 -プログラム上の変数は記号として処理され、\verb/a < b/ といった条件式により分岐が行なわれたのなら、その条件を持つ場合の経路、持たない場合の経路、と分岐していくのである。 - -GearsOS におけるモデル検査的なアプローチはCBMC のように実装言語をそのまま検証できるようにしたい。 -そのために、assert を利用した仕様の定義と、その検査、必要なら反例を提出するようなメタ計算を定義する。 -このメタ計算をメタ計算ライブラリ akasha として実装した。 - -この章では、メタ計算ライブラリ akasha を用いて GearsOS のデータ構造を検証していく。 -% }}} - -% {{{ GearsOS における非破壊赤黒木 -\section{GearsOS における非破壊赤黒木} -現状の GearsOS に実装されているメタ計算として、非破壊赤黒木が存在する。 -非破壊赤黒木はユーザがデータを保存する際に利用することを想定している。 -メタ計算として定義することで、ノーマルレベルからは木のバランスを考慮せず木への操作が行なえる。 - -なお、赤黒木とは二分探索木の一種であり、木のバランスを取るための情報として各ノードは赤か黒の色を持っている。 - -二分探索木の条件は以下である。 - -\begin{itemize} - \item 左の子孫の値は親の値より小さい - \item 右の子孫の値は親の値より大きい -\end{itemize} - -加えて、赤黒木が持つ具体的な条件は以下のものである。 - -\begin{itemize} - \item 各ノードは赤か黒の色を持つ。 - \item ルートノードの色は黒である。 - \item 葉ノードの色は黒である。 - \item 赤ノードは2つの黒ノードを子として持つ(よって赤ノードが続くことは無い)。 - \item ルートから最下位ノードへの経路に含まれる黒ノードの数はどの最下位ノードでも一定である。 -\end{itemize} - - -数値を要素に持つ赤黒木の例を図\ref{fig:rbtree}に示す。 -条件に示されている通り、ルートノードは黒であり、赤ノードは連続していない。 -加えて各最下位ノードへの経路に含まれる黒ノードの個数は全て2である。 - -\begin{figure}[htbp] - \begin{center} - \includegraphics[scale=0.5]{fig/rbtree.pdf} - \caption{赤黒木の例} - \label{fig:rbtree} - \end{center} -\end{figure} - -赤黒木の持つ条件を言い変えるのなら、「木をルートから辿った際に最も長い経路は最も短い経路の高々二倍に収まる」とも言える。 -この言い換えは「赤が続くことはない」という条件と「ルートから最下位への経路の黒ノードはどの最下位ノードでも同じ」であることから導ける。 -具体的には、最短経路は「黒のみの経路」であり、最長経路は「黒と赤が交互に続く経路」となる。 -この条件を言い変えた性質を仕様とし、検証していく。 - -GearsOS で実装されている赤黒木は特に非破壊赤黒木であり、一度構築した木構造は破壊される操作ごとに新しい木構造が生成される。 -非破壊の性質を付与した理由として、並列実行時のデータの保存がある。 -同じ赤黒木をロックせずに同時に更新した場合、ノードの値は実行順に依存したり、競合したりする。 -しかし、ロックを行なって更新した場合は同じ木に対する処理に待ち合わせが発生し、全体の並列度が下がる。 -この問題に対し GearsOS では、各スレッドは処理を行なう際には非破壊の木を利用することで並列度は保ち、値の更新が発生する時のみ木をアトミックな操作で置き換えることで競合を回避する。 -具体的には木の操作を行なった後はルートのノードを元に CAS で置き換え、失敗した時は木を読み込み直して処理を再実行する。 -CAS(Check and Set) とは、アトミックに値を置き換える操作であり、使う際は更新前の値と更新後の値を渡す。 -CAS で渡された更新前の値が、保存している値と同じであれば競合していないために値の更新に成功し、異なる場合は他に書き込みがあったことを示すために値の更新が失敗する操作のことである。 - -非破壊赤黒木の実装の基本的な戦略は、変更したいノードへのルートノードからの経路を全て複製し、変更後に新たなルートノードとすることである。 -この際に変更されていない部分は変更前の木と共有する(図\ref{fig:non-destructive-rbtree})。 -これは一度構築された木構造は破壊されないという非破壊の性質を用いたメモリ使用量の最適化である。 - -\begin{figure}[htbp] - \begin{center} - \includegraphics[scale=0.5]{fig/non-destructive-rbtree} - \caption{非破壊赤黒木の編集} - \label{fig:non-destructive-rbtree} - \end{center} -\end{figure} - -CbC を用いて赤黒木を実装する際の問題として、関数の呼び出しスタックが存在しないことがある。 -C における実装では関数の再帰呼び出しによって木が辿るが、それが行なえない。 -経路を辿るためには、ノードに親への参照を持たせるか、挿入や削除の際に辿った経路を記憶する必要がある。 -ノードが親への参照を持つ非破壊木構造は共通部分の共有が行なえないため、経路を記憶する方法を使う。 -経路の記憶にはスタックを用い、スタックは Meta DataSegment に保持する。 - -赤黒木を格納する DataSegment と Meta DataSegment の定義をリスト\ref{src:rbtree-context}に示す。 -経路の記憶に用いるスタックは Meta DataSegment である Context 内部の \verb/node_stack/ である。 -DataSegment は各ノード情報を持つ \verb/Node/構造体と、赤黒木を格納する \verb/Tree/構造体、挿入などで操作中の一時的な木を格納する \verb/Traverse/共用体などがある。 - -\lstinputlisting[label=src:rbtree-context, caption=赤黒木の DataSegment と Meta DataSegment] {src/rbtreeContext.h} - -Meta DataSegment を初期化する Meta CodeSegment initLLRBContext をリスト\ref{src:init-rbtree-context}に示す。 -この Meta CodeSegment ではメモリ領域の確保、CodeSegment 名と CodeSegment の実体の対応表の作成などを行なう。 -メモリ領域はプログラムの起動時に一定数のメモリを確保し、ヒープとして \verb/heap/ フィールドに保持させる。 -CodeSegment 名と CodeSegment の実体との対応は、enum で定義された CodeSegment 名の添字へと CodeSegment の関数ポインタを代入することにより持つ。 -例えば \verb/Put/ の実体は \verb/put_stub/ である。 -他にも DataSegment の初期化(リスト\ref{src:init-rbtree-context} 34-48)とスタックの初期化(リスト\ref{src:init-rbtree-context} 50-51)を行なう。 - -\lstinputlisting[label=src:init-rbtree-context, caption=赤黒木の Meta DataSegment の初期化を行なう Meta CodeSegment ] {src/initLLRBContext.c} - -実際の赤黒木の実装に用いられている Meta CodeSegment の一例をリスト\ref{src:rbtree-insert-case-2}に示す。 -Meta CodeSegment \verb/insertCase2/ は要素を挿入した場合に呼ばれる Meta CodeSegment の一つであり、親ノードの色によって処理を変える。 -まず、色を確認するために経路を記憶しているスタックから親の情報を取り出す。 -親の色が黒ならば処理を終了し、次の CodeSegment へと軽量継続する(リスト\ref{src:rbtree-insert-case-2} 5-8)。 -親の色が赤であるならばさらに処理を続行して \verb/InsertCase3/ へと軽量継続する。 -ここで、経路情報を再現するためにスタックへと親を再代入してから軽量継続を行なっている。 -なお、Meta CodeSegment でも Context から DataSegment を展開する処理は stub によって行なわれる(リスト\ref{src:rbtree-insert-case-2} 14-16)。 - -\lstinputlisting[label=src:rbtree-insert-case-2, caption=赤黒木の実装に用いられている Meta CodeSegment例] {src/insertCase2.c} - -% }}} - -% {{{ メタ計算ライブラリ akasha を用いた赤黒木の実装の検証 - -\section{メタ計算ライブラリ akasha を用いた赤黒木の実装の検証} -赤黒木の仕様の定義とその確認を CbC で行なっていく。 -仕様には赤黒木の利用方法などによっていくつかのものが考えられる。 -赤黒木に対する操作の仕様と、その操作によって保証されるべき赤黒木の状態を示すと以下のようになる。 - -\begin{itemize} - \item 挿入したデータは参照できること - \item 削除したデータは参照できないこと - \item 値を更新した後は更新された値が参照されること - \item 操作を行なった後の木はバランスしていること -\end{itemize} - -今回はバランスに関する仕様を確認する。 -操作を挿入に限定し、どのような順番で要素を挿入しても木がバランスすることを検証する。 -検証には当研究室で開発しているメタ計算ライブラリ akasha を用いる。 - -akasha では仕様は常に成り立つべき CbC の条件式として定義する。 -具体的には Meta CodeSegment に定義した assert が仕様に相当する。 -仕様の例として「木をルートから辿った際に最も長い経路は最も短い経路の高々2倍に収まる」という式を定義する(リスト\ref{src:assert})。 - -\lstinputlisting[label=src:assert, caption=木の高さに関する仕様記述] {src/assert.c} - -リスト\ref{src:assert} で定義した仕様がプログラムの持つ全ての状態に成り立つかを確認する。 -また、成り立たない場合には仕様に反する状態を反例として提出する。 - -まずは最も単純な検証として要素数を有限に固定し、その挿入順番を数え上げる。 -最初に、検証の対象となる赤黒木と、検証に必要な DataSegment を含む Meta DataSegment を定義する(リスト\ref{src:akasha-context})。 -これが akasha のレベルで利用する Meta DataSegment である。 -赤黒木自体はユーザから見るとメタレベル計算であるが、今回はその実装の検証するため、赤黒木がノーマルレベルとなる。 -よって akasha はメタメタレベルの計算とも考えられる(図~\ref{fig:metameta})。 - -\begin{figure}[htbp] - \begin{center} - \includegraphics[width=250pt]{fig/metameta.pdf} - \caption{akasha とメタの階層構造} - \label{fig:metameta} - \end{center} -\end{figure} - -akasha が使う DataSegment は データの挿入順を数え上げるためには使う環状リスト \verb/Iterator/ とその要素 \verb/IterElem/、検証に使う情報を保持する \verb/AkashaInfo/、木をなぞる際に使う \verb/AkashaNode/ がある。 - -\lstinputlisting[label=src:akasha-context, caption=検証を行なうための Meta DataSegment] {src/akashaContext.h} - -挿入順番の数え上げには環状リストを用いた深さ優先探索を用いる。 -最初に検証する要素を全て持つ環状リストを作成し、木に挿入した要素を除きながら環状リストを複製していく。 -環状リストが空になった時が組み合わせを一つ列挙し終えた状態となる。 -列挙し終えた後、前の深さの環状リストを再現してリストの先頭を進めることで異なる組み合わせを列挙する。 - -仕様には木の高さが含まれるので、高さを取得する Meta CodeSegment が必要となる。 -リスト\ref{src:get-min-height}に木の最も低い経路の長さを取得する Meta CodeSegment を示す。 - -木を辿るためのスタックに相当する \verb/AkshaNode/を用いて経路を保持しつつ、高さを確認している。 -スタックが空であれば全てのノードを確認したので次の CodeSegment へと軽量継続を行なう。 -空でなければ今辿っているノードが葉であるか確認し、葉ならば高さを更新して次のノードを確認するため自身へと軽量継続する。 -葉でなければ高さを1増やして左右の子をスタックに積み、自身へと軽量継続を行なう。 - -\lstinputlisting[label=src:get-min-height, caption=木の最も短かい経路の長さを確認する Meta CodeSegment] {src/getMinHeight.c} - -同様に最も高い高さを取得し、仕様であるリスト\ref{src:assert}の assert を挿入の度に実行する。 -assert は CodeSegment の結合を行なうメタ計算である \verb/meta/ を上書きすることにより実現する。 -イメージとしては、挿入を行なう Meta CodeSegment を利用するプログラム(図~\ref{fig:put}) の途中に検証用のメタ計算を挟むことで実現できる(図~\ref{fig:akashaPut})。 - -\begin{figure}[htbp] - \begin{center} - \includegraphics[width=300pt]{fig/put.pdf} - \caption{put を利用するプログラム} - \label{fig:put} - \end{center} -\end{figure} - -\begin{figure}[htbp] - \begin{center} - \includegraphics[width=300pt]{fig/akashaPut.pdf} - \caption{put を利用するプログラムのメタを上書きする} - \label{fig:akashaPut} - \end{center} -\end{figure} - -\verb/meta/ はリスト\ref{src:rbtree-insert-case-2}の \verb/insertCase2/ のように軽量継続を行なう際に CodeSegment 名と DataSegment を指定するものである。 -検証を行なわない通常の \verb/meta/ の実装は CodeSegment 名から対応する実体への軽量継続であった(リスト\ref{src:default-meta})。 - -\lstinputlisting[label=src:default-meta, caption=通常の CodeSegment の軽量継続] {src/meta.c} - -これを、検証を行なうように変更することで \verb/insertCase2/ といった赤黒木の実装のコードを修正することなく検証を行なうことができる。 -検証を行ないながら軽量継続する \verb/meta/ はリスト\ref{src:akasha-meta}のように定義される。 -実際の検証部分は \verb/PutAndGoToNextDepth/ の後に行なわれるため、直接は記述されていない。 -この \verb/meta/ が行なうのは検証用にメモリの管理である。 -状態の数え上げを行なう際に状態を保存したり、元の状態に戻す処理が行なわれる。 -このメタ計算を用いた検証では、要素数13個までの任意の順で挿入の際に仕様が満たされることを確認できた。 -また、赤黒木の処理内部に恣意的なバグを追加した際には反例を返した。 - -\lstinputlisting[label=src:akasha-meta, caption=検証を行なう CodeSegment の軽量継続] {src/akashaMeta.c} - -% }}} - -% {{{ モデル検査器 CBMC との比較 - -\section{モデル検査器 CBMC との比較} -akasha の比較対象として、 C言語の有限モデルチェッカ CBMC\cite{cbmc} を用いて赤黒木を検証した。 -CBMC は ANSI-C を記号実行し、仕様の否定となるような実行パターンが無いかを検証するツールである。 - -比較のために全く同じ赤黒木のソースコードを用いたいが、CbCの構文は厳密にはCとは異なるために変換が必要である。 -具体的には、\verb/__code/ を \verb/void/ に、 \verb/goto/ を \verb/return/ に置換することで機械的にC言語に変換できる。 - -CBMC における仕様は bool を返す式として記述するため、akashaと同様の仕様定義が利用できる(リスト\ref{src:cbmc-assert}。 -assert が true になるような実行パターンを CBMC が見付けると、その実行パターンが反例として出力される。 - -\lstinputlisting[label=src:cbmc-assert, caption=CBMC における仕様記述] {src/cbmc-assert.c} - -挿入順の数え上げにはCBMCの機能に存在する非決定的な値 \verb/nondet_int()/ を用いた(リスト\ref{src:enumerate-inputs})。 -この \verb/nondet_int()/ 関数は int の持ちうる値の内から非決定的に値を取得する関数である。 -akasha では有限の要素個分の組み合わせを用いて挿入順の数え上げとしたが、CBMC では要素数回分だけランダムな値を入力させることで数え上げとする。 - -\lstinputlisting[label=src:enumerate-inputs, caption= CBMC における挿入順の数え上げ] {src/enumerate-inputs.c} - -CBMCでは有限のステップ数だけC言語を記号実行し、その範囲内で仕様が満たされるかを確認する。 -条件分岐や繰り返しなどは展開されて実行される。 -基本的にはメモリの許す限り展開を行なうことができるが、今回の赤黒木の検証では411回まで展開することができた。 -この411回のうちの実行パスでは赤黒木の仕様は常に満たされる。 -しかし、この展開された回数は挿入された回数とは無関係であり、実際どの程度検証することができたか確認できない。 -実際、赤黒木に恣意的なバグを追加した際にも仕様の反例は得られず、CBMC で扱える範囲内では赤黒木の性質は検証できなかった。 - -よって、CBMCでは検証できない範囲の検証を akasha で行なえることが確認できた。 - -% }}}
--- a/paper/atton-master.tex Sat Jan 06 19:04:39 2018 +0900 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,138 +0,0 @@ -% TODO lists -% 比較対象 -% agda の stack? -% あと syntax を最新に合わせて動かしてくれ -% type system に名前を付ける? -% 先の展望を書くべきだな -% delta monad -% csComp, push-pop, exec-comp の解説 - -\documentclass[a4j,12pt]{jreport} -\usepackage{master_paper} -\usepackage{ascmac} -\usepackage{bussproofs} -\usepackage[dvipdfmx]{graphicx} -\usepackage{here} -\usepackage{listings} -\usepackage{comment} -\usepackage[deluxe, multi]{otf} -\usepackage{url} -\usepackage{cite} -\usepackage{listings} -\usepackage{bussproofs} -\usepackage{amssymb} -\usepackage{amsmath} -\usepackage{colonequals} -\usepackage[utf8]{inputenc} - -%\input{dummy.tex} %% font - -\jtitle{メタ計算を用いた Continuation based C の検証手法} -\etitle{Verification Methods of Continuation based C using Meta Computations} -\year{2017年 3月} -\eyear{March 2017} -\author{比嘉 健太} -\eauthor{Yasutaka HIGA} -\chife{指導教員：教授 和田 知久} -\echife{Supervisor: Prof. Tomohisa WADA} - -\marklefthead{% 左上に挿入 - \begin{minipage}[b]{.4\textwidth} - 琉球大学大学院学位論文(修士) -\end{minipage}} - -\markleftfoot{% 左下に挿入 - \begin{minipage}{.8\textwidth} - メタ計算を用いた Continuation based C の検証手法 -\end{minipage}} - -\newcommand\figref[1]{図 \ref{fig:#1}} -\newcommand\tabref[1]{表 \ref{tab:#1}} - -\lstset{ - frame=single, - keepspaces=true, - stringstyle={\ttfamily}, - commentstyle={\ttfamily}, - identifierstyle={\ttfamily}, - keywordstyle={\ttfamily}, - basicstyle={\ttfamily}, - breaklines=true, - xleftmargin=0zw, - xrightmargin=0zw, - framerule=.2pt, - columns=[l]{fullflexible}, - numbers=left, - stepnumber=1, - numberstyle={\scriptsize}, - numbersep=1em, - language={}, - tabsize=4, - lineskip=-0.5zw, - escapechar={@}, -} -\def\lstlistingname{リスト} -\def\lstlistlistingname{リスト目次} -\newtheorem{theorem}{定理}[section] -\newtheorem{lemma}{補題}[section] - - -%%% 索引のために以下の2行を追加 -\usepackage{makeidx,multicol} -\makeindex -\begin{document} - -%rome -\frontmatter - -\maketitle -\newpage - -\makecommission - -%要旨 -\input{abstract.tex} - -%目次 -\tableofcontents - -%図目次 -\listoffigures - -%表目次 -\listoftables - -%リスト目次 -\lstlistoflistings - - -%arabic -\mainmatter - -%chapters -\input{introduction.tex} -\input{cbc.tex} -\input{akasha.tex} -\input{type.tex} -\input{agda.tex} -\input{cbc-type.tex} -\input{summary.tex} - -%謝辞 -\addcontentsline{toc}{chapter}{謝辞} -\input{thanks.tex} - -%参考文献 -\nocite{*} -\bibliographystyle{junsrt} -\bibliography{reference} - -%発表履歴 -\addcontentsline{toc}{chapter}{発表履歴} -\input{history.tex} - -%付録 -\addcontentsline{toc}{chapter}{付録} -\appendix -\input{sources.tex} -\end{document}
--- a/paper/cbc-type.tex Sat Jan 06 19:04:39 2018 +0900 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,476 +0,0 @@ -\chapter{Agda による Continuation based C の表現} -\label{chapter:cbc-type} -~\ref{chapter:agda}章では Curry-Howard 同型対応により、型付きラムダ計算を用いて命題が証明できることを示した。 -加えて、証明支援系言語 Agda を用いてデータの定義とそれを扱う関数の性質の証明が行なえることを確認した。 - -CbC で自身を証明するために依存型を利用したいが、CbC には専用の型システムが存在しない。 -依存型をCbCコンパイラで扱うためにもまず現状の CbC を型付けする必要がある。 - -~\ref{chapter:cbc-type}章では CbC の項が部分型で型付けできることを示す。 -定義した型システムを用いて、Agda 上に DataSegment と CodeSegment の定義、CodeSegment の接続と実行、メタ計算を定義し、それらが型付けされることを確認する。 -また、Agda 上で定義した DataSegment とそれに付随する CodeSegment の持つ性質を Agda で証明する。 - -% {{{ DataSegment の定義 -\section{DataSegment の定義} -まず DataSegment から定義していく。 -DataSegment はレコード型で表現できるため、Agda のレコードをそのまま利用できる。 -例えは~\ref{src:goto} に示していた a と b を加算して c を出力するプログラムに必要な DataSegment を記述すると~\ref{src:agda-ds}のようになる。 -cs0 は a と b の二つの Int 型の変数を利用するため、対応する ds0 は a と b のフィールドを持つ。 -cs1 は計算結果を格納する c という名前の変数のみを持つので、同様にds1もcのみを持つ。 - -\lstinputlisting[label=src:agda-ds, caption=Agda における DataSegment の定義] {src/DataSegment.agda.replaced} -% }}} - -% {{{ CodeSegment の定義 -\section{CodeSegment の定義} -次に CodeSegment を定義する。 -CodeSegment は DataSegment を取って DataSegment を返すものである。 -よって $ I \rightarrow O $ を内包するデータ型を定義する。 - -レコード型の型は Set なので、Set 型を持つ変数 I と O を型変数に持ったデータ型 CodeSegment を定義する。 -I は Input DataSegment の型であり、 O は Output DataSegment である。 - -CodeSegment 型のコンストラクタには \verb/cs/ があり、Input DataSegment を取って Output DataSegment を返す関数を取る。 -具体的なデータ型の定義はリスト ~\ref{src:agda-cs} のようになる。 - -\lstinputlisting[label=src:agda-cs, caption= Agda における CodeSegment 型の定義] {src/CodeSegment.agda.replaced} - -この CodeSegment 型を用いて CodeSegment の処理本体を記述する。 - -まず計算の本体となる cs0 に注目する。 -cs0 は二つのInt型変数を持つ ds0 を取り、一つのInt型変数を作った上で cs1 に軽量継続を行なう。 -DataSegment はレコードなので、a と b のフィールドから値を取り出した上で加算を行ない、cを持つレコードを生成する。 -そのレコードを引き連れたまま cs1 へと goto する。 - -次に cs1 に注目する。 -cs1 は値に触れず cs2 へと goto するだけである。 -よって何もせずにそのまま goto する関数をコンストラクタ\verb/cs/ に渡すだけで良い。 - -最後に cs2 である。 -cs2 はリスト~\ref{src:goto}では省略していたが、今回は計算を終了させる CodeSegment として定義する。 -どの CodeSegment にも軽量継続せずに値を持ったまま計算を終了させる。 -コンストラクタ \verb/cs/ には関数を与えなくては値を構成できないため、何もしない関数である id を渡している。 - -最後に計算をする cs0 へと軽量継続する main を定義する。 -例として、 a の値を 100 とし、 b の値を50としている。 - -cs0, cs1, cs2, main をAgda で定義するとリスト~\ref{src:agda-css}のようになる。 - -\lstinputlisting[label=src:agda-css, caption= Agda における CodeSegment の定義] {src/CodeSegments.agda.replaced} - -正しく計算が行なえたなら値150が得られるはずである。 -% }}} - -% {{{ ノーマルレベル計算の実行 -\section{ノーマルレベル計算の実行} -\label{section:normal-level-exec} -プログラムを実行することは \verb/goto/ を定義することと同義である。 -軽量継続\verb/goto/ の性質としては - -\begin{itemize} - \item 次に実行する CodeSegment を指定する - \item CodeSegment に渡すべき DataSegment を指定する - \item 現在実行している CodeSegment から制御を指定された CodeSegment へと移動させる -\end{itemize} - -がある。 -Agda における CodeSegment の本体は関数である。 -関数をそのまま使用すると再帰を許してしまうために CbC との対応が失われてしまう。 -よって、\verb/goto/を利用できるのは関数の末尾のみである、という制約を関数に付け加える必要がある。 - -この制約さえ満たせば、CodeSegment の実行は CodeSegment 型から関数本体を取り出し、レコード型を持つ値を適用することに相当する。 -具体的に \verb/goto/ を関数として適用するとリスト~\ref{src:agda-goto}のようになる。 - -\lstinputlisting[label=src:agda-goto, caption=Agdaにおける goto の定義] {src/Goto.agda.replaced} - -この \verb/goto/ の定義を用いることで main などの関数が評価できるようになり、値150が得られる。 -本文中での CodeSegment の定義は一部を抜粋している。 -実行可能な Agda のソースコードは付録に載せる。 - -% }}} - -% {{{ Meta DataSegment の定義 - -\section{Meta DataSegment の定義} -ノーマルレベルの CbC を Agda 上で記述し、実行することができた。 -次にメタレベルの計算を Agda 上で記述していく。 - -Meta DataSegment はノーマルレベルの DataSegment の集合として定義できるものであり、全ての DataSegment の部分型であった。 -ノーマルレベルの DataSegment はプログラムによって変更されるので、事前に定義できるものではない。 -ここで、Agda の Parameterized Module を利用して、「Meta DataSegment の上位型は DataSegment である」のように DataSegment を定義する。 -こうすることにより、全てのプログラムは一つ以上の Meta DataSegment を持ち、任意の個数の DataSegment を持つ。 -また、Meta DataSegment をメタレベルの DataSegment として扱うことにより、「Meta DataSegment の部分型である Meta Meta DataSegment」を定義できるようになる。 -階層構造でメタレベルを表現することにより、計算の拡張を自在に行なうことができる。 - -具体的な Meta DataSegment の定義はリスト~\ref{src:agda-mds}のようになる。 -型システム \verb/subtype/ は、Meta DataSegment である \verb/Context/ を受けとることにより構築される。 -Context を Meta DataSegment とするプログラム上では DataSegment は Meta CodeSegment の上位型となる。 -その制約を \verb/DataSegment/ 型は表わしている。 - -\lstinputlisting[label=src:agda-mds, caption=Agda における Meta DataSegment の定義] {src/MetaDataSegment.agda.replaced} - - -ここで、関数を部分型に拡張する S-ARROW をもう一度示す。 - -\begin{align*} - \AxiomC{$ T_1 <: S_1$} - \AxiomC{$ S_2 <: T_2$} - \BinaryInfC{$ S_1 \rightarrow S_2 <: T_1 \rightarrow T_2 $} - \DisplayProof && \text{S-ARROW} -\end{align*} - -S-ARROW は、前提である部分型関係 $ T_1 <: S_1 $ と $ S_2 <: T_2 $ が成り立つ時に、 上位型 $ S_1 \rightarrow S_2 $ の関数を、部分型 $ T_1 \rightarrow T_2 $ に拡張できた。 -ここでの上位型は DataSegment であり、部分型は Meta DataSegment である。 -制約\verb/DataSegment/ の \verb/get/ は、 Meta DataSegment から DataSegment が生成できることを表す。 -これは前提 $ T_1 <: S_1 $ に相当する。 -そして、\verb/set/ は $ S_2 <: T_2 $ に相当する。 -しかし、任意の DataSegment が Meta DataSegment の部分型となるには、 DataSegment が Meta DataSegment よりも多くの情報を必ず持たなくてはならないが、これは通常では成り立たない。 -だが、メタ計算を行なう際には常に Meta DataSegment を一つ以上持っていると仮定するならば成り立つ。 -実際、GearsOS における赤黒木では Meta DataSegment に相当する \verb/Context/ を常に持ち歩いている。 -GearsOS における計算結果はその持ち歩いている Meta DataSegment の更新に相当するため、常に Meta DataSegment を引き連れていることを無視すれば DataSegment から Meta DataSegment を導出できる。 -よって $ S_2 <: T_2 $ が成り立つ。 - -なお、 $ S_2 <: T_2 $ は Output DataSegment を Meta DataSegment を格納する作業に相当し、 $ T_1 <: S_1 $ は Meta DataSegment から Input DataSegment を取り出す作業であるため、これは明らかに \verb/stub/ である。 - -% }}} - -% {{{ Meta CodeSegment の定義 - -\section{Meta CodeSegment の定義} -Meta DataSegment が定義できたので Meta CodeSegment を定義する。 -実際、DataSegment が Meta DataSegment に拡張できたため、Meta CodeSegment の定義には比較的変更は無い。 -ノーマルレベルの \verb/CodeSegment/ 型に、DataSegment を取って DataSegment を返す、という制約を明示的に付けるだけである(リスト~\ref{src:agda-mcs}) - -\lstinputlisting[label=src:agda-mcs, caption=Agda における Meta CodeSegment の定義] {src/MetaCodeSegment.agda.replaced} - -メタレベルの定義を部分型で行なって分かったことには以下のようなものがある。 - -\begin{itemize} - \item メタ計算は階層構造化できる - - メタ計算は階層構造を取ることができるため、組み合わせることも可能である。 - - \item 継続先が不定の場合は型を一様に扱う必要がある - - メタ計算がノーマルレベルの具体的な型を知ることができるのはコンパイル時のみである。 - よってメタ計算を定義する時は部分型制約しか記述できない。 - 逆に言えばノーマルレベル計算のみであれば部分型は解決され、レコード型で型付けができる。 - - \item \verb/stub/ は部分型付けにおいても必要である - - GearsOS では Meta DataSegment から DataSegment を取り出すための処理として \verb/stub/ が存在していた。 - これは Meta DataSegment で一様に扱っていた DataSegment に型を戻す処理として、型システムにおいても必要なものである。' - また、型システム経由で \verb/stub/ を生成することも可能であると考えられる。 - -\end{itemize} - -% }}} - -% {{{ メタレベル計算の実行 -\section{メタレベル計算の実行} -\label{section:meta-level-exec} -Meta DataSegment と Meta CodeSegment の定義を行なったので、残るは実行である。 - -実行はノーマルレベルにおいては軽量継続 \verb/goto/ を定義することによって表せた。 -メタレベル実行ではそれを Meta CodeSegment と Meta DataSegment を扱えるように拡張する。 -Meta DataSegment は Parameterized Module の引数 \verb/Context/ に相当するため、Meta CodeSegment は Context を取って Context を返す CodeSegment となる。 -軽量継続 \verb/goto/ と区別するために名前を \verb/exec/ とするリスト~\ref{src:agda-exec}のように定義できる。 -行なっていることは Meta CodeSegment の本体部分に Meta DataSegment を渡す、という \verb/goto/ と変わらないが、\verb/set/ と \verb/get/ を用いることで上位型である任意の DataSegment を実行する CodeSegment も Meta CodeSegment として一様に実行できる。 - -\lstinputlisting[label=src:agda-exec, caption=Agda におけるメタレベル実行の定義] {src/Exec.agda.replaced} - -実行例として、リスト~\ref{src:goto} に示していた a と b の値を加算して c に代入するプログラムを考える。 -実行する際に c の値を \verb/c'/ に保存してから加算ようなメタ計算を考える。 -c の値を \verb/c'/ に保存するタイミングは軽量継続時にユーザが指定する。 -よって軽量継続を行なうのと同等の情報を保持してなくてはならない。 -そのために Meta Meta DataSegment \verb/Meta/ には制御を移す対象であるノーマルレベル CodeSegment を持つ。 -値を格納する \verb/c'/ の位置は Meta DataSegment でも Meta Meta DataSegment でも構わないが、今回は Meta Meta DataSegemnt に格納するものとする。 -それらを踏まえた上での Meta Meta DataSegment の Agda 上での定義は~\ref{src:agda-mmds}のようになる。 -なお、\verb/goto/ などの名前の衝突を避けるためにノーマルレベルの定義は \verb/N/ に、メタレベルの定義は \verb/M/ へと名前を付けかえている。 - -\lstinputlisting[label=src:agda-mmds, caption=Agda における Meta Meta DataSegment の定義例] {src/MetaMetaDataSegment.agda.replaced} - -定義した \verb/Meta/ を利用して、c を \verb/c'/に保存するメタ計算 \verb/push/ を定義する。 -より構文が CbC に似るように \verb/gotoMeta/ を糖衣構文的に定義する。 -\verb/gotoMeta/ や \verb/push/ で利用している \verb/liftContext/ や \verb/liftMeta/ はノーマルレベル計算をメタ計算レベルとするように型を明示的に変更するものである。 -結果的に \verb/main/ の \verb/goto/ を \verb/gotoMeta/ に置き換えることにより、c の値を計算しながら保存できる。 -リスト~\ref{src:agda-mmcs} に示したプログラムでは、通常レベルのコードセグメントを全く変更せずにメタ計算を含む形に拡張している。 -加算を行なう前の \verb/c/ の値が \verb/70/ であったとした時、計算結果 \verb/150/ は \verb/c/ に格納されるが、\verb/c'/には\verb/70/に保存されている。 - -\lstinputlisting[label=src:agda-mmcs, caption=Agda における Meta Meta CodeSegment の定義と実行例] {src/MetaMetaCodeSegment.agda.replaced} - -CodeSegment や Meta CodeSegment などの定義が多かっため、どの処理やデータがどのレベルに属するか複雑になったため、一度図~\ref{fig:meta-hierarchy}にてまとめる。 -Meta DataSegment を含む任意の DataSegment は Meta DataSegment になりえるので、この階層構造は任意の段数定義することが可能である。 - -\begin{figure}[htbp] - \begin{center} - \includegraphics[width=450pt]{fig/meta-hierarchy.pdf} - \caption{メタの階層構造} - \label{fig:meta-hierarchy} - \end{center} -\end{figure} - -また、この節で取り扱ったソースコードは付録に付す。 - -% }}} - -% {{{ Agda を用いた Continuation based C の証明 - -\section{Agda を用いた Continuation based C の証明} -\label{section:cbc-proof} -Agda において CbC の CodeSegment と DataSegment を定義することができた。 -実際の CbC のコードを Agda で記述し、それらの性質を証明していく。 - -ここではGearsOS が持つ DataSegment \verb/SingleLinkedStack/ を証明していく。 -この\verb/SingleLinkedStack/はポインタを利用した片方向リストを用いて実装されている。 - -CbC における DataSegment \verb/SingleLinkedStack/ の定義はリスト~\ref{src:cbc-stack}のようになっている。 - -\lstinputlisting[label=src:cbc-stack, caption=CbC における構造体 stack の定義] {src/stack.h} - -次に Agda における \verb/SingleLinkedStack/の定義について触れるが、Agda にはポインタが無いため、メモリ確保や\verb/NULL/の定義は存在しない。 -CbC におけるメモリ確保部分はノーマルレベルには出現しないと仮定し、\verb/NULL/の表現にはAgda の標準ライブラリに存在する \verb/Data.Maybe/ を用いる。 - -\verb/Data.Maybe/ の \verb/maybe/ 型は、コンストラクタを二つ持つ。 -片方のコンストラクタ \verb/just/ は値を持ったデータであり、ポインタの先に値があることに対応している。 -一方のコンストラクタ \verb/nothing/ は値を持たない。 -これは値が存在せず、ポインタの先が確保されていない(\verb/NULL/ ポインタである)ことを表現できる。 - -\lstinputlisting[label=src:agda-maybe, caption=Agda における Maybe の定義] {src/Maybe.agda.replaced} - -Maybe を用いて片方向リストを Agda 上に定義するとリスト~\ref{src:agda-stack}のようになる。 -CbC とほぼ同様の定義ができている。 -CbC、 Agda 共に\verb/SingleLinkedStack/ は \verb/Element/ 型の \verb/top/ を持っている。 -\verb/Element/ 型は値と次の \verb/Element/ を持つ。 -CbC ではポインタで表現していた部分が Agda では Maybe で表現されているが、\verb/Element/ 型の持つ情報は変わっていない。 - -\lstinputlisting[label=src:agda-stack, caption=Agda における片方向リストを用いたスタックの定義] {src/AgdaStack.agda.replaced} - -Agda で片方向リストを利用する DataSegment の定義をリスト~\ref{src:agda-stack-ds}に示す。 -ノーマルレベルからアクセス可能な場所として \verb/Context/ に \verb/element/ フィールドを追加する。 -そしてノーマルレベルからアクセスできないよう分離した Meta Meta DataSegment である \verb/Meta/ にスタックの本体を格納する。 -CbC における実装では \verb/.../ で不定であった \verb/next/ も、agda ではメタレベルのコードセグメント \verb/nextCS/ となり、きちんと型付けされている。 - -\lstinputlisting[label=src:agda-stack-ds, caption=スタックを利用するための DataSegment の定義] {src/AgdaStackDS.agda.replaced} - -次にスタックへの操作に注目する。 -スタックへと値を積む \verb/pushSingleLinkedStack/ と値を取り出す \verb/popSingleLinkedStack/ の CbC 実装をリスト~\ref{src:cbc-push-pop}に示す。 -\verb/SingleLinkedStack/ は Meta CodeSegment であり、メタ計算を実行した後には通常の CodeSegment へと操作を移す。 -そのために \verb/next/ という名前で次のコードセグメントを保持している。 -具体的な \verb/next/ はコンパイル時にしか分からないため、\verb/.../ 構文を用いて不定としている。 - -\verb/pushSingleLinkedStack/ は \verb/element/ を新しく確保し、値を入れた後に \verb/next/ へと繋げ、 \verb/top/ を更新して軽量継続する。 -\verb/popSingleLinkedStack/ は先頭が空でなければ先頭の値を \verb/top/ から取得し、\verb/element/を一つ進める。 -値が空であれば \verb/data/ を \verb/NULL/ にしたまま軽量継続を行なう。 - -\lstinputlisting[label=src:cbc-push-pop, caption= CbC における SingleLinkedStack を操作する Meta CodeSegment] {src/singleLinkedStack.c} - -次に Agda における定義をリスト~\ref{src:agda-push-pop}に示す。 -同様に \verb/pushSingleLinkedStack/ と \verb/popSingleLinkedStack/ を定義している。 -\verb/pushsinglelinkedstack/ では、スタックの値を更新したのちにノーマルレベルの CodeSegment である \verb/n/ を \verb/exec/ している。 -なお、 \verb/liftMeta/ はノーマルレベルの計算をメタレベルとする関数である。 - -実際に値を追加する部分は where 句に定義された関数 \verb/push/ である。 -これはスタックへと積む値が空であれば追加を行なわず、値がある時は新たに element を作成して top を更新している。 -本来の CbC の実装では空かチェックはしていないが、値が空であるかに関わらずにスタックに積んでいるために挙動は同じである。 - -次に \verb/popSingleLinkedStack/ に注目する。 -こちらも操作後に \verb/nextCS/ へと継続を移すようになっている。 - -実際に値を取り出す操作はノーマルレベルからアクセスできる \verb/element/ の値の確定と、アクセスできない \verb/stack/ の更新である。 - -\verb/element/については、 \verb/top/ が空なら取り出した後の値は無いので \verb/element/ は \verb/nothing/ である。 -\verb/top/ が空でなければ \verb/element/ は \verb/top/ の値となる。 - -\verb/stack/ は空なら空のままであり、\verb/top/ に値があればその先頭を捨てる。 -ここで、\verb/pop/ の実装はスタックが空であっても、例外を送出したり停止したりせずに処理を続行できることが分かる。 - -\lstinputlisting[label=src:agda-push-pop, caption=Agda における片方向リストを用いたスタックの定義] {src/AgdaPushPop.agda.replaced} - -また、この章で取り上げた CbC と Agda の動作するソースコードは付録に載せる。 - -% }}} - -% {{{ スタックの実装の証明 -\section{スタックの実装の証明} -\label{section:stack-proof} -定義した SingleLinkedStack に対して証明を行なっていく。 -ここでの証明は SingleLinkedStack の処理が特定の性質を持つことを保証することである。 - -例えば - -\begin{itemize} - \item スタックに積んだ値は取り出せる - \item 値は複数積むことができる - \item スタックから値を取り出すことができる - \item スタックから取り出す値は積んだ値である - \item スタックから値を取り出したらその値は無くなる - \item スタックに値を積んで取り出すとスタックの内容は変わらない -\end{itemize} - -といった多くの性質がある。 - -ここでは、最後に示した「スタックに値を積んで取り出すとスタックの内容は変わらない」ことについて示していく。 -この性質を具体的に書き下すと以下のようになる。 - -\begin{definition} - 任意のスタック s に対して - - \begin{itemize} - \item 任意の値n - \item 値xを積む操作 push(x, s) - \item 値を一つスタックから取り出す操作 pop(s) - \end{itemize} - - がある時、 - - pop . push(n) s = s - - である。 -\end{definition} - -これを Agda 上で定義するとリスト~\ref{src:agda-push-pop-type-1} のようになる。 -Agda 上の定義ではスタックそのものではなく、スタックを含む任意の \verb/Meta/ に対してこの性質を証明する。 -この定義が \verb/Meta/ の値によらず成り立つことを、自然数の加算の交換法則と同様に等式変形を用いて証明していく。 - -\lstinputlisting[label=src:agda-push-pop-type-1, caption=Agda におけるスタックの性質の定義(1)] {src/PushPopType.agda.replaced} - -今回注目する条件分けは、スタック本体である \verb/stack/ と、push や pop を行なうための値を格納する \verb/element/ である。 -それぞれが持ち得る値を場合分けして考えていく。 - -\begin{itemize} - \item スタックが空である場合 - - \begin{itemize} - \item element が存在する場合 - - 値が存在するため、 push は実行される。 - push が実行されたためスタックに値があるため、pop が成功する。 - pop が成功した結果スタックは空となるため元のスタックと同一となり成り立つ。 - - \item element が存在しない場合 - - 値が存在しないため、 push が実行されない。 - push が実行されなかったため、スタックは空のままであり、pop も実行されない。 - 結果スタックは空のままであり、元のスタックと一致する。 - \end{itemize} - - \item スタックが空でない場合 - - \begin{itemize} - \item element が存在する場合 - - element に設定された値 n が push され、スタックに一つ値が積まれる。 - スタックの先頭は n であるため、pop が実行されて n は無くなる。 - 結果、スタックは実行する前の状態に戻る。 - - \item element が存在しない場合 - - element に値が存在しないため、push は実行されない。 - スタックは空ではないため、popが実行され、先頭の値が無くなる。 - 実行後、スタックは一つ値を失なっているため、これは成りたたない。 - \end{itemize} -\end{itemize} - -スタックが空でなく、push する値が存在しないときにこの性質は成り立たないことが分かった。 -また、\verb/element/ が空でない制約を仮定に加えることでこの命題は成り立つようになる。 - -push 操作と pop 操作を連続して行なうとスタックが元に復元されることは分かった。 -ここで SingleLinkedStack よりも範囲を広げて \verb/Meta/ も復元されるかを考える。 -一見これも自明に成り立ちそうだが、push 操作と pop 操作は操作後に実行される CodeSegment を持っている。 -この CodeSegment は任意に設定できるため、\verb/Meta/ 内部の DataSegement が書き換えられる可能性がある。 -よってこれも制約無しでは成り立たない。 - -逆にいえば、CodeSegment を指定してしまえば \verb/Meta/ に関しても push/pop の影響を受けないことを保証できる。 -全く値を変更しない CodeSegment \verb/id/ を指定した際には自明にこの性質が導ける。 -実際、 Agda 上でも等式変形を明示的に指定せず、定義からの推論でこの証明を導ける(リスト~\ref{src:agda-push-pop-proof})。 - -なお、今回 SingleLinkedStack に積むことができる値は Agda の標準ライブラリの(\verb/Data.Nat/)モジュールにおける自然数型 $ \mathbb{N} $ としている。 -これはスタックを利用する際に具体的な値があると証明に有用であるからである。 -push/pop 操作の後の継続が \verb/Meta/ に影響を与えない制約は \verb/id-meta/ に表れている。 -これは \verb/Meta/ を構成する要素を受け取り、継続先の CodeSegment に恒等関数 \verb/id/ を指定している。 -加えて、スタックが空で無い制約 where 句の \verb/meta/ に表れている。 -必ずスタックの先頭 \verb/top/ には値xが入っており、それ以降の値は任意としている。 -よってスタックは必ず一つ以上の値を持ち、空でないという制約を表わせる。 -証明は refl によって与えられる。 -つまり定義から自明に推論可能となっている。 - -\lstinputlisting[label=src:agda-push-pop-proof, caption=Agdaにおけるスタックの性質の証明(1)] {src/AgdaPushPopProof.agda.replaced} - -ここで興味深い点は、 SingleLinkedStack の実装から証明に仮定が必要なことが証明途中でに分かった点にある。 -例えば、CbC の SingleLinkedStack 実装の push/pop 操作は失敗しても成功しても指定された CodeSegment に軽量継続する。 -この性質により、指定された CodeSegment によっては、スタックの操作に関係なく \verb/Meta/ の内部の DataSegemnt が書き換えられる可能性があることが分かった。 -スタックの操作の際に行なわれる軽量継続の利用方法は複数考えられる。 -例えば、スタックが空である際に pop を行なった時はエラー処理用の継続を行なう、といった実装も可能である。 -実装が異なれば、同様の性質でも証明は異なるものとなる。 -このように、実装そのものを適切に型システムで定義できれば、明示されていない実装依存の仕様も証明時に確定させることができる。 - -証明した定理をより一般的な「任意の自然数回だけスタックへ値を積み、その後同じ回数スタックから値を取り出すとスタックは操作前と変わらない」という形に拡張する。 -この性質を Agda で定義するとリスト~\ref{src:agda-n-push-n-pop}のようになる。 -自然数n回だけ push/pop することを記述するために Agda 上に \verb/n-push/ 関数と \verb/n-pop/ 関数を定義している。 -それぞれ一度操作を行なった後に再帰的に自身を呼び出す再帰関数である。 - -\lstinputlisting[label=src:agda-n-push-n-pop, caption=Agda におけるスタックの性質の定義(2)] {src/AgdaNPushNPop.agda.replaced} - -この性質の証明は少々複雑である。 -結論から先に示すとリスト~\ref{src:agda-n-push-n-pop-proof}のように証明できる。 - -\lstinputlisting[label=src:agda-n-push-n-pop-proof, caption=Agda におけるスタックの性質の証明(2)] {src/AgdaNPushNPopProof.agda.replaced} - -これは以下のような形の証明になっている。 - -\begin{itemize} - \item 「n回pushした後にn回popしても同様になる」という定理を \verb/n-push-pop/ とおく。 - \item \verb/n-push-pop/ は自然数nと特定の \verb/Meta/ に対して \\ - \verb/exec (n-pop (suc n)) . (n-push (suc n))) m = m/ が成り立つことである - \item 特定の \verb/Meta/ とは、 push/pop 操作の後の継続が DataSegment を変更しない \verb/Meta/ である。 - \item また、簡略化のために \verb/csComp/ による CodeSegment の合成を二項演算子 \verb/./ とおく - \begin{itemize} - \item 例えば \verb/exec (csComp f g) x/ は \verb/exec (f . g) x/ となる。 - \end{itemize} - - \item \verb/n-push-pop/ を証明するための補題 \verb/pop-n-push/ を定義する - \item \verb/n-push-pop/ とは「n+1回push して1回 pop することは、n回pushすることと等しい」という補題である。 - \item \verb/n-push-pop/ は \verb/exec (pop . n-push (suc n)) m = exec (n-push n) m/ と表現できる。 - \item \verb/n-push-pop/ の n が zero の時は直ちに成り立つ。 - \item \verb/n-push-pop/ の n が zero でない時(suc n である時)は以下のように証明できる。 - - \begin{itemize} - \item \verb/exec (n-push (suc n)) m/ を \verb/X/ とおく - \item \verb/exec (pop . n-push (suc (suc n))) m = X/ - \item n-push の定義より \verb/exec (pop . (n-push (suc n) . push)) m = X/ - \item 補題 exec-comp より \verb/exec (pop (exec (n-push (suc n) . push) m)) = X/ - \item 補題 exec-comp より \verb/exec (pop (exec (n-push (suc n) (exec push m)))) = X/ - \item 一度pushした結果を \verb/m'/とおくと \verb/exec (pop (exec (n-push (suc n) m'))) = X/ - \item \verb/n-push-pop/ より \verb/exec (exec (n-push n m')) = X/ - \item push の定義より \verb/exec (exec (n-push n (exec push m))) = X/ - \item n-push の定義より \verb/exec (exec (n-push (suc n) m) = X/ となる - \item 全く同一の項に変更できたので証明終了 - \end{itemize} - - - \item 次に \verb/n-push-pop/ の証明を示す。 - \item \verb/n-push-pop/ の n が zero の時は、 \verb/suc zero/ 回の push/pop が行なわれるため、\verb/push-pop/より成り立つ。 - \item \verb/n-push-pop/ の n が zero でない時は以下により証明できる。 - - \begin{itemize} - \item \verb/exec ((n-pop (suc n)) . (n-push (suc n))) m = m / を示せれば良い。 - \item \verb/X/ に注目した時 n-pop の定義より \verb/exec (n-pop n) . pop . (n-push (suc n)) m = m/ - \item exec-comp より \verb/exec (n-pop n) (exec pop (n-push (suc n)) m) = m/ - \item exec-comp より \verb/exec (n-pop n) (exec pop (exec (n-push (suc n)) m)) = m/ - \item exec-comp より \verb/exec (n-pop n) (exec pop . (n-push (suc n)) m) = m/ - \item pop-n-push より \verb/exec (n-pop n) (exec (n-push n) m) = m/ - \item n-push-pop より \verb/m = m/ となり証明終了。 - \item なお、n-push-pop は (suc n) が n に減少するため、確実に停止することから自身を自身の証明に適用している。 - \end{itemize} -\end{itemize} - -push-pop を一般化した n-push-pop を証明することができた。 -n-push-pop は証明の途中で補題 pop-n-push と push-pop を利用した定理である。 -このように、CbC で記述されたプログラムを Agda 上に記述することで、データ構造の性質を定理として証明することができた。 -これらの証明機構を CbC のコンパイラやランタイム、モデルチェッカなどに組み込むことにより CbC は CbC で記述されたコードを証明することができるようになる。 -なお、本論文で取り扱っている Agda のソースコードは可読性の向上のために暗黙的な引数を省略している。 -完全なコードは付録に付す。 - -% }}} -
--- a/paper/cbc.tex Sat Jan 06 19:04:39 2018 +0900 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,202 +0,0 @@ -\chapter{Continuation based C} -\label{chapter:cbc} - -Continuation based C (CbC)は当研究室で開発しているプログラミング言語であり、OSや組み込みソフトウェアを主な対象としている。 -CbC は C言語の下位の言語であり、構文はほぼC言語と同じものを持つが、よりアセンブラに近い形でプログラムを記述する。 -CbC は CodeSegment と呼ばれる単位で処理を定義し、それらを組み合わせることにでプログラム全体を構成する。 -データの単位は DataSegment と呼ばれる単位で定義し、それら CodeSegment によって変更していくことでプログラムの実行となる。 -CbC の処理系には llvm/clang による実装\cite{110009766999} と gcc\cite{weko_82695_1}による実装などが存在する。 - -% {{{ section: CodeSegment と DataSegment - -\section{CodeSegment と DataSegment} -本研究室では検証を行ないやすいプログラムの単位として CodeSegment と DataSegment を用いるプラグラミングスタイルを提案している。 - -CodeSegment は処理の単位である。 -入力を受け取り、それに対して処理を行なった後を出力を行なう。 -また、CodeSegment は他の CodeSegment と組み合わせることが可能である。 -あるCodeSegment A を CodeSegment B に接続した場合、 A の出力は B の入力となる(図~\ref{fig:csds})。 - -DataSegment は CodeSegment が扱うデータの単位であり、処理に必要なデータが全て入っている。 -CodeSegment の入力となる DataSegment は Input DataSegment と呼ばれ、出力は Output DataSegment と呼ばれる。 -CodeSegment A と CodeSegment B を接続した時、A の Output DataSegment は B の入力 Input DataSegment となる。 - -\begin{figure}[htbp] - \begin{center} - \includegraphics[scale=0.5]{fig/csds.pdf} - \caption{CodeSegment と DataSegement} - \label{fig:csds} - \end{center} -\end{figure} - -% }}} - -% {{{ Continuation based C における CodeSegment と DataSegment - -\section{Continuation based C における CodeSegment と DataSegment} -最も基本的な CbC のソースコードをリスト\ref{src:goto}に、ソースコードが実行される流れを図\ref{fig:goto}に示す。 -Continuation based C における CodeSegment は返り値を持たない関数として表現される。 -CodeSegment を定義するためには、C言語の関数を定義する構文の返り値の型部分に \verb/__code/ キーワードを指定する。 -Input DataSegment は関数の引数として定義される。 -次の CodeSegment へ処理を移す際には \verb/goto/ キーワードの後に CodeSegment 名と Input DataSegment を指定する。 -処理の移動を軽量継続と呼び、リスト\ref{src:goto}内の \verb/goto cs1(a+b);/ がこれにあたる。 -この時の \verb/(a+b)/ が次の CodeSegment である cs1 の Input DataSegment となる cs0 の Output DataSegment である。 - -\lstinputlisting[label=src:goto, caption=CodeSegment の軽量継続] {src/goto.cbc} - -\begin{figure}[htbp] - \begin{center} - \includegraphics[scale=1.0]{fig/goto.pdf} - \caption{CodeSegment の軽量継続} - \label{fig:goto} - \end{center} -\end{figure} - -Scheme などの call/cc といった継続はトップレベルから現在までの位置を環境として保持する。 -通常環境とは関数の呼び出しスタックの状態である。 -CbC の軽量継続は呼び出し元の情報を持たないため、スタックを破棄しながら処理を続けていく。 -よって、リスト\ref{src:goto} のプログラムでは cs0 から cs1 へと継続した後には cs0 へ戻らずに処理を続ける。 - -もう少し複雑な CbC のソースコードをリスト\ref{src:factrial}に、実行される流れを図\ref{fig:factrial}に示す。 -このソースコードは整数の階乗を求めるプログラムである。 -CodeSegment factorial0 では自分自身への再帰的な継続を用いて階乗を計算している。 -軽量継続時には関数呼び出しのスタックは存在しないが、計算中の値を DataSegment で持つことで再帰を含むループ処理も行なうことができる。 - -\lstinputlisting[label=src:factrial, caption=階乗を求める CbC プログラム] {src/factrial.cbc} - -\begin{figure}[htbp] - \begin{center} - \includegraphics[scale=0.8]{fig/factorial.pdf} - \caption{階乗を求める CbC プログラム} - \label{fig:factrial} - \end{center} -\end{figure} - -% }}} - -% {{{ MetaCodeSegment と MetaDataSegment - -\section{MetaCodeSegment と MetaDataSegment} -プログラムを記述する際、本来行ないたい計算の他にも記述しなければならない部分が存在する。 -メモリの管理やネットワーク処理、エラーハンドリングや並列処理などがこれにあたり、本来行ないたい計算と区別してメタ計算と呼ぶ。 -プログラムを動作させるためにメタ計算部分は必須であり、しばしば本来の処理よりも複雑度が高い。 - -CodeSegment を用いたプログラミングスタイルでは計算とメタ計算を分離して記述する。 -なお、分離した計算は階層構造を持つ。 -本来行ないたい処理はノーマルレベルであり、メタ計算はメタレベルとして上位に位置する。 -複雑なメタ計算部分をライブラリやOS側が提供することで、ユーザはノーマルレベルの計算の記述に集中することができる。 -また、ノーマルレベルのプログラムに必要なメタ計算を追加することで、並列処理やネットワーク処理などを含むプログラムに拡張できる。 -さらに、ノーマルレベルからはメタレベルは隠蔽されているため、メタ計算の実装を切り替えることも可能である。 -例えば、並列処理のメタ計算用いたプログラムを作成する際、CPUで並列処理を行なうメタ計算とGPUで並列処理メタ計算を環境に応じて作成することができる。 - -なお、メタ計算を行なう CodeSegment は Meta CodeSegment と呼び、メタ計算に必要な DataSegment は Meta DataSegment と呼ぶ。 -Meta CodeSegment は CodeSegment の前後にメタ計算を挟むことで実現され、Meta DataSegment は DataSegment を含む上位の DataSegment として実現できる。 -よって、メタ計算は通常の計算を覆うように計算を拡張するものだと考えられる(図\ref{fig:meta})。 - -\begin{figure}[htbp] - \begin{center} - \includegraphics[scale=0.5]{fig/meta.pdf} - \caption{Meta CodeSegment と Meta DataSegment} - \label{fig:meta} - \end{center} -\end{figure} - -% }}} - -% {{{ Continuation based C におけるメタ計算の例: GearsOS -\section{Continuation based C におけるメタ計算の例: GearsOS} -CbC を用いてメタ計算を実現した例として、GearsOS\cite{weko_142109_1}が存在する。 -GearsOS は並列に、信頼性高く動作することを目標としたOS であり、 マルチコアCPUやGPU環境での動作を対象としている。 -現在はOSの設計と並列処理部分の実装が行なわれている。 -GearsOS におけるメタ計算はMonad\cite{Moggi:1991:NCM:116981.116984}を用いている~\cite{kkb-master}。 -実装済みのメタ計算はメモリの管理、並列に書き込むことが可能な Synchronized Queue、データの保存用の非破壊赤黒木がある。 - -GearsOS では CodeSegment と DataSegment はそれぞれ CodeGear と DataGear と呼ばれている。 -マルチコアCPU環境では CodeGear と CodeSegment は同一だが、GPU 環境では CodeGear には OpenCL~\cite{opencl}/CUDA~\cite{cuda} における kernel も含まれる。 -kernel とは GPU で実行される関数のことであり、GPU上のメモリに配置されたデータ群に対して並列に実行される。 -通常 GPU でデータの処理を行なう場合は - -\begin{itemize} - \item データをメインメモリから GPUのメモリへ転送 - \item 転送終了を同期で確認 - \item kernel 起動(GPUメモリ上のデータに対して並列に処理) - \item 処理終了を同期で確認 - \item 計算結果であるデータを GPU のメモリからメインメモリへ転送 - \item 転送終了を同期で確認 -\end{itemize} - -といった手順が必要であり、ユーザは処理したいデータの位置などを意識しながらプログラミングする必要がある。 -GearsOS では CPU/GPU での処理をメタ計算としてユーザから隠すことにより、 CodeGear が実行されるデバイスや DataGear の位置を意識する必要がなくなる。 - -GearsOS で利用する Meta DataGear には以下のものが含まれる。 - -\begin{itemize} - \item DataGear の型情報 - \item DataGear を格納するメモリの情報 - \item CodeGear の名前と CodeGear の関数ポインタ との対応表 - \item CodeGear が参照する DataGear へのポインタ -\end{itemize} - -実際の GearsOS におけるメモリ管理を含むメタ計算用の Meta DataGear の定義例をリスト\ref{src:context}に示す。 -Meta DataGear は Context という名前の構造体で定義されている。 -通常レベルの DataGear も構造体で定義されているが、メタ計算側から見た DataGear はそれぞれの構造体の共用体となっており、一様に扱える。 - -\lstinputlisting[label=src:context, caption=GearsOS における Meta DataGearの定義例] {src/context.h} - -リスト~\ref{src:context}のソースコードは以下のように対応している。 - -\begin{itemize} - \item DataGear の型情報 - - DataGear は構造体を用いて定義する(リスト\ref{src:context} 27-46行)。 - Tree や Node、 Allocate 構造体が DataGear に相当する。 - メタ計算は任意の DataGear 扱うために全ての DataGear を扱える必要がある。 - 全ての DataGear の共用体を定義することで、 DataGear を一律に扱うことができる(リスト\ref{src:context} 26-47行)。 - メモリを確保する場合はこの型情報からサイズを決定する。 - - \item DataGear を格納するメモリの情報 - - メモリ領域の管理は、事前に領域を確保した後、必要に応じてその領域を割り当てることで実現する。 - そのために Context は割り当て済みの領域 heap と、割り当てた DataGear の数 dataNum を持つ。 - - \item CodeGear の名前と CodeGear の関数ポインタ との対応表 - - CodeGear の名前と CodeGear の関数ポインタの対応は enum と関数ポインタによって実現されている。 - CodeGear の名前は enum (リスト\ref{src:context} 5-9行) で定義され、コンパイル後には整数へと変換される。 - プログラム全体で利用する CodeGear は code フィールドに格納されており、enum を用いてアクセスする。 - この対応表を動的に変更することで、実行時に比較ルーチンなどを変更することが可能になる。 - - \item CodeGear が参照する DataGear へのポインタ - - Meta CodeGear は Context を引数に取る CodeGear として定義されている。 - そのため、Meta CodeGear が DataGear の値を使う為には Context から DataGear を取り出す必要がある。 - 取り出す必要がある DataGear は enum を用いて定義し(リスト\ref{src:context} 11-14行)、 CodeGear を実行する際に data フィールドから取り出す。 -\end{itemize} - -Meta CodeGear は定義された Meta DataGear を処理する CodeGear である。 -メモリ管理や並列処理の待ち合わせといった処理はこのメタレベルにしか表れない。 - -GearsOS においては軽量継続もメタ計算として実現されている。 -とある CodeGear から次の CodeGear へと軽量継続する際には、次に実行される CodeGear の名前を指定する。 -その名前を Meta CodeGear が解釈し、対応する CodeGear へと処理を引き渡す(リスト~\ref{src:meta}の \verb/meta/)。 - -\lstinputlisting[label=src:meta, caption=通常の CodeSegment の軽量継続] {src/meta.c} - -CodeGear と名前の対応は Meta DataGear に格納されており、従来の OS の Process や Thread に相当する。 -名前の対応を動的に切り替えたり、Thread ごとに切り替えることにより、通常レベルのプログラムを変更せず実行を上書きできる。 -これは従来の OS の Dynamic Loading Libary や Command の呼び出しに相当する。 - -また、通常レベルの CodeGear から Meta DataGear を操作できてしまうと、ユーザがメタレベル操作を自由に記述できてしまい、メタ計算を分離した意味が無くなってしまう。 -これを防ぐために、CodeGear を実行する際は Meta DataGear から必要な DataGear だけを渡す。 -このように、 Meta DataGear から DataGear を取り出す Meta CodeGear を stub と呼ぶ。 -stub の例をリスト\ref{src:stub}に示す。 -\lstinputlisting[label=src:stub, caption=GearsOS における stub Meta CodeSegment] {src/stub.cbc} - -stub は Context が持つ DataGear のポインタ data に対して enum を用いてアクセスしている。 -なお、現在はメタレベルの計算とノーマルレベルの分離はコンパイラ側がサポートしていないため、引数に Meta DataGear である Context が渡されているが、本来はノーマルレベルではアクセスできない。 - -また、GearsOS におけるメタ計算として CodeGear のモデル検査がある。 -通常レベルの CodeGear を変更することなく、その仕様を検証するものである。 -個々の CodeGear の仕様を検証することにより、より信頼性の高いOSを目指す。 - -% }}}
--- a/paper/history.tex Sat Jan 06 19:04:39 2018 +0900 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,6 +0,0 @@ -\chapter*{発表履歴} -\begin{itemize} -\item 比嘉健太, 河野真治. Agda入門. オープンソースカンファレンス2014 Okinawa, May 2014. -\item 比嘉健太, 河野真治. 形式手法を学び始めて思うことと、形式手法を広めるには. 情報処理学会ソフトウェア工学研究会(IPSJ SIGSE) ウィンターワークショップ2015・イン・宜野湾(WWS2015), Jan 2015. -\item 比嘉健太, 河野真治. Continuation based C を用いたプログラムの検証手法. 2016年並列／分散／協調処理に関する『松本』サマー・ワークショップ(SWoPP2016) 情報処理学会・プログラミング研究会 第110回プログラミング研究会(PRO-2016-2) Aug 2016. -\end{itemize}
--- a/paper/sources.tex Sat Jan 06 19:04:39 2018 +0900 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,29 +0,0 @@ -\chapter{ソースコード一覧} -\label{chapter:sources} -本論文中に取り上げた Agda の動作するソースコードを示す。 - -\section{部分型の定義} -リスト~\ref{src:agda-subtype} に Agda 上で定義した CbC の部分型の定義を示す。 - -\lstinputlisting[label=src:agda-subtype, caption=Agda 上で定義した CbC の部分型の定義(subtype.agda)] {src/subtype.agda.replaced} - -\section{ノーマルレベル計算の実行} -\ref{section:normal-level-exec}節で取り上げたソースコードをリスト~\ref{src:normal-level-exec}に示す。 -CbC のコードにより近づけるよう Agda 上の \verb/Data.Nat/ を \verb/Int/ という名前に変更している。 - -\lstinputlisting[label=src:normal-level-exec, caption=ノーマルレベル計算例の完全なソースコード(atton-master-sample.agda)] {src/atton-master-sample.agda.replaced} - -\section{メタレベル計算の実行} -\ref{section:meta-level-exec}節で取り上げたソースコードをリスト~\ref{src:meta-level-exec}に示す。 - -\lstinputlisting[label=src:meta-level-exec, caption=メタレベル計算例の完全なソースコード(atton-master-meta-sample.agda)] {src/atton-master-meta-sample.agda.replaced} - -\section{Agda を用いた Continuation based C の検証} -\ref{section:cbc-proof}節で取り上げたソースコードを以下に示す。 - -\lstinputlisting[label=src:cbc-proof-cbc, caption=Agda を用いた Continuation based C の検証コード(SingleLinkedStack.cbc)] {src/SingleLinkedStack.cbc} -\lstinputlisting[label=src:cbc-proof-agda, caption=Agda を用いた Continuation based C の検証コード(stack-subtype.agda)] {src/stack-subtype.agda.replaced} - -\section{スタックの実装の検証} -\ref{section:stack-proof}節で取り上げたソースコードをリスト~\ref{src:stack-proof}に示す。 -\lstinputlisting[label=src:stack-proof, caption=スタックの実装の検証コード(stack-subtype-sample.agda)] {src/stack-subtype-sample.agda.replaced}
--- a/paper/src/AgdaBasics.agda Sat Jan 06 19:04:39 2018 +0900 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,1 +0,0 @@ -module AgdaBasics where
--- a/paper/src/AgdaBool.agda Sat Jan 06 19:04:39 2018 +0900 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,3 +0,0 @@ -data Bool : Set where - true : Bool - false : Bool
--- a/paper/src/AgdaElem.agda Sat Jan 06 19:04:39 2018 +0900 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,3 +0,0 @@ -elem : {A : Set} {{eqA : Eq A}} → A → List A → Bool -elem {{eqA}} x (y ∷ xs) = (Eq._==_ eqA x y) || (elem {{eqA}} x xs) -elem x [] = false
--- a/paper/src/AgdaElemApply.agda Sat Jan 06 19:04:39 2018 +0900 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,3 +0,0 @@ -listHas4 : Bool -listHas4 = elem 4 (3 ∷ 2 ∷ 5 ∷ 4 ∷ []) -- true -
--- a/paper/src/AgdaFunction.agda Sat Jan 06 19:04:39 2018 +0900 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,2 +0,0 @@ -f : Bool -> Bool -f x = true
--- a/paper/src/AgdaId.agda Sat Jan 06 19:04:39 2018 +0900 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,5 +0,0 @@ -identity : (A : Set) -> A -> A -identity A x = x - -identity-zero : Nat -identity-zero = identity Nat zero
--- a/paper/src/AgdaImplicitId.agda Sat Jan 06 19:04:39 2018 +0900 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,11 +0,0 @@ -id : {A : Set} -> A -> A -id x = x - -id-zero : Nat -id-zero = id zero - -id' : {A : Set} -> A -> A -id' {A} x = x - -id-true : Bool -id-true = id {Bool} true
--- a/paper/src/AgdaImport.agda Sat Jan 06 19:04:39 2018 +0900 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,6 +0,0 @@ -import Data.Nat -- import module -import Data.Bool as B -- renamed module -import Data.List using (head) -- import Data.head function -import Level renaming (suc to S) -- import module with rename suc to S -import Data.String hiding (_++_) -- import module without _++_ -open import Data.List -- import and expand Data.List
--- a/paper/src/AgdaInstance.agda Sat Jan 06 19:04:39 2018 +0900 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,9 +0,0 @@ -_==Nat_ : Nat -> Nat -> Bool -zero ==Nat zero = true -(suc n) ==Nat zero = false -zero ==Nat (suc m) = false -(suc n) ==Nat (suc m) = n ==Nat m - -instance - natHas== : Eq Nat - natHas== = record { _==_ = _==Nat_}
--- a/paper/src/AgdaLambda.agda Sat Jan 06 19:04:39 2018 +0900 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,5 +0,0 @@ -not-apply : Bool -> Bool -not-apply = (\b -> not b) -- use lambda - -not-apply : Bool -> Bool -not-appy b = not b -- not use lambda
--- a/paper/src/AgdaModusPonens.agda Sat Jan 06 19:04:39 2018 +0900 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,2 +0,0 @@ -f : {A B C : Set} -> ((A -> B) × (B -> C)) -> (A -> C) -f = \p x -> (snd p) ((fst p) x)
--- a/paper/src/AgdaNPushNPop.agda Sat Jan 06 19:04:39 2018 +0900 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,13 +0,0 @@ -n-push : {m : Meta} {{_ : M.DataSegment Meta}} (n : ℕ) -> M.CodeSegment Meta Meta -n-push {{mm}} (zero) = M.cs {{mm}} {{mm}} id -n-push {m} {{mm}} (suc n) = M.cs {{mm}} {{mm}} (\m -> M.exec {{mm}} {{mm}} (n-push {m} {{mm}} n) (pushOnce m)) - -n-pop : {m : Meta} {{_ : M.DataSegment Meta}} (n : ℕ) -> M.CodeSegment Meta Meta -n-pop {{mm}} (zero) = M.cs {{mm}} {{mm}} id -n-pop {m} {{mm}} (suc n) = M.cs {{mm}} {{mm}} (\m -> M.exec {{mm}} {{mm}} (n-pop {m} {{mm}} n) (popOnce m)) - -pop-n-push-type : ℕ -> ℕ -> ℕ -> SingleLinkedStack ℕ -> Set₁ -pop-n-push-type n cn ce s = M.exec (M.csComp {meta} (M.cs popOnce) (n-push {meta} (suc n))) meta - ≡ M.exec (n-push {meta} n) meta - where - meta = id-meta cn ce s
--- a/paper/src/AgdaNPushNPopProof.agda Sat Jan 06 19:04:39 2018 +0900 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,58 +0,0 @@ -pop-n-push-type : ℕ -> ℕ -> ℕ -> SingleLinkedStack ℕ -> Set₁ -pop-n-push-type n cn ce s = M.exec (M.csComp (M.cs popOnce) (n-push (suc n))) meta - ≡ M.exec (n-push n) meta - where - meta = id-meta cn ce s - -pop-n-push : (n cn ce : ℕ) -> (s : SingleLinkedStack ℕ) -> pop-n-push-type n cn ce s -pop-n-push zero cn ce s = refl -pop-n-push (suc n) cn ce s = begin - M.exec (M.csComp (M.cs popOnce) (n-push (suc (suc n)))) (id-meta cn ce s) - ≡⟨ refl ⟩ - M.exec (M.csComp (M.cs popOnce) (M.csComp (n-push (suc n)) (M.cs pushOnce))) (id-meta cn ce s) - ≡⟨ exec-comp (M.cs popOnce) (M.csComp (n-push (suc n)) (M.cs pushOnce)) (id-meta cn ce s) ⟩ - M.exec (M.cs popOnce) (M.exec (M.csComp (n-push (suc n)) (M.cs pushOnce)) (id-meta cn ce s)) - ≡⟨ cong (\x -> M.exec (M.cs popOnce) x) (exec-comp (n-push (suc n)) (M.cs pushOnce) (id-meta cn ce s)) ⟩ - M.exec (M.cs popOnce) (M.exec (n-push (suc n))(M.exec (M.cs pushOnce) (id-meta cn ce s))) - ≡⟨ refl ⟩ - M.exec (M.cs popOnce) (M.exec (n-push (suc n)) (id-meta cn ce (record {top = just (cons ce (SingleLinkedStack.top s))}))) - ≡⟨ sym (exec-comp (M.cs popOnce) (n-push (suc n)) (id-meta cn ce (record {top = just (cons ce (SingleLinkedStack.top s))}))) ⟩ - M.exec (M.csComp (M.cs popOnce) (n-push (suc n))) (id-meta cn ce (record {top = just (cons ce (SingleLinkedStack.top s))})) - ≡⟨ pop-n-push n cn ce (record {top = just (cons ce (SingleLinkedStack.top s))}) ⟩ - M.exec (n-push n) (id-meta cn ce (record {top = just (cons ce (SingleLinkedStack.top s))})) - ≡⟨ refl ⟩ - M.exec (n-push n) (pushOnce (id-meta cn ce s)) - ≡⟨ refl ⟩ - M.exec (n-push n) (M.exec (M.cs pushOnce) (id-meta cn ce s)) - ≡⟨ refl ⟩ - M.exec (n-push (suc n)) (id-meta cn ce s) - ∎ - - - -n-push-pop-type : ℕ -> ℕ -> ℕ -> SingleLinkedStack ℕ -> Set₁ -n-push-pop-type n cn ce st = M.exec (M.csComp (n-pop n) (n-push n)) meta ≡ meta - where - meta = id-meta cn ce st - -n-push-pop : (n cn ce : ℕ) -> (s : SingleLinkedStack ℕ) -> n-push-pop-type n cn ce s -n-push-pop zero cn ce s = refl -n-push-pop (suc n) cn ce s = begin - M.exec (M.csComp (n-pop (suc n)) (n-push (suc n))) (id-meta cn ce s) - ≡⟨ refl ⟩ - M.exec (M.csComp (M.cs (\m -> M.exec (n-pop n) (popOnce m))) (n-push (suc n))) (id-meta cn ce s) - ≡⟨ exec-comp (M.cs (\m -> M.exec (n-pop n) (popOnce m))) (n-push (suc n)) (id-meta cn ce s) ⟩ - M.exec (M.cs (\m -> M.exec (n-pop n) (popOnce m))) (M.exec (n-push (suc n)) (id-meta cn ce s)) - ≡⟨ refl ⟩ - M.exec (n-pop n) (popOnce (M.exec (n-push (suc n)) (id-meta cn ce s))) - ≡⟨ refl ⟩ - M.exec (n-pop n) (M.exec (M.cs popOnce) (M.exec (n-push (suc n)) (id-meta cn ce s))) - ≡⟨ cong (\x -> M.exec (n-pop n) x) (sym (exec-comp (M.cs popOnce) (n-push (suc n)) (id-meta cn ce s))) ⟩ - M.exec (n-pop n) (M.exec (M.csComp (M.cs popOnce) (n-push (suc n))) (id-meta cn ce s)) - ≡⟨ cong (\x -> M.exec (n-pop n) x) (pop-n-push n cn ce s) ⟩ - M.exec (n-pop n) (M.exec (n-push n) (id-meta cn ce s)) - ≡⟨ sym (exec-comp (n-pop n) (n-push n) (id-meta cn ce s)) ⟩ - M.exec (M.csComp (n-pop n) (n-push n)) (id-meta cn ce s) - ≡⟨ n-push-pop n cn ce s ⟩ - id-meta cn ce s - ∎
--- a/paper/src/AgdaNat.agda Sat Jan 06 19:04:39 2018 +0900 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,3 +0,0 @@ -data Nat : Set where - zero : Nat - suc : Nat -> Nat
--- a/paper/src/AgdaNot.agda Sat Jan 06 19:04:39 2018 +0900 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,3 +0,0 @@ -not : Bool -> Bool -not true = false -not false = true
--- a/paper/src/AgdaParameterizedModule.agda Sat Jan 06 19:04:39 2018 +0900 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,7 +0,0 @@ -module Sort (A : Set) (_<_ : A -> A -> Bool) where -sort : List A -> List A -sort = -- 実装は省略 ... - --- Parameterized Module により N.sort や B.sort が可能 -open import Sort Nat Nat._<_ as N -open import Sort Bool Bool._<_ as B
--- a/paper/src/AgdaPattern.agda Sat Jan 06 19:04:39 2018 +0900 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,3 +0,0 @@ -not : Bool -> Bool -not false = true -not x = false
--- a/paper/src/AgdaPlus.agda Sat Jan 06 19:04:39 2018 +0900 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,3 +0,0 @@ -_+_ : Nat -> Nat -> Nat -zero + m = m -suc n + m = suc (n + m)
--- a/paper/src/AgdaProduct.agda Sat Jan 06 19:04:39 2018 +0900 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,8 +0,0 @@ -data _×_ (A B : Set) : Set where - <_,_> : A -> B -> A × B - -fst : {A B : Set} -> A × B -> A -fst < a , _ > = a - -snd : {A B : Set} -> A × B -> B -snd < _ , b > = b
--- a/paper/src/AgdaProp.agda Sat Jan 06 19:04:39 2018 +0900 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,2 +0,0 @@ -prop : Bool -prop = true
--- a/paper/src/AgdaPushPop.agda Sat Jan 06 19:04:39 2018 +0900 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,28 +0,0 @@ -pushSingleLinkedStack : Meta -> Meta -pushSingleLinkedStack m = M.exec (liftMeta n) (record m {stack = (push s e) }) - where - n = Meta.nextCS m - s = Meta.stack m - e = Context.element (Meta.context m) - push : SingleLinkedStack A -> Maybe A -> SingleLinkedStack A - push s nothing = s - push s (just x) = record {top = just (cons x (top s))} - -popSingleLinkedStack : Meta -> Meta -popSingleLinkedStack m = M.exec (liftMeta n) (record m {stack = (st m) ; context = record con {element = (elem m)}}) - where - n = Meta.nextCS m - con = Meta.context m - elem : Meta -> Maybe A - elem record {stack = record { top = (just (cons x _)) }} = just x - elem record {stack = record { top = nothing }} = nothing - st : Meta -> SingleLinkedStack A - st record {stack = record { top = (just (cons _ s)) }} = record {top = s} - st record {stack = record { top = nothing }} = record {top = nothing} - - -pushSingleLinkedStackCS : M.CodeSegment Meta Meta -pushSingleLinkedStackCS = M.cs pushSingleLinkedStack - -popSingleLinkedStackCS : M.CodeSegment Meta Meta -popSingleLinkedStackCS = M.cs popSingleLinkedStack
--- a/paper/src/AgdaPushPopProof.agda Sat Jan 06 19:04:39 2018 +0900 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,11 +0,0 @@ -id-meta : ℕ -> ℕ -> SingleLinkedStack ℕ -> Meta -id-meta n e s = record { context = record {n = n ; element = just e} - ; nextCS = (N.cs id) ; stack = s} - -push-pop-type : ℕ -> ℕ -> ℕ -> Element ℕ -> Set₁ -push-pop-type n e x s = M.exec (M.csComp {meta} (M.cs popOnce) (M.cs pushOnce)) meta ≡ meta - where - meta = id-meta n e record {top = just (cons x (just s))} - -push-pop : (n e x : ℕ) -> (s : Element ℕ) -> push-pop-type n e x s -push-pop n e x s = refl
--- a/paper/src/AgdaRecord.agda Sat Jan 06 19:04:39 2018 +0900 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,7 +0,0 @@ -record Point : Set where - field - x : Nat - y : Nat - -makePoint : Nat -> Nat -> Point -makePoint a b = record { x = a ; y = b }
--- a/paper/src/AgdaRecordProj.agda Sat Jan 06 19:04:39 2018 +0900 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,8 +0,0 @@ -getX : Point -> Nat -getX p = Point.x p - -getY : Point -> Nat -getY record { x = a ; y = b} = b - -xPlus5 : Point -> Point -xPlus5 p = record p { x = (Point.x p) + 5}
--- a/paper/src/AgdaStack.agda Sat Jan 06 19:04:39 2018 +0900 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,13 +0,0 @@ -data Element (a : Set) : Set where - cons : a -> Maybe (Element a) -> Element a - -datum : {a : Set} -> Element a -> a -datum (cons a _) = a - -next : {a : Set} -> Element a -> Maybe (Element a) -next (cons _ n) = n - -record SingleLinkedStack (a : Set) : Set where - field - top : Maybe (Element a) -
--- a/paper/src/AgdaStackDS.agda Sat Jan 06 19:04:39 2018 +0900 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,17 +0,0 @@ -record Context : Set where - field - -- fields for stack - element : Maybe A - - -open import subtype Context as N - -record Meta : Set₁ where - field - -- context as set of data segments - context : Context - stack : SingleLinkedStack A - nextCS : N.CodeSegment Context Context - -open import subtype Meta as M -
--- a/paper/src/AgdaTypeClass.agda Sat Jan 06 19:04:39 2018 +0900 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,3 +0,0 @@ -record Eq (A : Set) : Set where - field - _==_ : A -> A -> Bool
--- a/paper/src/AgdaWhere.agda Sat Jan 06 19:04:39 2018 +0900 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,7 +0,0 @@ -f : Int -> Int -> Int -f a b c = (t a) + (t b) + (t c) - where - t x = x + x + x - -f' : Int -> Int -> Int -f' a b c = (a + a + a) + (b + b + b) + (c + c + c)
--- a/paper/src/CodeSegment.agda Sat Jan 06 19:04:39 2018 +0900 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,2 +0,0 @@ -data CodeSegment {l1 l2 : Level} (I : Set l1) (O : Set l2) : Set (l ⊔ l1 ⊔ l2) where - cs : (I -> O) -> CodeSegment I O
--- a/paper/src/CodeSegments.agda Sat Jan 06 19:04:39 2018 +0900 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,12 +0,0 @@ -cs2 : CodeSegment ds1 ds1 -cs2 = cs id - -cs1 : CodeSegment ds1 ds1 -cs1 = cs (\d -> goto cs2 d) - -cs0 : CodeSegment ds0 ds1 -cs0 = cs (\d -> goto cs1 (record {c = (ds0.a d) + (ds0.b d)})) - -main : ds1 -main = goto cs0 (record {a = 100 ; b = 50}) -
--- a/paper/src/DataSegment.agda Sat Jan 06 19:04:39 2018 +0900 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,8 +0,0 @@ -record ds0 : Set where - field - a : Int - b : Int - -record ds1 : Set where - field - c : Int
--- a/paper/src/Eq.Agda Sat Jan 06 19:04:39 2018 +0900 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,30 +0,0 @@ -module Eq where -open import Data.Nat -open import Data.Bool -open import Data.List - -record Eq (A : Set) : Set where - field - _==_ : A -> A -> Bool - -_==Nat_ : ℕ -> ℕ -> Bool -zero ==Nat zero = true -(suc n) ==Nat zero = false -zero ==Nat (suc m) = false -(suc n) ==Nat (suc m) = n ==Nat m - - -instance - _ : Eq ℕ - _ = record { _==_ = _==Nat_} - -_||_ : Bool -> Bool -> Bool -true || _ = true -false || x = x - -elem : {A : Set} {{eqA : Eq A}} → A → List A → Bool -elem {{eqA}} x (y ∷ xs) = (Eq._==_ eqA x y) || (elem {{eqA}} x xs) -elem x [] = false - -listHas4 : Bool -listHas4 = elem 4 (3 ∷ 2 ∷ 5 ∷ 4 ∷ []) -- true
--- a/paper/src/Equiv.agda Sat Jan 06 19:04:39 2018 +0900 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,1 +0,0 @@ -data _≡_ {a} {A : Set a} (x : A) : A → Set a where refl : x ≡ x \ No newline at end of file
--- a/paper/src/Exec.agda Sat Jan 06 19:04:39 2018 +0900 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,5 +0,0 @@ -exec : {l1 l2 : Level} {I : Set l1} {O : Set l2} - {{_ : DataSegment I}} {{_ : DataSegment O}} - -> CodeSegment I O -> Context -> Context -exec {l} {{i}} {{o}} (cs b) c = set o c (b (get i c)) -
--- a/paper/src/Goto.agda Sat Jan 06 19:04:39 2018 +0900 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,4 +0,0 @@ -goto : {l1 l2 : Level} {I : Set l1} {O : Set l2} - -> CodeSegment I O -> I -> O -goto (cs b) i = b i -
--- a/paper/src/Maybe.agda Sat Jan 06 19:04:39 2018 +0900 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,3 +0,0 @@ -data Maybe {a} (A : Set a) : Set a where - just : (x : A) -> Maybe A - nothing : Maybe A
--- a/paper/src/MetaCodeSegment.agda Sat Jan 06 19:04:39 2018 +0900 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,4 +0,0 @@ -data CodeSegment {l1 l2 : Level} (A : Set l1) (B : Set l2) : Set (l ⊔ l1 ⊔ l2) where - cs : {{_ : DataSegment A}} {{_ : DataSegment B}} - -> (A -> B) -> CodeSegment A B -
--- a/paper/src/MetaDataSegment.agda Sat Jan 06 19:04:39 2018 +0900 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,7 +0,0 @@ -module subtype {l : Level} (Context : Set l) where - -record DataSegment {ll : Level} (A : Set ll) : Set (l ⊔ ll) where - field - get : Context -> A - set : Context -> A -> Context -
--- a/paper/src/MetaMetaCodeSegment.agda Sat Jan 06 19:04:39 2018 +0900 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,29 +0,0 @@ --- meta level -liftContext : {X Y : Set} {{_ : N.DataSegment X}} {{_ : N.DataSegment Y}} -> N.CodeSegment X Y -> N.CodeSegment Context Context -liftContext {{x}} {{y}} (N.cs f) = N.cs (\c -> N.DataSegment.set y c (f (N.DataSegment.get x c))) - -liftMeta : {X Y : Set} {{_ : M.DataSegment X}} {{_ : M.DataSegment Y}} -> N.CodeSegment X Y -> M.CodeSegment X Y -liftMeta (N.cs f) = M.cs f - -gotoMeta : {I O : Set} {{_ : N.DataSegment I}} {{_ : N.DataSegment O}} -> M.CodeSegment Meta Meta -> N.CodeSegment I O -> Meta -> Meta -gotoMeta mCode code m = M.exec mCode (record m {next = (liftContext code)}) - -push : M.CodeSegment Meta Meta -push = M.cs (\m -> M.exec (liftMeta (Meta.next m)) (record m {c' = Context.c (Meta.context m)})) - --- normal level - -cs2 : N.CodeSegment ds1 ds1 -cs2 = N.cs id - -cs1 : N.CodeSegment ds1 ds1 -cs1 = N.cs (\d -> N.goto cs2 d) - -cs0 : N.CodeSegment ds0 ds1 -cs0 = N.cs (\d -> N.goto cs1 (record {c = (ds0.a d) + (ds0.b d)})) - --- meta level (with extended normal) -main : Meta -main = gotoMeta push cs0 (record {context = (record {a = 100 ; b = 50 ; c = 70}) ; c' = 0 ; next = (N.cs id)}) --- record {context = record {a = 100 ; b = 50 ; c = 150} ; c' = 70 ; next = (N.cs id)} -
--- a/paper/src/MetaMetaDataSegment.agda Sat Jan 06 19:04:39 2018 +0900 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,12 +0,0 @@ --- 上で各 DataSegement の定義を行なっているとする -open import subtype Context as N -- Meta Datasegment を定義 - --- Meta DataSegment を持つ Meta Meta DataSegment を定義できる -record Meta : Set where - field - context : Context - c' : Int - next : N.CodeSegment Context Context - -open import subtype Meta as M --- 以下よりメタメタレベルのプログラムを記述できる
--- a/paper/src/Nat.agda Sat Jan 06 19:04:39 2018 +0900 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,5 +0,0 @@ -module nat where - -data Nat : Set where - O : Nat - S : Nat -> Nat \ No newline at end of file
--- a/paper/src/NatAdd.agda Sat Jan 06 19:04:39 2018 +0900 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,6 +0,0 @@ -open import nat -module nat_add where - -_+_ : Nat -> Nat -> Nat -O + m = m -(S n) + m = S (n + m) \ No newline at end of file
--- a/paper/src/NatAddSym.agda Sat Jan 06 19:04:39 2018 +0900 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,12 +0,0 @@ -open import Relation.Binary.PropositionalEquality -open import nat -open import nat_add -open ≡-Reasoning - -module nat_add_sym where - -addSym : (n m : Nat) -> n + m ≡ m + n -addSym O O = refl -addSym O (S m) = cong S (addSym O m) -addSym (S n) O = cong S (addSym n O) -addSym (S n) (S m) = {!!} -- 後述
--- a/paper/src/PushPopType.agda Sat Jan 06 19:04:39 2018 +0900 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,9 +0,0 @@ -pushOnce : Meta -> Meta -pushOnce m = M.exec pushSingleLinkedStackCS m - -popOnce : Meta -> Meta -popOnce m = M.exec popSingleLinkedStackCS m - -push-pop-type : Meta -> Set₁ -push-pop-type meta = - M.exec (M.csComp (M.cs popOnce) (M.cs pushOnce)) meta ≡ meta
--- a/paper/src/Reasoning.agda Sat Jan 06 19:04:39 2018 +0900 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,21 +0,0 @@ -open import Relation.Binary.PropositionalEquality -open import nat -open import nat_add -open ≡-Reasoning - -module nat_add_sym_reasoning where - -addToRight : (n m : Nat) -> S (n + m) ≡ n + (S m) -addToRight O m = refl -addToRight (S n) m = cong S (addToRight n m) - -addSym : (n m : Nat) -> n + m ≡ m + n -addSym O O = refl -addSym O (S m) = cong S (addSym O m) -addSym (S n) O = cong S (addSym n O) -addSym (S n) (S m) = begin - (S n) + (S m) ≡⟨ refl ⟩ - S (n + S m) ≡⟨ cong S (addSym n (S m)) ⟩ - S ((S m) + n) ≡⟨ addToRight (S m) n ⟩ - S (m + S n) ≡⟨ refl ⟩ - (S m) + (S n) ∎
--- a/paper/src/SingleLinkedStack.cbc Sat Jan 06 19:04:39 2018 +0900 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,110 +0,0 @@ -#include "../context.h" -#include "../origin_cs.h" -#include <stdio.h> - -// typedef struct SingleLinkedStack { -// struct Element* top; -// } SingleLinkedStack; - -Stack* createSingleLinkedStack(struct Context* context) { - struct Stack* stack = new Stack(); - struct SingleLinkedStack* singleLinkedStack = new SingleLinkedStack(); - stack->stack = (union Data*)singleLinkedStack; - singleLinkedStack->top = NULL; - stack->push = C_pushSingleLinkedStack; - stack->pop = C_popSingleLinkedStack; - stack->pop2 = C_pop2SingleLinkedStack; - stack->get = C_getSingleLinkedStack; - stack->get2 = C_get2SingleLinkedStack; - stack->isEmpty = C_isEmptySingleLinkedStack; - stack->clear = C_clearSingleLinkedStack; - return stack; -} - -void printStack1(union Data* data) { - struct Node* node = &data->Element.data->Node; - if (node == NULL) { - printf("NULL"); - } else { - printf("key = %d ,", node->key); - printStack1((union Data*)data->Element.next); - } -} - -void printStack(union Data* data) { - printStack1(data); - printf("\n"); -} - -__code clearSingleLinkedStack(struct SingleLinkedStack* stack,__code next(...)) { - stack->top = NULL; - goto next(...); -} - -__code pushSingleLinkedStack(struct SingleLinkedStack* stack,union Data* data, __code next(...)) { - Element* element = new Element(); - element->next = stack->top; - element->data = data; - stack->top = element; - goto next(...); -} - -__code popSingleLinkedStack(struct SingleLinkedStack* stack, __code next(union Data* data, ...)) { - if (stack->top) { - data = stack->top->data; - stack->top = stack->top->next; - } else { - data = NULL; - } - goto next(data, ...); -} - -__code pop2SingleLinkedStack(struct SingleLinkedStack* stack, __code next(union Data* data, union Data* data1, ...)) { - if (stack->top) { - data = stack->top->data; - stack->top = stack->top->next; - } else { - data = NULL; - } - if (stack->top) { - data1 = stack->top->data; - stack->top = stack->top->next; - } else { - data1 = NULL; - } - goto next(data, data1, ...); -} - - -__code getSingleLinkedStack(struct SingleLinkedStack* stack, __code next(union Data* data, ...)) { - if (stack->top) - data = stack->top->data; - else - data = NULL; - goto next(data, ...); -} - -__code get2SingleLinkedStack(struct SingleLinkedStack* stack, __code next(union Data* data, union Data* data1, ...)) { - if (stack->top) { - data = stack->top->data; - if (stack->top->next) { - data1 = stack->top->next->data; - } else { - data1 = NULL; - } - } else { - data = NULL; - data1 = NULL; - } - goto next(data, data1, ...); -} - -__code isEmptySingleLinkedStack(struct SingleLinkedStack* stack, __code next(...), __code whenEmpty(...)) { - if (stack->top) - goto next(...); - else - goto whenEmpty(...); -} - - -
--- a/paper/src/ThreePlusOne.agda Sat Jan 06 19:04:39 2018 +0900 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,8 +0,0 @@ -open import Relation.Binary.PropositionalEquality -open import nat -open import nat_add - -module three_plus_one where - -3+1 : (S (S (S O))) + (S O) ≡ (S (S (S (S O)))) -3+1 = refl \ No newline at end of file
--- a/paper/src/akashaContext.h Sat Jan 06 19:04:39 2018 +0900 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,31 +0,0 @@ -// Data Segment -union Data { - struct Tree { /* ... 赤黒木の定義と同様 */ } tree; - struct Node { /* ... 赤黒木の定義と同様 */ } node; - - /* for verification */ - struct IterElem { - unsigned int val; - struct IterElem* next; - } iterElem; - struct Iterator { - struct Tree* tree; - struct Iterator* previousDepth; - struct IterElem* head; - struct IterElem* last; - unsigned int iteratedValue; - unsigned long iteratedPointDataNum; - void* iteratedPointHeap; - } iterator; - struct AkashaInfo { - unsigned int minHeight; - unsigned int maxHeight; - struct AkashaNode* akashaNode; - } akashaInfo; - struct AkashaNode { - unsigned int height; - struct Node* node; - struct AkashaNode* nextAkashaNode; - } akashaNode; -}; -
--- a/paper/src/akashaMeta.c Sat Jan 06 19:04:39 2018 +0900 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,31 +0,0 @@ -__code meta(struct Context* context, enum Code next) { - struct Iterator* iter = &context->data[Iter]->iterator; - - switch (context->prev) { - case GoToPreviousDepth: - if (iter->iteratedPointDataNum == 0) break; - if (iter->iteratedPointHeap == NULL) break; - - unsigned int diff =(unsigned long)context->heap - (unsigned long)iter->iteratedPointHeap; - memset(iter->iteratedPointHeap, 0, diff); - context->dataNum = iter->iteratedPointDataNum; - context->heap = iter->iteratedPointHeap; - break; - default: - break; - } - switch (next) { - case PutAndGoToNextDepth: // with assert check - if (context->prev == GoToPreviousDepth) break; - if (iter->previousDepth == NULL) break; - iter->previousDepth->iteratedPointDataNum = context->dataNum; - iter->previousDepth->iteratedPointHeap = context->heap; - break; - default: - break; - } - - context->prev = next; - goto (context->code[next])(context); -} -
--- a/paper/src/assert.c Sat Jan 06 19:04:39 2018 +0900 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,7 +0,0 @@ -__code verifySpecificationFinish(struct Context* context) { - if (context->data[AkashaInfo]->akashaInfo.maxHeight > 2*context->data[AkashaInfo]->akashaInfo.minHeight) { - context->next = Exit; - goto meta(context, ShowTrace); - } - goto meta(context, DuplicateIterator); -}
--- a/paper/src/atton-master-meta-sample.agda Sat Jan 06 19:04:39 2018 +0900 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,77 +0,0 @@ -module atton-master-meta-sample where - -open import Data.Nat -open import Data.Unit -open import Function -Int = ℕ - -record Context : Set where - field - a : Int - b : Int - c : Int - -open import subtype Context as N - -record Meta : Set where - field - context : Context - c' : Int - next : N.CodeSegment Context Context - -open import subtype Meta as M - -instance - _ : N.DataSegment Context - _ = record { get = id ; set = (\_ c -> c) } - _ : M.DataSegment Context - _ = record { get = (\m -> Meta.context m) ; - set = (\m c -> record m {context = c}) } - _ : M.DataSegment Meta - _ = record { get = id ; set = (\_ m -> m) } - - -liftContext : {X Y : Set} {{_ : N.DataSegment X}} {{_ : N.DataSegment Y}} -> N.CodeSegment X Y -> N.CodeSegment Context Context -liftContext {{x}} {{y}} (N.cs f) = N.cs (\c -> N.DataSegment.set y c (f (N.DataSegment.get x c))) - -liftMeta : {X Y : Set} {{_ : M.DataSegment X}} {{_ : M.DataSegment Y}} -> N.CodeSegment X Y -> M.CodeSegment X Y -liftMeta (N.cs f) = M.cs f - - -gotoMeta : {I O : Set} {{_ : N.DataSegment I}} {{_ : N.DataSegment O}} -> M.CodeSegment Meta Meta -> N.CodeSegment I O -> Meta -> Meta -gotoMeta mCode code m = M.exec mCode (record m {next = (liftContext code)}) - -push : M.CodeSegment Meta Meta -push = M.cs (\m -> M.exec (liftMeta (Meta.next m)) (record m {c' = Context.c (Meta.context m)})) - - -record ds0 : Set where - field - a : Int - b : Int - -record ds1 : Set where - field - c : Int - -instance - _ : N.DataSegment ds0 - _ = record { set = (\c d -> record c {a = (ds0.a d) ; b = (ds0.b d)}) - ; get = (\c -> record { a = (Context.a c) ; b = (Context.b c)})} - _ : N.DataSegment ds1 - _ = record { set = (\c d -> record c {c = (ds1.c d)}) - ; get = (\c -> record { c = (Context.c c)})} - -cs2 : N.CodeSegment ds1 ds1 -cs2 = N.cs id - -cs1 : N.CodeSegment ds1 ds1 -cs1 = N.cs (\d -> N.goto cs2 d) - -cs0 : N.CodeSegment ds0 ds1 -cs0 = N.cs (\d -> N.goto cs1 (record {c = (ds0.a d) + (ds0.b d)})) - - -main : Meta -main = gotoMeta push cs0 (record {context = (record {a = 100 ; b = 50 ; c = 70}) ; c' = 0 ; next = (N.cs id)}) --- record {context = record {a = 100 ; b = 50 ; c = 150} ; c' = 70 ; next = (N.cs id)}
--- a/paper/src/atton-master-sample.agda Sat Jan 06 19:04:39 2018 +0900 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,46 +0,0 @@ -module atton-master-sample where - -open import Data.Nat -open import Data.Unit -open import Function -Int = ℕ - -record Context : Set where - field - a : Int - b : Int - c : Int - - -open import subtype Context - - - -record ds0 : Set where - field - a : Int - b : Int - -record ds1 : Set where - field - c : Int - -instance - _ : DataSegment ds0 - _ = record { set = (\c d -> record c {a = (ds0.a d) ; b = (ds0.b d)}) - ; get = (\c -> record { a = (Context.a c) ; b = (Context.b c)})} - _ : DataSegment ds1 - _ = record { set = (\c d -> record c {c = (ds1.c d)}) - ; get = (\c -> record { c = (Context.c c)})} - -cs2 : CodeSegment ds1 ds1 -cs2 = cs id - -cs1 : CodeSegment ds1 ds1 -cs1 = cs (\d -> goto cs2 d) - -cs0 : CodeSegment ds0 ds1 -cs0 = cs (\d -> goto cs1 (record {c = (ds0.a d) + (ds0.b d)})) - -main : ds1 -main = goto cs0 (record {a = 100 ; b = 50})
--- a/paper/src/cbmc-assert.c Sat Jan 06 19:04:39 2018 +0900 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,7 +0,0 @@ -void verifySpecification(struct Context* context, - struct Tree* tree) { - assert(!(maxHeight(tree->root, 1) > - 2*minHeight(tree->root, 1))); - return meta(context, EnumerateInputs); -} -
--- a/paper/src/context.h Sat Jan 06 19:04:39 2018 +0900 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,47 +0,0 @@ -/* Context definition */ - -#define ALLOCATE_SIZE 1024 - -enum Code { - Code1, - Code2, - Allocator, -}; - -enum UniqueData { - Allocate, - Tree, -}; - -struct Context { - int codeNum; - __code (**code) (struct Context *); - void* heap_start; - void* heap; - long dataSize; - int dataNum; - union Data **data; -}; - -union Data { - struct Tree { - union Data* root; - union Data* current; - union Data* prev; - int result; - } tree; - struct Node { - int key; - int value; - enum Color { - Red, - Black, - } color; - union Data* left; - union Data* right; - } node; - struct Allocate { - long size; - enum Code next; - } allocate; -};
--- a/paper/src/enumerate-inputs.c Sat Jan 06 19:04:39 2018 +0900 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,13 +0,0 @@ -void enumerateInputs(struct Context* context, - struct Node* node) { - if (context->loopCount > LIMIT_OF_VERIFICATION_SIZE) { - return meta(context, Exit); - } - - node->key = nondet_int(); - node->value = node->key; - context->next = VerifySpecification; - context->loopCount++; - - return meta(context, Put); -}
--- a/paper/src/expr-term.txt Sat Jan 06 19:04:39 2018 +0900 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,8 +0,0 @@ -t ::= - true - false - if t then t else t - 0 - succ t - pred t - iszero t
--- a/paper/src/factrial.cbc Sat Jan 06 19:04:39 2018 +0900 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,29 +0,0 @@ -__code print_factorial(int prod) -{ - printf("factorial = %d\n", prod); - exit(0); -} - -__code factorial0(int prod, int x) -{ - if (x >= 1) { - goto factorial0(prod*x, x-1); - } else { - goto print_factorial(prod); - } - -} - -__code factorial(int x) -{ - goto factorial0(1, x); -} - -int main(int argc, char **argv) -{ - int i; - i = atoi(argv[1]); - - goto factorial(i); -} -
--- a/paper/src/getMinHeight.c Sat Jan 06 19:04:39 2018 +0900 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,51 +0,0 @@ -__code getMinHeight_stub(struct Context* context) { - goto getMinHeight(context, &context->data[Allocate]->allocate, &context->data[AkashaInfo]->akashaInfo); -} - -__code getMinHeight(struct Context* context, struct Allocate* allocate, struct AkashaInfo* akashaInfo) { - const struct AkashaNode* akashaNode = akashaInfo->akashaNode; - - if (akashaNode == NULL) { - allocate->size = sizeof(struct AkashaNode); - allocator(context); - akashaInfo->akashaNode = (struct AkashaNode*)context->data[context->dataNum]; - - akashaInfo->akashaNode->height = 1; - akashaInfo->akashaNode->node = context->data[Tree]->tree.root; - - goto getMaxHeight_stub(context); - } - - const struct Node* node = akashaInfo->akashaNode->node; - if (node->left == NULL && node->right == NULL) { - if (akashaInfo->minHeight > akashaNode->height) { - akashaInfo->minHeight = akashaNode->height; - akashaInfo->akashaNode = akashaNode->nextAkashaNode; - goto getMinHeight_stub(context); - } - } - - akashaInfo->akashaNode = akashaInfo->akashaNode->nextAkashaNode; - - if (node->left != NULL) { - allocate->size = sizeof(struct AkashaNode); - allocator(context); - struct AkashaNode* left = (struct AkashaNode*)context->data[context->dataNum]; - left->height = akashaNode->height+1; - left->node = node->left; - left->nextAkashaNode = akashaInfo->akashaNode; - akashaInfo->akashaNode = left; - } - - if (node->right != NULL) { - allocate->size = sizeof(struct AkashaNode); - allocator(context); - struct AkashaNode* right = (struct AkashaNode*)context->data[context->dataNum]; - right->height = akashaNode->height+1; - right->node = node->right; - right->nextAkashaNode = akashaInfo->akashaNode; - akashaInfo->akashaNode = right; - } - - goto getMinHeight_stub(context); -}
--- a/paper/src/goto.cbc Sat Jan 06 19:04:39 2018 +0900 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,7 +0,0 @@ -__code cs0(int a, int b){ - goto cs1(a+b); -} - -__code cs1(int c){ - goto cs2(c); -}
--- a/paper/src/initLLRBContext.c Sat Jan 06 19:04:39 2018 +0900 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,53 +0,0 @@ -__code initLLRBContext(struct Context* context, int num) { - context->heapLimit = sizeof(union Data)*ALLOCATE_SIZE; - context->code = malloc(sizeof(__code*)*ALLOCATE_SIZE); - context->data = malloc(sizeof(union Data*)*ALLOCATE_SIZE); - context->heapStart = malloc(context->heapLimit); - - context->codeNum = Exit; - - context->code[Code1] = code1_stub; - context->code[Code2] = code2_stub; - context->code[Code3] = code3_stub; - context->code[Code4] = code4; - context->code[Code5] = code5; - context->code[Find] = find; - context->code[Not_find] = not_find; - context->code[Code6] = code6; - context->code[Put] = put_stub; - context->code[Replace] = replaceNode_stub; - context->code[Insert] = insertNode_stub; - context->code[RotateL] = rotateLeft_stub; - context->code[RotateR] = rotateRight_stub; - context->code[InsertCase1] = insert1_stub; - context->code[InsertCase2] = insert2_stub; - context->code[InsertCase3] = insert3_stub; - context->code[InsertCase4] = insert4_stub; - context->code[InsertCase4_1] = insert4_1_stub; - context->code[InsertCase4_2] = insert4_2_stub; - context->code[InsertCase5] = insert5_stub; - context->code[StackClear] = stackClear_stub; - context->code[Exit] = exit_code; - - context->heap = context->heapStart; - - context->data[Allocate] = context->heap; - context->heap += sizeof(struct Allocate); - - context->data[Tree] = context->heap; - context->heap += sizeof(struct Tree); - - context->data[Node] = context->heap; - context->heap += sizeof(struct Node); - - context->dataNum = Node; - - struct Tree* tree = &context->data[Tree]->tree; - tree->root = 0; - tree->current = 0; - tree->deleted = 0; - - context->node_stack = stack_init(sizeof(struct Node*), 100); - context->code_stack = stack_init(sizeof(enum Code), 100); -} -
--- a/paper/src/insertCase2.c Sat Jan 06 19:04:39 2018 +0900 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,17 +0,0 @@ -__code insertCase2(struct Context* context, struct Node* current) { - struct Node* parent; - stack_pop(context->node_stack, &parent); - - if (parent->color == Black) { - stack_pop(context->code_stack, &context->next); - goto meta(context, context->next); - } - - stack_push(context->node_stack, &parent); - goto meta(context, InsertCase3); -} - -__code insert2_stub(struct Context* context) { - goto insertCase2(context, context->data[Tree]->tree.current); -} -
--- a/paper/src/meta.c Sat Jan 06 19:04:39 2018 +0900 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,4 +0,0 @@ -__code meta(struct Context* context, enum Code next) { - goto (context->code[next])(context); -} -
--- a/paper/src/rbtreeContext.h Sat Jan 06 19:04:39 2018 +0900 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,50 +0,0 @@ -// DataSegments for Red-Black Tree -union Data { - struct Comparable { // interface - enum Code compare; - union Data* data; - } compare; - struct Count { - enum Code next; - long i; - } count; - struct Tree { - enum Code next; - struct Node* root; - struct Node* current; - struct Node* deleted; - int result; - } tree; - struct Node { - // need to tree - enum Code next; - int key; // comparable data segment - int value; - struct Node* left; - struct Node* right; - // need to balancing - enum Color { - Red, - Black, - } color; - } node; - struct Allocate { - enum Code next; - long size; - } allocate; -}; - - -// Meta DataSegment -struct Context { - enum Code next; - int codeNum; - __code (**code) (struct Context*); - void* heapStart; - void* heap; - long heapLimit; - int dataNum; - stack_ptr code_stack; - stack_ptr node_stack; - union Data **data; -};
--- a/paper/src/singleLinkedStack.c Sat Jan 06 19:04:39 2018 +0900 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,18 +0,0 @@ -__code pushSingleLinkedStack(struct SingleLinkedStack* stack,union Data* data, __code next(...)) { - Element* element = new Element(); - element->next = stack->top; - element->data = data; - stack->top = element; - goto next(...); -} - -__code popSingleLinkedStack(struct SingleLinkedStack* stack, __code next(union Data* data, ...)) { - if (stack->top) { - data = stack->top->data; - stack->top = stack->top->next; - } else { - data = NULL; - } - goto next(data, ...); -} -
--- a/paper/src/stack-product.agda Sat Jan 06 19:04:39 2018 +0900 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,158 +0,0 @@ -module stack-product where - -open import product -open import Data.Product -open import Data.Nat -open import Function using (id) -open import Relation.Binary.PropositionalEquality - --- definition based from Gears(209:5708390a9d88) src/parallel_execution -goto = executeCS - -data Bool : Set where - True : Bool - False : Bool - -data Maybe (a : Set) : Set where - Nothing : Maybe a - Just : a -> Maybe a - - -record Stack {a t : Set} (stackImpl : Set) : Set where - field - stack : stackImpl - push : CodeSegment (stackImpl × a × (CodeSegment stackImpl t)) t - pop : CodeSegment (stackImpl × (CodeSegment (stackImpl × Maybe a) t)) t - - -data Element (a : Set) : Set where - cons : a -> Maybe (Element a) -> Element a - -datum : {a : Set} -> Element a -> a -datum (cons a _) = a - -next : {a : Set} -> Element a -> Maybe (Element a) -next (cons _ n) = n - -record SingleLinkedStack (a : Set) : Set where - field - top : Maybe (Element a) -open SingleLinkedStack - -emptySingleLinkedStack : {a : Set} -> SingleLinkedStack a -emptySingleLinkedStack = record {top = Nothing} - - - - -pushSingleLinkedStack : {a t : Set} -> CodeSegment ((SingleLinkedStack a) × a × (CodeSegment (SingleLinkedStack a) t)) t -pushSingleLinkedStack = cs push - where - push : {a t : Set} -> ((SingleLinkedStack a) × a × (CodeSegment (SingleLinkedStack a) t)) -> t - push (stack , datum , next) = goto next stack1 - where - element = cons datum (top stack) - stack1 = record {top = Just element} - -popSingleLinkedStack : {a t : Set} -> CodeSegment (SingleLinkedStack a × (CodeSegment (SingleLinkedStack a × Maybe a) t)) t -popSingleLinkedStack = cs pop - where - pop : {a t : Set} -> (SingleLinkedStack a × (CodeSegment (SingleLinkedStack a × Maybe a) t)) -> t - pop (record { top = Nothing } , nextCS) = goto nextCS (emptySingleLinkedStack , Nothing) - pop (record { top = Just x } , nextCS) = goto nextCS (stack1 , (Just datum1)) - where - datum1 = datum x - stack1 = record { top = (next x) } - - - - - -createSingleLinkedStack : {a b : Set} -> Stack {a} {b} (SingleLinkedStack a) -createSingleLinkedStack = record { stack = emptySingleLinkedStack - ; push = pushSingleLinkedStack - ; pop = popSingleLinkedStack - } - - - - -test01 : {a : Set} -> CodeSegment (SingleLinkedStack a × Maybe a) Bool -test01 = cs test01' - where - test01' : {a : Set} -> (SingleLinkedStack a × Maybe a) -> Bool - test01' (record { top = Nothing } , _) = False - test01' (record { top = Just x } , _) = True - - -test02 : {a : Set} -> CodeSegment (SingleLinkedStack a) (SingleLinkedStack a × Maybe a) -test02 = cs test02' - where - test02' : {a : Set} -> SingleLinkedStack a -> (SingleLinkedStack a × Maybe a) - test02' stack = goto popSingleLinkedStack (stack , (cs id)) - - -test03 : {a : Set} -> CodeSegment a (SingleLinkedStack a) -test03 = cs test03' - where - test03' : {a : Set} -> a -> SingleLinkedStack a - test03' a = goto pushSingleLinkedStack (emptySingleLinkedStack , a , (cs id)) - - -lemma : {A : Set} {a : A} -> goto (test03 ◎ test02 ◎ test01) a ≡ False -lemma = refl - - -n-push : {A : Set} {a : A} -> CodeSegment (ℕ × SingleLinkedStack A) (ℕ × SingleLinkedStack A) -n-push {A} {a} = cs (push {A} {a}) - where - push : {A : Set} {a : A} -> (ℕ × SingleLinkedStack A) -> (ℕ × SingleLinkedStack A) - push {A} {a} (zero , s) = (zero , s) - push {A} {a} (suc n , s) = goto pushSingleLinkedStack (s , a , {!!} {- n-push -}) -- needs subtype - - -{- - -n-push : {A : Set} {a : A} -> Nat -> SingleLinkedStack A -> SingleLinkedStack A -n-push zero s = s -n-push {A} {a} (suc n) s = pushSingleLinkedStack (n-push {A} {a} n s) a (\s -> s) - -n-pop : {A : Set} {a : A} -> Nat -> SingleLinkedStack A -> SingleLinkedStack A -n-pop zero s = s -n-pop {A} {a} (suc n) s = popSingleLinkedStack (n-pop {A} {a} n s) (\s _ -> s) - -open ≡-Reasoning - -push-pop-equiv : {A : Set} {a : A} (s : SingleLinkedStack A) -> popSingleLinkedStack (pushSingleLinkedStack s a (\s -> s)) (\s _ -> s) ≡ s -push-pop-equiv s = refl - -push-and-n-pop : {A : Set} {a : A} (n : Nat) (s : SingleLinkedStack A) -> n-pop {A} {a} (suc n) (pushSingleLinkedStack s a id) ≡ n-pop {A} {a} n s -push-and-n-pop zero s = refl -push-and-n-pop {A} {a} (suc n) s = begin - n-pop (suc (suc n)) (pushSingleLinkedStack s a id) - ≡⟨ refl ⟩ - popSingleLinkedStack (n-pop (suc n) (pushSingleLinkedStack s a id)) (\s _ -> s) - ≡⟨ cong (\s -> popSingleLinkedStack s (\s _ -> s)) (push-and-n-pop n s) ⟩ - popSingleLinkedStack (n-pop n s) (\s _ -> s) - ≡⟨ refl ⟩ - n-pop (suc n) s - ∎ - - -n-push-pop-equiv : {A : Set} {a : A} (n : Nat) (s : SingleLinkedStack A) -> (n-pop {A} {a} n (n-push {A} {a} n s)) ≡ s -n-push-pop-equiv zero s = refl -n-push-pop-equiv {A} {a} (suc n) s = begin - n-pop (suc n) (n-push (suc n) s) - ≡⟨ refl ⟩ - n-pop (suc n) (pushSingleLinkedStack (n-push n s) a (\s -> s)) - ≡⟨ push-and-n-pop n (n-push n s) ⟩ - n-pop n (n-push n s) - ≡⟨ n-push-pop-equiv n s ⟩ - s - ∎ - - -n-push-pop-equiv-empty : {A : Set} {a : A} -> (n : Nat) -> n-pop {A} {a} n (n-push {A} {a} n emptySingleLinkedStack) ≡ emptySingleLinkedStack -n-push-pop-equiv-empty n = n-push-pop-equiv n emptySingleLinkedStack --} -
--- a/paper/src/stack-subtype-sample.agda Sat Jan 06 19:04:39 2018 +0900 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,212 +0,0 @@ -module stack-subtype-sample where - -open import Level renaming (suc to S ; zero to O) -open import Function -open import Data.Nat -open import Data.Maybe -open import Relation.Binary.PropositionalEquality - -open import stack-subtype ℕ -open import subtype Context as N -open import subtype Meta as M - - -record Num : Set where - field - num : ℕ - -instance - NumIsNormalDataSegment : N.DataSegment Num - NumIsNormalDataSegment = record { get = (\c -> record { num = Context.n c}) - ; set = (\c n -> record c {n = Num.num n})} - NumIsMetaDataSegment : M.DataSegment Num - NumIsMetaDataSegment = record { get = (\m -> record {num = Context.n (Meta.context m)}) - ; set = (\m n -> record m {context = record (Meta.context m) {n = Num.num n}})} - - -plus3 : Num -> Num -plus3 record { num = n } = record {num = n + 3} - -plus3CS : N.CodeSegment Num Num -plus3CS = N.cs plus3 - - - -plus5AndPushWithPlus3 : {mc : Meta} {{_ : N.DataSegment Num}} - -> M.CodeSegment Num (Meta) -plus5AndPushWithPlus3 {mc} {{nn}} = M.cs (\n -> record {context = con n ; nextCS = (liftContext {{nn}} {{nn}} plus3CS) ; stack = st} ) - where - co = Meta.context mc - con : Num -> Context - con record { num = num } = N.DataSegment.set nn co record {num = num + 5} - st = Meta.stack mc - - - - -push-sample : {{_ : N.DataSegment Num}} {{_ : M.DataSegment Num}} -> Meta -push-sample {{nd}} {{md}} = M.exec {{md}} (plus5AndPushWithPlus3 {mc} {{nd}}) mc - where - con = record { n = 4 ; element = just 0} - code = N.cs (\c -> c) - mc = record {context = con ; stack = emptySingleLinkedStack ; nextCS = code} - - -push-sample-equiv : push-sample ≡ record { nextCS = liftContext plus3CS - ; stack = record { top = nothing} - ; context = record { n = 9} } -push-sample-equiv = refl - - -pushed-sample : {m : Meta} {{_ : N.DataSegment Num}} {{_ : M.DataSegment Num}} -> Meta -pushed-sample {m} {{nd}} {{md}} = M.exec {{md}} (M.csComp {m} {{md}} pushSingleLinkedStackCS (plus5AndPushWithPlus3 {mc} {{nd}})) mc - where - con = record { n = 4 ; element = just 0} - code = N.cs (\c -> c) - mc = record {context = con ; stack = emptySingleLinkedStack ; nextCS = code} - - - -pushed-sample-equiv : {m : Meta} -> - pushed-sample {m} ≡ record { nextCS = liftContext plus3CS - ; stack = record { top = just (cons 0 nothing) } - ; context = record { n = 12} } -pushed-sample-equiv = refl - - - -pushNum : N.CodeSegment Context Context -pushNum = N.cs pn - where - pn : Context -> Context - pn record { n = n } = record { n = pred n ; element = just n} - - -pushOnce : Meta -> Meta -pushOnce m = M.exec pushSingleLinkedStackCS m - -n-push : {m : Meta} {{_ : M.DataSegment Meta}} (n : ℕ) -> M.CodeSegment Meta Meta -n-push {{mm}} (zero) = M.cs {{mm}} {{mm}} id -n-push {m} {{mm}} (suc n) = M.cs {{mm}} {{mm}} (\m -> M.exec {{mm}} {{mm}} (n-push {m} {{mm}} n) (pushOnce m)) - -popOnce : Meta -> Meta -popOnce m = M.exec popSingleLinkedStackCS m - -n-pop : {m : Meta} {{_ : M.DataSegment Meta}} (n : ℕ) -> M.CodeSegment Meta Meta -n-pop {{mm}} (zero) = M.cs {{mm}} {{mm}} id -n-pop {m} {{mm}} (suc n) = M.cs {{mm}} {{mm}} (\m -> M.exec {{mm}} {{mm}} (n-pop {m} {{mm}} n) (popOnce m)) - - - -initMeta : ℕ -> Maybe ℕ -> N.CodeSegment Context Context -> Meta -initMeta n mn code = record { context = record { n = n ; element = mn} - ; stack = emptySingleLinkedStack - ; nextCS = code - } - -n-push-cs-exec = M.exec (n-push {meta} 3) meta - where - meta = (initMeta 5 (just 9) pushNum) - - -n-push-cs-exec-equiv : n-push-cs-exec ≡ record { nextCS = pushNum - ; context = record {n = 2 ; element = just 3} - ; stack = record {top = just (cons 4 (just (cons 5 (just (cons 9 nothing)))))}} -n-push-cs-exec-equiv = refl - - -n-pop-cs-exec = M.exec (n-pop {meta} 4) meta - where - meta = record { nextCS = N.cs id - ; context = record { n = 0 ; element = nothing} - ; stack = record {top = just (cons 9 (just (cons 8 (just (cons 7 (just (cons 6 (just (cons 5 nothing)))))))))} - } - -n-pop-cs-exec-equiv : n-pop-cs-exec ≡ record { nextCS = N.cs id - ; context = record { n = 0 ; element = just 6} - ; stack = record { top = just (cons 5 nothing)} - } - -n-pop-cs-exec-equiv = refl - - -open ≡-Reasoning - -id-meta : ℕ -> ℕ -> SingleLinkedStack ℕ -> Meta -id-meta n e s = record { context = record {n = n ; element = just e} - ; nextCS = (N.cs id) ; stack = s} - -exec-comp : (f g : M.CodeSegment Meta Meta) (m : Meta) -> M.exec (M.csComp {m} f g) m ≡ M.exec f (M.exec g m) -exec-comp (M.cs x) (M.cs _) m = refl - - -push-pop-type : ℕ -> ℕ -> ℕ -> Element ℕ -> Set₁ -push-pop-type n e x s = M.exec (M.csComp {meta} (M.cs popOnce) (M.cs pushOnce)) meta ≡ meta - where - meta = id-meta n e record {top = just (cons x (just s))} - -push-pop : (n e x : ℕ) -> (s : Element ℕ) -> push-pop-type n e x s -push-pop n e x s = refl - - - -pop-n-push-type : ℕ -> ℕ -> ℕ -> SingleLinkedStack ℕ -> Set₁ -pop-n-push-type n cn ce s = M.exec (M.csComp {meta} (M.cs popOnce) (n-push {meta} (suc n))) meta - ≡ M.exec (n-push {meta} n) meta - where - meta = id-meta cn ce s - -pop-n-push : (n cn ce : ℕ) -> (s : SingleLinkedStack ℕ) -> pop-n-push-type n cn ce s - -pop-n-push zero cn ce s = refl -pop-n-push (suc n) cn ce s = begin - M.exec (M.csComp {id-meta cn ce s} (M.cs popOnce) (n-push {id-meta cn ce (record {top = just (cons ce (SingleLinkedStack.top s))})} (suc (suc n)))) (id-meta cn ce s) - ≡⟨ refl ⟩ - M.exec (M.csComp {id-meta cn ce s} (M.cs popOnce) (M.csComp {id-meta cn ce s} (n-push {id-meta cn ce (record {top = just (cons ce (SingleLinkedStack.top s))})} (suc n)) (M.cs pushOnce))) (id-meta cn ce s) - ≡⟨ exec-comp (M.cs popOnce) (M.csComp {id-meta cn ce s} (n-push {id-meta cn ce (record {top = just (cons ce (SingleLinkedStack.top s))})} (suc n)) (M.cs pushOnce)) (id-meta cn ce s) ⟩ - M.exec (M.cs popOnce) (M.exec (M.csComp {id-meta cn ce s} (n-push {id-meta cn ce (record {top = just (cons ce (SingleLinkedStack.top s))})} (suc n)) (M.cs pushOnce)) (id-meta cn ce s)) - ≡⟨ cong (\x -> M.exec (M.cs popOnce) x) (exec-comp (n-push {id-meta cn ce (record {top = just (cons ce (SingleLinkedStack.top s))})} (suc n)) (M.cs pushOnce) (id-meta cn ce s)) ⟩ - M.exec (M.cs popOnce) (M.exec (n-push {id-meta cn ce (record {top = just (cons ce (SingleLinkedStack.top s))})} (suc n))(M.exec (M.cs pushOnce) (id-meta cn ce s))) - ≡⟨ refl ⟩ - M.exec (M.cs popOnce) (M.exec (n-push {id-meta cn ce (record {top = just (cons ce (SingleLinkedStack.top s))})} (suc n)) (id-meta cn ce (record {top = just (cons ce (SingleLinkedStack.top s))}))) - ≡⟨ sym (exec-comp (M.cs popOnce) (n-push {id-meta cn ce (record {top = just (cons ce (SingleLinkedStack.top s))})} (suc n)) (id-meta cn ce (record {top = just (cons ce (SingleLinkedStack.top s))}))) ⟩ - M.exec (M.csComp {id-meta cn ce s} (M.cs popOnce) (n-push {id-meta cn ce (record {top = just (cons ce (SingleLinkedStack.top s))})} (suc n))) (id-meta cn ce (record {top = just (cons ce (SingleLinkedStack.top s))})) - ≡⟨ pop-n-push n cn ce (record {top = just (cons ce (SingleLinkedStack.top s))}) ⟩ - M.exec (n-push n) (id-meta cn ce (record {top = just (cons ce (SingleLinkedStack.top s))})) - ≡⟨ refl ⟩ - M.exec (n-push n) (pushOnce (id-meta cn ce s)) - ≡⟨ refl ⟩ - M.exec (n-push n) (M.exec (M.cs pushOnce) (id-meta cn ce s)) - ≡⟨ refl ⟩ - M.exec (n-push {id-meta cn ce s} (suc n)) (id-meta cn ce s) - ∎ - - - -n-push-pop-type : ℕ -> ℕ -> ℕ -> SingleLinkedStack ℕ -> Set₁ -n-push-pop-type n cn ce st = M.exec (M.csComp {meta} (n-pop {meta} n) (n-push {meta} n)) meta ≡ meta - where - meta = id-meta cn ce st - -n-push-pop : (n cn ce : ℕ) -> (s : SingleLinkedStack ℕ) -> n-push-pop-type n cn ce s -n-push-pop zero cn ce s = refl -n-push-pop (suc n) cn ce s = begin - M.exec (M.csComp {id-meta cn ce s} (n-pop {id-meta cn ce s} (suc n)) (n-push {id-meta cn ce s} (suc n))) (id-meta cn ce s) - ≡⟨ refl ⟩ - M.exec (M.csComp {id-meta cn ce s} (M.cs (\m -> M.exec (n-pop {id-meta cn ce s} n) (popOnce m))) (n-push {id-meta cn ce s} (suc n))) (id-meta cn ce s) - ≡⟨ exec-comp (M.cs (\m -> M.exec (n-pop n) (popOnce m))) (n-push {id-meta cn ce s} (suc n)) (id-meta cn ce s) ⟩ - M.exec (M.cs (\m -> M.exec (n-pop {id-meta cn ce s} n) (popOnce m))) (M.exec (n-push {id-meta cn ce s} (suc n)) (id-meta cn ce s)) - ≡⟨ refl ⟩ - M.exec (n-pop n) (popOnce (M.exec (n-push {id-meta cn ce s} (suc n)) (id-meta cn ce s))) - ≡⟨ refl ⟩ - M.exec (n-pop n) (M.exec (M.cs popOnce) (M.exec (n-push {id-meta cn ce s} (suc n)) (id-meta cn ce s))) - ≡⟨ cong (\x -> M.exec (n-pop {id-meta cn ce s} n) x) (sym (exec-comp (M.cs popOnce) (n-push {id-meta cn ce s} (suc n)) (id-meta cn ce s))) ⟩ - M.exec (n-pop n) (M.exec (M.csComp {id-meta cn ce s} (M.cs popOnce) (n-push {id-meta cn ce s} (suc n))) (id-meta cn ce s)) - ≡⟨ cong (\x -> M.exec (n-pop {id-meta cn ce s} n) x) (pop-n-push n cn ce s) ⟩ - M.exec (n-pop n) (M.exec (n-push n) (id-meta cn ce s)) - ≡⟨ sym (exec-comp (n-pop n) (n-push n) (id-meta cn ce s)) ⟩ - M.exec (M.csComp (n-pop n) (n-push n)) (id-meta cn ce s) - ≡⟨ n-push-pop n cn ce s ⟩ - id-meta cn ce s - ∎ -
--- a/paper/src/stack-subtype.agda Sat Jan 06 19:04:39 2018 +0900 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,123 +0,0 @@ -open import Level hiding (lift) -open import Data.Maybe -open import Data.Product -open import Data.Nat hiding (suc) -open import Function - -module stack-subtype (A : Set) where - --- data definitions - -data Element (a : Set) : Set where - cons : a -> Maybe (Element a) -> Element a - -datum : {a : Set} -> Element a -> a -datum (cons a _) = a - -next : {a : Set} -> Element a -> Maybe (Element a) -next (cons _ n) = n - -record SingleLinkedStack (a : Set) : Set where - field - top : Maybe (Element a) -open SingleLinkedStack - -record Context : Set where - field - -- fields for concrete data segments - n : ℕ - -- fields for stack - element : Maybe A - - - - - -open import subtype Context as N - -instance - ContextIsDataSegment : N.DataSegment Context - ContextIsDataSegment = record {get = (\c -> c) ; set = (\_ c -> c)} - - -record Meta : Set₁ where - field - -- context as set of data segments - context : Context - stack : SingleLinkedStack A - nextCS : N.CodeSegment Context Context - - - - -open import subtype Meta as M - -instance - MetaIncludeContext : M.DataSegment Context - MetaIncludeContext = record { get = Meta.context - ; set = (\m c -> record m {context = c}) } - - MetaIsMetaDataSegment : M.DataSegment Meta - MetaIsMetaDataSegment = record { get = (\m -> m) ; set = (\_ m -> m) } - - -liftMeta : {X Y : Set} {{_ : M.DataSegment X}} {{_ : M.DataSegment Y}} -> N.CodeSegment X Y -> M.CodeSegment X Y -liftMeta (N.cs f) = M.cs f - -liftContext : {X Y : Set} {{_ : N.DataSegment X}} {{_ : N.DataSegment Y}} -> N.CodeSegment X Y -> N.CodeSegment Context Context -liftContext {{x}} {{y}} (N.cs f) = N.cs (\c -> N.DataSegment.set y c (f (N.DataSegment.get x c))) - --- definition based from Gears(209:5708390a9d88) src/parallel_execution - -emptySingleLinkedStack : SingleLinkedStack A -emptySingleLinkedStack = record {top = nothing} - - -pushSingleLinkedStack : Meta -> Meta -pushSingleLinkedStack m = M.exec (liftMeta n) (record m {stack = (push s e) }) - where - n = Meta.nextCS m - s = Meta.stack m - e = Context.element (Meta.context m) - push : SingleLinkedStack A -> Maybe A -> SingleLinkedStack A - push s nothing = s - push s (just x) = record {top = just (cons x (top s))} - - - -popSingleLinkedStack : Meta -> Meta -popSingleLinkedStack m = M.exec (liftMeta n) (record m {stack = (st m) ; context = record con {element = (elem m)}}) - where - n = Meta.nextCS m - con = Meta.context m - elem : Meta -> Maybe A - elem record {stack = record { top = (just (cons x _)) }} = just x - elem record {stack = record { top = nothing }} = nothing - st : Meta -> SingleLinkedStack A - st record {stack = record { top = (just (cons _ s)) }} = record {top = s} - st record {stack = record { top = nothing }} = record {top = nothing} - - - - -pushSingleLinkedStackCS : M.CodeSegment Meta Meta -pushSingleLinkedStackCS = M.cs pushSingleLinkedStack - -popSingleLinkedStackCS : M.CodeSegment Meta Meta -popSingleLinkedStackCS = M.cs popSingleLinkedStack - - --- for sample - -firstContext : Context -firstContext = record {element = nothing ; n = 0} - - -firstMeta : Meta -firstMeta = record { context = firstContext - ; stack = emptySingleLinkedStack - ; nextCS = (N.cs (\m -> m)) - } - - -
--- a/paper/src/stack.h Sat Jan 06 19:04:39 2018 +0900 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,7 +0,0 @@ -struct SingleLinkedStack { - struct Element* top; -} SingleLinkedStack; -struct Element { - union Data* data; - struct Element* next; -} Element;
--- a/paper/src/struct-init.c Sat Jan 06 19:04:39 2018 +0900 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,1 +0,0 @@ -struct Point p = {100 , 200};
--- a/paper/src/struct.c Sat Jan 06 19:04:39 2018 +0900 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,4 +0,0 @@ -struct Point { - int x; - int y; -};
--- a/paper/src/stub.cbc Sat Jan 06 19:04:39 2018 +0900 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,17 +0,0 @@ -__code put(struct Context* context, - struct Tree* tree, - struct Node* root, - struct Allocate* allocate) -{ - /* 実装コードは省略 */ -} - -__code put_stub(struct Context* context) -{ - goto put(context, - &context->data[Tree]->tree, - context->data[Tree]->tree.root, - &context->data[Allocate]->allocate); -} - -
--- a/paper/src/subtype.agda Sat Jan 06 19:04:39 2018 +0900 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,44 +0,0 @@ -open import Level -open import Relation.Binary.PropositionalEquality - -module subtype {l : Level} (Context : Set l) where - - -record DataSegment {ll : Level} (A : Set ll) : Set (l ⊔ ll) where - field - get : Context -> A - set : Context -> A -> Context -open DataSegment - -data CodeSegment {l1 l2 : Level} (A : Set l1) (B : Set l2) : Set (l ⊔ l1 ⊔ l2) where - cs : {{_ : DataSegment A}} {{_ : DataSegment B}} -> (A -> B) -> CodeSegment A B - -goto : {l1 l2 : Level} {I : Set l1} {O : Set l2} -> CodeSegment I O -> I -> O -goto (cs b) i = b i - -exec : {l1 l2 : Level} {I : Set l1} {O : Set l2} {{_ : DataSegment I}} {{_ : DataSegment O}} - -> CodeSegment I O -> Context -> Context -exec {l} {{i}} {{o}} (cs b) c = set o c (b (get i c)) - - -comp : {con : Context} -> {l1 l2 l3 l4 : Level} - {A : Set l1} {B : Set l2} {C : Set l3} {D : Set l4} - {{_ : DataSegment A}} {{_ : DataSegment B}} {{_ : DataSegment C}} {{_ : DataSegment D}} - -> (C -> D) -> (A -> B) -> A -> D -comp {con} {{i}} {{io}} {{oi}} {{o}} g f x = g (get oi (set io con (f x))) - -csComp : {con : Context} -> {l1 l2 l3 l4 : Level} - {A : Set l1} {B : Set l2} {C : Set l3} {D : Set l4} - {{_ : DataSegment A}} {{_ : DataSegment B}} {{_ : DataSegment C}} {{_ : DataSegment D}} - -> CodeSegment C D -> CodeSegment A B -> CodeSegment A D -csComp {con} {A} {B} {C} {D} {{da}} {{db}} {{dc}} {{dd}} (cs g) (cs f) - = cs {{da}} {{dd}} (comp {con} {{da}} {{db}} {{dc}} {{dd}} g f) - - - -comp-associative : {A B C D E F : Set l} {con : Context} - {{da : DataSegment A}} {{db : DataSegment B}} {{dc : DataSegment C}} - {{dd : DataSegment D}} {{de : DataSegment E}} {{df : DataSegment F}} - -> (a : CodeSegment A B) (b : CodeSegment C D) (c : CodeSegment E F) - -> csComp {con} c (csComp {con} b a) ≡ csComp {con} (csComp {con} c b) a -comp-associative (cs _) (cs _) (cs _) = refl
--- a/paper/src/type-cs.c Sat Jan 06 19:04:39 2018 +0900 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,9 +0,0 @@ -__code getMinHeight_stub(struct Context* context) { - goto getMinHeight(context, &context->data[Allocate]->allocate, &context->data[AkashaInfo]->akashaInfo); -} - -__code getMinHeight(struct Context* context, struct Allocate* allocate, struct AkashaInfo* akashaInfo) { - /* ... */ - goto getMinHeight_stub(context); -} -
--- a/paper/src/type-ds.h Sat Jan 06 19:04:39 2018 +0900 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,5 +0,0 @@ -struct AkashaInfo { - unsigned int minHeight; - unsigned int maxHeight; - struct AkashaNode* akashaNode; -};
--- a/paper/src/type-mds.h Sat Jan 06 19:04:39 2018 +0900 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,15 +0,0 @@ -struct Data { /* data segments as types */ - struct Tree { /* ... */ } tree; - struct Node { /* ... */ } node; - - struct IterElem { /* ... */ } iterElem; - struct Iterator { /* ... */ } iterator; - struct AkashaInfo { /* ... */} akashaInfo; - struct AkashaNode { /* ... */} akashaNode; -}; - - -struct Context { /* meta data segment as subtype */ - /* ... fields for meta computations ... */ - struct Data **data; /* data segments */ -};