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

簡約

CafeOBJ において簡約 (reduction) とは、宣言された等式を左辺から右辺への書き換え規則とみなし、与えられた項を書き換え規則を使って次々に書き換え (規則をどんな順序で適用するのかは任意) 、できるだけ簡単な表現にすることである。どの書き換え規則を使っても、これ以上書き換えできない項を標準形 (normal form) と呼ぶ。簡約とは、等式を一方向にだけ使う、等式推論 (equational reasoning) である。

コマンド red は項 <term> を簡約する:

red <term> .

簡約の例:

自然数の仕様で宣言したモジュール NAT+ を使って、項 s(s(0)) + s(s(s(0))) を簡約する。

最初に、モジュール NAT+ を選択する。

CafeOBJ> select NAT+
NAT+>

red コマンドを使って項 s(s(0)) + s(s(s(0))) を簡約する。

NAT+> red s(s(0)) + s(s(s(0))) .
-- reduce in NAT+ : s(s(0)) + s(s(s(0)))
s(s(s(s(s(0))))) : Nat
(0.000 sec for parse, 3 rewrites(0.010 sec), 5 matches)
NAT+>

red コマンドは s(s(0)) + s(s(s(0))) の簡単な表現である s(s(s(s(s(0))))) (つまり、2 + 3 = 5) を返す。

簡約過程の表示

簡約過程を表示するには trace スイッチを on にする。こうすると、red コマンドは、簡約過程を表示する:

NAT+> set trace on
NAT+> red s(s(0)) + s(s(s(0))) .
-- reduce in NAT+ : s(s(0)) + s(s(s(0)))
1>[1] rule: eq s(N:Nat) + M:Nat = s(N + M)
    { N:Nat |-> s(0), M:Nat |-> s(s(s(0))) }
1<[1] s(s(0)) + s(s(s(0))) --> s(s(0) + s(s(s(0))))
1>[2] rule: eq s(N:Nat) + M:Nat = s(N + M)
    { N:Nat |-> 0, M:Nat |-> s(s(s(0))) }
1<[2] s(0) + s(s(s(0))) --> s(0 + s(s(s(0))))
1>[3] rule: eq 0 + M:Nat = M
    { M:Nat |-> s(s(s(0))) }
1<[3] 0 + s(s(s(0))) --> s(s(s(0)))
s(s(s(s(s(0))))) : Nat
(0.000 sec for parse, 3 rewrites(0.020 sec), 5 matches)
NAT+>

より簡潔な別の表示スタイルも用意されている。これを使用するには trace whole スイッチを on にする:

NAT+> set trace whole on
NAT+> red s(s(0)) + s(s(s(0))) .
-- reduce in NAT+ : s(s(0)) + s(s(s(0)))
[1]: s(s(0)) + s(s(s(0)))
---> s(s(0) + s(s(s(0))))
[2]: s(s(0) + s(s(s(0))))
---> s(s(0 + s(s(s(0)))))
[3]: s(s(0 + s(s(s(0)))))
---> s(s(s(s(s(0)))))
s(s(s(s(s(0))))) : Nat
(0.000 sec for parse, 3 rewrites(0.020 sec), 5 matches)
NAT+>

こちらのスタイルでは、項全体が変化する過程のみが表示される。

[Next] 証明譜とは