typelevel / algebra
 1 ```package algebra ``` 2 ```package lattice ``` 3 4 ```import scala.{specialized => sp} ``` 5 6 ```/** ``` 7 ``` * Heyting algebras are bounded lattices that are also equipped with ``` 8 ``` * an additional binary operation `imp` (for implication, also ``` 9 ``` * written as →). ``` 10 ``` * ``` 11 ``` * Implication obeys the following laws: ``` 12 ``` * ``` 13 ``` * - a → a = 1 ``` 14 ``` * - a ∧ (a → b) = a ∧ b ``` 15 ``` * - b ∧ (a → b) = b ``` 16 ``` * - a → (b ∧ c) = (a → b) ∧ (a → c) ``` 17 ``` * ``` 18 ``` * In heyting algebras, `and` is equivalent to `meet` and `or` is ``` 19 ``` * equivalent to `join`; both methods are available. ``` 20 ``` * ``` 21 ``` * Heyting algebra also define `complement` operation (sometimes ``` 22 ``` * written as ¬a). The complement of `a` is equivalent to `(a → 0)`, ``` 23 ``` * and the following laws hold: ``` 24 ``` * ``` 25 ``` * - a ∧ ¬a = 0 ``` 26 ``` * ``` 27 ``` * However, in Heyting algebras this operation is only a ``` 28 ``` * pseudo-complement, since Heyting algebras do not necessarily ``` 29 ``` * provide the law of the excluded middle. This means that there is no ``` 30 ``` * guarantee that (a ∨ ¬a) = 1. ``` 31 ``` * ``` 32 ``` * Heyting algebras model intuitionistic logic. For a model of ``` 33 ``` * classical logic, see the boolean algebra type class implemented as ``` 34 ``` * `Bool`. ``` 35 ``` */ ``` 36 ```trait Heyting[@sp(Int, Long) A] extends Any with BoundedDistributiveLattice[A] { self => ``` 37 ``` def and(a: A, b: A): A ``` 38 2 ``` def meet(a: A, b: A): A = and(a, b) ``` 39 40 ``` def or(a: A, b: A): A ``` 41 2 ``` def join(a: A, b: A): A = or(a, b) ``` 42 43 ``` def imp(a: A, b: A): A ``` 44 ``` def complement(a: A): A ``` 45 46 0 ``` def xor(a: A, b: A): A = or(and(a, complement(b)), and(complement(a), b)) ``` 47 0 ``` def nand(a: A, b: A): A = complement(and(a, b)) ``` 48 0 ``` def nor(a: A, b: A): A = complement(or(a, b)) ``` 49 0 ``` def nxor(a: A, b: A): A = complement(xor(a, b)) ``` 50 ```} ``` 51 52 ```trait HeytingGenBoolOverlap[H[A] <: Heyting[A]] { ``` 53 ``` def and[@sp(Int, Long) A](x: A, y: A)(implicit ev: H[A]): A = ``` 54 0 ``` ev.and(x, y) ``` 55 ``` def or[@sp(Int, Long) A](x: A, y: A)(implicit ev: H[A]): A = ``` 56 0 ``` ev.or(x, y) ``` 57 ``` def xor[@sp(Int, Long) A](x: A, y: A)(implicit ev: H[A]): A = ``` 58 0 ``` ev.xor(x, y) ``` 59 ```} ``` 60 61 ```trait HeytingFunctions[H[A] <: Heyting[A]] extends ``` 62 ``` BoundedMeetSemilatticeFunctions[H] with ``` 63 ``` BoundedJoinSemilatticeFunctions[H] { ``` 64 65 ``` def complement[@sp(Int, Long) A](x: A)(implicit ev: H[A]): A = ``` 66 0 ``` ev.complement(x) ``` 67 68 ``` def imp[@sp(Int, Long) A](x: A, y: A)(implicit ev: H[A]): A = ``` 69 0 ``` ev.imp(x, y) ``` 70 ``` def nor[@sp(Int, Long) A](x: A, y: A)(implicit ev: H[A]): A = ``` 71 0 ``` ev.nor(x, y) ``` 72 ``` def nxor[@sp(Int, Long) A](x: A, y: A)(implicit ev: H[A]): A = ``` 73 0 ``` ev.nxor(x, y) ``` 74 ``` def nand[@sp(Int, Long) A](x: A, y: A)(implicit ev: H[A]): A = ``` 75 0 ``` ev.nand(x, y) ``` 76 ```} ``` 77 78 79 ```object Heyting extends HeytingFunctions[Heyting] with HeytingGenBoolOverlap[Heyting] { ``` 80 81 ``` /** ``` 82 ``` * Access an implicit `Heyting[A]`. ``` 83 ``` */ ``` 84 ``` @inline final def apply[@sp(Int, Long) A](implicit ev: Heyting[A]): Heyting[A] = ev ``` 85 ```} ```

Read our documentation on viewing source code .