0 Replies - 637 Views - Last Post: 30 November 2015 - 09:23 AM

#1 tease_bees  Icon User is offline

  • New D.I.C Head

Reputation: 0
  • View blog
  • Posts: 1
  • Joined: 30-November 15

about associativity in CafeOBJ

Posted 30 November 2015 - 09:23 AM

The following code is on CafeOBJ
mod* MONOID {
[ Elt ]
op e : -> Elt
op _*_ : Elt Elt -> Elt  { assoc id: e}
}

open  MONOID .
ops a b c : -> Elt .



At this stage assoicativity is held and everything is clear:

%MONOID> red (c * a) * b = c * (a * B ) .
_-- reduce in %MONOID : (((c * a) * B ) = (c * (a * B ))):Bool
(true):Bool
(0.0000 sec for parse, 0.0000 sec for 1 rewrites + 9 matches)

eq [e1] : c * a = e .
eq [e2] : a * b = e .



When this equations are added I get the following:

%MONOID> red (c * a) * b = c * (a * B ) .
-- reduce in %MONOID : (((c * a) * B ) = (c * (a * B ))):Bool
(b = c):Bool
(0.0000 sec for parse, 0.0000 sec for 4 rewrites + 27 matches)

Looks like associativity is not held, no matter it is operator property... why this happens?

b == c is what I need to proove (which mathematically follows from given equations eq1,eq2 + associativity), but a far as I undersand the interperter tells me the opposite!..

damn! B)/>/> is
B)/>/>/>

This post has been edited by modi123_1: 30 November 2015 - 09:25 AM
Reason for edit:: fixed the B ) for you.


Is This A Good Question/Topic? 0
  • +

Page 1 of 1