package lattice
 Alphabetic
 Public
 All
Type Members

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, doublenegation is true).
Boolean algebras are Heyting algebras with the additional constraint that the law of the excluded middle is true (equivalently, doublenegation 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
, andnxor
which are commonly used.Every boolean algebras has a dual algebra, which involves reversing true/false as well as and/or.

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 toand
;  ring addition (
plus
) corresponds toxor
; a or b
is then defined asa xor b xor (a and b)
; complement (
¬a
) is defined asa xor 1
.

trait
BoundedDistributiveLattice[A] extends BoundedLattice[A] with DistributiveLattice[A]
A bounded distributive lattice is a lattice that both bounded and distributive
 trait BoundedJoinSemilattice[A] extends JoinSemilattice[A]
 trait BoundedJoinSemilatticeFunctions[B[A] <: BoundedJoinSemilattice[A]] extends JoinSemilatticeFunctions[B]

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)
 trait BoundedMeetSemilattice[A] extends MeetSemilattice[A]
 trait BoundedMeetSemilatticeFunctions[B[A] <: BoundedMeetSemilattice[A]] extends MeetSemilatticeFunctions[B]

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.
 trait DeMorganFunctions[H[A] <: DeMorgan[A]] extends BoundedMeetSemilatticeFunctions[H] with BoundedJoinSemilatticeFunctions[H] with LogicFunctions[H]

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)
 class DualBool[A] extends Bool[A]

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

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 toand
;  ring addition (
plus
) corresponds toxor
; a or b
is then defined asa xor b xor (a and b)
; relative complement
a\b
is defined asa xor (a and b)
.
BoolRng.asBool.asBoolRing
gives back the originalBoolRng
.  trait GenBoolFunctions[G[A] <: GenBool[A]] extends BoundedJoinSemilatticeFunctions[G] with MeetSemilatticeFunctions[G]

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 tomeet
andor
is equivalent tojoin
; both methods are available.Heyting algebra also define
complement
operation (sometimes written as ¬a). The complement ofa
is equivalent to(a → 0)
, and the following laws hold: a ∧ ¬a = 0
However, in Heyting algebras this operation is only a pseudocomplement, 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
.  trait HeytingFunctions[H[A] <: Heyting[A]] extends BoundedMeetSemilatticeFunctions[H] with BoundedJoinSemilatticeFunctions[H]
 trait HeytingGenBoolOverlap[H[A] <: Heyting[A]] extends AnyRef

trait
JoinSemilattice[A] extends Serializable
A joinsemilattice (or upper semilattice) is a semilattice whose operation is called "join", and which can be thought of as a least upper bound.
 trait JoinSemilatticeFunctions[J[A] <: JoinSemilattice[A]] extends AnyRef

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 meetsemilattices 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

trait
Logic[A] extends BoundedDistributiveLattice[A]
Logic models a logic generally.
 trait LogicFunctions[H[A] <: Logic[A]] extends AnyRef

trait
MeetSemilattice[A] extends Serializable
A meetsemilattice (or lower semilattice) is a semilattice whose operation is called "meet", and which can be thought of as a greatest lower bound.
 trait MeetSemilatticeFunctions[M[A] <: MeetSemilattice[A]] extends AnyRef
 class MinMaxBoundedDistributiveLattice[A] extends MinMaxLattice[A] with BoundedDistributiveLattice[A]
 class MinMaxLattice[A] extends DistributiveLattice[A]
Value Members
 object Bool extends HeytingFunctions[Bool] with GenBoolFunctions[Bool] with Serializable
 object BoundedDistributiveLattice extends BoundedMeetSemilatticeFunctions[BoundedDistributiveLattice] with BoundedJoinSemilatticeFunctions[BoundedDistributiveLattice] with Serializable
 object BoundedJoinSemilattice extends JoinSemilatticeFunctions[BoundedJoinSemilattice] with BoundedJoinSemilatticeFunctions[BoundedJoinSemilattice] with Serializable
 object BoundedLattice extends BoundedMeetSemilatticeFunctions[BoundedLattice] with BoundedJoinSemilatticeFunctions[BoundedLattice] with Serializable
 object BoundedMeetSemilattice extends BoundedMeetSemilatticeFunctions[BoundedMeetSemilattice] with Serializable
 object DeMorgan extends DeMorganFunctions[DeMorgan] with Serializable
 object DistributiveLattice extends JoinSemilatticeFunctions[DistributiveLattice] with MeetSemilatticeFunctions[DistributiveLattice] with Serializable
 object GenBool extends GenBoolFunctions[GenBool] with Serializable
 object Heyting extends HeytingFunctions[Heyting] with HeytingGenBoolOverlap[Heyting] with Serializable
 object JoinSemilattice extends JoinSemilatticeFunctions[JoinSemilattice] with Serializable
 object Lattice extends JoinSemilatticeFunctions[Lattice] with MeetSemilatticeFunctions[Lattice] with Serializable
 object Logic extends LogicFunctions[Logic] with Serializable
 object MeetSemilattice extends MeetSemilatticeFunctions[MeetSemilattice] with Serializable