proverを書いてみたい

proverを作っているので、述語論理でproverを定義し、それの証明の様子をみてみたい。

とりあえずの目標としてUnificationをと考えたが、その前に必要なのはSubstitutionであり、そもそもExpressionの定義が必要。

表現(Expression; Expr)と呼んでいるのは当分はf(x,y)みたいなtermでよいと思うけれど、変数と定数の区別は気にしなくてよいだろう。(代入は論理の操作ではないので、述語記号やリテラルなどを区別したり、考える必要がないだろうと言う意味)

表現についての性質には何があるだろうか。
E1 ≡ E2
はどう定義するか?
あるいはE1≡E2について成り立つ性質は何か? その性質のうち、定義といえるものは何か?
関係に着目した書き方をしたいので、手続的な構造についてはなるべく触れないようにし、普遍条件的な書き方でなるべく話を進めたい。

そういえば、論理学では表現Eについて、E[v]みたいな書き方で、Eに出現するvのすべての出現を表すみたいなことが書いてあった気がするけど、これはちゃんと定義できるのだろうか。私には理解できない。vの出現する箇所の全体をこれで表したとして、それはどのような性質を持つのだろう。

表現を式として、雑に書くならば
　式 := 個体定数 | 関数定数(式,  …)
みたいな定義があるわけだが、その上で式[v]の意味をどうやって定義できるだろうか。

記号の同一性　s1≡s2はどうやって定義するのだろうか。与えられたものとするのか?　
証明論の研究者は、記号表現について、私の知らない何かの前提/知識を持っているのかもしれない。

記号が同じであることと、記号が指し示すものが同じであることの関係について考えるべきか。

[考えてみる]

まず、表現E1とE2が同じであるとはどういうことか。
E1に出現する記号とE2に出現する記号が、定義の構造に従って同じ順番(?)で同じ(?)であること。くらいしか思いつかない。

蛇足) 記号の同一性は定義されているとして、それをs1≡s2と書くとすると、このときのs1とs2は記号を指す変数ということになる。

「定義の構造に従って」の部分は、操作として定義するしかないのだろうか。別の方法を模索してみる。

まず、表現の抽象構文木みたいなのを考えると、その表現に出現するすべての記号は定義あるいは計算できそうなのでそれを
　S(E) = {Eに出現するすべての記号}
とする。この記号には、関数記号や個体定数を表す記号、変数記号がある。「括弧」などは含まない。

個々の記号の出現に1:1対応するパスというものを定義する。パスについては単純化するため、以下 S式を使って考える。

たとえば、"f(a,a)" をS式で (f a a)と書くことにする。
LISPを前提としたくはないので、listの要素はcar, cdrではなく出現順番の数字で表わす。この例では、f, a, aは1,2,3という数字で指し示す。この数字を使って記号の出現のパスを書く。

例
f(g(a,b),h(a))
を、S式で
(f (g a b) (h a))  … (あ)
と表わす。そのとき各記号の出現のパスは
　f    (1)
　g   (2 1)
　a    (2 2)
　b    (2 3)
　h    (3 1)
　a     (3 2)
となる。同じ記号(たとえば"a")も、パスが異なれば別の出現になる。

そこで、記号sのEにおけるすべての出現のパスの集合を
　{ p: E→s}
と書く。すると、表現Eのすべてのパスの集合は
　Π(E) = {p: E→s, ∀s∈S(E)}
　　　= ∪_{s∈S(E)} {p: E→s}
と定義できそうだ。

このとき、E1とE2が同じである(E1≡E2とかく)であるとは

E1 ≡ E2 ⇔ Π(E1) = Π(E2)
あるいは
　　　　⇔ (∀s∈S(E1)∧ ∀p ∈ P(E1→s) E2[p] ≡ s)∧
　　　　　 (∀s∈S(E2)∧∀p∈P(E2→s) E1[p] ≡s)
となるのではないだろうか。
記号の同一性 s1≡s2は定義されているとする。
表現の同一性は再帰的に定義されるのだが、ここでは記号の同一性に帰着している。表現の構造をパスでとらえているので、記号の同一性だけに着目するということなのだろう。

[S(E)の定義について]

S(E)は、Eの定義に基づいて計算できそうだ。
E1    := symbol | (f E2 E3 …)
と書いたとすると
S(E1) = {symbol}
S(E1) = {f} ∪ S(E2) ∪ S(E3) ∪…
という具合。

[p:E→sの定義]

Eからのパスは、表現の定義に基づいて定義することもできるだろうが、そういう手続的な定義はやめておきたいので、こういう方法も考えられそうだ。
まず、N*という列の集合を考える。(1), (2,1), (2,2,3)みたいな具合に無限集合である。
N* = N^1 ∪ N^2 ∪ N^3∪…
と書けるだろうか。
これは任意の表現Eについて、可能なパスの集合と解釈できる。(あ)の場合のパスは上に示した通りだ。
N*を特定の表現Eのパスとして解釈した場合、そのパスが何も指し示さない場合があるだろう。表現は有限の記号しか含まないので、そのようなパスは無限に存在する。
たとえば、(あ)では、(3 8 1)のようなパスに対応する記号は存在しない。(3 8 1)の指し示す記号はない。(とりあえず∅で表わすことにする)
すると、定義できるパスだけを集めた次の集合は、Eのすべてのパスの集合になる。

まず、表現E、パスp ∈ N*に対してE[p]をEからパスpで辿り着く表現と考える。このとき、E[p]の値は次のどれかになる。
　E[p] = symbol | Expr | ∅
∃E[p]と書いて、E[p]がsymbolかExprの場合に限定できるとすれば
　Π(E) = {p: ∃E[p]for ∀p ∈ N*}
と定義できるだろう。
(結局手続的な定義になるのか・・・)
こうするとΠの定義にS(E)はいらなくなる。

このような定義は計算には向かないが、計算とは独立した定義として有効にならないだろうか。
つまり、計算には向かないが関係をとらえた定義と、具体的な計算の正しさを考えるために必要な定義とは別にあってもよいはず。
どちらの定義も、いろいろ変えられるはずだけれど、それらが同値であるか、すくなくとも条件付きで同値であることが示ればよいと思う。
同じ目的/機能を実行するのに様々なアルゴリズムが存在するのは、このような関係があるからではないかと思う。

補足) ちなみに
定数を0引数の関数と考えて、aでなく(a)と書くようにすると、Eのパスの末尾が1のものが、定数だということになる。
指し示すもののあるパスの末尾が1でないときは、それの指し示すものは、Eの部分表現であるか、変数であるかだろう。
ちょっと楽しい。