Mercurial > hg > Members > atton > seminar_slides
view slides/20140218/slide.md @ 72:916d62123b1c
Update slide note
author | Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> |
---|---|
date | Tue, 07 Oct 2014 18:10:29 +0900 |
parents | 2a22a785d778 |
children |
line wrap: on
line source
title: 証明によるプログラムの信頼性の向上(仮) author: Yasutaka Higa cover: lang: Japanese # 研究目的(仮) * 証明によるプログラムの信頼性の向上を目指す。 * 信頼性とは、プログラムがプログラマの予期しない動作をしないことである。 * 目標の例としては、現在は実行時にしか検出できないエラーなどを実行以前に検出することがある。 # 近況報告 * ちょっとゲーデルの完全性定理と不完全性定理について調べた * 型システム入門 (Types and Programming Languages) を読み始めました # ゲーデルの完全性定理 * 述語論理の完全性定理 * 述語論理の論理式が真であれば、公理系の証明が存在する * これは完全性定理として証明されたらしい * 一回述語論理のみらしい * 一回述語論理とは命題論理に量化記号を導入したもの * 命題 : 人間は寝る * 量化された命題 : すべての人間は寝る # ゲーデルの不完全性定理 * 自然数論の不完全性定理 * すべての命題は証明可能/反証可能、というわけではないらしい * ゲーデル命題という「真であるにも関わらず、システムで証明可能で無い」命題が存在する # ゲーデル命題の例 * 前提 : 真==証明可能、偽==反証可能 だとすると * 前提 : 証明可能な命題が真で、証明不可能な命題が偽であることが決定的 * 例 : 「この命題はシステムによって証明可能では無い」 * 真なので反証はできない * 真なので証明可能かもしれないが、「証明可能で無い」という述語がついている * よってシステムで決定不可能 == システムで証明できない # 完全性定理と不完全性定理 * 結局 : 具体的に何を意味するのかはあまり良く分かっていない * 論理は完全っぽくて自然数論は不完全っぽい、くらいの認識 * 論理は真であれば証明が存在する * 自然数論では証明が存在しないものがある * なら論理と自然数論の違い……? * とりあえず、自己言及はしない方が良い、とかくらいの認識 # TaPL * 型システム入門 - プログラミング言語と型の理論 - * Types and Programming Languages * まだ読み始めたばかりです * 型を使わない演算についてまでしか読んでません * bool と Church 数のみのラムダ演算