# The Algebra Library (alglib)

Collection of algebraic operations.

## abelian_group

```
abelian_group(D, ⊙, N)
```

An abelian group is a commutative monoid where the operator `⊙`

has inverses defined by `N`

.

#### Definition

`@inline`

def abelian_group(D, ⊙, N) =

approximate_abelian_group(D, ⊙, N, =) and

group(D, ⊙, N) and

commutative_monoid(D, ⊙)

## absorption_laws

```
absorption_laws(D, ⊓, ⊔)
```

Binary operator `⊓`

and `⊔`

obey absorption laws if `a ⊔ (a ⊓ b) = a = a ⊓ (a ⊔ b)`

for all
`a`

and `b`

in `D`

. The absorption laws are one of the defining characteristics of the meet
and join operations of a lattice.

#### Definition

`@inline`

def absorption_laws(D, ⊓, ⊔) =

binary_operator(D, ⊓) and

binary_operator(D, ⊔) and

forall(a ∈ D, b ∈ D: (a ⊔ (a ⊓ b)) = a = (a ⊓ (a ⊔ b)))

## antisymmetric

```
antisymmetric(D, ∼)
```

A binary relation is antisymmetric if for all `a`

and `b`

in `D`

, whenever `a ∼ b`

and
`b ∼ a`

are true, then `b = a`

.

#### Definition

`@inline`

def antisymmetric(D, ∼) =

binary_relation(∼ ) and

binary_relation_substitution_laws(D, ∼, =) and

forall(a ∈ D, b ∈ D: ((a ∼ b) and (b ∼ a)) ⇒ a = b)

## approximate_abelian_group

```
approximate_abelian_group(D, ⊙, N, ≈)
```

An approximate abelian group is an approximate commutative monoid where the operator `⊙`

has approximate inverses defined by `N`

.

#### Definition

`@inline`

def approximate_abelian_group(D, ⊙, N, ≈) =

approximate_group(D, ⊙, N, ≈) and

approximate_commutative_monoid(D, ⊙, ≈)

## approximate_commutative_monoid

```
approximate_commutative_monoid(D, ⊙, ≈)
```

An approximate commutative monoid is an approximate monoid where the operator `⊙`

is
approximately commutative.

#### Definition

`@inline`

def approximate_commutative_monoid(D, ⊙, ≈) =

approximate_monoid(D, ⊙, ≈) and

approximately_commutative(D, ⊙, ≈)

## approximate_group

```
approximate_group(D, ⊙, N, ≈)
```

An approximate group is an approximate monoid where the operator `⊙`

has approximate
inverses defined by `N`

.

#### Definition

`@inline`

def approximate_group(D, ⊙, N, ≈) =

approximate_monoid(D, ⊙, ≈) and

approximately_has_inverse(D, ⊙, N, ≈)

## approximate_monoid

```
approximate_monoid(D, ⊙, ≈)
```

An approximate monoid is a set `D`

with a binary operator `⊙`

that is approximately
associative and has an identity element.

#### Definition

`@inline`

def approximate_monoid(D, ⊙, ≈) =

approximately_associative(D, ⊙, ≈) and

has_identity(D, ⊙)

## approximate_ring

```
approximate_ring(D, ⊕, N, ⊙, ≈)
```

An approximate ring is an approximate semiring where the `⊕`

operator has inverses defined
by `N`

.

#### Definition

`@inline`

def approximate_ring(D, ⊕, N, ⊙, ≈) =

approximate_abelian_group(D, ⊕, N, ≈) and

approximate_semiring(D, ⊕, ⊙, ≈)

## approximate_semiring

```
approximate_semiring(D, ⊕, ⊙, ≈)
```

An approximate semiring is a set `D`

with two operators, `⊕`

and `⊙`

, where `⊕`

forms an
approximate commutative monoid, `⊙`

forms an approximate monoid and has an approximate zero,
`⊙`

distributes over `⊕`

, and the identity of `⊕`

is approximately equal to the zero of `⊙`

.

#### Definition

`@inline`

def approximate_semiring(D, ⊕, ⊙, ≈) =

approximate_commutative_monoid(D, ⊕, ≈) and

approximate_monoid(D, ⊙, ≈) and

approximately_distributive(D, ⊙, ⊕, ≈) and

approximately_zero_annihilation(D, ⊙, ≈) and

