読者です 読者をやめる 読者になる 読者になる

Just $ A sandbox

プログラミングとかPCとかの技術的なメモ

原始帰納的函数で素数を計算

原始帰納函数; prf

原始帰納函数(primitive recursive function; prf)とは, 以下で定義される函数 $ \mathbb{N}^n \to \mathbb{N} $ のこと:

  • 定数函数 $zero : \mathbb{N}^0 \to \mathbb{N}$, 後続函数 $suc : \mathbb{N} \to \mathbb{N}$, 射影函数 $p^n_i : \mathbb{N}^n \to \mathbb{N}$ はprfである
  • prf $f : \mathbb{N}^m \to \mathbb{N}, f_i : \mathbb{N}^n \to \mathbb{N} (1 < i \leq m)$に対し, 合成 $g(\vec{x}) = f(f_1(\vec{x}), \cdots ,f_m(\vec{x}));\; g : \mathbb{N}^n \to \mathbb{N}$ はprfである
  • prf $f : \mathbb{N}^{n} \to \mathbb{N}, h : \mathbb{N}^{n+2} \to \mathbb{N}$に対し, 原始帰納法で定まる函数 $g(0,\vec{x}) = f(\vec{x});\;\; g(y+1,\vec{x})=h(g(y,\vec{x}),y,\vec{x});\;\; g : \mathbb{N}^{n+1} \to \mathbb{N}$ はprfである

n番目の素数を計算するprf $pr : \mathbb{N} \to \mathbb{N}$が定義できることを見る.

準備(自然数, n項直積)

自然数とタプル(長さ付きリスト)といくつかの函数を定義しておく.

data Nat = Z | S Nat deriving (Show)
type N0 = Z
type N1 = S N0
type N2 = S N1
type N3 = S N2
 
type family (+) a b where
  Z + m = m
  (S n) + m = S (n + m)
 
data Tuple n a where
  TEmpty :: Tuple N0 a
  TSuc :: a -> Tuple n a -> Tuple (S n) a
 
instance Functor (Tuple n) where
  fmap f TEmpty = TEmpty
  fmap f (TSuc x xs) = TSuc (f x) (fmap f xs)
 
lengthT :: Tuple n a -> Nat
lengthT TEmpty = Z
lengthT (TSuc _ t) = S (lengthT t)
 
infixr 4 %:
(%:) = TSuc

`Tuple n a`は函数合成を定義するために函数の組を与えるときに使う.
どうせ同じ型の組しか作らないのでこれで十分. 長さ付きにしたのは型チェックのため(後述).

prfの定義

上の定義をそのままGADTで書き下す.
ただし, `PrimRec n`で函数 $\mathbb{N}^n \to \mathbb{N}$を表すことにする. `PrimRec`に「引数の数」という情報を型で持たせることで, 引数の数が合わない場合はコンパイルエラーで弾くことができる.
(e.g. `suc(1,2)`や`add(2)`みたいなものはコンパイルエラーになる)

-- datatype of `p.r. function :: N^p -> N`
data PrimRec p where
  Zero :: PrimRec N0
  Suc :: PrimRec N1
  Proj :: Nat -> PrimRec n
  Comp :: PrimRec m -> Tuple m (PrimRec n) -> PrimRec n
  Induct :: PrimRec n -> PrimRec (S (S n)) -> PrimRec (S n)

infixl 6 %.
(%.) = Comp

prfの実行

さて`PrimRec`を定義したのでprfを宣言できるようになった.
函数を定義したので評価(実行)できるようにしたいということで`evalPR`を定義する.
evalPRは以下のような函数として定義したい.

\[ \begin{eqnarray}
eval(zero,*) &=& 0 \\
eval(suc,n) &=& n+1 \\
eval(p^n_i,\vec{x}) &=& x_i \\
eval(f \circ \{f_i\}_i,\vec{x}) &=& f(f_1(\vec{x}), \cdots f_m(\vec{x})) \\
eval(induction(f,h),0,\vec{x}) &=& f(\vec{x}) \\
eval(induction(f,h),y+1,\vec{x}) &=& h(eval(induction(f,h),y,\vec{x}),y,\vec{x})
\end{eqnarray} \]

