日々の流転

λ. 単純オートマトンの型について (HIMA' の補足)

先日のHIMA'で、

data Auto i o = A{ unA :: i → (o, Auto i o) }

という型*1が何故オートマトンの型なのかという話が少しあったので、簡単に補足しておく。 まず、入出力を扱う基本的なオートマトンとして、ミーリ・マシン（Mealy Machine）とムーア・マシン（Moore Machine）というものがある。

ミーリ・マシンは以下の組で定義される。

• 入力アルファベット集合 I
• 出力アルファベット集合 O
• 状態空間 S
• 初期状態 s0
• 遷移関数 δ: S×I→S×O

同様にムーア・マシンは以下の組で定義される。

• 入力アルファベット集合 I
• 出力アルファベット集合 O
• 状態空間 S
• 初期状態 s0
• 遷移関数 δ: S×I→S
• 出力関数 v: S→O

普通は入出力のアルファベットは固定したうえで、様々なオートマトンを考えると思うので、ここでは入出力のアルファベットはi,oに固定されているとする。すると、これらのオートマトンの初期状態を除いた構造は、

type T1 i o s = i → (o, s)
type T2 i o s = (o, i → s)

という型を定義して、ミーリ・マシンでは型S と 関数 S → T1 i o S の組によって、ムーア・マシンでは型Sと関数 S → T2 i o S の組によって表現できる。

T1 i o と T2 i o はともに関手になっていて、このような関手Tが与えれたときに、集合Xと関数 X → T X の組はT余代数(T-coalgebra)とも呼ばれる。そして、オートマトンの状態というのはこういう構造(=演算)を持った集合Sの要素であると考えることができる。

ただ、個々のオートマトン毎に型Sは異なっているので、いろんなオートマトンをシミュレーションしようと思うと、Haskellの型システム的には面倒くさい。それに、あるオートマトン(S1,δ1)の状態s1∈S1と、(S2,δ2)の状態s2∈S2は振る舞いが全く同じでも、値としては違う値であるかもしれなくて、これもよろしくない場合がある。

そこでS1やS2に相当する状態をすべて含んだ上で、かつ同じ振る舞いをする状態は同じ値になるような、そういう特別なオートマトンを考える。ミーリ・マシンの場合には (Auto i o, unA) がそれである。そして、以下のような関数 unfold phi によって、任意の (s, phi :: s → T1 i o s) の状態から、対応する (Auto i o, unA) の状態へと変換することができる。

unfold :: (s → T1 i o s) → s → Auto i o
unfold phi s = Auto $ \i →
  case phi s i of
    (o, s) → (o, unfold phi s)

余代数の言葉でいえば (Auto i o, unA) は T1 i o の終余代数(final (T1 i o)-coalgebra) で、unfold phi は (s, phi :: s → T1 i o s) から (Auto i o, unA) への一意な準同型射である。

このように、(Auto i o, unA) はある意味であらゆるオートマトンを表現できるような特別なオートマトンなので、これをオートマトンの型として扱っていると。

λ. Real World Haskell読書会 2010-12

後で書く……かも。

「間違いだらけの擬似乱数選び」 (参考: ヒビルテ(2002-02-06))。

λ. Beyond Classical Domain Theory by Alex Simpson

これは面白い。Synthetic Domain Theory って、昔、長谷川立氏のチュートリアル「パラメトリック・ポリモルフィズム」で

• 「この節では，パラメトリシティ原理を満たすモデルを幾つか紹介してみたい．いずれもかなり重たい数学を用いるので，深入りはしないことにしておく」
• 「もう1つのモデルは，直観主義的宇宙を用いる方法で得られる．これにはさらに難しい数学が必要なので，表面的なことを述べるだけにする」

と難しいことが随分強調されていたので、きっと難しいのだろうなと思って近づいていなかったんだけど、このスライドは分かりやすかった。effective topos とか realizability interpretation とか計算可能性とか、そういう難しいことを一切知らなくても、直観主義論理と圏論さえ知っていれば使えそうだと感じた。

そういえば、Synthetic Domain Theory については、長谷川真人氏の「自己言及の論理と計算」(参考: ヒビルテ(2003-06-29))の「Advanced Topic 直観主義的抜け道について」でも触れられていたな。ついでに、以下のように書いてあったので、今CLTT読書会で読んでいるCLTTにもそういう話が出てくるらしい。

これらの事柄はかなり専門的であり，今のところ研究論文以外に情報源はあまりないが，B. Jacobs: Categorical Logic and Type Theory (North-Holland, 1999) には，そのような直観主義的集合論のモデルに関するくわしい解説が含まれている．

以下、読んでいて気づいた点のメモや練習問題を解いてみたりしたもの。

Simple constructions (20)

集合の直積が集合なのは、A×B = {z | ∃x∈A, y∈B. z=(x,y)} = ∪_x∈A ∪_y∈B {z | z=(x,y) ∨ z=(x,y)} で、Indexed union axiom と pairing axiom から。

クラスA, 集合X に対してのクラス A^X の定義は、⊆の定義をクラスに一般化すれば、P(A)の定義もクラスに一般化されるので、Aが集合の場合と同じでよいはず。

• A⊆B ⇔ (∀x. x∈A ⇒ x∈B)
• P(A) = {z | z⊆A}
• A^X = {f ∈ P(X×A) | ∀x∈X. ∃!y∈A. (x,y)∈f}

Countable choice (22)

• axiom of choice を ∀x∈X. ∃y∈Y. φ ⇒ ∃f∈Y^X. φ[f(x)/y]
• countable choice を ∀n∈N. ∃y∈Y. φ ⇒ ∃f∈Y^N. φ[f(n)/y]

と書いてあるが、これらはそれぞれ

• ∀x∈X. ∃y∈Y. φ ⇒ ∃f∈Y^X. ∀x∈X. φ[f(x)/y] と
• ∀n∈N. ∃y∈Y. φ ⇒ ∃f∈Y^N. ∀n∈N. φ[f(n)/y]

の誤りだろう。

【2010-12-23 追記】 それはそれとして、型理論やBHK解釈に慣れ親しんでいると、選択公理は推論規則から自明に証明できてしまう気がするけど、こう書いてあるということは、ここではそうではないということで、なんだか少し気持ち悪い。どういう体系になっているのか、気になるところ。

Truth values (23)

⌜_⌝に関する幾つかの性質

• ⌜φ⌝=⊤ ⇔ {∅ | φ}={∅} ⇔ φ
• ⌜φ⌝=⊥ ⇔ {∅ | φ} = {φ | ⊥} ⇔ ¬φ
• X∈Ωに対して、∅∈⌜X=⊤⌝={∅ | X=⊤} ⇔ X=⊤ ⇔ ∅∈X より、 ⌜X=⊤⌝=X

以降では ⌜φ⌝=⊤ のことを単に ⌜φ⌝ と書いているようだ。

P(X) ≅ X→Ω の証明は、

• F: P(X)→(X→Ω)
  F(A) = {(x, ⌜x∈A⌝) | x∈X}
• G: (X→Ω)→P(X)
  G(f) = {x∈X | f(x)=⊤}

とおけば、

• GF(A) = {x | ⌜x∈A⌝=⊤} = {x | x∈A} = A かつ
• FGf = {(x, ⌜f(x)=⊤⌝) | x∈X} = {(x, f(x)) | x∈X} = f

なので言える。

Booleans (24)

Ω⊆2がLEM(排中律)と同値であることの証明。

LEMを仮定すると、以下より Ω⊆2

x∈Ω
⇒ (∃y. y∈x)∨¬(∃y. y∈x)  {- by LEM -}
⇔ x=⊤ ∨ x=⊥
⇔ x∈{x | x=⊤ ∨ x=⊥}=2

逆にΩ⊆2とすると、任意のφに対して、⌜φ⌝∈Ω⊆2 ⇒ ⌜φ⌝=⊤ ∨ ⌜φ⌝=⊥ ⇔ φ ∨ ¬φ なので、LEMが成り立つ。

Semidecidable properties and Markov's principle (25)

p,q∈Σ ⇒ p∧q ∈ Σ の証明

• p∈Σ より、P: N→2 が存在して p=⌜∃n∈N. P(n)⌝
• q∈Σ より、Q: N→2 が存在して q=⌜∃n∈N. Q(n)⌝

R(n) = P(π1(n))∩Q(π2(n)) とおくと、p∧q = {∅ | ∅∈p ∧ ∅∈q} = {∅ | ∃n∈N. P(n) ∧ ∃n∈N. Q(n)} = {∅ | ∃n∈N. R(n)} ∈ Σ

「p: N→Σ ならば (∃n∈N. p(n)) ∈ Σ」というのがあるけど、結論部は (∨_n∈N p(n)) ∈ Σ のことだろう。 ∀n∈N. p(n)∈Σ より ∀n∈N. ∃Q:N→2. p(n)=⌜∃m∈N. Q(m)=⊤⌝ で、ここで可算選択公理(countable choice)を使うと、 f : N→N→2 が存在して ∀n∈N. p(n)=⌜∃m∈N. f(n)(m)=⊤⌝ 。R(n) = f(π1(n))(π2(n)) とおくと、∨_n∈N p(n) = ∪_n∈N p(n) = {x | ∃n∈N. x∈p(n)} = {x | ∃n∈N. ⌜∃m∈N. f(n)(m)=⊤⌝=⊤} = {x | ∃n∈N, m∈N. f(n)(m)=⊤} = {x | ∃n∈N. R(n)=⊤} ∈ Σ

Towards synthetic domain theory (27)

N, 2, Q が fixpoint property を持たないこと。

Nの場合sが不動点を持たない。P={n∈N|s(n)≠n)とおくと、s(0)≠0なので0∈P、n∈Pとするとs(n)≠nなのでs(s(n))≠s(n)でs(n)∈P 。よって P=N 。

Ωの場合 not: Ω→Ω を not(x) = ⌜∅∉x⌝ とすると not(x)=x ⇔ ⌜∅∉x⌝=⌜∅∈x⌝ ⇒ ⊥ より、notには不動点が存在しない。

2の場合も、not を 2→2 に制限すれば同じ。

Basic propertis of probabilistic domains (66)

「Then (I,0,⊕) ⋌ η_D since (I,0,⊕) is an object of ProbDom'_⊥⊕」というのが理解できず悩んでしまったが、これはまさにユニットの性質そのもの。

λ. 「範疇文法と証明論」シンポジウム

「範疇文法と証明論」シンポジウム に参加。

λ. HIMA' #4: 関数型的正規表現マッチ

HIMA' #4: 関数型的正規表現マッチ に参加。

• 電通大のPFCという関数型言語処理系の話を聞き、PCFと空目しそうだと思った。
• Program-ing Finger Trees in Coq (参考: ヒビルテ(2007-11-04))

λ. 正格性解析 (Strictness Analysis)

この記事はHaskell Advent Calendarのために書かれたものです。(22日目)

正格性解析(strictness analysis)は、Haskellのような遅延評価を行う純粋関数型言語での最も基本的な最適化のひとつの割に、あまり知られていないようなので、簡単に紹介してみることに。

動機

よくある例だけど、末尾再帰で書かれた

sum' :: Int → [Int] → Int
sum' s [] = s
sum' s (x:xs) = sum' (s+x) xs

というプログラムは、Haskellでは最適化が行われない限り悲惨なことになる。

sum' 0 [1,2,3,4] を計算すると、sum' 0 [1,2,3] ⇒ sum' (0+1) [2,3] ⇒ sum' ((0+1)+2) [3] ⇒ sum' (((0+1)+2)+3) [] ⇒ (((0+1)+2)+3) という風に実行が進む。引数のsが未評価のまま蓄積されていき、だんだんと大きな式になってしまっている。

この例だとどうってことはないけど、入力がもっと大きい場合にはヒープを圧迫するし、最終的に (((0+1)+2)+3) を評価するときも、+3と+2をスタックに積んでから0+1を評価するという風になるので、入力が大きい場合にはスタックを大量に消費してしまう。

seqとBangPatterns

この問題は sum' が引数sを評価しなかったからで、引数を評価するようにすれば、sum' 0 [1,2,3] ⇒ sum' 1 [2,3] ⇒ sum' 3 [3] ⇒ sum' 6 [] ⇒ 6 という風に実行が進むようになり、ヒープを消費してしまう問題もスタックを消費してしまう問題も解決する。

そのようにするにはseqを使って

sum' :: Int → [Int] → Int
sum' s [] = s
sum' s (x:xs) = seq s $ sum' (s+x) xs

とすれば良い。 seq x y の直観的な意味は「xを評価してからyを返す」というもの。 なので、上の例では再帰呼び出しの前にsが評価されるようになり、問題が解決する。

もしくは、seqの代わりにBangPatterns拡張を使って

sum' :: Int → [Int] → Int
sum' s [] = s
sum' !s (x:xs) = sum' (s+x) xs

と書けば良い。 BangPatternsはseqのシンタックスシュガーと思って良い。もっとも、完全に構文的に変換するのは大変そうだけど。

正格性解析

「…と書けば良い」って、そりゃ書けば良いんだけど、そんなのイチイチ書きたくないので、GHCとかはそれを自動的にやってくれるようになっていて、それが正格性解析とその結果を利用した最適化。

そもそも上のsum'の場合だと、引数sは後で絶対評価されるのだから、それを先に評価してしまっても、結果は変わらないはず(停止するはずのプログラムが停止しなくなったりはしないはず)。正格性解析はこういう「先に評価してしまっても構わない引数」というのを発見してくる。で、コンパイラはそういう引数を先に評価したりとか、あるいはこの情報をworker-wrapper変換のような他の最適化のために利用する。

この「先に評価してしまっても構わない引数」というのをもう少し数学的に考えたのが関数の正格性で、正格性解析というのは文字通り、関数の正格性を解析する。

関数の正格性

関数fが正格なのは f ⊥ = ⊥ が成り立つとき。 ここで ⊥ は停止しない計算とかエラーとかを表した値である。Haskellでは典型的にはundefinedとかerror関数がこの値を持つ。MLなどの関数は全て正格な関数になっているけど、Haskellの関数は正格とは限らないので、Haskellは非正格関数型言語(non-strict functional language)と呼ばれたりもする。

上の正格性の定義は一引数関数に対してのものだったけど、多引数関数に対しても拡張できる。例えば、3引数関数fが 第二引数に対して正格というのは、任意のx,zについて　f x ⊥ z = ⊥ が成り立つとき。

幾つかお馴染みの関数の正格性を考えてみる:

• notは not undefined = undefined なので明らかに正格。
• id は id undefined = undefined なので正格。その関数自身が評価を行わなくても正格な場合もあるので注意。
• error は引数に関わらず結果が undefined なので、error undefined = undefined が成り立ち、正格。
• 整数の加算 (+) は undefiend + b = undefined かつ a + undefined = undefined なので、どちらの引数に対しても正格。
• (&&) は undefined && y = undefined なので第一引数に対して正格だけど、False && y = False ≠ undefined なので第二引数については非正格。
• 同様に const も第一引数に対して正格で、第二引数に対して非正格。
• seqの意味は以下の等式で定義されているので、どちらの引数に対しても正格。
  • seq ⊥ b = ⊥
  • seq a b = b, if a ≠ ⊥

上のsum'を考えると、sum' undefined xs = undefined でかつ sum' s undefined なので、この関数はどちらの引数に対しても正格である。したがって、どちらの引数も呼び出す前に評価してしまって構わないことが分かる。

正格性の計算方法

お次はこの正格性の情報を具体的にどうやって計算するか。方法は幾つかあるのだけど、私がちゃんと読んだことがあるのは「Strictness analysis — a practical approach」(Chris Clack and Simon L Peyton Jones)という論文だけなので、これを簡単に紹介する。

• <URL:ftp://cs.ucl.ac.uk/functional/papers/Published/strict.ps.gz>
• <URL:http://www.springerlink.com/content/f066h27646531051/>

この論文の方法は、通常の値を「絶対に停止しない事を表す値0」と「停止するかもしれない事を表す値1」の二値からなる領域{0,1}で解釈し、関数をこの領域の上の関数として解釈するという手法を使っている。値からこの領域上への関数を ABS と書くことにする。

関数 f に対して、この領域上で解釈した関数 f# は ABS (f x) = f# (ABS x) を満たす。これは「計算後に抽象化したもの」が、「抽象化してから抽象化した領域の上で計算した結果」と一致するということを言っていて、抽象化に求められる条件になっている。

例えば以下のような関数を考える。ただし、if' p t e = if p then t else e とする。

• g p q r = if' (p == 0) (q + r) (q + p)

この関数を{0,1}上で解釈した関数 g# に期待される条件を考えると、

• g# (ABS p) (ABS q) (ABS r) = ABS (if' (p == 0) (q + r) (q + p)) = if'# (ABS p ==# ABS 0) (ABS q +# ABS r) (ABS q +# ABS p)

となる。引数を書き換えると、

• g# p q r = if'# (p ==# ABS 0) (q +# r) (q +# p)

となる。

ここで、0は必ず停止するので ABS 0 = 1。また、「x==y が停止するかもしれない」のは、xが停止するかもしれなくて、かつyも停止するかもしれないときだけなので、(==#) = (&&) となる。同様に (+#) = (&&) 。また、「if' x y z が停止するかも知れない」のは、xが停止するかもしれなくて、かつyとzのいずれかが定義するかもしれないときだけなので、if'# x y z = x && (y || z) となる。

これらを g# の定義に当てはめると、

• g# p q r = (p && 1) && ((q && r) || (q && p)) = p && q && (r || p)

となる。ここから、

• g# 0 1 1 = 0 && 1 && (0 || 1) = 0 なので、pが停止しない場合、q, r が停止しても、全体は停止しない。すなわち、ｇはpに関して正格。
• g# 1 0 1 = 0 なので、qが停止しない場合、p, r が停止しても全体は停止しない。すなわち、gはqに関して正格。
• g# 1 1 0 = 1 なので、rが停止しない場合でも、p, q が停止すれば全体は停止するかもしれないことがわかる。すなわち、ｇはrに関して正格ではない。

ということが分かる。

再帰や高階関数を扱うこともできるけど、それは論文を参照してくださいな。といっても、多分もっと新しい論文を読んだほうが整理されているとは思う。この論文は抽象解釈といいつつ、あまり抽象解釈っぽくないし、もっと整理された論文があるんじゃないかと予想。ただ、この論文は束のフロンティアの概念とそれを利用したアルゴリズムを提案していて、そこは結構面白いと思うんで、読んで損はないと思う。

実験

正格性解析は最適化を有効にすると有効になるけど、 -fstrictness で明示的に有効にしたり、-fno-strictness で明示的に無効にしたりできる。以下のプログラムを -O と -O -fno-strictness でそれぞれコンパイルして比較してみると、違いが分かるはず。

main = print $ sum' 0 [1..10000000]

限界

このように素晴らしい正格性解析なのだけど、いつもうまく行くわけではない。

例えばsum'の定義が

sum' = foldl (+)

だったら、foldlがインライン化されない限り、正格性解析による最適化は期待できない。

というのは、foldlの定義が以下のようなものだとして、cの定義が分からないままでは、cが第一引数に関して正格かどうかわからず、結果としてfoldlもnに対して正格かどうかが分からないため。

foldl :: (a -> b -> a) -> a -> [b] -> a
foldl c n [] = n
foldl c n (x:xs) = foldl' c (c n x) xs

昔から思っているんだけど、こういう時って「cが正格なときとcが非正格なときようのコードを両方生成しておいて、さらにcの実行時のクロージャに正格性の情報を格納しておいて、実行時にcの正格性情報を見てどっちのコードか選ぶ」なんてことはできないものなのかな。

追記

Togetter - 「正格性解析 (Strictness Analysis) への反応」 で頂いた反応などをまとめてみます。

他の参加記事へはこちらから

• Haskell Advent Calendar jp 2010
• tt_clownさんによるカレンダーページ