expore のmguΣあたりの話をまとめつつある

	new file:   ../../docs/20240414-explore.txt
	modified:   dev.log
	new file:   docs/20240419-p2cprover.txt

docs/20240414-explore.txt

@@ -0,0 +1,97 @@
+20240414-explore.txt
+
+input clauses set Σと反証したいclause g ∈ Σが与えられた時
+Σ, ¬g⊢□か、Σ⊢gのG0レベルの証明はそのinputに対する計算と対応している。
+
+この資料では、G0レベルの証明というのは、個々のinput clauseを命題レベル(ground level)に変換してできる証明のことを指す。述語リテラルの引数部分を除去したものを考えればよいと思う。P(a)やP(b)のように変数を含まない部分を述語とみなし、変数のないリテラルを命題とみなすとか、そのような変形をしたあとで引数を除去するとか、いろいろ方法はあるように思う。単に引数を除去する方法は、述語記号という比較的意味の安定した概念を中心に話を展開できるので、よいのだろうと思う。
+
+Herbrand 宇宙の要素をinput、αとする場合、Σ, g(α)⊢□の証明を求めることになる。
+
+Σを仕様とするプログラムPは、このようなαのすべてについての処理を書いていると考えられる。
+
+そう考えると、PはこれらΣに従うすべての計算過程の記述であり、個々の証明をひとつに合成した証明に対応すると考えられる。
+
+一方で、プログラムP(α)の実行とは、個々の値αに対する証明を生成することである。
+その観点からは、プログラムは proverであるとも言える。
+
+プログラムの実行では、一部の分岐で使われる述語は除いて、プログラムの正当性の証明と違い、処理中のデータの関係を表す述語を使わない。
+これは、Σという特定のclause集合に特化した証明を作るための証明器であるからできることだろう。
+
+
+* プログラムの正しさをいうとき、このような述語/関係は明確に認識されていないことが多い。
+　機械語のプログラムやCOBOLなど関数機能が弱い言語では関数自体の入出力関係をとらえられないので、Hore型の処理の順序による関係に基づく証明になるが、その場合、プログラム構造が意図したものと同じであるかどうかの判定にしかならず、意図した機能を実現していることの証明は困難である。
+(as-isとはそういうことではないのだろうか)
+
+***
+プログラムPの実行 P(α)の実行過程を観察すると、Σ,¬g(α)⊢□の証明(反証)を構成するために必要な情報が得られる。
+逆に、Σ,¬g(α)⊢□の証明が構成できれば、そこからP(α)の計算過程を構成できる。
+
+P(α)の実行仮定では、Σに登場する述語や関係概念が明示されていないので、プログラムの実行と証明が等価であるとは言い難いだろう。
+
+***
+プログラムは、証明を作るという仕事から解放されているので、その内部構造においてはプログラムの正当性という制約なくプログラミングすることができる。
+
+***
+
+Σとgが与えられて、そこからΣ⊢gの証明ができたならば、その証明からプログラムを構成することはできるだろう。
+
+逆に、プログラムからΣ⊢gの証明を構成することは難しい。プログラムのどの部分がΣのどの述語/関係と対応しているのかが自明ではないからである。
+
+***
+変数を含む一般的な述語論理の証明を作ることは難しいが、変数がない場合は命題論理になるので、原理上は証明の構成ができる。
+
+これがプログラムのやっていることだと思う。
+
+***
+任意のαについてΣとg(α)から証明を作ることがPの実行に相当するが、αがデータの全域で定義されるとは限らない。
+
+証明を作れないαが存在するならば、そのPは部分関数になるだろう。
+
+***
+そこで、どのようなαを選んでも、Σとg(α)から証明を作ることができる
+
+
+***
+関係でなく手順の正しさだけを示すことは、プログラムの正当性というか、ΣをPに翻訳していることになるので、論理的な難しさは低いだろう。
+
+***
+
+
+
+
+***
+どうすればよいか?
+
+機能レベルでの正当性はどのように実現できるだろうか。
+
+**
+プログラムは、機能(あるいは利用)と実装の二つのレイヤーを結ぶ存在である。
+それぞれに正当性の概念があるはずで、あいまいに議論すると、無駄になってしまう。
+
+***
+機能の要求仕様をΦ、実装の定義仕様をΞとしよう。
+
+* 実装の定義仕様というのは
+
+* 機能の要求仕様というのは、Pを利用するときどのようになっていてほしいかを定義する。
+実装は、ホーア的なプログラムの正当性であり、必要な述語を導入すれば、機械的に証明できる。
+
+* 機能と実装の対応関係
+ 機能の要求仕様は、機能を定義するための定数や関数や関係をまず定義し、それらの語彙に基づいて記述される。
+
+　実装の定義仕様もまた語彙を持っている。
+
+　この機能と実装それぞれの定数、関数、関係がどのように関係づけられるか、変換されるかなどは証明されるものではなく、確認する仕掛けが必要になる。
+
+　・機能の語彙 X が実装の語彙の集合 XXによってどのように実現されるか、その実現が妥当であるかどうかを判定する方法が、また定義されていなくてはならない。
+
+　・実装の語彙はともかく、機能の語彙については、実行できないものも存在するので、機械的な判定が常にできるとは限らない。
+
+　・その確認のためには、機能の要求仕様側で、語彙の間に成り立つべき関係(公理)を定義する。
+　そして、機能の語彙を実装の語彙で実装の表現に翻訳した場合、この機能の公理が実装の上でどう変換され、それが正しいかどうかを判定する。という方法で確認できるだろう。む
+
+
+
+
+
+

