claustrophobia

一般λがなんか書くとか

プログラムの停止性とRanking関数

大学・大学院時代の研究テーマは、「プログラムの停止性の自動検証」 ー つまり任意の入力に対しプログラムが停止するかを自動で検証する手法についてだったのですが、プログラムの停止性の特徴付けとして有名なものにRanking関数(Ranking function)があります。

Ranking関数とはつまり、関係が定義された構造(Σ, →)から何らかのwell-ordered structure(W, >)への準同型 f のことで、つまり

a,b∈Σ, a→b ⇒  f(a) > f(b)

が成り立つような写像fのことを言います。大体はwell-ordered setとして(N, >)が使われます。

 

プログラムの停止性とRanking関数の関連について、詳しくはByron Cookの資料(サマースクールのテキスト?)が簡潔にまとまっていていい感じです。適当にググれば出てきます。

http://research.microsoft.com/en-us/um/cambridge/projects/terminator/principles.pdf

関連部分だけ軽く説明すると、プログラムを

  1. S: プログラムの状態
  2. R: プログラムの遷移関係
  3. I: 初期状態

の3つ組(S,R,I)で表したとき、プログラムの停止性は「IからRで到達可能な状態(R*(I)と書く)とRからなる構造(R*(I), R)がwell-founded structureである」ことと定義されます。

さて、(R*(I),R)にRanking関数があれば、(S,R,I)が停止することが言えます。なので、停止性検証の主流な手法の一つとして、そのプログラムに対するRanking関数を見つけてやる、という方法があります。

 

で、前々からちょくちょく考えてたのが「逆は成り立つのか?」ということで、つまりプログラムが停止するとき、そのプログラムに対するRanking関数は必ず存在するか?ということです。well-foundedだがwell-orderedでない集合なんていくらでもある訳で(例えば偶奇が異なる数同士は比較できないように制限した自然数の集合とか)実際どうなんだろうなぁと思っていたのですが、どうやら選択公理を仮定すればwell-founded relationからwell-orderedへの拡張は可能なようで:

[1503.06514] On the Well Extension of Partial Well Orderings

ということはつまりプログラムが停止するならばRを拡張して適当なwell orderingにできるということで、停止するプログラムには必ずRanking関数が存在する、ということになります。

あと、一般のwell-founded relationからwell-orderingへの拡張には整列可能定理が要りますが、 要はプログラムの状態の集合に適当な整列順序を一つ定義できればいいので、状態集合が加算なら選択公理も必要ないような気がします。

 

と、いうようなことを悶々と考えていたりしました。なお未だに以下の点が疑問です。

  1. このことに明確に言及した文献はないのか。(絶対にあると思う)
  2. computableな(つまりプログラムとして書き下せる)Ranking関数が見つかるための条件は何か。

誰か何か知ってたら教えて下さい。

Haskellのレコード更新構文を詳しく

スタック・オーバーフローにて


haskell - Text.Parser.Token.StyleのemptyIdentsの使い方について - スタック・オーバーフロー

といった質問をしたところ、このような回答を頂き、レコード更新構文についての詳細を知る必要を感じたので私的まとめ。
といってもほとんどHaskell Language Reportを見ていろいろ実験しただけなんですが。

レコード更新構文の解釈

3.15.3 Updates Using Field Labelsより。

{C}コンストラクタ{bs}を束縛の列、{v_{default}}を値として、{pick^C_i(bs, v_{default})}を次のように定義します:

コンストラクタ{C}{i}番目のフィールドの名前が{f}であり、かつ束縛の列{bs}{f}に関する束縛{f=v_{updated}}が含まれるならば{pick^C_i(bs, v_{default}) = v_{updated}}である。そうでないならば{pick^C_i(bs, v_{default})=v_{default}}である。」

データ型Tを

data T = {C_1} {{f^1_1} :: {T^1_1} ... {f^1_{k_1}} :: {T^1_{k_1}}}
       | ...
       | {C_m} {{f^m_1} :: {T^m_1} ... {f^m_{k_m}} :: {T^m_{k_m}}}

とすると、T型の式{e}に対するレコード更新構文{e} {{bs}}は

{e} {{bs}} = case {e} of
       {C_1} {v^1_1} ... {v^1_{k_1}} -> {C_1} {pick^{C_1}_1(bs, v^1_1)} ... {pick^{C_1}_{k_1}(bs, v^1_{k_1})}
       ...
       {C_m} {v^m_1} ... {v^m_{k_m}} -> {C_m} {pick^{C_m}_1(bs, v^m_1)} ... {pick^{C_m}_{k_m}(bs, v^m_{k_m})}

に変換されます。

多相的な値と組合せるときの注意点

変換された式を見ると、要するにただのパターンマッチになっていることがわかります。
マッチされる式 e の型が多相的で、かつユーザが型シグネチャを供給していないならば e の型は精密化されません。

