Lambda calculus, Church encoding
| T | λxy.x | λxy.xy | λxy.x | λxy.x | 
|---|---|---|---|---|
| F | λxy.y | λxy.y | λxy.yx | λxy.xy | 
| NOT | λx.x FT | λx.x(λz. F)T | λp.p F(λr.T) | λx.x FT | 
| AND | λxy.xy F | λxy.y(λz.x) F | λab.ab(λr. F) | λxy.xy F | 
| OR | λxy.x Ty | λxy.y(λz. T)x | λab.a T(λr.b) | λxy.x Ty | 
| XOR | λxy.x( NOTy)y | λxy.x(λz.( NOTy))y | λxy.x( NOTy)(λz.y) | λxy.x( NOTy)y | 
| EQ | λxy.xy( NOTy) | λxy.x(λz.y)( NOTy) | λxy.xy(λz.( NOTy)) | λxy.xy( NOTy) | 
<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 _ _ _ = []