# HG changeset patch
# User Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
# Date 1392708027 -32400
# Node ID 2a22a785d778dd09df572248afcd2b6371f256d3
# Parent  3fb1e07004fac4daaf7d7279399479cfc6aa7609
Add slide for seminar

diff -r 3fb1e07004fa -r 2a22a785d778 slides/20140218/slide.md
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/slides/20140218/slide.md	Tue Feb 18 16:20:27 2014 +0900
@@ -0,0 +1,56 @@
+title: 証明によるプログラムの信頼性の向上(仮)
+author: Yasutaka Higa
+cover:
+lang: Japanese
+
+
+# 研究目的(仮)
+
+* 証明によるプログラムの信頼性の向上を目指す。
+* 信頼性とは、プログラムがプログラマの予期しない動作をしないことである。
+* 目標の例としては、現在は実行時にしか検出できないエラーなどを実行以前に検出することがある。
+
+# 近況報告
+
+* ちょっとゲーデルの完全性定理と不完全性定理について調べた
+* 型システム入門 (Types and Programming Languages) を読み始めました
+
+# ゲーデルの完全性定理
+
+* 述語論理の完全性定理
+* 述語論理の論理式が真であれば、公理系の証明が存在する
+    * これは完全性定理として証明されたらしい
+* 一回述語論理のみらしい
+* 一回述語論理とは命題論理に量化記号を導入したもの
+    * 命題           : 人間は寝る
+    * 量化された命題 : すべての人間は寝る
+
+# ゲーデルの不完全性定理
+
+* 自然数論の不完全性定理
+* すべての命題は証明可能/反証可能、というわけではないらしい
+* ゲーデル命題という「真であるにも関わらず、システムで証明可能で無い」命題が存在する
+
+# ゲーデル命題の例
+* 前提 : 真==証明可能、偽==反証可能 だとすると
+* 前提 : 証明可能な命題が真で、証明不可能な命題が偽であることが決定的
+* 例 : 「この命題はシステムによって証明可能では無い」
+    * 真なので反証はできない
+    * 真なので証明可能かもしれないが、「証明可能で無い」という述語がついている
+    * よってシステムで決定不可能 == システムで証明できない
+
+# 完全性定理と不完全性定理
+
+* 結局 : 具体的に何を意味するのかはあまり良く分かっていない
+* 論理は完全っぽくて自然数論は不完全っぽい、くらいの認識
+    * 論理は真であれば証明が存在する
+    * 自然数論では証明が存在しないものがある
+    * なら論理と自然数論の違い……？
+* とりあえず、自己言及はしない方が良い、とかくらいの認識
+
+# TaPL
+* 型システム入門 - プログラミング言語と型の理論 -
+* Types and Programming Languages
+* まだ読み始めたばかりです
+* 型を使わない演算についてまでしか読んでません
+    * bool と Church 数のみのラムダ演算