pcp comments

pcp/lambda.hs

@@ -91,11 +91,11 @@ instance Show Term where
     showsPrec (app_prec + 1) u
     where
       app_prec = 5
-  showsPrec d (Abs x t) = showParen (d > abs_prec) $ showString "\\" . showsAbs x t
+  showsPrec d (Abs x t) = showParen (d > abs_prec) $ showString "/" . showsAbs x t
     where
       abs_prec = 4
       showsAbs x (Abs y t) = showString x . showString " " . showsAbs y t
-      showsAbs x t = showString x . showString ". " . showsPrec abs_prec t
+      showsAbs x t = showString x . showString "." . showsPrec abs_prec t
   showsPrec d S = showString "S"
   showsPrec d K = showString "K"
   showsPrec d I = showString "I"
@@ -122,7 +122,8 @@ isChurchNum t = churchNum t /= Nothing
 
 betastep :: Term -> Term
 betastep (Var x) = Var x
-betastep (Abs x t) = Abs x (betastep t)
+-- betastep (Abs x t) = Abs x (betastep t)
+betastep (Abs x t) = Abs x t
 betastep (App (Abs x e1) e2) = subst x e2 e1
 betastep (App I e1) = e1
 betastep (App (App K e1) e2) = e1
@@ -155,9 +156,9 @@ ttran (Abs x (Var y)) =
     if x == y then I
     else App K (Var y)
 -- translate \xy.x to K not to S (K K) I
-ttran (Abs x (Abs y (Var z))) =
-    if x == z then K else
-    App K (ttran (Abs y (Var z)))
+-- ttran (Abs x (Abs y (Var z))) =
+--     if x == z then K else
+--     App K (ttran (Abs y (Var z)))
 ttran (Abs x (Abs y e1)) =
     let f = elem x (fvs e1) in
     if f then ttran (Abs x (ttran (Abs y e1)))
@@ -176,8 +177,12 @@ true = Abs "x" (Abs "y" (Var "x"))
 false :: Term
 false = Abs "x" (Abs "y" (Var "y"))
 
-at = Abs "x" true
-af = Abs "x" false
+i = Abs "x" (Var "x")
+k = Abs "x" (Abs "y" (Var "x"))
+s = Abs "x" (Abs "y" (Abs "z" (App (App (Var "x") (Var "z")) (App (Var "y") (Var "z")))))
+
+at = Abs "z" true
+af = Abs "z" false
 
 ite = Abs "c" (Abs "a" (Abs "b" (App (App (Var "c") (Var "a")) (Var "b"))))
 
@@ -209,8 +214,8 @@ hd_a = Abs "s" (App (App (App (Var "s") at) af) false)
 hd_b = Abs "s" (App (App (App (Var "s") af) at) false)
 hd_eq = Abs "x" (Abs "y" (App (App lor (App (App land (App hd_a (Var "x"))) (App hd_a (Var "y")))) (App (App land (App hd_b (Var "x"))) (App hd_b (Var "y")))))
 
-next_a = Abs "x" (App (App pair (App prep_a (App first (Var "x")))) (App first (Var "x")))
-next_b = Abs "x" (App (App pair (App prep_b (App first (Var "x")))) (App first (Var "x")))
+next_a = Abs "k" (App (App pair (App prep_a (App first (Var "k")))) (App first (Var "k")))
+next_b = Abs "k" (App (App pair (App prep_b (App first (Var "k")))) (App first (Var "k")))
 
 tl_str = Abs "s" (App second (App (App (App (Var "s") next_a) next_b) (App (App pair empty) empty)))
 