ここで, Tupleのi番目を抜き出す操作が必要になるのでそれは別途`(!) :: Tuple n a -> Nat -> a`を定義しておく.

(!) :: Show a => Tuple n a -> Nat -> a
(TSuc n _) ! Z = n
(TSuc _ t) ! (S n) = t ! n
k ! a = error $ show k ++ " ! " ++ show a

evalPR :: PrimRec n -> Tuple n Nat -> Nat
evalPR Zero _ = Z
evalPR Suc (TSuc n TEmpty) = S n
evalPR (Proj k) t = t ! k
evalPR (Comp f fs) xs = evalPR f (go fs xs)
 where
   go :: Tuple m (PrimRec n) -> Tuple n Nat -> Tuple m Nat
   go (TSuc f fs) xs = TSuc (evalPR f xs) (go fs xs)
   go TEmpty xs = TEmpty
evalPR (Induct f h) (TSuc Z xs) = evalPR f xs
evalPR g@(Induct f h) (TSuc (S y) xs) = evalPR h (evalPR g (y %: xs) %: y %: xs)
evalPR _ z = case z of {}

prの構成

素数を計算する函数prを構成する.
まずは準備.

infixr 8 %..
(%..) f x = f %. (x %: TEmpty)
 
extend :: PrimRec N0 -> PrimRec n
extend n = n %. TEmpty
 
arg :: Int -> PrimRec n
arg n = Proj (nat n)
 
one :: PrimRec N0
one = Suc %.. Zero
 
two :: PrimRec N0
two = Suc %.. one

add(x,y)=x+y, pred(x)=x-1, sub(x,y)=if x < y then 0 else x-y, mult(x,y)=x*y
が原始帰納法で定義できる.
(例えば, add(x,0)=x; add(x,y+1)=suc(add(x,y)))

add :: PrimRec N2
add = Induct (arg 0) (Suc %. (arg 0 %: TEmpty))
 
predpr :: PrimRec N1
predpr = Induct Zero (Proj (nat 1))
 
sub :: PrimRec N2
sub = sub' %. (arg 1 %: arg 0 %: TEmpty) where
  sub' = Induct (arg 0) (predpr %. (arg 0 %: TEmpty))
 
mult :: PrimRec N2
mult = Induct (extend Zero) (add %. (arg 2 %: arg 0 %: TEmpty))

次に述語(Bool値をとる函数)を定義する.
今は便宜上, 原始帰納的述語を, {0,1}へのprfとして話を進めることにする.

述語$x=0$,$x=y$,$x \leq y$,$x < y$,not,and,orが定義できる.
(例えば, eq0(x)=sub(1,sub(1,x))とすれば, x=0のときeq0(x)=0, それ以外はeq0(x)=1となる)

equalZ :: PrimRec N1
equalZ = sub %. (extend one %: sub %. (extend one %: arg 0 %: TEmpty) %: TEmpty)
 
equal :: PrimRec N2
equal = equalZ %.. add %. (sub %. (arg 0 %: arg 1 %: TEmpty) %: sub %. (arg 1 %: arg 0 %: TEmpty) %: TEmpty)
 
leq :: PrimRec N2
leq = equalZ %.. sub %. (arg 0 %: arg 1 %: TEmpty)
 
lneq :: PrimRec N2
lneq = andp %. (leq %. (arg 0 %: arg 1 %: TEmpty) %: notp %.. equal %. (arg 0 %: arg 1 %: TEmpty) %: TEmpty)
 
notp :: PrimRec N1
notp = sub %. (extend one %: arg 0 %: TEmpty)
 
andp :: PrimRec N2
andp = equalZ %.. add %. (arg 0 %: arg 1 %: TEmpty)
 
orp :: PrimRec N2
orp = mult %. (arg 0 %: arg 1 %: TEmpty)

次に, $prod_r(y,\vec{x}) = \Pi_{z < y} r(z,\vec{x})$なるprodを定義する.
これを用いて, 原始帰納的述語pに対し, 原始帰納的述語$\exists z < y: p(z,\vec{x})$が定義できる.
同様にして函数$\sum_{z < y} r(z,\vec{x})$や述語$\forall z < y: p(z,\vec{x})$などが定義できる.

さて, ここで初めて可変長の引数を扱う必要が出てくる.
函数prodはprod(r,y,x1..xs)に対しr(z,x1..xs)を掛け算していく函数なので, 受け取った引数の「2番目から最後まで」(=x1..xs)を受け取り, rの0番目にz, 1番目以降にx1..xsを指定して合成する必要がある.
これをするために, $\text{varTuple} :: \text{PrimRec(n)} \to \mathbb{N}^n; \;\; \text{varTuple} _ = (p^n_0, \cdots p^n_{n-1})$なる函数を定義してやれば良さそうに見えるのでこれを定義する.

(varTupleの定義のために手間のかかるハックをしているけれど, もっと綺麗に書けない?)

class VarLenTuple n where
  varLenTuple :: Tuple n Nat
 
instance VarLenTuple Z where
  varLenTuple = TEmpty
 
instance (VarLenTuple n) => VarLenTuple (S n) where
  varLenTuple = Z %: varLenTuple
 
dimDom :: (VarLenTuple n) => PrimRec n -> Nat
dimDom = lengthT . go where
  go :: (VarLenTuple n) => PrimRec n -> Tuple n Nat
  go _ = varLenTuple
 
class VarTuple n where
  varTuple' :: Nat -> Tuple n (PrimRec m)
 
instance VarTuple Z where
  varTuple' _ = TEmpty
 
instance (VarTuple n) => VarTuple (S n) where
  varTuple' (S n) = attach (Proj n) $ varTuple' n

varTuple :: (VarLenTuple n, VarTuple n) => PrimRec n -> Tuple n (PrimRec m)
varTuple = varTuple' . dimDom 

