Binary Operation Specs
Binary Operation: Concepts, Issues, and Designs
Binary Operation Specs
The following specs are included in the file:
bin-op.re
- BIN-OP
- Sort E and op bin-op: E, E -> E
- ASSOCIATIVE
-
associativity: (equal (binop x (binop y z)) (binop (binop x y) z))
- COMMUTATIVE
-
commutativity: (equal (binop x y) (binop y x))
- IDEMPOTENT
-
idempotence: (equal (binop x x) x)
- BIN-OP-UNIT
-
left-unit-axiom: (equal (binop x unit) x)
right-unit-axiom: (equal (binop unit x) x)
- LEFT-INVERSE
-
left-inverse-axiom: (equal (binop (l-inv x) x) unit)
- RIGHT-INVERSE
-
right-inverse-axiom: (equal (binop x (r-inv x)) unit)
- INVERSE
-
left-inverse-axiom and right-inverse-axiom
- BINOP2
- Two (unshared) copies of BIN-OP
- PLUS-TIMES
-
BINOP2 with the operations renamed (translated to) plus and times
- LEFT-DISTRIBUTIVITY
-
left-distributivity:
(equal (times a (plus b c)) (plus (times a b) (times a c)) )
- RIGHT-DISTRIBUTIVITY
-
right-distributivity:
(equal (times (plus b c) a) (plus (times b a) (times c a)) )
- DISTRIBUTIVITY
- Left and right distributivity
(sharing plus and times)
SpecWeb Index
Specs