Toto je starší verze dokumentu!
Lambda calculus, Church encoding, http://safalra.com/science/lambda-calculus
T | λxy.x | λxy.xy | λxy.x | λxy.x |
|---|---|---|---|---|
F | λxy.y | λxy.y | λxy.yx | λxy.xy |
NOT | λx.xFT | λx.x(λz.F)T | λp.pF(λr.T) | λx.xFT |
AND | λxy.xyF | λxy.y(λz.x)F | λab.ab(λr.F) | λxy.xyF |
OR | λxy.xTy | λxy.y(λz.T)x | λab.aT(λr.b) | λxy.xTy |
XOR | λxy.x(NOT y)y | λxy.x(λz.(NOT y))y | λxy.x(NOT y)(λz.y) | λxy.x(NOT y)y |
EQ | λxy.xy(NOT y) | λxy.x(λz.y)(NOT y) | λxy.xy(λz.(NOT y)) | λxy.xy(NOT y) |
<Presci> Pitel: no ne vsechny, ale kdyz ti true nebo false budou vracet dve hodnodty (LET TRUE = \a b.b a, tak tu jednu musis nejak zabit (treba v notu) <Presci> a zabijes ji tam, ze ji nahradis \a.False treba, takze "a" se zahodi a zbyte False
| 0, 1, 2, 3, … | λfx.x λfx.fx λfx.f(fx) λfx.f(f(fx)) λfx.fnx |
|---|---|
| succ | λxgm.xg(gm) |
| add | λabgm.ag(bgm) |
| mult | λmnf.m(nf) |
| iszero | λm.m(λv.FALSE)TRUE |
| if then else | λctf.ctf |
| tuple | λfse.efs |
| first | λp.p TRUE |
| second | λp.p FALSE |
Learn You a Haskell for Great Good!
Sepsal Mike T
----------------------------------- ---------- LAMBDA KALKUL ----------------------------------- data LE = LVar String -- V | LApp LE LE -- (E1 E2) | LAbs String LE -- (\V . E) deriving (Show, Eq) -- Vrátí seznam všech volných proměnných v lambda výrazu. freeVars :: LE -> [String] freeVars lexp = fv lexp [] where fv (LVar v) xs = if elem v xs then [] else [v] fv (LApp lexp1 lexp2) xs = (fv lexp1 xs) ++ (fv lexp2 xs) fv (LAbs v lexp) xs = fv lexp (v:xs) -- Vrátí seznam všech vázaných proměnných v lambda výrazu. boundVars :: LE -> [String] boundVars lexp = bv lexp [] where bv (LVar v) xs = if elem v xs then [v] else [] bv (LApp lexp1 lexp2) xs = (bv lexp1 xs) ++ (bv lexp2 xs) bv (LAbs v lexp) xs = bv lexp (v:xs) -- Zjistí zda-li je možné provést substituci. -- isValidSub lexp lexp' v === lexp [lexp' / v] isValidSub :: LE -> LE -> String -> Bool isValidSub lexp lexp' v = validate lexp [] where validate (LVar var) xs = if (var == v) -- Jestli jde o proměnnou co se nahrazuje, -- musí být volná v lexp, a žádná volná v lexp' se nesmí stát vázanou. then (isFree var) && (check xs fv') -- Ostatní proměnné jsou OK. else True validate (LApp e1 e2) xs = (validate e1 xs) && (validate e2 xs) validate (LAbs var e) xs = validate e (var:xs) fv' = freeVars lexp' fv = freeVars lexp -- Zkontroluje zda průnik seznamů je prázdný check as bs = [ a | a <- as, b <- bs, a == b ] == [] isFree f = elem f fv alfaRed :: LE -> String -> LE alfaRed (LAbs v lexp) v' = if isFree v' lexp then error "Neplatna substituce (volna by se stala vazanou)" else (LAbs v' $ doAlfa lexp v' v) where isFree var lexp = elem var $ freeVars lexp doAlfa (LVar x) v' v = if x == v then (LVar v') else (LVar x) doAlfa (LApp lexp1 lexp2) v' v = LApp (doAlfa lexp1 v' v) (doAlfa lexp2 v' v) doAlfa (LAbs var lexp) v' v = LAbs var (doAlfa lexp v' v) betaRed :: LE -> LE betaRed (LApp (LAbs v e1) e2) = if isValidSub e1 e2 v then doBeta e1 e2 v else error "Neplatna substituce" where doBeta (LVar x) e v = if v == x then e else (LVar x) doBeta (LApp e1 e2) e v = LApp (doBeta e1 e v) (doBeta e2 e v) doBeta (LAbs x e1) e v = LAbs x (doBeta e1 e v) etaRed :: LE -> LE etaRed l@(LAbs v (LApp e (LVar v'))) = if v == v' && isNotFree then e else l where isNotFree = not $ elem v (freeVars e) subst :: LE -> LE -> String -> LE subst lexp lexp' v = if isValidSub lexp lexp' v then doSubst lexp else error "Substituce neni validni" where doSubst lvar@(LVar var) = if var == v then lexp' else lvar doSubst (LApp e1 e2) = LApp (doSubst e1) (doSubst e2) doSubst (LAbs var e) = LAbs var (doSubst e)
---- ------ BINÁRNÍ STROM ------------------------- data BTree a = Empty | Node a (BTree a) (BTree a) deriving (Show, Eq) singleton :: a -> BTree a singleton x = Node x (Empty) (Empty) treeInsert :: (Ord a) => a -> BTree a -> BTree a treeInsert x Empty = singleton x treeInsert x (Node a left right) | x == a = Node x left right | x < a = Node a (treeInsert x left) right | x > a = Node a left (treeInsert x right) treeFromList :: (Ord a) => [a] -> BTree a treeFromList xs = foldl (\acc x -> treeInsert x acc) Empty xs treeElem :: (Ord a) => a -> BTree a -> Bool treeElem x Empty = False treeElem x (Node a left right) | x == a = True | x < a = treeElem x left | x > a = treeElem x right treeEmpty :: BTree a -> Bool treeEmpty Empty = True treeEmpty _ = False treeNotEmpty :: BTree a -> Bool treeNotEmpty Empty = False treeNotEmpty _ = True treeRemoveElem :: (Ord a) => a -> BTree a -> BTree a treeRemoveElem x Empty = Empty treeRemoveElem x (Node a left right) | x < a = Node a (treeRemoveElem x left) right | x > a = Node a left (treeRemoveElem x right) | x == a && treeEmpty left && treeEmpty right = Empty | x == a && treeEmpty left && treeNotEmpty right = right | x == a && treeNotEmpty left && treeEmpty right = left | otherwise = Node (mostLeft right) left (treeRemoveElem (mostLeft right) right) where mostLeft (Node b l r) = if treeEmpty l then b else mostLeft l treePathToElem :: (Ord a) => a -> BTree a -> [a] treePathToElem x tree | not (treeElem x tree) = [] | otherwise = path x tree [] where path x (Node a left right) l | x == a = l ++ [a] | x < a = path x left (l ++ [a]) | x > a = path x right (l ++ [a]) treeDepth :: BTree a -> Int treeDepth Empty = 0 treeDepth (Node a left right) = 1 + max (treeDepth left) (treeDepth right) treePreorder :: BTree a -> [a] treePreorder x = pre x where pre Empty = [] pre (Node a left right) = (a:(pre left)) ++ (pre right) treePostorder :: BTree a -> [a] treePostorder x = post x where post Empty = [] post (Node a left right) = ((post left) ++ (post right)) ++ [a] treeInorder :: BTree a -> [a] treeInorder x = ino x where ino Empty = [] ino (Node a left right) = (ino left ) ++ (a:(ino right))
import IO {- -- Jen pro pripomenuti: data IOMode = ReadMode | WriteMode | AppendMode | ReadWriteMode getLine :: IO String putStrLn :: String -> IO () type FilePath = [Char] -- tj. jméno souboru openFile :: FilePath -> IOMode -> IO Handle hIsEOF :: Handle -> IO Bool hGetLine :: Handle -> IO String hClose :: Handle -> IO () hGetContents :: Handle -> IO String readFile :: FilePath -> IO String lines :: String -> [String] unlines :: [String] -> String words :: String -> [String] unwords :: [String] -> String -} -- Spocte pocet radku v souboru. countLines file = do content <- readFile file putStrLn $ show $ length $ lines content -- Spocte pocet slov v prvnich n radcich v souboru. countWordsN file n = do content <- readFile file putStrLn $ show $ length $ words $ unlines $ take n $ lines content -- Prokladane vypise obsah souboru na vystup. prokladane file1 file2 = do h1 <- openFile file1 ReadMode h2 <- openFile file2 ReadMode c1 <- hGetContents h1 c2 <- hGetContents h2 write (lines c1) (lines c2) hClose h1 hClose h2 where write [] _ = return () write _ [] = return () write (x:xs) (y:ys) = do putStrLn x putStrLn y write xs ys -- Vypise obsah souboru s cisly radky. printWithLineNumber file = do h <- openFile file ReadMode c <- hGetContents h write (lines c) 1 hClose h where write [] _ = return () write (x:xs) n = do putStrLn $ (show n) ++ ". " ++ x write xs (n+1) -- Vypise radky na vystup, ktere jsou v obou souborech, ve stejnem poradi. copyOut file1 file2 = do h1 <- openFile file1 ReadMode h2 <- openFile file2 ReadMode c1 <- hGetContents h1 c2 <- hGetContents h2 putStr $ unlines $ [x | x <- lines c1, y <- lines c2, x == y] hClose h1 hClose h2 -- Nacte radek a slova vypise v opacnem poradi. reverseOut = do line <- getLine if null line then return () else do putStrLn $ rev line reverseOut where rev l = unwords $ foldl (\acc x -> x : acc) [] (words l)
Structural induction, Standard Prelude
foldr :: (a -> b -> b) -> b -> [a] -> b foldr f z [] = z foldr f z (x:xs) = f x (foldr f z xs)
foldl :: (a -> b -> a) -> a -> [b] -> a foldl f z [] = z foldl f z (x:xs) = foldl f (f z x) xs
map :: (a -> b) -> [a] -> [b] map f [] = [] map f (x:xs) = f x : map f xs
(++) :: [a] -> [a] -> [a] [] ++ ys = ys (x:xs) ++ ys = x : (xs ++ ys)
take :: Int -> [a] -> [a] take n _ | n <= 0 = [] take _ [] = [] take n (x:xs) = x : take (n-1) xs
drop :: Int -> [a] -> [a] drop n xs | n <= 0 = xs drop _ [] = [] drop n (_:xs) = drop (n-1) xs
head :: [a] -> a head (x:_) = x head [] = error "Prelude.head: empty list"
tail :: [a] -> [a] tail (_:xs) = xs tail [] = error "Prelude.tail: empty list"
last :: [a] -> a last [x] = x last (_:xs) = last xs last [] = error "Prelude.last: empty list"
init :: [a] -> [a] init [x] = [] init (x:xs) = x : init xs init [] = error "Prelude.init: empty list"
length :: [a] -> Int length [] = 0 length (_:l) = 1 + length l
filter :: (a -> Bool) -> [a] -> [a] -- filter p xs = [x | x <- xs, p x] filter p [] = [] filter p (x:xs) | p x = x : filter p xs | otherwise = filter p xs