Lambda calculus, Church encoding, http://safalra.com/science/lambda-calculus

• α-konverze – λx.xy →_α λz.zy, substituce¹⁾
• β-konverze – (λxz.xz)(xy) →_β λz.xyz, aplikace funkce
• η-konverze – λx.(uv)x →_η uv

<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

• Learn You a Haskell for Great Good!
• Gist

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

takeWhile               :: (a -> Bool) -> [a] -> [a]
takeWhile p []          =  []
takeWhile p (x:xs) 
            | p x       =  x : takeWhile p xs
            | otherwise =  []

dropWhile               :: (a -> Bool) -> [a] -> [a]
dropWhile p []          =  []
dropWhile p xs@(x:xs')
            | p x       =  dropWhile p xs'
            | otherwise =  xs

P-99: Ninety-Nine Prolog Problems