組み込み述語 =

組み込み述語 _=_ は、両辺の項が同じ標準形を持つときに true を返す。_=_ は命題の表現などに用いられる。

組み込み述語 _=_ は、内蔵モジュール EQL で次のように宣言されている。

sys:mod! EQL
{
  imports {
    protecting (TRUTH)
  }
  signature {
    pred _ = _ : _ Cosmos _ _ Cosmos _  { comm prec: 51 }
  }
  axioms {
    eq CUX = CUX = true .
  }
}

※ _=_ は、等式宣言の構文要素である _=_ と紛らわしいため、等式の中で使用する際には、eq p(N:Nat, M:Nat) = (N = M) . のようにカッコを付けて、明示的に記述する必要がある。

_=_ は、次のように使うことができる。例えば、項 s(s(0)) + 0 と s(0) + s(0) は同じ標準形 s(s(0)) を持つ:

CafeOBJ> select NAT+ + EQL
NAT+ + EQL> red s(s(0)) + 0 = s(0) + s(0) .
-- reduce in NAT+ + EQL : s(s(0)) + 0 = s(0) + s(0)
true : Bool
(0.004 sec for parse, 6 rewrites(0.002 sec), 9 matches)
NAT+ + EQL> 

NAT+ + EQL はモジュール式と呼ばれ、この式はモジュール NAT+ と EQLの和を意味している。1行目で NAT+ + EQL を select したことによって、両方のモジュールで宣言されている項が使える。2行目で、s(s(0)) + 0 と s(0) + s(0)が等しいことを _=_ を使って判定するように CafeOBJ にコマンドを与えている。3行目以降は CafeOBJ の出力であり、簡約結果としてtrue (2つの項は等しい) が返されている。

_=_ はあくまで文法上の等しさを判定しており、意味上の等しさは判定できない。言い換えると、ある 2つの項を簡約して true が返ったときは両者は本当に等しいが、それ以外の項が返ったからと言って、本当に等しくないと帰結することはできない。

例えば、任意に選んだ 2つの自然数を定数 n と m で表し、n + m と m + n の等しさを推論する:

CafeOBJ> open NAT+ + EQL .
-- opening module NAT+ + EQL.. done.
%NAT+ + EQL> ops n m : -> Nat .  -- arbitrarily choosen two naturals n and m
%NAT+ + EQL> red n + m = m + n . -- try to verify + is commutative
_*
-- reduce in %NAT+ + EQL : n + m = m + n
n + m = m + n : Bool
(0.003 sec for parse, 0 rewrites(0.010 sec), 9 matches)
%NAT+ + EQL> close
CafeOBJ> 

open は select に似ているが少し違う。このことは、後で触れる。上記の簡約結果は true ではないが、我々はこの命題 (つまり + の交換律) が正しいことを知っている。CafeOBJ が交換律を知らないだけである。

CafeOBJ が_+_に交換律が成立することを知っているときは、当然 true が返る:

CafeOBJ> open NAT+ + EQL .
-- opening module NAT+ + EQL.. done.
%NAT+ + EQL> ops n m : -> Nat .
%NAT+ + EQL> op _+_ : Nat Nat -> Nat { comm } .
%NAT+ + EQL> red n + m = m + n .
-- reduce in %NAT+ + EQL : n + m = m + n
true : Bool
(0.002 sec for parse, 1 rewrites(0.003 sec), 9 matches)
%NAT+ + EQL> close
CafeOBJ> 

この例では、4行目で _+_ に交換律が成り立つことを (構文定義の上で) 宣言したので、CafeOBJ は n + m と m + n が等しいと判定する。

似たような機能を持つ別の組み込み述語として _==_ がある。この述語は証明の健全性を損なうことがあるため、使用しない方がよい。

[Next] 結合律の証明

Original Copyright © Takahiro Seino, all rights reserved.