exists(x, y: zero_of_operator[D, ⊙](x) and identity[D, ⊕](y) implies x ≈ y)

## approximately_associative

```
approximately_associative(D, ⊙, ≈)
```

A binary operator `⊙`

is approximately associative if `(a ⊙ b) ⊙ c`

is approximately equal
to `a ⊙ (b ⊙ c)`

for all `a`

, `b`

and `c`

in `D`

, where approximately equal is defined by
the binary relation `≈`

.

#### Definition

`@inline`

def approximately_associative(D, ⊙, ≈) =

binary_operator(D, ⊙) and

reflexive(D, ≈) and

symmetric(D, ≈) and

forall(a ∈ D, b ∈ D, c ∈ D: ((a ⊙ b) ⊙ c) ≈ (a ⊙ (b ⊙ c)))

## approximately_commutative

```
approximately_commutative(D, ⊙, ≈)
```

A binary operator `⊙`

is approximately commutative if `a ⊙ b`

is approximately equal to
`b ⊙ a`

for all `a`

and `b`

in `D`

, where approximately equal is defined by the binary
relation `≈`

.

#### Definition

`@inline`

def approximately_commutative(D, ⊙, ≈) =

binary_operator(D, ⊙) and

reflexive(D, ≈) and

symmetric(D, ≈) and

forall(a ∈ D, b ∈ D: (a ⊙ b) ≈ (b ⊙ a))

## approximately_distributive

```
approximately_distributive(D, ⊗, ⊕, ≈)
```

A binary operator `⊗`

is approximately distributive over another binary operator `⊕`

if it
is approximately both left and right distributive.

#### Definition

`@inline`

def approximately_distributive(D, ⊗, ⊕, ≈) =

approximately_left_distributive(D, ⊗, ⊕, ≈) and

approximately_right_distributive(D, ⊗, ⊕, ≈)

## approximately_has_inverse

```
approximately_has_inverse(D, ⊙, N, ≈)
```

For a binary relation `⊙`

, an inverse of an element `a`

is an element `b`

such that `a ⊙ b`

is approximately equal to the identity element. For `approximately_has_inverse`

, the
inverse operator is given as `N`

, so the inverse of `a`

is `N[a]`

, and approximately equal
to is defined by `≈`

.

#### Definition

`@inline`

def approximately_has_inverse(D, ⊙, N, ≈) =

binary_operator(D, ⊙) and

has_identity(D, ⊙) and

unary_operator(D, N) and

reflexive(D, ≈) and

symmetric(D, ≈) and

forall(a, i: D(a) and identity[D, ⊙](i) implies ((a ⊙ N[a]) ≈ i) and ((N[a] ⊙ a) ≈ i))

## approximately_left_distributive

```
approximately_left_distributive(D, ⊗, ⊕, ≈)
```

A binary operator `⊗`

is approximately left distributive over another binary operator `⊕`

if `a ⊗ (b ⊕ c)`

is approximately equal to `(a ⊗ b) ⊕ (a ⊗ c)`

for all `a`

, `b`

and `c`

in
`D`

.

#### Definition

`@inline`

def approximately_left_distributive(D, ⊗, ⊕, ≈) =

binary_operator(D, ⊗) and

binary_operator(D, ⊕) and

reflexive(D, ≈) and

symmetric(D, ≈) and

forall(a ∈ D, b ∈ D, c ∈ D: (a ⊗ (b ⊕ c)) ≈ ((a ⊗ b) ⊕ (a ⊗ c)))

## approximately_right_distributive

```
approximately_right_distributive(D, ⊗, ⊕, ≈)
```

A binary operator `⊗`

is approximately right distributive over another binary operator `⊕`

if `(a ⊕ b) ⊗ c`

is approximately equal to `(a ⊗ c) ⊕ (b ⊗ c)`

for all `a`

, `b`

and `c`

in
`D`

.

#### Definition

`@inline`

def approximately_right_distributive(D, ⊗, ⊕, ≈) =

binary_operator(D, ⊗) and

binary_operator(D, ⊕) and

reflexive(D, ≈) and

symmetric(D, ≈) and

forall(a ∈ D, b ∈ D, c ∈ D: ((a ⊕ b) ⊗ c) ≈ ((a ⊗ c) ⊕ (b ⊗ c)))

## approximately_zero_annihilation

```
approximately_zero_annihilation(D, ⊙, ≈)
```

A binary relation `⊙`

