p

algebra

# lattice 

Ordering
1. Alphabetic
Visibility
1. Public
2. All

### Type Members

1. trait Bool[A] extends Heyting[A] with GenBool[A]

Boolean algebras are Heyting algebras with the additional constraint that the law of the excluded middle is true (equivalently, double-negation is true).

Boolean algebras are Heyting algebras with the additional constraint that the law of the excluded middle is true (equivalently, double-negation is true).

This means that in addition to the laws Heyting algebras obey, boolean algebras also obey the following:

• (a ∨ ¬a) = 1
• ¬¬a = a

Boolean algebras generalize classical logic: one is equivalent to "true" and zero is equivalent to "false". Boolean algebras provide additional logical operators such as `xor`, `nand`, `nor`, and `nxor` which are commonly used.

Every boolean algebras has a dual algebra, which involves reversing true/false as well as and/or.

2. class BoolFromBoolRing[A] extends GenBoolFromBoolRng[A] with Bool[A]

Every Boolean ring gives rise to a Boolean algebra:

Every Boolean ring gives rise to a Boolean algebra:

• 0 and 1 are preserved;
• ring multiplication (`times`) corresponds to `and`;
• ring addition (`plus`) corresponds to `xor`;
• `a or b` is then defined as `a xor b xor (a and b)`;
• complement (`¬a`) is defined as `a xor 1`.
3. trait BoundedDistributiveLattice[A] extends BoundedLattice[A] with DistributiveLattice[A]

A bounded distributive lattice is a lattice that both bounded and distributive

4. trait BoundedJoinSemilattice[A] extends JoinSemilattice[A]
5. trait BoundedJoinSemilatticeFunctions[B[A] <: BoundedJoinSemilattice[A]] extends JoinSemilatticeFunctions[B]
6. trait BoundedLattice[A] extends Lattice[A] with BoundedMeetSemilattice[A] with BoundedJoinSemilattice[A]

A bounded lattice is a lattice that additionally has one element that is the bottom (zero, also written as ⊥), and one element that is the top (one, also written as ⊤).

A bounded lattice is a lattice that additionally has one element that is the bottom (zero, also written as ⊥), and one element that is the top (one, also written as ⊤).

This means that for any a in A:

join(zero, a) = a = meet(one, a)

(0 ∨ a) = a = (1 ∧ a)

7. trait BoundedMeetSemilattice[A] extends MeetSemilattice[A]
8. trait BoundedMeetSemilatticeFunctions[B[A] <: BoundedMeetSemilattice[A]] extends MeetSemilatticeFunctions[B]
9. trait DeMorgan[A] extends Logic[A]

De Morgan algebras are bounded lattices that are also equipped with a De Morgan involution.

De Morgan algebras are bounded lattices that are also equipped with a De Morgan involution.

De Morgan involution obeys the following laws:

• ¬¬a = a
• ¬(x∧y) = ¬x∨¬y

However, in De Morgan algebras this involution does not necessarily provide the law of the excluded middle. This means that there is no guarantee that (a ∨ ¬a) = 1. De Morgan algebra do not not necessarily provide the law of non contradiction either. This means that there is no guarantee that (a ∧ ¬a) = 0.

De Morgan algebras are useful to model fuzzy logic. For a model of classical logic, see the boolean algebra type class implemented as Bool.

10. trait DeMorganFunctions[H[A] <: DeMorgan[A]] extends BoundedMeetSemilatticeFunctions[H] with BoundedJoinSemilatticeFunctions[H] with LogicFunctions[H]
11. trait DistributiveLattice[A] extends Lattice[A]

A distributive lattice a lattice where join and meet distribute:

A distributive lattice a lattice where join and meet distribute:

• a ∨ (b ∧ c) = (a ∨ b) ∧ (a ∨ c)
• a ∧ (b ∨ c) = (a ∧ b) ∨ (a ∧ c)
12. class DualBool[A] extends Bool[A]
13. trait GenBool[A] extends DistributiveLattice[A] with BoundedJoinSemilattice[A]

Generalized Boolean algebra, that is, a Boolean algebra without the top element.

Generalized Boolean algebra, that is, a Boolean algebra without the top element. Generalized Boolean algebras do not (in general) have (absolute) complements, but they have relative complements (see GenBool.without).

14. class GenBoolFromBoolRng[A] extends GenBool[A]

Every Boolean rng gives rise to a Boolean algebra without top:

Every Boolean rng gives rise to a Boolean algebra without top:

