まだCafeOBJ：2つの構造を一緒にしたい

興味を持つ人は非常に少数、かつ反応はありそうにないことを承知でCafeOBJの話を続けます。

アーベル群の仕様を次のように書きました。

mod ABGRP {
 -- Abelian group
 [A]

 op _+_ : A A -> A
 op 0 : -> A
 op -_ : A -> A

 vars X Y Z : A
 eq X + Y = Y + X . -- 危険だが等式を使う
 eq X + (Y + Z) = (X + Y) + Z .
 eq 0 + X = X .
 eq X + - X = 0 .
}

これを次のように書いてもいいでしょう。むしろこのほうが、「アーベル群＝群＋可換性」ということを端的に表しています。

mod GRP {
 -- group
 [G]

 op _*_ : G G -> G
 op 1 : -> G
 op ~_ : G -> G

 vars X Y Z : G
 eq X * (Y * Z) = (X * Y) * Z .
 eq 1 * X = X .
 eq X * 1 = X .
 eq X * ~ X = 1 .
 eq ~ X * X = 1 .
}

mod ABGRP2 {
 -- Abelian group
 us(GRP * {sort G -> A, op _*_ -> _+_, op 1 -> 0, op ~_ -> -_})

 vars X Y : A
 eq X + Y = Y + X .
}

指標を(G, *, 1, ~)から(A, +, 0, -)にリネームしたのは気分の問題です。さらに、もっと分解してもいいでしょう -- 「アーベル群＝モノイド＋逆元の存在＋可換性」

mod MON {
 -- monoid
 [M]

 op _*_ : M M -> M
 op 1 : -> M

 vars X Y Z : M
 eq X * (Y * Z) = (X * Y) * Z .
 eq 1 * X = X .
 eq X * 1 = X .
}

mod GRP2 {
 -- group
 us(MON * {sort M -> G})  

 op ~_ : G -> G

 vars X : G
 eq X * ~ X = 1 .
 eq ~ X * X = 1 .
}

mod ABGRP3 {
 -- Abelian group
 us(GRP2 * {sort G -> A, op _*_ -> _+_, op 1 -> 0, op ~_ -> -_})

 vars X Y : A
 eq X + Y = Y + X . -- 危険
}

これらをもとに環の定義をするとします。数学においては、(R, +, 0, -, *, 1)が環であることは次のように表現してかまいません。

1. (R, +, 0, -) がアーベル群
2. (R, *, 1) がモノイド
3. 分配律が成立する

そこで、とりあえず次のように書いてみます。

mod RING2 {
 us(ABGRP3 * {sort A -> R}) -- (R, +, 0, -) をアーベル群とする
 us(MON * {sort M -> R}) -- (R, *, 1) をモノイドとする
 -- 分配律はまだ未定義
}

第1行によりアーベル群(R, +, 0, -)が定義され、第2行によりモノイド(R, * 1)が定義されるはずです。これで同じR上に2つの構造が一緒に載ってくれると思いきや、そうはなってないようです。異なる2つのソート記号A, Mを同じRにしても、単一ソートR上に全部の演算が寄せ集まるわけではないようです。

マニュアルによると、連続したインポート、例えばus(FOO) us(BAR)は、us(FOO + BAR)と同じらしく、FOO + BARは直和を表すので、これはしょうがない気もします。でも、なんか釈然としない。