documenation

pcp/pcp.hs

@@ -7,24 +7,29 @@ module Pcp where
 type LCBoolChurch = forall a . a -> a -> a
 newtype LCBool = LCBool { unBool :: LCBoolChurch }
 
-ite :: LCBool -> a -> a -> a
-ite = \c a b -> unBool c a b
-
 true :: LCBool
 true = LCBool $ \x y -> x
 
 false :: LCBool
 false = LCBool $ \x y -> y
 
+-- if then else
+ite :: LCBool -> a -> a -> a
+ite = \c a b -> unBool c a b
+
+-- returns always true
 at :: forall b. b -> LCBool
 at = \x -> true
 
+-- returns always false
 af :: forall b. b -> LCBool
 af = \x -> false
 
+-- logical and
 land :: LCBool -> LCBool -> LCBool
 land = \x y -> unBool x y false
 
+-- logical or
 lor :: LCBool -> LCBool -> LCBool
 lor = \x y -> unBool x true y
 
@@ -35,9 +40,11 @@ type LCPair a = (a -> a -> a) -> a
 pair :: a -> a -> LCPair a
 pair = \a -> \b -> \c -> c a b
 
+-- select first element in pair
 first :: LCPair a -> a
 first = \p -> p (\x -> \y -> x)
 
+-- select second element in pair
 second :: LCPair a -> a
 second = \p -> p (\x -> \y -> y)
 
@@ -46,50 +53,63 @@ 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
 
+-- check if a string is the empty string
 isempty :: LCStr -> LCBool
 isempty = \s -> unString s af af true
 
+-- concateation of two strings y, z
 conc :: LCStr -> LCStr -> LCStr
 conc = \y z -> LCStr $ \a b x -> unString y a b (unString z a b x)
 
+-- prepend an a to string s
 prepa :: LCStr -> LCStr
 prepa = \s -> LCStr $ \a b x -> a (unString s a b x)
 
+-- prepend a b to string s
 prepb :: LCStr -> LCStr
 prepb = \s -> LCStr $ \a b x -> b (unString s a b x)
 
-nexta :: LCPair LCStr -> LCPair LCStr
-nexta = \x -> pair (prepa (first x)) (first x)
-
-nextb :: LCPair LCStr -> LCPair LCStr
-nextb = \x -> pair (prepb (first x)) (first x)
-
+-- check if the string s starts with an a
 hd_a :: LCStr -> LCBool
 hd_a = \s -> unString s at af false
 
+-- check if the string s starts with a b
 hd_b :: LCStr -> LCBool
 hd_b = \s -> unString s af at false
 
+-- check if the inital character of the strings x, y are equal
 hd_eq :: LCStr -> LCStr -> LCBool
 hd_eq = \x y -> lor (land (hd_a x) (hd_a y)) (land (hd_b x) (hd_b y))
 
-hd :: LCStr -> LCStr
-hd = \s -> LCStr $ \a b x -> unString s (\y -> a x) (\y -> b x) x
+-- get a pair of strings (s1, s2) and return (a(s1), s1)
+nexta :: StrPair -> StrPair
+nexta = \x -> pair (prepa (first x)) (first x)
+
+-- get a pair of strings (s1, s2) and return (b(s1), s1)
+nextb :: StrPair -> StrPair
+nextb = \x -> pair (prepb (first x)) (first x)
 
+-- get the tail of a string
 tl :: LCStr -> LCStr
 tl = \s -> second (unString s nexta nextb (pair empty empty))
 
+-- check if two strings are equal
 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))))
 
+-- check if a string x is prefix of another string y
 prefix :: LCStr -> LCStr -> LCBool
-prefix = ycomb (\f x y -> ite (isempty x) true (land (hd_eq x y) (f (tl x) (tl y))))
+prefix = ycomb (\f x y ->
+  ite (isempty x) true
+  (land (hd_eq x y) (f (tl x) (tl y))))
 
 -- SOME STRINGS
 
@@ -129,6 +149,9 @@ baba = LCStr $ \a b x -> b (a (b (a x)))
 -- ycomb f = f (ycomb f)
 
 newtype Mu a = Mu (Mu a -> a)
+
+-- y combinator
+ycomb :: (b -> b) -> b
 ycomb f = (\h -> h $ Mu h) (\x -> f . (\(Mu g) -> g) x $ x)
 
 -- LISTS
@@ -136,53 +159,76 @@ ycomb f = (\h -> h $ Mu h) (\x -> f . (\(Mu g) -> g) x $ x)
 type LCListChurch b = forall a . (b -> a -> a) -> a -> a
 newtype LCList b = LCList { unList :: LCListChurch b }
 
+-- empty list
 nil :: LCList a
 nil = LCList $ \c -> \n -> n
 
+-- cons
 cons :: a -> LCList a -> LCList a
 cons = \h t -> LCList $ \c n -> c h (unList t c n)
 
+-- check if list is empty
 is_nil :: LCList a -> LCBool
 is_nil = \l -> unList l (\h t -> false) true
 
--- List Head - Idea to make it typable using unit from Types and Programming Languages by Pierce
+-- get head of a list
+-- Idea to make it typable using unit
+-- 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)) ()
 
+-- 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)
-next_l = \h p -> pair (cons h (first p)) (first p)
+next_l = \x p -> pair (cons x (first p)) (first p)
 
+-- get the tail of a list
 tl_l :: LCList a -> LCList a
 tl_l = \l -> second (unList l next_l (pair nil nil))
 
+-- append list y to list x
 append :: LCList a -> LCList a -> LCList a
 append = \x y -> LCList $ \c n -> unList x c (unList y c n)
 
 -- PCP Algorithm
-type StrPair = LCPair LCStr
+
 type ListStrPairs = LCList StrPair
 
+-- get a pair of strings (a s1, a s2) and return (s1, s2)
 simp :: StrPair -> StrPair
-simp = \p -> ycomb (\f x y -> ite (lor (isempty x) (isempty y)) (pair x y) (f (tl x) (tl y))) (first p) (second p)
+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 = \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 = ycomb (\f x -> ite (is_nil x) false (lor (eq (first (hd_l x)) (second (hd_l x))) (f (tl_l x))))
+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 = \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 = 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))))
+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 = ycomb (\f x y -> ite (is_nil x) nil (append (map_cmb (hd_l x) y) (f (tl_l x) y)))
+cross_cmb = ycomb (\f x y ->
+  ite (is_nil x) nil (append (map_cmb (hd_l x) y) (f (tl_l x) y)))
 
+-- combine pairs and check if any pair with equal strings is created, otherwise iterate
 pcp :: ListStrPairs -> 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 = \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
 
@@ -195,7 +241,7 @@ problem_2 = cons (pair a abbb) (cons (pair bb b) nil)
 problem_3 :: ListStrPairs -- undecidable
 problem_3 = cons (pair bba b) (cons (pair b ab) (cons (pair a bba) nil))
 
--- Output functions
+-- PARSE LC ENCODINGS TO STRINGS
 
 lcstr_tostr :: LCStr -> String
 lcstr_tostr = \s -> unString s (\a -> "a" ++ a) (\b -> "b" ++ b) ("")