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 .