@@ -230,6 +235,21 @@ tl_l = Abs "l" (App second (App (App (Var "l") next_l) (App (App pair nil) nil))
 
 append = Abs "x" (Abs "y" (Abs "c" (Abs "n" (App (App (Var "x") (Var "c")) (App (App (Var "y") (Var "c")) (Var "n"))))))
 
+simp = Abs "p" (App (App (App ycomb (Abs "f" (Abs "x" (Abs "y" (App  (App (App ite (App (App lor (App isempty (Var "x"))) (App isempty (Var "y")))) (App (App pair (Var "x")) (Var "y"))) (App (App (Var "f") (App tl_str (Var "x"))) (App tl_str (Var "y")))))))) (App first (Var "p"))) (App second (Var "p")))
+
+pvalid = Abs "p" (App (App lor (App (App prefix (App first (Var "p"))) (App second (Var "p")))) (App (App prefix (App second (Var "p"))) (App first (Var "p"))))
+
+find_eq = App ycomb (Abs "f" (Abs "x" (App (App (App ite (App is_nil (Var "x"))) false) (App (App lor (App (App eq (App first (App hd_l (Var "x")))) (App second (App hd_l (Var "x"))))) (App (Var "f") (App tl_l (Var "y")))))))
+
+cmb = Abs "p" (Abs "q" (App (App pair (App (App conc (App second (Var "p"))) (App second (Var "q")))) (App (App conc (App second (Var "p"))) (App second (Var "q")))))
+
+map_cmb = App ycomb (Abs "f" (Abs "x" (Abs "y" ( App (App (App ite (App is_nil (Var "y"))) false) ( App (App (App ite (App pvalid (App (App cmb (Var "x")) (App hd_l (Var "y"))))) (App (App cons (App simp (App (App cmb (Var "x")) (App hd_l (Var "x"))))) (App (App (Var "f") (Var "x")) (App tl_l (Var "y"))))) (App (App (Var "f") (Var "x")) (App tl_l (Var "y"))) ) ))))
+
+cross_cmb = App ycomb (Abs "f" (Abs "x" (Abs "y" (App (App (App ite (App is_nil (Var "y"))) nil) (App (App append (App (App map_cmb (App hd_l (Var "x"))) (Var "y"))) (App (App (Var "f") (App tl_l (Var "x"))) (Var "y")))))))
+
+pcp = Abs "x" (App (App (App ycomb (Abs "f" (Abs "x" (Abs "y" (App (App (App ite (App is_nil (Var "x"))) false) (App (App (App ite (App find_eq (Var "x"))) true) (App (App (Var "f") (App (App cross_cmb (Var "x")) (Var "y"))) (Var "y")))))))) (Var "x")) (Var "x"))
+
+
 p1 = App (App pair bba) b
 p2 = App (App pair b) ab
 p3 = App (App pair a) bba
@@ -240,16 +260,25 @@ p22 = App (App pair b) bb
 p32 = App (App pair a) b
 pairs2 = App (App cons p12) (App (App cons p22) (App (App cons p32) nil))
 
-simp = Abs "p" (App (App (App ycomb (Abs "f" (Abs "x" (Abs "y" (App  (App (App ite (App (App lor (App isempty (Var "x"))) (App isempty (Var "y")))) (App (App pair (Var "x")) (Var "y"))) (App (App (Var "f") (App tl_str (Var "x"))) (App tl_str (Var "y")))))))) (App first (Var "p"))) (App second (Var "p")))
+p13 = App (App pair a) a
+p23 = App (App pair b) bb
+pairs3 = App (App cons p13) (App (App cons p23) nil)
 
-pvalid = Abs "p" (App (App lor (App (App prefix (App first (Var "p"))) (App second (Var "p")))) (App (App prefix (App second (Var "p"))) (App first (Var "p"))))
+p14 = App (App pair a) a
+p24 = App (App pair b) b
+pairs4 = App (App cons p14) (App (App cons p24) nil)
 
-find_eq = App ycomb (Abs "f" (Abs "x" (App (App (App ite (App is_nil (Var "x"))) false) (App (App lor (App (App eq (App first (App hd_l (Var "x")))) (App second (App hd_l (Var "x"))))) (App (Var "f") (App tl_l (Var "y")))))))
+-- FIBONACCI
+zero = Abs "x" (Abs "y" (Var "y"))
+one  = Abs "x" (Abs "y" (App (Var "x") (Var "y")))
+two  = Abs "x" (Abs "y" (App (Var "x") (App (Var "x") (Var "y"))))
 
-cmb = Abs "p" (Abs "q" (App (App pair (App (App conc (App second (Var "p"))) (App second (Var "q")))) (App (App conc (App second (Var "p"))) (App second (Var "q")))))
+suc = Abs "n" (Abs "x" (Abs "y" (App (Var "x") (App (App (Var "n") (Var "x")) (Var "y")))))
+ad = Abs "n" (Abs "m" (Abs "x" (Abs "y" (App (App (Var "n") (Var "x")) (App (App (Var "m") (Var "x")) (Var "y"))))))
+mul = Abs "n" (Abs "m" (Abs "x" (App (Var "n") (App (Var "m") (Var "x")))))
 
-map_cmb = App ycomb (Abs "f" (Abs "x" (Abs "y" ( App (App (App ite (App is_nil (Var "y"))) false) ( App (App (App ite (App pvalid (App (App cmb (Var "x")) (App hd_l (Var "y"))))) (App (App cons (App simp (App (App cmb (Var "x")) (App hd_l (Var "x"))))) (App (App (Var "f") (Var "x")) (App tl_l (Var "y"))))) (App (App (Var "f") (Var "x")) (App tl_l (Var "y"))) ) ))))
+next1 = Abs "p" (App (App pair (App (App mul (App (Var "p") first)) (App suc (App (Var "p") second)))) (App suc (App (Var "p") second)))
 
-cross_cmb = App ycomb (Abs "f" (Abs "x" (Abs "y" (App (App (App ite (App is_nil (Var "y"))) nil) (App (App append (App (App map_cmb (App hd_l (Var "x"))) (Var "y"))) (App (App (Var "f") (App tl_l (Var "x"))) (Var "y")))))))
+factprim = Abs "n" (App (App (App (Var "n") next1) (App (App pair one) zero)) first)
 
-pcp = Abs "x" (App (App (App ycomb (Abs "f" (Abs "x" (Abs "y" (App (App (App ite (App is_nil (Var "x"))) false) (App (App (App ite (App find_eq (Var "x"))) true) (App (App (Var "f") (App (App cross_cmb (Var "x")) (Var "y"))) (Var "y")))))))) (Var "x")) (Var "x"))
+ex1 = App (App (App factprim (App (App ad two) two)) i) i

pcp/pcp.hs

@@ -17,13 +17,13 @@ false = LCBool $ \x y -> y
 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 constant true
+ct :: forall b. b -> LCBool
+ct = \x -> true
 
--- returns always false
-af :: forall b. b -> LCBool
-af = \x -> false
+-- returns constant false
+cf :: forall b. b -> LCBool
+cf = \x -> false
 
 -- logical and
 land :: LCBool -> LCBool -> LCBool
@@ -58,7 +58,7 @@ empty = LCStr $ \a b x -> x
 
 -- check if a string is the empty string
 isempty :: LCStr -> LCBool
-isempty = \s -> unString s af af true
+isempty = \s -> unString s cf cf true
 
 -- concateation of two strings y, z
 conc :: LCStr -> LCStr -> LCStr
@@ -74,11 +74,11 @@ prepb = \s -> LCStr $ \a b x -> b (unString s a b x)
 
 -- check if the string s starts with an a
 hd_a :: LCStr -> LCBool
-hd_a = \s -> unString s at af false
+hd_a = \s -> unString s ct cf false
 
 -- check if the string s starts with a b
 hd_b :: LCStr -> LCBool
-hd_b = \s -> unString s af at false
+hd_b = \s -> unString s cf ct false
 
 -- check if the inital character of the strings x, y are equal
 hd_eq :: LCStr -> LCStr -> LCBool
@@ -117,6 +117,9 @@ a = LCStr $ \a b x -> a x
 b :: LCStr
 b = LCStr $ \a b x -> b x
 
+aa :: LCStr
+aa = LCStr $ \a b x -> a (a x)
+
 ab :: LCStr
 ab = LCStr $ \a b x -> a (b x)
 
@@ -132,18 +135,9 @@ baa = LCStr $ \a b x -> b (a (a x))
 bba :: LCStr
 bba = LCStr $ \a b x -> b (b (a x))
 
-abb :: LCStr
-abb = LCStr $ \a b x -> a (b (b x))
-
-abba :: LCStr
-abba = LCStr $ \a b x -> a (b (b (a x)))
-
 abbb :: LCStr
 abbb = LCStr $ \a b x -> a (b (b (b x)))
 
-baba :: LCStr
-baba = LCStr $ \a b x -> b (a (b (a x)))
-
 -- RECURSION
 
 -- ycomb :: (t -> t) -> t
@@ -158,38 +152,36 @@ ycomb f = (\h -> h $ Mu h) (\x -> f . (\(Mu g) -> g) x $ x)
 
 -- LISTS
 
-type LCListT b = forall a . (b -> a -> a) -> a -> a
-newtype LCList b = LCList { unList :: LCListT b }
+type LCListPairStrT = forall a . ((LCPair LCStr) -> a -> a) -> a -> a
+newtype LCListPairStr = LCList { unList :: LCListPairStrT }
 
 -- empty list
-nil :: LCList a
+nil :: LCListPairStr
 nil = LCList $ \c -> \n -> n
 
 -- cons
-cons :: a -> LCList a -> LCList a
+cons :: LCPair LCStr -> LCListPairStr -> LCListPairStr
 cons = \h t -> LCList $ \c n -> c h (unList t c n)
 
 -- check if list is empty
-is_nil :: LCList a -> LCBool
+is_nil :: LCListPairStr -> LCBool
 is_nil = \l -> unList l (\h t -> false) true
 
 -- 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) nil
+-- in case of empty list just return a constant pair
+hd_l :: LCListPairStr -> LCPair LCStr
+hd_l = \l -> unList l (\h t -> h) (pair empty empty)
 
 -- 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 :: LCPair LCStr-> LCPair LCListPairStr -> LCPair LCListPairStr
 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 :: LCListPairStr -> LCListPairStr
 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 :: LCListPairStr -> LCListPairStr -> LCListPairStr
 append = \x y -> LCList $ \c n -> unList x c (unList y c n)
 
 -- PCP Algorithm
@@ -205,7 +197,7 @@ 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 :: LCList (LCPair LCStr) -> LCBool
+find_eq :: LCListPairStr -> 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))))
 
@@ -214,40 +206,40 @@ 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 :: LCPair LCStr -> LCList (LCPair LCStr) -> LCList (LCPair LCStr)
+map_cmb :: LCPair LCStr -> LCListPairStr -> LCListPairStr
 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 :: LCList (LCPair LCStr) -> LCList (LCPair LCStr) -> LCList (LCPair LCStr)
+cross_cmb :: LCListPairStr -> LCListPairStr -> LCListPairStr
 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 :: LCList (LCPair LCStr) -> LCBool
+-- if yes return true otherwise reitercte
+pcp :: LCListPairStr -> 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 :: LCList (LCPair LCStr)
+problem_1 :: LCListPairStr
 problem_1 = cons (pair a ab) (cons (pair bb b) nil)
 
 -- [(a, abbb), (bb, b)]
-problem_2 :: LCList (LCPair LCStr)
+problem_2 :: LCListPairStr
 problem_2 = cons (pair a abbb) (cons (pair bb b) nil)
 
 -- [(bba, b), (b, ab), (a, bba)]
-problem_3 :: LCList (LCPair LCStr) -- undecidable
+problem_3 :: LCListPairStr -- 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 :: LCList (LCPair LCStr) -- has a solution of length 76
+problem_4 :: LCListPairStr -- 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
@@ -261,3 +253,6 @@ lcbool_tostr :: LCBool -> String
 lcbool_tostr = \b -> ite b "True" "False"
 
 -- lcbool_tostr (pcp problem_1)
+
+-- reduction :: LCListPairStr -> LCStr
+reduction = \p -> (LCStr $ (ite (pcp p) aa bb)) (\x y z -> x z y)

pcp/ski.hs

@@ -4,8 +4,6 @@ type I = forall a . a -> a
 type K = forall a b . a -> b -> a
 type S = forall t1 t2 t3 . (t1 -> t2 -> t3) -> (t1 -> t2) -> t1 -> t3
 
-
-
 i :: I
 i = \x -> x
 
@@ -15,7 +13,20 @@ k = \x y -> x
 s :: S
 s = \x y z -> x z (y z)
 
-
-t20 = s s (s i)
+-- by def
+true = k
+-- (\x y z -> x z (y z)) ((\x y -> x) (\x y -> x)) (\x.x)
+-- (\x y z -> x z (y z)) (\y -> \x y -> x) (\x.x)
+-- (\z -> ((\y -> \x y -> x) z) ((\x.x) z))
+-- (\z -> ((\y -> \x y -> x) z) z)
+-- (\z -> (\x y -> x) z)
+-- (\z -> \y -> z)
+-- (t1 -> t2 -> t3) -> (t1 -> t2) -> t1 -> t3
+-- need to supply two arguments to s
+true2 = s (k k) (s k k)
+
+-- a -> b -> a
+-- need to supply term of type a -> a
+false = k (s k k)
 
 data SKITerm = I | K | S | A SKITerm SKITerm