Binary Operations



next up previous
Next: Binary Relations Up: Abstract Algebra Previous: Abstract Algebra

Binary Operations

(defrelation binop (?f ?s) := (and (binary-function ?f) (subset (universe ?f) ?s)))

(defrelation associative (?f ?s) := (forall (?x ?y ?z) (=> (member ?x ?s) (member ?y ?s) (member ?z ?s) (= (value ?f ?x (value ?f ?y ?z)) (value ?f (value ?f ?x ?y) ?z)))))

(defrelation commutative (?f ?s) := (forall (?x ?y) (=> (member ?x ?s) (member ?y ?s) (= (value ?f ?x ?y) (value ?f ?y ?x)))))

(defrelation invertible (?f ?o ?s) := (forall (?x) (=> (memberp ?x ?s) (exists (?y) (and (member ?y ?s) (= (value ?x ?y) ?o) (= (value ?y ?x) ?o))))))

(defrelation distributes (?f ?g ?s) := (and (binop ?f ?s) (binop ?g ?s) (forall (?x ?y ?z) (=> (member ?x ?s) (member ?y ?s) (member ?z ?s) (= (value ?f (value ?g ?x ?y) ?z) (value ?g (value ?f ?x ?z) (value ?f ?y ?z)))))))



Vishal I. Sikka
Wed Dec 7 13:23:42 PST 1994