linear-logic/RewriteRules.hs at master · andykitchen/linear-logic · GitHub

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
module RewriteRules (simplify, dedual, unexpt,
  prop_simplify_idempotent,
  prop_dedual_onlyNegativeAtoms,
  prop_unexpt_inExponentialLattice1,
  prop_unexpt_inExponentialLattice2)
where

import Test.QuickCheck
import Arbitrary

import Syntax
import Parser

import Rewrite

l --@ r = (tt l, tt r)

dedual_rules = [
    "a^^"      --@ "a",
    "(a * b)^" --@ "a^ $ b^",
    "(a $ b)^" --@ "a^ * b^",
    "(a & b)^" --@ "a^ + b^",
    "(a + b)^" --@ "a^ & b^",

    "(a -@ b)^" --@ "a * b^",

    "(!a)^" --@ "?(a^)",
    "(?a)^" --@ "!(a^)",

    "1^" --@ "%",
    "0^" --@ "#",
    "#^" --@ "0",
    "%^" --@ "1"
  ]

unexpt_rules = [
    "!!a" --@ "!a",
    "??a" --@ "?a",

    "!?!?a" --@ "!?a",
    "?!?!a" --@ "?!a",

    "!?1" --@ "1",
    "?!%" --@ "%"
  ]

unit_rules = [
    "!#" --@ "1",
    "?0" --@ "%",

    "a * 1" --@ "a",
    "a $ %" --@ "a",
    "a + 0" --@ "a",
    "a & #" --@ "a",

    "a * 0" --@ "0",
    "a $ #" --@ "#"
  ]

distrib_rules = [
    "a * (b + c)" --@ "(a * b) + (a * c)",
    "a $ (b & c)" --@ "(a $ b) & (a $ c)",

    "a * (b & c)" --@ "(a * b) & (a * c)",
    "a $ (b + c)" --@ "(a $ b) + (a $ c)"
  ]

unexpt_aux_rules = [
    "!(a & b)" --@ "!a * !b",
    "?(a + b)" --@ "?a $ ?b"
  ]

dedual :: Term -> Term
dedual = rewrite' dedual_rules

unexpt :: Term -> Term
unexpt = rewrite' unexpt_rules

simplify :: Term -> Term
simplify = rewrite' $ concat [dedual_rules, unexpt_rules, unit_rules]

reduce :: Term -> Term
reduce = rewrite' $ concat [distrib_rules, unexpt_aux_rules]

-- Second order idempotence predicate
prop_idempotent :: Eq a => (a -> a) -> a -> Bool
prop_idempotent f x  =  f (f x) == f x


prop_simplify_idempotent :: Term -> Bool
prop_dedual_idempotent   :: Term -> Bool
prop_unexpt_idempotent   :: Term -> Bool

prop_simplify_idempotent  =  prop_idempotent simplify
prop_dedual_idempotent    =  prop_idempotent dedual
prop_unexpt_idempotent    =  prop_idempotent unexpt

prop_dedual_onlyNegativeAtoms :: Term -> Bool
prop_dedual_onlyNegativeAtoms x  =  check (dedual x)
  where check (Not (Atom _)) = True
        check (Not _)    = False
        check (l :*:  r) = check l && check r
        check (l :$:  r) = check l && check r
        check (l :-@: r) = check l && check r
        check (l :&:  r) = check l && check r
        check (l :+:  r) = check l && check r
        check (OfCourse a) = check a
        check (WhyNot a)   = check a
        check _ = True

prop_unexpt_inExponentialLattice1 :: Term -> Bool
prop_unexpt_inExponentialLattice2 :: Term -> Property

prop_unexpt_inExponentialLattice1 x  =  lattice (unexpt x)

-- This is a weakened version of the prop above,
-- that makes counter examples easier to find for quickCheck
prop_unexpt_inExponentialLattice2 x  =
  forAllShrink exponentOnlyTerm shrink $ \t -> lattice (unexpt t)

lattice :: Term -> Bool

lattice (OfCourse (WhyNot (OfCourse a))) = latticeNoExp a
lattice (WhyNot   (OfCourse (WhyNot a))) = latticeNoExp a
lattice (OfCourse (WhyNot a))   = latticeNoExp a
lattice (WhyNot   (OfCourse a)) = latticeNoExp a
lattice (OfCourse a) = latticeNoExp a
lattice (WhyNot   a) = latticeNoExp a
lattice (l :*:  r) = lattice l && lattice r
lattice (l :$:  r) = lattice l && lattice r
lattice (l :-@: r) = lattice l && lattice r
lattice (l :&:  r) = lattice l && lattice r
lattice (l :+:  r) = lattice l && lattice r
lattice (Not a)    = lattice a
lattice _ = True

latticeNoExp (OfCourse _) = False
latticeNoExp (WhyNot   _) = False
latticeNoExp t = lattice t

(--@) :: String -> String -> (Term, Term)
dedual_rules :: [Rule]
unexpt_rules :: [Rule]