となると、例えば e が多相的な型を持ち、かつ e {bs} に単相的な型をユーザが与えていた場合、 e の値によって e {bs} の値が一意に決まらなかった場合などは困るわけで、このような場合曖昧性エラーが生じます。

具体的には以下のようなコードで曖昧性エラーが発生します。

data T a = T {element :: a, typeStr :: String}

class F a where mes :: a -> String
instance F Int where mes _ = "Int"
instance F Double where mes _ = "Double"

mkDefaultT :: F a => a -> T a
mkDefaultT x = T x (mes x)

defaultT :: (F a, Num a) => T a
defaultT = mkDefaultT 0

-- error!
modifiedT :: T Double
modifiedT = defaultT {element = 0.0}

defaultT は T Int 型のとき typeStr = "Int" で、 T Double 型のとき typeStr = "Double" です。なので、上の modifiedT の定義では defaultT {element = 0.0} の typeStr フィールドが "Int" なのか "Double" なのかが決定できす、曖昧性エラーとなります。

GHCはどこまで賢くやってくれるのか、という問題

上のような事情があるにはあるのですが、例えば以下のようなコードはコンパイルを通ります。

data T a = T {element :: String, typeStr :: String}

defaultT :: T a
defaultT = T "" "a"

-- error!
modifiedT :: T Double
modifiedT = defaultT {element = ""}

このケースでは defaultT にはいかなる制約もかかっていない forall a . T a という型がついており、このような場合は a がどんな型に具体化されようと e の値は変わらず T "" "a" です。
なので、 defaultT の型が曖昧でも modifiedT の定義は上のままでうまくいきます。

では、「型変数がどの型に具体化されても値が同じ」場合につねにうまくいくかというとそういうわけにもいかず、以下のコードはエラーになります。

data T a = T {element :: String, typeStr :: String}

class F a where mes :: a -> String
instance F Int where mes _ = "Int"
instance F Double where mes _ = "Double"

defaultT :: F a => T a
defaultT = T "" "a"

-- error!
modifiedT :: T Double
modifiedT = defaultT {element = ""}

単に defaultT の型に制約を増やしただけですが、これはエラーになります。
これはおそらく「型変数がどの型に具体化されても値が同じ」かどうかは型によってのみ判断されるからです。
forall a . F a => T a の型の値は「型変数 a が何に具体化されても同じ値」とは限らず、例えば

polyT :: F a => T a
polyT = mkPoly undefined
  where
    mkPoly :: F a => a -> T a
    mkPoly x = T "" (mes x)

のような値がありえます。

同じフィールド名に対するレコード更新構文

知ってた人には「今更」って感じなんでしょうが、

data User = Registered {uid :: Int, name :: String} | Guest {name :: String} deriving (Show)

updateName :: User -> String -> User
updateName u n = u {name = n}

-- 動作:
-- *Main> updateName (Registered {uid=0, name="Bob"}) "Alice"
-- Registered {uid = 0, name = "Alice"}
-- *Main> updateName (Guest {name="Alice"}) "Bob"
-- Guest {name = "Bob"}

みたいなの書けたんですね。知りませんでした。*1

*1:というかそもそも同じデータ型の定義中でならフィールド名被っててもいいのだということを初めて知りました。

Egisonで国士無双の判定(及び「速い」Egisonコードの書き方について少し)

RubyKaigiの実況TL (Egison at RubyKaigi 2014 - Togetterまとめ)にて、
Egisonで麻雀の役判定する話になったとき「国士無双は?」みたいな声を2、3見掛けたので、今更書いてみる。

;; tileの定義は公式のサンプルコードと同じ。

;; 么九牌の判定
(define $yaochu
  (pattern-function []
    (| <hnr _> <num _ ,1> <num _ ,9> )))

;; 全13種の么九牌のリスト
(define $all-yaochu-list
  {<Hnr <Haku>> <Hnr <Hatsu>> <Hnr <Chun>>
   <Hnr <Ton>> <Hnr <Nan>> <Hnr <Sha>> <Hnr <Pe>>
   <Num <Wan> 1> <Num <Wan> 9>
   <Num <Pin> 1> <Num <Pin> 9>
   <Num <Sou> 1> <Num <Sou> 9>})

;; 国士無双の判定
(define $kokushi-musou
  (pattern-function []
    <cons (yaochu) ,all-yaochu-list>))

つまり、「アタマの么九牌」+「13種類の么九牌」で正しく判定できる。

できるんですが、実は速度的に若干の問題を抱えているというか、このコードだと
「アタマを選んでから残りがall-yaochu-listとマッチするかどうかを判定する」という挙動になるので、
例えば手牌全部么九牌だけど国士無双じゃないみたいなコードは一々全部の牌をアタマにしたケースを探索してしまいます。

なので、こう書いたほうが速いはず。

(define $thirteen-orphans-fast
  (pattern-function []
    <join ,all-yaochu-list <cons (yaochu) <nil>>>))

