Mercurial > hg > Members > atton > generated_seminar_slides

annotate slides/20140520/slide.md @ 21:203db669ee3e

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
auto-Update generated slides by script
author Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
date Tue, 20 May 2014 18:04:50 +0900
parents
children
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
rev   line source
21
203db669ee3e auto-Update generated slides by script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
1 title: Agda 入門
203db669ee3e auto-Update generated slides by script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
2 author: Yasutaka Higa
203db669ee3e auto-Update generated slides by script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
3 cover:
203db669ee3e auto-Update generated slides by script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
4 lang: Japanese
203db669ee3e auto-Update generated slides by script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
5
203db669ee3e auto-Update generated slides by script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
6
203db669ee3e auto-Update generated slides by script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
7 # このセミナーの目的
203db669ee3e auto-Update generated slides by script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
8 * 証明支援系の言語である Agda の入門を目的としています
203db669ee3e auto-Update generated slides by script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
9 * 具体的には
203db669ee3e auto-Update generated slides by script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
10 * Agda による証明の方法を知る
203db669ee3e auto-Update generated slides by script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
11 * 実際に自然数の加算の交換法則の証明を追う
203db669ee3e auto-Update generated slides by script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
12
203db669ee3e auto-Update generated slides by script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
13
203db669ee3e auto-Update generated slides by script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
14 # セミナーについて必要する事前知識
203db669ee3e auto-Update generated slides by script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
15 * なお、このセミナーについては
203db669ee3e auto-Update generated slides by script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
16 * C や Java によるプログラミング言語を書いたことがある
203db669ee3e auto-Update generated slides by script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
17 * 関数や引数、型といった単語の詳細は省略することがあります
203db669ee3e auto-Update generated slides by script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
18 * 数学における述語論理
203db669ee3e auto-Update generated slides by script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
19 * P ならば Q といった論理
203db669ee3e auto-Update generated slides by script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
20 * といったことを前提条件としています
203db669ee3e auto-Update generated slides by script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
21
203db669ee3e auto-Update generated slides by script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
22
203db669ee3e auto-Update generated slides by script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
23 # Agda とはどういう言語なのか
203db669ee3e auto-Update generated slides by script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
24 * 証明支援系と呼ばれる分野の言語です
203db669ee3e auto-Update generated slides by script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
25 * 他には Coq などがあります
203db669ee3e auto-Update generated slides by script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
26 * Haskell で実装されています
203db669ee3e auto-Update generated slides by script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
27 * dependent type の言語 です
203db669ee3e auto-Update generated slides by script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
28 * 型から生成さえれた型を扱える
203db669ee3e auto-Update generated slides by script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
29 * いわゆる「強い静的型付け」などと言われる種類です
203db669ee3e auto-Update generated slides by script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
30
203db669ee3e auto-Update generated slides by script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
31
203db669ee3e auto-Update generated slides by script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
32 # 型と証明との対応 : Curry-Howard Isomorphism
203db669ee3e auto-Update generated slides by script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
33 * Agda における証明は
203db669ee3e auto-Update generated slides by script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
34 * 証明したい命題 == 関数の型
203db669ee3e auto-Update generated slides by script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
35 * 命題の証明 == 関数の定義
203db669ee3e auto-Update generated slides by script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
36 * として定義します。
203db669ee3e auto-Update generated slides by script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
37 * 関数と命題の対応を Curry-Howard Isomorphism と言います
203db669ee3e auto-Update generated slides by script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
38
203db669ee3e auto-Update generated slides by script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
39
203db669ee3e auto-Update generated slides by script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
40 # 'A ならば B' と 'A' が成り立つなら 'B'
203db669ee3e auto-Update generated slides by script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
41
203db669ee3e auto-Update generated slides by script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
42 * Agda において
203db669ee3e auto-Update generated slides by script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
43 * apply : A -> (A -> B) -> B
203db669ee3e auto-Update generated slides by script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
44 * apply a f = f a
203db669ee3e auto-Update generated slides by script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
45 * と記述します
203db669ee3e auto-Update generated slides by script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
46
203db669ee3e auto-Update generated slides by script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
47
203db669ee3e auto-Update generated slides by script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
48 # Agda のSyntax
203db669ee3e auto-Update generated slides by script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
49 * apply : A -> (A -> B) -> B
203db669ee3e auto-Update generated slides by script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
50 * apply a f = f a
203db669ee3e auto-Update generated slides by script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
51
203db669ee3e auto-Update generated slides by script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
52 * 関数名 : 型
203db669ee3e auto-Update generated slides by script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
53 * 関数名 <引数,,,> = 定義
203db669ee3e auto-Update generated slides by script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
54
203db669ee3e auto-Update generated slides by script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
55
203db669ee3e auto-Update generated slides by script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
56 # Agda の型のSyntax
203db669ee3e auto-Update generated slides by script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
57 * apply : A -> (A -> B) -> B
203db669ee3e auto-Update generated slides by script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
58
203db669ee3e auto-Update generated slides by script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
59 * 引数の型 -> 返り値の型
203db669ee3e auto-Update generated slides by script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
60 * 結合は右結合です。なのでこのようになります
203db669ee3e auto-Update generated slides by script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
61 * A -> ((A -> B) -> B)
203db669ee3e auto-Update generated slides by script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
62 * 右結合のため、A を受けとって ((A -> B) -> B) を返す、とも読めます
203db669ee3e auto-Update generated slides by script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
63
203db669ee3e auto-Update generated slides by script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
64
203db669ee3e auto-Update generated slides by script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
65 # Agda の型のSyntax : 複数の引数
203db669ee3e auto-Update generated slides by script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
66 * 複数の引数は
203db669ee3e auto-Update generated slides by script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
67 * Arg1Type -> Arg2Type -> ReturnType
203db669ee3e auto-Update generated slides by script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
68 * のように書きますが、右結合により
203db669ee3e auto-Update generated slides by script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
69 * Arg1Type -> (Arg2Type -> ReturnType)
203db669ee3e auto-Update generated slides by script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
70 * となり、引数は1つしかないと考えることができます。
203db669ee3e auto-Update generated slides by script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
71 * これを Curry 化と言い、引数が複数の場合を考えずに良くなります
203db669ee3e auto-Update generated slides by script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
72
203db669ee3e auto-Update generated slides by script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
73
203db669ee3e auto-Update generated slides by script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
74 # 関数の定義を C の Syntax 書くと
203db669ee3e auto-Update generated slides by script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
75 * apply : A -> (A -> B) -> B
203db669ee3e auto-Update generated slides by script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
76
203db669ee3e auto-Update generated slides by script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
77 * B apply(A a, B ( * f )(A))
203db669ee3e auto-Update generated slides by script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
78 * これを満たす定義を関数applyの実装として書けば良い
203db669ee3e auto-Update generated slides by script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
79 * 証明 == 正しい返り値を返す なので
203db669ee3e auto-Update generated slides by script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
80 * つまりコンパイルを通してしまえば良い
203db669ee3e auto-Update generated slides by script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
81
203db669ee3e auto-Update generated slides by script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
82
203db669ee3e auto-Update generated slides by script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
83 # Agda で書いてみると
203db669ee3e auto-Update generated slides by script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
84
203db669ee3e auto-Update generated slides by script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
85 * emacs から使うと良いです
203db669ee3e auto-Update generated slides by script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
86 * module < filename > where
203db669ee3e auto-Update generated slides by script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
87 * を先頭に書く必要があります
203db669ee3e auto-Update generated slides by script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
88 * 証明を定義していく
203db669ee3e auto-Update generated slides by script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
89 * C-c C-l で型チェック(証明チェック)ができます
203db669ee3e auto-Update generated slides by script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
90
203db669ee3e auto-Update generated slides by script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
91
203db669ee3e auto-Update generated slides by script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
92 # Agda による apply
203db669ee3e auto-Update generated slides by script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
93 * apply : A -> (A -> B) -> B
203db669ee3e auto-Update generated slides by script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
94 * apply a f = f a
203db669ee3e auto-Update generated slides by script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
95
203db669ee3e auto-Update generated slides by script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
96 * とは
203db669ee3e auto-Update generated slides by script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
97 * A を Int, B を String とすると
203db669ee3e auto-Update generated slides by script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
98 * Int と、 Int から String を返す関数があれば String を作れる
203db669ee3e auto-Update generated slides by script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
99 * と読めます。つまり関数適用です
203db669ee3e auto-Update generated slides by script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
100
203db669ee3e auto-Update generated slides by script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
101
203db669ee3e auto-Update generated slides by script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
102 # 命題に 'ならば' を含む場合
203db669ee3e auto-Update generated slides by script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
103 * 関数を返せば良いです
203db669ee3e auto-Update generated slides by script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
104 * Agda には lambda があるので
203db669ee3e auto-Update generated slides by script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
105 * id : (A -> A)
203db669ee3e auto-Update generated slides by script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
106 * id = \a -> a
203db669ee3e auto-Update generated slides by script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
107 * といったように書けます。
203db669ee3e auto-Update generated slides by script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
108 * lambda の syntax は \arg -> body です
203db669ee3e auto-Update generated slides by script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
109
203db669ee3e auto-Update generated slides by script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
110
203db669ee3e auto-Update generated slides by script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
111 # 'ならば' を含む証明
203db669ee3e auto-Update generated slides by script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
112 * 三段論法 の証明
203db669ee3e auto-Update generated slides by script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
113
203db669ee3e auto-Update generated slides by script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
114 * compose : (A -> B) -> (B -> C) -> (A -> C)
203db669ee3e auto-Update generated slides by script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
115 * compose f g = \a -> g (f a)
203db669ee3e auto-Update generated slides by script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
116
203db669ee3e auto-Update generated slides by script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
117 * 三段論法は関数の合成に相当しています
203db669ee3e auto-Update generated slides by script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
118
203db669ee3e auto-Update generated slides by script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
119
203db669ee3e auto-Update generated slides by script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
120 # Agda による 証明 の方法のまとめ
203db669ee3e auto-Update generated slides by script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
121 * 型として (仮定) -> (仮定) -> ... -> (命題)
203db669ee3e auto-Update generated slides by script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
122 * として命題を定義
203db669ee3e auto-Update generated slides by script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
123 * それを満たす定義を関数として定義する
203db669ee3e auto-Update generated slides by script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
124
203db669ee3e auto-Update generated slides by script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
125
203db669ee3e auto-Update generated slides by script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
126 # 自然数の加算の交換法則の証明
203db669ee3e auto-Update generated slides by script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
127 * まずは自然数を定義する
203db669ee3e auto-Update generated slides by script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
128 * ペアノ算術を使います
203db669ee3e auto-Update generated slides by script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
129
203db669ee3e auto-Update generated slides by script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
130
203db669ee3e auto-Update generated slides by script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
131 # ペアノ算術による自然数の定義
203db669ee3e auto-Update generated slides by script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
132 * ゼロは自然数である
203db669ee3e auto-Update generated slides by script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
133 * 自然数の後続数は自然数である
203db669ee3e auto-Update generated slides by script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
134 * TODO: 詳細は今から
203db669ee3e auto-Update generated slides by script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
135
203db669ee3e auto-Update generated slides by script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
136
203db669ee3e auto-Update generated slides by script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
137 # ペアノ算術の Agda による定義
203db669ee3e auto-Update generated slides by script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
138 * data type を定義します
203db669ee3e auto-Update generated slides by script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
139 * data Int where
203db669ee3e auto-Update generated slides by script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
140 * O -> Int
203db669ee3e auto-Update generated slides by script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
141 * S -> Int -> Int
203db669ee3e auto-Update generated slides by script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
142 * Int は O か、 Int に S をかけたもの、とします
203db669ee3e auto-Update generated slides by script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
143
203db669ee3e auto-Update generated slides by script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
144
203db669ee3e auto-Update generated slides by script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
145 # パターンマッチ
203db669ee3e auto-Update generated slides by script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
146 * Agda においてはデータ型を引数で分解することができます
203db669ee3e auto-Update generated slides by script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
147 * ある型に続している値が、どのコンストラクタにおいて構成されたかをパターンで示せます
203db669ee3e auto-Update generated slides by script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
148 * これをパターンマッチと言います
203db669ee3e auto-Update generated slides by script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
149 * double : Int -> Int
203db669ee3e auto-Update generated slides by script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
150 * double O = O
203db669ee3e auto-Update generated slides by script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
151 * double (S n) = S (S (double n))
203db669ee3e auto-Update generated slides by script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
152 * 関数名 (引数のパターン) = 定義
203db669ee3e auto-Update generated slides by script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
153
203db669ee3e auto-Update generated slides by script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
154
203db669ee3e auto-Update generated slides by script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
155 # パターンマッチによる自然数の加算の定義
203db669ee3e auto-Update generated slides by script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
156 * TODO: 今から
203db669ee3e auto-Update generated slides by script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
157
203db669ee3e auto-Update generated slides by script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
158
203db669ee3e auto-Update generated slides by script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
159 # '等しさ' ということ
203db669ee3e auto-Update generated slides by script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
160 * 交換法則においては '等しい' ということを証明しなければなりません
203db669ee3e auto-Update generated slides by script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
161 * 等しい、ということも定義する必要があります
203db669ee3e auto-Update generated slides by script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
162 * 命題は型で定義するため、'等しい'、という型が必要です
203db669ee3e auto-Update generated slides by script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
163
203db669ee3e auto-Update generated slides by script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
164
203db669ee3e auto-Update generated slides by script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
165 # 等しさをデータ型で定義する
203db669ee3e auto-Update generated slides by script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
166 * == を定義していきます
203db669ee3e auto-Update generated slides by script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
167 * == は型でなくてはならないので
203db669ee3e auto-Update generated slides by script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
168 * data _==_ : {A : Set} -> A -> A -> Set where
203db669ee3e auto-Update generated slides by script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
169 * となります
203db669ee3e auto-Update generated slides by script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
170 * よって、 hoge と fuga の等しさを証明したい場合は
203db669ee3e auto-Update generated slides by script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
171 * 'hoge == fuga' 、という型を持つ項を関数の定義に書くことが証明になります
203db669ee3e auto-Update generated slides by script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
172
203db669ee3e auto-Update generated slides by script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
173
203db669ee3e auto-Update generated slides by script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
174 # '等しい'ということの定義3つ
203db669ee3e auto-Update generated slides by script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
175 * TODO: refl, sym, cong を書きます
203db669ee3e auto-Update generated slides by script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
176 * comment
203db669ee3e auto-Update generated slides by script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
177 * 個人的には Relation.Binary.PropositionalEquality を open import するよりは自前で定義したい
203db669ee3e auto-Update generated slides by script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
178 * あと R とか reasoning もできれば使いたくない
203db669ee3e auto-Update generated slides by script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
179 * というか必要でないなら積極的に削っていかないと時間がおそらく足りない
203db669ee3e auto-Update generated slides by script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
180 * 時間あまった時用に証明をもう1,2 個くらい書いておきたい
203db669ee3e auto-Update generated slides by script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
181
203db669ee3e auto-Update generated slides by script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
182
203db669ee3e auto-Update generated slides by script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
183 # 交換法則を命題として定義する
203db669ee3e auto-Update generated slides by script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
184 * == を用いて
203db669ee3e auto-Update generated slides by script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
185 * (n : Int) -> (m : Int) -> n + m == m + n
203db669ee3e auto-Update generated slides by script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
186 * 引数は (名前 : 型) として名前付けできます
203db669ee3e auto-Update generated slides by script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
187
203db669ee3e auto-Update generated slides by script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
188
203db669ee3e auto-Update generated slides by script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
189 # 交換法則を証明する
203db669ee3e auto-Update generated slides by script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
190 * 交換法則を関数の定義として書いていきます
203db669ee3e auto-Update generated slides by script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
191 * TODO: 今から
203db669ee3e auto-Update generated slides by script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
192
203db669ee3e auto-Update generated slides by script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
193
203db669ee3e auto-Update generated slides by script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
194 # Agda による証明方法のまとめ
203db669ee3e auto-Update generated slides by script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
195 * 関数の型を命題、関数の定義を証明とする
203db669ee3e auto-Update generated slides by script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
196 * 命題を扱う必要があるため、型もデータ型として定義できる
203db669ee3e auto-Update generated slides by script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
197 * データ型はパターンマッチにより分解することができる
203db669ee3e auto-Update generated slides by script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
198 * C-c C-l により型のチェックが成功すれば証明終了
203db669ee3e auto-Update generated slides by script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
199
203db669ee3e auto-Update generated slides by script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
200
203db669ee3e auto-Update generated slides by script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
201 <!-- vim: set filetype=markdown.slide: -->