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)

   Or written using traditional notation:

   (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.

    See also

    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]