obeys approximate zero annihilation if there exists an element that
is approximately both a left and right zero.

#### Definition

`@inline`

def approximately_zero_annihilation(D, ⊙, ≈) =

binary_operator(D, ⊙) and

reflexive(D, ≈) and

symmetric(D, ≈) and

exists(zero ∈ D: forall(a ∈ D: ((a ⊙ zero) ≈ zero) and ((zero ⊙ a) ≈ zero)))

## associative

```
associative(D, ⊙)
```

A binary operator `⊙`

is associative if `(a ⊙ b) ⊙ c`

is equal to `a ⊙ (b ⊙ c)`

for all
`a`

, `b`

and `c`

in `D`

.

#### Definition

`@inline`

def associative(D, ⊙) =

approximately_associative(D, ⊙, =)

## binary_operator

```
binary_operator(D, ⊙)
```

A binary operator takes two arguments and returns another argument of the same type, i.e., it can be represented as a relation of arity 3.

#### Definition

`@inline`

def binary_operator(D, ⊙) =

equal(arity[⊙], 3)

## binary_relation

```
binary_relation(∼)
```

`true`

if `∼`

is a binary relation.

Note:
In case of `∼`

is a operator, use space after `∼`

as temporary workaround. eg., `binary_relation(= )`

#### Definition

`@inline`

def binary_relation( ∼ ) = equal(arity[∼], 2)

## binary_relation_substitution_laws

```
binary_relation_substitution_laws(D, R, ≈)
```

A binary relation obeys substitution laws if the relation `R`

produces the same results
when values are substituted according to the binary relation `≈`

.

#### Definition

`@inline`

def binary_relation_substitution_laws(D, ∼, ≈) =

binary_relation(∼ ) and binary_relation(≈ ) and

forall(a1 ∈ D, a2 ∈ D: a1 ≈ a2 ⇒ forall(b ∈ D: a1 ∼ b ≡ a2 ∼ b)) and

forall(b1 ∈ D, b2 ∈ D: b1 ≈ b2 ⇒ forall(a ∈ D: a ∼ b1 ≡ a ∼ b2))

## bounded_lattice

```
bounded_lattice(D, ⊓, ⊔)
```

A lattice is bounded if both the meet and join operators form bounded semilattices.

#### Definition

`@inline`

def bounded_lattice(D, ⊓, ⊔) =

meet_bounded_lattice(D, ⊓, ⊔) and

join_bounded_lattice(D, ⊓, ⊔)

## bounded_semilattice

```
bounded_semilattice(D, ⊓)
```

A bounded semilattice is a semilattice with a maximal element. Equivalently, a semilattice is bounded if it is an idempotent commutative monoid.

#### Definition

`@inline`

def bounded_semilattice(D, ⊓) =

semilattice(D, ⊓) and

commutative_monoid(D, ⊓) and

has_identity(D, ⊓)

## commutative

```
commutative(D, ⊙)
```

A binary operator `⊙`

is commutative if `a ⊙ b`

is equal to `b ⊙ a`

for all `a`

and `b`

in
`D`

.

#### Definition

`@inline`

def commutative(D, ⊙) =

approximately_commutative(D, ⊙, =)

## commutative_monoid

```
commutative_monoid(D, ⊙)
```

A commutative monoid is a monoid where the operator `⊙`

is commutative.

#### Definition

`@inline`

def commutative_monoid(D, ⊙) =

approximate_commutative_monoid(D, ⊙, =) and

commutative(D, ⊙)

## comparable

```
comparable(a, b, ≼)
```

Two elements `a`

and `b`

are comparable if either `a ≼ b`

or `b ≼ a`

.

#### Definition

`@inline`

def comparable(a, b, ≼) =

(a ≼ b) ∨ (b ≼ a)

## distributive

```
distributive(D, ⊗, ⊕)
```

A binary operator `⊗`

is distributive over another binary operator `⊕`

if it is both left
and right distributive.

#### Definition

`@inline`

def distributive(D, ⊗, ⊕) =

approximately_distributive(D, ⊗, ⊕, =)

## equivalence_relation

```
equivalence_relation(D, ∼)
```

A binary relation is an equivalence_relation if it is reflexive, symmetric, and transitive

#### Definition

`@inline`

def equivalence_relation(D, ∼) =

reflexive(D, ∼) and symmetric(D, ∼) and transitive(D, ∼)

## group

