=
The built-in equality predicate _=_
takes terms of the same sort and returns true
when they are reduced into a same term.
The equality predicate _=_
is defined in the built-in module EQL
as follows:
sys:mod! EQL { imports { protecting (TRUTH) } signature { pred _ = _ : _ Cosmos _ _ Cosmos _ { comm prec: 51 } } axioms { eq CUX = CUX = true . } }
(*) The equality predicate _=_
and the keyword _=_
in the equation declaration are confusing. When using the equality predicate in an equation, it is recommended to put a term in brackets like eq p(N:Nat, M:Nat) = (N = M) .
The following is an example of equational reasoning with the equality predicate _=_
:
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>
The expression NAT+ + EQL
is a module expression which stands for the sum of NAT+
and EQL
. In the first line, NAT+ + EQL
is selected, and elements of both modules can be used hereafter. In the next line, try to reduce the equation of s(s(0)) + 0
and s(0) + s(0)
. Here, the symbol _=_
is the equality predicate. In the fourth line, CafeOBJ system returns true
, which means that the input terms are equivalent.
The equality predicate _=_
(or reduction) does not give a complete equational reasoning. Only the output true
is trustworthy. From syntactical and/or semantical reasons, it may fail to prove an equation even if it is true.
The following is an example of equational reasoning with _=_
which fails to prove the equation n + m = m + n
for arbitrary elements n, m
, that is, the commutativity of +
:
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>
The output term is not true
, though the commutativity of +
holds for NAT+
.
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>
Original Copyright © Takahiro Seino, all rights reserved.