typelevel / algebra
1
package algebra
2
package lattice
3

4
import ring.BoolRing
5
import scala.{specialized => sp}
6

7
/**
8
 * Boolean algebras are Heyting algebras with the additional
9
 * constraint that the law of the excluded middle is true
10
 * (equivalently, double-negation is true).
11
 *
12
 * This means that in addition to the laws Heyting algebras obey,
13
 * boolean algebras also obey the following:
14
 *
15
 *  - (a ∨ ¬a) = 1
16
 *  - ¬¬a = a
17
 *
18
 * Boolean algebras generalize classical logic: one is equivalent to
19
 * "true" and zero is equivalent to "false". Boolean algebras provide
20
 * additional logical operators such as `xor`, `nand`, `nor`, and
21
 * `nxor` which are commonly used.
22
 *
23
 * Every boolean algebras has a dual algebra, which involves reversing
24
 * true/false as well as and/or.
25
 */
26
trait Bool[@sp(Int, Long) A] extends Any with Heyting[A] with GenBool[A] { self =>
27 2
  def imp(a: A, b: A): A = or(complement(a), b)
28 2
  def without(a: A, b: A): A = and(a, complement(b))
29

30
  // xor is already defined in both Heyting and GenBool.
31
  // In Bool, the definitions coincide, so we just use one of them.
32
  override def xor(a: A, b: A): A =
33 2
    or(without(a, b), without(b, a))
34

35 0
  override def dual: Bool[A] = new DualBool(this)
36

37
  /**
38
   * Every Boolean algebra is a BoolRing, with multiplication defined as
39
   * `and` and addition defined as `xor`. Bool does not extend BoolRing
40
   * because, e.g. we might want a Bool[Int] and CommutativeRing[Int] to
41
   * refer to different structures, by default.
42
   *
43
   * Note that the ring returned by this method is not an extension of
44
   * the `Rig` returned from `BoundedDistributiveLattice.asCommutativeRig`.
45
   */
46 2
  override def asBoolRing: BoolRing[A] = new BoolRingFromBool(self)
47
}
48

49
class DualBool[@sp(Int, Long) A](orig: Bool[A]) extends Bool[A] {
50 0
  def one: A = orig.zero
51 0
  def zero: A = orig.one
52 0
  def and(a: A, b: A): A = orig.or(a, b)
53 0
  def or(a: A, b: A): A = orig.and(a, b)
54 0
  def complement(a: A): A = orig.complement(a)
55 0
  override def xor(a: A, b: A): A = orig.complement(orig.xor(a, b))
56

57 0
  override def imp(a: A, b: A): A = orig.and(orig.complement(a), b)
58 0
  override def nand(a: A, b: A): A = orig.nor(a, b)
59 0
  override def nor(a: A, b: A): A = orig.nand(a, b)
60 0
  override def nxor(a: A, b: A): A = orig.xor(a, b)
61

62 0
  override def dual: Bool[A] = orig
63
}
64

65
private[lattice] class BoolRingFromBool[A](orig: Bool[A]) extends BoolRngFromGenBool(orig) with BoolRing[A] {
66 2
  def one: A = orig.one
67
}
68

69
/**
70
 * Every Boolean ring gives rise to a Boolean algebra:
71
 *  - 0 and 1 are preserved;
72
 *  - ring multiplication (`times`) corresponds to `and`;
73
 *  - ring addition (`plus`) corresponds to `xor`;
74
 *  - `a or b` is then defined as `a xor b xor (a and b)`;
75
 *  - complement (`¬a`) is defined as `a xor 1`.
76
 */
77
class BoolFromBoolRing[A](orig: BoolRing[A]) extends GenBoolFromBoolRng(orig) with Bool[A] {
78 2
  def one: A = orig.one
79 2
  def complement(a: A): A = orig.plus(orig.one, a)
80 2
  override def without(a: A, b: A): A = super[GenBoolFromBoolRng].without(a, b)
81 0
  override def asBoolRing: BoolRing[A] = orig
82

83 2
  override def meet(a: A, b: A): A = super[GenBoolFromBoolRng].meet(a, b)
84 2
  override def join(a: A, b: A): A = super[GenBoolFromBoolRng].join(a, b)
85
}
86

87
object Bool extends HeytingFunctions[Bool] with GenBoolFunctions[Bool] {
88

89
  /**
90
   * Access an implicit `Bool[A]`.
91
   */
92
  @inline final def apply[@sp(Int, Long) A](implicit ev: Bool[A]): Bool[A] = ev
93
}

Read our documentation on viewing source code .

Loading