removed type abberaviations

pcp/pcp.hs

@@ -53,8 +53,6 @@ second = \p -> p (\x -> \y -> y)
 type LCStrT = forall a . (a -> a) -> (a -> a) -> a -> a
 newtype LCStr = LCStr { unString :: LCStrT }
 
-type StrPair = LCPair LCStr
-
 empty :: LCStr
 empty = LCStr $ \a b x -> x
 
@@ -87,11 +85,11 @@ hd_eq :: LCStr -> LCStr -> LCBool
 hd_eq = \x y -> lor (land (hd_a x) (hd_a y)) (land (hd_b x) (hd_b y))
 
 -- get a pair of strings (s1, s2) and return (a(s1), s1)
-nexta :: StrPair -> StrPair
+nexta :: LCPair LCStr -> LCPair LCStr
 nexta = \x -> pair (prepa (first x)) (first x)
 
 -- get a pair of strings (s1, s2) and return (b(s1), s1)
-nextb :: StrPair -> StrPair
+nextb :: LCPair LCStr -> LCPair LCStr
 nextb = \x -> pair (prepb (first x)) (first x)
 
 -- get the tail of a string
@@ -180,7 +178,7 @@ is_nil = \l -> unList l (\h t -> false) true
 -- from Types and Programming Languages by Pierce
 hd_l :: (LCList a) -> a
 diverge = \u -> ycomb (\x -> x)
-hd_l = \l -> (unList l (\h t u -> h) (diverge)) ()
+hd_l = \l -> (unList l (\h t u -> h) diverge) ()
 
 -- get a list element x and a pair of lists (l1, l2) and return (x :: l1, l1)
 next_l :: a -> LCPair (LCList a) -> LCPair (LCList a)
@@ -196,62 +194,60 @@ append = \x y -> LCList $ \c n -> unList x c (unList y c n)
 
 -- PCP Algorithm
 
-type ListStrPairs = LCList StrPair
-
 -- get a pair of strings (a s1, a s2) and return (s1, s2)
-simp :: StrPair -> StrPair
+simp :: LCPair LCStr -> LCPair LCStr
 simp = \p -> ycomb (\f x y ->
   ite (lor (isempty x) (isempty y)) (pair x y)
   (f (tl x) (tl y))) (first p) (second p)
 
 -- check if pair of strings is valid (at least one string prefix of the other)
-pvalid :: StrPair -> LCBool
+pvalid :: LCPair LCStr -> LCBool
 pvalid = \p -> lor (prefix (first p) (second p)) (prefix (second p) (first p))
 
 -- check if there is a pair of two equal strings in a list of pair of strings
-find_eq :: ListStrPairs -> LCBool
+find_eq :: LCList (LCPair LCStr) -> LCBool
 find_eq = ycomb (\f x ->
   ite (is_nil x) false (lor (eq (first (hd_l x)) (second (hd_l x))) (f (tl_l x))))
 
 -- combine two pairs of strings (a1, a2), (b1, b2) to (a1 b1, a2 b2)
-cmb :: StrPair -> StrPair -> StrPair
+cmb :: LCPair LCStr -> LCPair LCStr -> LCPair LCStr
 cmb = \p s -> pair (conc (first p) (first s)) (conc (second p) (second s))
 
 -- combine a pair x with every pair in a list of pairs y
-map_cmb :: StrPair -> ListStrPairs -> ListStrPairs
+map_cmb :: LCPair LCStr -> LCList (LCPair LCStr) -> LCList (LCPair LCStr)
 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))))
 
 -- combine two lists of pairs x,y with each other
-cross_cmb :: ListStrPairs -> ListStrPairs -> ListStrPairs
+cross_cmb :: LCList (LCPair LCStr) -> LCList (LCPair LCStr) -> LCList (LCPair LCStr)
 cross_cmb = ycomb (\f x y ->
   ite (is_nil x) nil (append (map_cmb (hd_l x) y) (f (tl_l x) y)))
 
 -- combine lists of pairs of strings
 -- and check if any pair with equal strings is created
 -- if yes return true otherwise reiterate
-pcp :: ListStrPairs -> LCBool
+pcp :: LCList (LCPair LCStr) -> LCBool
 pcp = \x -> ycomb (\f x y ->
   ite (is_nil x) false (ite (find_eq x) true (f (cross_cmb x y) y))) x x
 
 -- PCP Problems
 
 -- [(a, ab), (bb, b)]
-problem_1 :: ListStrPairs
+problem_1 :: LCList (LCPair LCStr)
 problem_1 = cons (pair a ab) (cons (pair bb b) nil)
 
 -- [(a, abbb), (bb, b)]
-problem_2 :: ListStrPairs
+problem_2 :: LCList (LCPair LCStr)
 problem_2 = cons (pair a abbb) (cons (pair bb b) nil)
 
 -- [(bba, b), (b, ab), (a, bba)]
-problem_3 :: ListStrPairs -- undecidable
+problem_3 :: LCList (LCPair LCStr) -- undecidable
 problem_3 = cons (pair bba b) (cons (pair b ab) (cons (pair a bba) nil))
 
 -- [(ab, a), (ab, bba), (a, baa), (baa, ba)]
-problem_4 :: ListStrPairs -- has a solution of length 76
+problem_4 :: LCList (LCPair LCStr) -- has a solution of length 76
 problem_4 = cons (pair ab a) (cons (pair ab bba) (cons (pair a baa) (cons (pair baa ba) nil)))
 
 -- PARSE LC ENCODINGS TO STRINGS