日々の流転

λ. derivors

(後で書き直す)

Seven Trees 問題を定理自動証明器を使って解く - ヒビルテ(2008-10-29) でやったことを少し形式的に考えると、

• 指標 Σ1 = {+, T0, T1, …} と
• 公理 E1 = { +の可換/結合則, T1=T0+T2, T2=T1+T3, … }

からなるセオリー (Σ1, E1*) での定理 T1=T7 を、

• 指標 Σ2 = {+, ×, 1, T} と
• 公理 E2 = { +の可換/結合則, ×の可換/結合則, 分配則, 1×x=x, T=1+T×T }

からなるセオリー (Σ2, E2*) での定理 T=T⁷ へと写したことになる。

私は institution の thoery ってのはこういうのを扱うためにあるのかと思ったのだけど、theory morphism は指標射の一種なので演算子を演算子に写すのに対して、ここで使った写像は演算子である Tk を演算子ではなくただの項でしかない T^k に写しているので、theory morphism にはなっていないのだった。

derivors

institutionではこういうのにどう対処しているのかな思って、Joseph A Goguen, Rod M Burstall. Institutions: abstract model theory for specification and programming. J. ACM, Vol. 39, No. 1. (January 1992), pp. 95-146. を読むと、以下のようなことが書いてあった。

For equational logic, there is another category with theories as objects, but with derivors, which map operators in Σ to derived operators in Σ', that is, to Σ'-terms, as morphisms [45]; in fact, this kind of morphism agrees with the usual morphism notion for Lawvere theories [69].

---

• 45. GOGUEN, J., AND BURSTALL, R. Some fundamental algebraic tools for the semantics of computation. Part 1: Comma categories, colimits, signatures, and theories. Theoret. Comput. Sci. 31, 2 (1984), 175-209.
• 69. LAWVERE, F. W. Functorial semantics of algebraic theories, Proc. Nat. A cad. Sci., U.S.A. 50 (1963), 869-872.

普通の theory morphism の代わりにこのderivorというのを使えば扱えそうだ。 ただ特定のinstitutionに依存してしまっているのが嫌な感じではあるけど。

さらに、Burstall, R. M. and Goguen, J. A. (1980): The Semantics of Clear: A Specification Language. Internal Report CSR-65-80, Department of Computer Science, University of Edinburgh. には、もう少し詳しいことが書いてあった。

(Note that this category of theories has certain signature morphisms as its morphisms, another category with the same objects would have as its morphisms derivors which map operators in Σ to derived operators in Σ' i.e. terms in Σ' with a binding sequence for their variables; but we shall not need this more complicated category. For a discussion of derivors see Goguen and Burstall [1978].)

---

• Goguen, J.A. and Burstall, R.M. (1978) Some fundamental properties of algebraic theories: a tool for semantics of computation. DAI Research Report No. 53, Dept. of Artificial Intelligence, University of Edinburgh.

え? 「shall not need this more complicated category」ということはderivorは結局不要なの?　Goguen and Burstall [1978] は入手できなかったので、仕方ないので自分で考えてみた。

考えてみた

I=(Sig,Sen,Mod,|=) を単一ソートの代数セオリーのinstitutionとする。

まず、signature morphism の拡張として derivor を定義する。 derivor f : Σ1→Σ2 は、Σ1のn引数演算子σをΣ2のn引数の派生演算子(λx1,…,xn. …)へと写すものとする。 また、文e∈Sen(Σ1)についてe中の演算子σをf(σ)で置き換え正規化したものを f(e)とする。f(e)にはラムダ式は現れないのでf(e)∈Sen(Σ2)になっている。 また、E⊆Sen(Σ1)に対して f(E) = {f(e) | e∈E} と定義する。

Sigの射をderivorに拡張した institution I' を考えることが出来る。 そして、この I' で derivor f : Σ1→Σ2 がセオリー Th1=(Σ1,E1^・) からセオリー Th2=(Σ2,E2^・) への theory morphism になっている、すなわち f(E1)⊆E2^・ が成り立っているとする。 このとき φがTh1の定理(φ∈E1^・)ならばf(φ)はTh2の定理(f(φ)∈E2^・)になるのだけど、これをI'やderivorを直接使わずに言いたい。

そこで、以下からなるセオリーTh3=(Σ3, E3^・)を新たに考える。

• Σ3 = Σ1 + Σ2
• E3 = in2(E2) ∪ Ef
• where Ef = { in1(σ)(x1,…,xn)=in2(f(σ))(x1,…,xn) | σ∈Σ1 }

in2は明らかに Th2→Th3 の theory morphism になっていて in2(E2)⊆E3^・ が成り立つ。 また、fの条件から f(E1)⊆E2^・ なので、in2(f(E1))⊆in2(E2^・)⊆in2(E2)^・⊆E3^・ 。 ここで、Efより in1(φ)∈E3^・ ⇔ in2(f(φ))∈E3^・ なので in1(E1)⊆E3^・ となり、in1はTh1からTh2への theory morphism 。

次に、忘却関手 Mod(in2) : Mod(Th3)→Mod(Th2) には逆 F : Mod(Th2)→Mod(Th3) が存在するので、 in2(φ)∈E3^・ ⇔ ∀M3∈Mod(Th3). M3|=in2(φ) ⇔ ∀M2∈Mod(Th2). F(M2)|=in2(φ) ⇔ ∀M2∈Mod(Th2). Mod(in2)(F(M2))|=φ ⇔ ∀M2∈Mod(Th2). M2|=φ ⇔ φ∈E2^・ 。

これらを使うと、φ∈E1^・ から

• まず in1 : Th1→Th3 によって Th3 に移動して in1(φ)∈E3^・ を得て
• Th3 でそこから in2(f(φ))∈E3^・ を得て、
• 最後に in2 を逆に辿って f(φ)∈E2^・ を得る

という流れで考えることが出来る。

結局、トートロジーみたいなことしか言っていないのだけど、derivorを考える代わりに、Th2を拡張したセオリーTh3と theory morphism Th1→Th3 を考えれば、同様の推論は出来ると。

Seven Trees の場合

最初の問題を考えると、Th3=(Σ3, E3^・) は以下のようになる。

• Σ3 = {in1(+), in1(T0), in1(T1), …} ∪ {in2(+), in2(×), in2(1), in2(T)}
• E3 = { in2(+)の可換/結合則, in2(×)の可換/結合則, 分配則, in2(1)in2(×)x=x, in2(T)=in2(1)in2(+)in2(T)in2(×)in2(T) } ∪ {x in1(+) y = x in2(+) y, in1(T0)=in2(1), in1(T1)=in2(T), …}

そして、以下のように推論することが出来る。

• T1=T7 ∈ E1^・
• ⇒ in1(T1)=in1(T7) ∈ E3^・
• ⇔ in2(T)=in2(T⁷) ∈ E3^・
• ⇔ T=T⁷ ∈ E2^・