Mercurial > hg > Members > atton > seminar_slides

annotate slides/20140218/slide.md @ 26:2a22a785d778

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, 18 Feb 2014 16:20:27 +0900
parents
children
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
rev   line source
26
2a22a785d778 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
1 title: 証明によるプログラムの信頼性の向上(仮)
2a22a785d778 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
2 author: Yasutaka Higa
2a22a785d778 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
3 cover:
2a22a785d778 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
4 lang: Japanese
2a22a785d778 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
5
2a22a785d778 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
6
2a22a785d778 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
7 # 研究目的(仮)
2a22a785d778 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
8
2a22a785d778 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
9 * 証明によるプログラムの信頼性の向上を目指す。
2a22a785d778 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
10 * 信頼性とは、プログラムがプログラマの予期しない動作をしないことである。
2a22a785d778 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
11 * 目標の例としては、現在は実行時にしか検出できないエラーなどを実行以前に検出することがある。
2a22a785d778 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
12
2a22a785d778 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
13 # 近況報告
2a22a785d778 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
14
2a22a785d778 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
15 * ちょっとゲーデルの完全性定理と不完全性定理について調べた
2a22a785d778 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
16 * 型システム入門 (Types and Programming Languages) を読み始めました
2a22a785d778 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
17
2a22a785d778 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
18 # ゲーデルの完全性定理
2a22a785d778 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
19
2a22a785d778 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
20 * 述語論理の完全性定理
2a22a785d778 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
21 * 述語論理の論理式が真であれば、公理系の証明が存在する
2a22a785d778 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
22 * これは完全性定理として証明されたらしい
2a22a785d778 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
23 * 一回述語論理のみらしい
2a22a785d778 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
24 * 一回述語論理とは命題論理に量化記号を導入したもの
2a22a785d778 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
25 * 命題 : 人間は寝る
2a22a785d778 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
26 * 量化された命題 : すべての人間は寝る
2a22a785d778 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
27
2a22a785d778 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
28 # ゲーデルの不完全性定理
2a22a785d778 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
29
2a22a785d778 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
30 * 自然数論の不完全性定理
2a22a785d778 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
31 * すべての命題は証明可能/反証可能、というわけではないらしい
2a22a785d778 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
32 * ゲーデル命題という「真であるにも関わらず、システムで証明可能で無い」命題が存在する
2a22a785d778 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
33
2a22a785d778 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
34 # ゲーデル命題の例
2a22a785d778 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
35 * 前提 : 真==証明可能、偽==反証可能 だとすると
2a22a785d778 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
36 * 前提 : 証明可能な命題が真で、証明不可能な命題が偽であることが決定的
2a22a785d778 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
37 * 例 : 「この命題はシステムによって証明可能では無い」
2a22a785d778 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
38 * 真なので反証はできない
2a22a785d778 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
39 * 真なので証明可能かもしれないが、「証明可能で無い」という述語がついている
2a22a785d778 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
40 * よってシステムで決定不可能 == システムで証明できない
2a22a785d778 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
41
2a22a785d778 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
42 # 完全性定理と不完全性定理
2a22a785d778 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
43
2a22a785d778 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
44 * 結局 : 具体的に何を意味するのかはあまり良く分かっていない
2a22a785d778 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
45 * 論理は完全っぽくて自然数論は不完全っぽい、くらいの認識
2a22a785d778 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
46 * 論理は真であれば証明が存在する
2a22a785d778 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
47 * 自然数論では証明が存在しないものがある
2a22a785d778 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
48 * なら論理と自然数論の違い……？
2a22a785d778 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
49 * とりあえず、自己言及はしない方が良い、とかくらいの認識
2a22a785d778 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
50
2a22a785d778 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
51 # TaPL
2a22a785d778 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
52 * 型システム入門 - プログラミング言語と型の理論 -
2a22a785d778 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
53 * Types and Programming Languages
2a22a785d778 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
54 * まだ読み始めたばかりです
2a22a785d778 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
55 * 型を使わない演算についてまでしか読んでません
2a22a785d778 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
56 * bool と Church 数のみのラムダ演算