CafeOBJの紹介とCafeOBJの不明なところ - 檜山正幸のキマイラ飼育記 (はてなBlog)

まだ咳が止まらない。不調だ。それはともかく：

「ソートと指標と型、実例をまじえて」に、CafeOBJのサンプルコードを出したので、久しぶりにCafeOBJを触ってみました。あー、やっぱりこれ面白いな。でも、よく分からないところもありますね。

CafeOBJのユーザーってどのくらいいるのだろう？かなり少数なんじゃないかな。僕がここで「よく分からない」と書いてみても反応があることは期待できそうにないけど、まー、書いてみる。

CafeOBJは、自然でコンパクトな記述ができる

まず、CafeOBJのいいところを言っておくと、予約された特殊文字が少なく、前置／後置／中置の演算子も使え、演算子オーバーロードもOK、さまざまな略記が許されているし、と、そんなこんなで自然でコンパクトな記述ができるところですね。例えばアーベル群（可換群）の記述は：

mod ABGRP {
 -- Abelian group
 [A] -- 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はmodule（仕様記述モジュール）の略記です。二項中置演算子+、単項前置演算子-などもユーザー定義できます。定数0は無項（引数なし；nullary）演算子の扱いで、これもユーザー定義。ただし、文字'+', '-'は名前の一部に使えるので、X + Y, - X を X+Y, -X のようには書けません。

可換律（交換法則）X + Y = Y + Xのところに「危険」とコメントしてあるのは、等式とみるぶんには問題なくても、項書き換え規則とみなすと無限実行を招く可能性があるからです。可換性は、等式で宣言するより、演算子属性commを付けて「これは可換演算だよ」と処理系に知らせたほうがいいようです。

mod ABGRP {
 -- Abelian group
 [A]

 op _+_ : A A -> A {comm}
 op 0 : -> A
 op -_ : A -> A

 vars X Y Z : A
 eq X + (Y + Z) = (X + Y) + Z .
 eq 0 + X = X .
 eq X + - X = 0 .
}

実は、結合性や単位性も演算子属性で書けるので、等式はX + - X = 0だけに減らせます。僕は等式で書く方が好きですが。

3種類のインポートって何だそれ？

アーベル群の仕様をもとに環（ring）を記述すると：

mod RING {
 us(ABGRP *{sort A -> R}) -- renaming import

 op _*_ : R R -> R
 op 1 : -> R
 
 vars X Y Z : R
 eq X * (Y * Z) = (X * Y) * Z .
 eq 1 * X = X .
 eq X * 1 = X .
 -- 分配律
 eq X * (Y + Z) = (X * Y) + (X * Z) .
 eq (X + Y) * Z = (X * Z) + (Y * Z) .
}

usはusingの略記で、インポート宣言の一種です。us(ABGRP)は、「モジュールABGRPを利用する」という意味です。ただし、ABGRPのソートAをRという名前にリネームして取り込みます（それが、*{sort A -> R}）。演算（定数も含める）+, 0, - はABGRPで既に定義済みなので、新しく二項演算*と無項演算（定数）1を追加しています。

さてところで、CafeOBJのインポート宣言は3種類あります。protecting（略記pr）、extending（略記ex）、using （略記us）です。「CafeOBJ 入門」から説明を引用すると：

pr : モデルに新しい要素を付け加えたり、異なっていた 2つの要素を等しいものとしない。

ex : モデルに新しい要素を付け加えることは許すが、異なっていた 2つの要素を等しいものとしない。

us : 特に制限はない。

ウーム、よくわからん。モデルってなんのことでしょう。エルブラン・モデルのことだと思うんですが、、、そうだとすると、演算子を追加すると確実にエルブラン・モデル（エルブラン宇宙）は大きくなりますし、等式を追加するとエルブラン宇宙を等式（同値関係）で割った集合は小さくなります。

となると、prとexの使い方は：

演算子も法則も追加しないときはpr
演算子を追加して法則は追加しないときはex

となりそうです。

しかし、先に出したABGRPとRINGの例で考えると、そう単純ではありません。RINGにおいて演算子も法則も追加してますが、もともとのアーベル群のエルブラン宇宙における2つの要素（項）を同値にすることはありません。よって、exインポートでも良さそうです。つまり、exの使用法は次のようになりそうです。

演算子を追加して、もとのモジュール上で解釈可能な法則は追加しないときはex*1

exでも、新しく追加した演算子を含むような法則の追加は許されるだろう、ってこと。

以上は単に僕の憶測です。処理系で実験すると、処理系はpr, ex, usの違いを気にしてないようです。pr, ex, usは人間が区別するだけなんでしょうか。よくわからん。

*1:たしか、言語や構造の保守的拡大（conservative extension）と呼ぶのだと記憶してます。