読んだのメモ - Yet Another Ranha

暇なのと、FLTVのネタ蒐集を兼ねてJSSST読んでました。

http://www.jstage.jst.go.jp/browse/jssst/25/3/_contents/-char/ja/

ここの
「モデル生成型定理証明と要素技術」と「論理・制約プログラミングと並行計算」。

あと気になったのは(つまり読んでない)のは、

http://www.jstage.jst.go.jp/browse/jssst/25/2/_contents/-char/ja/
「型代入を遅延する最適化型推論アルゴリズム」

と

http://www.jstage.jst.go.jp/browse/jssst/24/2/_contents/-char/ja/
「表示的意味論に基づくパターンマッチングコンパイル方式の構築と実装」

ですね。

「モデル生成型定理証明と要素技術」

SATCHMOは恐らく「モデル生成法と呼ばれる方式に基づく「一階述語論理の」定理証明システム」。

それと、文中MGTPはModel Generation Theorem Proverの略(恐らく)
MGTPについてはコレ(http://ci.nii.ac.jp/naid/110002722918/)とかが日本語で読める気がします。私は読んでません。

準群の未解決問題へのアプローチ(これかな? http://ci.nii.ac.jp/naid/110002722763/ )なんかも、MGTPで行われたらしい。

2章で、最も基本となるモデル生成手続きが書かれていて、これはsemantic tree(凄く簡単に言うと、ORで分岐、ANDは下に連ねて行く形で作られたtree)を構築していく感じで見れば、なんとなく分かった。

それと、モデルっていうのは、素直に数理論理学でいうモデルだと思います。

んで、Prologでは同じ証明(本当は完全な一階述語論理の証明では無いんですけれども)をするのにresolution(導出法とか、融合とか、分解とかこの3つの訳語におおよそ訳されるんですが)法に従ってます。

ところが、Prologではunification時におけるOccurs Checkというものが省かれていて(なんで省かれてるとか詳しい解説は偉い人に聞くのが一番だと思いますが、簡単に思い当たるのは実行時コストを抑える事でしょう)、健全性が損なわれています。

例えば

is_nat(zero).
is_nat(succ(zero)).
is_nat(succ(succ(X))) :- is_nat(succ(X)).

という明らかに適当にでっち上げたものがあって、すいません、という感じなんですけれども

?- is_nat(succ(succ(zero))) = is_nat(X).
X = succ(succ(zero)).

%% これは良いんですが

?- is_nat(succ(X)) = is_nat(X).
X = succ(**).

%% これは普通ダメです。まぁ気持ちは分からんでも無いんですが
%% それと、これはunification失敗じゃなくて「成功」してます。

みたいな事になったり。

PTTPとSATCHMOは巧い事やって回避してるみたいです。(SATCHMOの値域限定条件をどう利用していくのかが)

4章で改善すべき2点として、

証明に無関連なモデル拡張
重複証明

が出て来た。

証明に無関連なモデル拡張でどうなるのか、というのは図3の通りなんですが、これは結局「出来るだけ木を小さくしたい」という向きの話で、これが証明濃縮。
重複証明は、同じ証明をしてしまう事があって、つまり無駄なので消し去りたい。この手のはmemoizationするんですけども、片っ端から覚えるっていうのは現実的な証明木に対して非現実的なので、どうするか、という話が畳み込み法。

拡張の話はすっ飛ばして、SAT-Solverと絡めるっていう話が載ってるんですが、そもそもSAT-Solverは良く知らないのでうーーーーーーーーーんん！！！！！！！！！！！！！！！

「論理・制約プログラミングと並行計算」

5章の計算モデルにおけるグランドチャレンジが面白かったです。

他の所は並行論理型そんな知らないのでなーという感じで。

「並行分野におけるλ計算」の確立という話があって、今現在(2009年時点では知りませんけど)λ計算ほど安定したモデルは得られていないらしいですね。
π計算とかは、まさにそれだと思ってたんですが、そうじゃない「らしい」、私はπ計算全然知らないので、のでそれは楽しいなーとか。

bigraphical reactive systemとかAmbient計算も初めて知りました。LMNtalは意味分からんげな言語という印象しかないです。

あとは型体系の整備とかっていう話が載っていて、この辺はすごく面白そうだよなー、とか面白そうだよなーとか思っただけで何もやってないのでありました。

でもMilnerのπ計算の本を何故か持ってるで読んでみよう。