いものやま。

雑多な知識の寄せ集め

「Lucid, the Dataflow Programming Language」を翻訳してみた。(その12)

前回の続き。

2.7 遅延評価

しかし、Iswimの操作的(動的)解釈として、より適切なものがある。
この方法論では、プログラムは実行されると考えるのではなく、プログラムは評価されると考え、その評価は必要に応じて行われるとする。
この評価の方法は、必要以上には評価を行わない(=必要になったときに必要なだけ評価を行う)ので、「遅延」と呼ばれる。
特に、関数呼び出しの実引数は自動的には評価されない。
この遅延評価の方法は、数学的意味論により忠実となっている。
実際、ちょっとした注意を払うことで、それらは完全に正しいものになり、形式的意味論が指定するものを正確に生成する。

これらのうちの最初のものは、「要求駆動(demand-driven)」解釈と呼ばれるかもしれない。
この方法では、プログラムの一部(最初はプログラム全体)の値に対する要求が、部分式の値に対する要求を生成する。
要求は感染症のようにプログラム全体に伝播していき、必要とされた値が要求元へと流れ返っていく。
2つの部分式 E_1 E_2の合計 E_1 + E_2を評価するために、評価マシンは E_1 E_2を(おそらく並行して)評価し、それらの結果を加算する。
個々の定数からなる式を評価するために、評価機は代数によって定数に割り当てられた値を返す。
個々の変数からなる式を評価するために、評価機は変数の適切な定義を検索し、その定義の右辺を評価する。
対象の変数が関数定義の仮引数である場合、対応する実引数を探し出してきて、それを評価する。
評価する式が if  C then  E_1 else  E_2 fiという形式であれば、まず Cを評価して、その真偽値にしたがって、 E_1 E_2のいずれかを評価する。
最後に、(例えば) f(E_1, E_2)という形式の式を評価するなら、 fの定義を見つけ出し、その右辺を評価する。

もちろん、要求駆動型の評価は、上記のざっくりした説明が示すよりも、もう少し複雑である。
それにもかかわらず、実装することはそれほど困難というわけではなく、完全に正しい。
(付録のマニュアルに記述されているpLucidインタプリタは、要求駆動の評価スキームを使用している;そして、Iswim( P)はpLucidの部分言語である)
(※データフロー言語の実装を考えるとき、pull型(シンク側から要求を出し、それに応じてソース側が計算を行う)とpush型(ソース側で計算を行い、結果をシンク側に流してシンク側を駆動させる)を考えることができるけど、この要求主導というのはpull型だという主張。実際の実装がそうなっているのかは未確認・・・)
要求駆動型のモデルは、プログラミングを助けるうえで、適切なものとなっている。
要求駆動型の観点では、定義が実行可能な順序で現れてくる必要はない。
実際、この方法だとプログラムを書くときによりトップダウンな形で書くことが出来る。
まず、欲しい出力の値となる式を書く(そこで使われる変数や関数の定義は書かない)。
この式はwhere節の主題になる。
次に、where節の本体に、必要に応じて主題で使われる変数の定義を書いていく。
したがって、要求駆動のインタプリタは、書かれたのと同じ順序で定義を進めていく(これはインタプリタにとって特別な助けになるというわけではない)。
この「必要に応じて定義する」アプローチは、プログラミングのスタイルをずっと良くし、Iswimの定義型の精神により合っている。

Iswimプログラムを実装する非逐次的な別の方法もある。
そのアイディアは、第7章で議論されるプログラム操作の規則を使用するもので、ソースプログラムを徐々に出力に変換していくものである。
変換方法は、プログラムの定義を書き換え規則として使用する。
実行する簡約(reduction)を選択する戦略が慎重に定義されている場合、実装は必要とされない式の値を評価しようとはしない。

この方法(簡約計算)は非常にシンプルであるが、プログラミングの助けとして無制限に推薦することは出来ない。
中間表現は非常に大きく、複雑になり、元のプログラムとの関係がほとんどなくなる。
この方法は主に構文的であり(※ここでの「構文的」というのは、記号操作的、という意味合いだと思う)、構文に関して排他的に考えるプログラマは、Iswimの意味論を理解するという利点を失う。
プログラマは、関数定義を「関数」ーーすなわち、データを変換する「デバイス」ーーの定義と考えるべきである。
定義をテキストを変換する書き換えルールと考えることはお勧めしない。
記号操作というより、計算であると考えたほうがいい。
(※ラムダ計算の理論では、定義による置換を行うことで計算が出来るとしていて、その置換の戦略によって遅延評価かそうでないかが変わってくる。ここで述べているのはその簡約による方法)

これらの代替操作的モデルは、どちらも \perpの意味をそれぞれの方法で大事にしている。 例えば、次のような定義を考えてみる:

X = X + 1;

要求駆動のインタプリタは、 Xの値に対する要求が Xに対する別の要求に直接つながるため、(要求が)無限に循環することになる。
そして簡約の実装は、 X X + 1に無限に置き換えることで、以下の系列を生み出すことになる:

 X +1, (X +1)+1, ((X +1)+1)+1, \cdots

どちらの場合も、計算は決して終わることなく、これはまさに \perpに対応する操作的な活動になっている。

最後に、プログラマは動的モデルをまったく使用しないことを望むかもしれないということを指摘しておく。
Iswimの最大の強みは、公式での意味論が厳密に静的であり、よく理解されている関数の概念を使用していることである。
プログラマがプログラムの効率(性能)を心配していない場合、実際の操作的な概念を考える必要はまったくない。
プログラマがもっぱら正しさにだけ関心を持つ場合、静的な意味論はプログラムの出力を完全に指定するので、静的な意味論だけで十分である。

しかし、一般的に、プログラマは性能に関する質問を無視できない(そうでなければ、プログラムはなく、仕様のみがあることになる)。
プログラマは、いくつかの操作上の観点から思考し、それを実行するのに必要なリソースの量を減らすようにプログラムを作らなければならない。
しかしこれは、プログラマは実装のあらゆる細かい部分について心配する必要があるだとか、実装のあらゆる部分の動作について理解している必要があるだとか、そういうことではない。
とても実用的なプログラミングでさえ、純粋に宣言的に理解されている部分があるだろう。
さらに、最も実用的で効率的なプログラムでさえ、その正しさは、表示的な(静的な)意味にのみ依存し、操作的なアイディアを参照することなく考えることが出来る。
「抽象性」という用語は、本質的に表現または実装の問題から独立であることを意味する。
したがって、Iswimの形式的で表示的な意味論は抽象的な意味論であり、この言語を使用したいと思う人であれば誰でも理解できるものである。


ということで、遅延評価に関して。

この節に書かれてることはとても興味深くて、遅延評価といえばHaskellが有名なわけだけど、Haskellが遅延評価を実現している方法はまさにこの節で書かれている2番目の方法(簡約による方法)で、簡約の戦略を非正格にすることで評価が遅延するようにしている。
一方で、pLucidはそれとは別の方法で遅延評価を実現していると言っていて、それが1番目に書かれた要求駆動による方法。
データフローの視点で考えることで、1番目の方法が出てくるのはとても面白い。

また、データフロープログラミングの後継と言われることの多いリアクティブプログラミングだと、(オブザーバ・パターンによる)push型の実装が多い印象なんだけど、pLucidはそうではなく、pull型の実装になっている、と。
確かに、push型だと遅延評価は無理だけど、pull型なら実装はWorkStealingアルゴリズムみたいに関数呼び出しを一つのタスクとしてスタックにプッシュする感じになりそうなので、遅延評価になりそう。
いやー、なるほどという感じ。

今日はここまで!