Mercurial > hg > Members > kono > Proof > automaton
annotate a02/lecture.ind @ 406:a60132983557
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Wed, 08 Nov 2023 21:35:54 +0900 |
| parents | 407684f806e4 |
| children |
| rev | line source |
|---|---|
| 37 | 1 -title: 証明と関数型言語、Agda |
| 2 | |
| 3 問題は、メールでSubjectを (a01 の 問題2.5ならば) | |
| 139 | 4 Subject: Report on Automaton Lecture 2.5 |
| 37 | 5 として、問題毎に提出すること。 |
| 6 | |
| 7 kono@ie.u-ryukyu.ac.jp まで送ること。 | |
| 8 番号のついてない問題はオプションです。 | |
| 9 | |
| 10 学籍番号をメールの中に記述すること。 | |
| 11 問題番号は正確に記述すること。 | |
| 12 出席しない場合でも、問題解答を送れば出席扱いとします。 | |
| 13 | |
| 14 提出期限は ura.ie.classes.automaton で知らせます。 | |
| 15 | |
| 16 | |
| 17 --証明と関数型言語の関係 | |
| 18 | |
| 19 証明とは、論理式それを結ぶ推論からなる数学的な構造である。また、関数型言語は集合である型とそれを結ぶ関数からなる数学的構造である。 | |
| 20 | |
| 21 型つきλ計算と論理が対応するように、データ構造と論理演算子(∧とか∨)を対応させることにより | |
| 22 | |
| 23 論理式を型として表し、推論を型つきλ計算の項とすると、この二つは似ていることがわかる。 | |
| 24 | |
| 406 | 25 この章の内容は基本的には Girad 先生の Proofs and Typesに書いてある内容です。 |
| 37 | 26 |
| 27 --あらすじ | |
| 28 | |
| 29 1) 論理式を変数とそれを結ぶ演算子(connectives)で定義する | |
| 30 これは構文定義、あるいは、論理式の作り方に相当する | |
| 31 | |
| 32 2) 演算子を導入する推論と、除去する推論を定義する。 | |
| 33 これには証明図を使う | |
| 34 | |
| 35 3) 推論に対応する関数を表す項を考える | |
| 36 項は関数型言語の要素になる | |
| 37 | |
| 38 項の導入 ... データ構造のconstructor | |
| 39 項の除去 ... データ構造のaccesor | |
| 40 | |
| 41 導入は関数の出力の型に現れる | |
| 42 除去は関数の入力の型に現れる | |
| 43 | |
| 44 これを演算子の数の分だけ繰り返す。 | |
| 45 | |
| 46 次に等式論理を学ぶ。 | |
| 47 | |
| 48 4) x = x の導入と除去 | |
| 49 | |
| 50 5) 項が等しいとはとういうことかを学ぶ | |
| 51 正規形 | |
| 52 | |
| 53 正規形を得ることが関数型言語の計算(項の操作) | |
| 54 | |
| 55 以上のことを Agda (Haskell に似た構文を持つ証明支援系)で記述する。 | |
| 56 | |
| 57 --証明の基本 | |
| 58 | |
| 59 A は論理式を表す変数。あるいは型Aという集合。論理式は変数と論理演算子で表される木構造。変数や演算子は構文要素。 | |
| 60 | |
| 61 A → B | |
| 62 | |
| 63 これは「AならばB」というのに対応する。関数の視点からは、Aという型からBという型への関数。 | |
| 64 AとBは型を表す論理式。 | |
| 65 | |
| 66 A | |
| 67 ----------- | |
| 68 B | |
| 69 | |
| 70 Aを仮定して、Bが証明されたことを表す図。証明図。 | |
| 71 | |
| 72 --関数適用による証明 | |
| 73 | |
| 266 | 74 導入 除去 |
| 37 | 75 |
| 76 A | |
| 77 : | |
| 78 B A A → B | |
| 79 ------------- ------------------ | |
| 80 A → B B | |
| 81 | |
| 82 対応する項。項とは、関数型プログラムを構成する構文要素。木構造で表される。 | |
| 83 | |
| 84 | |
| 85 λ x → y | |
| 86 | |
| 87 x は変数、y は項。y は複雑な項(関数のbody)でも良い。これは構文定義でもある。変数 x と項yから | |
| 88 λ x → y という項を作れる。 x は構文的にスコープを持っている。つまり、関数の引数と同じ扱いとする。 | |
| 89 | |
| 90 項には型が対応する。これは、再帰的に定義される | |
| 91 | |
| 92 x : A | |
| 93 | |
| 94 は、x という項が型Aを持つと言うのを表している。 | |
| 95 | |
| 96 x : A かつ y : B の時に、 | |
| 97 | |
| 98 λ x → y : A → B | |
| 99 | |
| 100 と定義する。 | |
| 101 | |
| 102 | |
| 103 | |
| 104 ---Agdaの構文 | |
| 105 | |
| 53 | 106 <a href="agda-install.html"> Agda のinstallの方法 </a> |
| 107 <br> | |
| 108 | |
| 37 | 109 型と値 |
| 110 | |
| 111 名前の作り方 | |
| 112 | |
| 113 indent | |
| 114 | |
| 115 implicit variable | |
| 116 | |
| 117 infix operator and operator order | |
| 118 | |
| 119 <a href="agda.html"> agda の細かい構文の話 </a> | |
| 120 | |
| 266 | 121 Unicode入力 |
| 122 | |
| 123 <a href="https://agda.readthedocs.io/en/v2.6.0.1/tools/emacs-mode.html"> Unicode入力 </a> | |
| 124 | |
| 330 | 125 --Agda introduction |
| 126 | |
| 127 <a href="https://gitlab.ie.u-ryukyu.ac.jp/teacher/kono/agda-introduction"> Agda introduction </a> | |
| 128 | |
| 266 | 129 --重要 |
| 130 | |
| 131 空白が入らないものは一単語になる (A→A は一単語、A → A とは別) | |
| 132 | |
| 133 A:Set は間違いで、A : Set | |
| 134 | |
| 135 A → B → C は、 A → ( B → C ) のこと | |
| 136 | |
| 137 f x y は (f x) y のこと | |
| 138 | |
| 53 | 139 |
| 140 ---問題2.1 Agdaによる関数と証明 | |
| 141 | |
| 142 | |
| 143 以下の agda の ? の部分を埋めよ。対応する証明図をコメントで書くこと。 | |
| 144 | |
| 145 <a href="agda/lambda.agda"> lambda </a> <!--- Exercise 2.1 ---> | |
| 146 | |
| 147 | |
| 37 | 148 --record または ∧ |
| 149 | |
| 266 | 150 導入 除去 |
| 37 | 151 |
| 152 A B A ∧ B A ∧ B | |
| 153 ------------- ----------- π1 ---------- π2 | |
| 154 A ∧ B A B | |
| 155 | |
| 156 除去は複数あるので名前を区別する必要がある。つまり、それぞれに項を用意する必要がある。 | |
| 157 | |
| 158 A ∧ B は新しく導入した型である。 | |
| 159 型Aと型Bから作るデータ構造であり、オブジェクトあるいは構造体だと思って良い。 | |
| 160 π1 π2 は構造体から field を抜き出す accesor によって実装できる。 | |
| 161 | |
| 162 | |
| 163 | |
| 164 record によって | |
| 165 | |
| 406 | 166 record _∧_ A B : Set where |
| 37 | 167 field |
| 168 π1 : A | |
| 169 π2 : B | |
| 170 | |
| 171 _∧_ は中置演算子を表す。 | |
| 172 | |
| 173 _∧_ A B | |
| 174 | |
| 175 は | |
| 176 | |
| 177 A ∧ B | |
| 178 | |
| 179 とかける。(Haskell では (∧) を使う) | |
| 180 | |
| 406 | 181 は、型Aと型Bから作るデータ構造である。オブジェクトあるいは構造体だと思って良い。 |
| 37 | 182 |
| 183 record { π1 = x ; π2 = y } | |
| 184 | |
| 185 | |
| 186 ---例題 | |
| 187 | |
| 188 A → B ∧ B → C → A → C | |
| 189 | |
| 190 まず、正しくかっこを付ける。 | |
| 191 | |
| 192 (( A → B ) ∧ ( B → C )) → ( A → C ) | |
| 193 | |
| 194 線を上に引く。 | |
| 195 | |
| 196 : | |
| 197 ------------------------------------------------- | |
| 198 (( A → B ) ∧ ( B → C )) → ( A → C ) | |
| 199 | |
| 200 : はこれから埋めていく部分。まず適用するのは→のintro duction である。 ( A → B ) ∧ ( B → C )を仮定で使えるようになる。 | |
| 201 | |
| 202 : | |
| 203 A → C | |
| 204 ------------------------------------------------- | |
| 205 (( A → B ) ∧ ( B → C )) → ( A → C ) | |
| 206 | |
| 207 さらに→introを使う。Aを仮定で使えるようになる。 | |
| 208 | |
| 209 : | |
| 210 C | |
| 211 ------------------------------------------------- | |
| 212 A → C | |
| 213 ------------------------------------------------- | |
| 214 (( A → B ) ∧ ( B → C )) → ( A → C ) | |
| 215 | |
| 216 仮定でCを生成できるのは B → C しかない。 | |
| 217 | |
| 218 B B → C | |
| 219 --------------------- | |
| 220 C | |
| 221 | |
| 222 これは→elim である。 B → C は仮定( A → B ) ∧ ( B → C )の左側が使える | |
| 223 | |
| 224 ( A → B ) ∧ ( B → C ) | |
| 225 --------------------- π2 | |
| 226 B → C | |
| 227 | |
| 228 B の方もがんばると、最終的に | |
| 229 | |
| 230 [ ( A → B ) ∧ ( B → C )]*1 | |
| 231 --------------------------------- π1 | |
| 232 [A]*2 A → B [ ( A → B ) ∧ ( B → C ) ]*1 | |
| 233 ---------------- →elim ------------------------------- π2 | |
| 234 B B → C | |
| 235 ----------------------------------------------- →elim | |
| 236 C | |
| 237 ------------------------------------------------- →intro 2 | |
| 238 A → C | |
| 239 ------------------------------------------------- →intro 1 | |
| 240 (( A → B ) ∧ ( B → C )) → ( A → C ) | |
| 241 | |
| 242 となる。 | |
| 243 | |
| 244 Agda では、 | |
| 245 | |
| 246 lemma : (( A → B ) ∧ ( B → C )) → ( A → C ) | |
| 247 lemma = ? | |
| 248 | |
| 249 とすると、A B C が未定義だと言われる。 | |
| 250 | |
| 251 lemma : {A B C : Set } → (( A → B ) ∧ ( B → C )) → ( A → C ) | |
| 252 lemma = ? | |
| 253 | |
| 254 引数が一つあるので、それに名前を付ける。 | |
| 255 | |
| 256 lemma : {A B C : Set } → (( A → B ) ∧ ( B → C )) → ( A → C ) | |
| 257 lemma f∧g = ? | |
| 258 | |
| 259 いや引数は二つだった。 | |
| 260 | |
| 261 lemma : {A B C : Set } → (( A → B ) ∧ ( B → C )) → ( A → C ) | |
| 262 lemma f∧g a = ? | |
| 263 | |
| 264 f∧g は直積なので、 | |
| 265 | |
| 266 π1 f∧g : A → B | |
| 267 π2 f∧g : B → C | |
| 268 | |
| 269 なことを考えると、 | |
| 270 | |
| 271 lemma : {A B C : Set } → (( A → B ) ∧ ( B → C )) → ( A → C ) | |
| 272 lemma f∧g a = π2 f∧g ? | |
| 273 | |
| 274 ここで、π2 f∧g ? は (π2 f∧g) ? であることを思い出そう。最終的に、 | |
| 275 | |
| 276 lemma : {A B C : Set } → (( A → B ) ∧ ( B → C )) → ( A → C ) | |
| 277 lemma f∧g a = π2 f∧g (π1 f∧g) a | |
| 278 | |
| 279 (ここで、(π2 f∧g (π1 f∧g)) a と書かなくても良いのは何故か?) | |
| 280 | |
| 281 前の証明図と、Agdaで証明とどこがどう対応しているのかを考えてみよう。 | |
| 282 | |
| 53 | 283 ---問題2.2 Agdaによる関数と証明 |
| 284 | |
| 37 | 285 |
| 286 以下の agda の ? の部分を埋めよ。対応する証明図をコメントで書くこと。 | |
| 287 | |
|
104
fba1cd54581d
use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
59
diff
changeset
|
288 最低限5題をまとめてレポートで提出せよ |
|
fba1cd54581d
use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
59
diff
changeset
|
289 |
| 266 | 290 <a href="agda/record1.agda"> record1</a> <!--- Exercise 2.2 ---> |
| 55 | 291 |
| 326 | 292 --data -- Sum type |
| 293 | |
| 294 record は ∧ に対応するが、∨はどうすれば良いのか。残念ながら∧と対称につくることはできない。(なぜか?) | |
| 295 | |
| 296 Agda では data という場合分けをする型を導入する。Curry Howard対応が成立する様に、論理記号に対応する | |
| 297 型を導入する。型には導入と削除がある。 | |
| 298 | |
| 299 導入のない data を定義すると、それを矛盾として使うことができる。それを使って否定を定義する。 | |
| 300 | |
| 301 さらに | |
| 302 | |
| 303 有限な要素を持つ集合(型) | |
| 304 自然数 | |
| 305 λ項の等しさとしての等式 | |
| 306 不等号 | |
| 307 | |
| 308 も data を使って定義できる。 | |
| 309 | |
| 310 data は invariant あるいは、制約付きのデータ構造を表すこともできる。 | |
| 311 | |
| 312 さらに、 | |
| 313 | |
| 314 規則にしたがって生成される集合 | |
| 315 | |
| 316 も表すことができる。一つ一つ、ゆっくり片付けていこう。 | |
| 37 | 317 |
| 266 | 318 <a href="sumtype.html"> Sum type 排他的論理和</a> |
| 37 | 319 |
| 326 | 320 以下は必要に応じて説明していく。 |
| 37 | 321 |
| 326 | 322 --λ計算の進み方 |
| 323 | |
| 324 Agda の値と型は項で定義されていて、それを簡約化することにより計算が進む。 | |
| 325 | |
| 326 Agda (そして Haskell )は、項を簡約化していくことにより計算が進むプログラミング言語である。 | |
| 327 | |
| 328 簡約化の順序には自由度があり、それは実装にって変わる。 | |
| 329 | |
| 330 関数適用にる置き換え | |
| 331 場合分けによる変数の確定 | |
| 332 確定した変数での置き換え | |
| 333 | |
| 334 自由度に関係なく、項は決まった形に簡約化されるようにλ計算は作られている。(合流性 -- 要証明だが、割と難しい) | |
| 335 | |
| 336 (Agda で Agda を実装できるのか?) | |
| 337 | |
| 338 合流性があるので、data で定義された等号が正しく動作する。 | |
| 339 | |
| 340 変数が含まれている場合の等号は単一化と呼ばれる。変数の置き換えが置きるのは data の場合分けと、関数呼び出しの二種類になる。 | |
| 341 | |
| 342 --停止性の問題 | |
| 343 | |
| 344 入力を data の場合分けで分解していくことは、入力が決まった大きさの項なので、必ず有限回しかできない。 | |
| 345 | |
| 346 つまり、そういう計算が止まることは Agda にはわかる。例えば List や Nat の分解である。 | |
| 347 | |
| 348 分解は再帰的なので、再帰呼び出しがとまるかどうかは、再帰呼び出しの引数が、dataの分解になっているかどうかで判断される。 | |
| 349 | |
| 350 これは一般的なプログラムでは自明にはならない。その時には型チェックエラーになる。 {-# TERMINATING #-} を指定することにより | |
| 351 それを抑制できる。その場合は、そういう止まるとすればという仮定を持つ計算あるいは証明になる。 | |
| 352 | |
| 353 -- induction | |
| 354 | |
| 355 自明な停止条件でない推論もいくつかある。 | |
| 356 | |
| 357 引数が直接 data を分解しないが、引数が減少する自然数に対応する場合 | |
| 358 生成される引数パターンが有限だと分かっている場合 | |
| 359 | |
| 360 の二つの場合は Agda で induction を定義できる。 | |
| 361 | |
| 362 --古典論理、一階述語論理との差 | |
| 363 | |
| 364 Agda の → ∧ ∨ は、項の型として定義されている。 | |
| 365 | |
| 366 _∧_ : Set → Set → Set | |
| 367 | |
| 368 古典論理では真と偽の二つしかない。 | |
| 369 | |
| 370 data Bool : Set where | |
| 371 true : Bool | |
| 372 false : Bool | |
| 373 | |
| 374 この差は、二重否定の扱いに現れる。 | |
| 375 | |
| 376 _/\_ : Bool → Bool → Bool | |
| 377 true /\ true = true | |
| 378 _ /\ _ = false | |
| 379 | |
| 380 _\/_ : Bool → Bool → Bool | |
| 381 false \/ false = false | |
| 382 _ \/ _ = true | |
| 383 | |
| 384 not_ : Bool → Bool | |
| 385 not true = false | |
| 386 not false = true | |
| 387 | |
| 388 | |
| 389 とする。 | |
| 390 | |
| 391 以下は Bool では証明できるが、Set では示せない。 | |
| 392 | |
| 393 lem-in-bool : (b : Bool) → not p \/ p | |
| 394 lem-in-bool = ? | |
| 395 | |
| 396 double-negation-bool : {B : Bool} → not (not B) → B | |
| 397 double-negation-bool = ? | |
| 398 | |
| 399 Set の方では対偶は一方向しか成立しない。また、二重否定や排中律も成立しない。 | |
| 400 | |
| 401 contra-position : {n m : Level } {A : Set n} {B : Set m} → (A → B) → ¬ B → ¬ A | |
| 402 contra-position {n} {m} {A} {B} f ¬b a ? | |
| 403 | |
| 404 これは、Agdaの Set が具体的なλ項を要求するためである。つまり、 | |
| 405 | |
| 406 実際に構成できる証明しか Set は受け付けない | |
| 407 | |
| 408 Bool の場合は最初から true / false がわかっている。Set の場合は、そこに入る項がある、入らないことを証明する項がある。 | |
| 409 そして、どちらかわからない場合がある。 | |
| 410 | |
| 411 実際にわからない場合があることが証明されている(不完全性定理)。一方で、 | |
| 412 | |
| 413 証明するべき式が恒真(すべての可能な入力について真)なら、証明がある(完全性) | |
| 414 | |
| 415 であることも証明されている。恒真かどうかはわからないので、この二つは矛盾しない。 | |
| 416 | |
| 417 | |
| 418 --一階述語論理の定義 | |
| 419 | |
| 420 Agda を使って一階述語論理を定義することもできる。 | |
| 421 | |
| 422 | |
| 423 | |
| 424 | |
| 425 | |
| 426 | |
| 427 | |
| 428 | |
| 429 | |
| 430 | |
| 330 | 431 ---問題2.3 sum type の問題 |
| 432 | |
| 433 問題2.9 まで | |
| 434 | |
| 435 <a href=""> </a> <!--- Exercise 2.3 ---> | |
| 436 <a href=""> </a> <!--- Exercise 2.4 ---> | |
| 437 <a href=""> </a> <!--- Exercise 2.5 ---> | |
| 438 <a href=""> </a> <!--- Exercise 2.6 ---> | |
| 439 <a href=""> </a> <!--- Exercise 2.7 ---> | |
| 440 <a href=""> </a> <!--- Exercise 2.8 ---> | |
| 441 <a href=""> </a> <!--- Exercise 2.9 ---> | |
| 442 <a href=""> </a> <!--- Exercise 2.8 ---> | |
| 443 <a href=""> </a> <!--- Exercise 2.9 ---> | |
| 444 | |
| 445 |