狠狠撸

2014-10-31 尾崎勝義
定理証明系の話

イントロ
?自己紹介/興味関心
?コンピュータネットワークを学ぶ大学3年
?ソフトウェアの形式的検証
?検索エンジンや推薦システム
?スライドの目的
?定理証明系の雰囲気を伝える
?古典的ATPの仕組みについて

定理証明系とは
?数学の定理を証明する
?四色定理の証明にCoqが使われた
?ケプラーの最密充填の証明にIsabelleが使われた
?プログラムの正当性の検証
?例: CompCert,JavaCard,…etc
?他の形式手法より強力な検証系
?コンピュータプログラムと証明の一致による

定理証明系(形式手法)の必要性
?仕様通りであることを証明できる
?ミドルウェアやミッションクリティカルなソフトウェアのバグは致命的。(言語処理系 , 暗号化ライブラリ , … etc )
?バグが存在しないことはテストでは検証できない
?四色定理の証明は支援系無しでは成し得なかった
?純粋に数学の定理証明における強力なツール

定理証明系の種類
?以下のように大別される(他にもある)
?基づく論理体系の違いにより証明アルゴリズムが違う
自動定理証明系(ATP)
定理証明支援系(ITP,PA)
?証明したい命題を入力し計算機に全自動で証明を見つけさせる。
?証明を人間が書き、そこに誤りが無いことをPAに証明させる。
Otter,Prover9,E,VampireACL2(Lisp製)…etc
Coq,Agda,Isabelle,…etc

Coqによる証明(1/3) – 例
?逆順にしたリストを返すreverse関数を定義する
??????.??????????????????=???? を証明したい

Coqによる証明(2/3) – 例

Coqによる証明(3/3)
?コマンド(タクティック)を対話的に入力し証明する
?証明のついたプログラムは別言語に出力可能
?Ocaml , Haskell , Scheme , Ruby,Scala
?プログラムに対して証明は一般に長くなる
?証明を書くには論理学の知識 + Coqの扱いに慣れる必要あり
→ 現実的なソフトウェアの検証にはコストが高い

プログラムと証明の一致?(1/4)
?形式的証明とは
?適当な論理体系(古典論理,直観論理,様相論理,…etc)を対象に作られた証明の枠組み(NK,NJ,LK,LJ…etc)
?型付ラムダ計算(プログラミング言語)とNJとの直接的対応
?プログラムがあれば証明が書ける。逆も然り。
?カリー=ハワード同型対応という
LJ
NJ
直観主義論理
対応
ML,Coq,Haskell
型付ラムダ計算
理論的基礎

プログラムと証明の一致(2/4)
?重要な推論規則
?を仮定し?が導かれるなら
?→?である(→導入則)
?→?でありかつ?であるなら?である (→除去則,前件肯定,MP,三段論法)
コロン左側では?をくっつける(?抽象)
コロン左側では関数呼び出し(関数適用)

?(int x) -> x +1というプログラムから対応した証明を書く
?ラムダ式
?(※ 簡単の為、+演算子はカリー化された関数とする)

?? →(?→?)→(?→?)→(?→?)の証明から対応したプログラムを得る

ATPによる証明 – 特徴
?主に古典論理(命題論理、1階述語論理)に基づく
?高階論理では確立された自動証明アルゴリズムが存在しない
?帰納法を厳密に表せない . ??∧????→??+?→???(?)
?全自動化されている
?人間が証明を書く必要はない
?導出原理を基礎とする証明
?述語論理に対しては「証明出来る場合」できると判定する計算手続き
?MP(モーダスポネンス)の一般化された推論規則
?ATPやPrologの基盤
?主に背理法による証明に使われる
?特定の論理式に対する効率的方法がある
?等式推論を行えない

導出原理について(1/10)
?概要
?相補的になるリテラルを消去する手続き
?論理式を節の集合に直す必要がある
?導出原理は節集合に対する証明アルゴリズム
?任意の論理式は節集合(連言標準形)で表すことができる
?論理式の変形手順
1.論理結合子を ? ,￢ , ∧ だけにする
2.否定を一番内側に移動する(リテラルにする)
3.冠頭形にする(量化部分と母式にわける)
4.スコーレム関数で量化子を消去
5.母式を連言標準形にする
6.選言部分(節)を取り出す

?冠頭形への変換手順
?任意の量化された述語論理式と同値な冠頭形の式を
以下の書き換えを繰り返す事によって求めることができる。
??を量化子,?を束縛変数とし、?が論理式?に自由出現しない場合は
以下の変換を行う。
??が論理式?に自由出現する場合は束縛変数?を付け変える
??.?? ∨ ? → ??.??∨ ?
??.?? ∧ ? → ??.(??∧?)

?量化子の除去
?スコーレム関数を導入することで存在量化子を消去することができる。
?この操作により式の同値性は失われるが充足不可能性は保障される
?手順
?スコーレム標準形でない冠頭形の式は以下のような形をしている
??????… ?????.?
??中の束縛変数?の出現を??(??,??,…,??)で置換し存在量化子を消去
??をスコーレム関数と呼ぶ
??=?(全称量化子が存在しない)の時??は0引数関数となるがこれを
スコーレム定数と呼ぶ

