title: 証明によるプログラムの信頼性の向上(仮)
author: Yasutaka Higa
cover:
lang: Japanese


# 研究目的(仮)

* 証明によるプログラムの信頼性の向上を目指す。
* 信頼性とは、プログラムがプログラマの予期しない動作をしないことである。
* 目標の例としては、現在は実行時にしか検出できないエラーなどを実行以前に検出することがある。

# 近況報告

* ちょっとゲーデルの完全性定理と不完全性定理について調べた
* 型システム入門 (Types and Programming Languages) を読み始めました

# ゲーデルの完全性定理

* 述語論理の完全性定理
* 述語論理の論理式が真であれば、公理系の証明が存在する
    * これは完全性定理として証明されたらしい
* 一回述語論理のみらしい
* 一回述語論理とは命題論理に量化記号を導入したもの
    * 命題           : 人間は寝る
    * 量化された命題 : すべての人間は寝る

# ゲーデルの不完全性定理

* 自然数論の不完全性定理
* すべての命題は証明可能/反証可能、というわけではないらしい
* ゲーデル命題という「真であるにも関わらず、システムで証明可能で無い」命題が存在する

# ゲーデル命題の例
* 前提 : 真==証明可能、偽==反証可能 だとすると
* 前提 : 証明可能な命題が真で、証明不可能な命題が偽であることが決定的
* 例 : 「この命題はシステムによって証明可能では無い」
    * 真なので反証はできない
    * 真なので証明可能かもしれないが、「証明可能で無い」という述語がついている
    * よってシステムで決定不可能 == システムで証明できない

# 完全性定理と不完全性定理

* 結局 : 具体的に何を意味するのかはあまり良く分かっていない
* 論理は完全っぽくて自然数論は不完全っぽい、くらいの認識
    * 論理は真であれば証明が存在する
    * 自然数論では証明が存在しないものがある
    * なら論理と自然数論の違い……？
* とりあえず、自己言及はしない方が良い、とかくらいの認識

# TaPL
* 型システム入門 - プログラミング言語と型の理論 -
* Types and Programming Languages
* まだ読み始めたばかりです
* 型を使わない演算についてまでしか読んでません
    * bool と Church 数のみのラムダ演算