lisp/rubbish/dev.log

@@ -1,3 +1,13 @@
+2024/04/19金
+
+しばらくdev.logを書くのわすれていた。
+
+extract-infは結果のmguしか求められない。
+
+
+
+
+
 2024/03/03日
 - extract-infoの使い方を忘れていたので関数のコメントに追加
 

lisp/rubbish/docs/20240419-p2cprover.txt

@@ -0,0 +1,52 @@
+20240419-p2cprover.txt
+
+
+ΣのG0レベルの証明をp2codeに写像すると、ループが1回だけに射影されたものになるので、証明全体が有限のp2codeに落ちる。
+　(これがうまくいくのは、rubbishが、すべてのliteralにlid、clauseにcidをつけて、区別しているからだろう)
+
+これを使って、G1レベルの証明をガイドできないか。あるいは、なんらかの証明を作りだすプログラムぽいものを作れないか。
+
+まず、input clauseのすべてのpairについてmguを求める。
+(readkqc ...)
+(defparameter mm (mguofΣ))
+
+mmは<L1:L2>の集合になる。
+ここで、(L1:L2)で、L1とL2をresolveしたresolutionを表すことにした。
+
+mmはmguの集合なのでinsideなpairは含まない。これを解除するとしたら
+　1) mguでなくdisagree を使う
+　　　(disagree '(x y) 'x '(f x) ()  #'collect)でdisagree setを求められるようだ(rubbish-unif.lisp)
+　　つまり、mguではinsideを含む情報がとりだせないが、disagreeなら取り出せる。それを圧縮しないので、安全に処理できる。
+
+　2) Σの書き方で、insideがないようにできる。
+　　　というのも、もしも潜在的なinsideがあった場合、それが顕在化するのは、□になるまでmguを圧縮したときの話で、input clauseでのpairのmguをもとめそのままにしているならば、変数の書き方をうまくすることで、insideが中和できる。(neutralized)。これはFlowのやっていたことかも。
+
+用語・記法
+　・<L1:L2>  L1と¬L2のmgu。これは¬L1とL2のmguに等しいので、¬をつけず<L1:L2>と書く。だから、符号は逆になっている。
+　・(L1:L2) (rubbishのlidやcidの方法を前提とすると) L1とL2はΣ全体でuniqueなので、L1とL2を指定すると1つのresolutionが決まる。そこで(L1: L2)でそのresolventを表す。この書き方だと、証明は lidをleafにもつバイナリツリーになる。renameも考慮すると、バイナリの部分の間にrenameの枝がのびている形になるだろう。
+　・G0レベル 命題算レベルということ。
+　・G1レベル 述語算レベルということ。
+　・(情報を)安全に取り出す　　unificationではinsideは禁止しているが、insideで起こる無限ループ(unification algorithmの問題)を回避して安全に処理すること。　
+　・圧縮　証明全体に散らばるmguは、証明の一番下のclause(□の場合に注目しているが)を考えると、証明全体のmguを合成してものになる。この合成をmguの圧縮と呼ぶ。
+　・中和　insideによって禁止されたmguがもつ情報を取り出すため、(圧縮せず)input clauseの形まま情報を取り出すとき、insideを中和していると考える。
+　・rubbish方式　clauseとそのliteralそれぞれにidをつける。cid, lid。すべてのclauseの変数は異なるように名前をつける。
+　　　これはresolutionでclauses間に共通の変数を持たないという前提を満たすため、resolutionのたびにrenameすることをやめ、clauseを作るときにすべての変数の名前を変えている、その処理とその効果をDVCと呼ぶ。(Disjoint Variables Condition)
+　　　これによって、ひとつの変数は、ひとつのclauseに属することになり、変数名からcidを求められるようになる。
+
+
+とりあえずmguで考えるとして(mguofΣ)はその環境にある全literalsの逆符号の述語記号についてpairを作り、そのmguを求める。
+このmgu集合は、(x y z) ← (t1 t2 t3)の形をしている。
+各mguには述語記号が対応しているが、その述語記号を省略しても、変数名からclauseがわかるので、mguだけで情報が欠落していないと考えられる。
+これをmmと呼ぶ。
+
+exploreでは、このmgu集合から次のような加工をしたm1を作っている。
+　1) (x y)←(a b)を変数ごとにわけて ((x←a)(y←b))とする
+　2) (x y)←(x b)の変化しない変数を除去して((y←b))とする
+
+こうして分解されたm1は、プログラムに近いが、どうもmmのように変数のtupleが、述語リテラルによる同時というか入出力の組み、つまり普遍性を反映しているのであり、プログラムとしてはこちらのほうが役に立つのではないかという気がしている。
+
+m1の場合、どの変数が同じclauseに属しているのかに着目して、変数の値のpushや遅延を行う必要があるのかなと思う。
+
+だんだん面倒になってきたので、これは一時保留。
+
+