導出原理について(4/10) – 単一化
?単一化
?適当な項の代入を求め同じリテラルとなるか調べる手続き
?代入が無い場合同じリテラルにすることはできない(失敗)
?リテラル??と??が相補的となる代入があれば導出が可能になる
?命題論理式の場合は項を持たないため必要ない(命題は0項述語)
?単一化アルゴリズム
2つのリテラル、 ??= ??(??,??,…,??) ??=??(??,??,…,??)について?={??= ?? ,??=?? ,…,??=??}を考える。?に次の操作を繰り返し代入?を求める。

導出原理について(5/10) – 単一化
(A) ?中の全ての等式の左辺が変項であり、どの等式の左辺の変項も何れの
等式の右辺の項中にも現れないとき、?を?として終了。(終了条件)
(B) 適当な等式 ? ∈?を1つ取り出し(※)?の形で処理の場合を分ける
(以下、?を変項、?を適当な項とする)
1. ???,…,??=?(??,…,??) の形の時 : ?に??= ?? ,…,??= ??を加える
2. ???,…,??=?(??,…,??) の形の時 : 関数記号が違うため単一化失敗
3. ?=? の形の時: 何もしない
4. ?=? の形の時 :
?? ?中に?が出現する → 単一化は失敗(出現検査を行う場合)
????????? → ?の全ての等式に出現する?を?に置換し?を?に戻す。
5. ?=?の形の時 : ?=? を? に追加する
(A)にもどる
(※ ?=?の形の?を取り出す場合は?は?中の等式に出現していること)

導出原理について(6/10) - 例1
? {?,?→?} を前提として?が証明されることを判定
?1. ?の否定を前提の節集合に加える→ ?,???? ,??
?2. 得られた節集合に導出を行う
?命題論理式の場合、冠頭形の変形や単一化は必要ない
?空節(矛盾□)が出たので前提から?が証明される (背理法)
??∨?
?
?
??
□

導出原理について(7/10) - 手順
?節集合?=?? ,?? ,…,??の充足不可能性の判定
??∶ ?? ? ?? ′ , ??∶ ?? ? ?? ′ の時
?? ,?? について単一化子?が存在し相補的であれば、
???から???を除いたものと、???から???を除いたものを選言で
接続した新しい節 ??∶ (?′ ? ? ?′ ?)?を得る。
??を?に加え空節が導出されるまでこれを繰り返す。
?? ? ? ? ? ∪?? ? であるから?の証明可能性を判定できる。

導出原理について(8/10) – 例2
???.? ? →???? ??.??? ? ??.?(?) を判定
?結論の否定を前提の集合に加えて節集合を求める
??? ? ??? ,??? ,???
?導出を行い証明図(導出反駁木)を求める
?どの節を選び導出を行うかなどの戦略は様々ある
???? ?(?(?))
?(??)
?=? →?? ?(?(??))
??(?)
?={? →??} □

導出原理について(9/10) – 等号推論
?等号推論ができない
?導出は特定の二項述語(等号)について特別な処理を行うことはない。
?(例) {=?,?,≠(?,?)}の充足不可能性を判定できない。
単一化子が無いため導出できない
?解決策
?同値律を公理として入れる
?Paramodulation(等号調整法)などで導出原理を拡張する
?等式推論の為の別のアルゴリズムを使う

導出原理について(10/10) – 等号推論
?Paramodulationについて
節 ??∶ ??? ? ?? ′ , ??∶ ?=? ? ?′ ? の時
?と?について単一化子?が存在すれば新しい節
??∶ ?????/?? ? ?? ′? ? ?′ ?? を得る。
(ただしはリテラル中の項の注目やスラッシュで置換
を表している.)
?例
???,? , ??=??,???(??,?,?)

自作ATP(1/3)
?対話的な処理系(REPL)
?1階述語論理と命題論理に対応したATP
?等式推論にもいくらか対応
?証明図を出力可能
?任意の形式の式を一般的な式表現で入力可能
?ソースコードはここ https://github.com/moratori/flexpr

自作ATP(2/3)
定理「??=?を満たす群は可換である」の証明例

参考(1/2)
?型付ラムダ計算の体系の性質
http://logic.cs.tsukuba.ac.jp/~kam/lecture/complogic2012/8.pdf
?単純型付ラムダ計算とその論理
http://www.fos.kuis.kyoto-u.ac.jp/~igarashi/class/cal12w/stlc.pdf
?カリー=ハワード同型対応入門
http://ocw.kyoto-u.ac.jp/ja/frp7an/002- 006/pdf/curryhoward2.pdf/at_download/file
?計算体系と論理体系の関係
http://logic.cs.tsukuba.ac.jp/~kam/lecture/complogic2008/9.pdf
?JavaCardにおける形式的技法適用例
http://www.cs.gunma- u.ac.jp/~fujita/nagamiya080310_html/presentation060908.pdf
?定理証明支援系Coq入門
https://staff.aist.go.jp/reynald.affeldt/ssrcoq/coq-jssst2014.pdf

参考(2/2)
?Krakatoa and Jessieを用いた、Javaプログラムの正当性＆安全性証
http://qnighy.hatenablog.com/entry/2011/12/12/104640
?導出原理による定理証明
http://ci.nii.ac.jp/naid/110002761456
?単一化について
http://www.sic.shibaura-it.ac.jp/~sasano/lecture/proglang/2013/unify.pdf

狠狠撸

Prover

More Related Content

Prover