haskell

猫とC#について書く代わりにHaskellについて書くmatarilloの日記

2012-02-21

第10章型とクラスの定義 #3

19:57 |

10.4 恒真式

命題論理式を表す型を作り、与えられた命題が恒真式（式に含まれる変数の値に関係なく、常に真となる式）かどうかを判定する関数を書く。

まずは命題の型を定義。

真理値(True, False): Const Bool
変数(A, B, ... , Z): Var Char
否定(￢): Not Prop
論理積(∧): And Prop Prop
論理包含(⇒): Imply Prop Prop

data Prop = Const Bool
  | Var Char
  | Not Prop
  | And Prop Prop
  | Imply Prop Prop

変数名を真理値に対応付ける置換表を定義して、与えられた置換表を元に命題の値を評価する関数も書く。

type Subst = Assoc Char Bool

eval               :: Subst -> Prop -> Bool
eval _ (Const b)   =  b
eval s (Var x)     =  find x s
eval s (Not p)     =  not (eval s p)
eval s (And p q)   =  eval s p && eval s q
eval s (Imply p q) =  eval s p <= eval s q

命題の中から変数（重複あり）を抽出する関数は

vars             :: Prop -> [Char]
vars (Const _)   =  []
vars (Var x)     =  [x]
vars (Not p)     =  vars p
vars (And p q)   =  vars p ++ vars q
vars (Imply p q) =  vars p ++ vars q

変数の数に対応して、とり得る真理値の組み合わせを列挙する関数は

bools   :: Int -> [[Bool]]
bools 0 = [[]]
bools n = map (False:) bss ++ map (True:) bss
          where bss = bools (n-1)

-- bools n =  map (map conv . make n . int2bin) [0..limit]
--   where
--     limit = (2 ^ n) - 1
--     make n bs = take n (bs ++ repeat 0)
--     conv 0 = False
--     conv 1 = True
--     int2bin 0 = []
--     int2bin n = n `mod` 2 : int2bin (n `div` 2)

道具がそろってきたので、命題に含まれる変数がとり得る真理値の組み合わせを置換表にして列挙する関数を定義し、それを使って恒真式の判定関数を書く。

substs   :: Prop -> [Subst]
substs p =  map (zip vs) (bools (length vs))
            where vs = rmdups (vars p)

isTaut   :: Prop -> Bool
isTaut p =  and [eval s p | s <- substs p]

コメントを書く

2012-02-20

第10章型とクラスの定義 #2

13:50 |

前回の日記でdataによる型定義を学んだけど、これ、もっと掘り下げておくべきだったな。

引数なしのデータコンストラクタだと列挙型みたいなもの。これはOK。たとえば、Bool型の要素がTrueとFalse、といった形でこれまでも登場している。

でも引数ありのデータコンストラクタを持つ型は、これまでになかったものだ。これはCで言えば構造体だし、オブジェクト指向言語でいえばオブジェクトにあたるのだけど、以下が違う。

フィールドには名前がいらない。
名前のないフィールドを参照するときはパターンマッチ（順序で区別する）。

この理解は正しいかな？と思いながらググったら、こんなこともわかった。

データコンストラクタのパターンマッチは、リストのパターンマッチという形ですでに登場していた
フィールドには名前をつけることもできる。

ふむ。教科書にはそこまで書いてないから、先取りしたことになるだろうか。

10.3 再帰型

ここのコード写経ではデータコンストラクタのパターンマッチがたくさん登場する。

まずは、ペアノの公理みたいな自然数定義（ゼロは自然数！）。

教科書ではn+kパターンで書かれていた部分を書き換えてみながら。

（ちなみに、NatをShowクラスのインスタンスにしていないので、hugsやghicでNatを評価するとエラーになってしまう。）

-- rec (Peano axioms)
data Nat = Zero | Succ Nat

nat2int          :: Nat -> Int
nat2int Zero     =  0
nat2int (Succ n) =  1 + nat2int n

int2nat   :: Int -> Nat
int2nat 0 =  Zero
int2nat n =  Succ (int2nat (n-1))
-- n + k pattern
-- int2nat (n + 1) =  Succ (int2nat n)

add            :: Nat -> Nat -> Nat
add Zero n     =  n
add (Succ m) n =  Succ (add m n)

続いて、リスト（コンスセルのリスト）を自分定義。

-- rec (List)
data List a = Nil | Cons a (List a)

len             :: List a -> Int
len Nil         =  0
len (Cons _ xs) =  1 + len xs

最後に、二分木。なお、occurs'関数は二分探索木用の定義。

-- rec (Binary Tree)
data Tree = Leaf Int | Node Tree Int Tree

t :: Tree
t =  Node (Node (Leaf 1) 3 (Leaf 4)) 5 (Node (Leaf 6) 7 (Leaf 9))

occurs                :: Int -> Tree -> Bool
occurs m (Leaf n)     =  m == n
occurs m (Node l n r) =  m == n || occurs m l || occurs m r

flatten              :: Tree -> [Int]
flatten (Leaf n)     =  [n]
flatten (Node l n r) =  flatten l ++ [n] ++ flatten r

