Mercurial > hg > Members > atton > seminar_slides

annotate slides/20140520/slide.md @ 119:9f874edd19a4

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