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

transform to ski calculus

parent 029ca04e
......@@ -253,6 +253,10 @@ type wbp = Empty | Node of string * symbol * simple_type | Comp of wbp list
let posymtyp_to_node = function p, s, t -> Node (p, s, t)
let wbp_isempty = function
| Empty -> true
| _ -> false
let append_wbp p n =
match p with
| Empty -> n
......@@ -596,6 +600,83 @@ let legal_paths term =
(* let wbp = L.filter is_legal wbp in *)
(fst wbp, L.map wbp_tolist (snd wbp))
let prepos pos = String.sub pos 0 ((String.length pos) - 1)
let rec _lazy_well_balanced_paths newpaths acc nodes bedges n =
if n <= 0 then (false, acc)
else
let apps =
L.filter (fun x -> match x with pa, AS _, _ -> pa != "e" | _ -> false) nodes
in
let activatedapps = L.filter (fun x -> not (wbp_isempty x)) (
L.map
(fun x ->
match x with
| pa, AS s, typ ->
let ppa = prepos pa in
let pexists = List.exists (fun x -> x = ppa) (List.map node_pos (List.map last_wbp acc)) in
let acc_acl = L.filter (fun p -> islam_node (last_wbp p)) acc in
let pexists2 = List.exists (fun x -> x = ppa) (List.map node_pos (List.map first_wbp acc_acl)) in
if pexists || pexists2 then
Comp
[
Node (pa, AS s, typ);
posymtyp_to_node (L.hd (get_node (pa ^ "0") nodes));
]
else Empty
| _ -> Empty)
apps)
in
let newpaths = newpaths @ activatedapps in
let paths = composition newpaths acc nodes bedges in
let newpaths =
L.filter
(fun x ->
(not (L.mem x acc))
&& (not (first_wbp x = last_wbp x)))
paths
in
let newacc = acc @ newpaths in
match newpaths with
| [] -> (true, acc)
| _ -> _lazy_well_balanced_paths newpaths newacc nodes bedges (n - 1)
let lazy_well_balanced_paths term =
let nodes = term_nodes term in
let bedges = b_edges term in
let apps =
L.filter (fun x -> match x with pa, AS _, _ -> pa = "e" | _ -> false) nodes
in
let acc = L.filter (fun x -> not (wbp_isempty x)) (
L.map
(fun x ->
match x with
| pa, AS s, typ -> (
let fp = posymtyp_to_node (L.hd (get_node (pa ^ "0") nodes)) in
match fp with
| Node (_, LS _ ,_) -> Comp [Node (pa, AS s, typ);fp]
| _ -> Empty
)
| _ -> Empty)
apps)
in
let max_compositions = 10 in
let compose = _lazy_well_balanced_paths acc acc nodes bedges max_compositions in
(fst compose, snd compose)
let lazy_well_balanced_paths_al term =
let lazy_wbp = lazy_well_balanced_paths term in
let applam = L.filter (fun p -> islam_node (last_wbp p)) (snd lazy_wbp) in
(fst lazy_wbp, applam)
let lazy_legal_paths term =
let lazy_wbp = lazy_well_balanced_paths_al term in
(* let wbp = L.filter is_legal wbp in *)
(fst lazy_wbp, L.map wbp_tolist (snd lazy_wbp))
let is_scc nodes path =
let f = get_node (L.hd path) nodes in
let l = get_node (L.hd (L.rev path)) nodes in
......@@ -783,6 +864,21 @@ let rec _reduce_lo subst term =
let reduce_lo subst term = _reduce_lo subst term
let rec _reduce_lazy subst term =
match term with
| AVar (s, t) -> term
| ALam ((xs, e), t) -> term
| AApp (e1, e2, t) -> (
match e1 with
| ALam _ -> beta subst term
| _ ->
let left = _reduce_lo subst e1 in
if left = e1 then AApp (e1, e2, t)
(* if left = e1 then AApp (e1, _reduce_lo subst e2, t) *)
else AApp (left, e2, t) )
let reduce_lazy subst term = _reduce_lazy subst term
let rec _reduce_ne subst term =
match term with
| AVar (s, t) -> term
......@@ -869,6 +965,10 @@ let rec nf subst term =
let new_term = reduce_lo subst term in
if new_term = term then term else nf subst new_term
let rec whnf subst term =
(* Printf.printf "%d %s\n" (size term) (a_term_to_string term); *)
let new_term = reduce_lazy subst term in
if new_term = term then term else whnf subst new_term
let rec _reduce_lo_memo subst term cache =
match Hashtbl.mem cache term with
......
module Term (
-- * Exercises 2 and 3
-- | See <../pdfs/05.pdf>.
Id,
Term(..),
-- * Exercise 4
vars, fvs,
-- * Exercise 5
freshName,
-- * Exercise 6
subst
) where
import Data.List
import Data.Maybe (fromJust)
-- | Identifiers as @String@s.
type Id = String
-- | Lambda terms: variables, application, abstraction.
data Term = Var Id | App Term Term | Abs Id Term | S | K | I
{-|
The set of all variables occurring in a term. For example
> vars (App (Var "x") (Abs "y" (Var "y"))) == ["x", "y"]
-}
vars :: Term -> [Id]
vars (Var x) = [x]
vars (App t u) = vars t `union` vars u
vars (Abs x t) = [x] `union` vars t
{-|
The set of free variables occurring in a term. For example
> fvs (App (Var "x") (Abs "y" (Var "y"))) == ["x"]
-}
fvs :: Term -> [Id]
fvs (Var x) = [x]
fvs (App t u) = fvs t `union` fvs u
fvs (Abs x t) = fvs t \\ [x]
fvs _ = []
-- infinite list of variants of a given string
variants :: String -> [String]
variants [] = [[]]
variants [x] = [[y] | y <- [x .. 'z']] ++ map (x:) (variants "a")
variants (x:xs) = map (x:) $ variants xs
-- apply a renaming function to all variables of a term
rename :: (Id -> Id) -> Term -> Term
rename r (Var y) = Var (r y)
rename r (App t u) = App (rename r t) (rename r u)
rename r (Abs x t) = Abs (r x) (rename r t)
{-|
Given a variable @x@ and a set of variable names to avoid @ys@, @freshName x ys@
computes a pair @(x', ren)@ such that @x'@ is a variable that is fresh for @ys@
(that is, different from all elements of @ys@) and @ren :: Term -> Term@ is a
function that renames all occurrences of @x@ in a term by @x'@.
-}
freshName :: Id -> [Id] -> (Id, (Term -> Term))
freshName x ys = (x', ren)
where
x' = head $ dropWhile (`elem` ys) $ variants x
ren = rename (\v -> if v == x then x' else v)
{-|
Applying a substition @[x := s]@ to a lambda term @t@. For example (note how the
bound variable @"y"@ is renamed in order to avoid variable capture)
> subst "x" (Var "y") (Abs "y" (App (Var "x") (Var "y"))) == Abs "z" (App (Var "y") (Var "z"))
-}
subst :: Id -> Term -> Term -> Term
subst x s (Var y) = if x == y then s else Var y
subst x s (App t u) = App (subst x s t) (subst x s u)
subst x s u@(Abs y t) = if x `elem` fvs u then Abs y' (subst x s (ren t)) else u
where
-- variables to avoid in fresh name
taboo = [x] `union` (fvs s `union` (vars t \\ [y]))
(y', ren) = freshName y taboo
{-|
Custom @Show@ instance for readability.-}
instance Show Term where
showsPrec d (Var x) = showString x
showsPrec d (App t u) = showParen (d > app_prec) $
showsPrec app_prec t .
showString " " .
showsPrec (app_prec + 1) u
where
app_prec = 5
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
showsPrec d S = showString "S"
showsPrec d K = showString "K"
showsPrec d I = showString "I"
instance Eq Term where
(Var y) == (Var z) = y==z
(App x1 x2) == (App y1 y2) = x1==y1 && x2 == y2
(Abs x t1) == (Abs y t2) = x==y && t1 == t2
_ == _ = False
churchNum :: Term -> Maybe Int
churchNum (Abs f (Abs x t)) = power f x t
where
power _ x (Var y) = if x == y then Just 0 else Nothing
power f x (App (Var g) t) =
if f == g then case power f x t of
Nothing -> Nothing
Just n -> Just $ n + 1
else Nothing
power _ _ _ = Nothing
churchNum _ = Nothing
isChurchNum t = churchNum t /= Nothing
beta :: Term -> Term
beta (App (Abs x t) u) = subst x u t
beta x = x
betastep :: Term -> Term
betastep (Abs x t) = Abs x (betastep t)
betastep (App (Abs x e1) e2) = beta (App (Abs x e1) e2)
betastep (App e1 e2) =
let left = betastep e1 in
if left == e1 then App e1 (betastep e2)
else App left e2
betastep x = x
nf :: Term -> Term
nf term = if (betastep term) == term then term else nf (betastep term)
-- data SKITerm = S | K | I | CA SKITerm SKITerm
--
-- instance Show SKITerm where
-- show S = show "S"
-- show K = show "K"
-- show I = show "I"
-- show (CA x y) = "(" ++ (show x) ++ " " ++ (show y) ++ ")"
-- ttran :: Term -> SKITerm
ttran (App x y) = App (ttran x) (ttran y)
ttran (Abs x (Var y)) =
if x == y then I
else App K (Var y)
ttran (Abs x (Abs y e1)) =
let f = elem x (fvs e1) in
if f then ttran (Abs x (ttran (Abs y e1)))
else App K (ttran (Abs y e1))
ttran (Abs x (App e1 e2)) =
let f1 = elem x (fvs e1) in
let f2 = elem x (fvs e2) in
if f1 || f2 then App (App S (ttran (Abs x e1))) (ttran (Abs x e2))
else App K (ttran (App e1 e2))
ttran (Abs x ski) = App K (ttran ski)
ttran x = x
true :: Term
true = Abs "x" (Abs "y" (Var "x"))
false :: Term
false = Abs "x" (Abs "y" (Var "y"))
ite :: Term
ite = Abs "c" (Abs "a" (Abs "b" (App (App (Var "c") (Var "a")) (Var "b"))))
land :: Term
land = Abs "x" (Abs "y" (App (App (Var "x") (Var "y")) false))
lor :: Term
lor = Abs "x" (Abs "y" (App (App (Var "x") true) (Var "y")))
......@@ -42,11 +42,11 @@ pair = \a -> \b -> \c -> c a b
-- select first element in pair
first :: LCPair a -> a
first = \p -> p (\x -> \y -> x)
first = \p -> p (\x y -> x)
-- select second element in pair
second :: LCPair a -> a
second = \p -> p (\x -> \y -> y)
second = \p -> p (\x y -> y)
-- STRINGS
......@@ -178,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) nil
-- 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)
......
{-# LANGUAGE RankNTypes #-}
module Pcp where
data T = O
-- BOOLEANS
type LCBoolT = T -> T -> T
newtype LCBool = LCBool { unBool :: LCBoolT }
true :: LCBool
true = LCBool $ \x y -> x
false :: LCBool
false = LCBool $ \x y -> y
-- if then else
ite :: LCBool -> T -> T -> T
ite = \c a b -> unBool c a b
-- returns always true
at :: T -> LCBool
at = \x -> true
-- returns always false
af :: T -> LCBool
af = \x -> false
-- logical and
land :: LCBool -> LCBool -> LCBool
land = \x y -> x y false
-- logical or
lor :: LCBool -> LCBool -> LCBool
lor = \x y -> unBool x true y
-- PAIRS
type LCPair = (T -> T -> T) -> T
pair :: T -> T -> LCPair
pair = \a -> \b -> \c -> c a b
-- select first element in pair
first :: LCPair -> T
first = \p -> p (\x y -> x)
-- select second element in pair
second :: LCPair -> T
second = \p -> p (\x y -> y)
-- STRINGS
-- type LCStrT = (T -> T) -> (T -> T) -> T -> T
-- newtype LCStr = LCStr { unString :: LCStrT }
--
-- 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)
--
-- -- 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))
--
-- -- get a pair of strings (s1, s2) and return (a(s1), s1)
-- nexta :: LCPair -> LCPair
-- nexta = \x -> pair (prepa (first x)) (first x)
--
-- -- get a pair of strings (s1, s2) and return (b(s1), s1)
-- nextb :: LCPair -> LCPair
-- 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))))
--
-- -- SOME STRINGS
--
-- a :: LCStr
-- a = LCStr $ \a b x -> a x
--
-- b :: LCStr
-- b = LCStr $ \a b x -> b x
--
-- ab :: LCStr
-- ab = LCStr $ \a b x -> a (b x)
--
-- ba :: LCStr
-- ba = LCStr $ \a b x -> b (a x)
--
-- bb :: LCStr
-- bb = LCStr $ \a b x -> b (b x)
--
-- baa :: LCStr
-- 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
-- -- 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
--
-- type LCListT b = forall a . (b -> a -> a) -> a -> a
-- newtype LCList b = LCList { unList :: LCListT 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
--
-- -- 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
--
-- -- 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 = \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
--
-- -- get a pair of strings (a s1, a s2) and return (s1, s2)
-- 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 :: 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 = 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 :: 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 = 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 = 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
-- 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 = cons (pair a ab) (cons (pair bb b) nil)
--
-- -- [(a, abbb), (bb, b)]
-- problem_2 :: LCList (LCPair LCStr)
-- 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 = 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 = cons (pair ab a) (cons (pair ab bba) (cons (pair a baa) (cons (pair baa ba) nil)))
--
-- -- PARSE LC ENCODINGS TO STRINGS
--
-- -- string encoding to String
-- lcstr_tostr :: LCStr -> String
-- lcstr_tostr = \s -> unString s (\a -> "a" ++ a) (\b -> "b" ++ b) ("")
--
-- -- bool encoding to String
-- lcbool_tostr :: LCBool -> String
-- lcbool_tostr = \b -> ite b "True" "False"
--
-- -- lcbool_tostr (pcp problem_1)
--
--
-- s :: T -> T
-- s = \x -> x
{-# LANGUAGE RankNTypes #-}
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
k :: K
k = \x y -> x
s :: S
s = \x y z -> x z (y z)
t20 = s s (s i)
data SKITerm = I | K | S | A SKITerm SKITerm
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