typelevel / algebra
1
package algebra
2
package lattice
3

4
import scala.{specialized => sp}
5

6
/**
7
  * Logic models a logic generally. It is a bounded distributive
8
  * lattice with an extra negation operator.
9
  *
10
  * The negation operator obeys the weak De Morgan laws:
11
  *  - ¬(x∨y) = ¬x∧¬y
12
  *  - ¬(x∧y) = ¬¬(¬x∨¬y)
13
  *
14
  * For intuitionistic logic see [[Heyting]]
15
  * For fuzzy logic see [[DeMorgan]]
16
  */
17
trait Logic[@sp(Int, Long) A] extends Any with BoundedDistributiveLattice[A] { self =>
18
  def and(a: A, b: A): A
19

20
  def or(a: A, b: A): A
21

22
  def not(a: A): A
23

24 0
  def xor(a: A, b: A): A = or(and(a, not(b)), and(not(a), b))
25 0
  def nand(a: A, b: A): A = not(and(a, b))
26 0
  def nor(a: A, b: A): A = not(or(a, b))
27 0
  def nxor(a: A, b: A): A = not(xor(a, b))
28
}
29

30
trait LogicFunctions[H[A] <: Logic[A]] {
31
  def complement[@sp(Int, Long) A](x: A)(implicit ev: H[A]): A =
32 0
    ev.not(x)
33

34
  def nor[@sp(Int, Long) A](x: A, y: A)(implicit ev: H[A]): A =
35 0
    ev.nor(x, y)
36
  def nxor[@sp(Int, Long) A](x: A, y: A)(implicit ev: H[A]): A =
37 0
    ev.nxor(x, y)
38
  def nand[@sp(Int, Long) A](x: A, y: A)(implicit ev: H[A]): A =
39 0
    ev.nand(x, y)
40
}
41

42

43
object Logic extends LogicFunctions[Logic] {
44

45
  /**
46
    * Access an implicit `Logic[A]`.
47
    */
48
  @inline final def apply[@sp(Int, Long) A](implicit ev: Logic[A]): Logic[A] = ev
49

50
  /**
51
    * Turn a [[Heyting]] into a `Logic`.
52
    * Used for binary compatibility.
53
    */
54
  final def fromHeyting[@sp(Int, Long) A](h: Heyting[A]): Logic[A] =
55 2
    new Logic[A] {
56 2
      def and(a: A, b: A): A = h.and(a, b)
57

58 2
      def or(a: A, b: A): A = h.or(a, b)
59

60 2
      def not(a: A): A = h.complement(a)
61

62 2
      def zero: A = h.zero
63

64 2
      def one: A = h.one
65

66 2
      def meet(lhs: A, rhs: A): A = h.meet(lhs, rhs)
67

68 2
      def join(lhs: A, rhs: A): A = h.join(lhs, rhs)
69
    }
70
}

Read our documentation on viewing source code .

Loading