Commit 6b0a183e authored by Frontull Samuel's avatar Frontull Samuel
Browse files

bool types

parent 033db585
......@@ -2,16 +2,19 @@
module Pcp where
type LCBool = forall a . a -> a -> a
-- BOOLEANS
ite :: (t1 -> t2 -> t3) -> t1 -> t2 -> t3
ite = \c a b -> c a b
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 = \x y -> x
true = LCBool $ \x y -> x
false :: LCBool
false = \x y -> y
false = LCBool $ \x y -> y
at :: forall b. b -> LCBool
at = \x -> true
......@@ -19,47 +22,32 @@ at = \x -> true
af :: forall b. b -> LCBool
af = \x -> false
land :: (t1 -> (a -> a -> a) -> t2) -> t1 -> t2
land = \x y -> x y false
lor :: ((a -> a -> a) -> t1 -> t2) -> t1 -> t2
lor = \x y -> x true y
type LCStrSamuel = forall a . a -> (a -> a) -> (a -> a) -> a
newtype LCStr = LCStr { unChurch :: LCStrSamuel }
empty :: LCStr
empty = LCStr $ \x a b -> x
a :: LCStr
a = LCStr $ \x a b -> a x
land :: LCBool -> LCBool -> LCBool
land = \x y -> unBool x y false
b :: LCStr
b = LCStr $ \x a b -> b x
lor :: LCBool -> LCBool -> LCBool
lor = \x y -> unBool x true y
ab :: LCStr
ab = LCStr $ \x a b -> a (b x)
-- PAIRS
ba :: LCStr
ba = LCStr $ \x a b -> b (a x)
type LCPair a = (a -> a -> a) -> a
bb :: LCStr
bb = LCStr $ \x a b -> b (b x)
pair :: a -> a -> LCPair a
pair = \a -> \b -> \c -> c a b
bba :: LCStr
bba = LCStr $ \x a b -> b (b (a x))
first :: LCPair a -> a
first = \p -> p (\x -> \y -> x)
abb :: LCStr
abb = LCStr $ \x a b -> a (b (b x))
second :: LCPair a -> a
second = \p -> p (\x -> \y -> y)
abba :: LCStr
abba = LCStr $ \x a b -> a (b (b (a x)))
-- STRINGS
abbb :: LCStr
abbb = LCStr $ \x a b -> a (b (b (b x)))
type LCStrT = forall a . a -> (a -> a) -> (a -> a) -> a
newtype LCStr = LCStr { unChurch :: LCStrT }
baba :: LCStr
baba = LCStr $ \x a b -> b (a (b (a x)))
empty :: LCStr
empty = LCStr $ \x a b -> x
isempty :: LCStr -> LCBool
isempty = \s -> unChurch s true af af
......@@ -73,17 +61,6 @@ 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 LCPair a = (a -> a -> a) -> a
pair :: a -> a -> LCPair a
pair = \a -> \b -> \c -> c a b
first :: LCPair a -> a
first = \p -> p (\x -> \y -> x)
second :: LCPair a -> a
second = \p -> p (\x -> \y -> y)
nexta :: LCPair LCStr -> LCPair LCStr
nexta = \x -> pair (prepa (first x)) (first x)
......@@ -105,12 +82,6 @@ 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)
-- ycomb :: (t -> t) -> t
-- ycomb f = f (ycomb f)
newtype Mu a = Mu (Mu a -> a)
ycomb f = (\h -> h $ Mu h) (\x -> f . (\(Mu g) -> g) x $ x)
eq :: LCStr -> LCStr -> LCBool
eq = ycomb (\f x y ->
ite (lor (isempty x) (isempty y))
......@@ -120,27 +91,66 @@ eq = ycomb (\f x y ->
prefix :: LCStr -> LCStr -> LCBool
prefix = ycomb (\f x y -> ite (isempty x) true (land (hd_eq x y) (f (tl x) (tl y))))
-- SOME STRINGS
a :: LCStr
a = LCStr $ \x a b -> a x
b :: LCStr
b = LCStr $ \x a b -> b x
ab :: LCStr
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)))
-- RECURSION
-- ycomb :: (t -> t) -> t
-- ycomb f = f (ycomb f)
newtype Mu a = Mu (Mu a -> a)
ycomb f = (\h -> h $ Mu h) (\x -> f . (\(Mu g) -> g) x $ x)
-- LISTS
type LCListChurch b = forall a . (b -> a -> a) -> a -> a
newtype LCList b = LCList { unList :: LCListChurch b }
-- List (nil)
nil :: LCList a
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)
is_nil :: LCList a -> LCBool
is_nil = \l -> unList l (\h t -> false) true
-- List Head - Idea to make it typable from Types and Programming Languages by Pierce
-- List Head - Idea to make it typable using unit 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
hd_l = \l -> (unList l (\h t u -> h) (diverge)) ()
next_l :: a -> LCPair (LCList a) -> LCPair (LCList a)
next_l = \h p -> pair (cons h (first p)) (first p)
tl_l :: LCList a -> LCList a
......@@ -149,6 +159,8 @@ 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)
-- PCP Algorithm
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)
......@@ -170,12 +182,6 @@ cross_cmb = ycomb (\f x y -> ite (is_nil x) nil (append (map_cmb (hd_l x) y) (f
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"
-- PCP Problems
problem_1 :: LCList (LCPair LCStr)
......@@ -187,4 +193,12 @@ problem_2 = cons (pair a abbb) (cons (pair bb b) nil)
problem_3 :: LCList (LCPair LCStr) -- undecidable
problem_3 = cons (pair bba b) (cons (pair b ab) (cons (pair a bba) nil))
-- Output functions
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 problem_1)
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment