脱関数化を実用する 1

1 背景と導入

一階のプログラムでは、全ての関数に名前があり、それぞれの関数呼び出しでは呼び出す関数を名前で指定している。高階のプログラムでは、関数は無名でありうるし、引数として渡されたり結果として返されたりしうる。ストレイチー [[50](脱関数化を実用する 8#reference50)] が述べたように、関数は、一階のプログラムでは第二級の表示可能な (denotable) 値であり、高階のプログラムでは第一級の表現可能な (expressible) 値である。ここで、第一級の関数が実行時にどのように表現されているか気になるかもしれない。

• 第一級の関数はしばしばクロージャ、つまりコードポインタとそのコードで自由に現れている変数の表示可能な値との組である、表現可能な値を使って表現されている。これはランディンが1960年代半ば [[30](脱関数化を実用する 8#reference30)] に提案した手法である。今日クロージャはイーガーな関数型プログラミングの世界において第一級関数の最も一般的な表現である [[1](脱関数化を実用する 8#reference1),[17](脱関数化を実用する 8#reference17),[32](脱関数化を実用する 8#reference32)] し、オブジェクト指向のプログラムを実装するための標準的な表現でもある [[23](脱関数化を実用する 8#reference23)]。高階論理プログラミングを実装するために使われてもいる [[8](脱関数化を実用する 8#reference8)]。

• その代わりの方法として、高階のプログラムは一階のプログラムへと脱関数化することもできる。これはレナルズによって1970年代初め [[43](脱関数化を実用する 8#reference43)] に提案された手法である。脱関数化されたプログラムでは第一級関数は第一級データ型として表現される――第一級関数は、関数抽象 (function abstraction) の自由変数の値を持つ構成子を使って導入され、対応する構成子をケース式でディスパッチ (dispatch) することで除去される。

• 第一級関数は、関数型プログラムをコンビネーターの集まりに翻訳してグラフ簡約を使うことでも処理される。これはターナーによって1970年代半ば [[52](脱関数化を実用する 8#reference52)] に提案された手法である。この実装テクニックはレイジーな関数型プログラミングの世界において精力的に探求されている [[27](脱関数化を実用する 8#reference27),[29](脱関数化を実用する 8#reference29),[37](脱関数化を実用する 8#reference37),[38](脱関数化を実用する 8#reference38)]。

クロージャへの変換やコンビネータへの変換と比べると、脱関数化はほんの少ししか使われていない。この論文の目的は脱関数化の実用的応用を研究することである。

私たちはまず、2つの具体的な例を使って脱関数化を説明する（[§1.1](脱関数化を実用する 1#section1-1), [§1.2](脱関数化を実用する 1#section1-2)）。1番目のプログラムでは、2つの関数抽象が一度だけ実体化 (instantiate) されていて、2番目のプログラムでは一つの関数抽象が何度も実体化されている。そのあと私たちは脱関数化の特徴を簡潔に説明し（[§1.3](脱関数化を実用する 1#section1-3)）、関連する研究を再検討する（[§1.4](脱関数化を実用する 1#section1-4)）。最後に私たちは、脱関数が答えを与えるいくつかの問いを投げかける（[§1.5](脱関数化を実用する 1#section1-5)）。

1.1 静的な個数のクロージャのある高階のプログラムのサンプル

以下の Haskell プログラムにおいて、auxは第一級関数を渡され、その関数を1と10に適用し、結果を足し合わせる。main'関数はauxを2回呼び出し、結果を掛け合わせる。すべてを考慮すると、2つの関数抽象がこのプログラムで、つまりmain'で現れる。［元論文では ML のコードであるが、このページではすべて Haskell のコードに直している。それに合わせて文章に最小限の修正を施している。］

aux :: (Int -> Int) -> Int
aux f = f 1 + f 10

main' :: (Int, Int, Bool) -> Int
main' (x, y, b) = aux (\z -> x+z) * aux (\z -> if b then y+z else y-z)

このプログラムを脱関数化するには、2つの構成子があるデータ型（それぞれの関数抽象のためのもの）、そして関連している適用関数を定義する必要がある。1番目の関数抽象は1つの自由変数（整数型のx）を持つので、1番目のデータ構成子は整数を必要とする。2番目の関数抽象は2つの自由変数（整数型のyとブール型のb）を持つので、2番目のデータ構成子は整数とブール値を必要とする。

ゆえにmain'において、1番目の第一級関数は1番目の構成子と値xを使って導入され、2番目は2番目の構成子と値yとbを使って導入される。

auxにおいて、関数の引数は第二級関数applyに渡され、2つの構成子をディスパッチするケース式を使って除去される。

data Lam = Lam1 Int
         | Lam2 Int Bool

apply :: (Lam, Int) -> Int
apply (Lam1 x, z)   = x+z
apply (Lam2 y b, z) = if b then y+z else y-z

aux_def :: Lam -> Int
aux_def f = apply (f,1) + apply (f,10)

main_def :: (Int, Int, Bool) -> Int
main_def (x,y,b) = aux_def (Lam1 x) * aux_def (Lam2 y b)

1.2 動的な個数のクロージャのある高階のプログラムのサンプル

PPDP のあるレビュワーは、新しいクロージャを「動的に生成する」プログラムではどうなるか、そしてそのようなプログラムは新しい定数を生むから拡張可能なケース式を必要とするのか、という疑問を投げかけた。以下の例を使って、そのような状況について説明し、新たな定数も新たな拡張可能ケース式も必要でないということを示す。

以下の Haskell プログラムにおいて、auxは2引数を渡されて、一方を他方に適用する。main'関数は数iと数のリスト[j1,j2,...]を与えられて、数のリスト[i+j1,i+j2,i+j3,...]を返す。一つの関数抽象\i -> i+jがこのプログラム（main'）で一度だけauxの2番目の引数として現れる。長さnのリストの入力を得たならば、関数抽象は計算全体でn回実体化される。

aux :: (Int, Int -> Int) -> Int
aux (i, f) = f i

main' :: (Int, [Int]) -> [Int]
main' (i, js) = walk js
  where
    walk []       = []
    walk (j : js) = aux (i, \i -> i+j) : walk js

このプログラムを脱関数化するには、1つの構成子しかないデータ型（関数抽象は1つしかないので）と関連する適用関数を定義すればよい。この関数抽象は1つの自由変数（整数型のj）を含んでいるので、データ型の構成子は整数を必要とする。

main'において、第一級の関数は構成子と値jを使って導入される。

auxにおいて、関数の引数は第二級関数applyに渡され、そこで構成子をディスパッチするケース式によって除去される。

data Lam = Lam Int

apply :: (Lam, Int) -> Int
apply (Lam j, i) = i+j

aux_def :: (Int, Lam) -> Int
aux_def (i, f) = apply (f, i)

main_def :: (Int, [Int]) -> [Int]
main_def (i, js) = walk js
  where
    walk []       = []
    walk (j : js) = aux_def (i, Lam j) : walk js

長さnのリストの入力が与えられたならば、構成子Lamは計算全体でn回使われる。

1.3 脱関数化とはつまり

高階のプログラムにおいて、第一級関数は関数抽象の実体として生まれる。プログラム全体で現れるこれらの関数抽象は、すべて列挙することができる。ゆえに脱関数化は関数型がプログラム内の関数抽象の列挙へと置換される、プログラム全体の変換なのである。

したがって脱関数化の起源は型理論にある。実際、関数型は環境からの型の推測を隠すのであり、南出・モリセット・ハーパーによって型付きクロージャ変換 [[32](脱関数化を実用する 8#reference32)] についての研究で指摘されたように、これらの推測を明示するには存在型が必要なのだ。プログラム全体を扱う場合、この存在型は有限和、そして対応する入射とケースディスパッチ (case dispatch) によって表すことができ、この表現がまさに脱関数化の獲得するところのものなのである。

こうした型理論的起源は、レナルズの Algol についての言葉 [[47](脱関数化を実用する 8#reference47)] を言い換えると、脱関数化を何の拘束にもしていない。例えば（ベル・ベルガルド・フックによる研究 [[4](脱関数化を実用する 8#reference4)] のように、型ごとにグループ化するなどして得られる）いくつかの適用関数を使うこともできる。また（[§3](脱関数化を実用する 3#section3) のように、継続だけを対象とするなどして）プログラムを選択的に脱関数化することもできる。さらに（バナジー・ハインツェ・リーケの最近の研究 [[2](脱関数化を実用する 8#reference2)] のように）ステックラーとワンドの軽量クロージャ変換に似た軽量脱関数化を想像することすらできるだろう。

1.4 関連研究

元々、レナルズは、高階インタプリタを一階インタプリタに変換するため [[43](脱関数化を実用する 8#reference43)] に脱関数化を考案した。彼はこれをプログラミングのテクニックとして提示したが、プログラミング言語についての彼の教科書において一階の意味論を導出する [[45](脱関数化を実用する 8#reference45), §12.4] 以外の用途では、二度と使わなかった [[44](脱関数化を実用する 8#reference44)]。

それ以来、脱関数化はあまり使われなかったが、使われればそれは一人前の実装テクニックとして使われた。ボンドルフは高階のプログラムを一階の部分評価に合うようにするのに脱関数化を使った [[5](脱関数化を実用する 8#reference5)]。トルマッハとオリーヴァは ML のプログラムを Ada へとコンパイルするために脱関数化を使った [[51](脱関数化を実用する 8#reference51)]。フェガラスは自分のオブジェクト指向のデータベース管理システム、lambda-DB において脱関数化を使った [[18](脱関数化を実用する 8#reference18)]。ワンとアッペルは型安全なガーベジコレクターにおいて脱関数化を使った [[55](脱関数化を実用する 8#reference55)]。また、脱関数化は MLton [[7](脱関数化を実用する 8#reference7)] とボクィストの Haskell コンパイラの重要な部分を成している。

脱関数化はごく最近になってようやく形式化された。ベル・ベルガルド・フックは脱関数化が型を保存することを示した [[4](脱関数化を実用する 8#reference4)]。ニールセンは脱関数化の正しさを表示的意味論を使って部分的に証明した [[35](脱関数化を実用する 8#reference35),[36](脱関数化を実用する 8#reference36)]。バナジー・ハインツェ・リーケは脱関数化の正しさを操作的意味論を使って完全に証明した [[2](脱関数化を実用する 8#reference2)]。

1.5 この研究

関数型プログラミングは、fold のような、通常補助的な (auxiliary) 再帰関数を使う再帰下降 (recursive descent) を使うように推奨する。しばしばこれらの補助関数は、終域 (co-domain) が関数空間になっているという点で高階である。たとえば、補助関数が型aの蓄積引数を持つ場合、その終域はあるbについてa -> bとなっている。別の例を挙げると、補助関数があるbについて型a -> bの継続である場合、終域は(a -> b) -> bである。これらの関数型のプログラムは一階の、データ構造指向のアプローチを使って書かれたプログラムと比べると、どのような違いがあるだろうか？

ワンドの継続ベースのプログラム変換に関する定評のある研究 [[54](脱関数化を実用する 8#reference54)] は、「データ構造の継続は何か？」という疑問に動機付けされた。ワンドの論文で熟考されているそれぞれの例は、継続を表すためのデータ構造を設計するためのヒラメキ (eureka step) が必要である。このようなヒラメキは常に必要なのだろうか？

継続は、計算の残りの関数的表現として、あるいは計算の環境の関数的表現として [[20](脱関数化を実用する 8#reference20)]、様々な方法で提示されている。ワンドの研究は前者の見方をしていたから、私たちは後者の見方を考えてみよう。例えば、自らの博士論文 [[19](脱関数化を実用する 8#reference19)] において、フェライゼンは「評価環境 (evaluation context)」と「式の環境への差し込み (plugging expressions into contexts)」という一階の概念に頼った意味論への構文的な取り組みを発展させた。これらの一階の概念は継続の概念と比べてどのような違いがあるのだろうか？

私たちは、この論文のこれ以降において、脱関数化がこれらの問いすべてに一つの答えを提供するということを示す。私たちが考えていくプログラムはすべて再帰下降を行い補助関数を使う。この補助関数が高階ならば、脱関数化は蓄積引数のある一階のバージョンを生み出す（例：[§2.1](脱関数化を実用する 2#section2-1) の木の平坦化と [§2.2](脱関数化を実用する 2#section2-2) のリストの反転）。この補助関数が一階ならば、私たちはこの関数を継続渡しスタイルへと変換する。ゆえに脱関数化は、データ構造の形の蓄積引数を持つ、反復的な (iterative) 一階のバージョンを生み出すのだ（例：[§3.1](脱関数化を実用する 3#section3-1) の文字列のパースと [§5](脱関数化を実用する 5#section5) の正規表現のマッチ）。また、私たちは2つの構文論に対する解釈器を考え、それらの解釈器が脱関数化された形で書かれていることを確認する。そののち私たちはそれらを「再関数化 (refunctionalization)」し、継続が対応する構文論の評価環境を表現するような、継続渡しの解釈器を取得する（[§4](脱関数化を実用する 4#section4)）。

＊ ＊ ＊

更に私たちは脱関数化とチャーチ符号化 (Church encoding) が双対な目的を持っていることに気付いている（チャーチ符号化はデータ構造を高階な関数を使って表現する古典的な手法だからである）。チャーチ符号化されたデータ構造を脱関数化した結果は何だろう？そしてその脱関数化した結果を更にチャーチ符号化したら何が得られるだろう？

同様に、私たちはバックトラッキングが、あるいは1,2個のスタックのある一階の状況において、あるいは1,2個の継続のある高階の状況において実装されるということに気付いている。スタックをチャーチ符号化し継続を脱関数化した結果は何なのかと疑問に思うのは全く自然なことだ。これらのプログラムの正当性証明 (correctness proof) についても疑問に思いうるだろう――両者はどのような違いがあるのか、と。

この論文のこれ以降ではこれらの問いにも答える。私たちは中間リスト (intermediate list) の高階表現を使った2つのプログラムを脱関数化し、2つの効率的で伝統的な一階のプログラムを得る（[§2.2](脱関数化を実用する 2#section2-2)）。また、私たちはチャーチ符号化と脱関数化が互いに逆であるとどの程度みなすことができるのかも明らかにする（[§2.3](脱関数化を実用する 2#section2-3),[§2.4](脱関数化を実用する 2#section2-4),[§2.5](脱関数化を実用する 2#section2-5)）。最後に、私たちは脱関数化の前後で正規表現のマッチャーとその証明を比較対照する（[§5](脱関数化を実用する 5#section5)）。