--- a/paper/agda.tex	Wed Feb 08 15:52:44 2017 +0900
+++ b/paper/agda.tex	Wed Feb 08 17:25:27 2017 +0900
@@ -10,7 +10,7 @@
 型システムは Curry-Howard 同型対応により命題と型付きラムダ計算が一対一に対応する。
 依存型という型を持つ証明支援系言語 Agda を用いて型システムで証明が行なえることを示す。
 
-% {{{ 型システムとは TODO: もう少し大ざっぱに説明
+% {{{ 型システムとは
 \section{型システムとは}
 型システムとは、計算する値を分類することにでプログラムがある種の振舞いを行なわないことを保証する機構の事である\cite{Pierce:2002:TPL:509043}\cite{pierce2013型システム入門プログラミング言語と型の理論}。
 ある種の振舞いとはプログラム中の評価不可能な式や、言語として未定義な式などが当て嵌まる。
@@ -57,6 +57,188 @@
 
 % }}}
 
+% {{{ 依存型を持つ証明支援系言語 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}
+
+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}
+
+
+関数の定義は 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}
+
+引数は変数名で受けることもできるが、具体的なコンストラクタを指定することでそのコンストラクタが渡された時の挙動を定義できる。
+これはパターンマッチと呼ばれ、コンストラクタで case 文を行なっているようなものである。
+例えば Bool 型の値を反転する \verb/not/ 関数を書くとリスト~\ref{src:agda-not}のようになる。
+
+\lstinputlisting[label=src:agda-not, caption=Agdaにおける関数 not の定義] {src/AgdaNot.agda}
+
+パターンマッチは全てのコンストラクタのパターンを含まなくてはならない。
+例えば、Bool 型を受け取る関数で \verb/true/ の時の挙動のみを書くことはできない。
+なお、コンストラクタをいくつか指定した後に変数で受けると、変数が持ちうる値は指定した以外のコンストラクタとなる。
+例えばリスト~\ref{src:agda-pattern}の not は x には true しか入ることは無い。
+なお、マッチした値を変数として利用しない場合は \verb/_/ を用いて捨てることもできる。
+
+\lstinputlisting[label=src:agda-pattern, caption=Agdaにおけるパターンマッチ] {src/AgdaPattern.agda}
+
+関数にはリテラルが存在し、関数名を定義せずともその場で生成することができる。
+これをラムダ式と呼び、\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}
+
+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}
+
+
+データ型のコンストラクタには自分自身の型を引数に取ることもできる(リスト~\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}
+
+自然数に対する演算は再帰関数として定義できる。
+例えば自然数どうしの加算は二項演算子\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}
+
+次に依存型について見ていく。
+依存型で最も基本的なものは関数型である。
+依存型を利用した関数は引数の型に依存して返す型を決定できる。
+
+Agda で \verb/(x : A) -> B/ と書くと関数は型 A を持つx を受け取り、Bを返す。
+ここで B の中で x を扱っても良い。
+例えば任意の型に対する恒等関数はリスト~\ref{src:agda-id}のように書ける。
+
+\lstinputlisting[label=src:agda-id, caption=依存型を持つ関数の定義] {src/AgdaId.agda}
+
+この恒等関数 \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}
+
+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}
+
+構築されたレコードから値を取得する際には \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}
+
+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}
+
+ある型 T がこの部分型制約を満たすことを示すには、型 T でこのレコードを作成できることを示し、それを instance 構文で登録する。
+型Nat が Eq の上位型であることを記述するとリスト~\ref{src:agda-instance}のようになる。
+
+\lstinputlisting[label=src:agda-instance, caption=Agdaにおける部分型関係の構築] {src/AgdaInstance.agda}
+
+これで \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}
+
+また、モジュールには値を渡すことができる。
+そのようなモジュールは 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}
+
+% }}}
+
 % {{{ Natural Deduction
 \section{Natural Deduction}
 \label{section:natural_deduction}
@@ -331,183 +513,6 @@
 \end{center}
 % }}}
 
