Mercurial > hg > Members > kono > Proof > automaton
annotate a02/lecture.ind @ 287:ce16779e72a5
fix decrement case
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Tue, 28 Dec 2021 03:17:29 +0900 |
| parents | e5cf49902db3 |
| children | a3fb231feeb9 |
| 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 | |
| 25 | |
| 26 --あらすじ | |
| 27 | |
| 28 1) 論理式を変数とそれを結ぶ演算子(connectives)で定義する | |
| 29 これは構文定義、あるいは、論理式の作り方に相当する | |
| 30 | |
| 31 2) 演算子を導入する推論と、除去する推論を定義する。 | |
| 32 これには証明図を使う | |
| 33 | |
| 34 3) 推論に対応する関数を表す項を考える | |
| 35 項は関数型言語の要素になる | |
| 36 | |
| 37 項の導入 ... データ構造のconstructor | |
| 38 項の除去 ... データ構造のaccesor | |
| 39 | |
| 40 導入は関数の出力の型に現れる | |
| 41 除去は関数の入力の型に現れる | |
| 42 | |
| 43 これを演算子の数の分だけ繰り返す。 | |
| 44 | |
| 45 次に等式論理を学ぶ。 | |
| 46 | |
| 47 4) x = x の導入と除去 | |
| 48 | |
| 49 5) 項が等しいとはとういうことかを学ぶ | |
| 50 正規形 | |
| 51 | |
| 52 正規形を得ることが関数型言語の計算(項の操作) | |
| 53 | |
| 54 以上のことを Agda (Haskell に似た構文を持つ証明支援系)で記述する。 | |
| 55 | |
| 56 --証明の基本 | |
| 57 | |
| 58 A は論理式を表す変数。あるいは型Aという集合。論理式は変数と論理演算子で表される木構造。変数や演算子は構文要素。 | |
| 59 | |
| 60 A → B | |
| 61 | |
| 62 これは「AならばB」というのに対応する。関数の視点からは、Aという型からBという型への関数。 | |
| 63 AとBは型を表す論理式。 | |
| 64 | |
| 65 A | |
| 66 ----------- | |
| 67 B | |
| 68 | |
| 69 Aを仮定して、Bが証明されたことを表す図。証明図。 | |
| 70 | |
| 71 --関数適用による証明 | |
| 72 | |
| 266 | 73 導入 除去 |
| 37 | 74 |
| 75 A | |
| 76 : | |
| 77 B A A → B | |
| 78 ------------- ------------------ | |
| 79 A → B B | |
| 80 | |
| 81 対応する項。項とは、関数型プログラムを構成する構文要素。木構造で表される。 | |
| 82 | |
| 83 | |
| 84 λ x → y | |
| 85 | |
| 86 x は変数、y は項。y は複雑な項(関数のbody)でも良い。これは構文定義でもある。変数 x と項yから | |
| 87 λ x → y という項を作れる。 x は構文的にスコープを持っている。つまり、関数の引数と同じ扱いとする。 | |
| 88 | |
| 89 項には型が対応する。これは、再帰的に定義される | |
| 90 | |
| 91 x : A | |
| 92 | |
| 93 は、x という項が型Aを持つと言うのを表している。 | |
| 94 | |
| 95 x : A かつ y : B の時に、 | |
| 96 | |
| 97 λ x → y : A → B | |
| 98 | |
| 99 と定義する。 | |
| 100 | |
| 101 | |
| 102 | |
| 103 ---Agdaの構文 | |
| 104 | |
| 53 | 105 <a href="agda-install.html"> Agda のinstallの方法 </a> |
| 106 <br> | |
| 107 | |
| 37 | 108 型と値 |
| 109 | |
| 110 名前の作り方 | |
| 111 | |
| 112 indent | |
| 113 | |
| 114 implicit variable | |
| 115 | |
| 116 infix operator and operator order | |
| 117 | |
| 118 <a href="agda.html"> agda の細かい構文の話 </a> | |
| 119 | |
| 266 | 120 Unicode入力 |
| 121 | |
| 122 <a href="https://agda.readthedocs.io/en/v2.6.0.1/tools/emacs-mode.html"> Unicode入力 </a> | |
| 123 | |
| 124 --重要 | |
| 125 | |
| 126 空白が入らないものは一単語になる (A→A は一単語、A → A とは別) | |
| 127 | |
| 128 A:Set は間違いで、A : Set | |
| 129 | |
| 130 A → B → C は、 A → ( B → C ) のこと | |
| 131 | |
| 132 f x y は (f x) y のこと | |
| 133 | |
| 53 | 134 |
| 135 ---問題2.1 Agdaによる関数と証明 | |
| 136 | |
| 137 | |
| 138 以下の agda の ? の部分を埋めよ。対応する証明図をコメントで書くこと。 | |
| 139 | |
| 140 <a href="agda/lambda.agda"> lambda </a> <!--- Exercise 2.1 ---> | |
| 141 | |
| 142 | |
| 37 | 143 --record または ∧ |
| 144 | |
| 266 | 145 導入 除去 |
| 37 | 146 |
| 147 A B A ∧ B A ∧ B | |
| 148 ------------- ----------- π1 ---------- π2 | |
| 149 A ∧ B A B | |
| 150 | |
| 151 除去は複数あるので名前を区別する必要がある。つまり、それぞれに項を用意する必要がある。 | |
| 152 | |
| 153 A ∧ B は新しく導入した型である。 | |
| 154 型Aと型Bから作るデータ構造であり、オブジェクトあるいは構造体だと思って良い。 | |
| 155 π1 π2 は構造体から field を抜き出す accesor によって実装できる。 | |
| 156 | |
| 157 | |
| 158 | |
| 159 record によって | |
| 160 | |
| 161 record _∧_ A B : Set | |
| 162 field | |
| 163 π1 : A | |
| 164 π2 : B | |
| 165 | |
| 166 _∧_ は中置演算子を表す。 | |
| 167 | |
| 168 _∧_ A B | |
| 169 | |
| 170 は | |
| 171 | |
| 172 A ∧ B | |
| 173 | |
| 174 とかける。(Haskell では (∧) を使う) | |
| 175 | |
| 176 は、型Aと型Bから作るデ0ータ構造である。オブジェクトあるいは構造体だと思って良い。 | |
| 177 | |
| 178 record { π1 = x ; π2 = y } | |
| 179 | |
| 180 | |
| 181 ---例題 | |
| 182 | |
| 183 A → B ∧ B → C → A → C | |
| 184 | |
| 185 まず、正しくかっこを付ける。 | |
| 186 | |
| 187 (( A → B ) ∧ ( B → C )) → ( A → C ) | |
| 188 | |
| 189 線を上に引く。 | |
| 190 | |
| 191 : | |
| 192 ------------------------------------------------- | |
| 193 (( A → B ) ∧ ( B → C )) → ( A → C ) | |
| 194 | |
| 195 : はこれから埋めていく部分。まず適用するのは→のintro duction である。 ( A → B ) ∧ ( B → C )を仮定で使えるようになる。 | |
| 196 | |
| 197 : | |
| 198 A → C | |
| 199 ------------------------------------------------- | |
| 200 (( A → B ) ∧ ( B → C )) → ( A → C ) | |
| 201 | |
| 202 さらに→introを使う。Aを仮定で使えるようになる。 | |
| 203 | |
| 204 : | |
| 205 C | |
| 206 ------------------------------------------------- | |
| 207 A → C | |
| 208 ------------------------------------------------- | |
| 209 (( A → B ) ∧ ( B → C )) → ( A → C ) | |
| 210 | |
| 211 仮定でCを生成できるのは B → C しかない。 | |
| 212 | |
| 213 B B → C | |
| 214 --------------------- | |
| 215 C | |
| 216 | |
| 217 これは→elim である。 B → C は仮定( A → B ) ∧ ( B → C )の左側が使える | |
| 218 | |
| 219 ( A → B ) ∧ ( B → C ) | |
| 220 --------------------- π2 | |
| 221 B → C | |
| 222 | |
| 223 B の方もがんばると、最終的に | |
| 224 | |
| 225 [ ( A → B ) ∧ ( B → C )]*1 | |
| 226 --------------------------------- π1 | |
| 227 [A]*2 A → B [ ( A → B ) ∧ ( B → C ) ]*1 | |
| 228 ---------------- →elim ------------------------------- π2 | |
| 229 B B → C | |
| 230 ----------------------------------------------- →elim | |
| 231 C | |
| 232 ------------------------------------------------- →intro 2 | |
| 233 A → C | |
| 234 ------------------------------------------------- →intro 1 | |
| 235 (( A → B ) ∧ ( B → C )) → ( A → C ) | |
| 236 | |
| 237 となる。 | |
| 238 | |
| 239 Agda では、 | |
| 240 | |
| 241 lemma : (( A → B ) ∧ ( B → C )) → ( A → C ) | |
| 242 lemma = ? | |
| 243 | |
| 244 とすると、A B C が未定義だと言われる。 | |
| 245 | |
| 246 lemma : {A B C : Set } → (( A → B ) ∧ ( B → C )) → ( A → C ) | |
| 247 lemma = ? | |
| 248 | |
| 249 引数が一つあるので、それに名前を付ける。 | |
| 250 | |
| 251 lemma : {A B C : Set } → (( A → B ) ∧ ( B → C )) → ( A → C ) | |
| 252 lemma f∧g = ? | |
| 253 | |
| 254 いや引数は二つだった。 | |
| 255 | |
| 256 lemma : {A B C : Set } → (( A → B ) ∧ ( B → C )) → ( A → C ) | |
| 257 lemma f∧g a = ? | |
| 258 | |
| 259 f∧g は直積なので、 | |
| 260 | |
| 261 π1 f∧g : A → B | |
| 262 π2 f∧g : B → C | |
| 263 | |
| 264 なことを考えると、 | |
| 265 | |
| 266 lemma : {A B C : Set } → (( A → B ) ∧ ( B → C )) → ( A → C ) | |
| 267 lemma f∧g a = π2 f∧g ? | |
| 268 | |
| 269 ここで、π2 f∧g ? は (π2 f∧g) ? であることを思い出そう。最終的に、 | |
| 270 | |
| 271 lemma : {A B C : Set } → (( A → B ) ∧ ( B → C )) → ( A → C ) | |
| 272 lemma f∧g a = π2 f∧g (π1 f∧g) a | |
| 273 | |
| 274 (ここで、(π2 f∧g (π1 f∧g)) a と書かなくても良いのは何故か?) | |
| 275 | |
| 276 前の証明図と、Agdaで証明とどこがどう対応しているのかを考えてみよう。 | |
| 277 | |
| 53 | 278 ---問題2.2 Agdaによる関数と証明 |
| 279 | |
| 37 | 280 |
| 281 以下の agda の ? の部分を埋めよ。対応する証明図をコメントで書くこと。 | |
| 282 | |
|
104
fba1cd54581d
use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
59
diff
changeset
|
283 最低限5題をまとめてレポートで提出せよ |
|
fba1cd54581d
use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
59
diff
changeset
|
284 |
| 266 | 285 <a href="agda/record1.agda"> record1</a> <!--- Exercise 2.2 ---> |
| 55 | 286 |
| 266 | 287 --Sum type |
| 37 | 288 |
| 266 | 289 <a href="sumtype.html"> Sum type 排他的論理和</a> |
| 37 | 290 |
| 291 |