Relation BINARY-OPERATOR-ON

• Defined in theory: Abstract-algebra
• Source code: abstract-algebra.lisp

Slots on this relation:

Documentation:

A function is a binary operator on a domain if it is closed on the domain, that is, it is defined for all pairs of objects that are instances of the domain and its value on all such pairs is an instance of the domain.

Instance-Of: Relation

Arity: 2

Domain: Binary-function

Equivalence Axioms:

(<=> (Binary-Operator-On ?Function ?Domain)
     (And (Binary-Function ?Function)
          (Forall (?X ?Y)
                  (=> (And (Instance-Of ?X ?Domain)
                           (Instance-Of ?Y ?Domain))
                      (Instance-Of (Value ?Function ?X ?Y) ?Domain)))))

Other Related Axioms:

(=> (Binary-Operator-On $X $Y) (Binary-Function $X))

(<=> (Binary-Operator-On ?Function ?Domain)
     (And (Binary-Function ?Function)
          (Forall (?X ?Y)
                  (=> (And (Instance-Of ?X ?Domain)
                           (Instance-Of ?Y ?Domain))
                      (Instance-Of (Value ?Function ?X ?Y) ?Domain)))))

(<=> (Distributes ?Op ?G ?Domain)
     (And (Binary-Operator-On ?Op ?Domain)
          (Binary-Operator-On ?G ?Domain)
          (Forall (?X ?Y ?Z)
                  (=> (Instance-Of ?X ?Domain)
                      (Instance-Of ?Y ?Domain)
                      (Instance-Of ?Z ?Domain)
                      (= (Value ?Op (Value ?G ?X ?Y) ?Z)
                         (Value ?G
                                (Value ?Op ?X ?Z)
                                (Value ?Op ?Y ?Z)))))))

(<=> (Identity-Element-For ?Id ?Op ?Domain)
     (And (Instance-Of ?Id ?Domain)
          (Binary-Operator-On ?Op ?Domain)
          (Forall (?X)
                  (=> (Instance-Of ?X ?Domain)
                      (= (Value ?Op ?Id ?X) ?X)))))

(<=> (Semigroup ?Domain ?Op ?Id)
     (And (Binary-Operator-On ?Op ?Domain)
          (Associative ?Op ?Domain)
          (Identity-Element-For ?Id ?Op ?Domain)))

(<=> (Group ?Domain ?Op ?Id)
     (And (Binary-Operator-On ?Op ?Domain)
          (Associative ?Op ?Domain)
          (Identity-Element-For ?Id ?Op ?Domain)
          (Invertible ?Op ?Id ?Domain)))

(<=> (Integral-Domain ?Domain ?Plus-Op ?Zero-Id ?Mult-Op ?One-Id)
     (And (Commutative-Ring ?Domain
                            ?Plus-Op
                            ?Zero-Id
                            ?Mult-Op
                            ?One-Id)
          (Binary-Operator-On ?Mult-Op
                              (Kappa (?X)
                                     (And (Instance-Of ?X ?Domain)
                                          (/= ?X ?Zero-Id))))))