pcp.hs 6.78 KB
Newer Older
1
2
3
4
{-# LANGUAGE RankNTypes #-}

module Pcp where

Frontull Samuel's avatar
Frontull Samuel committed
5
-- BOOLEANS
6

Frontull Samuel's avatar
Frontull Samuel committed
7
8
type LCBoolT = forall a . a -> a -> a
newtype LCBool = LCBool { unBool :: LCBoolT }
Frontull Samuel's avatar
Frontull Samuel committed
9

10
true :: LCBool
Frontull Samuel's avatar
Frontull Samuel committed
11
true = LCBool $ \x y -> x
12
13

false :: LCBool
Frontull Samuel's avatar
Frontull Samuel committed
14
false = LCBool $ \x y -> y
15

Frontull Samuel's avatar
Frontull Samuel committed
16
17
18
19
20
-- if then else
ite :: LCBool -> a -> a -> a
ite = \c a b -> unBool c a b

-- returns always true
21
22
23
at :: forall b. b -> LCBool
at = \x -> true

Frontull Samuel's avatar
Frontull Samuel committed
24
-- returns always false
25
26
27
af :: forall b. b -> LCBool
af = \x -> false

Frontull Samuel's avatar
Frontull Samuel committed
28
-- logical and
Frontull Samuel's avatar
Frontull Samuel committed
29
30
land :: LCBool -> LCBool -> LCBool
land = \x y -> unBool x y false
31

Frontull Samuel's avatar
Frontull Samuel committed
32
-- logical or
Frontull Samuel's avatar
Frontull Samuel committed
33
34
lor :: LCBool -> LCBool -> LCBool
lor = \x y -> unBool x true y
35

Frontull Samuel's avatar
Frontull Samuel committed
36
-- PAIRS
37

Frontull Samuel's avatar
Frontull Samuel committed
38
type LCPair a = (a -> a -> a) -> a
39

Frontull Samuel's avatar
Frontull Samuel committed
40
41
pair :: a -> a -> LCPair a
pair = \a -> \b -> \c -> c a b
42

Frontull Samuel's avatar
Frontull Samuel committed
43
-- select first element in pair
Frontull Samuel's avatar
Frontull Samuel committed
44
45
first :: LCPair a -> a
first = \p -> p (\x -> \y -> x)
46

Frontull Samuel's avatar
Frontull Samuel committed
47
-- select second element in pair
Frontull Samuel's avatar
Frontull Samuel committed
48
49
second :: LCPair a -> a
second = \p -> p (\x -> \y -> y)
50

Frontull Samuel's avatar
Frontull Samuel committed
51
-- STRINGS
52

53
type LCStrT = forall a . (a -> a) -> (a -> a) -> a -> a
Frontull Samuel's avatar
Frontull Samuel committed
54
newtype LCStr = LCStr { unString :: LCStrT }
55

Frontull Samuel's avatar
Frontull Samuel committed
56
empty :: LCStr
57
empty = LCStr $ \a b x -> x
58

Frontull Samuel's avatar
Frontull Samuel committed
59
-- check if a string is the empty string
60
isempty :: LCStr -> LCBool
61
isempty = \s -> unString s af af true
62

Frontull Samuel's avatar
Frontull Samuel committed
63
-- concateation of two strings y, z
64
conc :: LCStr -> LCStr -> LCStr
65
conc = \y z -> LCStr $ \a b x -> unString y a b (unString z a b x)
66

Frontull Samuel's avatar
Frontull Samuel committed
67
-- prepend an a to string s
68
prepa :: LCStr -> LCStr
69
prepa = \s -> LCStr $ \a b x -> a (unString s a b x)
70

Frontull Samuel's avatar
Frontull Samuel committed
71
-- prepend a b to string s
72
prepb :: LCStr -> LCStr
73
prepb = \s -> LCStr $ \a b x -> b (unString s a b x)
74

Frontull Samuel's avatar
Frontull Samuel committed
75
-- check if the string s starts with an a
76
hd_a :: LCStr -> LCBool
77
hd_a = \s -> unString s at af false
78

Frontull Samuel's avatar
Frontull Samuel committed
79
-- check if the string s starts with a b
80
hd_b :: LCStr -> LCBool
81
hd_b = \s -> unString s af at false
82

Frontull Samuel's avatar
Frontull Samuel committed
83
-- check if the inital character of the strings x, y are equal
84
85
86
hd_eq :: LCStr -> LCStr -> LCBool
hd_eq = \x y -> lor (land (hd_a x) (hd_a y)) (land (hd_b x) (hd_b y))

Frontull Samuel's avatar
Frontull Samuel committed
87
-- get a pair of strings (s1, s2) and return (a(s1), s1)
Frontull Samuel's avatar
Frontull Samuel committed
88
nexta :: LCPair LCStr -> LCPair LCStr
Frontull Samuel's avatar
Frontull Samuel committed
89
90
91
nexta = \x -> pair (prepa (first x)) (first x)

-- get a pair of strings (s1, s2) and return (b(s1), s1)
Frontull Samuel's avatar
Frontull Samuel committed
92
nextb :: LCPair LCStr -> LCPair LCStr
Frontull Samuel's avatar
Frontull Samuel committed
93
nextb = \x -> pair (prepb (first x)) (first x)
94

Frontull Samuel's avatar
Frontull Samuel committed
95
-- get the tail of a string
96
tl :: LCStr -> LCStr
97
tl = \s -> second (unString s nexta nextb (pair empty empty))
98

Frontull Samuel's avatar
Frontull Samuel committed
99
-- check if two strings are equal
100
101
102
103
104
105
eq :: LCStr -> LCStr -> LCBool
eq = ycomb (\f x y ->
  ite (lor (isempty x) (isempty y))
  (land (isempty x) (isempty y))
  (land (hd_eq x y) (f (tl x) (tl y))))

Frontull Samuel's avatar
Frontull Samuel committed
106
-- check if a string x is prefix of another string y
107
prefix :: LCStr -> LCStr -> LCBool
Frontull Samuel's avatar
Frontull Samuel committed
108
109
110
prefix = ycomb (\f x y ->
  ite (isempty x) true
  (land (hd_eq x y) (f (tl x) (tl y))))
111

Frontull Samuel's avatar
Frontull Samuel committed
112
113
114
-- SOME STRINGS

a :: LCStr
115
a = LCStr $ \a b x -> a x
Frontull Samuel's avatar
Frontull Samuel committed
116
117

b :: LCStr
118
b = LCStr $ \a b x -> b x
Frontull Samuel's avatar
Frontull Samuel committed
119
120

ab :: LCStr
121
ab = LCStr $ \a b x -> a (b x)
Frontull Samuel's avatar
Frontull Samuel committed
122
123

ba :: LCStr
124
ba = LCStr $ \a b x -> b (a x)
Frontull Samuel's avatar
Frontull Samuel committed
125
126

bb :: LCStr
127
bb = LCStr $ \a b x -> b (b x)
Frontull Samuel's avatar
Frontull Samuel committed
128

129
130
131
baa :: LCStr
baa = LCStr $ \a b x -> b (a (a x))

Frontull Samuel's avatar
Frontull Samuel committed
132
bba :: LCStr
133
bba = LCStr $ \a b x -> b (b (a x))
Frontull Samuel's avatar
Frontull Samuel committed
134
135

abb :: LCStr
136
abb = LCStr $ \a b x -> a (b (b x))
Frontull Samuel's avatar
Frontull Samuel committed
137
138

abba :: LCStr
139
abba = LCStr $ \a b x -> a (b (b (a x)))
Frontull Samuel's avatar
Frontull Samuel committed
140
141

abbb :: LCStr
142
abbb = LCStr $ \a b x -> a (b (b (b x)))
Frontull Samuel's avatar
Frontull Samuel committed
143
144

baba :: LCStr
145
baba = LCStr $ \a b x -> b (a (b (a x)))
Frontull Samuel's avatar
Frontull Samuel committed
146
147
148
149
150
151
152

-- RECURSION

-- ycomb :: (t -> t) -> t
-- ycomb f = f (ycomb f)

newtype Mu a = Mu (Mu a -> a)
Frontull Samuel's avatar
Frontull Samuel committed
153
154
155

-- y combinator
ycomb :: (b -> b) -> b
Frontull Samuel's avatar
Frontull Samuel committed
156
157
ycomb f = (\h -> h $ Mu h) (\x -> f . (\(Mu g) -> g) x $ x)

Frontull Samuel's avatar
Frontull Samuel committed
158

159
-- LISTS
Frontull Samuel's avatar
Frontull Samuel committed
160

Frontull Samuel's avatar
Frontull Samuel committed
161
162
type LCListT b = forall a . (b -> a -> a) -> a -> a
newtype LCList b = LCList { unList :: LCListT b }
163

Frontull Samuel's avatar
Frontull Samuel committed
164
-- empty list
165
166
167
nil :: LCList a
nil = LCList $ \c -> \n -> n

Frontull Samuel's avatar
Frontull Samuel committed
168
-- cons
169
170
171
cons :: a -> LCList a -> LCList a
cons = \h t -> LCList $ \c n -> c h (unList t c n)

Frontull Samuel's avatar
Frontull Samuel committed
172
-- check if list is empty
173
174
175
is_nil :: LCList a -> LCBool
is_nil = \l -> unList l (\h t -> false) true

Frontull Samuel's avatar
Frontull Samuel committed
176
177
178
-- get head of a list
-- Idea to make it typable using unit
-- from Types and Programming Languages by Pierce
Frontull Samuel's avatar
Frontull Samuel committed
179
180
hd_l :: (LCList a) -> a
diverge = \u -> ycomb (\x -> x)
Frontull Samuel's avatar
Frontull Samuel committed
181
hd_l = \l -> (unList l (\h t u -> h) diverge) ()
182

Frontull Samuel's avatar
Frontull Samuel committed
183
-- get a list element x and a pair of lists (l1, l2) and return (x :: l1, l1)
Frontull Samuel's avatar
Frontull Samuel committed
184
next_l :: a -> LCPair (LCList a) -> LCPair (LCList a)
Frontull Samuel's avatar
Frontull Samuel committed
185
next_l = \x p -> pair (cons x (first p)) (first p)
186

Frontull Samuel's avatar
Frontull Samuel committed
187
-- get the tail of a list
188
189
190
tl_l :: LCList a -> LCList a
tl_l = \l -> second (unList l next_l (pair nil nil))

Frontull Samuel's avatar
Frontull Samuel committed
191
-- append list y to list x
Frontull Samuel's avatar
Frontull Samuel committed
192
193
194
append :: LCList a -> LCList a -> LCList a
append = \x y -> LCList $ \c n -> unList x c (unList y c n)

Frontull Samuel's avatar
Frontull Samuel committed
195
-- PCP Algorithm
Frontull Samuel's avatar
Frontull Samuel committed
196
197

-- get a pair of strings (a s1, a s2) and return (s1, s2)
Frontull Samuel's avatar
Frontull Samuel committed
198
simp :: LCPair LCStr -> LCPair LCStr
Frontull Samuel's avatar
Frontull Samuel committed
199
200
201
simp = \p -> ycomb (\f x y ->
  ite (lor (isempty x) (isempty y)) (pair x y)
  (f (tl x) (tl y))) (first p) (second p)
Frontull Samuel's avatar
Frontull Samuel committed
202

Frontull Samuel's avatar
Frontull Samuel committed
203
-- check if pair of strings is valid (at least one string prefix of the other)
Frontull Samuel's avatar
Frontull Samuel committed
204
pvalid :: LCPair LCStr -> LCBool
Frontull Samuel's avatar
Frontull Samuel committed
205
206
pvalid = \p -> lor (prefix (first p) (second p)) (prefix (second p) (first p))

Frontull Samuel's avatar
Frontull Samuel committed
207
-- check if there is a pair of two equal strings in a list of pair of strings
Frontull Samuel's avatar
Frontull Samuel committed
208
find_eq :: LCList (LCPair LCStr) -> LCBool
Frontull Samuel's avatar
Frontull Samuel committed
209
210
find_eq = ycomb (\f x ->
  ite (is_nil x) false (lor (eq (first (hd_l x)) (second (hd_l x))) (f (tl_l x))))
Frontull Samuel's avatar
Frontull Samuel committed
211

Frontull Samuel's avatar
Frontull Samuel committed
212
-- combine two pairs of strings (a1, a2), (b1, b2) to (a1 b1, a2 b2)
Frontull Samuel's avatar
Frontull Samuel committed
213
cmb :: LCPair LCStr -> LCPair LCStr -> LCPair LCStr
Frontull Samuel's avatar
Frontull Samuel committed
214
215
cmb = \p s -> pair (conc (first p) (first s)) (conc (second p) (second s))

Frontull Samuel's avatar
Frontull Samuel committed
216
-- combine a pair x with every pair in a list of pairs y
Frontull Samuel's avatar
Frontull Samuel committed
217
map_cmb :: LCPair LCStr -> LCList (LCPair LCStr) -> LCList (LCPair LCStr)
Frontull Samuel's avatar
Frontull Samuel committed
218
219
220
221
map_cmb = ycomb (\f x y ->
  ite (is_nil y) nil
    (ite (pvalid (cmb x (hd_l y))) (cons (simp (cmb x (hd_l y))) (f x (tl_l y)))
    (f x (tl_l y))))
Frontull Samuel's avatar
Frontull Samuel committed
222

Frontull Samuel's avatar
Frontull Samuel committed
223
-- combine two lists of pairs x,y with each other
Frontull Samuel's avatar
Frontull Samuel committed
224
cross_cmb :: LCList (LCPair LCStr) -> LCList (LCPair LCStr) -> LCList (LCPair LCStr)
Frontull Samuel's avatar
Frontull Samuel committed
225
226
cross_cmb = ycomb (\f x y ->
  ite (is_nil x) nil (append (map_cmb (hd_l x) y) (f (tl_l x) y)))
Frontull Samuel's avatar
Frontull Samuel committed
227

Frontull Samuel's avatar
Frontull Samuel committed
228
229
230
-- combine lists of pairs of strings
-- and check if any pair with equal strings is created
-- if yes return true otherwise reiterate
Frontull Samuel's avatar
Frontull Samuel committed
231
pcp :: LCList (LCPair LCStr) -> LCBool
Frontull Samuel's avatar
Frontull Samuel committed
232
233
pcp = \x -> ycomb (\f x y ->
  ite (is_nil x) false (ite (find_eq x) true (f (cross_cmb x y) y))) x x
234

235
236
-- PCP Problems

Frontull Samuel's avatar
Frontull Samuel committed
237
-- [(a, ab), (bb, b)]
Frontull Samuel's avatar
Frontull Samuel committed
238
problem_1 :: LCList (LCPair LCStr)
239
240
problem_1 = cons (pair a ab) (cons (pair bb b) nil)

Frontull Samuel's avatar
Frontull Samuel committed
241
-- [(a, abbb), (bb, b)]
Frontull Samuel's avatar
Frontull Samuel committed
242
problem_2 :: LCList (LCPair LCStr)
243
244
problem_2 = cons (pair a abbb) (cons (pair bb b) nil)

Frontull Samuel's avatar
Frontull Samuel committed
245
-- [(bba, b), (b, ab), (a, bba)]
Frontull Samuel's avatar
Frontull Samuel committed
246
problem_3 :: LCList (LCPair LCStr) -- undecidable
247
248
problem_3 = cons (pair bba b) (cons (pair b ab) (cons (pair a bba) nil))

249
-- [(ab, a), (ab, bba), (a, baa), (baa, ba)]
Frontull Samuel's avatar
Frontull Samuel committed
250
problem_4 :: LCList (LCPair LCStr) -- has a solution of length 76
Frontull Samuel's avatar
Frontull Samuel committed
251
problem_4 = cons (pair ab a) (cons (pair ab bba) (cons (pair a baa) (cons (pair baa ba) nil)))
252

Frontull Samuel's avatar
Frontull Samuel committed
253
-- PARSE LC ENCODINGS TO STRINGS
Frontull Samuel's avatar
Frontull Samuel committed
254

Frontull Samuel's avatar
Frontull Samuel committed
255
-- string encoding to String
Frontull Samuel's avatar
Frontull Samuel committed
256
lcstr_tostr :: LCStr -> String
257
lcstr_tostr = \s -> unString s (\a -> "a" ++ a) (\b -> "b" ++ b) ("")
Frontull Samuel's avatar
Frontull Samuel committed
258

Frontull Samuel's avatar
Frontull Samuel committed
259
-- bool encoding to String
Frontull Samuel's avatar
Frontull Samuel committed
260
261
262
lcbool_tostr :: LCBool -> String
lcbool_tostr = \b -> ite b "True" "False"

263
-- lcbool_tostr (pcp problem_1)