Mercurial > hg > Papers > 2018 > nozomi-master
annotate paper/agda.tex @ 85:9d154c48a1f6
Update curry-howard isomorphism
| author | atton <atton@cr.ie.u-ryukyu.ac.jp> |
|---|---|
| date | Thu, 09 Feb 2017 15:36:52 +0900 |
| parents | c0199291c58e |
| children | e437746d6038 |
| rev | line source |
|---|---|
| 49 | 1 \chapter{証明支援系言語 Agda による証明手法} |
| 2 \label{chapter:agda} | |
|
83
c0199291c58e
Add simple/sub type description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
80
diff
changeset
|
3 \ref{chapter:type}章ではCbCにおける CodeSegment と DataSegment が部分型で定義できることを示した。 |
| 78 | 4 |
| 5 型システムは Curry-Howard 同型対応により命題と型付きラムダ計算が一対一に対応する。 | |
| 6 依存型という型を持つ証明支援系言語 Agda を用いて型システムで証明が行なえることを示す。 | |
| 7 | |
| 80 | 8 % {{{ 依存型を持つ証明支援系言語 Agda |
| 9 | |
| 10 \section{依存型を持つ証明支援系言語 Agda} | |
| 11 型システムを用いて証明を行なうことができる言語に Agda~\cite{agda} が存在する。 | |
| 12 Agda は依存型という強力な型システムを持っている。 | |
| 13 依存型とは型も第一級オブジェクトとする型システムであり、型の型や型を引数に取る関数、値を取って型を返す関数などが記述できる。 | |
| 14 この節では Agda の文法的な紹介を行なう~\cite{Norell:2009:DTP:1481861.1481862}~\cite{agda-documentation}。 | |
| 15 | |
| 16 Agda はインデントに意味を持つ言語であるため、インデントはきちんと揃える必要がある。 | |
| 17 また、非常に多くの記号を利用できる言語であり、スペースの有無は厳格にチェックされる。 | |
| 18 なお、 \verb/--/ の後はコメントである。 | |
| 19 | |
| 20 まず、Agda のプログラムを記述するファイルを作成する。 | |
| 21 Agda のプログラムは全てモジュール内部に記述されるため、まずはトップレベルにモジュールを定義する必要がある。 | |
| 22 トップレベルのモジュールはファイル名と同一となる。 | |
| 23 例えば \verb/AgdaBasics.agda/ を作成する時のモジュール名はリスト~\ref{src:agda-module}のように定義する。 | |
| 24 | |
| 25 \lstinputlisting[label=src:agda-module, caption=Agdaのモジュールの定義する] {src/AgdaBasics.agda} | |
| 26 | |
| 27 Agda における型指定は $:$ を用いて行なう。 | |
| 28 例えば、変数xが型Aを持つ、ということを表すには \verb/x : A/ と記述する。 | |
| 29 | |
| 30 データ型は Haskell や ML に似た代数的なデータ構造である。 | |
| 31 データ型の定義は \verb/data/ キーワードを用いる。 | |
| 32 \verb/data/キーワードの後に \verb/where/ 句を書きインデントを深くした後、値にコンストラクタとその型を列挙する。 | |
| 33 例えば Bool 型を定義するとリスト~\ref{src:agda-bool}のようになる。 | |
| 34 Bool はコンストラクタ \verb/true/ か \verb/false/ を持つデータ型である。 | |
| 35 Bool 自身の型は \verb/Set/ であり、これは Agda が組み込みで持つ「型の型」である。 | |
| 36 Set は階層構造を持ち、型の型の型を指定するには Set1 と書く。 | |
| 37 | |
| 38 \lstinputlisting[label=src:agda-bool, caption=Agdaにおけるデータ型 Bool の定義] {src/AgdaBool.agda} | |
| 39 | |
| 40 | |
| 41 関数の定義は Haskell に近い。 | |
| 42 関数名と型を記述した後に関数の本体を \verb/=/ の後に指定する。 | |
| 43 関数の型は $ \rightarrow $ を用いる。 | |
| 44 なお、$\rightarrow$に対しては糖衣構文 \verb/->/ も用意されている。 | |
| 45 例えば引数が型 \verb/A/ で返り値が型 \verb/B/ の関数は \verb/A -> B/ のように書ける。 | |
| 46 Bool 変数 \verb/x/ を取って true を返す関数 \verb/f/はリスト~\ref{src:agda-function}のようになる。 | |
| 47 | |
| 48 \lstinputlisting[label=src/agda-function, caption=Agda における関数定義] {src/AgdaFunction.agda} | |
| 49 | |
| 50 引数は変数名で受けることもできるが、具体的なコンストラクタを指定することでそのコンストラクタが渡された時の挙動を定義できる。 | |
| 51 これはパターンマッチと呼ばれ、コンストラクタで case 文を行なっているようなものである。 | |
| 52 例えば Bool 型の値を反転する \verb/not/ 関数を書くとリスト~\ref{src:agda-not}のようになる。 | |
| 53 | |
| 54 \lstinputlisting[label=src:agda-not, caption=Agdaにおける関数 not の定義] {src/AgdaNot.agda} | |
| 55 | |
| 56 パターンマッチは全てのコンストラクタのパターンを含まなくてはならない。 | |
| 57 例えば、Bool 型を受け取る関数で \verb/true/ の時の挙動のみを書くことはできない。 | |
| 58 なお、コンストラクタをいくつか指定した後に変数で受けると、変数が持ちうる値は指定した以外のコンストラクタとなる。 | |
| 59 例えばリスト~\ref{src:agda-pattern}の not は x には true しか入ることは無い。 | |
| 60 なお、マッチした値を変数として利用しない場合は \verb/_/ を用いて捨てることもできる。 | |
| 61 | |
| 62 \lstinputlisting[label=src:agda-pattern, caption=Agdaにおけるパターンマッチ] {src/AgdaPattern.agda} | |
| 63 | |
| 64 関数にはリテラルが存在し、関数名を定義せずともその場で生成することができる。 | |
| 65 これをラムダ式と呼び、\verb/\arg1 arg2 -> function body/ のように書く。 | |
| 66 例えば Bool 型の引数 \verb/b/ を取って not を適用する \verb/not-apply/ をラムダ式で書くとリスト~\ref{src:agda-lambda}のようになる。 | |
| 67 関数 \verb/not-apply/ をラムダ式を使わずに定義すると \verb/not-apply-2/ になるが、この二つの関数は同一の動作をする。 | |
| 68 | |
| 69 \lstinputlisting[label=src:agda-lambda, caption=Agda におけるラムダ式] {src/AgdaLambda.agda} | |
| 70 | |
| 71 Agda では特定の関数内のみで利用する関数を \verb/where/ 句で記述できる。 | |
| 72 これは関数内部の冗長な記述を省略するのに活用できる。 | |
| 73 スコープは \verb/where/句が存在する関数内部のみであるため、名前空間が汚染させることも無い。 | |
| 74 例えば自然数3つを取ってそれぞれ3倍して加算する関数 \verb/f/ を定義するとき、 \verb/where/ を使うとリスト~\ref{src:agda-where} のように書ける。 | |
| 75 これは \verb/f'/ と同様の動作をする。 | |
| 76 \verb/where/ 句は利用したい関数の末尾にインデント付きで \verb/where/ キーワードを記述し、改行の後インデントをして関数内部で利用する関数を定義する。 | |
| 77 | |
| 78 \lstinputlisting[label=src:agda-where, caption=Agda における where 句] {src/AgdaWhere.agda} | |
| 79 | |
| 80 | |
| 81 データ型のコンストラクタには自分自身の型を引数に取ることもできる(リスト~\ref{src:agda-nat})。 | |
| 82 自然数のコンストラクタは2つあり、片方は自然数ゼロ、片方は自然数を取って後続数を返すものである。 | |
| 83 例えば0 は \verb/zero/ であり、1 は \verb/suc zero/に、3は \verb/suc (suc (suc zero))/ に対応する。 | |
| 84 | |
| 85 \lstinputlisting[label=src:agda-nat, caption=Agdaにおける自然数の定義] {src/AgdaNat.agda} | |
| 86 | |
| 87 自然数に対する演算は再帰関数として定義できる。 | |
| 88 例えば自然数どうしの加算は二項演算子\verb/+/としてリスト~\ref{src:agda-plus}のように書ける。 | |
| 89 | |
| 90 この二項演算子は正確には中置関数である。 | |
| 91 前置や後置で定義できる部分を関数名に \verb/_/ として埋め込んでおくことで、関数を呼ぶ時にあたかも前置や後置演算子のように振る舞う。 | |
| 92 例えば \verb/!_/ 関数を定義すると \verb/! true/ のように利用でき、\verb/_~/ 関数を定義すると \verb/false ~/ のように利用できる。 | |
| 93 | |
| 94 また、Agda は再帰関数が停止するかを判定できる。 | |
| 95 この加算の二項演算子は左側がゼロに対しては明らかに停止する。 | |
| 96 左側が1以上の時の再帰時には \verb/suc n/ から \verb/n/へと減っているため、再帰で繰り返し減らすことでいつかは停止する。 | |
| 97 もし \verb/suc n/ のまま自分自身へと再帰した場合、Agda は警告を出す。 | |
| 98 | |
| 99 \lstinputlisting[label=src:agda-plus, caption=Agda における自然数の加算の定義] {src/AgdaPlus.agda} | |
| 100 | |
| 101 次に依存型について見ていく。 | |
| 102 依存型で最も基本的なものは関数型である。 | |
| 103 依存型を利用した関数は引数の型に依存して返す型を決定できる。 | |
| 104 | |
| 105 Agda で \verb/(x : A) -> B/ と書くと関数は型 A を持つx を受け取り、Bを返す。 | |
| 106 ここで B の中で x を扱っても良い。 | |
| 107 例えば任意の型に対する恒等関数はリスト~\ref{src:agda-id}のように書ける。 | |
| 108 | |
| 109 \lstinputlisting[label=src:agda-id, caption=依存型を持つ関数の定義] {src/AgdaId.agda} | |
| 110 | |
| 111 この恒等関数 \verb/identitiy/ は任意の型に適用可能である。 | |
| 112 実際に関数 \verb/identitiy/ を Nat へ適用した例が \verb/identitiy-zero/ である。 | |
| 113 | |
| 114 多相の恒等関数では型を明示的に指定せずとも \verb/zero/ に適用した場合の型は自明に \verb/Nat -> Nat/である。 | |
| 115 Agda はこのような推論をサポートしており、推論可能な引数は省略できる。 | |
| 116 推論によって解決される引数を暗黙的な引数(implicit arguments) と言い、記号 \verb/{}/ でくくる。 | |
| 117 | |
| 118 例えば、\verb/identitiy/ の対象とする型\verb/A/を暗黙的な引数として省略するとリスト~\ref{src:agda-implicit-id}のようになる。 | |
| 119 この恒等関数を利用する際は特定の型に属する値を渡すだけでその型が自動的に推論される。 | |
| 120 よって関数を利用する際は \verb/id-zero/ のように型を省略して良い。 | |
| 121 なお、関数の本体で暗黙的な引数を利用したい場合は \verb/{variableName}/ で束縛することもできる(\verb/id'/ 関数)。 | |
| 122 適用する場合も \verb/{}/でくくり、\verb/id-true/のように使用する。 | |
| 123 | |
| 124 \lstinputlisting[label=src:agda-implicit-id, caption=Agdaにおける暗黙的な引数を持つ関数] {src/AgdaImplicitId.agda} | |
| 125 | |
| 126 Agda には C における構造体に相当するレコード型も存在する。 | |
| 127 定義を行なう際は \verb/record/キーワードの後にレコード名、型、\verb/where/ の後に \verb/field/ キーワードを入れた後、フィールド名と型名を列挙する。 | |
| 128 例えば x と y の二つの自然数からなるレコード \verb/Point/ を定義するとリスト~\ref{src:agda-record}のようになる。 | |
| 129 レコードを構築する際は \verb/record/ キーワードの後の \verb/{}/ の内部に \verb/fieldName = value/ の形で値を列挙していく。 | |
| 130 複数の値を列挙する際は \verb/;/ で区切る。 | |
| 131 | |
| 132 \lstinputlisting[label=src:agda-record, caption=Agdaにおけるレコード型の定義] {src/AgdaRecord.agda} | |
| 133 | |
| 134 構築されたレコードから値を取得する際には \verb/RecordName.fieldName/ という名前の関数を適用する(リスト~\ref{src:agda-record-proj} 内2行目) 。 | |
| 135 なお、レコードにもパターンマッチが利用できる(リスト~\ref{src:agda-record-proj} 内5行目)。 | |
| 136 また、値を更新する際は \verb/record oldRecord {field = value ; ... }/ という構文を利用する。 | |
| 137 Point の中の x の値を5増やす関数 \verb/xPlus5/ はリスト~\ref{src:agda-record-proj}の 7,8行目のように書ける。 | |
| 138 | |
| 139 \lstinputlisting[label=src:agda-record-proj, caption=Agda におけるレコードの射影、パターンマッチ、値の更新] {src/AgdaRecordProj.agda} | |
| 140 | |
| 141 Agda における部分型のように振る舞う機能として Instance Arguments が存在する。 | |
| 142 これはとあるデータ型が、ある型と名前を持つ関数を持つことを保証する機能であり、Haskell における型クラスや Java におけるインターフェースに相当する。 | |
| 143 Agda における部分型の制約は、必要な関数を定義した record に相当し、その制約を保証するにはその record を instance として登録することになる。 | |
| 144 例えば、同じ型と比較することができる、という性質を表すとリスト~\ref{src:agda-type-class}のようになる。 | |
| 145 具体的にはとある型 A における中置関数 \verb/_==_/ を定義することに相当する。 | |
| 146 | |
| 147 \lstinputlisting[label=src:agda-type-class, caption=Agdaにおける部分型制約] {src/AgdaTypeClass.agda} | |
| 148 | |
| 149 ある型 T がこの部分型制約を満たすことを示すには、型 T でこのレコードを作成できることを示し、それを instance 構文で登録する。 | |
| 150 型Nat が Eq の上位型であることを記述するとリスト~\ref{src:agda-instance}のようになる。 | |
| 151 | |
| 152 \lstinputlisting[label=src:agda-instance, caption=Agdaにおける部分型関係の構築] {src/AgdaInstance.agda} | |
| 153 | |
| 154 これで \verb/Eq/ が要求される関数に対して Nat が適用できるようになる。 | |
| 155 例えば型 A の要素を持つ List A から要素を探してくる elem を定義する。 | |
| 156 部分型のインスタンスは \verb/{{}}/ 内部に名前と型名で記述する。 | |
| 157 なお、名前部分は必須である。 | |
| 158 仮に変数として受けても利用しない場合は \verb/_/ で捨てると良い。 | |
| 159 部分型として登録した record は関数本体において \verb/{{variableName}}/ という構文で変数に束縛できる。 | |
| 160 | |
| 161 \lstinputlisting[label=src:agda-use-instance, caption=Agdaにおける部分型を使う関数の定義] {src/AgdaElem.agda.replaced} | |
| 162 | |
| 163 この \verb/elem/ 関数はリスト~\ref{src:agda-elem-apply} のように利用できる。 | |
| 164 Nat型の要素を持つリストの内部に4が含まれるか確認している。 | |
| 165 この \verb/listHas4/ は \verb/true/ に評価される。 | |
| 166 | |
| 167 \lstinputlisting[label=src:agda-elem-apply, caption=部分型を持つ関数の適用] {src/AgdaElemApply.agda.replaced} | |
| 168 | |
| 169 最後にモジュールについて述べる。 | |
| 170 モジュールはほとんど名前空間として作用する。 | |
| 171 なお、依存型の解決はモジュールのインポート時に行なわれる。 | |
| 172 モジュールをインポートする時は \verb/import/ キーワードを指定する。 | |
| 173 また、インポートを行なう際に名前を別名に変更することもでき、その際は \verb/as/ キーワードを用いる。 | |
| 174 モジュールから特定の関数のみをインポートする場合は \verb/using/ キーワードを、関数の名前を変える時は \verb/renaming/キーワードを、特定の関数のみを隠す場合は \verb/hiding/ キーワードを用いる。 | |
| 175 なお、モジュールに存在する関数をトップレベルで用いる場合は \verb/open/ キーワードを使うことで展開できる。 | |
| 176 モジュールをインポートする例をリスト~\ref{src:agda-import}に示す。 | |
| 177 | |
| 178 \lstinputlisting[label=src:agda-import, caption=Agdaにおけるモジュールのインポート] {src/AgdaImport.agda} | |
| 179 | |
| 180 また、モジュールには値を渡すことができる。 | |
| 181 そのようなモジュールは Parameterized Module と呼ばれ、渡された値はそのモジュール内部で一貫して扱える。 | |
| 182 例えば要素の型と比較する二項演算子を使って並べ替えをするモジュール\verb/Sort/ を考える。 | |
| 183 そのモジュールは引数に型Aと二項演算子 \verb/</を取り、ソートする関数を提供する。 | |
| 184 \verb/Sort/モジュールを \verb/Nat/ と \verb/Bool/ で利用した例がリスト~\ref{src:agda-parameterized-module}である。 | |
| 185 | |
| 186 \lstinputlisting[label=src:agda-parameterized-module, caption=Agda における Parameterized Module] {src/AgdaParameterizedModule.agda} | |
| 187 | |
| 188 % }}} | |
| 189 | |
|
50
451c510825de
Add natural deduction and curry-howard isomorphism
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
49
diff
changeset
|
190 % {{{ Natural Deduction |
| 49 | 191 \section{Natural Deduction} |
| 55 | 192 \label{section:natural_deduction} |
|
50
451c510825de
Add natural deduction and curry-howard isomorphism
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
49
diff
changeset
|
193 まず始めに証明を行なうためにNatural Deduction(自然演繹)を示す。 |
|
451c510825de
Add natural deduction and curry-howard isomorphism
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
49
diff
changeset
|
194 |
|
64
10a550bf7e4a
Mini fixes with ryokka-san
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
55
diff
changeset
|
195 Natural Deduction は Gentzen によって作られた論理と、その証明システムである~\cite{Girard:1989:PT:64805}。 |
|
50
451c510825de
Add natural deduction and curry-howard isomorphism
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
49
diff
changeset
|
196 命題変数と記号を用いた論理式で論理を記述し、推論規則により変形することで求める論理式を導く。 |
|
451c510825de
Add natural deduction and curry-howard isomorphism
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
49
diff
changeset
|
197 |
|
451c510825de
Add natural deduction and curry-howard isomorphism
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
49
diff
changeset
|
198 natural deduction において |
|
451c510825de
Add natural deduction and curry-howard isomorphism
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
49
diff
changeset
|
199 |
|
451c510825de
Add natural deduction and curry-howard isomorphism
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
49
diff
changeset
|
200 \begin{eqnarray} |
|
451c510825de
Add natural deduction and curry-howard isomorphism
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
49
diff
changeset
|
201 \vdots \\ \nonumber |
|
451c510825de
Add natural deduction and curry-howard isomorphism
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
49
diff
changeset
|
202 A \\ \nonumber |
|
451c510825de
Add natural deduction and curry-howard isomorphism
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
49
diff
changeset
|
203 \end{eqnarray} |
|
451c510825de
Add natural deduction and curry-howard isomorphism
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
49
diff
changeset
|
204 |
|
451c510825de
Add natural deduction and curry-howard isomorphism
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
49
diff
changeset
|
205 と書いた時、最終的に命題Aを証明したことを意味する。 |
|
451c510825de
Add natural deduction and curry-howard isomorphism
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
49
diff
changeset
|
206 証明は木構造で表わされ、葉の命題は仮定となる。 |
|
451c510825de
Add natural deduction and curry-howard isomorphism
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
49
diff
changeset
|
207 仮定には dead か alive の2つの状態が存在する。 |
|
451c510825de
Add natural deduction and curry-howard isomorphism
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
49
diff
changeset
|
208 |
|
451c510825de
Add natural deduction and curry-howard isomorphism
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
49
diff
changeset
|
209 \begin{eqnarray} |
|
451c510825de
Add natural deduction and curry-howard isomorphism
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
49
diff
changeset
|
210 \label{exp:a_implies_b} |
|
451c510825de
Add natural deduction and curry-howard isomorphism
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
49
diff
changeset
|
211 A \\ \nonumber |
|
451c510825de
Add natural deduction and curry-howard isomorphism
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
49
diff
changeset
|
212 \vdots \\ \nonumber |
|
451c510825de
Add natural deduction and curry-howard isomorphism
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
49
diff
changeset
|
213 B \\ \nonumber |
|
451c510825de
Add natural deduction and curry-howard isomorphism
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
49
diff
changeset
|
214 \end{eqnarray} |
|
451c510825de
Add natural deduction and curry-howard isomorphism
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
49
diff
changeset
|
215 |
|
451c510825de
Add natural deduction and curry-howard isomorphism
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
49
diff
changeset
|
216 式\ref{exp:a_implies_b}のように A を仮定して B を導いたとする。 |
|
451c510825de
Add natural deduction and curry-howard isomorphism
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
49
diff
changeset
|
217 この時 A は alive な仮定であり、証明された B は A の仮定に依存していることを意味する。 |
|
451c510825de
Add natural deduction and curry-howard isomorphism
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
49
diff
changeset
|
218 |
|
451c510825de
Add natural deduction and curry-howard isomorphism
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
49
diff
changeset
|
219 ここで、推論規則により記号 $ \Rightarrow $ を導入する。 |
|
451c510825de
Add natural deduction and curry-howard isomorphism
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
49
diff
changeset
|
220 |
|
451c510825de
Add natural deduction and curry-howard isomorphism
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
49
diff
changeset
|
221 \begin{prooftree} |
|
451c510825de
Add natural deduction and curry-howard isomorphism
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
49
diff
changeset
|
222 \AxiomC{[$ A $]} |
|
451c510825de
Add natural deduction and curry-howard isomorphism
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
49
diff
changeset
|
223 \noLine |
|
451c510825de
Add natural deduction and curry-howard isomorphism
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
49
diff
changeset
|
224 \UnaryInfC{ $ \vdots $} |
|
451c510825de
Add natural deduction and curry-howard isomorphism
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
49
diff
changeset
|
225 \noLine |
|
451c510825de
Add natural deduction and curry-howard isomorphism
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
49
diff
changeset
|
226 \UnaryInfC{ $ B $ } |
|
451c510825de
Add natural deduction and curry-howard isomorphism
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
49
diff
changeset
|
227 \RightLabel{ $ \Rightarrow \mathcal{I} $} |
|
451c510825de
Add natural deduction and curry-howard isomorphism
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
49
diff
changeset
|
228 \UnaryInfC{$ A \Rightarrow B $} |
|
451c510825de
Add natural deduction and curry-howard isomorphism
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
49
diff
changeset
|
229 \end{prooftree} |
|
451c510825de
Add natural deduction and curry-howard isomorphism
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
49
diff
changeset
|
230 |
|
451c510825de
Add natural deduction and curry-howard isomorphism
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
49
diff
changeset
|
231 $ \Rightarrow \mathcal{I} $ を適用することで仮定 A は dead となり、新たな命題 $ A \Rightarrow B $ を導くことができる。 |
|
451c510825de
Add natural deduction and curry-howard isomorphism
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
49
diff
changeset
|
232 A という仮定に依存して B を導く証明から、「A が存在すれば B が存在する」という証明を導いたこととなる。 |
|
451c510825de
Add natural deduction and curry-howard isomorphism
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
49
diff
changeset
|
233 このように、仮定から始めて最終的に全ての仮定を dead とすることで、仮定に依存しない証明を導ける。 |
|
451c510825de
Add natural deduction and curry-howard isomorphism
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
49
diff
changeset
|
234 なお、dead な仮定は \verb/[A]/ のように \verb/[]/ で囲んで書く。 |
|
451c510825de
Add natural deduction and curry-howard isomorphism
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
49
diff
changeset
|
235 |
|
451c510825de
Add natural deduction and curry-howard isomorphism
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
49
diff
changeset
|
236 alive な仮定を dead にすることができるのは $ \Rightarrow \mathcal{I} $ 規則のみである。 |
|
451c510825de
Add natural deduction and curry-howard isomorphism
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
49
diff
changeset
|
237 それを踏まえ、 natural deduction には以下のような規則が存在する。 |
|
451c510825de
Add natural deduction and curry-howard isomorphism
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
49
diff
changeset
|
238 |
|
451c510825de
Add natural deduction and curry-howard isomorphism
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
49
diff
changeset
|
239 \begin{itemize} |
|
451c510825de
Add natural deduction and curry-howard isomorphism
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
49
diff
changeset
|
240 \item Hypothesis |
|
451c510825de
Add natural deduction and curry-howard isomorphism
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
49
diff
changeset
|
241 |
|
451c510825de
Add natural deduction and curry-howard isomorphism
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
49
diff
changeset
|
242 仮定。葉にある式が仮定となるため、論理式A を仮定する場合に以下のように書く。 |
|
451c510825de
Add natural deduction and curry-howard isomorphism
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
49
diff
changeset
|
243 |
|
451c510825de
Add natural deduction and curry-howard isomorphism
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
49
diff
changeset
|
244 $ A $ |
|
451c510825de
Add natural deduction and curry-howard isomorphism
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
49
diff
changeset
|
245 |
|
451c510825de
Add natural deduction and curry-howard isomorphism
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
49
diff
changeset
|
246 \item Introductions |
|
451c510825de
Add natural deduction and curry-howard isomorphism
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
49
diff
changeset
|
247 |
|
451c510825de
Add natural deduction and curry-howard isomorphism
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
49
diff
changeset
|
248 導入。証明された論理式に対して記号を導入することで新たな証明を導く。 |
|
451c510825de
Add natural deduction and curry-howard isomorphism
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
49
diff
changeset
|
249 |
|
451c510825de
Add natural deduction and curry-howard isomorphism
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
49
diff
changeset
|
250 |
|
451c510825de
Add natural deduction and curry-howard isomorphism
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
49
diff
changeset
|
251 \begin{prooftree} |
|
451c510825de
Add natural deduction and curry-howard isomorphism
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
49
diff
changeset
|
252 \AxiomC{ $ \vdots $} |
|
451c510825de
Add natural deduction and curry-howard isomorphism
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
49
diff
changeset
|
253 \noLine |
|
451c510825de
Add natural deduction and curry-howard isomorphism
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
49
diff
changeset
|
254 \UnaryInfC{ $ A $ } |
|
451c510825de
Add natural deduction and curry-howard isomorphism
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
49
diff
changeset
|
255 \AxiomC{ $ \vdots $} |
|
451c510825de
Add natural deduction and curry-howard isomorphism
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
49
diff
changeset
|
256 \noLine |
|
451c510825de
Add natural deduction and curry-howard isomorphism
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
49
diff
changeset
|
257 \UnaryInfC{ $ B $ } |
|
451c510825de
Add natural deduction and curry-howard isomorphism
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
49
diff
changeset
|
258 \RightLabel{ $ \land \mathcal{I} $} |
|
451c510825de
Add natural deduction and curry-howard isomorphism
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
49
diff
changeset
|
259 \BinaryInfC{$ A \land B $} |
|
451c510825de
Add natural deduction and curry-howard isomorphism
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
49
diff
changeset
|
260 \end{prooftree} |
|
451c510825de
Add natural deduction and curry-howard isomorphism
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
49
diff
changeset
|
261 |
|
451c510825de
Add natural deduction and curry-howard isomorphism
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
49
diff
changeset
|
262 \begin{prooftree} |
|
451c510825de
Add natural deduction and curry-howard isomorphism
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
49
diff
changeset
|
263 \AxiomC{ $ \vdots $} |
|
451c510825de
Add natural deduction and curry-howard isomorphism
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
49
diff
changeset
|
264 \noLine |
|
451c510825de
Add natural deduction and curry-howard isomorphism
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
49
diff
changeset
|
265 \UnaryInfC{ $ A $ } |
|
451c510825de
Add natural deduction and curry-howard isomorphism
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
49
diff
changeset
|
266 \RightLabel{ $ \lor 1 \mathcal{I} $} |
|
451c510825de
Add natural deduction and curry-howard isomorphism
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
49
diff
changeset
|
267 \UnaryInfC{$ A \lor B $} |
|
451c510825de
Add natural deduction and curry-howard isomorphism
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
49
diff
changeset
|
268 \end{prooftree} |
|
451c510825de
Add natural deduction and curry-howard isomorphism
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
49
diff
changeset
|
269 |
|
451c510825de
Add natural deduction and curry-howard isomorphism
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
49
diff
changeset
|
270 \begin{prooftree} |
|
451c510825de
Add natural deduction and curry-howard isomorphism
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
49
diff
changeset
|
271 \AxiomC{ $ \vdots $} |
|
451c510825de
Add natural deduction and curry-howard isomorphism
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
49
diff
changeset
|
272 \noLine |
|
451c510825de
Add natural deduction and curry-howard isomorphism
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
49
diff
changeset
|
273 \UnaryInfC{ $ B $ } |
|
451c510825de
Add natural deduction and curry-howard isomorphism
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
49
diff
changeset
|
274 \RightLabel{ $ \lor 2 \mathcal{I} $} |
|
451c510825de
Add natural deduction and curry-howard isomorphism
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
49
diff
changeset
|
275 \UnaryInfC{$ A \lor B $} |
|
451c510825de
Add natural deduction and curry-howard isomorphism
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
49
diff
changeset
|
276 \end{prooftree} |
|
451c510825de
Add natural deduction and curry-howard isomorphism
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
49
diff
changeset
|
277 |
|
451c510825de
Add natural deduction and curry-howard isomorphism
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
49
diff
changeset
|
278 \begin{prooftree} |
|
451c510825de
Add natural deduction and curry-howard isomorphism
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
49
diff
changeset
|
279 \AxiomC{[$ A $]} |
|
451c510825de
Add natural deduction and curry-howard isomorphism
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
49
diff
changeset
|
280 \noLine |
|
451c510825de
Add natural deduction and curry-howard isomorphism
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
49
diff
changeset
|
281 \UnaryInfC{ $ \vdots $} |
|
451c510825de
Add natural deduction and curry-howard isomorphism
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
49
diff
changeset
|
282 \noLine |
|
451c510825de
Add natural deduction and curry-howard isomorphism
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
49
diff
changeset
|
283 \UnaryInfC{ $ B $ } |
|
451c510825de
Add natural deduction and curry-howard isomorphism
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
49
diff
changeset
|
284 \RightLabel{ $ \Rightarrow \mathcal{I} $} |
|
451c510825de
Add natural deduction and curry-howard isomorphism
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
49
diff
changeset
|
285 \UnaryInfC{$ A \Rightarrow B $} |
|
451c510825de
Add natural deduction and curry-howard isomorphism
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
49
diff
changeset
|
286 \end{prooftree} |
|
451c510825de
Add natural deduction and curry-howard isomorphism
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
49
diff
changeset
|
287 |
|
451c510825de
Add natural deduction and curry-howard isomorphism
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
49
diff
changeset
|
288 \item Eliminations |
|
451c510825de
Add natural deduction and curry-howard isomorphism
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
49
diff
changeset
|
289 |
|
451c510825de
Add natural deduction and curry-howard isomorphism
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
49
diff
changeset
|
290 除去。ある論理記号で構成された証明から別の証明を導く。 |
|
451c510825de
Add natural deduction and curry-howard isomorphism
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
49
diff
changeset
|
291 |
|
451c510825de
Add natural deduction and curry-howard isomorphism
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
49
diff
changeset
|
292 \begin{prooftree} |
|
451c510825de
Add natural deduction and curry-howard isomorphism
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
49
diff
changeset
|
293 \AxiomC{ $ \vdots $} |
|
451c510825de
Add natural deduction and curry-howard isomorphism
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
49
diff
changeset
|
294 \noLine |
|
451c510825de
Add natural deduction and curry-howard isomorphism
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
49
diff
changeset
|
295 \UnaryInfC{ $ A \land B $ } |
|
451c510825de
Add natural deduction and curry-howard isomorphism
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
49
diff
changeset
|
296 \RightLabel{ $ \land 1 \mathcal{E} $} |
|
451c510825de
Add natural deduction and curry-howard isomorphism
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
49
diff
changeset
|
297 \UnaryInfC{$ A $} |
|
451c510825de
Add natural deduction and curry-howard isomorphism
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
49
diff
changeset
|
298 \end{prooftree} |
|
451c510825de
Add natural deduction and curry-howard isomorphism
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
49
diff
changeset
|
299 |
|
451c510825de
Add natural deduction and curry-howard isomorphism
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
49
diff
changeset
|
300 \begin{prooftree} |
|
451c510825de
Add natural deduction and curry-howard isomorphism
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
49
diff
changeset
|
301 \AxiomC{ $ \vdots $} |
|
451c510825de
Add natural deduction and curry-howard isomorphism
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
49
diff
changeset
|
302 \noLine |
|
451c510825de
Add natural deduction and curry-howard isomorphism
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
49
diff
changeset
|
303 \UnaryInfC{ $ A \land B $ } |
|
451c510825de
Add natural deduction and curry-howard isomorphism
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
49
diff
changeset
|
304 \RightLabel{ $ \land 2 \mathcal{E} $} |
|
451c510825de
Add natural deduction and curry-howard isomorphism
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
49
diff
changeset
|
305 \UnaryInfC{$ B $} |
|
451c510825de
Add natural deduction and curry-howard isomorphism
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
49
diff
changeset
|
306 \end{prooftree} |
|
451c510825de
Add natural deduction and curry-howard isomorphism
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
49
diff
changeset
|
307 |
|
451c510825de
Add natural deduction and curry-howard isomorphism
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
49
diff
changeset
|
308 \begin{prooftree} |
|
451c510825de
Add natural deduction and curry-howard isomorphism
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
49
diff
changeset
|
309 \AxiomC{ $ \vdots $} |
|
451c510825de
Add natural deduction and curry-howard isomorphism
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
49
diff
changeset
|
310 \noLine |
|
451c510825de
Add natural deduction and curry-howard isomorphism
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
49
diff
changeset
|
311 \UnaryInfC{ $ A \lor B $ } |
|
451c510825de
Add natural deduction and curry-howard isomorphism
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
49
diff
changeset
|
312 |
|
451c510825de
Add natural deduction and curry-howard isomorphism
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
49
diff
changeset
|
313 \AxiomC{[$A$]} |
|
451c510825de
Add natural deduction and curry-howard isomorphism
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
49
diff
changeset
|
314 \noLine |
|
451c510825de
Add natural deduction and curry-howard isomorphism
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
49
diff
changeset
|
315 \UnaryInfC{ $ \vdots $} |
|
451c510825de
Add natural deduction and curry-howard isomorphism
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
49
diff
changeset
|
316 \noLine |
|
451c510825de
Add natural deduction and curry-howard isomorphism
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
49
diff
changeset
|
317 \UnaryInfC{ $ C $ } |
|
451c510825de
Add natural deduction and curry-howard isomorphism
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
49
diff
changeset
|
318 |
|
451c510825de
Add natural deduction and curry-howard isomorphism
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
49
diff
changeset
|
319 \AxiomC{[$B$]} |
|
451c510825de
Add natural deduction and curry-howard isomorphism
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
49
diff
changeset
|
320 \noLine |
|
451c510825de
Add natural deduction and curry-howard isomorphism
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
49
diff
changeset
|
321 \UnaryInfC{ $ \vdots $} |
|
451c510825de
Add natural deduction and curry-howard isomorphism
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
49
diff
changeset
|
322 \noLine |
|
451c510825de
Add natural deduction and curry-howard isomorphism
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
49
diff
changeset
|
323 \UnaryInfC{ $ C $ } |
|
451c510825de
Add natural deduction and curry-howard isomorphism
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
49
diff
changeset
|
324 |
|
451c510825de
Add natural deduction and curry-howard isomorphism
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
49
diff
changeset
|
325 \RightLabel{ $ \lor \mathcal{E} $} |
|
451c510825de
Add natural deduction and curry-howard isomorphism
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
49
diff
changeset
|
326 \TrinaryInfC{ $ C $ } |
|
451c510825de
Add natural deduction and curry-howard isomorphism
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
49
diff
changeset
|
327 \end{prooftree} |
|
451c510825de
Add natural deduction and curry-howard isomorphism
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
49
diff
changeset
|
328 |
|
451c510825de
Add natural deduction and curry-howard isomorphism
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
49
diff
changeset
|
329 \begin{prooftree} |
|
451c510825de
Add natural deduction and curry-howard isomorphism
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
49
diff
changeset
|
330 \AxiomC{ $ \vdots $} |
|
451c510825de
Add natural deduction and curry-howard isomorphism
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
49
diff
changeset
|
331 \noLine |
|
451c510825de
Add natural deduction and curry-howard isomorphism
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
49
diff
changeset
|
332 \UnaryInfC{ $ A $ } |
|
451c510825de
Add natural deduction and curry-howard isomorphism
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
49
diff
changeset
|
333 |
|
451c510825de
Add natural deduction and curry-howard isomorphism
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
49
diff
changeset
|
334 \AxiomC{ $ \vdots $} |
|
451c510825de
Add natural deduction and curry-howard isomorphism
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
49
diff
changeset
|
335 \noLine |
|
451c510825de
Add natural deduction and curry-howard isomorphism
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
49
diff
changeset
|
336 \UnaryInfC{ $ A \Rightarrow B $ } |
|
451c510825de
Add natural deduction and curry-howard isomorphism
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
49
diff
changeset
|
337 |
|
451c510825de
Add natural deduction and curry-howard isomorphism
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
49
diff
changeset
|
338 \RightLabel{ $ \Rightarrow \mathcal{E} $} |
|
451c510825de
Add natural deduction and curry-howard isomorphism
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
49
diff
changeset
|
339 \BinaryInfC{$ B $} |
|
451c510825de
Add natural deduction and curry-howard isomorphism
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
49
diff
changeset
|
340 \end{prooftree} |
|
451c510825de
Add natural deduction and curry-howard isomorphism
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
49
diff
changeset
|
341 |
|
451c510825de
Add natural deduction and curry-howard isomorphism
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
49
diff
changeset
|
342 \end{itemize} |
|
451c510825de
Add natural deduction and curry-howard isomorphism
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
49
diff
changeset
|
343 |
|
451c510825de
Add natural deduction and curry-howard isomorphism
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
49
diff
changeset
|
344 記号 $ \lor, \land, \Rightarrow $ の導入の除去規則について述べた。 |
|
451c510825de
Add natural deduction and curry-howard isomorphism
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
49
diff
changeset
|
345 natural deduction には他にも $ \forall, \exists, \bot $ といった記号が存在するが、ここでは解説を省略する。 |
|
451c510825de
Add natural deduction and curry-howard isomorphism
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
49
diff
changeset
|
346 |
|
451c510825de
Add natural deduction and curry-howard isomorphism
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
49
diff
changeset
|
347 それぞれの記号は以下のような意味を持つ |
|
451c510825de
Add natural deduction and curry-howard isomorphism
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
49
diff
changeset
|
348 \begin{itemize} |
|
451c510825de
Add natural deduction and curry-howard isomorphism
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
49
diff
changeset
|
349 \item $ \land $ |
|
451c510825de
Add natural deduction and curry-howard isomorphism
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
49
diff
changeset
|
350 conjunction。2つの命題が成り立つことを示す。 |
|
85
9d154c48a1f6
Update curry-howard isomorphism
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
83
diff
changeset
|
351 $ A \land B $ と記述すると、 A かつ B と考えることができる。 |
|
50
451c510825de
Add natural deduction and curry-howard isomorphism
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
49
diff
changeset
|
352 |
|
451c510825de
Add natural deduction and curry-howard isomorphism
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
49
diff
changeset
|
353 \item $ \lor $ |
|
451c510825de
Add natural deduction and curry-howard isomorphism
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
49
diff
changeset
|
354 disjunction。2つの命題のうちどちらかが成り立つことを示す。 |
|
85
9d154c48a1f6
Update curry-howard isomorphism
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
83
diff
changeset
|
355 $ A \lor B $ と記述すると、 A または B と考えることができる。 |
|
50
451c510825de
Add natural deduction and curry-howard isomorphism
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
49
diff
changeset
|
356 |
|
451c510825de
Add natural deduction and curry-howard isomorphism
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
49
diff
changeset
|
357 \item $ \Rightarrow $ |
|
451c510825de
Add natural deduction and curry-howard isomorphism
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
49
diff
changeset
|
358 implication。左側の命題が成り立つ時、右側の命題が成り立つことを示す。 |
|
85
9d154c48a1f6
Update curry-howard isomorphism
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
83
diff
changeset
|
359 $ A \Rightarrow B $ と記述すると、 A ならば B と考えることができる。 |
|
50
451c510825de
Add natural deduction and curry-howard isomorphism
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
49
diff
changeset
|
360 \end{itemize} |
|
451c510825de
Add natural deduction and curry-howard isomorphism
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
49
diff
changeset
|
361 |
|
451c510825de
Add natural deduction and curry-howard isomorphism
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
49
diff
changeset
|
362 例として、natural deduction で三段論法を証明する。 |
|
451c510825de
Add natural deduction and curry-howard isomorphism
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
49
diff
changeset
|
363 なお、三段論法とは「A は B であり、 B は C である。よって A は C である」といった文を示す。 |
|
451c510825de
Add natural deduction and curry-howard isomorphism
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
49
diff
changeset
|
364 |
|
451c510825de
Add natural deduction and curry-howard isomorphism
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
49
diff
changeset
|
365 \begin{prooftree} |
|
451c510825de
Add natural deduction and curry-howard isomorphism
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
49
diff
changeset
|
366 \AxiomC{ $ [A] $ $_{(1)}$} |
|
451c510825de
Add natural deduction and curry-howard isomorphism
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
49
diff
changeset
|
367 \AxiomC{ [$ (A \Rightarrow B) \land (B \Rightarrow C)$] $_{(2)}$ } |
|
451c510825de
Add natural deduction and curry-howard isomorphism
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
49
diff
changeset
|
368 \RightLabel{ $ \land 1 \mathcal{E} $ } |
|
451c510825de
Add natural deduction and curry-howard isomorphism
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
49
diff
changeset
|
369 \UnaryInfC{ $ (A \Rightarrow B) $ } |
|
85
9d154c48a1f6
Update curry-howard isomorphism
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
83
diff
changeset
|
370 \RightLabel{ $ \Rightarrow \mathcal{E} $} |
|
50
451c510825de
Add natural deduction and curry-howard isomorphism
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
49
diff
changeset
|
371 \BinaryInfC{ $ B $ } |
|
451c510825de
Add natural deduction and curry-howard isomorphism
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
49
diff
changeset
|
372 |
|
451c510825de
Add natural deduction and curry-howard isomorphism
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
49
diff
changeset
|
373 \AxiomC{ [$ (A \Rightarrow B) \land (B \Rightarrow C)$] $_{(2)}$ } |
|
451c510825de
Add natural deduction and curry-howard isomorphism
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
49
diff
changeset
|
374 \RightLabel{ $ \land 2 \mathcal{E} $ } |
|
451c510825de
Add natural deduction and curry-howard isomorphism
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
49
diff
changeset
|
375 \UnaryInfC{ $ (B \Rightarrow C) $ } |
|
451c510825de
Add natural deduction and curry-howard isomorphism
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
49
diff
changeset
|
376 |
|
85
9d154c48a1f6
Update curry-howard isomorphism
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
83
diff
changeset
|
377 \RightLabel{ $ \Rightarrow \mathcal{E} $} |
|
50
451c510825de
Add natural deduction and curry-howard isomorphism
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
49
diff
changeset
|
378 \BinaryInfC{ $ C $ } |
|
451c510825de
Add natural deduction and curry-howard isomorphism
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
49
diff
changeset
|
379 \RightLabel{ $ \Rightarrow \mathcal{I} _{(1)}$} |
|
451c510825de
Add natural deduction and curry-howard isomorphism
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
49
diff
changeset
|
380 \UnaryInfC{ $ A \Rightarrow C $} |
|
451c510825de
Add natural deduction and curry-howard isomorphism
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
49
diff
changeset
|
381 \RightLabel{ $ \Rightarrow \mathcal{I} _{(2)}$} |
|
451c510825de
Add natural deduction and curry-howard isomorphism
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
49
diff
changeset
|
382 \UnaryInfC{ $ ((A \Rightarrow B) \land (B \Rightarrow C)) \Rightarrow (A \Rightarrow C) $} |
|
451c510825de
Add natural deduction and curry-howard isomorphism
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
49
diff
changeset
|
383 \end{prooftree} |
|
451c510825de
Add natural deduction and curry-howard isomorphism
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
49
diff
changeset
|
384 |
|
451c510825de
Add natural deduction and curry-howard isomorphism
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
49
diff
changeset
|
385 まず、三段論法を論理式で表す。 |
|
451c510825de
Add natural deduction and curry-howard isomorphism
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
49
diff
changeset
|
386 |
|
451c510825de
Add natural deduction and curry-howard isomorphism
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
49
diff
changeset
|
387 「A は B であり、 B は C である。よって A は C である」 が証明するべき命題である。 |
|
451c510825de
Add natural deduction and curry-howard isomorphism
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
49
diff
changeset
|
388 まず、「A は B であり」から、Aから性質Bが導けることが分かる。これが $ A \Rightarrow B $ となる。 |
|
451c510825de
Add natural deduction and curry-howard isomorphism
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
49
diff
changeset
|
389 次に、「B は C である」から、Bから性質Cが導けることが分かる。これが $ B \Rightarrow C $ となる。 |
|
451c510825de
Add natural deduction and curry-howard isomorphism
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
49
diff
changeset
|
390 そしてこの2つは同時に成り立つ。 |
|
451c510825de
Add natural deduction and curry-howard isomorphism
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
49
diff
changeset
|
391 よって $ (A \Rightarrow B) \land (B \Rightarrow C)$ が仮定となる。 |
|
451c510825de
Add natural deduction and curry-howard isomorphism
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
49
diff
changeset
|
392 この仮定が成り立つ時に「Aは Cである」を示せば良い。 |
|
451c510825de
Add natural deduction and curry-howard isomorphism
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
49
diff
changeset
|
393 仮定と同じように「A は C である」は、 $ A \Rightarrow C $ と書けるため、証明するべき論理式は $ ((A \Rightarrow B) \land (B \Rightarrow C)) \Rightarrow (A \Rightarrow C) $ となる。 |
|
451c510825de
Add natural deduction and curry-howard isomorphism
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
49
diff
changeset
|
394 |
|
451c510825de
Add natural deduction and curry-howard isomorphism
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
49
diff
changeset
|
395 証明の手順はこうである。 |
|
451c510825de
Add natural deduction and curry-howard isomorphism
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
49
diff
changeset
|
396 まず条件$ (A \Rightarrow B) \land (B \Rightarrow C)$とAの2つを仮定する。 |
|
451c510825de
Add natural deduction and curry-howard isomorphism
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
49
diff
changeset
|
397 条件を $ \land 1 \mathcal{E} $ $ \land 2 \mathcal{E} $ により分解する。 |
|
451c510825de
Add natural deduction and curry-howard isomorphism
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
49
diff
changeset
|
398 A と $ A \Rightarrow B$ から B を、 B と $ B \Rightarrow C $ から C を導く。 |
|
451c510825de
Add natural deduction and curry-howard isomorphism
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
49
diff
changeset
|
399 ここで $ \Rightarrow \mathcal{I} $ により $ A \Rightarrow C $ を導く。 |
|
451c510825de
Add natural deduction and curry-howard isomorphism
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
49
diff
changeset
|
400 この際に dead にする仮定は A である。 |
|
451c510825de
Add natural deduction and curry-howard isomorphism
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
49
diff
changeset
|
401 数回仮定を dead にする際は $_{(1)} $ のように対応する \verb/[]/の記号に数値を付ける。 |
|
451c510825de
Add natural deduction and curry-howard isomorphism
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
49
diff
changeset
|
402 これで残る alive な仮定は $ (A \Rightarrow B) \land (B \Rightarrow C)$ となり、これから $ A \Rightarrow C $ を導くことができたためにさらに $ \Rightarrow \mathcal{I} $ を適用する。 |
|
451c510825de
Add natural deduction and curry-howard isomorphism
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
49
diff
changeset
|
403 結果、証明すべき論理式$ ((A \Rightarrow B) \land (B \Rightarrow C)) \Rightarrow (A \Rightarrow C) $ が導けたために証明終了となる。 |
|
451c510825de
Add natural deduction and curry-howard isomorphism
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
49
diff
changeset
|
404 |
|
451c510825de
Add natural deduction and curry-howard isomorphism
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
49
diff
changeset
|
405 % }}} |
|
451c510825de
Add natural deduction and curry-howard isomorphism
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
49
diff
changeset
|
406 |
|
85
9d154c48a1f6
Update curry-howard isomorphism
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
83
diff
changeset
|
407 % {{{ Curry-Howard Isomorphism |
| 49 | 408 \section{Curry-Howard Isomorphism} |
|
50
451c510825de
Add natural deduction and curry-howard isomorphism
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
49
diff
changeset
|
409 \label{section:curry_howard_isomorphism} |
|
85
9d154c48a1f6
Update curry-howard isomorphism
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
83
diff
changeset
|
410 \ref{section:natural_deduction}節では Natural Deduction における証明手法について述べた。 |
|
9d154c48a1f6
Update curry-howard isomorphism
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
83
diff
changeset
|
411 Natural Deduction はプログラム上では型付きのラムダ式として表現できる。 |
|
9d154c48a1f6
Update curry-howard isomorphism
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
83
diff
changeset
|
412 これは Curry-Howard Isomorphism と呼ばれ、 Natural Deduction と型付き $ \lambda $ 計算が同じ構造であることを表している。 |
|
9d154c48a1f6
Update curry-howard isomorphism
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
83
diff
changeset
|
413 Curry-Howard Isomorphism の概要を表~\ref{table:curry}に示す。 |
|
50
451c510825de
Add natural deduction and curry-howard isomorphism
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
49
diff
changeset
|
414 |
|
451c510825de
Add natural deduction and curry-howard isomorphism
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
49
diff
changeset
|
415 \begin{center} |
|
85
9d154c48a1f6
Update curry-howard isomorphism
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
83
diff
changeset
|
416 \begin{table}[htbp] |
|
9d154c48a1f6
Update curry-howard isomorphism
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
83
diff
changeset
|
417 \begin{tabular}{|c|c|} \hline |
|
9d154c48a1f6
Update curry-howard isomorphism
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
83
diff
changeset
|
418 Natural Deduction & 型付き $ \lambda $ 計算 \\ \hline \hline |
|
9d154c48a1f6
Update curry-howard isomorphism
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
83
diff
changeset
|
419 $ A $ & 型 A を持つ変数 x \\ \hline |
|
9d154c48a1f6
Update curry-howard isomorphism
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
83
diff
changeset
|
420 $ A \Rightarrow B $ & 型 A を取り型 B の変数を返す関数 f \\ \hline |
|
9d154c48a1f6
Update curry-howard isomorphism
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
83
diff
changeset
|
421 $ \Rightarrow \mathcal{I} $ & ラムダの抽象化 \\ \hline |
|
9d154c48a1f6
Update curry-howard isomorphism
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
83
diff
changeset
|
422 $ \Rightarrow \mathcal{E} $ & 関数適用 \\ \hline |
|
9d154c48a1f6
Update curry-howard isomorphism
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
83
diff
changeset
|
423 $ A \land B $ & 型 A と型 B の直積型 を持つ変数 x \\ \hline |
|
9d154c48a1f6
Update curry-howard isomorphism
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
83
diff
changeset
|
424 $ \land \mathcal{I} $ & 型A,Bを持つ値から直積型へのコンストラクタ \\ \hline |
|
9d154c48a1f6
Update curry-howard isomorphism
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
83
diff
changeset
|
425 $ \land 1 \mathcal{E} $ & 直積型からの型Aを取り出す射影fst \\ \hline |
|
9d154c48a1f6
Update curry-howard isomorphism
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
83
diff
changeset
|
426 $ \land 2 \mathcal{E} $ & 直積型からの型Bを取り出す射影snd \\ \hline |
|
9d154c48a1f6
Update curry-howard isomorphism
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
83
diff
changeset
|
427 $ A \lor B $ & 型 A と型 B の直和型 を持つ変数 x \\ \hline |
|
9d154c48a1f6
Update curry-howard isomorphism
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
83
diff
changeset
|
428 $ \lor \mathcal{I} $ & 型A,Bの値から直和型へのコンストラクタ \\ \hline |
|
9d154c48a1f6
Update curry-howard isomorphism
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
83
diff
changeset
|
429 $ \lor \mathcal{E} $ & 直和型から型Cの値を返す関数f \\ \hline |
|
9d154c48a1f6
Update curry-howard isomorphism
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
83
diff
changeset
|
430 \end{tabular} |
|
9d154c48a1f6
Update curry-howard isomorphism
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
83
diff
changeset
|
431 \caption{natural deuction と 型付き $ \lambda $ 計算との対応(Curry-Howard Isomorphism)} |
|
9d154c48a1f6
Update curry-howard isomorphism
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
83
diff
changeset
|
432 \label{table:curry} |
|
9d154c48a1f6
Update curry-howard isomorphism
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
83
diff
changeset
|
433 \end{table} |
|
50
451c510825de
Add natural deduction and curry-howard isomorphism
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
49
diff
changeset
|
434 \end{center} |
|
85
9d154c48a1f6
Update curry-howard isomorphism
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
83
diff
changeset
|
435 |
|
9d154c48a1f6
Update curry-howard isomorphism
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
83
diff
changeset
|
436 型付きラムダ計算における命題は型に相当する。 |
|
9d154c48a1f6
Update curry-howard isomorphism
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
83
diff
changeset
|
437 例えば恒等関数id の型は $ \text{A} \rightarrow \text{A}$ という型を持つが、これは「Aが成り立つならAが成り立つ」という命題と等しい。 |
|
9d154c48a1f6
Update curry-howard isomorphism
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
83
diff
changeset
|
438 命題の仮定は引数となって表れ、証明はその型を導くための式となる。 |
|
9d154c48a1f6
Update curry-howard isomorphism
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
83
diff
changeset
|
439 |
|
9d154c48a1f6
Update curry-howard isomorphism
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
83
diff
changeset
|
440 例えば Natural Deduction における三段論法は $ ((A \Rightarrow B) \land (B \Rightarrow C)) \Rightarrow (A \Rightarrow C) $ という形をしていた。 |
|
9d154c48a1f6
Update curry-howard isomorphism
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
83
diff
changeset
|
441 仮定は $ ((A \Rightarrow B) \land (B \Rightarrow C)) $ となる。 |
|
9d154c48a1f6
Update curry-howard isomorphism
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
83
diff
changeset
|
442 |
|
9d154c48a1f6
Update curry-howard isomorphism
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
83
diff
changeset
|
443 直積に対応する型には直積型が存在する。 |
|
9d154c48a1f6
Update curry-howard isomorphism
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
83
diff
changeset
|
444 Agda において直積型に対応するデータ構造 \verb/Product/ を定義するとリスト~\ref{src:agda-product}のようになる。 |
|
9d154c48a1f6
Update curry-howard isomorphism
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
83
diff
changeset
|
445 例えば \verb/Int/ 型と \verb/String/ 型を取る直積型は \verb/Int/ $ \times $ \verb/String/ 型となる。 |
|
9d154c48a1f6
Update curry-howard isomorphism
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
83
diff
changeset
|
446 これは二つの型を取る型であり、Natural Deduction の $ \land $ に相当する。 |
|
9d154c48a1f6
Update curry-howard isomorphism
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
83
diff
changeset
|
447 |
|
9d154c48a1f6
Update curry-howard isomorphism
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
83
diff
changeset
|
448 直積型から値を射影する関数 \verb/fst/ と \verb/snd/ を定義する。 |
|
9d154c48a1f6
Update curry-howard isomorphism
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
83
diff
changeset
|
449 これらは Natural Deduction における $ \land 1 \mathcal{E} $ と $ \land 2 \mathcal{E} $ に相当する。 |
|
9d154c48a1f6
Update curry-howard isomorphism
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
83
diff
changeset
|
450 |
|
9d154c48a1f6
Update curry-howard isomorphism
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
83
diff
changeset
|
451 なお、直積型は型Aを持つフィールド\verb/fst/と型Bを持つフィールド\verb/snd/を持つレコード型と考えても良い。 |
|
9d154c48a1f6
Update curry-howard isomorphism
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
83
diff
changeset
|
452 |
|
9d154c48a1f6
Update curry-howard isomorphism
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
83
diff
changeset
|
453 \lstinputlisting[label=src:agda-product, caption=Agda における直積型] {src/AgdaProduct.agda} |
|
9d154c48a1f6
Update curry-howard isomorphism
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
83
diff
changeset
|
454 |
|
9d154c48a1f6
Update curry-howard isomorphism
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
83
diff
changeset
|
455 三段論法の証明は 「1つの仮定から $ \land 1 \mathcal{E} $ と $ \land 2 \mathcal{E} $ を用いて仮定を二つ取り出し、それぞれに $ \Rightarrow \mathcal{E} $ を適用した後に仮定を $ \Rightarrow \mathcal{I}$ で dead にする」形であった。 |
|
9d154c48a1f6
Update curry-howard isomorphism
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
83
diff
changeset
|
456 |
|
9d154c48a1f6
Update curry-howard isomorphism
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
83
diff
changeset
|
457 $ \Rightarrow \mathcal{I}$ に対応するのは関数適用である。 |
|
9d154c48a1f6
Update curry-howard isomorphism
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
83
diff
changeset
|
458 よってこの証明は「一つの変数から \verb/fst/ と \verb/snd/ を使って関数を二つ取り出し、それぞれを関数適用する」という形になる。 |
|
9d154c48a1f6
Update curry-howard isomorphism
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
83
diff
changeset
|
459 これをラムダ式で書くとリスト~\ref{src:agda-modus-ponens}のようになる。 |
|
9d154c48a1f6
Update curry-howard isomorphism
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
83
diff
changeset
|
460 仮定 A $ \times $ B と仮定 A から A $ \rightarrow $ C を導いている。 |
|
9d154c48a1f6
Update curry-howard isomorphism
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
83
diff
changeset
|
461 |
|
9d154c48a1f6
Update curry-howard isomorphism
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
83
diff
changeset
|
462 \lstinputlisting[label=src:agda-modus-ponens, caption=Agda における三段論法の証明] {src/AgdaModusPonens.agda.replaced} |
|
9d154c48a1f6
Update curry-howard isomorphism
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
83
diff
changeset
|
463 |
|
9d154c48a1f6
Update curry-howard isomorphism
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
83
diff
changeset
|
464 このように Agda では証明を記述することができる。 |
|
9d154c48a1f6
Update curry-howard isomorphism
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
83
diff
changeset
|
465 |
|
50
451c510825de
Add natural deduction and curry-howard isomorphism
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
49
diff
changeset
|
466 % }}} |
|
451c510825de
Add natural deduction and curry-howard isomorphism
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
49
diff
changeset
|
467 |
| 55 | 468 % {{{ Reasoning |
| 51 | 469 |
| 49 | 470 \section{Reasoning} |
|
85
9d154c48a1f6
Update curry-howard isomorphism
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
83
diff
changeset
|
471 次に依存型を利用して等式の証明を記述していく。 |
|
9d154c48a1f6
Update curry-howard isomorphism
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
83
diff
changeset
|
472 |
| 55 | 473 例題として、自然数の加法の可換法則を示す。 |
| 474 証明を行なうためにまずは自然数を定義する。 | |
| 475 今回用いる自然数の定義は以下のようなものである。 | |
| 476 | |
| 477 \begin{itemize} | |
| 478 \item 0 は自然数である | |
| 479 \item 任意の自然数には後続数が存在する | |
| 480 \item 0 はいかなる自然数の後続数でもない | |
| 481 \item 異なる自然数どうしの後続数は異なる ($ n \neq m \rightarrow S n \neq S m $) | |
| 482 \item 0がある性質を満たし、aがある性質を満たせばその後続数 S(n) も自然数である | |
| 483 \end{itemize} | |
| 484 | |
| 485 この定義は peano arithmetic における自然数の定義である。 | |
| 486 | |
| 487 Agda で自然数型 Nat を定義するとリスト \ref{src:agda-nat-2} のようになる。 | |
| 488 | |
| 489 \lstinputlisting[label=src:agda-nat-2, caption=Agda における自然数型 Nat の定義] {src/Nat.agda} | |
| 490 | |
| 491 自然数型 Nat は2つのコンストラクタを持つ。 | |
| 492 | |
| 493 \begin{itemize} | |
| 494 \item O | |
| 495 | |
| 496 引数を持たないコンストラクタ。これが0に相当する。 | |
| 497 | |
| 498 \item S | |
| 499 | |
| 500 Nat を引数に取るコンストラクタ。これが後続数に相当する。 | |
| 501 | |
| 502 \end{itemize} | |
| 503 | |
| 504 よって、数値の 3 は \verb/S (S (S O))/ のように表現される。 | |
| 505 Sの個数が数値に対応する。 | |
| 506 | |
| 507 次に加算を定義する(リスト\ref{src:agda-nat-add})。 | |
| 508 | |
| 509 \lstinputlisting[label=src:agda-nat-add, caption=Agdaにおける自然数型に対する加算の定義] {src/NatAdd.agda} | |
| 510 | |
| 511 加算は中置関数 \verb/_+_/ として定義する。 | |
| 512 2つの Nat を取り、Natを返す。 | |
| 513 関数 \verb/_+_/ はパターンマッチにより処理を変える。 | |
| 514 0に対して m 加算する場合は m であり、 n の後続数に対して m 加算する場合は n に m 加算した数の後続数とする。 | |
| 515 S を左の数から右の数へ1つずつ再帰的に移していくような加算である。 | |
| 516 | |
| 517 例えば 3 + 1 といった計算は (S (S (S O))) + (S O) のように記述される。 | |
| 518 ここで 3 + 1 が 4と等しいことの証明を行なう。 | |
| 519 | |
| 520 等式の証明には agda の standard library における Relation.Binary.Core の定義を用いる。 | |
| 521 | |
| 522 \lstinputlisting[label=src:agda-equiv, caption= Relation.Binary.Core による等式を示す型 $ \equiv $] {src/Equiv.agda.replaced} | |
| 523 Agda において等式は、等式を示すデータ型 $ \equiv $ により定義される。 | |
| 524 $ \equiv $ は同じ両辺が同じ項に簡約される時にコンストラクタ refl で構築できる。 | |
| 525 | |
| 526 実際に 3 + 1 = 4 の証明は refl で構成できる(リスト\ref{src:agda-three-plus-one})。 | |
| 527 | |
| 528 \lstinputlisting[label=src:agda-three-plus-one, caption= Agda における 3 + 1 の結果が 4 と等しい証明] {src/ThreePlusOne.agda} | |
| 529 | |
| 530 3+1 という関数を定義し、その型として証明すべき式を記述し、証明を関数の定義として定義する。 | |
| 531 証明する式は \verb/(S (S (S O))) + (S O)≡(S (S (S (S O))))/ である。 | |
| 532 今回は \verb/_+_/ 関数の定義により \verb/ (S (S (S (S O)))) / に簡約されるためにコンストラクタ refl が証明となる。 | |
| 533 | |
| 534 $ \equiv $ によって証明する際、必ず同じ式に簡約されるとは限らないため、いくつかの操作が Relation.Binary.PropositionalEquality に定義されている。 | |
| 535 | |
| 536 \begin{itemize} | |
| 537 \item sym : $ x \equiv y \rightarrow y \equiv x $ | |
| 538 | |
| 539 等式が証明できればその等式の左辺と右辺を反転しても等しい。 | |
| 540 | |
| 541 \item cong : $ f \rightarrow x \equiv y \rightarrow f x \equiv f y $ | |
| 542 | |
| 543 証明した等式に同じ関数を与えても等式は保たれる。 | |
| 544 | |
| 545 \item trans : $ x \equiv y \rightarrow y \equiv z \rightarrow x \equiv z $ | |
| 546 | |
| 547 2つの等式に表れた同じ項を用いて2つの等式を繋げた等式は等しい。 | |
| 548 \end{itemize} | |
| 549 | |
| 550 ではこれから nat の加法の交換法則を証明していく(リスト\ref{src:agda-nat-add-sym})。 | |
| 551 | |
| 552 \lstinputlisting[label=src:agda-nat-add-sym, caption= Agda における加法の交換法則の証明] {src/NatAddSym.agda} | |
| 553 | |
| 554 証明する式は $ n + m \equiv m + n $ である。 | |
| 555 n と m は Nat であるため、それぞれがコンストラクタ O か S により構成される。 | |
| 556 そのためにパターンは4通りある。 | |
| 557 | |
| 558 \begin{itemize} | |
| 559 \item n = O, m = O | |
| 560 | |
|
64
10a550bf7e4a
Mini fixes with ryokka-san
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
55
diff
changeset
|
561 \verb/_+_/ の定義により、 O に簡約されるため refl で証明できる。 |
| 55 | 562 |
| 563 \item n = O, m = S m | |
| 564 | |
| 565 $ O + (S m) \equiv (S m) + O $ を証明することになる。 | |
|
64
10a550bf7e4a
Mini fixes with ryokka-san
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
55
diff
changeset
|
566 この等式は \verb/_+_/ の定義により $ O + (S m) \equiv S (m + O) $ と変形できる。 |
| 55 | 567 $ S (m + O) $ は $ m + O $ に S を加えたものであるため、 cong を用いて再帰的に \verb/addSym/ を実行することで証明できる。 |
| 568 | |
| 569 この2つの証明はこのような意味を持つ。 | |
| 570 n が 0 であるとき、 m も 0 なら簡約により等式が成立する。 | |
| 571 n が 0 であり、 m が 0 でないとき、 m は後続数である。 | |
| 572 よって m が (S x) と書かれる時、 x は m の前の値である。 | |
|
64
10a550bf7e4a
Mini fixes with ryokka-san
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
55
diff
changeset
|
573 前の値による交換法則を用いてからその結果の後続数も \verb/_+_/ の定義により等しい。 |
| 55 | 574 |
| 575 ここで、 \verb/addSym/ に渡される m は1つ値が減っているため、最終的には n = 0, m = 0 である refl にまで簡約され、等式が得られる。 | |
| 576 | |
| 577 \item n = S n, m = O | |
| 578 | |
| 579 $ (S n) + O \equiv O + (S n) $ を証明する。 | |
|
64
10a550bf7e4a
Mini fixes with ryokka-san
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
55
diff
changeset
|
580 この等式は \verb/_+_/ の定義により $ S (n + O) \equiv (S n) $ と変形できる。 |
| 55 | 581 さらに変形すれば $ S (n + O) \equiv S (O + n) $ となる。 |
| 582 よって \verb/addSym/ により O と n を変換した後に cong で S を加えることで証明ができる。 | |
| 583 | |
|
64
10a550bf7e4a
Mini fixes with ryokka-san
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
55
diff
changeset
|
584 ここで、 $ O + n \equiv n $ は \verb/_+_/ の定義により自明であるが、$ n + O \equiv n $ をそのまま導出できないことに注意して欲しい。 |
|
10a550bf7e4a
Mini fixes with ryokka-san
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
55
diff
changeset
|
585 \verb/_+_/ の定義は左側の項から S を右側の項への移すだけであるため、右側の項への演算はしない。 |
| 55 | 586 |
| 587 \item n = S n, m = S m | |
| 588 | |
| 589 3つのパターンは証明したが、このパターンは少々長くなるため別に解説することとする。 | |
| 590 \end{itemize} | |
| 591 | |
| 592 3 つのパターンにおいては refl や cong といった単純な項で証明を行なうことができた。 | |
| 593 しかし長い証明になると refl や cong といった式を trans で大量に繋げていく必要性がある。 | |
| 594 長い証明を分かりやすく記述するために $ \equiv $-Reasoning を用いる。 | |
| 595 | |
| 596 $ \equiv $-Reasoning では等式の左辺を begin の後に記述し、等式の変形を $ \equiv \langle expression \rangle $ に記述することで変形していく。 | |
| 597 最終的に等式の左辺を $ \blacksquare $ の項へと変形することで等式の証明が得られる。 | |
| 598 | |
| 599 自然数の加法の交換法則を $ \equiv $-Reasoning を用いて証明した例がリスト\ref{src:agda-reasoning}である。 | |
| 600 特に n と m が1以上である時の証明に注目する。 | |
| 601 | |
| 602 \lstinputlisting[label=src:agda-reasoning, caption= $ \equiv $ - Reasoning を用いた証明の例] {src/Reasoning.agda.replaced} | |
| 603 | |
|
64
10a550bf7e4a
Mini fixes with ryokka-san
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
55
diff
changeset
|
604 まず \verb/ (S n) + (S m)/ は \verb/_+_/ の定義により \verb/ S (n + (S m)) / に等しい。 |
| 55 | 605 よって refl で導かれる。 |
| 606 なお、基本的に定義などで同じ項に簡約される時は refl によって記述することが多い。 | |
| 607 | |
| 608 次に \verb/S (n + (S m)) / に対して addSym を用いて交換し、 cong によって S を追加することで \verb/ S ((S m) + n) / を得る。 | |
| 609 これは、前3パターンにおいて + の右辺の項が 1以上であっても上手く交換法則が定義できたことを利用して項を変形している。 | |
| 610 このように同じ法則の中でも、違うパターンで証明できた部分を用いて別パターンの証明を行なうこともある。 | |
| 611 | |
| 612 最後に \verb/S ((S m) + n)/ から \verb/(S m) + (S n)/を得なくてはならない。 | |
|
64
10a550bf7e4a
Mini fixes with ryokka-san
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
55
diff
changeset
|
613 しかし、 \verb/_+_/ の定義には右辺に対して S を移動する演算が含まれていない。 |
| 55 | 614 よってこのままでは証明することができない。 |
| 615 そのため、等式 $ S (m + n) \equiv m + (S n) $ を addToRight として定義する。 | |
|
64
10a550bf7e4a
Mini fixes with ryokka-san
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
55
diff
changeset
|
616 addToRight はコンストラクタによる分岐を用いて証明できる。 |
|
10a550bf7e4a
Mini fixes with ryokka-san
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
55
diff
changeset
|
617 値が0であれば自明に成り立ち、1以上であれば再帰的に addToRight を適用することで任意の数に対して成り立つ。 |
| 55 | 618 addToRight を用いることで \verb/S ((S m) + n)/ から \verb/(S m) + (S n)/を得られた。 |
| 619 これで等式 $ (S m) + (S n) \equiv (S n) + (S m) $ の証明が完了した。 | |
| 620 | |
| 621 自然数に対する + の演算を考えた時にありえるコンストラクタの組み合せ4パターンのいずれかでも交換法則の等式が成り立つことが分かった。 | |
| 622 このように、Agda における等式の証明は、定義や等式を用いて右辺と左辺を同じ項に変形することで行なわれる。 | |
| 623 | |
| 624 % }}} |