```
group(D, ⊙, N)
```

A group is a monoid where the operator `⊙`

has inverses defined by `N`

.

#### Definition

`@inline`

def group(D, ⊙, N) =

approximate_group(D, ⊙, N, =) and

monoid(D, ⊙) and

approximately_has_inverse(D, ⊙, N, =)

## has_identity

```
has_identity(D, ⊙)
```

`true`

if `⊙`

has an identity.

#### Definition

`@inline`

def has_identity(D, ⊙) =

binary_operator(D, ⊙) and

exists(ident ∈ D: forall(a ∈ D: (a ⊙ ident) = a and (ident ⊙ a) = a))

## has_left_identity

```
has_left_identity(D, ⊙)
```

`true`

if `⊙`

has a left identity.

#### Definition

`@inline`

def has_left_identity(D, ⊙) =

binary_operator(D, ⊙) and

equivalence_relation(D, =) and

// TODO: ideally we could do

// exists(ident ∈ D: left_identity[D, ⊙](ident))

// however this doesn't terminate

exists(ident ∈ D: forall(a ∈ D: ((ident ⊙ a) = a)))

## has_left_zero

```
has_left_zero(D, ⊙)
```

`true`

if `⊙`

has a left zero.

#### Definition

`@inline`

def has_left_zero(D, ⊙) =

binary_operator(D, ⊙) and

exists(zero ∈ D: forall(a ∈ D: ((zero ⊙ a) = zero)))

## has_maximal_element

```
has_maximal_element(D, ≼)
```

`true`

if the partial order `≼`

contains a maximal element.

#### Definition

`@inline`

def has_maximal_element(D, ≼) =

partial_order(D, ≼) and

exists(max_elem ∈ D: forall(a ∈ D: a ≼ max_elem))

## has_minimal_element

```
has_minimal_element(D, ≼)
```

`true`

if the partial order `≼`

contains a minimal element.

#### Definition

`@inline`

def has_minimal_element(D, ≼) =

partial_order(D, ≼) and

exists(min_elem ∈ D: forall(a ∈ D: min_elem ≼ a))

## has_right_identity

```
has_right_identity(D, ⊙)
```

`true`

if `⊙`

has a right identity.

#### Definition

`@inline`

def has_right_identity(D, ⊙) =

binary_operator(D, ⊙) and

exists(ident ∈ D: forall(a ∈ D: ((a ⊙ ident) = a)))

## has_right_zero

```
has_right_zero(D, ⊙)
```

`true`

if `⊙`

has a right zero.

#### Definition

`@inline`

def has_right_zero(D, ⊙) =

binary_operator(D, ⊙) and

exists(zero ∈ D: forall(a ∈ D: ((a ⊙ zero) = zero)))

## idempotent

```
idempotent(D, ⊙, ≈)
```

A binary operator `⊙`

is idempotent if `a ⊙ a = a`

for all `a`

in `D`

.

#### Definition

`@inline`

def idempotent(D, ⊙) =

binary_operator(D, ⊙) and

forall(a ∈ D: (a ⊙ a) = a)

## identity

```
identity[D, ⊙]
```

An identity of a binary operator `⊙`

is both a left and right identity.

#### Definition

`@inline`

def identity[D, ⊙] =

ident: D(ident) and

left_identity[D, ⊙](ident) and right_identity[D, ⊙](ident)

## irreflexive

```
irreflexive(D, ∼)
```

A binary relation is irreflexive if `a ∼ a`

is never true for all `a`

in `D`

.

#### Definition

`@inline`

def irreflexive(D, ∼) =

binary_relation(∼ ) and

forall(a ∈ D: ¬(a ∼ a))

## join_bounded_lattice

```
join_bounded_lattice(D, ⊓, ⊔)
```

A lattice is join bounded if the join operator `⊔`

forms a bounded semilattice.

#### Definition

`@inline`

def join_bounded_lattice(D, ⊓, ⊔) =

lattice(D, ⊓, ⊔) and

bounded_semilattice(D, ⊔)

## lattice

```
lattice(D, ⊓, ⊔)
```

A lattice is a set `D`

with two operators, `⊓`

and `⊔`

, usually denoted `join`

and `meet`

respectively, such that `(D, ⊓)`

and `(D, ⊔)`

are semilattices, and the operators `⊓`

and
`⊔`

obey absorption laws.

#### Definition

`@inline`

