このブログの更新は Twitterアカウント @m_hiyama で通知されます。
Follow @m_hiyama

メールでのご連絡は hiyama{at}chimaira{dot}org まで。

はじめてのメールはスパムと判定されることがあります。最初は、信頼されているドメインから差し障りのない文面を送っていただけると、スパムと判定されにくいと思います。

参照用 記事

プログラムの実行時間を計る事と半環の代数

零の概念とmax-plus半環の紹介」において:

max-plus半環やmin-plus半環の計算技術は、トロピカル代数(tropical algebra、より一般にはエキゾチック代数)と呼ばれたりします。[...snip...] 例えば、プログラム意味論に計量的な要素を入れるとき、トロピカル代数が使えそうです。

実際にトロピカル代数を使ってプログラムの実行時間を計って*1みます。 「零の概念とmax-plus半環の紹介」で導入した概念は断りなしに使います。内容はまだ生煮えなところがあります。

内容:

プログラムのモノイドとプログラムの半環

p, q などはプログラムを表すとします。プログラムの全体をMとします。当然に、その「プログラム」ってのは何だ? という話になりますが、今は詮索しないで、p∈M と書いてあったら「pはプログラム」と読んでください。

pとqがプログラムのとき、pの後にすぐqを実行する直列結合(逐次実行)を p;q で表します。eは何もしないプログラムとします。すると、次のモノイド法則が成立します。

  • (p;q);r = p;(q;r)
  • e;p = p;e = p

