Mercurial > hg > Papers > 2018 > nozomi-master

comparison paper/agda.tex @ 86:e437746d6038

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Fix lstinput
author atton <atton@cr.ie.u-ryukyu.ac.jp>
date Thu, 09 Feb 2017 15:40:11 +0900
parents 9d154c48a1f6
children 2bc816f4af27
comparison
equal deleted inserted replaced
85:9d154c48a1f6 86:e437746d6038
20 まず、Agda のプログラムを記述するファイルを作成する。 20 まず、Agda のプログラムを記述するファイルを作成する。
21 Agda のプログラムは全てモジュール内部に記述されるため、まずはトップレベルにモジュールを定義する必要がある。 21 Agda のプログラムは全てモジュール内部に記述されるため、まずはトップレベルにモジュールを定義する必要がある。
22 トップレベルのモジュールはファイル名と同一となる。 22 トップレベルのモジュールはファイル名と同一となる。
23 例えば \verb/AgdaBasics.agda/ を作成する時のモジュール名はリスト~\ref{src:agda-module}のように定義する。 23 例えば \verb/AgdaBasics.agda/ を作成する時のモジュール名はリスト~\ref{src:agda-module}のように定義する。
24 24
25 \lstinputlisting[label=src:agda-module, caption=Agdaのモジュールの定義する] {src/AgdaBasics.agda} 25 \lstinputlisting[label=src:agda-module, caption=Agdaのモジュールの定義する] {src/AgdaBasics.agda.replaced}
26 26
27 Agda における型指定は $:$ を用いて行なう。 27 Agda における型指定は $:$ を用いて行なう。
28 例えば、変数xが型Aを持つ、ということを表すには \verb/x : A/ と記述する。 28 例えば、変数xが型Aを持つ、ということを表すには \verb/x : A/ と記述する。
29 29
30 データ型は Haskell や ML に似た代数的なデータ構造である。 30 データ型は Haskell や ML に似た代数的なデータ構造である。
33 例えば Bool 型を定義するとリスト~\ref{src:agda-bool}のようになる。 33 例えば Bool 型を定義するとリスト~\ref{src:agda-bool}のようになる。
34 Bool はコンストラクタ \verb/true/ か \verb/false/ を持つデータ型である。 34 Bool はコンストラクタ \verb/true/ か \verb/false/ を持つデータ型である。
35 Bool 自身の型は \verb/Set/ であり、これは Agda が組み込みで持つ「型の型」である。 35 Bool 自身の型は \verb/Set/ であり、これは Agda が組み込みで持つ「型の型」である。
36 Set は階層構造を持ち、型の型の型を指定するには Set1 と書く。 36 Set は階層構造を持ち、型の型の型を指定するには Set1 と書く。
37 37
38 \lstinputlisting[label=src:agda-bool, caption=Agdaにおけるデータ型 Bool の定義] {src/AgdaBool.agda} 38 \lstinputlisting[label=src:agda-bool, caption=Agdaにおけるデータ型 Bool の定義] {src/AgdaBool.agda.replaced}
39 39
40 40
41 関数の定義は Haskell に近い。 41 関数の定義は Haskell に近い。
42 関数名と型を記述した後に関数の本体を \verb/=/ の後に指定する。 42 関数名と型を記述した後に関数の本体を \verb/=/ の後に指定する。
43 関数の型は $ \rightarrow $ を用いる。 43 関数の型は $ \rightarrow $ を用いる。
44 なお、$\rightarrow$に対しては糖衣構文 \verb/->/ も用意されている。 44 なお、$\rightarrow$に対しては糖衣構文 \verb/->/ も用意されている。
45 例えば引数が型 \verb/A/ で返り値が型 \verb/B/ の関数は \verb/A -> B/ のように書ける。 45 例えば引数が型 \verb/A/ で返り値が型 \verb/B/ の関数は \verb/A -> B/ のように書ける。
46 Bool 変数 \verb/x/ を取って true を返す関数 \verb/f/はリスト~\ref{src:agda-function}のようになる。 46 Bool 変数 \verb/x/ を取って true を返す関数 \verb/f/はリスト~\ref{src:agda-function}のようになる。
47 47
48 \lstinputlisting[label=src/agda-function, caption=Agda における関数定義] {src/AgdaFunction.agda} 48 \lstinputlisting[label=src/agda-function, caption=Agda における関数定義] {src/AgdaFunction.agda.replaced}
49 49
50 引数は変数名で受けることもできるが、具体的なコンストラクタを指定することでそのコンストラクタが渡された時の挙動を定義できる。 50 引数は変数名で受けることもできるが、具体的なコンストラクタを指定することでそのコンストラクタが渡された時の挙動を定義できる。
51 これはパターンマッチと呼ばれ、コンストラクタで case 文を行なっているようなものである。 51 これはパターンマッチと呼ばれ、コンストラクタで case 文を行なっているようなものである。
52 例えば Bool 型の値を反転する \verb/not/ 関数を書くとリスト~\ref{src:agda-not}のようになる。 52 例えば Bool 型の値を反転する \verb/not/ 関数を書くとリスト~\ref{src:agda-not}のようになる。
53 53
54 \lstinputlisting[label=src:agda-not, caption=Agdaにおける関数 not の定義] {src/AgdaNot.agda} 54 \lstinputlisting[label=src:agda-not, caption=Agdaにおける関数 not の定義] {src/AgdaNot.agda.replaced}
55 55
56 パターンマッチは全てのコンストラクタのパターンを含まなくてはならない。 56 パターンマッチは全てのコンストラクタのパターンを含まなくてはならない。
57 例えば、Bool 型を受け取る関数で \verb/true/ の時の挙動のみを書くことはできない。 57 例えば、Bool 型を受け取る関数で \verb/true/ の時の挙動のみを書くことはできない。
58 なお、コンストラクタをいくつか指定した後に変数で受けると、変数が持ちうる値は指定した以外のコンストラクタとなる。 58 なお、コンストラクタをいくつか指定した後に変数で受けると、変数が持ちうる値は指定した以外のコンストラクタとなる。
59 例えばリスト~\ref{src:agda-pattern}の not は x には true しか入ることは無い。 59 例えばリスト~\ref{src:agda-pattern}の not は x には true しか入ることは無い。
60 なお、マッチした値を変数として利用しない場合は \verb/_/ を用いて捨てることもできる。 60 なお、マッチした値を変数として利用しない場合は \verb/_/ を用いて捨てることもできる。
61 61
62 \lstinputlisting[label=src:agda-pattern, caption=Agdaにおけるパターンマッチ] {src/AgdaPattern.agda} 62 \lstinputlisting[label=src:agda-pattern, caption=Agdaにおけるパターンマッチ] {src/AgdaPattern.agda.replaced}
63 63
64 関数にはリテラルが存在し、関数名を定義せずともその場で生成することができる。 64 関数にはリテラルが存在し、関数名を定義せずともその場で生成することができる。
65 これをラムダ式と呼び、\verb/\arg1 arg2 -> function body/ のように書く。 65 これをラムダ式と呼び、\verb/\arg1 arg2 -> function body/ のように書く。
66 例えば Bool 型の引数 \verb/b/ を取って not を適用する \verb/not-apply/ をラムダ式で書くとリスト~\ref{src:agda-lambda}のようになる。 66 例えば Bool 型の引数 \verb/b/ を取って not を適用する \verb/not-apply/ をラムダ式で書くとリスト~\ref{src:agda-lambda}のようになる。
67 関数 \verb/not-apply/ をラムダ式を使わずに定義すると \verb/not-apply-2/ になるが、この二つの関数は同一の動作をする。 67 関数 \verb/not-apply/ をラムダ式を使わずに定義すると \verb/not-apply-2/ になるが、この二つの関数は同一の動作をする。
68 68
69 \lstinputlisting[label=src:agda-lambda, caption=Agda におけるラムダ式] {src/AgdaLambda.agda} 69 \lstinputlisting[label=src:agda-lambda, caption=Agda におけるラムダ式] {src/AgdaLambda.agda.replaced}
70 70
71 Agda では特定の関数内のみで利用する関数を \verb/where/ 句で記述できる。 71 Agda では特定の関数内のみで利用する関数を \verb/where/ 句で記述できる。
72 これは関数内部の冗長な記述を省略するのに活用できる。 72 これは関数内部の冗長な記述を省略するのに活用できる。
73 スコープは \verb/where/句が存在する関数内部のみであるため、名前空間が汚染させることも無い。 73 スコープは \verb/where/句が存在する関数内部のみであるため、名前空間が汚染させることも無い。
74 例えば自然数3つを取ってそれぞれ3倍して加算する関数 \verb/f/ を定義するとき、 \verb/where/ を使うとリスト~\ref{src:agda-where} のように書ける。 74 例えば自然数3つを取ってそれぞれ3倍して加算する関数 \verb/f/ を定義するとき、 \verb/where/ を使うとリスト~\ref{src:agda-where} のように書ける。
75 これは \verb/f'/ と同様の動作をする。 75 これは \verb/f'/ と同様の動作をする。
76 \verb/where/ 句は利用したい関数の末尾にインデント付きで \verb/where/ キーワードを記述し、改行の後インデントをして関数内部で利用する関数を定義する。 76 \verb/where/ 句は利用したい関数の末尾にインデント付きで \verb/where/ キーワードを記述し、改行の後インデントをして関数内部で利用する関数を定義する。
77 77
78 \lstinputlisting[label=src:agda-where, caption=Agda における where 句] {src/AgdaWhere.agda} 78 \lstinputlisting[label=src:agda-where, caption=Agda における where 句] {src/AgdaWhere.agda.replaced}
79 79
80 80
81 データ型のコンストラクタには自分自身の型を引数に取ることもできる(リスト~\ref{src:agda-nat})。 81 データ型のコンストラクタには自分自身の型を引数に取ることもできる(リスト~\ref{src:agda-nat})。
82 自然数のコンストラクタは2つあり、片方は自然数ゼロ、片方は自然数を取って後続数を返すものである。 82 自然数のコンストラクタは2つあり、片方は自然数ゼロ、片方は自然数を取って後続数を返すものである。
83 例えば0 は \verb/zero/ であり、1 は \verb/suc zero/に、3は \verb/suc (suc (suc zero))/ に対応する。 83 例えば0 は \verb/zero/ であり、1 は \verb/suc zero/に、3は \verb/suc (suc (suc zero))/ に対応する。
84 84
85 \lstinputlisting[label=src:agda-nat, caption=Agdaにおける自然数の定義] {src/AgdaNat.agda} 85 \lstinputlisting[label=src:agda-nat, caption=Agdaにおける自然数の定義] {src/AgdaNat.agda.replaced}
86 86
87 自然数に対する演算は再帰関数として定義できる。 87 自然数に対する演算は再帰関数として定義できる。
88 例えば自然数どうしの加算は二項演算子\verb/+/としてリスト~\ref{src:agda-plus}のように書ける。 88 例えば自然数どうしの加算は二項演算子\verb/+/としてリスト~\ref{src:agda-plus}のように書ける。
89 89
90 この二項演算子は正確には中置関数である。 90 この二項演算子は正確には中置関数である。
94 また、Agda は再帰関数が停止するかを判定できる。 94 また、Agda は再帰関数が停止するかを判定できる。
95 この加算の二項演算子は左側がゼロに対しては明らかに停止する。 95 この加算の二項演算子は左側がゼロに対しては明らかに停止する。
96 左側が1以上の時の再帰時には \verb/suc n/ から \verb/n/へと減っているため、再帰で繰り返し減らすことでいつかは停止する。 96 左側が1以上の時の再帰時には \verb/suc n/ から \verb/n/へと減っているため、再帰で繰り返し減らすことでいつかは停止する。
97 もし \verb/suc n/ のまま自分自身へと再帰した場合、Agda は警告を出す。 97 もし \verb/suc n/ のまま自分自身へと再帰した場合、Agda は警告を出す。
98 98
99 \lstinputlisting[label=src:agda-plus, caption=Agda における自然数の加算の定義] {src/AgdaPlus.agda} 99 \lstinputlisting[label=src:agda-plus, caption=Agda における自然数の加算の定義] {src/AgdaPlus.agda.replaced}
100 100
101 次に依存型について見ていく。 101 次に依存型について見ていく。
102 依存型で最も基本的なものは関数型である。 102 依存型で最も基本的なものは関数型である。
103 依存型を利用した関数は引数の型に依存して返す型を決定できる。 103 依存型を利用した関数は引数の型に依存して返す型を決定できる。
104 104
105 Agda で \verb/(x : A) -> B/ と書くと関数は型 A を持つx を受け取り、Bを返す。 105 Agda で \verb/(x : A) -> B/ と書くと関数は型 A を持つx を受け取り、Bを返す。
106 ここで B の中で x を扱っても良い。 106 ここで B の中で x を扱っても良い。
107 例えば任意の型に対する恒等関数はリスト~\ref{src:agda-id}のように書ける。 107 例えば任意の型に対する恒等関数はリスト~\ref{src:agda-id}のように書ける。
108 108
109 \lstinputlisting[label=src:agda-id, caption=依存型を持つ関数の定義] {src/AgdaId.agda} 109 \lstinputlisting[label=src:agda-id, caption=依存型を持つ関数の定義] {src/AgdaId.agda.replaced}
110 110
111 この恒等関数 \verb/identitiy/ は任意の型に適用可能である。 111 この恒等関数 \verb/identitiy/ は任意の型に適用可能である。
112 実際に関数 \verb/identitiy/ を Nat へ適用した例が \verb/identitiy-zero/ である。 112 実際に関数 \verb/identitiy/ を Nat へ適用した例が \verb/identitiy-zero/ である。
113 113
114 多相の恒等関数では型を明示的に指定せずとも \verb/zero/ に適用した場合の型は自明に \verb/Nat -> Nat/である。 114 多相の恒等関数では型を明示的に指定せずとも \verb/zero/ に適用した場合の型は自明に \verb/Nat -> Nat/である。
119 この恒等関数を利用する際は特定の型に属する値を渡すだけでその型が自動的に推論される。 119 この恒等関数を利用する際は特定の型に属する値を渡すだけでその型が自動的に推論される。
120 よって関数を利用する際は \verb/id-zero/ のように型を省略して良い。 120 よって関数を利用する際は \verb/id-zero/ のように型を省略して良い。
121 なお、関数の本体で暗黙的な引数を利用したい場合は \verb/{variableName}/ で束縛することもできる(\verb/id'/ 関数)。 121 なお、関数の本体で暗黙的な引数を利用したい場合は \verb/{variableName}/ で束縛することもできる(\verb/id'/ 関数)。
122 適用する場合も \verb/{}/でくくり、\verb/id-true/のように使用する。 122 適用する場合も \verb/{}/でくくり、\verb/id-true/のように使用する。
123 123
124 \lstinputlisting[label=src:agda-implicit-id, caption=Agdaにおける暗黙的な引数を持つ関数] {src/AgdaImplicitId.agda} 124 \lstinputlisting[label=src:agda-implicit-id, caption=Agdaにおける暗黙的な引数を持つ関数] {src/AgdaImplicitId.agda.replaced}
125 125
126 Agda には C における構造体に相当するレコード型も存在する。 126 Agda には C における構造体に相当するレコード型も存在する。
127 定義を行なう際は \verb/record/キーワードの後にレコード名、型、\verb/where/ の後に \verb/field/ キーワードを入れた後、フィールド名と型名を列挙する。 127 定義を行なう際は \verb/record/キーワードの後にレコード名、型、\verb/where/ の後に \verb/field/ キーワードを入れた後、フィールド名と型名を列挙する。
128 例えば x と y の二つの自然数からなるレコード \verb/Point/ を定義するとリスト~\ref{src:agda-record}のようになる。 128 例えば x と y の二つの自然数からなるレコード \verb/Point/ を定義するとリスト~\ref{src:agda-record}のようになる。
129 レコードを構築する際は \verb/record/ キーワードの後の \verb/{}/ の内部に \verb/fieldName = value/ の形で値を列挙していく。 129 レコードを構築する際は \verb/record/ キーワードの後の \verb/{}/ の内部に \verb/fieldName = value/ の形で値を列挙していく。
130 複数の値を列挙する際は \verb/;/ で区切る。 130 複数の値を列挙する際は \verb/;/ で区切る。
131 131
132 \lstinputlisting[label=src:agda-record, caption=Agdaにおけるレコード型の定義] {src/AgdaRecord.agda} 132 \lstinputlisting[label=src:agda-record, caption=Agdaにおけるレコード型の定義] {src/AgdaRecord.agda.replaced}
133 133
134 構築されたレコードから値を取得する際には \verb/RecordName.fieldName/ という名前の関数を適用する(リスト~\ref{src:agda-record-proj} 内2行目) 。 134 構築されたレコードから値を取得する際には \verb/RecordName.fieldName/ という名前の関数を適用する(リスト~\ref{src:agda-record-proj} 内2行目) 。
135 なお、レコードにもパターンマッチが利用できる(リスト~\ref{src:agda-record-proj} 内5行目)。 135 なお、レコードにもパターンマッチが利用できる(リスト~\ref{src:agda-record-proj} 内5行目)。
136 また、値を更新する際は \verb/record oldRecord {field = value ; ... }/ という構文を利用する。 136 また、値を更新する際は \verb/record oldRecord {field = value ; ... }/ という構文を利用する。
137 Point の中の x の値を5増やす関数 \verb/xPlus5/ はリスト~\ref{src:agda-record-proj}の 7,8行目のように書ける。 137 Point の中の x の値を5増やす関数 \verb/xPlus5/ はリスト~\ref{src:agda-record-proj}の 7,8行目のように書ける。
138 138
139 \lstinputlisting[label=src:agda-record-proj, caption=Agda におけるレコードの射影、パターンマッチ、値の更新] {src/AgdaRecordProj.agda} 139 \lstinputlisting[label=src:agda-record-proj, caption=Agda におけるレコードの射影、パターンマッチ、値の更新] {src/AgdaRecordProj.agda.replaced}
140 140
141 Agda における部分型のように振る舞う機能として Instance Arguments が存在する。 141 Agda における部分型のように振る舞う機能として Instance Arguments が存在する。
142 これはとあるデータ型が、ある型と名前を持つ関数を持つことを保証する機能であり、Haskell における型クラスや Java におけるインターフェースに相当する。 142 これはとあるデータ型が、ある型と名前を持つ関数を持つことを保証する機能であり、Haskell における型クラスや Java におけるインターフェースに相当する。
143 Agda における部分型の制約は、必要な関数を定義した record に相当し、その制約を保証するにはその record を instance として登録することになる。 143 Agda における部分型の制約は、必要な関数を定義した record に相当し、その制約を保証するにはその record を instance として登録することになる。
144 例えば、同じ型と比較することができる、という性質を表すとリスト~\ref{src:agda-type-class}のようになる。 144 例えば、同じ型と比較することができる、という性質を表すとリスト~\ref{src:agda-type-class}のようになる。
145 具体的にはとある型 A における中置関数 \verb/_==_/ を定義することに相当する。 145 具体的にはとある型 A における中置関数 \verb/_==_/ を定義することに相当する。
146 146
147 \lstinputlisting[label=src:agda-type-class, caption=Agdaにおける部分型制約] {src/AgdaTypeClass.agda} 147 \lstinputlisting[label=src:agda-type-class, caption=Agdaにおける部分型制約] {src/AgdaTypeClass.agda.replaced}
148 148
149 ある型 T がこの部分型制約を満たすことを示すには、型 T でこのレコードを作成できることを示し、それを instance 構文で登録する。 149 ある型 T がこの部分型制約を満たすことを示すには、型 T でこのレコードを作成できることを示し、それを instance 構文で登録する。
150 型Nat が Eq の上位型であることを記述するとリスト~\ref{src:agda-instance}のようになる。 150 型Nat が Eq の上位型であることを記述するとリスト~\ref{src:agda-instance}のようになる。
151 151
152 \lstinputlisting[label=src:agda-instance, caption=Agdaにおける部分型関係の構築] {src/AgdaInstance.agda} 152 \lstinputlisting[label=src:agda-instance, caption=Agdaにおける部分型関係の構築] {src/AgdaInstance.agda.replaced}
153 153
154 これで \verb/Eq/ が要求される関数に対して Nat が適用できるようになる。 154 これで \verb/Eq/ が要求される関数に対して Nat が適用できるようになる。
155 例えば型 A の要素を持つ List A から要素を探してくる elem を定義する。 155 例えば型 A の要素を持つ List A から要素を探してくる elem を定義する。
156 部分型のインスタンスは \verb/{{}}/ 内部に名前と型名で記述する。 156 部分型のインスタンスは \verb/{{}}/ 内部に名前と型名で記述する。
157 なお、名前部分は必須である。 157 なお、名前部分は必須である。
173 また、インポートを行なう際に名前を別名に変更することもでき、その際は \verb/as/ キーワードを用いる。 173 また、インポートを行なう際に名前を別名に変更することもでき、その際は \verb/as/ キーワードを用いる。
174 モジュールから特定の関数のみをインポートする場合は \verb/using/ キーワードを、関数の名前を変える時は \verb/renaming/キーワードを、特定の関数のみを隠す場合は \verb/hiding/ キーワードを用いる。 174 モジュールから特定の関数のみをインポートする場合は \verb/using/ キーワードを、関数の名前を変える時は \verb/renaming/キーワードを、特定の関数のみを隠す場合は \verb/hiding/ キーワードを用いる。
175 なお、モジュールに存在する関数をトップレベルで用いる場合は \verb/open/ キーワードを使うことで展開できる。 175 なお、モジュールに存在する関数をトップレベルで用いる場合は \verb/open/ キーワードを使うことで展開できる。
176 モジュールをインポートする例をリスト~\ref{src:agda-import}に示す。 176 モジュールをインポートする例をリスト~\ref{src:agda-import}に示す。
177 177
178 \lstinputlisting[label=src:agda-import, caption=Agdaにおけるモジュールのインポート] {src/AgdaImport.agda} 178 \lstinputlisting[label=src:agda-import, caption=Agdaにおけるモジュールのインポート] {src/AgdaImport.agda.replaced}
179 179
180 また、モジュールには値を渡すことができる。 180 また、モジュールには値を渡すことができる。
181 そのようなモジュールは Parameterized Module と呼ばれ、渡された値はそのモジュール内部で一貫して扱える。 181 そのようなモジュールは Parameterized Module と呼ばれ、渡された値はそのモジュール内部で一貫して扱える。
182 例えば要素の型と比較する二項演算子を使って並べ替えをするモジュール\verb/Sort/ を考える。 182 例えば要素の型と比較する二項演算子を使って並べ替えをするモジュール\verb/Sort/ を考える。
183 そのモジュールは引数に型Aと二項演算子 \verb/</を取り、ソートする関数を提供する。 183 そのモジュールは引数に型Aと二項演算子 \verb/</を取り、ソートする関数を提供する。
184 \verb/Sort/モジュールを \verb/Nat/ と \verb/Bool/ で利用した例がリスト~\ref{src:agda-parameterized-module}である。 184 \verb/Sort/モジュールを \verb/Nat/ と \verb/Bool/ で利用した例がリスト~\ref{src:agda-parameterized-module}である。
185 185
186 \lstinputlisting[label=src:agda-parameterized-module, caption=Agda における Parameterized Module] {src/AgdaParameterizedModule.agda} 186 \lstinputlisting[label=src:agda-parameterized-module, caption=Agda における Parameterized Module] {src/AgdaParameterizedModule.agda.replaced}
187 187
188 % }}} 188 % }}}
189 189
190 % {{{ Natural Deduction 190 % {{{ Natural Deduction
191 \section{Natural Deduction} 191 \section{Natural Deduction}
448 直積型から値を射影する関数 \verb/fst/ と \verb/snd/ を定義する。 448 直積型から値を射影する関数 \verb/fst/ と \verb/snd/ を定義する。
449 これらは Natural Deduction における $ \land 1 \mathcal{E} $ と $ \land 2 \mathcal{E} $ に相当する。 449 これらは Natural Deduction における $ \land 1 \mathcal{E} $ と $ \land 2 \mathcal{E} $ に相当する。
450 450
451 なお、直積型は型Aを持つフィールド\verb/fst/と型Bを持つフィールド\verb/snd/を持つレコード型と考えても良い。 451 なお、直積型は型Aを持つフィールド\verb/fst/と型Bを持つフィールド\verb/snd/を持つレコード型と考えても良い。
452 452
453 \lstinputlisting[label=src:agda-product, caption=Agda における直積型] {src/AgdaProduct.agda} 453 \lstinputlisting[label=src:agda-product, caption=Agda における直積型] {src/AgdaProduct.agda.replaced}
454 454
455 三段論法の証明は 「1つの仮定から $ \land 1 \mathcal{E} $ と $ \land 2 \mathcal{E} $ を用いて仮定を二つ取り出し、それぞれに $ \Rightarrow \mathcal{E} $ を適用した後に仮定を $ \Rightarrow \mathcal{I}$ で dead にする」形であった。 455 三段論法の証明は 「1つの仮定から $ \land 1 \mathcal{E} $ と $ \land 2 \mathcal{E} $ を用いて仮定を二つ取り出し、それぞれに $ \Rightarrow \mathcal{E} $ を適用した後に仮定を $ \Rightarrow \mathcal{I}$ で dead にする」形であった。
456 456
457 $ \Rightarrow \mathcal{I}$ に対応するのは関数適用である。 457 $ \Rightarrow \mathcal{I}$ に対応するのは関数適用である。
458 よってこの証明は「一つの変数から \verb/fst/ と \verb/snd/ を使って関数を二つ取り出し、それぞれを関数適用する」という形になる。 458 よってこの証明は「一つの変数から \verb/fst/ と \verb/snd/ を使って関数を二つ取り出し、それぞれを関数適用する」という形になる。
484 484
485 この定義は peano arithmetic における自然数の定義である。 485 この定義は peano arithmetic における自然数の定義である。
486 486
487 Agda で自然数型 Nat を定義するとリスト \ref{src:agda-nat-2} のようになる。 487 Agda で自然数型 Nat を定義するとリスト \ref{src:agda-nat-2} のようになる。
488 488
489 \lstinputlisting[label=src:agda-nat-2, caption=Agda における自然数型 Nat の定義] {src/Nat.agda} 489 \lstinputlisting[label=src:agda-nat-2, caption=Agda における自然数型 Nat の定義] {src/Nat.agda.replaced}
490 490
491 自然数型 Nat は2つのコンストラクタを持つ。 491 自然数型 Nat は2つのコンストラクタを持つ。
492 492
493 \begin{itemize} 493 \begin{itemize}
494 \item O 494 \item O
504 よって、数値の 3 は \verb/S (S (S O))/ のように表現される。 504 よって、数値の 3 は \verb/S (S (S O))/ のように表現される。
505 Sの個数が数値に対応する。 505 Sの個数が数値に対応する。
506 506
507 次に加算を定義する(リスト\ref{src:agda-nat-add})。 507 次に加算を定義する(リスト\ref{src:agda-nat-add})。
508 508
509 \lstinputlisting[label=src:agda-nat-add, caption=Agdaにおける自然数型に対する加算の定義] {src/NatAdd.agda} 509 \lstinputlisting[label=src:agda-nat-add, caption=Agdaにおける自然数型に対する加算の定義] {src/NatAdd.agda.replaced}
510 510
511 加算は中置関数 \verb/_+_/ として定義する。 511 加算は中置関数 \verb/_+_/ として定義する。
512 2つの Nat を取り、Natを返す。 512 2つの Nat を取り、Natを返す。
513 関数 \verb/_+_/ はパターンマッチにより処理を変える。 513 関数 \verb/_+_/ はパターンマッチにより処理を変える。
514 0に対して m 加算する場合は m であり、 n の後続数に対して m 加算する場合は n に m 加算した数の後続数とする。 514 0に対して m 加算する場合は m であり、 n の後続数に対して m 加算する場合は n に m 加算した数の後続数とする。
523 Agda において等式は、等式を示すデータ型 $ \equiv $ により定義される。 523 Agda において等式は、等式を示すデータ型 $ \equiv $ により定義される。
524 $ \equiv $ は同じ両辺が同じ項に簡約される時にコンストラクタ refl で構築できる。 524 $ \equiv $ は同じ両辺が同じ項に簡約される時にコンストラクタ refl で構築できる。
525 525
526 実際に 3 + 1 = 4 の証明は refl で構成できる(リスト\ref{src:agda-three-plus-one})。 526 実際に 3 + 1 = 4 の証明は refl で構成できる(リスト\ref{src:agda-three-plus-one})。
527 527
528 \lstinputlisting[label=src:agda-three-plus-one, caption= Agda における 3 + 1 の結果が 4 と等しい証明] {src/ThreePlusOne.agda} 528 \lstinputlisting[label=src:agda-three-plus-one, caption= Agda における 3 + 1 の結果が 4 と等しい証明] {src/ThreePlusOne.agda.replaced}
529 529
530 3+1 という関数を定義し、その型として証明すべき式を記述し、証明を関数の定義として定義する。 530 3+1 という関数を定義し、その型として証明すべき式を記述し、証明を関数の定義として定義する。
531 証明する式は \verb/(S (S (S O))) + (S O)≡(S (S (S (S O))))/ である。 531 証明する式は \verb/(S (S (S O))) + (S O)≡(S (S (S (S O))))/ である。
532 今回は \verb/_+_/ 関数の定義により \verb/ (S (S (S (S O)))) / に簡約されるためにコンストラクタ refl が証明となる。 532 今回は \verb/_+_/ 関数の定義により \verb/ (S (S (S (S O)))) / に簡約されるためにコンストラクタ refl が証明となる。
533 533
547 2つの等式に表れた同じ項を用いて2つの等式を繋げた等式は等しい。 547 2つの等式に表れた同じ項を用いて2つの等式を繋げた等式は等しい。
548 \end{itemize} 548 \end{itemize}
549 549
550 ではこれから nat の加法の交換法則を証明していく(リスト\ref{src:agda-nat-add-sym})。 550 ではこれから nat の加法の交換法則を証明していく(リスト\ref{src:agda-nat-add-sym})。
551 551
552 \lstinputlisting[label=src:agda-nat-add-sym, caption= Agda における加法の交換法則の証明] {src/NatAddSym.agda} 552 \lstinputlisting[label=src:agda-nat-add-sym, caption= Agda における加法の交換法則の証明] {src/NatAddSym.agda.replaced}
553 553
554 証明する式は $ n + m \equiv m + n $ である。 554 証明する式は $ n + m \equiv m + n $ である。
555 n と m は Nat であるため、それぞれがコンストラクタ O か S により構成される。 555 n と m は Nat であるため、それぞれがコンストラクタ O か S により構成される。
556 そのためにパターンは4通りある。 556 そのためにパターンは4通りある。
557 557