grundy number
grundy number について知ったのでメモ．
これは
ある完全情報ゲームについて，両プレイヤーが勝つために最善の状態遷移を選択したとき，与えられた初期状態から先手が勝つか後手が勝つかを答えよ．
というような問題を解くときに使えるかもしれない考え方．
基本的に Algorithm Tutorials しか参考にしていないので，これくらいの英語なら特に苦労せずに読める人はこっちを読んだほうがいいと思います…
Nim
まずそのようなゲームの代表例として Nim というゲームについて考える．
ニム - Wikipedia
最後に必勝法として触れられているように，Nim は各山のコインの枚数をそれぞれ a[1], ..., a[n] とすると，X = a[1] ^ a[2] ^ ... ^ a[n] として，X != 0 のときに限り先手必勝であることが知られている．
このようなゲームにおいて，状態は大きく2つに分けることができる．
- losing: どうがんばっても相手がうまくプレイすると負ける状態
- winning: うまくプレイすると相手がどうがんばろうとも勝てる状態
言い換えると，
- losing: どうがんばっても winning にしか遷移できない
- winning: うまく手を選ぶと losing に遷移できる
となる．よって，初期状態が losing か winning かを判定できれば，先手が勝つか後手が勝つかわかるということになる．
ではなぜ X == 0 だと losing で，逆に X != 0 だと winning であるか．
X == 0 だと losing
X == 0 の状態で自分の番が回ってきたときを考える．
自分はどれかの山から1枚以上のコインを取り除かなければならないので，取り除いた後の X は必ず 0 以外になる．
X != 0 だと winning
X != 0 の状態で自分の番が回ってきたときを考える．
X の立っているビットのうち最上位のビット(これを k ビット目とする)に注目し，k ビット目が立っている山の一つ(これを i とする)を選び，プレイヤーはここからコインをとる．a[i] からは好きな数だけ引くことができるので，うまく引く数を選ぶことで k ビット目を 0 にしつつ，任意の j (< k) ビット目を任意に変えることができる．よって，a[i] からうまく引くことで X を 0 にできる．
よって，どこか不思議なかんじがするが，xor によって先手必勝か後手必勝かを初期状態から判定することができる．
grundy number
grundy number というものを用いることで，この考えを Nim 以外にも応用できる．
Nim の性質で xor による判定に関わる重要な点は
- 全部の山が0になったら負け
- 1つの山からしかコインを取れない
- 1つの山から1以上の好きな数だけ引ける
というようなものだった．
これらを保持するために，grundy number を
「ある状態の grundy number が n」 := 「その状態から n 未満の任意の i (>= 0) について，grundy number が i であるような状態に遷移できる」
となるようにつける．最終状態の grundy number は 0 になる．
例題として，TopCoder のと一緒だとつまらないのでほぼ同じような POJ の問題を解いてみる．
頂点数 N の DAG が与えられ，M 個の駒がそれぞれどこかの頂点に置かれている．プレイヤーは1ターンに1つの駒を有向辺に沿って隣りの頂点に動かす．どの駒も動かせなくなったプレイヤーの負け．N <= 1000, M <= 10
というような問題．
これはある駒に注目すると(Nim の「山」に相当する)，上の定義に従って頂点 x の grundy number を
int memo[1000]; Graph g; int grundyNumber(int x) { int& n = memo[x]; if (n != -1) { return n; } bool s[1000]; fill_n(s, 1000, false); for (int y : g.nodes_from(x)) { s[grundyNumber(y)] = true; } for (n = 0; s[n]; ++n); return n; }
というようなかんじのメモ化再帰で求めることができる．すると，最初の駒の位置が x[1], ..., x[M] のとき，grundyNumber(x[1]) ^ ... ^ grundyNumber(x[M]) == 0 のときに "LOSE"，そうでないときは "WIN" と答えればよい．
類題: 2311 -- Cutting Game
ちょっと工夫は必要だが，これも grundy number を利用して解ける．
ランタイムに失敗しないインデックス演算子
前回の発展のようなかんじで，GADT を用いて型レベル自然数同士の大小関係を表現する項を作れるようにし，「n が m より小さい」ことを示す項と Vec m a を受け取って n 番目の要素を返す関数を定義してみた．
例によって一度ランタイムに compare して LT, GT, EQ のいずれかの Ordering を得て，LT のときのみ (!!) 関数に渡せるようになっている．
しかしなんか全体的に冗長な実装になっているような気がする… LtZ と LtS の2つに対して同じようなものを書いていたりとか．
{-# LANGUAGE GADTs, Rank2Types #-} import Prelude hiding (Ordering, Eq, compare, length, (!!)) data Z = Z data S n = S n data LT = LT data GT = GT data EQ = EQ data Ordering n m o where EqZ :: Ordering Z Z EQ EqS :: (Nat n, Nat m) => Ordering n m EQ -> Ordering (S n) (S m) EQ LtZ :: Nat m => S m -> Ordering Z (S m) LT LtS :: (Nat n, Nat m) => Ordering n m LT -> Ordering (S n) (S m) LT GtZ :: Nat n => S n -> Ordering (S n) Z GT GtS :: (Nat n, Nat m) => Ordering n m GT -> Ordering (S n) (S m) GT data SomeOrdering n m = forall o. SomeOrdering (Ordering n m o) data IsZero n where IsZero :: IsZero Z NotZero :: Nat n => S n -> IsZero (S n) class Nat n where toInt :: n -> Int isZero :: n -> IsZero n compare :: Nat m => n -> m -> SomeOrdering n m instance Nat Z where toInt _ = 0 isZero _ = IsZero compare _ m = case isZero m of IsZero -> SomeOrdering EqZ NotZero _ -> SomeOrdering $ LtZ m instance Nat n => Nat (S n) where toInt ~(S n) = 1 + toInt n isZero n = NotZero n compare ~(S n) m = case isZero m of IsZero -> SomeOrdering $ GtZ (S n) NotZero ~(S m') -> case compare n m' of SomeOrdering o@(LtZ _) -> SomeOrdering (LtS o) SomeOrdering o@(LtS _) -> SomeOrdering (LtS o) SomeOrdering o@(GtZ _) -> SomeOrdering (GtS o) SomeOrdering o@(GtS _) -> SomeOrdering (GtS o) SomeOrdering EqZ -> SomeOrdering (EqS EqZ) SomeOrdering o@(EqS _) -> SomeOrdering (EqS o) reifyInt :: Int -> (forall n. Nat n => n -> a) -> a reifyInt 0 k = k Z reifyInt n k = reifyInt (n-1) $ \m -> k (S m) data Vec n a where Nil :: Vec Z a (:::) :: Nat n => a -> Vec n a -> Vec (S n) a toList :: Vec n a -> [a] toList Nil = [] toList (x ::: xs) = x : toList xs fromList :: [a] -> (forall n. Nat n => Vec n a -> b) -> b fromList [] k = k Nil fromList (x:xs) k = fromList xs $ \xs' -> k (x ::: xs') length :: Vec n a -> n length Nil = Z length (_ ::: xs) = S (length xs) (!!) :: (Nat n, Nat m) => Vec m a -> Ordering n m LT -> a (x ::: _) !! (LtZ _) = x (_ ::: xs) !! (LtS o) = xs !! o _ !! _ = error "should not happen!" main :: IO () main = do xs <- readLn :: IO [Int] x <- readLn :: IO Int reifyInt x $ \n -> fromList xs $ \ls -> case compare n (length ls) of SomeOrdering o@(LtZ _) -> print $ ls !! o SomeOrdering o@(LtS _) -> print $ ls !! o _ -> putStrLn "out of range!"
ランタイムのチェックを一度で済ます
http://d.hatena.ne.jp/Lost_dog/20111128/1322504143
reify_integer がおもしろいなーと思った．
これと同じ雰囲気で， dependent type の例によく出てくる「長さ n のベクトル型 Vec n a」についてこんなのが書けそう．
同じ長さ n のベクトル同士だけ zipWith．長さが異なるベクトル同士だと型が合わずにコンパイルエラー．長さが等しいことは sameLength でランタイムにチェックすることができて，一度チェックすればそれ以降は型で保証される．
{-# LANGUAGE Rank2Types, GADTs, EmptyDataDecls #-} import Prelude hiding (zipWith, foldl) import Control.Applicative ((<$>)) data Z data S n data Vec n a where Nil :: Vec Z a (:::) :: a -> Vec n a -> Vec (S n) a toList :: Vec n a -> [a] toList Nil = [] toList (x ::: xs) = x : toList xs fromList :: [a] -> (forall n. Vec n a -> b) -> b fromList [] k = k Nil fromList (x:xs) k = fromList xs $ \ys -> k (x ::: ys) sameLength :: Vec n a -> Vec m b -> Maybe (Vec n b) sameLength Nil Nil = Just Nil sameLength (_ ::: xs) (y ::: ys) = (y :::) <$> sameLength xs ys sameLength _ _ = Nothing zipWith :: (a -> b -> c) -> Vec n a -> Vec n b -> Vec n c zipWith _ Nil Nil = Nil zipWith f (x ::: xs) (y ::: ys) = f x y ::: zipWith f xs ys zipWith _ _ _ = error "should not happen!" foldl :: (a -> b -> a) -> a -> Vec n b -> a foldl _ z Nil = z foldl f z (x ::: xs) = foldl f (f z x) xs innerProd :: Num a => Vec n a -> Vec n a -> a innerProd xs ys = foldl (+) 0 $ zipWith (*) xs ys main :: IO () main = do as <- readLn :: IO [Int] bs <- readLn :: IO [Int] fromList as $ \xs -> fromList bs $ \ys -> -- ここで zipWith (,) xs ys とは書けない case sameLength xs ys of Just ys' -> do putStr "zip: " >> print (toList $ zipWith (,) xs ys') putStr "innerProd: " >> print (innerProd xs ys') Nothing -> putStrLn $ "different length..."
実行例
% ./Vec [1,2,3] [4,5,6] zip: [(1,4),(2,5),(3,6)] innerProd: 32 % ./Vec [1,2] [3,4,5] different length...
GHC API を使ってある型コンストラクタのデータコンストラクタを得る
neco-ghc などで，Haskell 用の補完候補をより正確に計算するときに活用できないかなーと思った．
GHC 7.0.3 で試した．
あるモジュールがエクスポートしている名前は modInfoExports でとれる．
そのモジュールで定義されていれば modInfoTyThings で TyThing をとれるけど，例えば aeson の Data.Aeson のように他のモジュールからインポートしたものをエクスポートしている場合，名前は modInfoExports には含まれているけど TyThing が modInfoTyThings に含まれていない，ということが発生する．
なので，modInfoExports で得た名前に関して lookupName で改めて問い合わせて TyThing を得ている．
コンパイルするときは
% ghc -package ghc Browse.hs
と明示的に -package ghc をつけてやる必要がある．
import GHC import GHC.Paths (libdir) import MonadUtils (liftIO) import Name import Data.Maybe (catMaybes) import Control.Applicative ((<$>)) import System.Environment (getArgs) main :: IO () main = do args <- getArgs runGhc (Just libdir) $ do getSessionDynFlags >>= setSessionDynFlags mapM_ browse args browse :: GhcMonad m => String -> m () browse m = do xs <- maybe [] modInfoExports <$> lookupModuleInfo >>= collapseData liftIO $ mapM_ putStrLn xs where lookupModuleInfo = findModule (mkModuleName m) Nothing >>= getModuleInfo collapseData = fmap (map expand . catMaybes) . mapM lookupName . filter (not . isDataConName) where expand (ATyCon ty) = unwords $ (getOccString ty :) $ map getOccString $ tyConDataCons ty expand t = getOccString t
ghc-mod browse との違い
% ghc-mod browse -o Data.Aeson (.:) (.:?) (.=) Array Array Bool DotNetTime DotNetTime Error FromJSON Null Number Object Object Result String Success ToJSON Value encode fromDotNetTime fromJSON json object parseJSON toJSON
% ./Browse Data.Aeson encode json .: .:? .= Array DotNetTime DotNetTime fromDotNetTime FromJSON parseJSON Object Result Error Success ToJSON toJSON Value Object Array String Number Bool Null fromJSON object
型エラーとして FizzBuzz を出力
GHC で以下のコードをコンパイルしようとすると，型エラーとして FizzBuzz 的なものが出力されます．
出力を見やすくしようとして Template Haskell を使ったら比較的最近の GHC でないとコンパイルできなくなってしまった…
手元の GHC (7.0.3) だと OK で，ideone の GHC (6.8.2) だとダメ*1だった．
#define N 30
のところでいくつまで出力するかを決めている．
N を大きくしたら -fcontext-stack の値も大きくしないと別のエラーが出る．
{-# LANGUAGE TypeFamilies, EmptyDataDecls, TypeOperators, UndecidableInstances #-} {-# LANGUAGE TemplateHaskell, CPP #-} {-# OPTIONS_GHC -fcontext-stack=64 #-} import Language.Haskell.TH data Z data S n data Yes data No data Nil data x ::: xs type family a :<= b :: * type instance Z :<= Z = Yes type instance Z :<= S b = Yes type instance S n :<= Z = No type instance S a :<= S b = a :<= b type family a :== b :: * type instance Z :== Z = Yes type instance Z :== S b = No type instance S a :== Z = No type instance S a :== S b = a :== b type family a :- b :: * type instance a :- Z = a type instance S a :- S b = a :- b type Divisible a b = Divisible' (a :<= b) a b type family Divisible' t a b :: * type instance Divisible' Yes a b = a :== b type instance Divisible' No a b = Divisible (a :- b) b data Fizz data Buzz data FizzBuzz #define N 30 type family ToReadable x :: * type instance ToReadable Fizz = Fizz type instance ToReadable Buzz = Buzz type instance ToReadable FizzBuzz = FizzBuzz $( let cls = mkName "ToReadable" f i = let name = mkName ('N' : show i) nat = foldr appT (conT (mkName "Z")) $ replicate i (conT (mkName "S")) in [dataD (cxt []) name [] [] [], tySynInstD cls [nat] (conT name)] in sequence $ concatMap f [1 .. N] ) type ToFizzBuzz n = ToFizzBuzz' (Divisible n (S (S (S Z)))) (Divisible n (S (S (S (S (S Z)))))) n type family ToFizzBuzz' t3 t5 n :: * type instance ToFizzBuzz' No No n = ToReadable n type instance ToFizzBuzz' Yes No n = Fizz type instance ToFizzBuzz' No Yes n = Buzz type instance ToFizzBuzz' Yes Yes n = FizzBuzz type FizzBuzzList n = FizzBuzzList' n n type family FizzBuzzList' n i :: * type instance FizzBuzzList' n Z = Nil type instance FizzBuzzList' n (S i) = (ToFizzBuzz (n :- i)) ::: (FizzBuzzList' n i) class ShowType a where showType :: a main = let _ = showType :: FizzBuzzList $(foldr appT (conT (mkName "Z")) $ replicate N (conT (mkName "S"))) in return ()
出力例:
(snip)
No instance for (ShowType
(N1
::: (N2
::: (Fizz
::: (N4
::: (Buzz
::: (Fizz
::: (N7
::: (N8
::: (Fizz
::: (Buzz
::: (N11
::: (Fizz
::: (N13
::: (N14
::: (FizzBuzz
::: (N16
::: (N17
::: (Fizz
::: (N19
::: (Buzz
::: (Fizz
::: (N22
::: (N23
::: (Fizz
::: (Buzz
::: (N26
::: (Fizz
::: (N28
::: (N29
::: (FizzBuzz
::: Nil)))))))))))))))))))))))))))))))
arising from a use of `showType'
(snip)*1:tySynInstD が無いらしい
ext3 から ext4 へ
パーティションの内容を保持しつつ ext3 から ext4 へのマイグレーション．
今回はルートパーティションの /dev/sda7 について作業した．
基本的には ArchWiki に書いてある通りに．
https://wiki.archlinux.org/index.php/Ext4#Converting_ext3_partitions_to_ext4
適当な Live CD が無かったので Arch のインストールディスクを使った．
# tune2fs -O extents,uninit_bg,dir_index /dev/sda7 # fsck.ext4 -fDp /dev/sda7
fsck でちょっとつまづいたものの，問題無く通った．
/dev/sda7 をマウントできることを確認し，/etc/fstab を書き換えてリブート．
しかしブートの途中でルートパーティションのマウント時に No such device とか言われて失敗して起動できなかった．
ArchWiki の注意書きに
Warning: If the user converted their root (/) partition, a kernel panic may be encountered when attempting to boot. If this happens, simply reboot using the 'fallback' initial ramdisk and re-create the 'default' initial ramdisk: mkinitcpio -p linux
とあって，これっぽいかんじだった．
fallback のほうだとたしかに起動できたので，
# mkinitcpio -p linux # mkinitcpio -p linux-pae # linux-pae を入れている場合
で作り直した後，通常通りに起動できることを確認した．
あとは extent を有効にするために chattr +e するとか．
プログラミングコンテストの記録
そういえばこんなかんじにネタバレを書いてます．
http://eagletmt.github.com/contests/
POJ, AOJ を中心に，AC したコード + 簡単な解法の説明．
今のところ POJ 200問くらいと，AOJ 30問くらいを書いてる．
まぁ自分の実力は高くないので，どれくらいの人に役立つか謎ですが…
(※ 2011-11-02 に書き直しました)
