typelevel / algebra
1
package algebra.laws
2

3
import algebra._
4
import algebra.lattice.{Heyting, Bool, GenBool}
5

6
import org.scalacheck.{Arbitrary, Prop}
7
import org.scalacheck.Prop._
8

9
object LogicLaws {
10 3
  def apply[A: Eq: Arbitrary] = new LogicLaws[A] {
11 3
    def Equ = Eq[A]
12 3
    def Arb = implicitly[Arbitrary[A]]
13
  }
14
}
15

16
trait LogicLaws[A] extends LatticeLaws[A] {
17

18 3
  def heyting(implicit A: Heyting[A]) = new LogicProperties(
19 3
    name = "heyting",
20 3
    parents = Seq(),
21 3
    ll = boundedDistributiveLattice,
22

23 3
    Rules.distributive(A.or)(A.and),
24

25 3
    "consistent" -> forAll { (x: A) => A.and(x, A.complement(x)) ?== A.zero },
26 3
    "¬x = (x → 0)" -> forAll { (x: A) => A.complement(x) ?== A.imp(x, A.zero) },
27 3
    "x → x = 1" -> forAll { (x: A) => A.imp(x, x) ?== A.one },
28

29 3
    "if x → y and y → x then x=y" -> forAll { (x: A, y: A) =>
30 3
      (A.imp(x, y) ?!= A.one) || (A.imp(y, x) ?!= A.one) || (x ?== y)
31
    },
32

33 3
    "if (1 → x)=1 then x=1" -> forAll { (x: A) =>
34 3
      (A.imp(A.one, x) ?!= A.one) || (x ?== A.one)
35
    },
36

37 3
    "x → (y → x) = 1" -> forAll { (x: A, y: A) => A.imp(x, A.imp(y, x)) ?== A.one },
38

39 3
    "(x→(y→z)) → ((x→y)→(x→z)) = 1" -> forAll { (x: A, y: A, z: A) =>
40 3
      A.imp(A.imp(x, A.imp(y, z)), A.imp(A.imp(x, y), A.imp(x, z))) ?== A.one
41
    },
42

43 3
    "x∧y → x = 1" -> forAll { (x: A, y: A) => A.imp(A.and(x, y), x) ?== A.one },
44 3
    "x∧y → y = 1" -> forAll { (x: A, y: A) => A.imp(A.and(x, y), y) ?== A.one },
45 3
    "x → y → (x∧y) = 1" -> forAll { (x: A, y: A) => A.imp(x, A.imp(y, A.and(x, y))) ?== A.one },
46

47 3
    "x → x∨y" -> forAll { (x: A, y: A) => A.imp(x, A.or(x, y)) ?== A.one },
48 3
    "y → x∨y" -> forAll { (x: A, y: A) => A.imp(y, A.or(x, y)) ?== A.one },
49

50 3
    "(x → z) → ((y → z) → ((x | y) → z)) = 1" -> forAll { (x: A, y: A, z: A) =>
51 3
      A.imp(A.imp(x, z), A.imp(A.imp(y, z), A.imp(A.or(x, y), z))) ?== A.one
52
    },
53

54 3
    "(0 → x) = 1" -> forAll { (x: A) => A.imp(A.zero, x) ?== A.one }
55
  )
56

57 3
  def generalizedBool(implicit A: GenBool[A]) = new LogicProperties(
58 3
    name = "generalized bool",
59 3
    parents = Seq(),
60 3
    ll = new LatticeProperties(
61 3
      name = "lowerBoundedDistributiveLattice",
62 3
      parents = Seq(boundedJoinSemilattice, distributiveLattice),
63 3
      join = Some(boundedSemilattice(A.joinSemilattice)),
64 3
      meet = Some(semilattice(A.meetSemilattice))
65
    ),
66

67 3
    """x\y ∧ y = 0""" -> forAll { (x: A, y: A) =>
68 3
      A.and(A.without(x, y), y) ?== A.zero },
69

70 3
    """x\y ∨ y = x ∨ y""" -> forAll { (x: A, y: A) =>
71 3
      A.or(A.without(x, y), y) ?== A.or(x, y) }
72
  )
73

74 3
  def bool(implicit A: Bool[A]) = new LogicProperties(
75 3
    name = "bool",
76 3
    parents = Seq(heyting, generalizedBool),
77 3
    ll = boundedDistributiveLattice,
78

79 3
    "excluded middle" -> forAll { (x: A) => A.or(x, A.complement(x)) ?== A.one }
80
  )
81

82
  class LogicProperties(
83
    val name: String,
84
    val parents: Seq[LogicProperties],
85
    val ll: LatticeProperties,
86
    val props: (String, Prop)*
87
  ) extends RuleSet {
88 3
    val bases = Seq("lattice" -> ll)
89
  }
90

91
}

Read our documentation on viewing source code .

Loading