2009-01-09
■ Haskellで自分の足を撃つ方法(抜粋/意訳) 
(http://www.haskell.org/haskellwiki/Shooting_your_self_in_the_foot)
- あなたは銃を発射した。しかし銃弾はIOモナドにからめとられた。
- プログラムをコンパイルしようとしたら、コンパイラが型エラーを発生させ、それはカーネルバッファをオーバーフローするほど長かったために、トリガーコントロールレジスタを上書きし、足を撃つことになった。
- 型エラーという暗号を解読しようとして、あなたの頭は爆発した。
- 足を撃ったが、何も起きなかった。Haskellの世界では副作用は起きないのだ。
- 足を撃とうとしたが、Gunというdatatypeが無かったため、変わりにArrowを使った。
- 足を撃ったが完全に元気だ。足を評価するまでは。
- 足を撃った。しかしSTM(Software Transactional Memory)モナドのなかにいるので、やりたいことがみつかるまでいつだってやりなおせる。
■ Programming in Haskell Exercises
Chapter 11
- Redefine the combination function choices using a list comprehension rather than the library functions concat and map.
choices' xs = [perms x|x <- subs xs]
- Define a recursive function isChoice::Eq a=>[a]->[a]->Bool that decides if one list is chosen from another,without using the combinatorial functions perms and subs,Hint:start by defining a function that removes the first occurrence of a value from a list.
isChoice [] ys = True isChoice (x:xs) ys = elem x ys && isChoice xs (deleteFirst x ys) deleteFirst x [] = error $ (show x)++" does not exsist." deleteFirst x (y:ys) |x == y = ys |otherwise = y:deleteFirst x ys
- What effect would generalizing the function split to also return pairs containing the empty list have on the behavior of solutions?
意味がわからず。solutions以前にexprsの評価において、要素を減らさずに再帰するので、無限ループになると思われる。
- Using choices,exprs,and eval,verify that there are 33,665,406 possible expressions over the numbers 1,3,7,10,25,50,and that only 4,672,540 of these expressions evaluate successfully.
*Main> length $ [y|xs<-choices [1,3,7,10,25,50],y<-exprs xs] 33665406 *Main> length $ [z|xs<-choices [1,3,7,10,25,50],y<-exprs xs,z<-eval y] 4672540
- Similarly,verify that the number of expressions that evaluate successfully increases to 10,839,369 if the numeric domain is generalised to arbitrary integers.Hint:modify the definition of valid.
Main> length $ [z|xs<-choices [1,3,7,10,25,50],y<-exprs xs,z<-eval y] 10839369
- Modify the final program to:
- allow the use of exponentiation in expressions:
- produced the nearest solutions if no exact solution is possible
- order the solutions using a suitable measure of simplicity
import Data.List import Data.Ord data Op = Add | Sub | Mul | Div | Exp deriving Enum apply :: Op -> Int -> Int -> Int apply Add x y = x + y apply Sub x y = x - y apply Mul x y = x * y apply Div x y = x `div` y apply Exp x y = x ^ y data Expr = Val Int | App Op Expr Expr values :: Expr -> [Int] values (Val n) = [n] values (App _ l r) = values l ++ values r subs :: [a] -> [[a]] subs [] = [[]] subs (x:xs) = yss ++ map (x:) yss where yss = subs xs interleave :: a -> [a] -> [[a]] interleave x [] = [[x]] interleave x (y:ys) = (x:y:ys) : map (y:) (interleave x ys) perms :: [a] -> [[a]] perms [] = [[]] perms (x:xs) = concat (map (interleave x) (perms xs)) choices :: [a] -> [[a]] choices xs = concat (map perms (subs xs)) split :: [a] -> [([a],[a])] split [] = [] split [_] = [] split (x:xs) = ([x],xs) : [(x:ls,rs) | (ls,rs) <- split xs] valid :: Op -> Int -> Int -> Bool valid Add x y = x <= y valid Sub x y = x > y valid Mul x y = x /= 1 && y /= 1 && x <= y valid Div x y = y /= 1 && x `mod` y == 0 valid Exp x y = x /= 1 && y /= 1 type Result = (Expr,Int) results :: [Int] -> [Result] results [] = [] results [n] = [(Val n,n) | n > 0] results ns = [res | (ls,rs) <- split ns , lx <- results ls , ry <- results rs , res <- combine lx ry] combine :: Result -> Result -> [Result] combine (l,x) (r,y) = [(App o l r, apply o x y) | o <- [(Add)..(Exp)] , valid o x y] solutions :: [Int] -> Int -> [Expr] solutions ns n = let evals = evaluations ns n correct = sortBy (comparing values) $ map fst $ filter (\x->snd x==0) evals nearest = fst $ minimumBy (comparing snd) evals in if null correct then [nearest] else correct evaluations :: [Int] -> Int -> [Result] evaluations ns n = [(e,abs(m-n))| ns' <- choices ns ,(e,m) <- results ns']
Chapter 12
=Identify the redexes inthe following expressions,and determine whether each redex is inner most,outer most,neigher,or both.
- 1+(2*3)
1+(2*3):outermost (2*3):innermost
- (1+2)*(2+3)
(1+2)*(2+3):outermost (1+2):innermost (2+3):innermost
- fst (1+2,2+3)
fst (1+2,2+3):outermost (1+2):innermost (2+3):innermost
(\x->1+x)(2*3):outermost (2*3):innermost
- Show why outermost evaluation is preferable to innermost for thepurposes of evaluating the expression fst (1+2,2+3).
innermost evaluationの場合 fst(1+2,2+3) ->fst(3,2+3) ->fst(3,5) ->3 outermost evaluationの場合 fst(1+2,2+3) ->1+2 ->3 となり簡約のステップが減る。
- Given the definiton mult = \x->(\y-> x* y),show how the evaluation of mult 3 4 can be broken dwon into four separate steps
mult 3 4 ->(\x->(\y-> x* y)) 3 4 ->(\y-> 3 * y) 4 ->3 * 4 ->12
- Using a list comprehension,define an expression fibs::[Integer] that generates the infinite sequences of Fibonacchi numbers 0,1,1,2,3,5,8,13,21,34... using the following simple procedure:(Hint:make use of library functions zip and tail.Note that numbers in the Fibonacci sequence quickly large,hence the use of the type Integer of arbitrary-precision integers above.
よくわからず。
題意を満たしてないがとりあえず。
fibs = 0:1:zipWith(+)fibs (tail fibs)
もしかして
fibs = 0:1:[f+s|(f,s)<-zip fibs (tail fibs)]
これでいいんだろうか。
- Using fibs,defina a function fib::Int->Integer that returns the nth Fibonacchi number(counting from zero),and an expression that calculates the first Fibonacchi number greater than one thousand.
fib n = fibs !! n head $ dropWhile (<=1000) fibs
- Define appropriate version of the library functions
repeat::a -> [a] repeat x = xs where xs = x :xs take::Int->[a]->[a] take 0 _ = [] take (n+1) [] = [] take (n+1) (x:xs) = x : take n xs replicate::Int->a->[a] replicate n = take n . repeat
for the following type of binary trees
data Tree a = Leaf|Node (Tree a) a (Tree a)
repeatTree x = Node (repeatTree x) x (repeatTree x) takeTree 0 _ = Leaf takeTree _ [] = Leaf takeTree n (Node left x right)= Node (takeTree (n-1) left) x (takeTree (n-1) right) replicateTree n = takeTree n.repeatTree
Chapter 13
- Give an example of a function from the standard library in appendix A that is defined using overlapping patterns.
last [x] = x last (_:xs) = last xs
前者の定義がなければ、シングルトンリストは後者にもマッチしうる。
- Show that add n (Succ m) = Succ (add n m) by induction on n.
add Zero m = m add (Succ n) m = Succ(add n m)
n = Zeroのとき
左辺=add Zero (Succ m)={applying add} Succ m
右辺=Succ(add Zero m) ={applying add} Succ m
よって成り立つ
n = kのとき、つまり
add k (Succ m) = Succ (add k m)が成りたつとすると、
add (Succ k) (Succ m) = Succ (add (Succ k) m)が成りたつことを証明する。
左辺=add (Succ k) (Succ m)={applying add}Succ (add k (Succ m)
右辺=Succ (add (Succ k) m)={applying add}Succ (Succ (add k m)
ここで、add k (Succ m) = Succ (add k m)なので成りたつ。 q.e.d
- Using this property,together with add n Zero = n,show the addition is communtative,add n m = add m n,by induction on n
仮定：
add Zero m = m -- (1)
add (Succ n) m = Succ(add n m) -- (2)
add n (Succ m)= Succ(add n m) -- (3)
add n Zero = n -- (4)
結論：
add n m = add m n
証明:
*base case
add Zero m = add m Zeroを証明する。
左辺=add Zero m ={using 1} m
右辺=add m Zero ={using 4} m
*inductive case
add k m = add m k -- (ih) Induction Hypothesis
を使って
add (Succ k) m = add m (Succ k)を証明する.
左辺=add (Succ k) m ={using 2} Succ (add k m) = {using ih} Succ (add m k)
右辺=add m (Succ k) ={using 3} Succ (add m k)
q.e.d.
- Using the following definition for the library function that decides if all elements of a list satisfy a predicate,complete the proof of the correctness of replicate by showing that it produces a list with identical elements,all(==x)(replicate n x),by induction on n >= .Hint:show that the property is always True.
all p [] = True all p (x:xs) = p x && all p xs
仮定: replicate 0 _ = [] -- (1) replicate (n+1) x = x:replicate n x -- (2) all p [] = True -- (3) all p (x:xs) = p x && all p xs -- (4) 結論: all(==x) (replicate n x) は常にTrue 証明: *base case all(==x) (replicate 0 x) ={using 1} all (==x) [] ={using 3} True *inductive case 「all(==x) (replicate k x) は常にTrue」-- (ih) を使ってall(==x) (replicate (k+1) x)は常にTrueを証明する。 all (==x) (replicate (k+1) x) ={using 2} all (==x) (x:replicate k x) ={using 4} (==x) x && all (==x) replicate k x =(applying (==x)} True && all (==x) replicate k x ={appying &&} all (==x)replicate k x ={using ih} True q.e.d
- Using the definition
[] ++ ys = ys -- (1) (x:xs) ++ ys = x :(xs++ys) -- (2)
verify the following two properties,by induction on xs:
xs ++ [] = xs xs ++ (ys ++ zs) = (xs ++ ys) ++ zs
xs ++ [] = xsを証明する
*base case
[] ++ [] = []
*inductive case
(x:xs)++ [] ={using 1} x:(xs++[])={using ih} x:xs
q.e.d.
xs ++ (ys ++ zs) = (xs++ ys) ++ zsを証明する。
*base case
[] ++ (ys ++ zs) ={using 1} ys ++ zs
([]++ ys )++ zs ={using 1} ys ++ zs
*inductive case
(x:xs)++(ys++zs) ={using 2} x:(xs++(ys++zs)) = {using ih} x:((xs++ys)++zs)
((x:xs)++ ys) ++ zs ={using 2} (x:(xs++ys)) ++ zs = {using 2} x:((xs++ys)++zs)
q.e.d.
- The equation reverse(reverse xs) = xs can also be probed using a single auxiliary result,result reverse (xs ++[x])=x:reverse xs,which can itself be verified by induction on xs.Why might the proof using three auxiliary results as in this chapter be viewed as preferable?
よくわからないので、とりあえず証明してみる。
仮定
reverse [] = [] --(1)
reverse (x:xs) = reverse xs++[x] --(2)
reverse (xs ++[x]) = x:reverse xs --(3)
証明
*base caseは省略
*inductive case
reverse (reverse (x:xs))
={using 2} reverse (reverse xs ++ [x])
={using 3} x:reverse(reverse (xs))
={using ih} x:xs
次にreverse (xs ++[x]) = x:reverse xs を証明する。
仮定
reverse [] = [] --(1)
reverse (x:xs) = reverse xs++[x] --(2)
[] ++ ys = ys --(4)
(x:xs) ++ ys = x:(xs++ys) --(5)
*base case
reverse ([] ++ [x])
={using 4} reverse [x]
={using 2} reverse [] ++ [x]
={using 1} [] ++ [x]
={using 4} [x]
x:reverse []
={using 1} x:[]
={syntax sugar} [x]
*inductive case
reverse ((x:xs)++[y])
={using 5} reverse(x:(xs++[y])
={using 2} reverse (xs++[y]) ++ [x]
={using ih} y:reverse xs ++ [x]
y:reverse(x:xs)
={using 2} y:(reverse xs++[x])
={unapplying 5} y:(reverse xs) ++[x]
証明はできた。結局理由はわからない。
- Using the definitoons
map f [] = [] -- (1) map f (x:xs) = f x:map f xs -- (2) (f.g) x = f (g x) -- (3)
show that map f (map g xs) = map (f.g) xs by induction on xs.
*base case
map f (map g [])
={using 1} map f []
={using 1} []
map (f.g) []
={using 1 []
*inductive case
map f(map g (x:xs))
={using 2} map f (g x:map g xs)
={using 2} f (g x):map f (map g xs)
map (f.g) (x:xs)
={using 2} (f.g) x:map (f.g) xs
={using 3} f (g x):map (f.g) xs
={using ih} f (g x):map f (map g xs)
- Using the definition for ++ given above,together with
take 0 _ =[] take (n+1) [] =[] take (n+1) (x:xs)=x:take n xs drop 0 xs =xs drop (n+1) [] =[] drop (n+1) (_:xs)=drop n xs
show that take n xs ++ drop n xs == xs,by simultaneous induction on the integeer n>= 0 and the list xs. Hint:there are three cases,one for each pattern of arguments in the definition of take and drop
仮定
take 0 _ =[] --(1)
take (n+1) [] =[] --(2)
take (n+1) (x:xs)=x:take n xs --(3)
drop 0 xs =xs --(4)
drop (n+1) [] =[] --(5)
drop (n+1) (_:xs)=drop n xs --(6)
[] ++ ys = ys --(7)
(x:xs) ++ ys = x:(xs++ys) --(8)
*base case
n = 0のとき
take 0 xs ++ drop 0 xs ={using 1}[] ++ drop 0 xs={using 4} [] ++ xs ={using 7}xs
xs = []のとき
take n [] ++ drop n [] ={using 2} [] ++drop n []={using 5} [] ++ [] ={using 7} []
*inductive case
take k xs ++ drop k xs == xsのとき --(ih)
take (k+1) (x:xs)++drop (k+1) (x:xs)
={using 3} (x:take k xs)++drop (k+1) (x:xs)
={using 6} (x:take k xs)++drop k xs
={using 8} x:(take k xs ++ drop k xs)
={using ih} x:xs
自然数nと要素数m個のリストについて、
n>mならば (n-m,m-m)=(n-m,0)がbase caseとなり
n<=mならば(n-n,m-n)=(0,m-n)がbase caseとなるので、常に成立する。
- Given the type declaration "data Tree = Leaf Int|Node Tree Tree" show that the number of leaves in such a tree is always one greater than the numbe rof nodes,by induction on trees.Hint:start by defining functions that count the number of leaves and nodes in a tree.
data Tree = Leaf Int|Node Tree Tree deriving Show t1 = Node (Leaf 3) (Node (Leaf 5) (Leaf 6)) t2 = Leaf 3 t3 = Node (Node (Node (Leaf 4) (Leaf 8)) (Leaf 3)) (Node (Leaf 4) (Leaf 2)) countLeaves::Tree->Int countLeaves (Leaf _) = 1 countLeaves (Node left right)= countLeaves left + countLeaves right countNodes::Tree->Int countNodes (Leaf _) = 0 countNodes (Node left right) = 1 + countNodes left + countNodes right
実行結果
*Main> countLeaves t1 3 *Main> countLeaves t2 1 *Main> countLeaves t3 5 *Main> countNodes t1 2 *Main> countNodes t2 0 *Main> countNodes t3 4
証明する
仮定：
countLeaves (Leaf _) = 1 --(1)
countLeaves (Node left right)= countLeaves left + countLeaves right --(2)
countNodes (Leaf _) = 0 --(3)
countNodes (Node left right) = 1 + countNodes left + countNodes right --(4)
結論：
countLeaves tree = countNodes tree + 1
証明:
*base case
countLeaves (Leaf leaf) = 1
countNodes (Leaf leaf) = 0
*inductive case
countLeaves left = countNodes left + 1 --(ih-1)
countLeaves right= countNodes right+ 1 --(ih-1)
を仮定する。
countLeaves (Node left right)
={using 2)countLeaves left + countLeaves right
={using ih-1,ih-2}countNodes left + 1 + countNodes right + 1
countNodes (Node left right)
={using 4}1 + countNodes left + countNodes right
- Given the equation comp' e c = comp e ++ c,show how to construct the recursive definition for comp',by induction on e.
comp (Val n) = [PUSH n] comp (Add x y) = comp x ++ comp y ++ [ADD] comp' (Val n) c =comp (Val n) ++ c =[PUSH n]++c =PUSH n:c comp' (Add x y) c =comp (Add x y) ++ c =comp x ++ comp y ++ [ADD] ++ c =comp x ++ (comp y ++ ([ADD] ++ c)) =comp' x (comp y ++ ([ADD] ++ c)) =comp' x (comp' y ([ADD] ++ c)) =comp' x (comp' y (ADD:c)) comp' (Val n) c = PUSH n:c comp' (Add x y) c = comp' x (comp' y (ADD:c))
コメントを書く
Patience2012/01/08 13:13This is the perfcet way to break down this information.
hyetlrtk2012/01/09 03:03T76K7x <a href="http://gndgrqeiuiyj.com/">gndgrqeiuiyj</a>
hhpdahd2012/01/09 20:46UlfWue , [url=http://vyqauabetkei.com/]vyqauabetkei[/url], [link=http://irtuwgunyrnf.com/]irtuwgunyrnf[/link], http://fuejlwudquxd.com/
