他人のHaskell日記 RSSフィード

Haskell初心者が、リハビリがてらに「ふつける」と「入門Haskell」片手に、試行錯誤するサイト。

2009-01-09

Haskellで自分の足を撃つ方法(抜粋/意訳) Haskellで自分の足を撃つ方法(抜粋/意訳) - 他人の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  Programming in Haskell Exercises - 他人のHaskell日記 を含むブックマーク

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)
(\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.
    • the first two numbers are 0 and 1
    • the next is the sum of the previous two;
    • return to the second step.

よくわからず。

題意を満たしてないがとりあえず。

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))

PatiencePatience2012/01/08 13:13This is the perfcet way to break down this information.

hyetlrtkhyetlrtk2012/01/09 03:03T76K7x <a href="http://gndgrqeiuiyj.com/">gndgrqeiuiyj</a>

hhpdahdhhpdahd2012/01/09 20:46UlfWue , [url=http://vyqauabetkei.com/]vyqauabetkei[/url], [link=http://irtuwgunyrnf.com/]irtuwgunyrnf[/link], http://fuejlwudquxd.com/