multisetにはsnocがないのでjoinを使って、先に「13種類全ての么九牌がある」かどうかを判定して、残った一牌がアタマとして正しいかどうかを判定するパターンにしています。こうすれば、13種類の么九牌がなかった時点、或いはアタマが不適切(つまり么九牌じゃない)だった場合に即座に失敗してくれます。

しかしなんというか、こんな風にマッチャーの挙動が計算量に割とクリティカルに作用*1してくるケースが生じてくるのは、Egisonプログラミングの難点の一つなのかなぁと思いました。要は、Egisonの処理系の速い遅いの問題はともかく、コーディングする側が「速度」を意識してパターンマッチを書くのが結構難しいんですよね。麻雀の役判定ぐらい複雑なパターンマッチになると、その辺はどうしても無視できなくはるはずです。

たとえば、サンプルコードで七対子の判定パターンがありますが、
あれもたとえば手牌に3対子(aa, bb, cc)しかない状態で判定を走らせると、

  • th_1 = aa, th_2 = bb, th_3 = cc
  • th_1 = aa, th_2 = cc, th_3 = bb
  • th_1 = bb, th_2 = cc, th_3 = aa
  • th_1 = bb, th_2 = aa, th_3 = cc
  • th_1 = cc, th_2 = aa, th_3 = bb
  • th_1 = cc, th_2 = bb, th_3 = aa

の6通りの失敗パターンを通るわけですが、一つ目失敗した時点でもう全体のマッチ失敗が確定するはずなんで、探索を切っていいはずですよね。

そういえば、昔のEgison*2にはcut patternってのがあって、

