日々の流転

λ. 正格性解析 (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さんによるカレンダーページ