Chapter 31

11. 宣言型プログラミング / 第2部への導入

さのたけと
さのたけと
2021.05.06に更新

原文:1. Declarative Programming

この本の第1部では,圏論もプログラミングもどちらも合成可能性(composability)が主題だということを述べた.プログラミングは,なんとかできるところまで問題を分解しつづけ,それぞれの小問題を順番に解決し,そしてそれらの解をボトムアップに再合成することである.大雑把に言って,これをするには2つの方法がある: 何をするかをコンピュータに伝えるか,あるいはそれをどうやってやるかを伝えるかである.前者を宣言的(declarative)と言い,後者を命令的(imperative)という.

このことは,最も基本的なレベルでさえ見ることができる.合成それ自身は宣言的に定義することができて, hfの後にgを合成したものだと言うことができる:

h = g . f

あるいは命令的に定義することもできて,まずfを呼び出し,その呼出の結果を記憶して,その後その結果を用いてgを呼び出すということもできる:

h x = let y = f x
      in g y

命令型のプログラムは普通,時系列での動作の列として書かれる.特に,gの呼出はfの実行が完了するより先には起こり得ない.少なくとも,それが概念上の描像である --- 遅延評価のある言語,つまり 必要呼び (call by need) での引数渡しを採用している言語では,実際の実行は違ったやりかたで進むかもしれない.

実際,コンパイラの賢さによっては,宣言型のコードと命令型のコードとの間にどう実行されるかの差異はほとんど無いか,あるいは全く無いかもしれない.しかし,どう問題に取り組むかや,出来上がるコードのメンテナンスのしやすさ,テストのしやすさという点で,これら2つの技法は(時折劇的に)異なるのである.

主な疑問は: 問題に直面したとき,我々はそれを解決するために宣言型のアプローチと命令型のアプローチの両方を常に取れるのだろうか?さらに,もし宣言的な解があるなら,それをコンピュータコードに常に変換できるのだろうか?これらの疑問に対する答えは全く自明ではない.もしもそんな答えが見つかったなら,世界への理解が大転換するだろう.

深入りさせてほしい.物理でも似たような双対性があり,それは物理の根底の原理に連なるものであったり,あるいは我々の精神がどう物理を理解するかについて教えてくれるようなものなのだ.リチャード・ファインマンはこの双対性が彼の量子電磁気学での仕事のインスピレーションとなったと言っている.

ほとんどの物理法則は2通りに表現することができる.1つは局所的,言い換えるなら無限小的(infinitesimal)な思考を用いる.この思考では,我々は系の状態の小さな近傍に注目し,次の瞬間にそれがどう発展するかを予測する.これは普通,時間の区間にわたって積分したり合計したりしなければいけないような微分方程式で表現される.

このアプローチは命令型の思考に似ていることに注意しよう: 我々は最後の解に,小さなステップの列を順に追っていくことによってたどりつく.それらのステップはそれぞれ,1つ手前のステップの結果に依存しているのである.実際,物理系のコンピュータシミュレーションは,微分方程式を差分方程式に変換して,その差分方程式を反復するというお決まりの方法で実装されている.これはアステロイド[1]で宇宙船を動かすのと同じやりかたである.各時間ステップで,宇宙船の位置は小さな増分を足すことによって変化させられ,その増分は速度に微小時間を掛け合わせることによって計算される.速度はというと,これは加速度に比例する小さな増分によって変化させられ,その加速度は力を質量で割ることによって計算される.

ニュートンの運動法則に対応する微分方程式

\begin{aligned} F &= m \frac{dv}{dt} \\ v &= \frac{dx}{dt} \end{aligned}

の直接のエンコーディングがある.似た方法がもっと複雑な問題にも適用できる: たとえばマクスウェルの方程式を使って電磁場の伝播を計算することもできるし,格子QCD(lattice QCD)を使って陽子の中のクォークとグルーオンの振舞さえも計算することができる.

デジタル計算機の使用によってやりやすくなった,時間と空間を離散化するこの局所的な考え方は,世界全体の複雑性をセルオートマトンの系に帰着させるステファン・ウルフラムの勇敢な試みにその極致を見ることができる.

もう1つのアプローチは大域的なものである.その系の最初と最後の状態を見て,ある汎関数を最小化することによってそれらを繋ぐ経路を計算する.一番単純な例はフェルマーの最小時間の原理である.この原理は,光線はその滞空時間を最小化するように伝播するということを言っている.特に,反射させたり屈折させたりする物体がない場合には,点Aから点Bに進む光線は最短経路を通り,その最短経路というのはつまり直線である.しかし,光は密な(そして透明な)物体の中ではゆっくり伝播する.なので,もし始点を空気中に選んで,終点を水中に選んだなら,光にとっては空中を長く移動し,水中では近道をするのがより有利になる.この最小時間の経路を通るために光線は空気と水との境界で屈折し,スネルの屈折の法則が導かれる:

\frac{sin(\theta_1)}{sin(\theta_2)} = \frac{v_1}{v_2}.