def lattice(D, ⊓, ⊔) =

semilattice(D, ⊓) and

semilattice(D, ⊔) and

absorption_laws(D, ⊓, ⊔)

## left_distributive

```
left_distributive(D, ⊗, ⊕)
```

A binary operator `⊗`

is left distributive over another binary operator `⊕`

if
`a ⊗ (b ⊕ c)`

is equal to `(a ⊗ b) ⊕ (a ⊗ c)`

for all `a`

, `b`

and `c`

in `D`

.

#### Definition

`@inline`

def left_distributive(D, ⊗, ⊕) =

approximately_left_distributive(D, ⊗, ⊕, =)

## left_identity

```
left_identity[D, ⊙]
```

A left identity of a binary operator `⊙`

is an element `i`

such that `i ⊙ a = a`

for all
`a`

in `D`

.

#### Definition

`@inline`

def left_identity[D, ⊙] =

ident: D(ident) and

forall(a ∈ D: ((ident ⊙ a) = a)) and

binary_operator(D, ⊙)

## left_zero

```
left_zero[D, ⊙]
```

A left zero of a binary operator `⊙`

is an element `z`

such that `z ⊙ a = z`

for all `a`

in
`D`

.

#### Definition

`@inline`

def left_zero[D, ⊙] =

zero: D(zero) and

forall(a ∈ D: ((zero ⊙ a) = zero)) and

binary_operator(D, ⊙)

## maximal_element

```
maximal_element[D, ≼]
```

The maximal element of a partial order `≼`

is an element which is greater than all other
elements in `D`

.

#### Definition

`@inline`

def maximal_element[D, ≼] =

max_elem: D(max_elem) and

partial_order(D, ≼) and

forall(a ∈ D: a ≼ max_elem)

## meet_bounded_lattice

```
meet_bounded_lattice(D, ⊓, ⊔)
```

A lattice is meet bounded if the meet operator `⊓`

forms a bounded semilattice.

#### Definition

`@inline`

def meet_bounded_lattice(D, ⊓, ⊔) =

lattice(D, ⊓, ⊔) and

bounded_semilattice(D, ⊓)

## minimal_element

```
minimal_element[D, ≼]
```

The minimal element of a partial order `≼`

is an element which is less than all other
elements in `D`

.

#### Definition

`@inline`

def minimal_element[D, ≼] =

min_elem: D(min_elem) and

partial_order(D, ≼) and

forall(a ∈ D: min_elem ≼ a)

## monoid

```
monoid(D, ⊙)
```

A monoid is a set `D`

with a binary operator `⊙`

that is associative and has an identity
element.

#### Definition

`@inline`

def monoid(D, ⊙) =

approximate_monoid(D, ⊙, =) and

associative(D, ⊙)

## nullary_relation

```
nullary_relation(∼)
```

`true`

if `∼`

is a relation of 0-arity.

Note:
In case of `∼`

is a operator, use space after `∼`

as temporary workaround. eg., `nullary_relation(= )`

#### Definition

`@inline`

def nullary_relation( ∼ ) = equal(arity[∼], 0)

## partial_order

```
partial_order(D, ≼)
```

A binary relation `≼`

is a partial order if it is reflexive, antisymmetric, and transitive.

#### Definition

`@inline`

def partial_order(D, ≼) =

reflexive(D, ≼) and antisymmetric(D, ≼) and transitive(D, ≼)

## partial_order_and_bounded_lattice

```
partial_order_and_bounded_lattice(D, ≼, ⊓, ⊔)
```

A partially ordered lattice is bounded if is both meet and join bounded.

#### Definition

`@inline`

def partial_order_and_bounded_lattice(D, ≼, ⊓, ⊔) =

partial_order_and_meet_bounded_lattice(D, ≼, ⊓, ⊔) and

partial_order_and_join_bounded_lattice(D, ≼, ⊓, ⊔)

## partial_order_and_join_bounded_lattice

```
partial_order_and_join_bounded_lattice(D, ≼, ⊓, ⊔)
```

A partially ordered lattice is join bounded if the join operator `⊔`

forms a bounded
semilattice, and the identity of `⊔`

is the minimal element of `≼`

.

#### Definition

`@inline`

def partial_order_and_join_bounded_lattice(D, ≼, ⊓, ⊔) =

partial_order_and_lattice(D, ≼, ⊓, ⊔) and

join_bounded_lattice(D, ⊓, ⊔) and

