FC2ブログ
--.--
--
上記の広告は1ヶ月以上更新のないブログに表示されています。
新しい記事を書く事で広告が消せます。

08.08
Fri
Coqの勉強をしていて、練習問題によく(?)取り上げられる、リストを2回反転させるともとのリストに戻るというのを証明してみます.どのように考えたかを残しておこうと思います。

まずリストとappendとreverseの定義をします。これが要するにプログラムとなるわけです.
リストは簡単のため要素に自然数しか取れないものを定義しました。



でこのプログラムがもつ性質をCoqで証明します
今回はどんなリストを渡しても2回reverseするともとに戻るというものです。

以下にコードを貼りますが、証明はトップダウンに書いてあるので(思考の過程としては補題を証明してから定理を証明したわけではない)一番下からから読むとどうしてその補題が必要になるのかわかってわかりやすいと思います.



まずをlistに関する帰納法で真っ向から証明してみようとすると、詰みます。なのでなにか補助定理が必要だろうと思います。

は定義よりとなります。(xsはlistのcdr部、xはcar部)
これにreverseをかけた物がになるのでという事になりす。

ここからがちょっと試行錯誤というかひらめきが必要だったのですが(自分は)、xsとxに適当に値を代入して考えてみます.
例えばl = (1,2,3,4)みたいなリストの時xs = (2,3,4),x = 1となりますが上に代入してみるととなります。
これを少しずつ簡単にしていくと
という風になるわけですが、
ここで別にappendしてからreverseしてしなくても先にreverseしてからappendしても同じようになるなーとか、
そのままreverseを先にやるとreverseを2回適用する形が出てきてしまって堂々巡りになりそうだなーと思いつきます。
ということでを補題として証明してやるとうまくいきました。





スポンサーサイト
comment 0 trackback 0
08.05
Tue
ここのページを参考にCoqでドモルガンの法則を証明していたときのメモです.
証明したいのはです。
おおまかな方針としては、まず含意の式なので前件を仮定して後件をひねり出せばいいだけです。

apply conjで連言を分けて別々に証明すればいいようにします.
or_introl,or_introlはそのまま選言の導入の推論規則みたいな感じです.

以下Coqのコード

Lemma de_morgan3 :
forall (A B : Prop) , ~(A \/ B) -> (~A /\ ~B).
Proof.
unfold not. (* ~はシンタックスシュガー *)
intros. (* 含意の前件を仮定する *)
apply conj. (* ∧の命題を証明したい.つまり 左と右を別個に証明すればいい *)
intros. (* 含意の前件を仮定する*)
apply H. (* Falseを得たい *)
apply or_introl. (* 論理和の導入は左か右が証明できればいい.左のAが仮定にある *)
exact H0.
(* 以下同様にして証明する *)
intros.
apply H.
apply or_intror.
exact H0.
Qed.

いくらか分かりやすさが増すので自然演繹の証明図もはっておきます。

Screenshot from 2014-08-05 01:55:00



comment 0 trackback 0
08.01
Fri
NJでの証明にはまっています。
所謂カリーハワード対応のおかげでNJ provableな論理式を型としてもつ型付きラムダ項を得たり
逆に型付きラムダ項からNJの証明図を得たりできます。なんか楽しいです。
ということで以下の型をもつラムダ項を証明図を書いてもとめてみようと思います




Screenshot_from_2014-08-01 00:16:40

コロンを挟んで右(の論理式)がラムダ項の型を表しています。
つまり、右だけ見てけば普通に上の論理式をNJで証明していく過程を表していることになります。
で左側がラムダ項を表しています。推論規則MPを適用するときには項をくっつけて、
仮定が落ちるときはラムダをくっつけてやればいい感じです。おおまかいうと。

で得られた関数をHaskellで実際に定義してみたら以下のようになりました。


GHCi, version 7.4.2: http://www.haskell.org/ghc/ :? for help
Loading package ghc-prim ... linking ... done.
Loading package integer-gmp ... linking ... done.
Loading package base ... linking ... done.
Prelude> data A
Prelude> data B
Prelude> data C
Prelude> let fun :: (A -> (B -> C)) -> ((A -> B) -> (A -> C)); fun x z y = ((x y) (z y))
Prelude> :type fun
fun :: (A -> B -> C) -> (A -> B) -> A -> C
Prelude>


おおーちゃんと定義できたみたい?ですね。




comment 0 trackback 0
07.31
Thu
直観論理と古典論理における証明体系であるNJとNKの推論規則を列挙してみる

Screenshot_from_2014-07-31 19:34:49
Screenshot_from_2014-07-31 19:35:06

これが直観論理における推論規則なんだけれど、ここに以下の2つの推論規則、
二重否定除去(DN)またはRAA(背理法)を加えるか公理として排中律を認めてやると古典論理の体系つまりNKにもどる。
なぜかというと、DN、RAA、排中律の何れかを使えば他2つはそれで表すことができ、またその何れかをもつことが、直観論理に比べた古典論理の特徴らしいので。
Screenshot_from_2014-07-31 19:43:54



comment 0 trackback 0
07.05
Sat
導出原理を使って自動定理証明系を書いているわけですが、
純粋な導出原理のみの実装だと扱いにくくなる論理式があります。式が等号を含んでいる場合です。

導出原理はパターンマッチによって相補的になるリテラルの除去を繰り返し行うだけで特別な論理式
(推論の効率的な意味で特別に扱うべき式、つまり等号を含んでいるものという意味)
について特別な処理を行うことはしません。あたりまえですね。
述語記号が等号であっても、等号に固有な性質を考慮した推論は行うことができない
つまり、単なる二項述語としての扱いしかしません。

これを解決する方法がいくつかあります。

まず、特別扱いする方法ではなくて単に等号公理を入れる方法を見てから
それをベースに導出原理の拡張を考えてみます。

以下を公理として入れてしまえば、等号に関する論理式が証明できます

(Pが全てのn引数の述語を暗黙に表しているという問題がある。つまり高階論理)
(上と同じ問題はある)
証明したい式が等号を含む場合は常にこれらの公理を考えることになり効率は当然よくありません。
定理証明において(というか何でも)効率が良くない、要するに探索空間を爆発させてしまうやり方は
有限時間内で証明できる式の範囲を狭めかねませんのでよろしくありません。

ところで等号公理の下2つが表す事は何かというと、"等しいもの"同士は置き換えが効くという置換の規則を
表しているように考えられます。なのでこれをもとに導出原理を拡張したのがParamodulation法です。
正確な定義は述べませんが、やっている事は簡単でからを導くというもので、
これで導出原理を拡張します。
ところがParamodulationはあまり効率の良くないアルゴリズムです。なぜかを説明すると上の簡単な例だと置き換えられる場所つまり中の項として現れるのは一箇所だけですが(というか1引数の述語なので)、
一般には複数ヶ所に現れますし、更に項が関数項ならその中にも出現する可能性があります。
この場合どこをに置き換えたらいいのでしょうか?
もし全てのパターン数だけ、新たな節が生成されたらかなり厄介です。

そして3つ目の方法。等号を書き換え規則として考えるのは前2つと同じものでKnuth-Bendixの完備化アルゴリズムというのがあり、これが等式の証明に使えます。がこれは次回にまとめたいと思います。

comment 0 trackback 0
back-to-top
上記広告は1ヶ月以上更新のないブログに表示されています。新しい記事を書くことで広告を消せます。