ただし,v_1は空気中での光の速さであり,v_2は水中での光の速さである.

古典力学は,すべて最小作用の原理から導くことができる.どの軌跡についても,作用はラグランジアンを積分することにより計算することができる.ただし,ラグランジアンは運動エネルギーとポテンシャルエネルギーとの差である(注意: 和ではなく差である --- 和はエネルギーの総和になる).目標に向けて迫撃砲を撃ったなら,砲弾は最初は上昇し,それによって重力に由来するポテンシャルエネルギーを高くし,そこで時間をつぶして作用に負の貢献をする.砲弾は放物線の頂点で減速し,運動エネルギーを最小化する.その後,ポテンシャルエネルギーが低いところを早く駆け抜けるために,砲弾は加速する.

ファインマンの最も偉大な貢献は,最小作用の原理が量子力学に一般化できるということに気づいたことであった.問題は再び,初期状態と最終状態によって定式化される.遷移の確率を計算するために,それらの状態の間についてファインマンの経路積分が用いられる.

重要なのは,物理法則を記述するとき,説明のできないような奇妙な双対性があらわれるというところである.我々は,物事が順番に小さい増分ずつで起こるような局所的な描像を使うことができる.あるいは,初期状態と最終状態を宣言して,その間のことは全てそれらに付き従うだけであるという大域的な描像を使うこともできるのだ.

この大域的なアプローチはプログラミングでも使うことができる.例えば,レイトレーシングを実装するときがそうである.我々は目の位置と光源の位置とを宣言した上で,それらを繋ぐ光線の通り道を見つければよい.このために明示的に光線の飛行時間を最小化するということはしないが,同じ趣旨でスネルの法則と反射の幾何学を使うことはする.

局所的なアプローチと大域的なアプローチとの間の一番大きな違いは,空間,そして(こちらのほうがより重要だが)時間の扱いにある.局所的なアプローチはここ,そして今の即座の享楽を大事にするが,他方,大域的なアプローチは長期的で静的な視座に立ち,あたかも未来は運命付けられているかのように永遠の宇宙の性質を解析するだけなのである.

このことは,ユーザインタラクションへのアプローチである FRP (Functional Reactive Programming) において最もよくあらわれている.起こりえるユーザアクションすべてに対して分離したハンドラ(何らかの可変な共有状態にアクセスできる)を書く代わりに,FRPは外部のイベントを無限リストとして扱い,変換の列をそれに適用する.概念的には,未来におこるアクションすべてがそこにあり,プログラムに対する入力データとして利用可能である.プログラムの観点からすると,円周率\piの桁の列も,乱数の列も,ハードウェアから来るマウスの位置の列も何ら変わりない.どの場合も,もしn番目が欲しいのなら,最初のn-1個を読み飛ばす必要がある.これが時系列のイベント列に適用されるとき,この性質は 因果性 (causality) と呼ばれる.

一体これが圏論と何の関係があるのだろう?私は,圏論が大域的なアプローチを推し進め,宣言的プログラミングの支えになるのだということを言いたい.まず始めに,圏論には微積分学と違って備え付けの距離や近傍や時間の概念はない.あるのは抽象的な対象と,それらの間の抽象的な繋がりだけだ.もしAからBまで何歩かで行けるのなら,そこには1歩でも行くことができる.さらに,圏論での重要な道具は普遍的構成(universal construction)であり,これは大域的なアプローチの典型である.我々はこのことを実際に,例えば圏論的な直積の定義で見てきた.この定義は性質を指定することによって行なわれる --- まさに宣言的なアプローチだ.直積は2つの射影を備えており,さらにそのような対象のうち一番良いものである --- つまりある性質を最適にするようなものであり,その性質とはそのような他の対象の射影を分解するというものだ.

このことを,フェルマーの最小時間の原理や最小作用の原理と比べてみてほしい.

反対に,この定義を(ずっと命令的な)カルテジアン積の昔ながらの定義と比較してみよう.その直積の元をどうやって作るかを,1つの集合から元を取ってきて,さらにもう1つの集合からもう1つの元を取ってくることによって記述することになる.これがペアを作るためのレシピだ.さらに,ペアを分解するためのレシピもある.

ほとんどのプログラミング言語(Haskellのような関数型言語を含む)では,直積型,直和型,そして関数型は組み込みであり,それらが普遍的構成で定義されることはない.そういう圏論的なプログラミング言語を作ろうという試みもあるけれども[2]

直接的に使われるにせよそうでないにせよ,圏論的な定義はすでに存在するプログラミングでの構成を正当化し,新しいものを生み出してくれる.一番重要なことは,圏論はコンピュータプログラムについて宣言的なレベルで論じるためのメタ言語を提供してくれることである.さらに,コードに落とす前に問題の仕様について論じることを促してもくれる.

(和訳:@ashiato45

脚注
  1. 訳注: アタリ社のテレビゲーム ↩︎

  2. 原注: 例えば,萩野達也の学位論文を見よ. http://web.sfc.keio.ac.jp/~hagino/thesis.pdf ↩︎