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 .

Loading