has_maximal_element(D, ≼) and

equal(identity[D, ⊔], minimal_element[D, ≼])

## partial_order_and_lattice

```
partial_order_and_lattice(D, ≼, ⊓, ⊔)
```

A lattice is partially ordered if it has an operator `≼`

defining a partial order, such
that `a ≼ b`

if and only if `(a ⊓ b) = a`

, and `(a ⊔ b) = b`

.

#### Definition

`@inline`

def partial_order_and_lattice(D, ≼, ⊓, ⊔) =

partial_order(D, ≼) and

lattice(D, ⊓, ⊔) and

forall(a ∈ D, b ∈ D: (a ≼ b) ≡ ((a ⊓ b) = a)) and

forall(a ∈ D, b ∈ D: (a ≼ b) ≡ ((a ⊔ b) = b))

## partial_order_and_meet_bounded_lattice

```
partial_order_and_meet_bounded_lattice(D, ≼, ⊓, ⊔)
```

A partially ordered lattice is meet bounded if the meet operator `⊓`

forms a bounded
semilattice, and the identity of `⊓`

is the maximal element of `≼`

.

#### Definition

`@inline`

def partial_order_and_meet_bounded_lattice(D, ≼, ⊓, ⊔) =

partial_order_and_lattice(D, ≼, ⊓, ⊔) and

meet_bounded_lattice(D, ⊓, ⊔) and

has_minimal_element(D, ≼) and

equal(identity[D, ⊓], maximal_element[D, ≼])

## preorder

```
preorder(D, ≼)
```

A binary relation `≼`

is a preorder if it is reflexive and transitive.

#### Definition

`@inline`

def preorder(D, ≼) =

reflexive(D, ≼) and transitive(D, ≼)

## reflexive

```
reflexive(D, ∼)
```

A binary relation is reflexive if `a ∼ a`

is always true for all `a`

in `D`

.

#### Definition

`@inline`

def reflexive(D, ∼) =

binary_relation(∼ ) and

forall(a ∈ D: a ∼ a)

## right_distributive

```
right_distributive(D, ⊗, ⊕, ≈)
```

A binary operator `⊗`

is right distributive over another binary operator `⊕`

if
`(a ⊕ b) ⊗ c`

is equal to `(a ⊗ c) ⊕ (b ⊗ c)`

for all `a`

, `b`

and `c`

in `D`

.

#### Definition

`@inline`

def right_distributive(D, ⊗, ⊕) =

approximately_right_distributive(D, ⊗, ⊕, =)

## right_identity

```
right_identity[D, ⊙]
```

A right identity of a binary operator `⊙`

is an element `i`

such that `a ⊙ i = a`

for all
`a`

in `D`

.

#### Definition

`@inline`

def right_identity[D, ⊙] =

ident: D(ident) and

forall(a ∈ D: ((a ⊙ ident) = a)) and

binary_operator(D, ⊙)

## right_zero

```
right_zero[D, ⊙]
```

A right zero of a binary operator `⊙`

is an element `z`

such that `z ⊙ a = z`

for all `a`

in `D`

.

#### Definition

`@inline`

def right_zero[D, ⊙] =

zero: D(zero) and

forall(a ∈ D: ((a ⊙ zero) = zero)) and

binary_operator(D, ⊙)

## ring

```
ring(D, ⊕, N, ⊙)
```

A ring is a semiring where the `⊕`

operator has inverses.

#### Definition

`@inline`

def ring(D, ⊕, N, ⊙) =

approximate_ring(D, ⊕, N, ⊙, =) and

abelian_group(D, ⊕, N) and

semiring(D, ⊕, ⊙)

## semilattice

```
semilattice(D, ⊓)
```

A semilattice is a set `D`

, with an operator `⊓`

, such that `⊓`

is commutative,
associative, and idempotent. The classic example of a semilattice is a set of subsets with
the intersection operator.

#### Definition

`@inline`

def semilattice(D, ⊓) =

commutative(D, ⊓) and

associative(D, ⊓) and

idempotent(D, ⊓)

## semiring

```
semiring(D, ⊕, ⊙)
```

A semiring is an approximate semiring with equality defined as `=`

.

#### Definition

`@inline`

def semiring(D, ⊕, ⊙) =

approximate_semiring(D, ⊕, ⊙, =) and

commutative_monoid(D, ⊕) and

