Binary Operation Specs

Binary Operation: Concepts, Issues, and Designs

Order Specs

BIN-REL

Sort E and op binrel: E, E -> Boolean

REFLEXIVE

reflexivity-axiom: (binrel x x)

TRANSITIVE

transitivity-axiom: (implies (and (binrel x y) (binrel y z)) (binrel x z))

SYMMETRIC

symmetry-axiom: (implies (binrel x y) (binrel y x))

ANTI-SYMMETRIC

anti-symmetry-axiom: (implies (and (binrel x y) (binrel y x)) (equal x y))

ASYMMETRIC

asymmetry-axiom: (implies (binrel x y) (not (binrel y x)) )

CONNECTED-REL

axiom connectivity-axiom is (or (or (binrel x y) (binrel y x)) (equal x y))
Some call this trichotomy. We use trichotomy for the stronger notion: exactly one case holds.

STRONGLY-CONNECTED-REL

axiom strong-connectivity-axiom is (or (binrel x y) (binrel y x))

CONVERSE-BIN-REL

axiom (iff (conv-br y x) (binrel x y) )

PRE-ORDER

REFLEXIVE and TRANSITIVE

PARTIAL-ORDER

REFLEXIVE, ANTI-SYMMETRIC, and TRANSITIVE (via PRE-ORDER)

EQUIVALENCE

REFLEXIVE, SYMMETRIC, and TRANSITIVE (via PRE-ORDER)

CONGRUENCE1

EQUIVALENCE + congruence for op func : E -> E

TOTAL-ORDER

STRONGLY-CONNECTED PARTIAL-ORDERs (I.e., leq) Also, contains the connected ordering lt.

ORDER-HIERARCHY

Diagram with (some of the) morphisms between orderings.

STRICT-PARTIAL-ORDER

ANTI-SYMMETRIC, and TRANSITIVE

STRICT-TOTAL-ORDER

Connected STRICT-PARTIAL-ORDER

INDUCED-STRICT-ORDER

lt defined from leq in PARTIAL-ORDER

INDUCED-NONSTRICT-ORDER

leq defined from lt in STRICT-PARTIAL-ORDER

DENSE-ORDER

STRICT-TOTAL-ORDER + density: (implies (lt x y) (Ex (z)(and (lt x z) (lt z y))))

COMPLETE-ORDER

STRICT-TOTAL-ORDER + completeness: every nonempty set bounded below has a greatest lower bound
The complete order spec is in the file: complete-orders.re

SpecWeb Index

Specs