ここでまた、プログラムのあいだの「イコール」ってのは何だ? という話になりますが、(以下略。そういうわけで、(M, ;, e) はモノイドです。プログラムのモノイドです。

⊥を、無限ループして永久に戻ってこないプログラムとします。すると:

  • ⊥;p = p;⊥ = ⊥

つまり、⊥はモノイド演算「;」に対する吸収元です。よって、(M, ;, e, ⊥) は吸収元付きモノイドとなります。

Mの要素を有限個取ってきて、形式的な和をつくります。p1, p2, ..., pn ∈M に対して、p1 + p2 + ... + pn のような形を考えるわけです。この形式的な和の意味は、「p1, p2, ..., pn のなかのどれか1つが実行されるプログラム」ということです。非決定性の選択的実行ですね。足し算の記号「+」を使うより、縦棒を使って p1 | p2 | ... | pn と書いたほうが選択の感じが出るかも知れません。

上記の形式和の全体をRとしましょう。Mの要素pは、ただ1つの項を持つ和と解釈できるので、自然に M⊆R とみなせます。0個のMの要素からなる和(空な式)は0と書きます。Rの0を⊥と同一視することが普通ですが、今回は別物としておきます。0は加法的零で、⊥は乗法的零です。常識的には加法的零と乗法的零は一致しますが、一致する必然性はありません(「零の概念とmax-plus半環の紹介」参照)。

R内での演算「;」は、分配法則が成立するように定義します。すると、Rの計算で次が成立します。

  1. (p + q) + r = p + (q + r)
  2. p + 0 = 0 + p = p
  3. p + q = q + p
  4. p + p = p (足し算のベキ等性)
  5. (p;q);r = p;(q;r)
  6. e;p = p;e = p
  7. ⊥;p = p;⊥ = ⊥
  8. p;(q + r) = p;q + p;r
  9. (p + q);r = p;r + q;r

これらの法則を満たす (R, +, 0, ;, e, ⊥) をプログラムの半環だとします。非決定性の繰り返しを表すクリーネスター p* を加えれば、プログラムの半環はクリーネ半環(クリーネ代数)になります。ただし、通常のクリーネ半環では 0 = ⊥ を仮定します。

プログラムの実行時間

プログラムpをなんらかの実行環境で実行するとして、とある固定した実行環境での実行時間を τ(p) とします(τはギリシャ文字タウ)。時間の計測単位を決めれば、τ(p) は非負の実数としていいでしょう。無限走行するプログラム(終わらないプログラム)も考慮して、τ(p) = ∞ も認めます。

P = {x∈R | 0 ≦ x }∪{∞} とします(この記法の問題点は「零の概念とmax-plus半環の紹介」の注釈を参照)。実行時間τは、τ:R→P という写像となります。

まず、逐次実行に関しては、次の性質を持つべきだと考えられます。

  1. τ(p;q) = τ(p) + τ(q)
  2. τ(e) = 0
  3. τ(⊥) = ∞

eは、ほんとに何もしないことであって、何の出力も効果もないけど時間は消費するタイムフィラーではありません。時間ゼロで実行されるプログラムはeに限るでしょうから、次の条件は妥当でしょう。

  • τ(p) = 0 ならば p = e

同じように、次の条件を入れてもいいかも知れません。

  • τ(p) = ∞ ならば p = ⊥

次に、プログラムの足し算に関する実行時間を考えてみます。τ(p + q) の値はどうあるべきでしょう。足し算 p + q の意味は、非決定性の選択的実行なので、pが実行されるかqが実行されるか事前には分かりません。長い方の実行時間により評価するなら、

  • τ(p + q) = max{τ(p), τ(q)}

となります。これは、悪い方のケースを想定しています。一方、楽観的に良い方のケースを想定するなら、

  • τ(p + q) = min{τ(p), τ(q)}

ですね。当然ながら、この2つはまったく違った結果となります。e + ⊥ (何もしないか、無限ループのどちらか)というプログラムに対して、次のようになります。

  • τ(e + ⊥) = max{τ(e), τ(⊥)} = max{0, ∞} = ∞
  • τ(e + ⊥) = min{τ(e), τ(⊥)} = min{0, ∞} = 0

実行時間の計測値となる半環

プログラの足し算(非決定性の選択的実行)に対して、悪い方のケースで評価するとして、実行時間が満たす法則を書き並べてみましょう。

  1. τ(p;q) = τ(p) + τ(q)
  2. τ(e) = 0
  3. τ(⊥) = ∞
  4. τ(p + q) = max{τ(p), τ(q)}

イコールの右側を「零の概念とmax-plus半環の紹介」で導入したmax-plus半環の記法で書き直してみると:

  1. τ(p;q) = τ(p)\odotτ(q)
  2. τ(e) = ι (ι = 0)
  3. τ(⊥) = ∞ (∞は掛け算の吸収元)
  4. τ(p + q) = τ(p) \oplus τ(q)

写像τが、プログラの半環 (R, +, 0, ;, e, ⊥) を、max-plus半環 (P, \oplus, θ, \odot, ι, ∞) に写す準同型写像になっていることが分かります。足し算の中立元(加法的零)も対応するはずなので、次も成立すべきです。

  • τ(0) = θ (θ = 0)

実行時間の値の領域にmax-plus半環を使うときは、加法的零である0と乗法的零である⊥を同一視するのはマズイことが分かります。だって、τによる値がまったく異なりますもの。

  • τ(0) = 0
  • τ(⊥) = ∞

一方で、実行時間の値の領域にmin-plus半環を使うなら、0と⊥を同一視することができます。min-plus半環における足し算の中立元は∞でした。τ(0) = ∞ は、τが加法構造の準同型写像であるなら必然です。もし「τ(p) = ∞ ⇔ p = ⊥」を仮定するなら、「0 = ⊥」を導くことができます。

ゼロ(加法的零)とボトム(乗法的零)を同一視するなら、実行時間評価に楽観的立場を取ることが強制されます。ただし、max-plus半環、min-plus半環以外にも選択肢はあります(次節を参照)。

もっと精密に実行時間を記録するには

p1 + p2 + ... + pn という形式的な和で与えられるプログラの実行時間は、τ(p1), τ(p2), ..., τ(pn) のどれかになります。最大値または最小値で評価するのは荒っぽすぎる気もします。すべての実行時間の値の集合 {τ(p1), τ(p2), ..., τ(pn)} をそのまま扱ったほうが精密になるでしょう。

今まで τ:R→P でしたが、τを集合値写像に拡張します。τ:R→Powf(P) とします。ここで、Powf(P) は、集合Pの有限部分集合全体からなる集合です。有限性の条件を落として、τ:R→Pow(P) (Powはベキ集合)としても大差ないですが、有限なら集合を完全に書き下すことができます。

実行時間の計測結果は、Powf(P)の要素(つまり、非負実数値の有限集合)として記録することになりました。Powf(P)にも足し算と掛け算を導入して、実行時間を計る写像τを半環の準同型写像としたいものです。

Powf(P)の足し算と掛け算は素直に考えれば定義できます。足し算のほうが簡単です。次の性質が欲しいですよね。

  • τ(p + q) = τ(p)∪τ(q)

であるなら、Powf(P)の足し算は集合の合併にすればいいのです。

掛け算は、

  • τ(p;q) = τ(p)・τ(q)

となるような演算「・」が欲しい、と。そのためには、A, B∈Powf(P) に対して、次の定義をします。

  • A・B = {z∈P | x∈A, y∈B があって z = x + y}

実はこの定義、形式言語理論における「言語の掛け算」の定義と同じです。形式言語理論では、アルファベットから自由生成された自由モノイドを使いますが、今回は非負実数の足し算のモノイドがベースになっています。より一般的には、モノイドの畳み込み半環における掛け算の定義です。

Powf(P)に足し算(集合の合併)と掛け算(畳み込み積)を入れると、プログラムの実行時間計測写像τは次の性質を持つことになります。

  1. τ(p;q) = τ(p)・τ(q)
  2. τ(e) = {0}
  3. τ(⊥) ={∞}
  4. τ(p + q) = τ(p)∪τ(q)
  5. τ(0) = \emptyset\emptyset空集合

Powf(P)では、\emptysetが加法的零(中立元)かつ乗法的零(吸収元)です。{∞}はほとんど吸収元ですが、\emptysetには負けます。\emptysetを除いたPowf+(P)で考えたほうが辻褄が合うかも知れません(ここらへん生煮え)。

まだ精密さが足りないと思うなら

実行時間の計測結果を、値の集合に拡張しました。しかしこの方式では、「τ(p) = {1}, τ(q) = {2}」と「τ(p) = {1, 2}, τ(q) = {1, 2}」のどちらでも「τ(p + q) = {1, 2}」になってしまいます。実行時間の広がりは分かりますが、広がりのなかの濃い薄いの情報がありません。

単なる値の集合ではなくて、値に重みを付けたものを考えればいいでしょう。重みとして、{0, 1, 3, ...} という離散的個数を取ることもできますし、[0, 1] という相対比率を表す区間を取るのもよいでしょう。そうすると、τの値は実行時間の統計的分布(あるいは確率密度)になるでしょう。有限離散値を連続分布にまで拡張してもかまいません。

プログラムpの実行時間計測を、単一の実行環境ではなくてn個の環境で行うとすると、ベースとなるモノイドはPから直積モノイド(P)nになります。実行時間計測写像τの値は、多次元空間上の分布になります。並列実行を考える際も、(色々なnに対する)(P)nが必要になるでしょう。

いずれにしても、半環と半環の準同型写像が背後にあることは分かると思います。プログラムのモノイド/半環をプログラムの圏に拡張することは難しくありません。そのとき、τは関手になります。プログラムの圏にトレースを導入して、クリーネスターも真面目に考えれば、関手τに関して、おそらくパリクの定理の類似が成立するでしょう。

と、まー、プログラムの実行時間にも色々な代数構造が潜んでいるのでした。

*1:「計る」と「測る」のどっちがふさわしいのだろう?