diff --git a/lambda.hs b/lambda.hs index 2c893e6..2922b01 100644 --- a/lambda.hs +++ b/lambda.hs @@ -1,24 +1,45 @@ - import Data.List import Data.Maybe -- A symbol denoting a variable; consists of a textual name and some (or no) apostrophes to ensure uniqueness -data Symbol = Symbol { symBase :: String -- lowercase a to z - , symLen :: Int -- nonnegative - } +class (Eq s) => Symbol s where + -- Present symbols (not including symbol to change) -> symbol to change -> + -- simplest unique symbol + findName :: [s] -> s -> s + +-- Symbol that appends apostrophes to become unique +data SymApostrophe = SymApostrophe { symApoBase :: String -- lowercase a to z + , symApoLen :: Int -- nonnegative + } deriving (Eq) -instance Show Symbol where - show (Symbol s n) = s ++ (replicate n '\'') +instance Show SymApostrophe where + show (SymApostrophe s n) = s ++ (replicate n '\'') + +instance Symbol SymApostrophe where + findName other (SymApostrophe base n) = + let sameBase = filter ((base ==) . symApoBase) other + lengths = map symApoLen sameBase + freeLengths = [0..] \\ (nub lengths) + in SymApostrophe base (head freeLengths) -- [0..] is infinite + +-- Symbol that changes to another letter in the alphabet to become unique +data SymLetter = SymLetter {symLetBase :: String } -- lowercase a to z, aa to zz, ... + deriving (Eq) + +instance Show SymLetter where + show (SymLetter l) = l + +instance Symbol SymLetter where + findName other _ = + let bases = map symLetBase other + freeBases = names \\ (nub bases) + in SymLetter (head freeBases) + where letters = ['a'..'z'] + namesN 0 = [""] + namesN n = [n ++ [l] | n <- namesN (n - 1), l <- letters] + names = concatMap namesN [1..] --- Present symbols (not including symbol to change) -> symbol to change -> --- unique symbol with same base and minimal amount of apostrophes -findName :: [Symbol] -> Symbol -> Symbol -findName other (Symbol base n) = - let sameBase = filter ((base ==) . symBase) other - lengths = map symLen sameBase - freeLengths = [0..] \\ (nub lengths) - in Symbol base (head freeLengths) -- [0..] is infinite -- An expression. Can be a mere symbol, a lambda application, or a lambda abstraction. data Expression s = ESymbol s @@ -36,6 +57,9 @@ showTopLevel :: (Show s) => Expression s -> String showTopLevel e@(EExpr _ _) = tail . init . show $ e showTopLevel e = show e +printTopLevel :: (Show s) => Expression s -> IO () +printTopLevel = putStrLn . showTopLevel + {- Apply a function Insert an expression into another expression: @@ -43,7 +67,7 @@ Insert an expression into another expression: change all symbols within that expression to be unique in the expression's new context simplify all symbols -} -simplifyExpr :: [(Symbol, Symbol)] -> [Symbol] -> Expression Symbol -> Expression Symbol +simplifyExpr :: (Symbol s) => [(s, s)] -> [s] -> Expression s -> Expression s simplifyExpr mapping context (ESymbol s) = ESymbol $ fromMaybe (findName context s) $ lookup s mapping simplifyExpr mapping context (EExpr a b) = EExpr (simplifyExpr mapping context a) (simplifyExpr mapping context b) simplifyExpr mapping context (ELambda l e) = @@ -52,135 +76,100 @@ simplifyExpr mapping context (ELambda l e) = newcontext = newl : context in ELambda newl (simplifyExpr newmapping newcontext e) -makeUnique :: [Symbol] -> Expression Symbol -> Expression Symbol +makeUnique :: (Symbol s) => [s] -> Expression s -> Expression s makeUnique = simplifyExpr [] -simplify :: Expression Symbol -> Expression Symbol +simplify :: (Symbol s) => Expression s -> Expression s simplify = makeUnique [] -insertExpr :: Symbol -> Expression Symbol -> [Symbol] -> Expression Symbol -> Expression Symbol +insertExpr :: (Symbol s) => s -> Expression s -> [s] -> Expression s -> Expression s insertExpr r new context old@(ESymbol s) | r == s = makeUnique context new | otherwise = old insertExpr r new context (EExpr a b) = EExpr (insertExpr r new context a) (insertExpr r new context b) insertExpr r new context (ELambda l e) = ELambda l (insertExpr r new (l : context) e) -apply :: Expression Symbol -> Expression Symbol +apply :: (Symbol s) => Expression s -> Expression s apply (EExpr (ELambda s l) b) = insertExpr s b [] l -- [], not [s] apply (EExpr a@(EExpr _ _) b) = EExpr (apply a) b apply e = e +step :: (Symbol s) => Expression s -> Expression s step = simplify . apply --- EXPERIMENT ZONE START -- -letters = ['a'..'z'] -namesN :: Int -> [String] -namesN 0 = [""] -namesN n = [n ++ [l] | n <- namesN (n-1), l <- letters] -names :: [String] -names = concatMap namesN [1..] -findNewName :: [Symbol] -> Symbol -findNewName other = - let bases = map symBase other - freeBases = names \\ (nub bases) - in Symbol (head freeBases) 0 -simplifyExpr_ :: [(Symbol, Symbol)] -> [Symbol] -> Expression Symbol -> Expression Symbol -simplifyExpr_ mapping context (ESymbol s) = ESymbol $ fromMaybe (findNewName context) $ lookup s mapping -simplifyExpr_ mapping context (EExpr a b) = EExpr (simplifyExpr_ mapping context a) (simplifyExpr_ mapping context b) -simplifyExpr_ mapping context (ELambda l e) = - let newl = findNewName context - newmapping = (l, newl) : mapping - newcontext = newl : context - in ELambda newl (simplifyExpr_ newmapping newcontext e) -makeUnique_ :: [Symbol] -> Expression Symbol -> Expression Symbol -makeUnique_ = simplifyExpr_ [] -simplify_ :: Expression Symbol -> Expression Symbol -simplify_ = makeUnique_ [] -insertExpr_ :: Symbol -> Expression Symbol -> [Symbol] -> Expression Symbol -> Expression Symbol -insertExpr_ r new context old@(ESymbol s) - | r == s = makeUnique_ context new - | otherwise = old -insertExpr_ r new context (EExpr a b) = EExpr (insertExpr_ r new context a) (insertExpr_ r new context b) -insertExpr_ r new context (ELambda l e) = ELambda l (insertExpr_ r new (l : context) e) -apply_ :: Expression Symbol -> Expression Symbol -apply_ (EExpr (ELambda s l) b) = insertExpr_ s b [] l -- [], not [s] -apply_ (EExpr a@(EExpr _ _) b) = EExpr (apply_ a) b -apply_ e = e -step_ = simplify_ . apply_ --- EXPERIMENT ZONE END -- - -_s :: String -> Expression Symbol -_s s = ESymbol $ _ss s - -_ss :: String -> Symbol -_ss s = Symbol s 0 +_sa = flip SymApostrophe 0 +_sl = SymLetter +_ea s = ESymbol $ _sa s +_el s = ESymbol $ _sl s main = do putStrLn "Testing: Showing expressions" - print (EExpr (_s "a") (EExpr (_s "b") (_s "c"))) - print (EExpr (_s "a") (EExpr (_s "b") (EExpr (_s "c") (_s "d")))) - print (EExpr (EExpr (_s "a") (_s "b")) (_s "c")) - print (EExpr (EExpr (EExpr (_s "a") (_s "b")) (_s "c")) (_s "d")) - print (EExpr (EExpr (_s "a") (EExpr (_s "b") (_s "c"))) (_s "d")) - print (ELambda (Symbol "a" 0) (_s "a")) - print (ELambda (Symbol "a" 0) (EExpr (EExpr (_s "a") (EExpr (_s "b") (_s "c"))) (_s "d"))) + print (EExpr (_ea "a") (EExpr (_ea "b") (_ea "c"))) + print (EExpr (_ea "a") (EExpr (_ea "b") (EExpr (_ea "c") (_ea "d")))) + print (EExpr (EExpr (_ea "a") (_ea "b")) (_ea "c")) + print (EExpr (EExpr (EExpr (_ea "a") (_ea "b")) (_ea "c")) (_ea "d")) + print (EExpr (EExpr (_ea "a") (EExpr (_ea "b") (_ea "c"))) (_ea "d")) + print (ELambda (_sa "a") (_ea "a")) + print (ELambda (_sa "a") (EExpr (EExpr (_ea "a") (EExpr (_ea "b") (_ea "c"))) (_ea "d"))) putStrLn "" -- test of findName (seems to be working) ~G putStrLn "Testing: Finding new symbols" - print $ findName [(Symbol "a" 0), (Symbol "b" 0), (Symbol "a" 1)] (Symbol "a" 4) - print $ findName [(Symbol "a" 0), (Symbol "b" 0), (Symbol "a" 1)] (Symbol "b" 3) - print $ findName [(Symbol "a" 0), (Symbol "b" 0), (Symbol "a" 1)] (Symbol "c" 2) - print $ findName [(Symbol "a" 1), (Symbol "a" 3), (Symbol "a" 0)] (Symbol "a" 1) --- EXPERIMENT ZONE START -- - print $ findNewName [(Symbol "a" 0), (Symbol "b" 0), (Symbol "a" 1)] - print $ findNewName [(Symbol "a" 0), (Symbol "b" 0), (Symbol "a" 1)] - print $ findNewName [(Symbol "a" 0), (Symbol "b" 0), (Symbol "a" 1)] - print $ findNewName [(Symbol "a" 1), (Symbol "a" 3), (Symbol "a" 0)] --- EXPERIMENT ZONE END -- + putStrLn "SymApostrophe" + print $ findName [(SymApostrophe "a" 0), (SymApostrophe "b" 0), (SymApostrophe "a" 1)] (SymApostrophe "a" 4) + print $ findName [(SymApostrophe "a" 0), (SymApostrophe "b" 0), (SymApostrophe "a" 1)] (SymApostrophe "b" 3) + print $ findName [(SymApostrophe "a" 0), (SymApostrophe "b" 0), (SymApostrophe "a" 1)] (SymApostrophe "c" 2) + print $ findName [(SymApostrophe "a" 1), (SymApostrophe "a" 3), (SymApostrophe "a" 0)] (SymApostrophe "a" 1) + putStrLn "SymLetter" + print $ findName [(_sl "a"), (_sl "b"), (_sl "a")] (_sl "a") + print $ findName [(_sl "a"), (_sl "b"), (_sl "d")] (_sl "b") + print $ findName [(_sl "a"), (_sl "d"), (_sl "c")] (_sl "c") + print $ findName [(_sl "b"), (_sl "a"), (_sl "c")] (_sl "d") putStrLn "" putStrLn "Testing: Applying expressions" - let t = (ELambda (_ss "a") (ELambda (_ss "b") (ESymbol (_ss "a")))) - f = (ELambda (_ss "a") (ELambda (_ss "b") (ESymbol (_ss "b")))) - n = (ELambda (_ss "a") (EExpr (EExpr (ESymbol (_ss "a")) (makeUnique [(_ss "a")] f)) (makeUnique [(_ss "a")] t))) --- EXPERIMENT ZONE START -- - n_ = (ELambda (_ss "a") (EExpr (EExpr (ESymbol (_ss "a")) (makeUnique_ [(_ss "a")] f)) (makeUnique_ [(_ss "a")] t))) --- EXPERIMENT ZONE END -- - print t - print f - print n - print $ simplify $ (ELambda (Symbol "a" 1) (ESymbol (Symbol "a" 1))) - print (EExpr n f) - putStrLn $ showTopLevel (EExpr n f) + let ta = (ELambda (_sa "a") (ELambda (_sa "b") (_ea "a"))) + fa = (ELambda (_sa "a") (ELambda (_sa "b") (_ea "b"))) + na = (ELambda (_sa "a") (EExpr (EExpr (_ea "a") (makeUnique [(_sa "a")] fa)) (makeUnique [(_sa "a")] ta))) + tl = (ELambda (_sl "a") (ELambda (_sl "b") (_el "a"))) + fl = (ELambda (_sl "a") (ELambda (_sl "b") (_el "b"))) + nl = (ELambda (_sl "a") (EExpr (EExpr (_el "a") (makeUnique [(_sl "a")] fl)) (makeUnique [(_sl "a")] tl))) + print ta + print fa + print na + print tl + print fl + print nl + print $ simplify $ (ELambda (SymApostrophe "a" 1) (ESymbol (SymApostrophe "a" 1))) + print $ simplify $ (ELambda (_sl "b") (ESymbol (_sl "b"))) + putStrLn $ showTopLevel (EExpr na fa) + putStrLn $ showTopLevel (EExpr nl fl) putStrLn "" putStrLn "Replacing symbols: apostrophe" putStrLn "Running: not false" - print (EExpr n f) - print . step $ (EExpr n f) - print . step . step $ (EExpr n f) - print . step . step . step $ (EExpr n f) + printTopLevel (EExpr na fa) + printTopLevel . step $ (EExpr na fa) + printTopLevel . step . step $ (EExpr na fa) + printTopLevel . step . step . step $ (EExpr na fa) putStrLn "Running: not true" - print (EExpr n t) - print . step $ (EExpr n t) - print . step . step $ (EExpr n t) - print . step . step . step $ (EExpr n t) + printTopLevel (EExpr na ta) + printTopLevel . step $ (EExpr na ta) + printTopLevel . step . step $ (EExpr na ta) + printTopLevel . step . step . step $ (EExpr na ta) putStrLn "" --- EXPERIMENT ZONE START -- - putStrLn "Replacing symbols: new base" + putStrLn "Replacing symbols: letter" putStrLn "Running: not false" - print (EExpr n_ f) - print . step_ $ (EExpr n_ f) - print . step_ . step_ $ (EExpr n_ f) - print . step_ . step_ . step_ $ (EExpr n_ f) + printTopLevel (EExpr nl fl) + printTopLevel . step $ (EExpr nl fl) + printTopLevel . step . step $ (EExpr nl fl) + printTopLevel . step . step . step $ (EExpr nl fl) putStrLn "Running: not true" - print (EExpr n_ t) - print . step_ $ (EExpr n_ t) - print . step_ . step_ $ (EExpr n_ t) - print . step_ . step_ . step_ $ (EExpr n_ t) + printTopLevel (EExpr nl tl) + printTopLevel . step $ (EExpr nl tl) + printTopLevel . step . step $ (EExpr nl tl) + printTopLevel . step . step . step $ (EExpr nl tl) putStrLn "" --- EXPERIMENT ZONE END --