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
|
module Logic where
data Prop =
Pred Ident [Exp]
| And Prop Prop
| Or Prop Prop
| If Prop Prop
| Not Prop
| All Prop
| Exist Prop
deriving Show
data Exp =
App Ident [Exp]
| Var Int -- de Bruijn index
deriving Show
type Ident = String
data Model a = Model {
app :: Ident -> [a] -> a,
prd :: Ident -> [a] -> Bool,
dom :: [a]
}
type Assignment a = [a]
update :: a -> Assignment a -> Assignment a
update x assign = x : assign
look :: Int -> Assignment a -> a
look i assign = assign !! i
valExp :: Model a -> Assignment a -> Exp -> a
valExp model assign exp = case exp of
App f xs -> app model f (map (valExp model assign) xs)
Var i -> look i assign
valProp :: Model a -> Assignment a -> Prop -> Bool
valProp model assign prop = case prop of
Pred f xs -> prd model f (map (valExp model assign) xs)
And a b -> v a && v b
Or a b -> v a || v b
If a b -> if v a then v b else True
Not a -> not (v a)
All p -> all (\x -> valProp model (update x assign) p) (dom model)
Exist p -> any (\x -> valProp model (update x assign) p) (dom model)
where
v = valProp model assign
liftProp :: Int -> Prop -> Prop
liftProp i p = case p of
Pred f xs -> Pred f (map liftExp xs)
And a b -> And (lift a) (lift b)
Or a b -> Or (lift a) (lift b)
If a b -> If (lift a) (lift b)
Not a -> Not (lift a)
All p -> All (liftProp (i+1) p)
Exist p -> Exist (liftProp (i+1) p)
where
lift = liftProp i
liftExp e = case e of
App f xs -> App f (map liftExp xs)
Var j -> Var (j + i)
_ -> e
-- example: initial segments of integers
intModel :: Int -> Model Int
intModel mx = Model {
app = \f xs -> case (f,xs) of
("+",_) -> sum xs
(_,[]) -> read f,
prd = \f xs -> case (f,xs) of
("E",[x]) -> even x
("<",[x,y]) -> x < y
("=",[x,y]) -> x == y
_ -> error "undefined val",
dom = [0 .. mx]
}
exModel = intModel 100
ev x = Pred "E" [x]
lt x y = Pred "<" [x,y]
eq x y = Pred "=" [x,y]
int i = App (show i) []
ex1 :: Prop
ex1 = Exist (ev (Var 0))
ex2 :: Prop
ex2 = All (Exist (lt (Var 1) (Var 0)))
ex3 :: Prop
ex3 = All (If (lt (Var 0) (int 100)) (Exist (lt (Var 1) (Var 0))))
ex4 :: Prop
ex4 = All (All (If (lt (Var 1) (Var 0)) (Not (lt (Var 0) (Var 1)))))
|