prod :: (VarTuple n, VarLenTuple n) => PrimRec (S n) -> PrimRec (S n)
prod r = Induct (extend one) (mult %. (arg 0 %: r' %: TEmpty)) where
  r' = r %. fmap (mapProj S) (varTuple r)
 
existL :: (VarTuple n, VarLenTuple n) => PrimRec (S n) -> PrimRec (S n)
existL r = equalZ %.. prod r
 
sumpr :: (VarTuple n, VarLenTuple n) => PrimRec (S n) -> PrimRec (S n)
sumpr r = Induct (extend Zero) (add %. (arg 0 %: r' %: TEmpty)) where
  r' = r %. fmap (mapProj S) (varTuple r)
 
forallL :: PrimRec N1 -> PrimRec N1
forallL r = equalZ %.. sumpr r

$prime(x) = x > 1 \land \neg (\exists u < x: \exists v < x: u v = x)$はxが素数であるという述語を表す.
これを定義する.

primep :: PrimRec N1
primep = andp %. (lneq %. (extend one %: arg 0 %: TEmpty) %:
                  notp %.. (existL r' %. (arg 0 %: arg 0 %: TEmpty)) %: TEmpty)
  where
    r' :: PrimRec N2
    r' = existL r'' %. (arg 1 %: arg 0 %: arg 1 %: TEmpty)
 
    r'' :: PrimRec N3
    r'' = equal %. (mult %. (arg 0 %: arg 1 %: TEmpty) %: arg 2 %: TEmpty)

さて, $\mu_{z < y}p(z,\vec{x}) = \min\{z\in \mathbb{N}; z < y \land p(z,\vec{x})\} \cup \{y\}$とおく. この函数はy未満のzで$p(z,\vec{x})$を満たすものの中で最小の数(そのようなものが存在しなければy)を返す函数である.
この函数はprfとして, $\mu_{z < y}p(z,\vec{x}) = \sum_{v < y} g(v,\vec{x}) ; \;\; g(v,\vec{x}) = \exists z\leq v: p(z,\vec{x})$で定義できる.

mu :: (VarTuple n, VarLenTuple n) => PrimRec (S n) -> PrimRec (S n)
mu p = sumpr g %. (varTuple p) where
  f :: Tuple (S n) (PrimRec m) -> Tuple (S n) (PrimRec m)
  f (TSuc x xs) = TSuc (Suc %.. x) xs
 
  g :: (VarTuple n, VarLenTuple n) => PrimRec (S n)
  g = existL p %. (f $ varTuple p)

最後に, 目標だった函数prは,
$pr(0) = 2; pr(n+1) = \mu_{z < pr(x)!+2}(pr(x) < z \land prime(z))$
とすれば得られる.

factorial :: PrimRec N1
factorial = Induct (extend one) (mult %. (arg 0 %: Suc %.. arg 1 %: TEmpty))
 
pr :: PrimRec N1
pr = Induct (extend two) (mu p %. (add %. (extend two %: factorial %.. arg 0 %: TEmpty) %: arg 1 %: TEmpty)) where
  p :: PrimRec N2
  p = andp %. (lneq %. (pr %.. arg 1 %: arg 0 %: TEmpty) %: (primep %.. arg 0) %: TEmpty)

実行

上の函数が正しい挙動をするかどうかを手で検証するのは大変なのでQuickCheckを使った.
なお, 直接実行するとprやfactorialなどはすごく時間がかかる(私のPCだとpr(4)ですでに数分では終わらない)ので本当にこれで正しい出力を返すかどうかは怪しい.

コード全体


参考文献

計算論 計算可能性とラムダ計算 (コンピュータサイエンス大学講座)

計算論 計算可能性とラムダ計算 (コンピュータサイエンス大学講座)

戦略を予約しておくRPGの戦闘システムについて(アイデア)

概要

RPGの戦闘システムとして考えたやつ。

戦闘は普通のターン制。各ターンに1つのアクションが取れる(攻撃・防御・回復 など)。
プレイヤーは戦闘の前に、アクションを並べて作った列をスロットという形で保存しておく。
敵との戦闘時、プレイヤーの作ったスロットからいくつかが手札として与えられ、そのどれかのスロットを選ぶと、スロットに登録されたアクションが実行されて戦闘が進む。

要は、戦闘時に入るパターンとか戦略を予め用意しておいて、それを使って戦う感じのゲーム。

こまかい話

  • 各スロットには長さ(上限)が設定されていて、ゲームが進むとより長いスロットが使えるようになる(複雑な戦略が組める)
  • デッキ(持ち運べるスロット全体)にはスロットの長さの合計に対する上限があって、長いスロットを少し用意するか短いスロットをたくさん用意するか選べる
  • 戦闘開始時、デッキからスロットが決まった数だけランダムに抜き出し手札として与えられる。手札がなくなったら(全てのスロットを1回ずつ使用した上で戦闘が終了しなかったら)無条件で負け。
  • 回復は少し甘めの行動にしておいて、「一番ダメージを負っている仲間1人の体力を回復する」みたいな感じで、必要以上に戦闘のランダム性に左右されない形にする
  • 敵の状態異常(?)の一種として、スロットへ影響を与えるものを用意する。(現在実行中のスロットを破棄する、手札を強制的に選びなおす、次のアクションを飛ばす 等)
  • PCキャラに個性はあってもよいが, 転職などはさせないようにする. 職業を上手く選べば1つの戦略だけで攻略出来てしまうとつまらないから、戦略はあくまでスロット制度の方で賄うことにしたい。
  • スロットに条件分岐的なアクションを挟めるようにしてもいいかもしれない。「誰かが死んでいたら復活させる」+「死んでいなければ攻撃」みたいなのを作れるようにしておくみたいな。
  • スロットによっては、各スロット中で一度だけコマンド選択のターンが与えられるようにする。不測の事態が起こった時の救済措置として。
  • スロットそのものに特別な効果があるものもある。(ときどき2回分行動とか、2回連続の防御で防御率アップとか)

どうでもいい話

つい最近ブレイブリーデフォルトというゲームをやって、そのゲームにあるブレイブ&デフォルトシステムが微妙にこのシステムに似ているような気がした。
あんまりRPGに詳しくないのでこのシステムがすでにあるものなのかどうなのか知らない。あればやりたい。

追記 智代アフターってゲームにはミニゲーム要素で似たようなのがあると教えてもらいました。(智代アフター D&T ゲームの流れ/システム)

もう5年以上も前に考えたアイデアなのでそろそろ供養ということで。

DataKindsとGADTの使い方について

Haskellで型レベルプログラミング(あるいはごく簡単な証明)を書くときに, DataKindsでデータ型をそのまま持ち上げると困る場面がある.

{-# LANGUAGE DataKinds, GADTs, TypeOperators, TypeFamilies #-}

data a :=: b where
  Refl :: a :=: a

data Nat = Zero | Succ Nat

type family (:+:) a b where
  Zero :+: n = n
  (Succ n) :+: m = Succ (n :+: m)

と定義した時, 「任意の自然数nについてn+0=n」を示すにはどうすればよいだろうか.

prop :: (n :: Nat) -> (n :+: Zero) :=: n
prop = undefined

{-
error:
    Expected a type, but ‘n’ has kind ‘Nat’
    In the type signature for ‘prop’:
      prop :: (n :: Nat) -> (n :+: Zero) :=: n
-}

コンパイルが通らない. これは, n :: Natだが(:=:) :: * -> * -> *なので, カインドが合わないと怒られている.

こういう時に, Natの方の定義を工夫して, 上のような命題が表現できるようにしたい.

[追記] コメントで教えてもらったように,

data SNat (n :: Nat) where
  SZ :: SNat Zero
  SS :: SNat n -> SNat (S n)

として, Nat aとする代わりにSNat aとしてやれば上手くいくみたいです。

[/追記]

(Kindに昇格したい)データ型が与えられた時, 以下のような変形を行う.

data Hoge = A a b | B c

↓

data A a b
data B c
data Hoge h where
  A :: a -> b -> Hoge (A a b)
  B :: c -> Hoge (B c)

このとき, Hoge hh :: Hogeのように考えればよい. これによって自然数の例も上手くかける.

data Zero
data Succ n

data Nat n where
  Zero :: Nat Zero
  Succ :: Nat n -> Nat (Succ n)

type family (:+:) a b where
  Zero :+: n = n
  (Succ n) :+: m = Succ (n :+: m)

prop :: Nat a -> (a :+: Zero) :=: a
prop Zero = Refl
prop (Succ n) = case prop n of Refl -> Refl

上のやり方は, GADTの使い方をよく考えれば自然に分かる: 集合AがA := {(x,y)|x ∈ X, y ∈ Y}によって定義される時,

data A a where
  pair :: X -> Y -> A <X,Y>

と置くと, A *型の値全体とAは一致する. pairによって構成される値の型はA <X,Y>となっているが, これはXとYの値((x,y)のこと)を保持する必要があるので直積の形にする.

さらにAがいくつかの集合の和の形にかけているとき, すなわちA := {(x,y)}∪{(z,w)} = A1∪A2のような場合は, Aの元はA1またはA2に入っているので, 上で定義したpair_A1とpair_A2の直和の形にかけていると考えればよい.

data A a where
  pair_1 :: X -> Y -> A <X,Y>
  pair_2 :: Z -> W -> A <Z,W>

あるいはAが帰納的な定義になっている場合(自然数など)の場合も, 全く同様に定義ができる. 自然数の例では, N = {0}∪{succ n | n ∈ N}より,

data Nat n where
  pair_0 :: {*} -> Nat <{*}>
  pair_succ :: Nat n -> Nat <succ n>

となることが分かる.