Lambda calculus, Church encoding
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.xT y | λxy.y(λz.T )x | λab.aT (λr.b) | λxy.xT y |
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
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
zipWith :: (a->b->c) -> [a]->[b]->[c] zipWith z (a:as) (b:bs) = z a b : zipWith z as bs zipWith _ _ _ = []