# HG changeset patch # User ryokka # Date 1517415270 -32400 # Node ID 0035f6d4826f37ad9665876da75d8a04ae1859a3 # Parent 46d543c569d2bdaa8dd548f182e9931d139f1f04 fix MindMap,add some chapter diff -r 46d543c569d2 -r 0035f6d4826f final_main/Makefile --- a/final_main/Makefile Thu Jan 25 17:00:42 2018 +0900 +++ b/final_main/Makefile Thu Feb 01 01:14:30 2018 +0900 @@ -52,7 +52,7 @@ .PHONY : pdf pdf : $(PDF_FILE) - open $(TARGET).pdf + open $(TARGET).pdf $(PDF_FILE) : $(DVI_FILE) $(TEX_FILES) $(EPS_FILES) $(CLASS_FILE) $(DVIPDF) $(TARGET) diff -r 46d543c569d2 -r 0035f6d4826f final_main/bibliography.tex --- a/final_main/bibliography.tex Thu Jan 25 17:00:42 2018 +0900 +++ b/final_main/bibliography.tex Thu Feb 01 01:14:30 2018 +0900 @@ -8,9 +8,20 @@ %書籍、論文、URLによって若干書き方が異なる。 %URLを載せる人は参考にした年月日を最後に記入すること。 -\bibitem{比嘉健太} +\bibitem{Verified} {比嘉健太, 河野真治}: メタ計算を用いた Continuation based C の検証手法 -, 琉球大学工学部情報工学科平成 29 年度学位論文(修士) (2016). +, 琉球大学工学部情報工学科平成 29 年度学位論文(修士) (2017). + +\bibitem{CbC-meta} +{宮城光希, 河野真治}: CbC 言語による OS 記述 +, 琉球大学工学部情報工学科平成 29 年度学位論文(学士) (2017). + +\bibitem{CbC-llvm} +{徳森海斗, 河野真治}: LLVM Clang 上の Contimuation based C コンパイラの改良 +, 琉球大学工学部情報工学科平成 28 年度学位論文(修士) (2016). + +\bibitem{Agda} +The Agda wiki \\\verb|http://wiki.portal.chalmers.se/agda/pmwiki.php| % \bibitem{gears} % {伊波立樹, 東恩納琢偉, 河野真治}: Code Gear、Data Gear に基づく OS のプロトタイプ diff -r 46d543c569d2 -r 0035f6d4826f final_main/chapter1.tex --- a/final_main/chapter1.tex Thu Jan 25 17:00:42 2018 +0900 +++ b/final_main/chapter1.tex Thu Feb 01 01:14:30 2018 +0900 @@ -1,4 +1,4 @@ -\chapter{(タイトル)} + \chapter{はじめに} \label{chap:introduction} \pagenumbering{arabic} @@ -9,13 +9,17 @@ 動作するプログラム(ソフトウェア)は高い信頼性を持つことが望ましい。 +% しかし、既存の言語で関数より細かい単位に分割することは難しい。そのために当研究 +% 室ではコードの単位を CodeSegment ~ プログラムの信頼性を保証するにはプログラムが期待される仕様を満たすことを検証する手法と、その仕様を直接証明する手法が存在している。 - しかし、期待される仕様を満たすかを検証する際、仕様が大きくなるに連れ指数関数的に検証する項が増えてしまう。そのため、ここでは仕様を直接証明する手法を利用している。 - 証明では - -そのために当研究室ではコードセグメント、データセグメントという単位を用いてプログラムを記述する手法を提案している。 + + % しかし、期待される仕様を満たすかを検証する際、仕様が大きくなるに連れ指数関数的に検証する項が増えてしまう。そのため、ここでは仕様を直接証明する手法を用いている。 + +そのために当研究室ではCodeSegment、DataSegmentという単位を用いてプログラムを記述する手法を提案している。 + %% コードセグメントは通常の言語での関数を細かくしたものとしてよい？ + 本研究では CbC を用いて UnblanceTree を実装し、等価な Agda でその一部を証明する。 %% 動作するプログラムの信頼性を保証したい diff -r 46d543c569d2 -r 0035f6d4826f final_main/chapter2.tex --- a/final_main/chapter2.tex Thu Jan 25 17:00:42 2018 +0900 +++ b/final_main/chapter2.tex Thu Feb 01 01:14:30 2018 +0900 @@ -1,27 +1,134 @@ -\chapter{Continuation based C} +\chapter{Continuation based C (CbC)} + %% CbCとはなにか？どのようなものか？どのようにしてなりたっているか？ +Continuation based C (以下 CbC )は当研究室で開発しているプログラミング言語である。 +CbC は殆ど C 言語と同じ構文を持つが、関数よりも細かい記述でプログラミングする。 +CbC では処理を CodeSegment という単位で定義し、処理に使うデータをまとめて +　DataSegment という単位で定義している。 +実行時には CodeSegment で DataSegment を変更しながら処理を遷移していくことでプロ +グラムを実行する。 +CbCの処理系には llvm/clang による実装と gcc による実装などが存在している。 + + +\section{CodeSegment と DataSegment} +%% どういう概念？ どうしてそうするの？ どうやってつかうの？ + +本研究室では検証しやすいプログラムの単位として CodeSegment と DataSegment を用いるプ +ログラミングスタイルを提案している。% 本当に検証のためだけなの？ +この単位では通常の関数より細かいもので、通常の関数処理をより細かく分割できる。そのため通常より細かい単位で検証できる。 + CodeSegment は処理の単位である。入力を受け取り、処理を行なった後に出力を行う。 + CodeSegment は他の CodeSegment と接続することができる。 + + DataSegment は CodeSegment で扱うデータの単位であり、処理に必要なデータが全て入って +いる。CodeSegment の入力となる DataSegment は Input DataSegment と呼ばれ、 +出力は Output DataSegment と呼ばれる。 +リスト \ref{code_simple} の場合, cs0 は cs1 に継続すると cs0 の環境は破棄されて +しまうため, cs0 に戻ることは出来ない. +\begin{lstlisting}[frame=lrbt,label=code_simple,caption={\footnotesize code segment の軽量継続}] +__code cs0(int a, int b){ + goto cs1(a+b); +} + +__code cs1(int c){ + goto cs2(c); +} +\end{lstlisting} + +\begin{figure}[htpb] + \begin{center} + \scalebox{0.55}{\includegraphics{fig/codesegment.pdf}} + \end{center} + \caption{code segment の軽量継続} + \label{fig:code_simple} +\end{figure} + -Continuation based C (以下CbC)は当研究室で開発しているプログラミング言語である。 -CbC は殆どC言語と同じ構文を持っているが、C言語よりアセンブラに近い記述をすることで細 -かい動作を -CodeSegment、 DataSegment という単位を使いプログラムを記述する。 +\begin{lstlisting}[frame=lrbt,label=factorial,caption={\footnotesize 階乗を求め +る CbC プログラムの例}] +__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); + } + +} -\section{CodeSegmentとDataSegment} -%% CodeSegmentとはなにか？どのようなものか？くらいかけばよしかな -CodeSegmentは処理の単位である。入力を受け取り、処理を行い出力を行う。 +__code factorial(int x) +{ + goto factorial0(1, x); +} + +int main(int argc, char **argv) +{ + int i; + i = atoi(argv[1]); + + goto factorial(i); +} +\end{lstlisting} + +\begin{figure}[htpb] + \begin{center} + \scalebox{0.55}{\includegraphics{fig/factorial.pdf}} + \end{center} + \caption{階乗を求める CbC プログラムの軽量継続図} + \label{fig:factorial} +\end{figure} + +% \section{環境付き継続} +% \label{sec:withEnv} +% 環境付き継続の話いれる。。。？ - -% \section{DataSegment} -%% DataSegmentとはなにか？どのようなものか -DataSegmentはCodeSegmentで扱うデータの単位であり、処理に必要なデータがすべて入っている。 - -\section{CbC上でのCodeSegment、DataSegmentの表現} %% 例題 -%% CbCの具体的なコード類。どういう風に書くのか〜くらい +\section{CbC での CodeSegment と DataSegment の表現} %% 例題 +%% CbCの具体的なコード類。どういう風に書くのか〜？ %% Metaな話は今書いてもどうせ使わないので検証に使える〜くらいで置いておく。Meta %% 部分は生成でき、そこで検証用の動作をする感じでは？hora理論使ったりするといい %% かんじにできるんじゃないかな +% 流れ CbCではどうやってCodeSegmentつかうの？他との違いは？軽量継続って何？ルー +% プ処理とかってどうするの？ Metaってなに？なるほど？ってかんじ + +CbC 上で CodeSegment を定義するためには、C言語の関数を定義する構文の返り値の型部 +分に \_\_code キーワードを指定する。その際、Input DataSegment は関数の引数として定義される。 +次の CodeSegment をの実行には goto キーワードの後に CodeSegment 名と Input +DataSegment を指定する必要がある。 + +Scheme などの call/cc といった継続はトップレベルから現在までの位置を環境として保持する。 +これを通常の継続とする。環境とは関数を呼び出している際のスタックの状態である。 +CbC では通常の継続とは異なり、呼び出し元の情報を持たず、スタックを破棄しながら処 +理を続けていく。この継続は軽量継続と呼ばれる。 +% よって、リスト のプログラムでは cs0 から cs1 へと継続した後には +% cs0 へ戻らずに処理を続ける。 + +軽量継続時には関数呼び出しのスタックは存在しないが、計算中の値を DataSegment で +スタックを持つことで再帰を含むループ処理を行なうことも可能である。 +% meta とか stub とかはmirさんの論文から持ってこようよ +% 見てみたけどattonさん以外はGearsのとこにmetaのお話入ってるからどうしたものか。。。 + +% \section{MetaCodeSegment と MetaDataSegment} +% プログラムを記述する際、本来行いたい処理の他に記述しなければならないメタレベルの処理が存在し +% ている。例えば、メモリ管理、並列処理、エラーハンドリングなどの処理がこれにあたり、これ +% らをメタ計算と呼ぶ。% 自己反映計算〜とかリフレクション〜っていいたい気もする +% CodeSegment と DataSegment を用いたプログラミングでは通常の処理とメタレベルの処 +% 理を分離して記述する。 +% 通常の処理と比べてメタレベルの処理は高度なものが多く、通常メタレベルの処理はライブラ +% リや OS 側が提供している。そのため、ユーザー側は通常メタレベルの処理を触ることが +% できない。CbCでは通常の処理を書いているプログラムにメタレベルの処理を追 +% 加することができる。また、通常の処理からメタレベルの処理は遮蔽されているため、通 +% 常の処理を弄ることなくメタレベルの処理を切り替えることもできる。 +% CbC ではメタレベルの処理を行う CodeSegment のことを Meta CodeSegmentと呼び、メタ +% レベルの処理に必要な DataSegment を Meta DataSegment と呼ぶ。Meta CodeSegment は通 +% 常の CodeSegment の前に + diff -r 46d543c569d2 -r 0035f6d4826f final_main/chapter3.tex --- a/final_main/chapter3.tex Thu Jan 25 17:00:42 2018 +0900 +++ b/final_main/chapter3.tex Thu Feb 01 01:14:30 2018 +0900 @@ -1,7 +1,191 @@ -\chapter{Agda} +\chapter{定理証明支援系 Agda} + +型システムは Curry-Howard 同型対応により命題と型付きラムダ計算が一対一で対応する。 +依存型という表現力の高い型を持つ証明支援系 Agda を用いて型システムで証明が行える +ことを示す。 + +%% ここではAgdaの文法に触るだけにとどめて Agdaと証明のchapを一つ追加。 +% 其処に自然証明とAgdaの証明とかCurry-Howard対応の話とかを入れるときれいになるか +% も + +\section{Agda の文法} + +型システムを用いて証明を行うことができる言語として Agda が存在する。 Agda は依存 +型という型システムを持つ。依存型とは型も第一級オブジェクトとする型システム +で、依存型を持っている言語では型を基本的な操作に制限なしに使用できる。 +%% 依存型を持っている言語には Agda の他に ATS 、 Coq 、 F* 、 Idris 、 Shen など +%% がある。 + +Agda はインデントに意味を持つため、きちんと揃える必要がある。 +また、スペースの有無は厳格にチェックされる。 +なお、 \verb/--/ の後はコメントである。 + +Agda のプログラムでは全てモジュール内部に記述されるため、まずはトップレベルにモ +ジュールを定義する必要がある。トップレベルのモジュールはファイル名と同一になる。 + +通常のモジュールをインポートする時は \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/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} -\section{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/{}/ でくくることで表す。 -型システムを用いて証明を行うことができる言語として Agda が存在する。 +例えば、\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} + diff -r 46d543c569d2 -r 0035f6d4826f final_main/chapter4.tex --- a/final_main/chapter4.tex Thu Jan 25 17:00:42 2018 +0900 +++ b/final_main/chapter4.tex Thu Feb 01 01:14:30 2018 +0900 @@ -1,5 +1,298 @@ -\chapter{CbCとAgda} +%% Natural Deduction の説明をして、 Agda が命題を証明することができることを示す +%% 章? 要る。。。かどうかは微妙な気がする。 「こういう話で Agda では証明ができます。」 +%% で勝手に証明して証明できたね！はありだけど読み手があんまり嬉しくないかも。 +%% ソレだとやっぱり自然演繹の話しして~同型対応でちゃんとつながってるね~じゃあ +%% Agda で表現できるし証明できるねでいい感じかも + +\chapter{定理証明支援器 Agda による証明手法} + +前章では Agda の文法について書いた。本章では Natural Deduction での証明とそれに +対応して実際に 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を証明したことを意味する。 +証明は木構造で表わされる。葉の命題は仮定であり、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} -\section{} -実装部分。 -Agdaでの実装とかAgdaでの証明とかその解説とか? +\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 と Agda} +ここでは、 Natural Deduction と型付き$ \lambda $ 計算の対応を定義する。 + +\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} + +ここでは例として ((A ならば B) かつ (B ならば C)) ならば (A ならば C) が成り立つという三段論法を証明をする。 + +この三段論法は自然演繹では次のような証明木になった。 + +\begin{figure}[htpb] + \begin{center} + \includegraphics{pic/modus-ponens.pdf} + \end{center} + \caption{自然演繹での三段論法の証明} + \label{fig:modus-ponens} +\end{figure} + + +この証明木に対応するAgdaによる証明は次のようになる。 + +\begin{lstlisting}[basicstyle=\ttfamily\footnotesize, frame=single] +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 でも自然演繹と同様の証明を記述し、証明することができた。 + diff -r 46d543c569d2 -r 0035f6d4826f final_main/chapter5.tex --- a/final_main/chapter5.tex Thu Jan 25 17:00:42 2018 +0900 +++ b/final_main/chapter5.tex Thu Feb 01 01:14:30 2018 +0900 @@ -1,13 +1,10 @@ -\chapter{Agdaでの証明} - -前章ではノーマルレベルでのAgdaが正しく動くことを示した。 - -本章では - -\section{自然演繹} - -\section{Agdaでの証明} +\chapter{Agda での継続の表現} +\section{Agda での継続} + +\section{Agda での Interface の実装} + +\section{} diff -r 46d543c569d2 -r 0035f6d4826f final_main/main.tex --- a/final_main/main.tex Thu Jan 25 17:00:42 2018 +0900 +++ b/final_main/main.tex Thu Feb 01 01:14:30 2018 +0900 @@ -1,38 +1,69 @@ \documentclass[a4j,12pt]{jreport} \usepackage[dvipdfmx]{graphicx} \usepackage{mythesis} +\usepackage{bussproofs} \usepackage{multirow} \usepackage{here} \usepackage{listings} +\usepackage{url} +\usepackage{cite} +\usepackage{listings} +\usepackage{amssymb} +\usepackage{amsmath} +\usepackage[utf8]{inputenc} + \lstset{ - language={C}, - basicstyle={\footnotesize\ttfamily}, - identifierstyle={\footnotesize}, - commentstyle={\footnotesize\itshape}, - keywordstyle={\footnotesize\bfseries}, - ndkeywordstyle={\footnotesize}, - stringstyle={\footnotesize\ttfamily}, - frame={tb}, + basicstyle={\ttfamily}, breaklines=true, columns=[l]{fullflexible}, + commentstyle={\ttfamily}, + escapechar={@}, + frame=single, + framerule=.5pt, + identifierstyle={\ttfamily}, + keepspaces=true, + keywordstyle={\ttfamily}, + language={}, + lineskip=-0.1zw, numbers=left, - xrightmargin=0zw, - xleftmargin=3zw, + numbersep=1em, numberstyle={\scriptsize}, stepnumber=1, - numbersep=1zw, - lineskip=-0.5ex + stringstyle={\ttfamily}, + tabsize=4, + xleftmargin=0zw, + xrightmargin=0zw, } + +% \lstset{ +% language={C}, +% basicstyle={\footnotesize\ttfamily}, +% identifierstyle={\footnotesize}, +% commentstyle={\footnotesize\itshape}, +% keywordstyle={\footnotesize\bfseries}, +% ndkeywordstyle={\footnotesize}, +% stringstyle={\footnotesize\ttfamily}, +% frame={tb}, +% breaklines=true, +% columns=[l]{fullflexible}, +% numbers=left, +% xrightmargin=0zw, +% xleftmargin=3zw, +% numberstyle={\scriptsize}, +% stepnumber=1, +% numbersep=1zw, +% lineskip=-0.5ex +% } \def\lstlistingname{リスト} \def\lstlistlistingname{リスト目次} \setlength{\itemsep}{-1zh} -\title{CbC 言語とプログラムの証明} +\title{Agda と継続を用いたプログラムの検証} \icon{ \includegraphics[width=80mm,bb=0 0 595 642]{fig/ryukyu.pdf} %%元は 642じゃなくて842 } \year{平成30年度 卒業論文} \belongto{琉球大学工学部情報工学科} -\author{145750B 外間 \\ 指導教員 {河野 真治} } +\author{145750B 外間 政尊 \\ 指導教員 {河野 真治} } %% %% プリアンブルに記述 %% Figure 環境中で Table 環境の見出しを表示・カウンタの操作に必要 @@ -80,6 +111,10 @@ \input{chapter6.tex} % 参考文献 + +% \bibliographystyle{junsrt} +% \bibliography{reference} + \input{bibliography.tex} % 謝辞 diff -r 46d543c569d2 -r 0035f6d4826f thesis.mm --- a/thesis.mm Thu Jan 25 17:00:42 2018 +0900 +++ b/thesis.mm Thu Feb 01 01:14:30 2018 +0900 @@ -1,14 +1,14 @@ - + - + @@ -16,33 +16,36 @@ + - - - - - - - + + + + + + + + + - + - + - + - + @@ -51,13 +54,39 @@ - - - - - - - + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + +