pcp lambda calculus in haskell

pcp/pcp.hs

@@ -2,8 +2,7 @@
 
 module Pcp where
 
-type LCBool = forall a.a -> a -> a
--- newtype LCBoolC = LCBoolC { unBool :: LCBool }
+type LCBool = forall a . a -> a -> a
 
 ite :: (t1 -> t2 -> t3) -> t1 -> t2 -> t3
 ite = \c a b -> c a b
@@ -26,8 +25,8 @@ land = \x y -> x y false
 lor :: ((a -> a -> a) -> t1 -> t2) -> t1 -> t2
 lor = \x y -> x true y
 
-type LCStrSam = forall a . a -> (a -> a) -> (a -> a) -> a
-newtype LCStr = LCStr { unChurch :: LCStrSam }
+type LCStrSamuel = forall a . a -> (a -> a) -> (a -> a) -> a
+newtype LCStr = LCStr { unChurch :: LCStrSamuel }
 
 empty :: LCStr
 empty = LCStr $ \x a b -> x
@@ -44,9 +43,21 @@ ab = LCStr $ \x a b -> a (b x)
 ba :: LCStr
 ba = LCStr $ \x a b -> b (a x)
 
+bb :: LCStr
+bb = LCStr $ \x a b -> b (b x)
+
+bba :: LCStr
+bba = LCStr $ \x a b -> b (b (a x))
+
+abb :: LCStr
+abb = LCStr $ \x a b -> a (b (b x))
+
 abba :: LCStr
 abba = LCStr $ \x a b -> a (b (b (a x)))
 
+abbb :: LCStr
+abbb = LCStr $ \x a b -> a (b (b (b x)))
+
 baba :: LCStr
 baba = LCStr $ \x a b -> b (a (b (a x)))
 
@@ -62,30 +73,29 @@ prepa = \s -> LCStr $ \x a b -> a (unChurch s x a b)
 prepb :: LCStr -> LCStr
 prepb = \s -> LCStr $ \x a b -> b (unChurch s x a b)
 
--- type LCPairSam = (LCStr -> LCStr -> LCStr) -> LCStr
--- newtype LCPair = LCPair { unPair :: LCPairSam }
+type LCPair a = (a -> a -> a) -> a
 
-pair :: a1 -> a2 -> (a1 -> a2 -> a) -> a
+pair :: a -> a -> LCPair a
 pair = \a -> \b -> \c -> c a b
 
-first :: ((a2 -> a1 -> a2) -> a) -> a
+first :: LCPair a -> a
 first = \p -> p (\x -> \y -> x)
 
-second :: ((a1 -> a2 -> a2) -> a) -> a
+second :: LCPair a -> a
 second = \p -> p (\x -> \y -> y)
 
-nexta :: ((a2 -> a1 -> a2) -> LCStr) -> (LCStr -> LCStr -> a) -> a
+nexta :: LCPair LCStr -> LCPair LCStr
 nexta = \x -> pair (prepa (first x)) (first x)
 
-nextb :: ((a2 -> a1 -> a2) -> LCStr) -> (LCStr -> LCStr -> a) -> a
+nextb :: LCPair LCStr -> LCPair LCStr
 nextb = \x -> pair (prepb (first x)) (first x)
---
+
 hd_a :: LCStr -> LCBool
 hd_a = \s -> unChurch s false at af
---
+
 hd_b :: LCStr -> LCBool
 hd_b = \s -> unChurch s false af at
---
+
 hd_eq :: LCStr -> LCStr -> LCBool
 hd_eq = \x y -> lor (land (hd_a x) (hd_a y)) (land (hd_b x) (hd_b y))
 
@@ -94,11 +104,8 @@ hd = \s -> LCStr $ \x a b -> unChurch s x (\y -> a x) (\y -> b x)
 
 tl :: LCStr -> LCStr
 tl = \s -> second (unChurch s (pair empty empty) nexta nextb)
---
--- -- A non-recursive version of the Y combinator
--- newtype Mu a = Mu (Mu a -> a)
--- ynr f = (\h -> h $ Mu h) (\x -> f . (\(Mu g) -> g) x $ x)
---
+
+ycomb :: (t -> t) -> t
 ycomb g = g (ycomb g)
 
 eq :: LCStr -> LCStr -> LCBool
@@ -111,12 +118,8 @@ prefix :: LCStr -> LCStr -> LCBool
 prefix = ycomb (\f x y -> ite (isempty x) true (land (hd_eq x y) (f (tl x) (tl y))))
 
 -- LISTS
--- type LCListSam = forall a.(a -> a -> a) -> a -> a
--- newtype LCList = LCList { unList :: LCListSam }
-
--- type LCListSam a = forall b . (a -> b -> b) -> b -> b
-type LCListSam b = forall a . (b -> a -> a) -> a -> a
-newtype LCList b = LCList { unList :: LCListSam b }
+type LCListChurch b = forall a . (b -> a -> a) -> a -> a
+newtype LCList b = LCList { unList :: LCListChurch b }
 
 -- List (nil)
 nil :: LCList a
@@ -124,20 +127,17 @@ nil = LCList $ \c -> \n -> n
 
 -- List Cons
 cons :: a -> LCList a -> LCList a
--- cons = \h t -> LCList $ \c n -> c h (unList t c n)
 cons = \h t -> LCList $ \c n -> c h (unList t c n)
 
 is_nil :: LCList a -> LCBool
--- is_nil = \x -> unList x (\h t -> false) true
 is_nil = \l -> unList l (\h t -> false) true
 
--- -- List Head
+-- List Head - Idea to make it typable from Types and Programming Languages by Pierce
 hd_l :: (LCList a) -> a
 unit = ()
 diverge = \u -> ycomb (\x -> x)
 hd_l = \l -> (unList l (\h t u -> h) (diverge)) unit
 
--- List Tail
 next_l = \h p -> pair (cons h (first p)) (first p)
 
 tl_l :: LCList a -> LCList a
@@ -146,34 +146,33 @@ tl_l = \l -> second (unList l next_l (pair nil nil))
 append :: LCList a -> LCList a -> LCList a
 append = \x y -> LCList $ \c n -> unList x c (unList y c n)
 
--- lent = ycomb (\f x -> ite (is_nil x) 0 (1 + (f (tl_l x))))
---
--- flat :: LCList String -> String
--- flat = (ycomb (\f x -> ite (is_nil x) "" ((hd_l x) ++ (f (tl_l x))))) (cons "as" nil)
-
--- PCP
-simp' :: (LCStr -> LCStr -> (LCStr -> LCStr -> a) -> a)
-     -> LCStr -> LCStr -> (LCStr -> LCStr -> a) -> a
-simp' = \f x y -> ite (lor (isempty x) (isempty y)) (pair x y) (f (tl x) (tl y))
-
-simp :: ((a1 -> a1 -> a1) -> LCStr) -> (LCStr -> LCStr -> a) -> a
-simp = \p -> ycomb simp' (first p) (second p)
+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)
 
+pvalid :: LCPair LCStr -> LCBool
 pvalid = \p -> lor (prefix (first p) (second p)) (prefix (second p) (first p))
 
+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))))
 
+cmb :: LCPair LCStr -> LCPair LCStr -> LCPair LCStr
 cmb = \p s -> pair (conc (first p) (first s)) (conc (second p) (second s))
 
+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))))
 
+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)))
 
-pcp' = \f x y -> ite (is_nil x) false (ite (find_eq x) true (f (cross_cmb x y) y))
-pcp = \x -> ycomb pcp' x x
+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
 
 lcstr_tostr :: LCStr -> String
 lcstr_tostr = \s -> unChurch s ("") (\a -> "a" ++ a) (\b -> "b" ++ b)
 
 lcbool_tostr :: LCBool -> String
 lcbool_tostr = \b -> ite b "True" "False"
+
+-- lcbool_tostr (pcp (cons (pair a ab) (cons (pair bb b) nil)))
+-- lcbool_tostr (pcp (cons (pair a abbb) (cons (pair bb b) nil)))
+-- lcbool_tostr (pcp (cons (pair bba b) (cons (pair b ab) (cons (pair a bba) nil))))