• 0 is preserved;
• ring multiplication (`times`) corresponds to `and`;
• ring addition (`plus`) corresponds to `xor`;
• `a or b` is then defined as `a xor b xor (a and b)`;
• relative complement `a\b` is defined as `a xor (a and b)`.

`BoolRng.asBool.asBoolRing` gives back the original `BoolRng`.

algebra.lattice.GenBool.asBoolRing

15. trait GenBoolFunctions[G[A] <: GenBool[A]] extends BoundedJoinSemilatticeFunctions[G] with MeetSemilatticeFunctions[G]
16. trait Heyting[A] extends BoundedDistributiveLattice[A]

Heyting algebras are bounded lattices that are also equipped with an additional binary operation `imp` (for implication, also written as →).

Heyting algebras are bounded lattices that are also equipped with an additional binary operation `imp` (for implication, also written as →).

Implication obeys the following laws:

• a → a = 1
• a ∧ (a → b) = a ∧ b
• b ∧ (a → b) = b
• a → (b ∧ c) = (a → b) ∧ (a → c)

In heyting algebras, `and` is equivalent to `meet` and `or` is equivalent to `join`; both methods are available.

Heyting algebra also define `complement` operation (sometimes written as ¬a). The complement of `a` is equivalent to `(a → 0)`, and the following laws hold:

• a ∧ ¬a = 0

However, in Heyting algebras this operation is only a pseudo-complement, since Heyting algebras do not necessarily provide the law of the excluded middle. This means that there is no guarantee that (a ∨ ¬a) = 1.

Heyting algebras model intuitionistic logic. For a model of classical logic, see the boolean algebra type class implemented as `Bool`.

17. trait HeytingFunctions[H[A] <: Heyting[A]] extends BoundedMeetSemilatticeFunctions[H] with BoundedJoinSemilatticeFunctions[H]
18. trait HeytingGenBoolOverlap[H[A] <: Heyting[A]] extends AnyRef
19. trait JoinSemilattice[A] extends Serializable

A join-semilattice (or upper semilattice) is a semilattice whose operation is called "join", and which can be thought of as a least upper bound.

20. trait JoinSemilatticeFunctions[J[A] <: JoinSemilattice[A]] extends AnyRef
21. trait Lattice[A] extends JoinSemilattice[A] with MeetSemilattice[A]

A lattice is a set `A` together with two operations (meet and join).

A lattice is a set `A` together with two operations (meet and join). Both operations individually constitute semilattices (join- and meet-semilattices respectively): each operation is commutative, associative, and idempotent.

Join can be thought of as finding a least upper bound (supremum), and meet can be thought of as finding a greatest lower bound (infimum).

The join and meet operations are also linked by absorption laws:

meet(a, join(a, b)) = join(a, meet(a, b)) = a

22. trait Logic[A] extends BoundedDistributiveLattice[A]

Logic models a logic generally.

Logic models a logic generally. It is a bounded distributive lattice with an extra negation operator.

The negation operator obeys the weak De Morgan laws:

• ¬(x∨y) = ¬x∧¬y
• ¬(x∧y) = ¬¬(¬x∨¬y)

For intuitionistic logic see Heyting For fuzzy logic see DeMorgan

23. trait LogicFunctions[H[A] <: Logic[A]] extends AnyRef
24. trait MeetSemilattice[A] extends Serializable

A meet-semilattice (or lower semilattice) is a semilattice whose operation is called "meet", and which can be thought of as a greatest lower bound.

25. trait MeetSemilatticeFunctions[M[A] <: MeetSemilattice[A]] extends AnyRef
26. class MinMaxBoundedDistributiveLattice[A] extends MinMaxLattice[A] with BoundedDistributiveLattice[A]
27. class MinMaxLattice[A] extends DistributiveLattice[A]

### Value Members

1. object Bool extends HeytingFunctions[Bool] with GenBoolFunctions[Bool] with Serializable
2. object
3. object
4. object
5. object
6. object DeMorgan extends DeMorganFunctions[DeMorgan] with Serializable
7. object
8. object GenBool extends GenBoolFunctions[GenBool] with Serializable
9. object Heyting extends HeytingFunctions[Heyting] with HeytingGenBoolOverlap[Heyting] with Serializable
10. object
11. object Lattice extends JoinSemilatticeFunctions[Lattice] with MeetSemilatticeFunctions[Lattice] with Serializable
12. object Logic extends LogicFunctions[Logic] with Serializable
13. object