(twin !$th_1 (twin !$th_2 ...

みたいな感じで、th_1, th_2にマッチしたら、その一つ目の結果でダメなら探索を切るということができました。
要はつまりPrologのカット節と同じ感じで「バックトラックを行わない」ことを指定できたんですが、もう復活はしないのかな。

*1:今回のコードは前者でもまあまあ速いですが。

*2:少なくともversion 2にはあった。

Haskellの多相関数と自然変換(というか射の族)について

これなんですが、以前も聞いた気がするし*1、忘れないように備忘録をば。

たとえば、HaskellでInt -> Double型の関数を1つ与えるというのは、Hask圏において対象Intから対象Doubleへの射を1つ与えることに対応していると思ってよい。

そういう視点で今度はforall a . a -> [a]型の多相関数を考えてみる。
aにある具体的な型、つまりHaskの対象Xを代入すると一つの具体化された型 X -> [X]が決まり、それに対応してHask圏上の(Xから[X]への)射が1つ与えられることになる。
つまり、forall a . a -> [a]型の多相関数は、Hask圏上の射の族{\theta_X: X \rightarrow List(X)}と対応していると考えることができるはず。

射の族が表せるなら、自然変換も表せるという道理になる。*2
つまり、

nat :: (Functor f, Functor g) => f a -> g a
nat = ...

という多相関数は、関手{F:Hask \rightarrow Hask}から関手{G:Hask \rightarrow Hask}への自然変換{\theta: F \Rightarrow G}と対応していると考えることができるし、

nat_l :: Functor f => f a -> a
nat_l = ...

nat_r :: Functor g => a -> g a
nat_r = ...

はそれぞれ自然変換{\theta: F \Rightarrow 1_{Hask}}及び自然変換{\theta: 1_{Hask} \Rightarrow G}と対応していると考えることができる。

そういう視点でMonadのreturn, joinの型を見ると、

class Monad m where
  return :: a -> m a
  join :: m (m a) -> m a

これらはそのまま圏論モナド{(T: C \rightarrow C, \mu, \eta)}の2つの自然変換の成分{\mu: 1_C \Rightarrow T}{\eta: T^2 \Rightarrow T}に対応しているというのがはっきりわかる。

今までHaskellでのMonadの定義と圏論におけるモナドの定義はなんとなく一致してるなーぐらいの感覚で見ていたんですが、今回この多相関数と自然変換との関係を再確認することでより理解が深まった感じがします。よかったよかった。


ところで、Functorのfmap :: (a -> b) -> f a -> f bも多相関数ですが、あれは関手{F}の射関数{F_{Arr(X, Y)}}を表しています。
したがって、fmapはHask圏の射の族ではなく、射{X \rightarrow Y}を射{FX \rightarrow FY}に写す関数の族を表していると言うべきでしょう。
Haskellの(->)はHask圏の射であり、かつ関数でもある*3ので、どちらと取ればいいかには常に気をつけていく必要がありそうですね。

*1:http://d.hatena.ne.jp/hiratara/?of=15 を見るにつけおそらく圏論勉強会で既に学んでいるはず。

*2:自然性をコードで表現できると言っている訳ではない。

*3:あと、A -> B(A,Bは具体的な型)はそれ自体が型なのでHask圏の対象でもありうる。

【随時追記予定】読書メモ:関数プログラミング 珠玉のアルゴリズムデザイン

関数プログラミング 珠玉のアルゴリズムデザイン」を買いました。

読みながらツイートしてたら

というフリを受けたので、理解を深めるためにもメモを書くことにします。
随時更新していきますが、とりあえず3章まで。

(11/19追記)サポートサイトがあるようです。なんとこの記事にリンクを貼っていただきました。ありがとうございます。
関数プログラミング 珠玉のアルゴリズムデザイン


【更新履歴】
2014/11/19: 6章まで更新。あと見た目を多少改善
2015/5/4: 7章を更新。

1章「最小自由数」:

最初の章だけあって平和だった。
強いていえばaccumArray関数の説明がわかりにくかったことぐらい。
なんかこんな感じに挙動の例があれば一瞬で理解できたと思う:

accumArray (+) 0 (1,5) []
= array (1,5) [(1,0),(2,0),(3,0),(4,0),(5,0)]

accumArray (+) 0 (1,5) [(1, 3), (5, 6), (1, 2)]
 = array (1,5) [(1,0+3+2),(2,0),(3,0),(4,0),(5,0+6)]
 = array (1,5) [(1,5),(2,0),(3,0),(4,0),(5,6)]

2章「上位者問題」:

運算を追っていたらウッとなりました。一部の行間がデカいです。
まぁ手を動かせばいい話なんですが。 

  [(z, scount z zs) | z:zs <- map (++ys) (tails xs) ++ tails ys]
= {- <- を++上で分配 -}
  [(z, scount z (zs ++ ys)) | z:zs <- tails xs] ++ 
  [(z, scount z zs) | z:zs <- tails ys]

これはつまり

  [(z, scount z zs) | z:zs <- map (++ys) (tails xs) ++ tails ys]
= {- <- を++上で分配 -}
  [(z, scount z zs) | z:zs <- map (++ys) (tails xs)] ++ 
  [(z, scount z zs) | z:zs <- tails ys]
= 
  [(z, scount z zs') | z:zs <- tails xs, let zs' = zs ++ ys] ++ 
  [(z, scount z zs) | z:zs <- tails ys]
= 
  [(z, scount z (zs ++ ys)) | z:zs <- tails xs] ++ 
  [(z, scount z zs) | z:zs <- tails ys]

ということ。
今後もこれぐらいは瞬時に脳内補完できるような運算力が求められてくるのだろうか。

3章「鞍型探索の改良」:

p12. Theoの発言

最悪の場合で{f}をおよそ{ \displaystyle 2\log z + (m + n) }回計算し, 最良の場合では{ \displaystyle 2\log z + (m \min n) }回になります.{m}または{n}のどちらかは{z}よりも十分小さくなりうるので, たとえば, { f (x,y) = 2^x+3^y }であれば最悪の場合で{ \displaystyle O(\log z) }ステップしかかからないアルゴリズムになりますね

これは全く何を言っているのかわからなかったし、今でも理解できない。
理解できないというのは、「{m}または{n}のどちらかは{z}よりも十分小さい」からの話の流れとして意味がわからない、ということ。{ f(x,y) = 2^x+3^y }の場合は{m}{n}{z}に比べて十分小さいので最悪ケースでも{O(\log z)}ステップという結論自体は正しいと思います。

p14. Anneによるinvert関数の計算量の下界の解析

ここで { A(m, n) }というのは、二引数狭義単調増加関数 { f }の値を { z }にする(、つまり { f(x,y) =z }となる)ような { (x,y)\ (0 \leq x < n, 0 \leq y < m)}のリストとしてありうる全ての組み合わせの数。
(つまりたとえば {m=2, n=2}なら、問題「{f(x,y)=z}をみたすような {(x,y)}のリストを求めよ」の答えとしては
{ [ ], [(0,0)], [(1,0)], [(0,1)], [(1,0), (0,1)], [(1,1)] }
の6通りが考えられるから、 {A(2,2)=6}

 {A(m,n)}を見積もるのはやさしいことです.  {0 \leq x < n}かつ {0 \leq y < m}の範囲で { f (x,y)=z }となる対 { (x,y) }のそれぞれのリストが,  { m \times n }の長方形を左上隅から右上隅へいく階段形状と一対一で対応しています. この階段形状内の角部分に {z}が現れます.

ここは難しかった。

まず、この章のテーマでもある鞍型探索アルゴリズムが解を見つけていく挙動をみてもわかるように、 { f(x,y)=z }をみたす { (x,y) } { m \times n }長方形上に左上から右下に

f:id:xenophobia:20141115030416p:plain

( { f(x,y)=z }をみたす { (x,y) }を赤で表示している)

のように並ぶということがわかる。
すると、 { (x,y) }のリスト一つに対し、その各点が角になるような階段

f:id:xenophobia:20141115030424p:plain

を対応付けることができる。これは一対一の対応である。

4章「選択問題」:

以下、タイトルに「」が付いていた場合は引用であることを意味するものとします。

「順序付き型の要素の……」

型に順序が付いてる……?とか一瞬思ったけど要はOrd型クラスのインスタンスになるような型のことを言っているらしい。

abideな演算子

縦横不問(abide)というのは初めて聞いたが、要するに

xs U ys
++   ++
ys U vs

と並べたときに
縦、横の順で[xs ++ ys] ∪ [us ++ vs]と計算しても、
横、縦の順で[xs ∪ us] ++ [ys ∪ vs]と計算しても結果は同じ、というイメージで理解した。

 {a>b}の場合は双対になる」

smallest k (xs ++ [a] ++ ys) (us ++ [b] ++ vs)の結果は(xs ++ [a] ++ ys)と(us ++ [b] ++ vs)とを取り替えても変わらないので、
適当に取り替えることで {a\lt b}を仮定できるという意味。

 {a=b}の場合は?

今、unionする集合同士は互いに素であることを仮定している。

5章「組和の整列」:

「この行列は標準Young盤の一例である」

xs,ysが昇順ソート済みなら、[[x {\oplus} y | y <- ys] | x <- xs]の各行・各列は明らかに昇順だから標準Young盤(ヤング図形 - Wikipedia)になっている。ここでは、xs及びysは集合(なので要素に重複がない)という前提が使われている。(重複がもしあれば半標準(semi-standard)というべき)

比較回数の下界 {\log E(n)}

{E(n)}はソートしたい組和が並ぶ行列の各要素にインデックスを割り振る方法の数なので、ソートの出力は{E(n)}通りありうる。
あとは一般的な比較ソートの下界の議論と同じ。

tableの意味

xs、ysを順序集合{A}の要素のリストとする。

table xs ys :: [(Int, Int, Int)]の中の(1, i, j) < (2, k, l)という2つの要素を見ることで得られる情報は、
(xsのi番目の要素){\ominus}(xsのj番目の要素) {\lt} (ysのk番目の要素){\ominus}(ysのl番目の要素)
つまり
(xsのi番目の要素){\ominus}(ysのk番目の要素) {\lt} (xsのj番目の要素){\ominus}(ysのl番目の要素) ((5.2)より)
である。

したがって、2つの組差{x \ominus y}{x' \ominus y'}を比較するにはtable xs ysの対応する要素の大小を参照すればよく、配列に変換してしまえばこれは定数時間でできる。

ここで重要なのは、目的は{{\bf A}}上の比較回数を減らすことであるということ。当然、tableを使ってもソートには{O(|xs||ys| \log |xs| |ys|)}かかるが、その際の比較演算は自然数上の比較演算なので、
必要な{A}上の要素の比較はtableを構築する際に必要な分だけということになる。

6章「小町算」:

正格関数

divergence: {\bot}を適用した結果が発散する関数を正格関数という。
Haskellなら「undefinedを適用したときに*** Exception: Prelude.undefinedを吐かない」と言いかえてもいいはず。

filter f: [a] -> [b]はまずリストをパターンマッチして次の挙動を決めるのだから、自明に正格。

(6.3)は(iii)の具体化

(6.3)が

filter (ok . value) . extend x
= filter (ok . value) . extend x . filter (ok . value)

f = filter (ok . value), g = extend, h = extend' = filter (ok . value) . extendを代入して

f . (g x) = h x . f

両辺にyを適用

f (g x y) = h x (f y)

これが条件(iii)に一致。

(6.10)の導出

なんでこれだけ導出載ってないんだろう。「自明」ってことだろうか。

filter (p . snd) . map (fork (f, g))
= {- filter p . map f = map f . filter (p . f) より -}
map (fork (f, g)) . filter (p . snd . fork (f, g))
= {- (6.5) snd . fork (f, g) = g より -}
map (fork (f, g)) . filter (p . g)

glue(一つめの定義)の意味

glue 1 "23×4+56"
=  "123×4+56"
++ "1×23×4+56"
++ "1+23×4+56"

のような「式の一番前に数字を一つ加える」挙動が、

glue 1 [[[2,3],[4]],[[5,6]]]
=  [[[1,2,3],[4]],[[5,6]]]
++ [[[1], [2,3],[4]],[[5,6]]]
++ [[[1]], [[2,3],[4]],[[5,6]]]

とリスト上の操作で実現されている。

7章「最小高さ木の構築」:

長らく更新がなかったのは普通にこの章が難しいからです。
誤りがあるかもしれませんのでこの章に関するツッコミは特に歓迎です。

この章を難しくしている最大の要因は、『木(Treeデータ型)』に対して定義されている関数と『森(Forestデータ型)*1』に対して定義されている関数が同名で、
かつそれらが文脈によってフレキシブルに入れかわる
という点だと思います。後述するようにそれらは実質同じものなのでそうすることで議論の本質を外してしまうことはありませんが、
どちらがどちらなのかを注意して読まないとどっかで置いていかれることもあるかと思います。

prefixes関数(Tree版)

prefixes x tで「tの一番左の葉としてxを挿入した場合の木のリスト」を返すとあるが、
これは「周縁の最左要素がxとなるようにtにxを挿入した場合の木のリスト」という意味である。
つまりは木の周縁(fringe)を返す関数fringeを

fringe :: Tree -> [Int]
fringe (Leaf x) = [x]
fringe (Fork u v) = fringe u ++ fringe v

と定義したとき、以下の性質

t' ∈ prefixes x t
⇒ fringe t' === x ++ (fringe t)

を満たすということ。

left spine(木の左背骨)

二分木の定義

data Tree = Leaf Int | Fork Tree Tree

より、二分木は必ずFork (Fork (...(Fork (Leaf x) {t_1})... {t_{n-1}}) {t_n}という形をしている。
このとき[{(t_0=)}Leaf x{, t_1, t_2, \dots, t_n}]を元の木の左背骨という。これは森である。
後に、左背骨を求める関数spineが登場する。

f:id:xenophobia:20150501111150p:plain

この左背骨をrollup = foldl1 Forkで一つの木にすると元の木に戻る。この操作を巻き上げという。
木の左背骨は一意に決まるので、これをもって左背骨(=最左要素が葉であるような森)と木とに一対一対応がつけられる。

prefixesの再定義

これまで木に対して各関数を考えてきたが、左背骨(:: Forest)と木の間に一対一対応がつけられることがわかった。
また、森の各木の周縁を同じ順で連結すると、その森を巻き上げた木の周縁になる、つまり

concatMap fringe forest === fringe $ rollup forest

成り立つ。

したがって、prefixes x tsを「(巻き上げた後にできる木の)周縁の最左要素がxとなるように森tsにxを挿入した場合の森のリスト」と再定義できる。

非決定的な(nondeterministic)関数

ここでいう非決定的とは、プログラム中に非決定性(nondeterminism)が含まれているという意味ではなく、
仕様だけでは出力が一意に決まらないという意味。

これとは別に、定義に乱数やインプットが含まれているようなプログラムをnondeterministicと呼ぶケースもある。
*2

この先の議論にはminBy costの定義がしっかりと与えられている必要はなく、
あくまで「costが最小の木を返す」という仕様が満たされていればよいので、定義を一部曖昧なままにした、と捉えたほうがいいかもしれない。

精緻化関係 {e_1 \leadsto e_2} 上の運算

非決定的な関数にもプログラム運算が適用できるように精緻化関係{\leadsto}上の運算が導入される。
つまり、精緻化関係{e_1 \leadsto e_2}の右辺が出力しうる値は左辺でも出力されうることが保証されている。
たとえば、anyOf :: [Int] -> Intを

anyOf [n1, n2, ..., nm] ∈ {n1, n2, ..., nm} {- n1, ..., nm のどれかをランダムに(非決定的に)出力 -}

と定義すると、anyOf (l1 ++ l2) {\leadsto} anyOf l1 のような関係が成り立つ。

たまに{\forall x . f x \leadsto g x}を指して{f \leadsto g}と書かれていることがあるっぽい?*3

融合変換の章

個人的にはここの話の流れが掴みづらい。
全体として「cost関数で順序付けをすると融合条件等を考えづらいので、cost'を使う」みたいな話になっている。
色々なことが省略され、行間に消えてしまっているので、補いつつ読むしかない。

cost', costsについて

costは木のコストで、cost'は木の左背骨に沿ってコスト情報を拾うことで得られるリストである。
cost' tの最左要素はcost tなので、cost'で最小の要素はcostで最小の要素でもある。
またcosts = map cost . reverseは、左背骨のコストを定義していると思ってよい。
cost' = costs . spineなので、costs = cost' . rollupである。つまり、costs ts < costs ts'ならばtsを左背骨にもつ木はts'を左背骨にもつ木よりコストが小さい。

insertについて

p40の最下部にある運算では、insertの規定が

minBy costs . prefixes x {\leadsto} insert x

になっている。元々示されていたinsertの規定はminBy cost . prefixes x {\leadsto} insert xなので、型がInt -> Tree -> TreeからInt -> Forest -> Forestに変わっている。
つまり、insert xは「森に対し、コストが最小になるようにxを挿入した森(のうちのどれか一つ)を返す」という関数。実際には一般の森ではなく左背骨に対して挿入が行われる。

以下、insertはInt -> Forest -> Forestの版として議論します。
以下、議論に必要なのでInt -> Tree -> Tree版のinsertをinsert'で表します。
insertとinsert'の間には次のような関係が成り立ちます。

(insert-rel): insert' x (rollup ts) = rollup (insert x ts)

p40最下部の運算で行われている「融合変換(fusion)」について

minBy costs . foldrn (concatMap . prefixes) (wrap . wrap . Leaf) {\leadsto} foldrn insert (wrap . Leaf)

が単に「minBy costs . prefixes x {\leadsto} insert xを用いて融合変換すると……」と書かれている。
これも要するに全てのxsについて

minBy costs (foldrn (concatMap . prefixes) (wrap . wrap . Leaf) xs) {\leadsto} foldrn insert (wrap . Leaf) xs

ということだと思うのでそのつもりで解説する。
foldrnの融合変換を上の形で使うには、以下の2つが成り立たなければならない。

  1. 任意のxについて minBy costs ((wrap . wrap . Leaf) x) {\leadsto} (wrap . Leaf) x
  2. (7.1'): 任意のx, fs, ts'について minBy costs fs {\leadsto} ts' ならば minBy costs (concatMap (prefixes x) fs) {\leadsto} insert x ts'

前者は要素が一つしかないので自明。後者(7.1')についてはp39に倣っていろいろ言う必要がある。
ここが完全に省略されているのは多分「前のページと同じようにできるので」的な意味合いなのだと思う。

まず、以下に示す(7.2')が成り立てば(7.1')が成り立つ。(★)

(7.2') minBy costs fs {\leadsto} ts {\Rightarrow} minBy costs (map (insert x) fs) {\leadsto} insert x ts

(★)を示すには、p39の最下段にある運算と全く同じことをすればよいです。

minBy costs (concatMap (prefixes x) fs)
    {- concatMapを展開 -}
= minBy costs (concat (map (prefixes x) fs))
= (minBy costs . concat) (map (prefixes x) fs)
    {- minBy costs . concat = minBy costs . map (minBy costs) -}
= (minBy costs . map (minBy costs)) (map (prefixes x) fs)
= minBy costs . (map (minBy costs) (map (prefixes x) fs))
    {- map f (map g xs) = map (f.g) xs -}
= minBy costs . (map (minBy costs . prefixes x) fs)
    {- f {\leadsto} f' ならば map f {\leadsto} map f' かつ g.f {\leadsto} g.f' -}
{\leadsto} minBy costs . (map (insert x) fs)

で、(7.2')が言えるためには単調性条件が言えて欲しいが、(7.2)とは違い、ここでは(7.4)が成り立つならば以下の単調性条件(7.3')が成り立つことが言える。

(7.3'): costs us {\leq} costs vs {\Rightarrow} costs (insert x us) {\leq} costs (insert x vs)

なぜならば、costs us {\leq} costs vs {\Leftrightarrow} cost' (rollup us) {\leq} cost' (rollup vs)であり、
また、これと(insert-rel)より
costs (insert x us) {\leq} costs (insert x vs)
{\Leftrightarrow} cost' (rollup (insert x us)) {\leq} cost' (rollup (insert x vs))
{\Leftrightarrow} cost' (insert' (rollup us)) {\leq} cost' (insert' (rollup vs))
なので、(7.3')と(7.4)は同値であるからである。

すなわち、(7.4)が言えれば(7.2')、(7.1')が言えるから融合変換が可能になる。

結局、insert :: Int -> Forest -> Forestが実装でき、(7.4)が}成り立てば融合変換が可能ということになり、p41冒頭の主張に繋がる。

単調性条件について

なぜ(7.3)ならば(7.2)が成り立つのか、について。

(7.3)は関数 insert x が順序関係{u \preceq v \Leftrightarrow \text{cost}\ u \leq \text{cost}\ v}に関して単調であるという条件であり、
これが成り立つならばtsで{\preceq}に関して最小の要素はt_min = [insert x t | t<-ts]で{\preceq}に関して最小の要素はinsert x t_minとなるので、(7.2)が成り立つこととなる。
上述した(7.2')⇒(7.3')も同じ議論で導ける。

「(7.4)から……が導けることをこのあと示す」

ここが全くわからない。どう見てもこの後に導出があるようには見えないし、そもそもこの先の議論で必要な事実ではない。
訳出ミスでもなさそう。情報求む。

j+1 {\leq} k {\leq} nの範囲で{c_k' = c_k}

「観察によって確かめよ」とあるが、以下の事実に着目するとわかりやすい。

{c_k}, {c_k'}の定義より、{c_k'}{c_k}より真に増加するのは、
{c_{k-1}'}{c_{k-1}}より真に増加し、かつその値が{\text{cost}\ t_k}より大きいとき
、つまり
{c_{k-1}' > (c_{k-1}\ \max\ \text{cost}\ t_k) = c_k-1}のときである。

つまり、{c_j' < c_{j+1}}ならば{c_{j+1}}は増加しないことになり、当然kがj+1より大きい範囲で{c_k}は増加しようがない。

最適なinsertの方針

p42冒頭では、「jが(7.5)を満たし、かつi{\lt}jなるiも(7.5)を満たすなら、(下から数えて)i番目に挿入したほうがj番目に挿入するよりコストが低くなる」
という事を述べている。これはつまり、コスト最小を目指すなら(7.5)を満たす範囲でなるべく低い位置に挿入すべきだということを示している。
これで、最適な挿入を実装する方針が固まったことになる。

計算時間の見積もり(帰納部)

ちょっと訳が微妙だが、「長さm'のリストに適用して長さmのリストを返すときにはsplitがm'-m回呼ばれる」というのは、
splitを長さm'のリストに適用した返り値のリストの長さがmだった場合の再帰呼び出しの回数がm'-mであるということである。

foldrn insert (wrap . leaf)におけるinsertの呼び出し回数はリストの長さが1増えるごとに1回だけ増えるので、
foldrnがリストの要素をn-1個食ったあとのアキュムレータの長さがm'だとすると

  1. 帰納法の仮定より今までのsplitの呼び出し回数が 2(n-1)-m' 回
  2. insert呼び出し時に一回だけ呼ぶsplitの回数が 1 回
  3. splitの再帰呼び出しが m'-m 回

ということになり、これを全部足すと最後の式が出てきます。

*1:正確には木の左背骨

*2:ていうか個人的にはnondeterministicの用法はコレしか見たことがない……

*3:自信ないけどinsertの規定とかはどうみてもこの意味ですよね……?

Egisonポーカー再考

Egisonコードの例としてよく紹介される(?)例としてポーカーの役判定があります。

http://www.egison.org/demonstrations/poker-hands.html

  • コレクションをMultisetとして扱うことにより手札の順序を考慮しなくてよい
  • non-linear patternを扱える(value patternを使える)おかげでペアやスリーカード系の判定が直接的に書ける
  • カードの数部分をintegerではなくmod 13でマッチすることで、ストレートにおける10-11-12-13-Aのようなケースをうまく扱える(後述するように、実際はこれだけだと11-12-13-A-2とかにマッチしてしまってマズいですが)

など、いろいろな面倒をマッチャーに任せて楽ができるという主旨のものです。

これを題材にいろいろやってみました。

Jokerを加える

Jokerを所謂ワイルドカードとして加えるルールがあります。これをカードに加えたポーカーを考えたい、つまり

(poker-hands {<Card <Club> 12>
              <Card <Club> 10>
              <Joker>
              <Card <Club> 1>
              <Card <Club> 11>})

のようにJokerを含んだ手を役判定したいとき、考えられる手段としては

  1. poker-handのパターンを修正する
  2. cardマッチャーを修正する

前者は、要は例えばスリーカードのパターン

<cons <card _ $n>
 <cons <card _ ,n>
  <cons <card _ ,n>
   <cons _
    <cons _
     <nil>>>>>>

<cons <card _ $n>
 <cons (| <card _ ,n> ,<Joker>)
  <cons (| <card _ ,n> ,<Joker>)
   <cons _
    <cons _
     <nil>>>>>>

とか書き直せばいいという話ですが、全パターンにこれをやろうとすると場合分けやらがひどいことになって多分死にます。あと、折角直感的にパターンを書けていたのに煩雑になってしまいます。

後者は<Joker>がワイルドカード、つまり存在する全てのカードとしてマッチするようにマッチャーを書き直すというものです。一から全部書き直してもいいですが、algebraic-data-matcherになんとかしてもらえそうなところは全面的に委託する感じで書いてみます。

このようにすると<Joker>がワイルドカードとしてのふるまいをするようになり、poker-handsは何も変えなくてよいということになります。

役判定アルゴリズムのパターン記述部とカードの実装を分離できている

ので、個人的にはこっちの解決策のほうが好きです。

ストレート(及びストレートフラッシュ)の修正

これは普通に間違ってるなーと前からちょっと思っていて、要はストレート(ストレートフラッシュ)のパターンって微妙に間違っていて、12->13->A->2->3みたいなのはストレートにはならんわけです。

これを修正するのは一瞬で、

でOK。一番小さい数字が11未満であることを保証してやれば、12->13->A->2->3はちゃんと弾かれるわけですね。

個人的にはEgisonやりたてのころはpredicate patternは慣れないと使い方わからないようなところあったので、ちょっと複雑にはなるけど例として入れといたら入門的な意味でいいんじゃねーのと思ったりしました。ANDパターンの使用例にもなりますし。

Type Level Ifについて

前記事 http://xenophobia.hatenablog.com/entry/2014/05/07/004251 書いてるときにふと、型レベルのIf使ったほうがいいのかなと一瞬思ったりしました。

singletonsパッケージのData.Singletons.Types(https://hackage.haskell.org/package/singletons-0.10.0/docs/Data-Singletons-Types.html)とかに型レベルのIfが置いてありますが、Type familyの「評価」ってそもそもLazyなんですかね。LazyだったらちゃんとIfとして機能しますが。というわけでやってみました。

結果、ループにハマりました。つまりこのコードにおいては引数部分が先に評価されている。

Line 10: 1 error(s), 0 warning(s)
    
Context reduction stack overflow; size = 201
Use -fcontext-stack=N to increase stack size to N
  Loop Int ~ uf0
In the expression: undefined :: If True Int (Loop Int)
In an equation for `a': a = undefined :: If True Int (Loop Int)
In the expression:
  do { let a = undefined :: If True Int (Loop Int);
       print "Hello" }

ということは式とは違って評価はStrictっぽい?ちょっと意外。