はじめに
CafeOBJ の使い方: CafeOBJ の起動・終了; 仕様の記述; 仕様の読み込み
CafeOBJ の文法: コメント; モジュール; ソート; 輸入; オペレータ; 等式; 変数; 定義済みモジュールの表示; 項の構文解析; 簡約
証明譜を使った検証: 証明譜とは; 組み込み述語 =; 結合律の証明; 交換律の証明
補足: トラブル発生時の対応; 内蔵モジュール; 識別子で日本語を使う; 練習問題

オペレータ

オペレータは op を使って宣言する:

op <op-name> : <arity> -> <sort-of-op> { <operator-attribute> }

<op-name> にはオペレータ名、<arity> にはアリティ (arity) 、<sort-of-op> にはオペレータのソート (sort of operator) を指定する。アリティとは引数に対応する概念であり、ソート名の列である。オペレータのソート※とは返戻値の型に対応する概念である。アリティとオペレータのソートの組をランク (rank) と呼ぶ。オペレータの属性については、後述する。

※ コアリティ (co-arity) と呼ぶこともある。

同じランクを持つ複数のオペレータは ops を使って一度に宣言できる:

ops <op-name> ... <op-name> : <arity> -> <sort-of-op> { <operator-attribute> }

CafeOBJ では、オペレータの引数の位置を自由に指定することができる。例えば、中置演算子の + や、より複雑な演算子を宣言できる。オペレータの位置はオペレータ名の中の _ (下線) で表される。

オペレータの宣言例を以下に示す:

** 定数 (アリティが空列の演算)
ops true false : -> Bool

** 中置演算子の加算
op _+_ : Nat Nat -> Nat

** mix-fix の if 文
op if_then_else_if : Bool Exp Exp -> Exp

** (juxtaposition) の列
op __ : Elt Sequence -> Sequence

オペレータの属性

オペレータには、以下の属性を指定できる:

assoc : 結合律
comm : 交換律
r-assoc : 右結合
l-assoc : 左結合
idem : べき等律
id: <op-name> : <op-name> は単位元
idr: <op-name> : <op-name> は単位元 (id との違いは割愛)
prec: <precedence> : 演算子の結合の強さ (<precedence> の数値が小さいほど強い)
strat: (<e-strategy>) : E 戦略を用いた簡約順序の指定

それぞれの詳しい解説は CafeOBJ マニュアルを参照してほしい。

例えば、自然数の仕様に現れる、+ が結合律と交換律を持つことが証明できたならば、+ は属性指定を使って次のように宣言し直すことができる:

mod! NAT+AC {
  pr(NAT+)
  op _+_ : Nat Nat -> Nat { assoc comm }
}

これらの属性は演算の意味を簡潔に記述するのに大いに役立つが、よく理解しないで用いると思いもよらぬ結果を招くことがある。初心者は、使用法が確立され、その効用がよく理解されている{assoc comm}などの組み合わせに限定して使うことが望ましい。

[Next] 等式