monoid(D, ⊙) and

distributive(D, ⊙, ⊕) and

zero_annihilation(D, ⊙) and

equal(zero_of_operator[D, ⊙], identity[D, ⊕])

## strict_partial_order

```
strict_partial_order(D, ≺)
```

A binary relation `≺`

is a strict partial order if it is irreflexive, antisymmetric, and
transitive. This is similar to a partial order, but is irreflexive rather than reflexive.

#### Definition

`@inline`

def strict_partial_order(D, ≺) =

irreflexive(D, ≺) and antisymmetric(D, ≺) and transitive(D, ≺)

## strict_total_order

```
strict_total_order(D, ≺)
```

A binary relation `≺`

is a strict total order if it is a strict partial order, and every
element in `D`

is either comparable or equal to another element in `D`

.

#### Definition

`@inline`

def strict_total_order(D, ≺) =

strict_partial_order(D, ≺) and

forall(a ∈ D, b ∈ D: comparable(a, b, ≺) ∨ (b = a))

## symmetric

```
symmetric(D, ∼)
```

A binary relation is symmetric if for all `a`

and `b`

in `D`

, whenever `a ∼ b`

is true,
then also `b ∼ a`

is also true.

#### Definition

`@inline`

def symmetric(D, ∼) =

binary_relation(∼ ) and

forall(a ∈ D, b ∈ D: a ∼ b ≡ b ∼ a)

## ternary_relation

```
ternary_relation(∼)
```

`true`

if `∼`

is a ternary relation.

Note:
In case of `∼`

is a operator, use space after `∼`

as temporary workaround. eg., `ternary_relation(= )`

#### Definition

`@inline`

def ternary_relation( ∼ ) = equal(arity[∼], 3)

## total_order

```
total_order(D, ≼)
```

A binary relation `≼`

is a total order if it is a partial order, and every element in `D`

is comparable with every other element in `D`

with respect to the partial order.

#### Definition

`@inline`

def total_order(D, ≼) =

partial_order(D, ≼) and

forall(a ∈ D, b ∈ D: comparable(a, b, ≼))

## transitive

```
transitive(D, ∼)
```

A binary relation is transitive if for all `a`

, `b`

and `c`

in `D`

, whenever `a ∼ b`

and
`b ∼ c`

are true, then also `a ∼ c`

is true.

#### Definition

`@inline`

def transitive(D, ∼) =

binary_relation(∼ ) and

forall(a ∈ D, b ∈ D, c ∈ D: a ∼ b and b ∼ c implies a ∼ c)

## unary_operator

```
unary_operator(D, ⊙)
```

A unary operator takes one argument and returns another argument of the same type, i.e., it can be represented as a binary relation.

#### Definition

`@inline`

def unary_operator(D, ⊙) =

equal(arity[⊙], 2)

## unary_relation

```
unary_relation(∼)
```

`true`

if `∼`

is a unary relation.

Note:
In case of `∼`

is a operator, use space after `∼`

as temporary workaround. eg., `unary_relation(= )`

#### Definition

`@inline`

def unary_relation( ∼ ) = equal(arity[∼], 1)

## unary_relation_substitution_laws

```
unary_relation_substitution_laws(D, R, ≈)
```

A unary relation obeys substitution laws if the relation `R`

produces the same results when
values are substituted according to the binary relation `≈`

.

For example, `unary_relation_substitution_laws({1; 2}, {1; 2}, (1, 2))`

is true because
the result of `R(1)`

remains true when `1`

is replaced by `2`

.

#### Definition

`@inline`

def unary_relation_substitution_laws(D, R, ≈) =

unary_relation(R) and binary_relation(≈ ) and

forall(a ∈ D, b ∈ D: (a ≈ b) ⇒ (R(a) ≡ R(b)))

## zero_annihilation

```
zero_annihilation(D, ⊙)
```

A binary relation `⊙`

obeys zero annihilation if there exists an element that is both a
left and right zero.

#### Definition

`@inline`

def zero_annihilation(D, ⊙) =

approximately_zero_annihilation(D, ⊙, =)

## zero_of_operator

```
zero_of_operator[D, ⊙]
```

A zero of a binary operator `⊙`

is an element that is both a left and right zero.

#### Definition

`@inline`

def zero_of_operator[D, ⊙] =

zero: D(zero) and

left_zero[D, ⊙](zero) and

right_zero[D, ⊙](zero)