-% {{{ 依存型を持つ証明支援系言語 Agda
-
-\section{依存型を持つ証明支援系言語 Agda}
-型システムを用いて証明を行なうことができる言語に Agda~\cite{agda} が存在する。
-Agda は依存型という強力な型システムを持っている。
-依存型とは型も第一級オブジェクトとする型であり、型を引数に取る関数や値を取って型を返す関数、型の型などが記述できる。
-この節では Agda の文法的な紹介を行なう~\cite{Norell:2009:DTP:1481861.1481862}~\cite{agda-documentation}。
-
-まず Agda のプログラムは全てモジュールの内部に記述されるため、まずはトップレベルにモジュールを定義する必要がある。
-トップレベルのモジュールはファイル名と同一となる。
-例えば \verb/AgdaBasics.agda/ のモジュール名定義はリスト~\ref{src:agda-module}のようになる。
-
-\lstinputlisting[label=src:agda-module, caption=Agdaのモジュールの定義する] {src/AgdaBasics.agda}
-
-また、Agda はインデントに意味を持つ言語であるため、インデントはきちんと揃える必要がある。
-
-まず Agda におけるデータ型について触れていく。
-Agda における型指定は $:$ を用いて行なう。
-例えば、変数xが型Aを持つ、ということを表すには \verb/x : A/ と記述する。
-
-データ型は Haskell や ML に似て代数的なデータ構造のパターンマッチを扱うことができる
-データ型の定義は \verb/data/ キーワードを用いる。
-\verb/data/キーワードの後に \verb/where/ 句を書きインデントを深くした後、値にコンストラクタとその型を列挙する。
-例えば Bool 型を定義するとリスト~\ref{src:agda-bool}のようになる。
-
-\lstinputlisting[label=src:agda-bool, caption=Agdaにおけるデータ型 Bool の定義] {src/AgdaBool.agda}
-
-Bool はコンストラクタ \verb/true/ か \verb/false/ を持つデータ型である。
-Bool 自身の型は \verb/Set/ であり、これは Agda が組み込みで持つ「型の型」である。
-Set は階層構造を持ち、型の型の型を指定するには Set1 と書く。
-
-関数の定義は Haskell に近い。
-関数名と型を記述した後に関数の本体を \verb/=/ の後に指定する。
-関数の型は単純型付き $ \lambda$ 計算と同様に $ \rightarrow $ を用いる。
-なお、$\rightarrow$に対しては糖衣構文 \verb/->/ も用意されている。
-引数は変数名で受けることもできるが、具体的なコンストラクタを指定することでそのコンストラクタが渡された時の挙動を定義できる。
-これはパターンマッチと呼ばれ、コンストラクタで case 文を行なっているようなものである。
-例えば Bool 型の値を反転する \verb/not/ 関数を書くとリスト~\ref{src:agda-not}のようになる。
-
-\lstinputlisting[label=src:agda-not, caption=Agdaにおける関数 not の定義] {src/AgdaNot.agda}
-
-関数にはリテラルが存在し、関数名を定義せずともその場で生成することができる。
-これをラムダ式と呼び、\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}
-
-コンストラクタによって処理を分岐する場合はパターンマッチを利用する。
-関数の変数部分にコンストラクタを指定し、それぞれに対する処理を \verb/=/ で繋いで記述する。
-パターンマッチは全てのコンストラクタのパターンを含まなくてはならない。
-なお、コンストラクタをいくつか指定した後に変数で受けると、変数が持ちうる値は指定した以外のコンストラクタとなる。
-例えばリスト~\ref{src:agda-pattern}の not は x には true しか入ることは無い。
-なお、マッチした値を変数として利用しない場合は \verb/_/ を用いて捨てることもできる。
-
-\lstinputlisting[label=src:agda-pattern, caption=Agdaにおけるパターンマッチ] {src/AgdaPattern.agda}
-
-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}
-
-
-データ型のコンストラクタには自分自身の型を引数に取ることもできる(リスト~\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}
-
-自然数に対する演算は再帰関数として定義できる。
-例えば自然数どうしの加算は二項演算子\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}
-
-次に依存型について見ていく。
-依存型で最も基本的なものは関数型である。
-依存型を利用した関数は引数の型に依存して返す型を決定できる。
-
-Agda で \verb/(x : A) -> B/ と書くと関数は型 A を持つx を受け取り、Bを返す。
-ここで B の中で x を扱っても良い。
-例えば任意の型に対する恒等関数はリスト~\ref{src:agda-id}のように書ける。
-
-\lstinputlisting[label=src:agda-id, caption=依存型を持つ関数の定義] {src/AgdaId.agda}
-
-この恒等関数 \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}
-
-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}
-
-構築されたレコードから値を取得する際には \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}
-
-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}
-
-ある型 T がこの部分型制約を満たすことを示すには、型 T でこのレコードを作成できることを示し、それを instance 構文で登録する。
-型Nat が Eq の上位型であることを記述するとリスト~\ref{src:agda-instance}のようになる。
-
-\lstinputlisting[label=src:agda-instance, caption=Agdaにおける部分型関係の構築] {src/AgdaInstance.agda}
-
-これで \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/ に評価される。
-なお、 \verb/--/ の後はコメントである。
-
-\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}
-
-また、モジュールには値を渡すことができる。
-そのようなモジュールは 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}
-
-% }}}
-
 % {{{ Reasoning
 
 \section{Reasoning}

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/paper/src/AgdaFunction.agda	Wed Feb 08 17:25:27 2017 +0900
@@ -0,0 +1,2 @@
+f : Bool -> Bool
+f x = true

--- a/paper/summary.tex	Wed Feb 08 15:52:44 2017 +0900
+++ b/paper/summary.tex	Wed Feb 08 17:25:27 2017 +0900
@@ -1,19 +1,20 @@
 \chapter{まとめ}
-本論文では Continuation based C のプログラムの CodeSegment と DataSegment が部分型で型付け可能なことを示した。
-部分型を利用した定義により Agda で CbC のプログラムを記述し、GearsOS のデータ構造 SingleLinkedStack の性質を証明した。
-よって、 CbC コンパイラやランタイムに依存型を加えることでCbCが自身を証明可能となることが分かった。
+本論文ではメタ計算を用いた Continuation based C プログラムの検証手法を二つ提案した。
+
+一つはモデル検査的なアプローチであり、メタ計算ライブラリ akasha を用いて GearsOS の非破壊赤黒木の仕様を保証した。
+CbC における仕様の定義は assert に渡す論理式として定義され、状態の数え上げは軽量継続 \verb/meta/ を切り替えることで実現できた。
+CbC で記述された非破壊赤黒木のプログラムを検証用に変更することなく、CbC 自身で検証した。
+検証できた範囲は有限の要素数のみであるが、有限モデルチェッカ CBMC よりも大きな範囲を検証した。
 
-また、部分型の定義により CodeSegment の再利用性が向上する機能を提案した。
-GearsOS では実行するプログラムごとに Meta DataSegemnt から DataSegment を取り出す CodeSegment \verb/stub/ を記述する必要があったが、部分型を利用することでコンパイル時やランタイムに自動生成できることが分かった。
-具体的には、プログラムを実行する際の全ての DataSegment の部分型となるような Meta DataSegment を処理系が用意することで実現できる。
+二つめは定理証明的なアプローチである。
+akasha を用いた検証では挿入回数は有限の数に限定されていた。
+データ構造とそれにまつわる処理を直接証明することにより、任意の回数操作を行なっても性質を保証する。
+部分型を利用して CbC の型システムの定義を行ない、依存型を持つ言語 Agda 上で記述することで CbC の形式的な定義とした。
+Agda 上で記述された CbC プログラムの性質を証明することで、 CbC が部分型できちんと型付けできること、依存型をCbCコンパイラに組み込むことでCbC 自身を証明できることが分かった。
 
-さらに、証明とは別のアプローチとしてモデル検査的な検証が可能であることを示した。
-メタ計算ライブラリ akasha を用いて赤黒木のプログラムを変更することなく仕様を保証した。
-その際、全ての状態を総当たりで列挙することは非効率であり、状態を縮小させる手法を適用すべきことが分かった。
-この状態の縮小にも、依存型が利用できると考えている。
-証明された性質を利用して、検査の必要が無い状態を排除するのである。
-
-CbC の型システムを定義することで、証明とモデル検査的なアプローチにおける検証手法と、GearsOS における CodeSegment の再利用性の向上を提案できた。
+また、型システムは証明以外にも実用的に利用できることが分かった。
+akasha を用いて検証を行なう際、全ての CodeSegment に対して stub をユーザが定義する必要があった。
+CbC の型を定義することにより、stub の自動生成と型チェックが行なえることが分かった。
 
 \section{今後の課題}
 今後の課題として、型システムの詳細な性質の解析がある。
@@ -21,14 +22,12 @@
 CodeSegment は関数呼び出しを末尾でしか許さない制限があるので、関数型の計算規則をより制限できるはずである。
 その制約の元に生まれた計算体系の持つ性質や表現能力に興味がある。
 
-また、提案した Agda における CbC 表現をより利用しやすい形でユーザに提供することも必要である。
-例えば CbC のコードから Agda のコードへの変換系や、Agda の内部表現から直接 CbC を生成することなどが考えられる。
-
-stub の自動生成に関しては、コンパイル時に DataSegment の部分型を自動で構成するようコンパイラを改良する必要がある。
-また、ランタイム時に生成された部分型情報を比較することにより、ネットワーク越しに CodeSegment を接続した際に互換性の確認が行なえると考えている。
+また、提案した型システムを CbC コンパイラの内部に組み込み、CodeSegment と DataSegment の型チェックを行なえるようにしたい。
+加えて部分型を組み込むことにより、stub の自動生成をする。
+さらに依存型を加えれば CbC で CbC 自身を証明できるようになる。
 
 モデル検査的アプローチの展望としては、依存型を CbC コンパイラに実装し、型情報を用いた記号実行や状態の列挙を行なうシステムの構築などがある。
 
-また、型システムの拡張として総称型などを CbC に適用することも挙げられる。
-総称型は \verb/Java/ における Generics や \verb/C++/ におけるテンプレートに相当し、ユーザが定義できるデータ構造の表現能力が向上する。
+また、型システムの拡張としては総称型などを CbC に適用することも挙げられる。
+総称型は \verb/Java/ におけるジェネリクスや \verb/C++/ におけるテンプレートに相当し、ユーザが定義できるデータ構造の表現能力が向上する。
 他にも、CbC における型推論や推論器のコンパイラへの実装などが挙げられる。