Mercurial > hg > Papers > 2019 > oshiro-thesis
changeset 9:6cc7d59970a0
update tex
| author | e155702 |
|---|---|
| date | Sun, 17 Feb 2019 14:33:29 +0900 |
| parents | 1f35e28d486c |
| children | ef433c736f4f |
| files | final_main/chapter3.tex final_main/chapter4.tex final_main/main.pdf final_main/main.tex |
| diffstat | 4 files changed, 19 insertions(+), 671 deletions(-) [+] |
line wrap: on
line diff
--- a/final_main/chapter3.tex Sun Feb 17 06:09:03 2019 +0900 +++ b/final_main/chapter3.tex Sun Feb 17 14:33:29 2019 +0900 @@ -1,487 +1,12 @@ -\chapter{定理証明支援器 Agda での証明} - -型システムを用いて証明を行うことができる言語として Agda \cite{agda}が存在する。 -Agda は依存型という型システムを持つ。依存型とは型も第一級オブジェクトとする型シ -ステムで、依存型を持っている言語では型を基本的な操作に制限なしに使用できる -。 -型システムは Curry-Howard 同型対応により命題と型付きラムダ計算が一対一で対応する。 - - -本章では Agda で証明をするために必要な要素について説明し、Natural Deduction での証明とそれに対応して Agda 使って証明ができることを示す。 -% 型システムは Curry-Howard 同型対応により命題と型付きラムダ計算が一対一で対応する。 -% 依存型という表現力の高い型を持つ証明支援系 Agda を用いて型システムで証明が行える -% ことを示す。 - -%% ここではAgdaの文法に触るだけにとどめて Agdaと証明のchapを一つ追加。 -% 其処に自然証明とAgdaの証明とかCurry-Howard対応の話とかを入れるときれいになるか -% も -%% 依存型を持っている言語には Agda の他に ATS 、 Coq 、 F* 、 Idris 、 Shen など -%% がある。 - -\section{Agda の文法} +\chapter{TreeVNC の改良点} -Agda はインデントに意味を持つため、きちんと揃える必要がある。 -また、スペースの有無は厳格にチェックされる。 -なお、 \verb/--/ の後はコメントである。 - -Agda のプログラムでは全てモジュール内部に記述されるため、まずはトップレベルにモ -ジュールを定義する必要がある。トップレベルのモジュールはファイル名と同一になる。 - -通常のモジュールをインポートする時は \verb/import/ キーワードを指定する。 -また、インポートを行なう際に名前を別名に変更することもでき、その際は \verb/as/ キーワードを用いる。 -モジュールから特定の関数のみをインポートする場合は \verb/using/ キーワードの後に -関数名を、関数の名前を変える時は \verb/renaming/キーワードを、特定の関数のみを隠 -す場合は \verb/hiding/ キーワードを用いる。 -なお、モジュールに存在する関数をトップレベルで用いる場合は \verb/opestack に対する操作を定義しており、n/ キーワードを使うことで展開できる。 -モジュールをインポートする例をリスト~\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} - -Agda における型指定は $:$ を用いて行う。 - -例えば、変数xが型Aを持つ、ということを表すには \verb/x : A/ と記述する。 - -データ型は、代数的なデータ構造で、その定義には \verb/data/ キーワードを用いる。 -\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} +\section{IPv6 アドレス対応} -関数の定義は、関数名と型を記述した後に関数の本体を \verb/=/ の後に記述する。 -関数の型には $ \rightarrow $ 、 または\verb/->/ を用いる。 -例えば引数が型 \verb/A/ で返り値が型 \verb/B/ の関数は \verb/A -> B/ のように書 -ける。 -また、複数の引数を取る関数の型は \verb/A -> A -> B/ のように書ける。この -時の型は \verb/A -> (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} - -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} - -% この \verb/elem/ 関数はリスト~\ref{src:agda-elem-apply} のように利用できる。 -% Nat型の要素を持つリストの内部に4が含まれるか確認している。 -% この \verb/listHas4/ は \verb/true/ に評価される。 - -% \lstinputlisting[label=src:agda-elem-apply, caption=部分型を持つ関数の適用] {src/AgdaElemApply.agda} - -\section{Natural Deduction} -% Natural Deduction のお話。細かい規則は…書かなきゃいけないよね… -% いらない規則は省略しようと、少なくとも3段論法を証明できるだけ置く。。。？ -% とりあえず証明に使えるやつは全部書いて必要あるやつを詳しく。 - -Natural Deduction (自然演繹)は Gentzen によって作られた論理及びその証明システムである。 -% ~\cite{Girard:1989:PT:64805}。 -命題変数と記号を用いた論理式で論理を記述し、推論規則により変形することで求める論理式を導く。 - -Natural Deduction では次のように - -\begin{eqnarray} - \vdots \\ \nonumber - A \\ \nonumber -\end{eqnarray} - -と書いた時、命題Aを証明したことを意味する。証明は木構造で表わされ、葉の命題は仮 -定となる。 - -\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 - - 導入。証明された論理式に対して記号を導入することで新たな証明を導く。 +\section{hidescreen} +%displaymode の時に viewer が出ないようにしている -\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 では、これまでで説明したような規則を使い証明を行うことができる。 - -例として Natural Deduction で三段論法の証明を行う。 -このとき、「A は B であり、 B は C である。よって A は C である」 が証明するべき -命題である。 - -この命題では 「A は B であり」と 「B は C である」の二つの小さい命題に分けられる。 -この「A は B であり」から、AからBが導出できることが分かり、これは $ A \Rightarrow B $ と表せる。 -また、「B は C である」から、BからCが導出できることが分かる。これも「A は B であ -り」の時と同様に $ B \Rightarrow 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} - - -Natural Deductionでは次のような証明木になる。 - - -\begin{figure}[htpb] - \begin{center} - \includegraphics{pic/modus-ponens.pdf} - \end{center} - \caption{自然演繹での三段論法の証明} - \label{fig:modus-ponens} -\end{figure} - -これにより自然演繹を使って三段論法が証明できた。 -%%%%%%%%%%%%%%%%%%%%%% - - -\section{Natural Deduction と 型付き $ \lambda $ 計算} - -ここでは、 Natural Deduction と型付き$ \lambda $ 計算の対応を定義する。 -対応は以下の表\ref{table:curry-howard}のようになる。 - -\begin{center} - \begin{table}[h] -% \scalebox{0.75}{ - \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 - \end{tabular} -% } - \caption{natural deuction と 型付き $ \lambda $ 計算との対応(Curry-Howard Isomorphism)} - \label{table:curry-howard} - \end{table} -\end{center} - -この対応をもとに Agda で型付き $\lambda$ 計算による証明を示す。 -% ここでは例として ((A ならば B) かつ (B ならば C)) ならば (A ならば C) が成り立つという三段論法を証明をする。 -ここでも先程 Natural Deduction で証明した三段論法を例とする。 -% この三段論法は自然演繹では\ref{fig:modus-ponens}のようになっていた。 - -% \begin{figure}[htpb] -% \begin{center} -% \includegraphics{pic/modus-ponens.pdf} -% \end{center} -% \caption{自然演繹での三段論法の証明} -% \label{fig:modus-ponens} -% \end{figure} - -%McCこの証明木に対応するAgdaによる証明はリスト\ref{agda-moduse-ponens}のようになる。 - -\begin{lstlisting}[frame=lrbt,label=agda-moduse-ponens,caption={\footnotesize Agda による - 三段論法の定義と証明}] -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 - - -f : {A B C : Set} → ((A → B) × (B → C)) → (A → C) -f = λ p x → (snd p) ((fst p) x) -\end{lstlisting} - -自然演繹での三段論法の証明は、1つの仮定から $ \land 1 \mathcal{E} $ と $ \land 2 \mathcal{E} $ を用いて仮定を二つ取り出し、それぞれに $ \Rightarrow \mathcal{E} $ を適用した後に仮定を $ \Rightarrow \mathcal{I}$ して導出していた。 - -ここで $ \Rightarrow \mathcal{I}$ に対応するのは関数適用である。 -よってこの証明は「一つの変数から fst と snd を使って関数を二つ取り出し、それぞれを関数適用する」という形になる。 -これをラムダ式で書くとリスト~\ref{src:agda-modus-ponens}のようになる。 -仮定 $ (A \rightarrow B) \times (B \rightarrow C) $ と仮定 A から A $ \rightarrow $ C を導いている。 - -仮定に相当する変数 p の型は$ (A \rightarrow B) \times (B \rightarrow C) $ であり、p からそれぞれの命題を取り出す操作が fst と snd に相当する。 -fst p の型は $ (A \rightarrow B) $ であり、snd p の型は $ (B \rightarrow C) $ である。 -もう一つの仮定xの型は A なので、fst p を関数適用することで B が導ける。 -得られた B を snd p に適用することで最終的に C が導ける。 - -\lstinputlisting[label=src:agda-modus-ponens, caption=Agda における三段論法の証明] {src/AgdaModusPonens.agda} - -このように Agda でも自然演繹と同様に証明を記述できる。 +\section{errordialog} \ No newline at end of file
--- a/final_main/chapter4.tex Sun Feb 17 06:09:03 2019 +0900 +++ b/final_main/chapter4.tex Sun Feb 17 14:33:29 2019 +0900 @@ -1,199 +1,22 @@ -%% Natural Deduction の説明をして、 Agda が命題を証明することができることを示す -%% 章? 要る。。。かどうかは微妙な気がする。 「こういう話で Agda では証明ができます。」 -%% で勝手に証明して証明できたね！はありだけど読み手があんまり嬉しくないかも。 -%% ソレだとやっぱり自然演繹の話しして~同型対応でちゃんとつながってるね~じゃあ -%% Agda で表現できるし証明できるねでいい感じかも - -\chapter{Agda における CbC の表現} - -% ツッコミどころさん -% どうするのかは書けるけどなんでAgdaなの？みたいな話が飛んでくる - -前章では Agda の文法について説明した。 -本章では CbC と対応して CodeGear、 DataGear、 継続を Agda で表現する。 -また、 Agda で継続を記述することで得た知見を示す。 - -\section{Agda での CodeGear 、 DataGear 、 継続の表現} - -%% 書くこと -% CodeGearとDataGearのAgda上での定義 - -DataGear はレコード型で表現できるため、 Agda のレコード型をそのまま利用して定義 -してく。 -記述は~\ref{src:agda-ds}のようになる。 - -\lstinputlisting[label=src:agda-ds, caption=Agda における DataGear の定義] -{src/DataSegment.agda.replaced} - -CodeGear は DataGear を受け取って DataGear を返すという定義であるため、 -$ I \rightarrow O $ を内包する CodeGear 型のデータ型(~\ref{src:agda-cs})を定義する。 - -\lstinputlisting[label=src:agda-cs, caption= Agda における CodeGear 型の定義] {src/CodeSegment.agda.replaced} - -CodeGear 型を定義することで、 Agda での CodeGear の本体は Agda での関数そのもの -と対応する。 -% しかし、そのままだと再帰呼び出しの点で CbC との対応が失われてしまう。 -% そのため、 Agda では \verb/goto/を利用できるのは関数の末尾のみという制約を設ける -% 必要がある。 -% この制約さえ満たせば、 - -CodeGear の実行は CodeGear 型から関数本体を取り出し、レコード型を持つ値を適用す -ることに相当する。 +\chapter{マルチキャスト対応} -CbC での軽量継続は - -\begin{itemize} - \item 次に実行する CodeGear を指定する - \item CodeGear に渡す DataGear を指定する - \item 現在実行している CodeGear から制御を指定された CodeGear へと移す -\end{itemize} +\section{有線接続との接続形式の違い} +マルチキャスト通信では、サーバー側は一度の送信で接続しているデバイス全てにデータを届けることができる。 -の機能を持っている。 - -この機能を満たす関数はソースコード\ref{src:agda-goto} として定義されている。 - -\lstinputlisting[label=src:agda-goto, caption=Agdaにおける goto の定義] {src/Goto.agda.replaced} - -goto は CodeGear よりも一つ Level が上の Meta CodeGear にあたり、次に実行する -CodeGear 型を受け取り、Input DataGear、 Output DataGear を返す。型になっている。 +TreeVNC に無線 LAN 接続した場合、マルチキャスト通信を行う想定で実装しているため、新たな Node を有線接続の際行なっていたバイナリツリー状での接続方式とは異なった方法で管理する(図)。 -\section{Agda での Stack、 Tree の実装} - -ここでは Agda での Stack 、 Tree の実装を示す。 - -Stack の実装を以下のソースコード\ref{src:stack-impl}で示す。 -実装は SingleLinkedStack という名前で定義されている。 -定義されている API は push を例に残りは省略する。残りのの実装は付録に示す。 %~\ - -\lstinputlisting[label=src:stack-impl, caption=Agdaにおける Stack の実装] {src/AgdaStackImpl.agda.replaced} - -Element は SingleLinkedStack で扱われる要素の定義で、現在のデータ datum と次のデー -タを Maybe 型という値の存在が不確かな場合の型で包み、自身で再帰的に定義している。 -Maybe 型では値が存在する場合は Just 、 存在しない場合は Nothing を返す。 - -SingleLinkedStack 型では、この Element の top 部分のみを定義している。 - -Stack に対する push 操作では stack と push する element 型の datum を受け取り、 datum -の next に現在の top を入れ、 stack の top を受け取った datum に切り替え、新しい -stack を返すというような実装をしている。 - -Tree の実装(以下のソースコード\ref{src:tree-impl})は RedBlackTree という名前で定義されている。 -定義されている API は put 以後省略する。残りのの実装は付録に示す。 %~\ - -\lstinputlisting[label=src:tree-impl, caption=Agdaにおける Tree の実装] {src/AgdaTreeImpl.agda.replaced} +\section{Blocking} +無線 LAN 通信は、有線接続と比較して一度に送信できるデータ量が少ない。そのためサーバー側が送信した更新データが正確にクライアントに送られない可能性がある。 -Node 型は key と value 、 Color と Node の rihgt 、 left の情報を持っている。 -Tree を構成する末端の Node は leafNode 型で定義されている。 - -RedBlackTree 型は root の Node 情報と Tree に関する計算をする際に、そこまでの -Node の経路情報を保持するための nodeStack と 比較するための compare を持っている。 - -Tree の put 操作では tree 、 put するノードのキーと値(k1、value)を引数として受け -取り、Tree の root に Node が存在しているかどうかで場合分けしている。 -Nothing が返ってきたときは RedBlackTree 型の tree 内に定義されている root に受け -取ったキーと値を新しいノードとして追加する。 -Just が返ってきたときは root が存在するので、経路情報を積むために nodeStack を初 -期化し、受け取ったキーと値で新たなノードを作成した後、ノードが追加されるべき位置 -までキーの値を比べて新しい Tree を返すというような実装になっている。 - -\section{Agda における Interface の実装} - -%% 書くこと -% stack の Interface部分と redBlackTree の Interface部分。 -% interfaceとは?->cbcのとこに突っ込んでこっちは同様に〜で済ませたい - -Agda 側でも CbC 側と同様に interface を実装した。 -interface は record で列挙し、ソースコード~\ref{src:agda-interface}のように紐付けることができる。 -CbC とは異なり、 Agda では型を明記する必要があるため record 内に型を記述している。 - -例として Agda で実装した Stack 上の interface (ソースコード\ref{src:agda-interface})を見る。 -Stack の実装は SingleLinkedStack(ソースコード\ref{src:agda-single-linked-stack}) として書かれている。それを Stack 側から -interface を通して呼び出している。 +対策として、データを分割(Blocking)して送信する手法を実装した。 -ここでの interface の型は Stack の record 内にある pushStack や popStack などで、 -実際に使われる Stack の操作は StackMethods にある push や popである。この push -や pop は SingleLinkedStack で実装されている。 - -% \lstinputlisting[label=src:agda-single-linked-stack, caption=Agda における Stack -% の実装] {src/AgdaSingleLinkedStack.agda.replaced} - -\lstinputlisting[label=src:agda-interface, caption=Agda における Interface の定義] {src/AgdaInterface.agda.replaced} - -interface を通すことで、実際には Stack の push では stackImpl と何らかのデータ a を取 -り、 stack を変更し、継続を返す型であったのが、 pushStack では 何らかのデータ a を取り stack を変更 -して継続を返す型に変わっている。 - -また、 Tree でも interface を記述した。 - -\lstinputlisting[label=src:agda-tree, caption=Tree Interface の定義]{src/AgdaTree.agda.replaced} - -interface を記述することによって、データを push する際に予め決まっている引数を省 -略することができた。 -また、 Agda で interface を記述することで CbC 側では意識していなかった型が、明確 -化された。 - -% 元の push では 送り先の stack を関数に書く必要があり、異なる stack に push -% する可能性があったが、 pushStack では紐付けた Stack に push することになり +従来の TreeVNC では、配信側の画面が更新された場合、サーバーから FRAME_BUFFER_UPDATE メッセージが送信され、更新データは MulticastQueue というキューに格納される。 -\section{継続を使った Agda における Test , Debug} - -Agda ではプログラムのコンパイルが通ると型の整合性が取れていることは保証できるが、必ず -しも期待した動作をするとは限らない。そのため、本研究中に書いたプログラムが正しい動 -作をしているかを確認するために行なった手法を幾つか示す。 - -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -今回は実験中にソースコード\ref{src:agda-stack-test}のような Test を書いた。 -この Test では Stack をターゲットにしていて、 Stack に1、 2の二つの$ \mathbb{N} $型のデー -タを push した後、 pop2 Interface を使って Stack に入っている 1、 2 が Stack の -定義である First in Last out の通りに 2、 1 の順で取り出せるかを確認するために作成した。 - -\lstinputlisting[label=src:agda-stack-test, caption=Agdaにおけるテスト]{src/AgdaStackTest.agda.replaced} +Blocking は、更新データを長方形(Rectangle)で分割し、 MulticastQueue に格納する。 -上の Test では、02 が 2つのデータを push し、 03 で 二つのデータを pop する pop2 -を行っている。それらをまとめて記述したものが 04 で 2 回 push し、 2つのデータを pop する動 -作が正しく行われていれば 04 は True を返し、 05 で記述された型通りに互いに等しくなる -ため 05 が refl でコンパイルが通るようになる。 -今回は、 pop2 で取れた値を確認するため 03 の後に 031、 032 の二つの作成した。 -032 では 03 で扱っている値が Maybe であるため、 031 のような比較をする前に値が確 -実に存在していることを示す補題である。 032 を通すことで 031 では 2つの値があり、 -かつ$\mathbb{N}$型である事がわかる。 031 では直接取れた値が 2、 1 の順番で入って -いるかを確認している。 - -この Test でエラーが出なかったことから、 Stack に1、2の二つのデータを pushする -と、 push した値が Stack 上から消えることなく push した順番に取り出せることが分 -かる。 +\section{圧縮形式} -また、継続を用いて記述することで関数の Test を書くことで計算途中のデータ内部をチェックするこ -とができた。 - -ここでの \$ は \( \) をまとめる糖衣構文で、 \$ が書かれた一行を\(\)でくくること -ができる。 -% \ref{sintax}のようなコードを -% \begin{lstlisting}[frame=lrbt,label=sintax,caption={\footnotesize 通常の継続の -% コード}] - -% \end{lstlisting} - -% \begin{lstlisting}[frame=lrbt,label=sintax-sugar,caption={\footnotesize 糖衣構文 -% を用いた継続のコード}] - -% \end{lstlisting} - -ソースコード~\ref{src:agda-tree-debug}のように関数本体に記述してデータを返し、C-c C-n -(Compute normal form) で関数を評価すると関数で扱っているデータを見ることができる。 -また、途中の計算で受ける変数名を変更し、 Return 時にその変更した変数名に変えるこ -とで、計算途中のデータの中身を確認することができる。評価結果はソースコード内にコメントで記述した。 - - \lstinputlisting[label=src:agda-tree-debug, caption=Agdaにおけるテスト]{src/AgdaTreeDebug.agda.replaced} - -今回、この手法を用いることで複数の関数を組み合わせた findNode 関数内に異常があるこ -とが分かった。 - - -%getRedBlackTree の関数に - -% \lstinputlisting[label=agda-Debug, caption=Agdaにおけるデバッグ]{src/AgdaTreeDebug.agda.replaced} -% Tree全然載せてないけどどうしよ。。。どこに書こうかは考えておきましょう +\section{}