occurs' :: Int -> Tree -> Bool
occurs' m (Leaf n) =  m == n
occurs' m (Node l n r)
  | m == n    = True
  | m < n     = occurs' m l
  | otherwise = occurs' m r

おまけで、木構造の定義のバリエーション。

-- data Tree a = Leaf a | Node (Tree a) (Tree a)
-- data Tree a = Leaf | Node (Tree a) a (Tree a)
-- data Tree a b = Leaf a | Node (Tree a b) b (Tree a b)
-- data Tree a = Node a [Tree a]

コメントを書く

2012-02-19

第10章型とクラスの定義 #1

15:36 |

10.1 typeによる型宣言

typeキーワードは型のエイリアスに名前をつける方法。再帰定義はできない。

type Assoc k v = [(k,v)]

find     :: Eq k => k -> Assoc k v -> v
find k t =  head [v | (k',v) <- t, k == k']

newtypeキーワードは教科書に出て来てないなあ。

10.2 dataによる型宣言

dataはデータコンストラクタ（構築子）を並べる型宣言。

下の例だと、Left_、Right_、Up_、Down_が引数なしのデータコンストラクタ。

要するに、型Moveは列挙型ということ。

-- nullary data constructor
type Pos = (Int,Int)
data Move = Left_ | Right_ | Up_ | Down_

move              :: Move -> Pos -> Pos
move Left_ (x,y)  =  (x-1,  y)
move Right_ (x,y) =  (x+1,  y)
move Up_ (x,y)    =  (  x,y-1)
move Down_ (x,y)  =  (  x,y+1)

moves          :: [Move] -> Pos -> Pos
moves [] p     =  p
moves (m:ms) p =  moves ms (move m p)

flip        :: Move -> Move
flip Left_  =  Right_
flip Right_ =  Left_
flip Up_    =  Down_
flip Down_  =  Up_

下の例は、Circleが1引数のデータコンストラクタ、Rectが2引数のデータコンストラクタ。

-- unary/binary data constructor
data Shape = Circle Float | Rect Float Float

square   :: Float -> Shape
square n =  Rect n n

area            :: Shape -> Float
area (Circle r) =  pi * r ^ 2
area (Rect x y) =  x * y

多相型（型引数付き）も定義可能。ここでMaybe aが例に登場。

-- polymorphic data constructor with a type parameter
-- (data Maybe a = Nothing | Just a)
safediv     :: Int -> Int -> Maybe Int
safediv _ 0 =  Nothing
safediv m n = Just (m `div` n)

safehead    :: [a] -> Maybe a
safehead [] =  Nothing
safehead xs =  Just (head xs)

コメントを書く

2012-02-18

第9章対話プログラム #9

19:12 |

9.9 練習問題

練習問題5は「グラフィック・ライブラリを用いて」とか書いてあって面倒なのでパス。Windowsで動かなかったりするし。

ニムはボードを使うゲームである。ボードには、番号の付いた行が五つあり、はじめは星が以下のように並べてある。
```
1:*****
2:****
3:***
4:**
5:*
```
二人のプレイヤーは、交互に行を一つ選び、その最後から一つ以上の星を取る。ボードから最後の星を取った方が勝ちである。ニムをHaskellで実装せよ。
ヒント：それぞれの残っている星の数のリストでボードを定義せよ。ボードの初期値は [5,4,3,2,1] となる。

割と長くなったので解説を入れながら。

まず、入力のところを考える。

入力は"行番号星の数"と入力してEnterを押す仕様にする。

せっかくなのでパーザーモナドを使う。

import Parsing

niminput :: Parser (Int,Int)
niminput =  do
  row <- nat
  space
  count <- nat
  return (row,count)

こんな感じで、パーズに成功したら(行番号,星の数)というタプルを返すことにする。

出力は、9.5の関数を一部使う。

zip関数で(行番号,星の数)というタプルのリストを作って、それぞれを表示する。

import NineFive

type Board = [Int]

display    :: Board -> IO ()
display xs =  seqn $ map displayline $ zip [1..length xs] xs

displayline :: (Int,Int) -> IO ()
displayline (row,count) = do
  putStr (show row ++ ":")
  putStrLn (replicate count '*')

星を取る関数の仕様はちょっと悩んだ。

入力が不正だと星を取れないというロジックを組み込まないといけない。

というわけで、(成否を表す真偽値,結果のボード)のタプルを返すようにしてみた。

Maybeモナドのほうがいいのかもしれないが、まだ教科書には出て来てないからな。

getstars :: Board -> (Int,Int) -> (Bool,Board)
getstars xs (row,count)
  | row == 0              = (False,xs)
  | count == 0            = (False,xs)
  | row > length xs       = (False,xs)
  | xs !! (row-1) < count = (False,xs)
  | otherwise             = (True,take (row-1) xs ++ [xs !! (row-1) - count] ++ drop row xs)

あとはIOモナドでグリグリと表示したり入力したり。

というわけで、回答はこちら。

module NineNineFive where

import Parsing
import NineFive

niminput :: Parser (Int,Int)
niminput =  do
  row <- nat
  space
  count <- nat
  return (row,count)

type Board = [Int]

display    :: Board -> IO ()
display xs =  seqn $ map displayline $ zip [1..length xs] xs

displayline :: (Int,Int) -> IO ()
displayline (row,count) = do
  putStr (show row ++ ":")
  putStrLn (replicate count '*')

getstars :: Board -> (Int,Int) -> (Bool,Board)
getstars xs (row,count)
  | row == 0              = (False,xs)
  | count == 0            = (False,xs)
  | row > length xs       = (False,xs)
  | xs !! (row-1) < count = (False,xs)
  | otherwise             = (True,take (row-1) xs ++ [xs !! (row-1) - count] ++ drop row xs)

turn :: Int -> Board -> IO ()
turn p b
  | all (==0) b = return ()
  | otherwise   = do {display b; input p b}

input :: Int -> Board -> IO ()
input p b = do
  putStr ("Player " ++ show p ++ ": ")
  xs <- getLine
  process p b $ parse niminput xs

process :: Int -> Board -> [((Int,Int),String)] -> IO ()
process p b []      = do {beep; input p b}
process p b [(r,_)] = check p $ getstars b r

check :: Int -> (Bool,Board) -> IO ()
check p (False, b) = do {beep; input p b}
check p (True , b) =
  if all (==0) b then
    putStrLn ("Player " ++ show p ++ " won!")
  else
    turn (chenge p) b

chenge   :: Int -> Int
chenge 1 =  2
chenge 2 =  1

nim :: IO ()
nim =  turn 1 [5,4,3,2,1]

コメントを書く

2012-02-17

第9章対話プログラム #8

14:30 |

9.9 練習問題

ライフゲームのボードを対話的に作成したり、変更したりできるエディターを作れ。

9.7で写経したライフゲームを修正して、ボードサイズを可変にできるようにしてやったぜ。

module NineNineFour where

import System.IO
import NineFive

getCh :: IO Char
getCh =  do hSetEcho stdin False
            c <- getChar
            hSetEcho stdin True
            return c

-- variable size

type Board = [Pos]
type Size  = Pos

showcells   :: Board -> IO ()
showcells b =  seqn [writeat p "O" | p <- b]

isAlive     :: Board -> Pos -> Bool
isAlive b p =  elem p b

isEmpty     :: Board -> Pos -> Bool
isEmpty b p =  not (isAlive b p)

neighbs         :: Size -> Pos -> [Pos]
neighbs s (x,y) =  map (wrap s)
                     [(x-1,y-1), (x,y-1), (x+1,y-1),
                      (x-1,y),            (x+1,y),
                      (x-1,y+1), (x,y+1), (x+1,y+1)]

wrap             :: Size -> Pos -> Pos
wrap (w,h) (x,y) =  (((x-1) `mod` w) + 1, ((y-1) `mod` h) + 1)

liveneighbs      :: Size -> Board -> Pos -> Int
liveneighbs s b  =  length . filter (isAlive b) . neighbs s

survivors     :: Size -> Board -> [Pos]
survivors s b =  [p | p <- b, elem (liveneighbs s b p) [2,3]]

births     :: Size -> Board -> [Pos]
births s b =  [p | p <- rmdups (concat (map (neighbs s) b)),
                   isEmpty b p,
                   liveneighbs s b p == 3]

rmdups        :: Eq a => [a] -> [a]
rmdups []     =  []
rmdups (x:xs) =  x:rmdups (filter ((/=) x) xs)

nextgen     :: Size -> Board -> Board
nextgen s b =  survivors s b ++ births s b

life     :: Size -> Board -> IO ()
life s b =  do
  cls
  showcells b
  wait 5000
  life s (nextgen s b)

wait   :: Int -> IO ()
wait n =  seqn [return () | _ <- [1..n]]

-- board maker

runlife     :: Int -> Int -> IO ()
runlife w h =  makeboard (w,h) [] (1,1)

makeboard       :: Size -> Board -> Pos -> IO ()
makeboard s b p =  do
  cls
  showcells b
  goto p
  c <- getCh
  process s b p c

move                   :: Size -> Pos -> Pos -> Pos
move s (dx,dy) (px,py) =  wrap s (px+dx,py+dy)

up    = ( 0, -1)
down  = ( 0,  1)
right = ( 1,  0)
left  = (-1,  0)

process      :: Size -> Board -> Pos -> Char -> IO ()
process s b p c
  | elem c "\n" = life s b
  | elem c " "  = makeboard s (flippos p b) p
  | elem c "c"  = makeboard s [] p
  | elem c "k"  = makeboard s b (move s up p)
  | elem c "j"  = makeboard s b (move s down p)
  | elem c "h"  = makeboard s b (move s left p)
  | elem c "l"  = makeboard s b (move s right p)
  | otherwise   = makeboard s b p

flippos     :: Pos -> Board -> Board
flippos p b =  if elem p b
               then [q | q <- b, q /= p]
               else p : b

コメントを書く