非正格関数に対して適用可能な融合変換

修士論文

2006 年度 (平成 18 年度)

非正格関数に対して適用可能な融合変換

Fusion Transformations Applicable to Non-Strict Functions

慶應義塾大学大学院 政策・メディア研究科 酒井 政裕

修士論文要旨

2006 年度 (平成 18 年度)

非正格関数に対して適用可能な融合変換 概要 関数型言語が広範な関心を集めており、関数型言語最適化の手法としてプログラム変換、特に融 合変換の重要性が高まっている。

Haskell のような純粋関数型言語は参照透明であり、未定義な値や停止しない計算を含む参照透 明な言語の数学的モデルは、非正格な関数 (未定義な引数値に対しても値が定義される関数) を含 む圏となる。 しかし、CPO と正格な連続関数の圏では再帰的データ型を始代数として解釈可能であるが、

CPO と (正格なものに制限されない全ての) 連続関数の圏では一般には再帰的データ型を始代数と 解釈できるとは限らない。一方、プログラム変換の中にはデータ型が始代数であることを利用する ものが存在する。そのような変換は対象となる関数が正格である場合に制限されてしまう。 そこで本論文では正格性の条件を必要とせずに変換を行うことを目的として、非正格な関数の存 在する圏であってもデータ型が始代数になるための条件を示す。そのために、一般的な定理として 「圏 C と圏 D の間に関手 F : C → D と関手 G : D → C が与えられたとき、F G : D → C の始代 数が存在することと GF : C → D の始代数が存在することとが同値であること」を示す。そして、 それを用いて「任意の関数 f : A → B に対して F (f ) が常に正格であるならば、F は CPO と連 続関数の圏においても始代数を持つ」ことを示す。関数型言語で通常使われている多くのデータ型 はこの条件を満たす。 さらに、その条件を Haskell におけるデータ型に適用する。また、入れ子データ型が関手圏の変 種で始代数となる条件についても述べる。

キーワード

1 非正格性 2 始代数 3 CPO 4 Haskell 5 融合変換

慶應義塾大学大学院

政策・メディア研究科 酒井 政裕

Abstract of Master’s Thesis Academic Year 2006

Fusion Transformations Applicable to Non-Strict Functions Abstract Functional languages attract broad interest and importance of program transformations (especially fusion transformations) rises as techniques of functional language optimization. Purely functional languages like Haskell are referentially transparent. If a referentialy transparent language contains undefined values or non-terminating computations, its mathematical model is a category that contains non-strict functions: funcions defined on undefined input value. Although recursive data types can be interpreted as initial algebras in the category of CPO and strict continuous functions, in general they cannot be interpreted as initial algebra in the category of CPO and arbitrary continuous functions. On the other hand, some program transformations depend on the initiality of da ta types. Therefore, targets of such transformations are restricted to strict functions. This paper aims to achieve fusion transformations applicable to all functions (not restricted to strict ones). We show an condition which guarantees recursive data types are indeed initial algebras. To prove this, we first show an general theorem: given functors F : C → D and G : D → C, initial algebra of F G : D → C exists if and only if initial algebra of GF : C → D exists. Then we use the theorem to show that initial algebra of F exists in the category of CPO and continuous functions if F (f ) is strict for all f . This condition covers most familiar data types. Additionally, we apply this to data types of Haskell. We also show a condition which guarantees that nested data types are indeed initial algebras in the certain variant of functor category.

Keywords 1 Non-Strictness 4 Haskell

2 Initial Algebra 3 CPO 5 Fusion

Keio University Graduate School of Media and Governance SAKAI Masahiro –i–

目次 第1章

序論

1

研究の背景 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

1

1.1.1

関数型プログラミングと関数型言語 . . . . . . . . . . . . . . . . . . . .

2

1.1.2

融合変換 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

2

1.2

研究の位置づけ . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

4

1.3

本論文の構成 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

5

予備知識

6

2.1

記法について . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

6

2.2

圏論について . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

6

2.2.1

代数 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

9

2.2.2

余代数

. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

10

. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

11

2.3.1

Cpo, 連続関数, 最小不動点 . . . . . . . . . . . . . . . . . . . . . . . . .

12

2.3.2

CPO 圏 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

12

2.3.3

関手 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

13

本章のまとめ . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

15

非正格性と始代数

16

3.1

始代数の普遍性に基づいた融合変換 . . . . . . . . . . . . . . . . . . . . . . . . .

16

3.2

領域理論的な圏での場合の問題 . . . . . . . . . . . . . . . . . . . . . . . . . . .

17

3.3

始代数が存在するための条件

. . . . . . . . . . . . . . . . . . . . . . . . . . . .

19

3.4

具体的なデータ型への適用 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

21

3.5

他アプローチとの比較 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

22

3.5.1

代数のみを正格なものに制限

. . . . . . . . . . . . . . . . . . . . . . .

22

3.5.2

代数と準同型を正格なものに制限 . . . . . . . . . . . . . . . . . . . . .

22

本章のまとめ . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

23

Haskell への適用

24

型宣言と領域方程式 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

24

1.1

第2章

2.3

2.4 第3章

3.6 第4章

4.1

領域理論について

– ii –

4.1.1

data 宣言 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

24

4.1.2

newtype 宣言 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

26

4.2

関手の不動点としての解釈 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

26

4.3

本章のまとめ . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

27

多相関数の圏の場合

28

5.1

高階の多相性と入れ子データ型 . . . . . . . . . . . . . . . . . . . . . . . . . . .

28

5.2

多相関数の圏 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

28

5.3

GADT . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

30

5.4

本章のまとめ . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

31

結論

32

6.1

まとめ . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

32

6.2

今後の課題 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

32

6.2.1

更なる検討 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

32

6.2.2

反変性を扱うよう拡張 . . . . . . . . . . . . . . . . . . . . . . . . . . .

33

6.2.3

処理系への実装 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

33

6.2.4

変換アルゴリズムの導出 . . . . . . . . . . . . . . . . . . . . . . . . . .

33

6.2.5

パラメトリシティ

. . . . . . . . . . . . . . . . . . . . . . . . . . . . .

33

6.2.6

操作的意味論との関係 . . . . . . . . . . . . . . . . . . . . . . . . . . .

33

6.2.7

正格性と非正格性の組み合わせについて . . . . . . . . . . . . . . . . . .

34

第5章

第6章

謝辞

35

参考文献

36

– iii –

図目次 1.1

変換の列からなるプログラム

. . . . . . . . . . . . . . . . . . . . . . . . . . . .

3

2.1

合体直和、持ち上げ、分離直和 . . . . . . . . . . . . . . . . . . . . . . . . . . .

15

3.1

最終的な可換図式の全体 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

20

3.2

cata-Fusion の適用 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

21

4.1

data 宣言の文法 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

24

– iv –

表目次 4.1

Tree 型の各定義の性質 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

26

6.1

プログラミング言語・計算体系・圏論理の関係 . . . . . . . . . . . . . . . . . . .

34

–v–

リスト目次 1.1

関数定義の例 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

4.1

data 宣言による木のデータ型の定義

. . . . . . . . . . . . . . . . . . . . . . . .

25

5.1

高階の型引数を持つデータ型の例 . . . . . . . . . . . . . . . . . . . . . . . . . .

28

5.2

入れ子データ型の例 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

28

5.3

GADT . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

30

– vi –

3

第1章

序論

概要 本章では本論文の背景・目的および構成について述べる。まず背景を述べ，問題点について言及 する。そして，その問題点を解決するためのアプローチについて述べる。最後に本論文の構成につ いて述べる。

1.1 研究の背景 近年ソフトウェアの不具合が社会問題化することが増えてきている。その背景にはソフトウェア が必要とされる領域の拡大や、ソフトウェアの高機能化・多機能化にともなう複雑化がある。その ような状況において、信頼性を確保するための方法として、形式的手法の重要性が再び注目されて いる。ソフトウェアの最適化においても、アドホックな方法よりも形式的手法に基づくことが、信 頼性を損なわないために重要である。 一般的傾向として、概念を素直に表現したプログラムは理解しやすく、またモジュール性が高く 扱いやすいといった優れた面を持つが、性能が劣ることが多い。そのため、最適化が必要になる。 しかし、この最適化を人間が手でアドホックに行うと、その過程でバグが混入する可能性がある。 また、その結果のプログラムは複雑で保守が困難となってしまう。また、モジュール性が低く再利 用が困難なものとなってしまう。 形式的手法を用いた最適化では、元のプログラムの意味が保存されていることの数学的証明があ るため、最適化の過程でバグが混入する可能性がない。したがって、人間が概念を素直に表現した プログラムを記述し、そこから形式的手法に基づいて最適化されたプログラムを導出することによ り前述の問題を避けることが出来る。 一方で、関数型プログラミングや関数型言語が大きな注目を集めている。関数型言語は他の言語 に比較すると、プログラムの意味が数学的に定義されており、形式的手法に基づいた最適化を行う のに向いている。そのため、関数型言語を対象として等式変形によりプログラムの変換を行うこと が、構成的アルゴリズム論 (Constructive Algorithmics) [8][20] として広く研究がなされている。

–1–

第 1 章 序論

1.1. 研究の背景

1.1.1 関数型プログラミングと関数型言語 C 言語や Java 等に代表される命令型言語は、チューリングマシンを理論的基礎として発展して きた。これらの言語におけるプログラムとは計算機に対する命令の列を構造化したものである。こ れらの言語は現在の計算機のアーキテクチャと相性がよい。そのため効率的であり、また広範な状 況で用いることが可能であるというメリットが存在し、広く用いられている。 しかし、命令型言語ではプログラムを計算機に対する命令列として記述され、一般に各命令は現 在の計算機の状態に依存するとともに状態に変化を与える。このことは命令の順序を注意深く選択 しなくてはならないことを意味する。また、プログラム中の順序が本質的でない場合にも順序をつ けて記述しなくてはならない。 そのような問題に対して、より宣言的な記述によってプログラムを記述するたアプローチが存在 する。関数型プログラミングはそのようなアプローチの一つであり、数学的な関数と値に基づいた プログラミング・スタイルである。数学的な関数は、状態に依存せず同じ引数に対しては同じ値を 返す。関数型プログラミングでは、関数や定数の定義の集まりがプログラムとなり、式からそれが 表す値を求める (= 評価する) ことが計算過程となる。 命令型言語であっても関数型プログラミングを行うことは不可能ではないが、関数型プログラミ ングを支援・推奨するプログラミング言語も存在し、これは関数型言語と呼ばれる。主な関数型言 語として Haskell[13] や ML (OCaml[5], SML[21]) といったものが存在する。 本論文で主に扱う Haskell は 1987 年に生まれ、以来純粋関数型言語の標準たるべく進化してき たプログラミング言語である。現在の標準仕様は 1998 年に策定された Haskell 98[16] と呼ばれる 仕様で，2003 年にマイナーな改定がされている。

1.1.2 融合変換 Backus が [2] で関数型言語 FP とプログラム代数の概念を提唱して以降、プログラムを代数と して扱う流れが生まれた。それは構成的アルゴリズム論として発展し、プログラムの代数的性質に 基づいた変換であるプログラム変換が発展した。融合変換はプログラム変換の一つである。 ある種のプログラムは図 1.1(a) のようにデータ構造上の変換の列として記述されることが多い。 特に関数型プログラミングではそのようなプログラミングスタイルが推奨されている。そのような プログラムは分かりやすいが、変換の間で受け渡される中間データが存在し、効率が悪いという問 題がある。融合変換はこれを単一のパスに変換するプログラム変換である。 例としてリスト 1.1 のコード中の foo を考える。この foo はリストの各要素に対して関数 g を作 用させ、その結果のリストの各要素に対して関数 f を作用させたリストを結果とする関数である。 中間で生成されるリストは最終的な結果自体には含まれないにも関わらず、生成され、後に破棄さ れる。遅延評価を行うプログラミング言語の場合には、中間リストの全体が一度にメモリ上に生成

– 2–

第 1 章 序論

1.1. 研究の背景

(a) 融合変換前

(b) 融合変換後

図 1.1

変換の列からなるプログラム

される代わりに徐々に生成されるが、中間的なリストが生成されること自体は同じである。そのた め、やはりガベージコレクションに対する負荷を生じさせる。 それに対して foo’ は、リストの各要素に合成関数 (f ◦ g) を作用させたリストを結果とする関数 である。この関数では中間リストが生成されないため、そのような問題が生じない。両者は数学的 には同じ関数を表しているので、前者を後者に書き換えることが出来れば、中間リストを生成しな いプログラムになり、プログラムの効率が向上する。このような変換が融合変換である。 また、関数 all の定義は関数型プログラミングの特徴をよくあらわした簡潔な定義だが、ここで もリストの各要素に関数 p を作用させた結果のリストを一度作成し、それに対して and を適用し ている。この all も all’ のような定義に変換することによって、中間リストを生成しないプログラ ムに変換することが出来る。 これらの変換を行うにあたっては変換の前後で意味が変化しないことを保障することが必要で ある。したがって、プログラムの意味を形式的に定義し、その等価性を示さなくてはならない。そ のために用いられる主な道具には、圏論における普遍性と、多相ラムダ計算におけるパラメトリシ ティがある。 リスト 1.1 関数定義の例

−− 与 え ら れ た 関 数 を リ ス ト の 各 要 素 に 作 用 さ せ る 関 数 map : : ( a → b) → ( [ a] → [ b] ) map f [ ] =[] map f ( x: xs) = f x : ( map f xs) foo : : [ Int] → [ Int] foo = map f ◦ map g foo’ : : [ Int] → [ Int]

– 3–

第 1 章 序論

1.2. 研究の位置づけ

foo’ = map ( f ◦ g) −− 与 え ら れ た 関 数 と 初 期 値 を 用 い て リ ス ト を 畳 み 込 む 関 数 foldr : : ( a → b → b) → b → [ a] → b foldr c n [ ] =n foldr c n ( x: xs) = c x ( foldr c n xs) −− 論 理 値 の リ ス ト か ら 論 理 積 を と る and : : [ Bool] → Bool and = foldr (&&) True −− 関 数 と し て 与 え ら れ た 術 語 が リ ス ト の 全 要 素 で 成 り 立 っ て い る か を 判 定 a l l : : ( a → Bool) → ( [ a] → Bool) a l l p = and ◦ map p all ’ : : ( a → Bool) → ( [ a] → Bool) all ’ p = foldr phi True where phi a r = p a && r

1.2 研究の位置づけ プログラム変換の分野では、Meijer や Fokkinga ら [20][9][8] を初めとして、融合変換の研究に 関しては高野ら [26] や尾上 [30] を初めとして、様々な研究がなされている。 これらの研究を Haskell のような現実に存在する言語に対して適用する際に問題になるのは、そ れらの言語に存在するプログラム変換を困難にする様々な特徴である。そのような特徴には例えば 以下のようなものがある。

• 非正格な関数の存在 • 高階の多相 (higher-order polymorphism) • 非可述的多相 (impredicative polymorphism) • 遅延性 (lazyness) 本研究で着目したのは「非正格な関数の存在」である。非正格な関数は純粋関数型言語の利点の 一つであるにも関わらず、これまでの研究における非正格性の扱いは必ずしも満足のいくものでは なかった。 我々の知る限り、これまでの研究においての非正格性の扱いは、個々の等式や変換に対して「∼ が正格なとき」といった条件をアドホックにつけているか、あるいは誤った前提に基づくため非正 格性を正しく扱えていないかのどちらかであった。特に後者の場合には、そのような理論に基づい た最適化には、本来成り立っていない等式に基づいた変換を行ってしまう可能性があるという問題 がある。 そこで、本研究では始代数の普遍性に基づいた融合変換を対象として、非正格な関数を正格な関 数と同様に扱うことが出来るための、簡単かつ適用範囲の広い条件を示す。また、本研究ではその

– 4–

第 1 章 序論

1.3. 本論文の構成

結果に基づき、「高階の多相性」と入れ子データ型に対しても同様の条件と性質が成り立つことも 示す。 それによって、融合変換を安全により広い範囲で使用可能にすることが期待される。

1.3 本論文の構成 第 2 章では本論文の理論を展開する上で必要となる予備知識を説明する。第 3 章では、始代数 の普遍性に基づいた融合変化について論じ、本論文の主要な結果を述べる。第 4 章では第 3 章で 示したことを純粋関数型言語 Haskell へと適用する。第 5 章では第 3 章の内容を高階の多相性と 入れ子データ型に応用する。第 6 章ではまとめと今後の課題を述べる。

– 5–

第2章

予備知識

概要 本章では以降の章に必要な予備知識を説明する。まず、本論文で用いる記法について説明し、次 に後の章における理論を展開するのに必要な、圏論と領域理論の初歩的な知識について説明する。 後の章で利用する命題についても列挙する。

2.1 記法について 本論文で用いる記法について説明する。 関数などの適用の括弧は省略することがある。f (x) と書く代わりに f x と書くことがある。ま た、適用は左結合的であるとする。すなわち、f xy は (f x)y と解釈される。 等式変形の記法や等式の命名規則については Vene[28] に倣った。

2.2 圏論について 圏論は非常に抽象的な数学として知られている*1 が、プログラミング言語の意味論では圏論の言 葉が広く用いられている。また、萩野 [12] が圏論に基づいたプログラミングが可能であることを示 して以降、関数型言語のコミュニティでは圏論の概念を用いてプログラムを構造化することが盛ん になった。そのような構造は様々な良い性質を持つ。融合変換もプログラム中に明示的もしくは潜 在的に存在するそのような構造を利用する。 そこで、以下では圏論で用いられる幾つかの基本的な概念を説明する。圏論についての詳細は

[19] 等を参照のこと。 定義 2.1 (圏). 圏 C は以下の構成要素と条件からなる。

• 対象の集まり |C| • 任意の対象 X, Y ∈ |C| に対する射の集まり homC (X, Y ) 。f ∈ homC (X, Y ) はしばしば f

f : X → Y や X → Y と書かれる。X は f の定義域と呼ばれ dom(f ) と書かれる。Y は f の余域または値域と呼ばれ cod(f ) と書かれる。

• 任意の対象 X, Y, Z ∈ |C| に対して、homC (Y, Z) × homC (X, Y ) から homC (X, Z) への合 *1

しばしば Abstract Non-sense と揶揄されることもある

–6–

第 2 章 予備知識

2.2. 圏論について

成 ◦ が定義され、結合律 (f ◦ g) ◦ h = f ◦ (g ◦ h) を満たす。

• 任意の対象 X に対して、恒等射 idX : X → X が存在し、任意の f : W → X, g : X → Y に対して idX ◦ f = f と g ◦ idX = g を満たす。(idX の添え字 X は文脈から明らかである 場合には省略することがある)

例 2.2. 典型的な圏の例として以下のようなものがある。

• 集合を対象、集合の間の関数を射とする圏 Set • 代数を対象、順同型を射とする圏 • プログラミング言語における型を対象、入力の型が A で出力の型が B であるプログラムを 射 A → B とする圏

定義 2.3 (逆圏 (opposite category)). C op は C の射の向きを逆にしただけの圏である。

|C op | = |C| homC op (A, B) = homC (B, A)

定義 2.4 (積圏). C × D は、C と D の対象の組を対象、C と D の射の組を射とする圏である。

|C × D| = |C| × |D| homC×D (⟨A, C⟩, ⟨B, D⟩) = homC (A, B) × homD (C, D)

定義 2.5 (同型). f : X → Y は、g : Y → X が存在して g ◦ f = idX と f ◦ g = idY を満たす とき同型射と呼ばれる。同型射 X → Y が存在するとき X と Y は同型であるという。また、g は f の逆 (inverse) と呼ばれ、f に対して高々ひとつだけしか存在しないので f −1 と書かれる。

定義 2.6 (関手). 圏 C から 圏 D への関手 F : C → D は以下の構成要素と条件からなる。

• X ∈ |C| への F X ∈ |D| の割り当て • f ∈ homC (X, Y ) への F (f ) ∈ homD (F X, F Y ) の割り当て • F (idX ) = idF X • F (f ◦ g) = F f ◦ F g

– 7–

第 2 章 予備知識

2.2. 圏論について

関手は対象と射の両方に対して作用する。そのため、型とプログラムを対象とした圏では、デー タ型と制御の両方を同時に扱うことが出来る。 定義 2.7 (恒等関手). 圏 C 上の恒等関手 Id : C → C は以下のように定義される。

{

IdX Idf

= X = f

定義 2.8 (定数関手). A ∈ |D| に対して、圏 C から D への定数関手 KA : C → D は以下のように 定義される。

{

KA X KA f

= A = idA

.

定義 2.9 (自然変換). 関手 F : C → D から関手 G : C → D への自然変換 α : F → G は以下の構 成要素と条件からなる。

• 各 X ∈ |C| に対する射 αX : F X → GX の割り当て • 自然性 (naturality): 任意の f : X → Y に対して、図式

FX

αX

ª

Ff

² FY

αY

/ GX Gf

² / GY

*2 が可換。

定義 2.10 (終対象). 任意の対象 X からただ一つ射が存在する対象を終対象 (terminal object) と 呼び 1 と書く。X から 1 へのただ一つの射を ! : X → 1 と書く。

定義 2.11 (始対象). 任意の対象 X へただ一つ射が存在する対象を始対象 (initial object) と呼び

0 と書く。0 から X へのただ一つの射を !! : 0 → X と書く。

*2

このように圏論では可換図式を用いて等式を表現することが多い。

– 8–

第 2 章 予備知識

2.2. 圏論について fst

f

snd

g

定義 2.12 (直積). A ← A × B → B は、任意の A ← C → B に対して、図式

/B A ×O B A cFo F ; x FF xx FF h x FF xx f F xxx g C fst

snd

を可換にする h がただ一つ存在するとき、直積であるという。ただ一つの h を ⟨f, g⟩ と書く。 直積は二引数の関手であり、射に対する作用は

f × g = ⟨f ◦ fst, g ◦ snd⟩ で定義される。

inl

f

inr

g

定義 2.13 (直和). A → A + B ← B は、任意の A → C ← B に対して、図式 inl / inr A+B o A FF B FF xx x FF h x FF xx f F# ² {xxx g C

を可換にする h がただ一つ存在するとき、直積であるという。ただ一つの h を [f, g] と書く。 直和は二引数の関手であり、射に対する作用は

f + g = [inl ◦ f, inr ◦ g] で定義される。

ev

定義 2.14 (冪). A × (A ⇒ B) → B は任意の f : A × C → B に対して、図式

/6 B lll l l lll llfl l l lll

A × (A ⇒ B) O idA ×h

A×C

ev

を可換にする h がただ一つ存在するとき、冪であるという。ただ一つの h を curry(f ) と書く。

2.2.1 代数 定義 2.15 (T 代数). 関手 T : C → C が与えられているとする。このとき、A ∈ |C| と φ : T A → A の組 (A, φ) を T 代数と呼ぶ。

– 9–

第 2 章 予備知識

2.2. 圏論について

また、(A, φ) から (B, ψ) への T 準同型射とは、C の射 h : A → B で h ◦ φ = ψ ◦ T h を満たす ものである。

T 代数と T 準同型射の全体は圏 ALG T をなす。

定義 2.16 (始代数 と catamorphism). T 始代数 (µT, inT ) は、任意の T 代数 (A, φ) へのただ一 つの準同型射 (|φ|)T : (µT, inT ) → (A, φ) が存在する T 代数である。 すなわち以下が成り立つ。

h ◦ inT = φ ◦ T h ⇔ h = (|φ|)T

cata-Charn

(|φ|)T は catamorphism と呼ばれる。添え字 T は文脈から明らかであるときには省略すること がある。

系 2.17.  

• Cancelation: • Reflection:

(|φ|)T ◦ inT = φ ◦ T (|φ|)T

cata-Self

idµT = (|inT |)T

cata-Refl

• Fusion: 任意の T 代数 (C, φ), (D, ψ) と射 f : C → D に対して、 f ◦ φ = ψ ◦ T f ⇒ f ◦ (|φ|)T = (|ψ|)T

cata-Fusion

命題 2.18 (Lambek’s lemma [18]).

in−1 T = (|T inT |)T

in-inv-Def

始代数は自然数や (有限) リストや (有限) 木といった帰納的なデータ型をモデル化するために 用いられる。例えば、自然数は F X = 1 + X で定義される関手の、要素が A であるリストは

LA X = 1 + A × X で定義される関手の始代数としてモデル化される。

2.2.2 余代数 T 代数, 始代数, catamorphism の概念の双対を考えることにより、以下が得られる。 定義 2.19 (T 余代数). 関手 T : C → C が与えられているとする。このとき、A ∈ |C| と

φ : A → T A の組 (A, φ) を T 余代数と呼ぶ。 – 10–

第 2 章 予備知識

2.3. 領域理論について

また、(A, φ) から (B, ψ) への T 準同型射とは、C の射 h : A → B で ψ ◦ h = φ ◦ T h を満たす ものである。

T 余代数と T 準同型射の全体は圏 COALG T をなす。

定義 2.20 (終余代数 と anamorphism). T 終余代数 (νT, outT ) は、任意の T 余代数からのただ 一つの順同型射 [(φ)]T : (A, φ) → (νF, outT ) が存在する T 余代数である。 すなわち以下が成り立つ。

outT ◦ h = T h ◦ φ ⇔ h = [(φ)]T

ana-Charn

[(φ)]T は anamorphism と呼ばれる。添え字 T は文脈から明らかであるときには省略することが ある。

系 2.21.  

• Cancelation:

outT ◦ [(φ)]T = T [(φ)]T ◦ φ

ana-Self

idνT = [(outT )]T

ana-Refl

• Reflection:

• Fusion: 任意の T 余代数 (C, φ), (D, ψ) と射 f : C → D に対して、 ψ ◦ f = T f ◦ φ ⇒ [(ψ)]T ◦ f = [(φ)]T

ana-Fusion

終余代数はストリームや無限リストや無限木といった余帰納的なデータ型をモデル化するために 用いられる。例えば、要素が A であるストリーム Stream(A) は A × − の終余代数 ν(A × −) で モデル化される。

2.3 領域理論について 全域的なプログラムだけを対象にするのであれば、集合の圏を考えればよい。しかし、現実のプ ログラミング言語では再帰的な定義を自由に用いることが出来、停止しない計算を表現することが 出来る。再帰的な定義や停止しない計算を解釈するためには、単純な集合の代わりに、特別な構造 を持った集合である領域 (domain) を用いなくてはならない。そこで、以下では領域理論について 説明する。

– 11–

第 2 章 予備知識

2.3. 領域理論について

2.3.1 Cpo, 連続関数, 最小不動点 定義 2.22 (Cpo). 以下が定義されている半順序集合を Cpo とする。

• ω 鎖 (上昇列) a0 ⊑ a1 ⊑ a2 ⊑ . . .) の上限

⊔ n<ω

xn

• 最小元 ⊥ ⊥ は「未定義」を表す値であり、停止しない計算を表現するため等に用いられる。

定義 2.23 (連続関数). Cpo 間の関数 f はω鎖の上限を保存するとき連続関数である。

f(

⊔

xn ) =

⊔

f (xn )

n<ω

n<ω

Cpo と連続関数は圏 Cpo をなす。 定義 2.24 (正格性). 関数 f は ⊥ を保存するとき正格である。

f (⊥) = ⊥

Cpo と正格な連続関数は圏 Cpo⊥ をなす。 命題 2.25. 連続関数 f : A → A の最小不動点

lfp f =

⊔

f n⊥

n<ω

が存在する。

2.3.2 CPO 圏 Freyd[10] は Cpo や Cpo⊥ を直接扱う代わりに、より抽象的に CPO 圏とその CPO 構造に関 する関手の概念を定義し、それらを用いた。 定義 2.26 (CPO 圏). 以下を満たす圏 C を CPO 圏と呼ぶ。

CPOC-0 終対象 1 が存在する CPOC-1 各対象 A, B ∈ |C| について hom 集合 hom(A, B) が Cpo CPOC-2 各対象 A, B, C ∈ |C| について 合成 ◦ : hom(B, C) × hom(A, B) → hom(A, C) が連続 かつ正格

– 12–

第 2 章 予備知識

2.3. 領域理論について

CPOC-3 idempotent split.

hom(A, B) の最小元を ⊥ : A → B もしくは ⊥A→B と書くことにする。 例 2.27. Cpo と Cpo⊥ は CPO 圏である。 定義 2.28 (正格な射). 射 f : A → B は以下が成り立つときに、正格であるという。

f ◦ ⊥1→A = ⊥1→B

命題 2.29 (CPOC-2’). 任意の A, B, C と f : A → B に対して、以下が成り立つ。

⊥B→C ◦ f = ⊥A→C

命題 2.30. CPO 構造に関する関手は射の正格性を保存する。

f

g

g

命題 2.31. A → B → C が正格ならば、B → C は正格

定義 2.32. C, D を CPO 圏とする。関手 F : C → D は、各対象 A, B ∈ |C| について、 射の写像 hom(A, B) → hom(F A, F B) が連続であるとき、CPO 構造に関する関手という。

以降では CPO 圏の間の関手は、CPO 構造に関する関手であるものとする。 命題 2.33 (始代数と終余代数の一致). CPO 構造に関する関手 T の始代数 (µT, inT ) が存在すれ ば、 (µT, in−1 T ) は T の終余代数になっている。 命題 2.34. CPO 構造に関する関手 T : Cpo⊥ → Cpo⊥ の始代数が存在する。

2.3.3 関手 領域理論で用いる関手を以下に述べる。 前述の関手では直積は Cpo, Cpo⊥ に存在する。冪は Cpo に存在し、Cpo⊥ には存在しない。 定義 2.35 (合体直和). Cpo⊥ での直和を合体直和 (coalesced sum) と呼び A ⊕ B のように書く。 集合論的には A ⊕ B = {(0, a) | a ∈ A, a ̸= ⊥} ∪ {(1, b) | b ∈ B, b ̸= ⊥} ∪ {⊥} という集合に、

– 13–

第 2 章 予備知識

2.3. 領域理論について

以下のような半順序を定義したものである (図 2.1(a))。

(0, a) ≤A⊕B (0, a′ ) ⇔ a ≤A a′ (1, b) ≤A⊕B (0, b′ ) ⇔ b ≤B b′ ⊥ ≤A⊕B x

合体直和は Cpo⊥ × Cpo⊥ → Cpo⊥ の関手になっている。しかし、関手としての定義域を

Cpo に拡大することは出来ない。 定義 2.36 (持ち上げ). Cpo A に対して、Cpo A⊥ を以下のように定義する。これは A⊥ =

{⟨o, a⟩ | a ∈ A} ∪ {⊥} という集合に、以下のような半順序を定義したものである (図 2.1(b)) ⟨o, a⟩ ≤A⊥ ⟨o, a′ ⟩ ⇔ a ≤A a′ ⊥ ≤A⊥ x

射に対する作用は以下で定義される。

f⊥ ⟨o, a⟩ = ⟨o, f a⟩ f⊥ ⊥ = ⊥

定義 2.37 (分離直和). 分離直和 (separated sum) は A1 +A2 +· · ·+An = A1 ⊥ ⊕A2 ⊥ ⊕· · ·+An ⊥ で定義され、Cpo × Cpo × · · · × Cpo → Cpo⊥ の関手になっている。集合論的には図 2.1(c) の ようになっている。領域理論では + 記号を圏論の直和ではなくこの分離直和に対して用いるので 注意が必要である。

定義 2.38 (スマッシュ積). スマッシュ積 A ⊗ B は A ⊗ B = {⟨a, b⟩ | a ∈ A, a ̸= ⊥, b ∈ B, b ̸=

⊥} ∪ {⊥} という集合に以下のような半順序を定義したものである。 ⟨a, b⟩ ≤A⊗B ⟨a′ , b′ ⟩ ⇔ a ≤A a′ ∧ b ≤B b′ ⊥ ≤A⊗B x

射に対する作用は以下で定義される。

{ ⟨f a, gb⟩ (f ⊗ g)⟨a, b⟩ = ⊥ (f ⊗ g)⊥ = ⊥ – 14–

f a ̸= ⊥ ∧ gb ̸= ⊥ otherwise

第 2 章 予備知識

2.4. 本章のまとめ

A

A

A

B

B

(a) 合体直和 A ⊕ B

(b) 持 ち 上 げ A⊥

(c) 分離直和 A + B

図 2.1 合体直和、持ち上げ、分離直和

(A × B)⊥ = A⊥ ⊗ B⊥ が成り立つ。 スマッシュ積は圏論的には bistrict な射の中で普遍的なものとして定義できる。

2.4 本章のまとめ 本章では、本論文で用いる記法について説明し、さらに圏論と領域理論のうち以降の章で必要と なる部分の説明を行った。次章以降では本章で準備した定義や補題を必要に応じて用いる。

– 15–

第3章

非正格性と始代数

概要 本章ではまず始代数の普遍性に基づいた融合変換について述べる。次に、非正格な射の存在する 領域理論的な圏では始代数が存在しないことがあることと、そのために始代数の普遍性に基づいた 融合変換が適用出来ないことがあるを述べる。その後、問題が起こらないための条件として、「任 意の関数 f : A → B に対して F (f ) が常に正格であるならば、F は CPO と連続関数の圏におい ても始代数を持つ」ことを示す。

3.1 始代数の普遍性に基づいた融合変換 プログラム変換は効率の劣るプログラムから等しい意味のより効率的なプログラムへの変換であ り、変換の前後で意味が保存されていることが必要である。二つのプログラムの意味が等しいこと を保証するためには、圏論の普遍性やパラメトリシティが用いられる。 圏論の普遍性を用いる際には、データ型が何らかの普遍性を満たすことを仮定し、その普遍性を 満たすただ一つの射としてプログラムを特定する。それによって同じ条件を満たすプログラムが全 て等しくなるため、それらのプログラムの間で書き換えを自由に行うことが出来る。

catamorphism では始代数の普遍性を利用して cata-Charn で条件を満たすただ一つの射とし てプログラムを特定している。そして、条件を満たす射がただ一つだけであるということを利用し て cata-Fusion のような融合変換を行うことが出来る。 また、Vene[28] は catamorphism や anamorphism だけでなく、原始帰納関数を抽象化した

paramorphism、その双対の apomorphism、一種のメモ化を行う再帰形式を抽象化した histomorphism、その双対の futumorphism といった非常に多様な射を同様にして特徴付け、融合規則を定 義している。 さらに、Uustalu と Vene[27] は余モナドを用いた comonadic iteration という再帰形式を定義 し、catamorphism, paramorphism, histomorphism は comonadic iteration を個々の余モナドで 具体化したものになっていることを示した。しかし、それらの特徴付けは適当な条件のもと全て始 代数の普遍性に帰着される。したがって、本章では始代数の普遍性と catamorphism を主に取り上 げる。 また、始代数の普遍性と終余代数の普遍性に加え、始代数と終余代数の一致を利用した融合変換

– 16 –

第 3 章 非正格性と始代数

3.2. 領域理論的な圏での場合の問題

に hylomorphism を用いたものがある。 定 義 3.1 (hylomorphism). 関 手 T の 始 代 数 (µT, inT ) が 存 在 し て 、(µT, in−1 T ) が終余代数

(νT, outT ) と等しいとする。このとき、T 余代数 (A, ψ) から得られる関数 [(ψ)]T : A → νT と、T 代数 (B, φ) から得られる関数 (|φ|)T : µT → B を合成して、(|φ|)T ◦ [(ψ)]T : A → B という 関数を定義できる。これを hylomorphism と呼び [[φ, ψ]]T と書かれる。

A

[(ψ)]T

outT

ψ

² TA

T [(ψ)]T

(|φ|)T

/ νT = µT O

/B O φ

inT

² / T νT = T µT

T (|φ|)T

/ TB

hylomorphism [[φ, ψ]]T は λf. ϕ ◦ T f ◦ ψ の最小不動点に等しく、後者の定義に変換することで、 中間データ型 µT = νT の値を生成せずに計算を行うことが出来る。

3.2 領域理論的な圏での場合の問題 ここで領域理論の対象となる圏を考える。Cpo⊥ では CPO 構造に関する関手 F の始代数と終 余代数が存在し、始代数 (µF, inF ) に対して (µF, in−1 F ) は終余代数になっている。そのため再帰的 なデータ型を定義域とするような関数を cata-Charn によって特徴づけ、cata-Fusion によって 融合することが出来る。また、始代数と終余代数が一致するので hylomorphism を利用することが 出来る。しかし、Cpo には始対象が存在しないため、一般にはそのような事は成り立たない。 構成的アルゴリズム論の分野では Cpo で多項式関手 (+, ×, Id および定数関手からなる関手) の 始代数が存在し終余代数と一致するなどと書かれている論文が少なくない。そのような論文には例 えば [14][26] がある。しかし多項式関手であっても始代数が存在しない場合がある。以下で反例を 示す。 定理 3.2. 圏 C に終対象 1 と、異なる 2 点 f, g : 1 → X が存在するとする。また、関手 F が自然 .

変換 ε : F → Id を持つとする。このとき、F の始代数 (µF, in) が存在すれば、点 1 → µF は存在 しない。 証明. 任意の x : 1 → X は (1, ε1 ) から (X, εX ) への準同型なので、

F µF in

² µF

F !µF

ª !µF

/ F1

Fx

!=ε1

ª

² /1

– 17–

x

/ FX εX

² /X

第 3 章 非正格性と始代数

3.2. 領域理論的な圏での場合の問題

より x◦!µF = (|εX |) となる。ここでもし、点 p : 1 → µF が存在すれば、

f = f ◦ id1 = f ◦!µF ◦ p = (|εX |) ◦ p = g◦!µF ◦ p = g ◦ id1 = g となり、これは異なる 2 点が存在するとした仮定に矛盾する。 よって、背理法により点 1 → µF は存在しない。 系 3.3. Set では、2 を 2 点集合として、異なる 2 点 f, g : 1 → 2 を取ることが出来る。したがっ .

て、自然変換 ε : F → Id が存在すれば、F 始代数は存在すればそれは点を持たない集合、すなわ ち空集合 ∅ でなくてはならない。 実際、関数 ε∅ : F ∅ → ∅ が存在するので F ∅ も空集合であり、(∅, ε∅ ) が始代数であることを確認 できる。

系 3.4. Cpo では 2 = {⊥ ⊑ ⊤} とおくと、異なる二点 ⊥ : 1 → 2, ⊤ : 1 → 2 をとることが出来 .

る。したがって、自然変換 ε : F → Id が存在する関手 F の始代数が存在すれば、それは点を持た ない対象である。しかし、Cpo では全ての対象 X が点 ⊥ : 1 → X を持つので、背理法によりそ のような関手 F の始代数は存在しない。 一 方 、Cpo⊥ で は 各 X に は ⊥ : 1 → X 以 外 の 点 が 存 在 し な い た め 、そ も そ も 異 な る

2 点 f, g : 1 → X を と る こ と が 出 来 な い 。し た が っ て 、Cpo⊥ で は 問 題 は 起 こ ら な い 。

例 3.5. 余モナド F は自然変換 ε : F → Id を持つので、Cpo では余モナドの始代数は存在しな い。代表的な例としては、恒等関手 Id, 直積 A × −, ストリーム Stream(A) = ν(A × −) がある。

例 3.6. F (X) = A ⇒ X は、a : 1 → A が存在するならば、自然変換 ev◦⟨idA⇒X , a◦!⟩ : F X → X を得られるので、Cpo ではこの F の始代数は存在しない。

実際には始代数でないのにも関わらず始代数として扱ってしまうと、誤った変換を行ってしまう 可能性がある。 例 3.7 (誤った変換). 誤って (Stream(A), out−1 ) が関手 A × − の始代数であると仮定してしまっ たとする。 点 h ̸= ⊥ : 1 → B をとる。h ◦ snd = snd ◦ (A × h) が成り立つので、cata-Fusion により、

– 18–

第 3 章 非正格性と始代数

3.3. 始代数が存在するための条件

h ◦ (|snd|) ̸= ⊥ : Stream(A) → B は (|snd|) = ⊥ : Stream(A) → B へと融合される。 A × Stream(A)

A×(|snd|)

/ A×1

out−1

snd

² Stream(A)

² /1

(|snd|)

A×h

/ A×B

snd

h

² /B

この変換によって ⊥ と異なっていたプログラムが ⊥ に変換されてしまった。プログラムの意味が 変化するだけでなく、less-defined な定義に変換されてしまっている。これは変換前は停止したプ ログラムが変換後には停止しなくなってしまったことを意味するので、大きな問題である。

3.3 始代数が存在するための条件 始代数が存在するための条件として、以下を証明した。 定理 3.8. 関手 F : C → D, G : D → C が与えられているとする。F G : D → D の始代数が存在 するとき及びそのときに限って GF : C → C の始代数が存在する。 証明. (µF G, inF G ) が F G の始代数だとする。このとき (GµF G, GinF G ) が GF の始代数である ことを示す。

GF 代数 (X, φ) に対して、準同型 (GµF G, GinF G ) → (X, φ) を h = φ ◦ G((|F φ|)F G ) で定 める。 まず、これが (GµF G, GinF G ) から (X, φ) への準同型になっている、つまり h◦GinF G = φ◦GF h が成り立っていることを示す (最終的な可換図式の全体は図 3.1)。

                 

= = = = =

h ◦ GinF G  - definition of h φ ◦ G(|F φ|)F G ◦ GinF G  - G functor φ ◦ G((|F φ|)F G ◦ inF G )  - FG cata-Self φ ◦ G(F φ ◦ F G(|F φ|)F G )  - F functor φ ◦ GF (φ ◦ G(|F φ|)F G )  - definition of h φ ◦ GF h

次 に (GµF G, GinF G ) か ら (X, φ) へ の 準 同 型 が た だ 一 つ で あ る こ と を 示 す 。準 同 型 f :

– 19–

第 3 章 非正格性と始代数

3.3. 始代数が存在するための条件

GF h

GF G(µF G)

G(inF G )

² G(µF G)

GF G(|F φ|)F G

/ GF GF X

GF φ

ª

GF φ

ª

G((|F φ|)F G )

² / GF X

φ

/, GF X

φ

² /2 X

h

図 3.1

最終的な可換図式の全体

(GµF G, GinF G ) → (X, φ) が与えられたときに f = h であることを示す。  ◃ f ◦ GinF G = φ ◦ GF f  f   = f ◦ idGµF G   =  - G functor   f ◦ GidµF G   =  - in-inv-Def   f ◦ GinF G ◦ Gin−1 FG   =  - ▹   φ ◦ GF f ◦ Gin−1 FG   =  - G functor   φ ◦ G(F f ◦ in−1  F G)  =  - in-inv-Def   φ ◦ G(F f ◦ (|F GinF G |)F G )   =  - cata-Fusion (図 3.2)    F f ◦ F GinF G    =  - F functor     F (f ◦ GinF G )     =  - ▹       F (φ ◦ GF f )     =  - F functor   F φ ◦ F G(F f )   φ ◦ G(|F φ|) FG   =  - definition of h h これで F G : D → D の始代数が存在するときに GF : C → C の始代数が存在することを示せ た。同様に、GF : C → C の始代数が存在するときに F G : D → D の始代数が存在する。

F op : C op → Dop と Gop : Dop → C op に対してこれを適用することにより次が得られる。 系 3.9. 関 手 F : C → D, G : D → C が 与 え ら れ て い る と す る 。F G : D → D の

– 20–

第 3 章 非正格性と始代数

3.4. 具体的なデータ型への適用

F G(|F φ|)

F GµF G

inF G

² µF G

/ F GF GµF G

F G(|F GinF G |)F G

F GF f

ª

F GinF G

ª

(|F GinF G |)F G

² / F GµF G

Ff

/, F GF X

Fφ

² /2 F X

(|F φ|)

図 3.2

cata-Fusion の適用

終 余 代 数 が 存 在 す る と き 及 び そ の と き に 限 っ て GF : C → C の 終 余 代 数 が 存 在 す る 。

系 3.10. CPO 構造に関する関手 T : Cpo → Cpo が、任意の f に対して T f が正格であるとす る。このとき T の始代数が存在して終余代数と一致する。 証明. 任意の f に対して T f が正格であるので、ある T ′ : Cppo → Cppo⊥ と忘却関手

U : Cpo⊥ → Cpo とで、T = U T ′ と分解できる。T ′ U : Cpp⊥ → Cpo⊥ は CPO 構造に関す る関手であり、Cpo⊥ で始代数が存在する。定理 3.8 によって、U T ′ = T の始代数が Cpo で存 在する。

3.4 具体的なデータ型への適用 この条件はデータ型を定義する関手だけをみれば容易に判別可能である。

2.3 節で定義した関手のうち、分離直和は Cpo × · · · × Cpo → Cpo⊥ という関手になってい る。したがって、F X = G1 X + · · · + Gn X という式で定義される関手では、Cpo⊥ で始代数と 終余代数が存在して一致し、それは Cpo でも始代数と終余代数になっている。 自然数は F X = 1 + X という式で定義される関手の、要素の型が A であるリストの型は

LA X = 1 + A × X の、始代数としてモデル化されると書いた。これらは Cpo → Cpo⊥ の関手な ので、リストや自然数などのようなよく使うデータ型に対しては、cata-Fusion や hylomorphism を利用することが出来る。

– 21–

第 3 章 非正格性と始代数

3.5. 他アプローチとの比較

3.5 他アプローチとの比較 3.5.1 代数のみを正格なものに制限 高野と Meijer[26] は φ : F X → X を正格なものに制限するが、準同型は正格なものに制限しな い、ALG F の変種を用いている。そして、その前提で多項式関手に対する始代数の存在と終余代数 との一致を仮定している。しかし、このような制限を導入したとしても始代数の存在しない多項式 関手が存在する。 .

恒等関手や直積は多項式関手に含まれるので、自然変換 ε : F → Id の各成分 εX : F X → X が 正格であることを示せば、定理 3.2 と系 3.4 を適用出来る。 .

補題 3.11. 自然変換 α : F → G の各成分の正格性は一致する。 証明.

αX strict ⇒  - G preserves strictness (命題 2.30) G⊥X→Y ◦ αX strict ⇔  - naturality αY ◦ F ⊥X→Y strict ⇒  - 命題 2.31 αY strict

FX αX

² GX

F⊥

ª G⊥

/ FY αY

² / GY

.

定理 3.12. 自然変換 ε : F → Id は正格。 証明. ε1 = ⊥ : F 1 → 1 より ε1 は正格であり、補題 3.11 より ε の全ての成分は正格。

3.5.2 代数と準同型を正格なものに制限 Fokkinga と Meijer[9] は再帰的データ型を Cpo⊥ 上の始代数として解釈している。そのため、 代数だけを正格に制限したときのような問題は起こらない。 しかし、(|φ|) は正格な φ : F X → X に対してのみしか定義されない。また、cata-Fusionにつ

– 22–

第 3 章 非正格性と始代数

3.6. 本章のまとめ

いても、以下のように正格性の条件がついていた。

f ◦ φ = ψ ◦ T f ∧ f strict ⇒ f ◦ (|φ|)T = (|ψ|)T 本研究のアプローチを適用した場合には、条件を満たさない一部のデータ型については正格性の 条件を外すことは出来ないが、それ以外の一般的なデータ型については Cpo 上の始代数として解 釈することが出来、より自由な変換を行うことが出来る。我々の条件が適用できる場合には、f の 正格性を調べる必要はない。

3.6 本章のまとめ 本章では始代数の普遍性に基づく融合変換について説明し、領域理論的な圏では始代数が存在せ ず問題が起こる可能性について説明した。そして、非正格な関数を扱う際の既存の理論では問題が あることを示し、問題が起こらないことを保障するための条件を証明した。 定理 3.8 と系 3.10 は非常に簡単に示すことが出来るが、我々の知る限り同様の事を示した研究 は他に存在しない。

hylomorphism の難しさは，始代数＝終余代数という仮定が満たされにくいことである．通 常の型付きラムダ計算を考えている場合，この仮定はめったなことでは満たされない．普通 の表示的意味論で考えても，これらは多くの場合，同等ではない． プログラム言語意味論の専門家である長谷川立氏も上に引用したように [29] で述べている。 次章では本章で示したことを Haskell に対して適用する。

– 23–

第4章

Haskell への適用

概要 本章では第 3 章章で示した理論の Haskell で定義されるデータ型に対して適用する。

Haskell の型宣言が領域理論的にどのように解釈されるかを示し、Cpo で始代数として解釈可能 かチェックする方法を示した。

4.1 型宣言と領域方程式 Haskell では新たな型は data 宣言もしくは newtype 宣言によって定義される。本節ではそれら によってなされたデータ型の定義を領域方程式によって表現する。

4.1.1 data 宣言 Haskell では通常のデータ型は data 宣言 (図 4.1) によって定義される。ここで D は型構築子 の名前であり、ai はその型引数である。Ci はデータ構築子の名前である。Fi,j はデータ構築子の フィールドであり、型式 T もしくは型式に正格性フラグをつけた !T という形をしている。

data D a1 · · · an =

C1 F1,1 · · · F1,c1

|

C2 F2,1 · · · F2,c2 .. .

|

Cm Fm,1 · · · Fm,cm

図 4.1 data 宣言の文法

例えば、多相的な二分木はリスト 4.1 の Tree として定義可能である。また、Tree’ や Tree” の ようなバリエーションを考えることが出来る。本章ではこれらの定義を例として用いる。 データ宣言で定義されるデータ型は、以下のように右辺がスマッシュ積の合体直和になっている 領域方程式の最小解として解釈することが出来る。正格性フラグのついているフィールドに対して は持ち上げが行われず、それ以外のフィールドに対しては持ち上げが行われる。

– 24 –

第 4 章 Haskell への適用

4.1. 型宣言と領域方程式

リスト 4.1 data 宣言による木のデータ型の定義

data Tree a = Leaf a | Branch ( Tree a) ( Tree a) data Tree’ a = Leaf’ ! a | Branch’ ( Tree’ a) ( Tree’ a) data Tree’ ’ a = Leaf’ ’ a | Branch’ ’ ! ( Tree’ ’ a) ! ( Tree’ ’ a)

D a1 · · · an ∼ = { where

ci m ⊗ ⊕ i

[[!T ]]F [[T ]]F

[[Fi,j ]]F

j

= T = T⊥

例のデータ型はそれぞれ以下の領域方程式の最小解として解釈される。 例 4.1.

Tree a ∼ = a⊥ ⊕ ((Tree a)⊥ ⊗ (Tree a)⊥ ) ∼ a⊥ ⊕ (Tree a × Tree a)⊥ = ∼ = a + (Tree a × Tree a) ′ Tree a ∼ = a ⊕ ((Tree′ a)⊥ ⊗ (Tree′ a)⊥ )

∼ = a ⊕ (Tree′ a × Tree′ a)⊥ Tree′′ a ∼ = a⊥ ⊕ (Tree′′ a ⊗ Tree′′ a)

ここで、D が正則データ型であるとする。すなわちこの領域方程式の右辺に D は D aa · · · an 以外の形で現れないとする。このとき、

FD aa · · · an x = ( 右辺に表れる D aa · · · an を x で置き換えたもの ) とおくと、D aa · · · an は FD aa · · · an − の最小不動点 µ(FD aa · · · an −) として解釈される。 例のデータ型の場合には FD はそれぞれ以下のようになる。 例 4.2.

FTree a x = a + (x × x) FTree′ a x = a ⊕ (x × x)⊥ FTree′′ a x = a⊥ ⊕ (x ⊗ x)

– 25–

第 4 章 Haskell への適用

4.2. 関手の不動点としての解釈

4.1.2 newtype 宣言 newtype 宣言は、表現が既存の型と同一だが、型システムの中では別の型として識別されるよう な型を定義するために用いられる。newtype 宣言ではデータ型は「newtype D a1 · · · an = C T 」 という形で定義されるが、これは「data D a1 · · · an = C !T 」で定義されるデータ型と同型であ るので、本論文では newtype 宣言にはこれ以上触れない。

4.2 関手の不動点としての解釈 FD を関手として解釈可能か、解釈可能ならばどの圏とどの圏の間の関手として解釈可能かを チェックする。型定義中に使われている各型構築子についての情報が与えられていれば、それらを 用いて FD についての情報が容易にチェック可能である。 先ほどの例であれば、以下のような関手として解釈することが出来る。 例 4.3.

FTree : Cpo × Cpo → Cpo⊥ FTree′ : Cpo⊥ × Cpo → Cpo⊥ FTree′′ : Cpo × Cpo⊥ → Cpo⊥

ここで、FTree a は Cpo から Cpo⊥ への関手なので、系 3.10 より Tree a = µ(FTree a) は Cpo における FTree a の始代数となっている。また、Tree は Cpo から Cpo⊥ への関手となる。

FTree′ a は Cpo から Cpo⊥ への関手なので、Tree′ a = µ(FTree′ a) は Cpo における FTree′ a の始代数となっている。また、Tree′ は Cpo⊥ から Cpo⊥ への関手となる。

FTree′′ a は Cpo⊥ から Cpo⊥ への関手なので、Tree′′ a = µ(FTree′′ a) は Cpo⊥ における FTree′′ a の始代数となっているが、Cpo では始代数になっていることは言えない。また、Tree は Cpo から Cpo⊥ への関手となる。 まとめると表 4.1 のようになっている。 表 4.1

D Tree Tree Tree

′ ′′

Tree 型の各定義の性質

Da は Cpo⊥ で FD a 始代数

Cpo で始代数

関手 D の定義域

Yes

Yes

Cpo

Yes

Yes

Cpo⊥

Yes

No

Cpo

このようにすることで Haskell のデータ型が Cpo における始代数として解釈可能かを判定で

– 26–

第 4 章 Haskell への適用

4.3. 本章のまとめ

きる。 またこの結果を用いることで、これらのデータ構築子を用いて定義される新たな再帰的データ型 に対して同様のことが行える。

4.3 本章のまとめ 本章では第 3 章で示した理論を Haskell のデータ型に対して適用し、始代数として扱えるかどう かを判定する方法を示した。ここで述べた方法は十分単純であり、このような処理を Haskell の処 理系に組み込むのは難しくないと考えられる。 しかし、以上は型引数として渡されるのは型だけであり、型構築子が型引数として渡される場合 については考慮していないという問題がある。この問題に関連して、5 では関手圏の変種として、 多相関数の圏を定義する。

– 27–

第5章

多相関数の圏の場合

概要 本章では前章までに示した基礎に基づいて、より複雑なデータ構造を対象とした融合変換につい て論じる。まず高階の多相性と入れ子データ型について論じ、第 2 章と同様の条件を示す。次に

GADT (Generalized Algebraic Datatypes) について論じる。

5.1 高階の多相性と入れ子データ型 Haskell では型変数は ∗ 以外の種に属することも出来る。これは通常の型だけでなく、型構築子 を量化するすることが出来ることを意味する。そのため、リスト 5.1 のようなデータ型を定義でき る。型引数 f の種は ∗ → ∗ となっており、f は型上の関数である。 リスト 5.1 高階の型引数を持つデータ型の例

data GRoseTree f a = Leaf a | Branch ( f ( GRoseTree f a) )

また、リスト 5.2 のようなデータ型を定義することが出来る。PTree の引数は左辺では a だっ たのが右辺では (a, a) となっている。このように型パラメータが変化する再帰的データ型は、非正 則データ型 (Non-regular Datatypes) または入れ子データ型 (Nested Datatypes) と呼ばれる [4]。 入れ子データ型は単純に関手 Cpo → Cpo の始代数として解釈することは出来ない。 リスト 5.2

入れ子データ型の例

data PTree a = PZero a | PSucc ( PTree ( a, a) ) data Term a = Var a | App ( Term a) ( Term a) | Abs ( Term ( Bind a) ) data Bind a = Zero | Succ a

5.2 多相関数の圏 入れ子データ型を圏論的に扱うため、関手を対象、関手の間の多相関数を射とする圏を考え、その 上の関手の始代数や終余代数として扱うことが考えられる。PTree は P (F )(A) = A + F (A × A) と解釈される。これは全域的な関数を考えている場合には関手圏を考えることである [11]。 また、高階の多相性を考えるときには、同様の圏からの関手を考える。

– 28 –

第 5 章 多相関数の圏の場合

5.2. 多相関数の圏

しかし、領域理論的な圏の場合には、高階のデータ型と多相関数を解釈するのに、関手圏そのも のを用いることは適当ではない。何故ならば、{⊥ : F X → GX}X は多相関数としては定義でき るが、非正格な関数が存在する場合には自然変換にはならないためである。 補題 5.1. CPO 圏 C, D と 関手 F, G : D → C が与えられたとする。U : D⊥ → D を忘却関手と すると、{⊥F X→GX }X∈|D| は F U から GU への自然変換になっている。 証明.



◃ h : X → Y strict  Gh ◦ ⊥F X→GX   =  - G preserve strictness of h (命題 2.30)   ⊥F X→GY   =  - 命題 2.29 ⊥F Y →GY ◦ F h

定義 5.2. C, D を CPO 圏とする。CPO 圏 Functvrs (D, C) を以下のように定義する*1 。。

• 対象: CPO 構造に関する関手 D → C .

• 射 F → G: 自然変換 F U → GU • CPOC-0 (終対象): K1 : D → C • CPOC-1 (hom 集合の CPO 構造): – 順序: α ≤ β ⇔ ∀X ∈ |D|. αX ≤ βX – 上限:

⊔

αn = {

n<ω

⊔

αn X }X∈|D|

n<ω

– 最小元: ⊥F →G = {⊥F X→GX }X∈|D| • CPOC-2 (射の合成が連続かつ正格): 明らか • CPOC-3 (idempotent split): 明らか

.

系 5.3. α : F → G が正格であるのは、全ての X ∈ |D| について αX : F X → GX が正格である ときである。

補題 5.4. Functvrs (D, Cpo⊥ ) は余完備である。

*1

vrs は Variation Restricted to Strict morphism の略である

– 29–

第 5 章 多相関数の圏の場合

5.3. GADT

証明. Cpo⊥ は余完備なので、F : J → Functvrs (D, Cpo⊥ ) に対して、FX : J → Cpo⊥ を

FX (Y ) = F (Y, X) で定義し、(colimF )(X) = colimFX と定義する。 定理 5.5. U : Functvrs (D, Cpo⊥ ) → Functvrs (D, Cpo) を忘却関手とする。 関手 H : Functvrs (D, Cpo) → Functvrs (D, Cpo⊥ ) が CPO 構造に関する関手であるとする。

HU が ω 余完備ならば、U H の始代数が存在する。 証明. Functvrs (D, Cpo⊥ ) は余完備であり、始対象も存在するので、HU が余連続ならば、HU の 始代数が存在する。 定理 3.8 を H

Functvrs (D, Cpo) k

+ Functvrs (D, Cpo⊥ )

U

に対して適用し、U H の始代数が得られる。 また、Functvrs (D, Cpo⊥ ) は CPO 圏であるので、命題 2.33 からこれは HU の終余代数でもあ る。 この条件が成り立つとき、catamorphism や hylomorphism を利用することが出来る。

5.3 GADT GHC では GADT (Generalized Algebraic Datatypes) [17] という拡張機能が存在する。これ はリスト 5.3 のような文法で定義されるデータ型で、構築子によって型引数が変化する*2 。 リスト 5.3 GADT

data Term Lit Succ IsZero If eval eval eval eval eval

a where : : Int → Term Int : : Term Int → Term Int : : Term Int → Term Bool : : Term Bool → Term a → Term a → Term a

: : Term a → ( Lit i ) ( Succ t ) ( IsZero i ) ( I f b e1 e2)

a =i = 1 + eval t = eval i == 0 = i f eval b then eval e1 else eval e2 .

もし、二つの型 A, B が等しいことを表現する型 A = B が存在すれば、構築子による型引数の 変化を除去出来ることが知られている [6, 1, 25]。リスト 5.3 のデータ型はリスト 5.3 のように書 き換えることで通常の入れ子データ型と同様に扱える。 data Term a where *2

これを用いることで依存型のようなことが一部実現できるため、貧者のための依存型などと呼ばれることもある。

– 30–

第 5 章 多相関数の圏の場合 Lit Succ IsZero If

:: :: :: ::

5.4. 本章のまとめ

.

( a = Int) → Int → Term a . ( a = Int) → Term Int → Term a . ( a = Bool) → Term Int → Term a Term Bool → Term a → Term a → Term a .

多相ラムダ計算では A, B : k に対して、ライプニッツの等号 (A = B) = ∀F : k → ∗.(F A →

F B) を定義できる。また、多相ラムダ計算の領域理論的なモデルが存在する [7] ので、ライプニッ ツの等号を使って、この等号を解釈することが考えられる。 しかし、そのようにしても我々のアプローチでは始代数のように特徴付けることは出来ないこと .

が分かった。何故ならば、ライプニッツの等号 = は関手として振舞わないためである。

5.4 本章のまとめ 本章では前章までに示した基礎に基づいて、より複雑なデータ構造である、高階の多相性と入れ 子データ型、そして GADT について簡単に論じた。 高階の多相性は入れ子データ型を解釈するために Functvrs (D, Cpo⊥ ) を定義し、第 3 章におけ る条件と同様の条件を示した。 しかし、GADT についてはそのようなアプローチではうまくいかないことが分かった。

– 31–

第6章

結論

概要 この最後の章では本論文の貢献をまとめ、幾つかの今後の課題について検討を行う。

6.1 まとめ 本論文では、非正格な関数が存在する言語において融合変換を行う際に、始代数が存在しないこ とにより生じる問題について論じた。 この問題に対して、本論文では非正格な関数の存在する圏であってもデータ型が始代数になるた めの条件を示した。そのために、一般的な定理として「圏 C と圏 D の間に関手 F : C → D と関手

G : D → C が与えられたとき、F G : D → C の始代数が存在することと GF : C → D の始代数が 存在することとが同値であること」を示した。そして、それを用いて「任意の関数 f : A → B に 対して F (f ) が常に正格であるならば、F は CPO と連続関数の圏においても始代数を持つ」こと を示した。 この条件は関数型言語で通常使われている多くのデータ型をカバーするので、十分広い応用範囲 がある。また、簡単であるため Haskell の処理系に対して組み込むことは難しくないと考えられ、

Haskell のデータ型に対して適用する方法についても示した。 また、この条件を関手圏の変種に対して適用し、入れ子データ型が始代数となる条件についても 示した。

6.2 今後の課題 本論文における今後の課題としては以下のような項目が挙げられる。

6.2.1 更なる検討 第 4 章や第 5 章の内容は未だ十分に検討できているとは言いがたい。これらの章の内容につい てより詳細に検討することが必要だろう。

– 32 –

第 6 章 結論

6.2. 今後の課題

6.2.2 反変性を扱うよう拡張 本論文では、説明を簡略化するためにも、型変数が正の位置にしか現れない場合だけを扱い、共 変関手だけを用いていた。これを型変数が負の位置に現れる場合や両方の位置に現れる場合を扱う よう拡張することが考えられる。そのような拡張は容易である。 一つの方法は、用いる圏を Cpo 等から、射として埋め込みと射影の組を扱う圏に変更すること である。型変数が負の位置に現れる場合は通常は反変関手として解釈されるが、そのような圏では 共変関手として解釈可能である。したがって、共変関手のみを扱えばよくなる。 もう一つの方法は反変関手をそのまま扱う方法である。型上の各オペレータ F (X) の中で正の位 置に現れる X を X + 、負の位置に現れる X − と分けてしまい、2 引数の型オペレータ F (X − , X + ) として扱うことである。それによってこの型オペレータを関手 F : C op × C → C として扱うことが 可能になる。そして、始代数の代わりに正則自由両代数 (regular free dialgebra)[10] を用い、自然 変換の代わりに強対角自然変換 [22] を用いれば良い。

6.2.3 処理系への実装 第 4 章で示した Haskell への適用方法を実際に Haskell の処理系に実装することが考えられる。

6.2.4 変換アルゴリズムの導出 本論文では融合変換が可能であるための条件を示したが、変換を行うためのアルゴリズムを導出 してはいない。本論文で示した条件に基づいて変換を行うための具体的アルゴリズムを導出し、こ れも Haskell の処理系に実装することが考えられる。

6.2.5 パラメトリシティ 本論文では始代数の普遍性に基づいた融合変換を対象とした。しかし、プログラム変換の根拠に は普遍性だけでなく、多相ラムダ計算のパラメトリシティも用いられる。本論文のアプローチがパ ラメトリシティとパラメトリシティに基づいた融合変換に対して適用可能かどうか検証することが 考えられる。

6.2.6 操作的意味論との関係 本論文ではプログラムを表示的意味論の観点から扱っており、操作的意味論には触れなかった。 しかし、現代では表示的意味論よりも操作的意味論がプログラムを分析する道具として好んで使わ れている。 例えば、Pitts[23] は文脈等価性 (contextual equivalence) とそれに基づいた論理関係を定義し、 不動点演算子と再帰的データ型の存在する言語において再帰的データ型とチャーチエンコーディン

– 33–

第 6 章 結論

6.2. 今後の課題

グが文脈同型であることを示した。また、Johann はそれに基き、shortcut deforestation が正し いことを示した [15]。 それらの研究と本研究との関係を調べ、また本論文で示したことを操作的意味論の観点から分析 することが考えられる。

6.2.7 正格性と非正格性の組み合わせについて 本研究の途上では定理 3.8 を証明してから系 3.10 を導いたのではなく、実際には系 3.10 を一般 化することで定理 3.8 を証明した。そのきっかけとなったのは Benton[3] の直観主義論理と直観主 義線形論理のシーケントを混在させるロジックとそのモデルについて知ったことだった。本論文で

Cpo と Cpo⊥ を同時に考えるのはそこからきている。 表 6.1 の対応を考えると、Haskell ではなく Benton の計算体系を用いることにより、正格な関 数と非正格な関数をより精確に扱うことが考えられる。それによって、より精緻な結果が得られる 可能性がある。 表 6.1

プログラミング言語・計算体系・圏論理の関係

プログラミング言語

計算体系

圏

論理

Haskell

ラムダ計算 (call-by-name)

カルテシアン閉圏 (CCC)

直観主義論理

ML

ラムダ計算 (call-by-value)

モノイダル閉圏

直観主義線形論理

また、Haskell のような非正格な言語と ML のような正格な言語の関係を明らかにし、両者を組 み合わせたものとして、Rudiak-Gould らの研究 [24] がある。彼らは否定 (=継続) を含むが、含 意 (=関数) を含まない計算体系 IL (intermediate language) を作り、非正格な言語と正格な言語 を埋め込んだ。このアプローチとの関係も興味深いと考えている。

– 34–

謝辞 本論文の執筆に際しては、多くの方々のお世話になりました。 日頃より数多くの御指導・助言をいただきました萩野達也環境情報学部教授、服部隆志環境情報 学部助教授、向井国昭環境情報学部教授に深く感謝いたします。 萩野・服部研究室と向井研究室の諸氏の、日頃からのあたたかい励ましとご協力に、心よりお 礼申し上げます。この修士論文の執筆に際しても様々なご協力をいただきました。私が慣れない

LATEX で論文を書く上で、清水智公氏、中村翔吾氏らからアドバイスを頂きました。 また、今回修士論文を共に書いた安達央一郎氏、太田尚志氏、鈴木尚宏氏との切磋琢磨は大いに 励みとなりました。 圏論との出会いを与えてくれたのは向井国昭教授でした。また、山下伸夫氏の翻訳した Haskell のドキュメントがなければ、Haskell に出会うことはなかったかも知れません。これらの出会いが 無ければこの研究は始まってすらいなかったでしょう。 最後に、長い学生生活の間、経済的な支援とそれにとどまらない有形無形の支援をしてくれた両 親と家族に心から感謝いたします。 皆さん、本当にありがとうございました。

– 35 –

参考文献 [1] Arthur I. Baars and S. Doaitse Swierstra. Typing dynamic typing. In ICFP ’02: Proceedings of the seventh ACM SIGPLAN international conference on Functional programming, pp. 157–166, New York, NY, USA, 2002. ACM Press. [2] John Backus. Can programming be liberated from the von neumann style?: a functional style and its algebra of programs. Commun. ACM, Vol. 21, No. 8, pp. 613–641, 1978. [3] P. N. Benton. A mixed linear and non-linear logic: Proofs, terms and models (extended abstract). In CSL, pp. 121–135, 1994. [4] Richard Bird and Lambert Meertens. Nested datatypes. In J. Jeuring, editor, Proceedings 4th Int. Conf. on Mathematics of Program Construction, MPC’98, Marstrand, Sweden, 15–17 June 1998, Vol. 1422, pp. 52–67. Springer-Verlag, Berlin, 1998. [5] The caml language. http://caml.inria.fr/. [6] J. Cheney and R. Hinze. A lightweight implementation of generics and dynamics, 2002. [7] Thierry Coquand, Carl A. Gunter, and Glynn Winskel. Domain theoretic models of polymorphism. Information and Computation, Vol. 81, No. 2, pp. 123–167, 1989. [8] Maarten Fokkinga. Law and Order in Algorithmics. PhD thesis, University of Twente, Enschede, February 1992. [9] Maarten Fokkinga and Erik Meijer. Program calculation properties of continuous algebras. Technical Report 91-4, Computer Science/Department of Algorithmics and Architecture, CWI, Amsterdam, NL, 1991. [10] Peter J. Freyd. Recursive types reduced to inductive types. In Proceedings 5th IEEE Annual Symp. on Logic in Computer Science, LICS’90 (Philadelphia, PA, USA, 4-7 June 1990), pp. 498–507. IEEE Computer Society Press, Los Alamitos, 1990. [11] Neil Ghani and Patricia Johann. Folds, church encodings, builds, and short cut fusion for nested types: A principled approach. Preprint, 2006. [12] Tatsuya Hagino. A Categorical Programming Language. PhD thesis, University of Edinburgh, 1987. ECS-LFCS-87-38, http://www.tom.sfc.keio.ac.jp/∼hagino/index. html.en. [13] Haskell – a purely functional language. http://www.haskell.org/.

– 36 –

参考文献

[14] Zhenjiang Hu, Hideya Iwasaki, and Masato Takeichi. Deriving structural hylomorphisms from recursive definitions. In Proceedings 1st ACM SIGPLAN Int. Conf. on Functional Programming, ICFP’96, Philadelphia, PA, USA, 24–26 May 1996, Vol. 31(6), pp. 73–82. ACM Press, New York, 1996. [15] Patricia Johann. Short cut fusion is correct. J. Funct. Program., Vol. 13, No. 4, pp. 797–814, 2003. [16] Simon Peyton Jones and John Hughes (editors). Haskell 98: A non-strict, purely functional language. Technical report, February 1999. [17] Simon Peyton Jones, Dimitrios Vytiniotis, Stephanie Weirich, and Geoffrey Washburn. Simple unification-based type inference for gadts. SIGPLAN Not., Vol. 41, No. 9, pp. 50–61, 2006. [18] Joachim Lambek. Subequalizers. Canadian Math. Bull., Vol. 13, pp. 337–349, 1970. [19] Saunders MacLane. Categories for the Working Mathematician. Springer, 1971. [20] Erik Meijer, Maarten Fokkinga, and Ross Paterson. Functional programming with bananas, lenses, envelopes and barbed wire. In J. Hughes, editor, Proceedings 5th ACM Conf. on Functional Programming Languages and Computer Architecture, FPCA’91, Cambridge, MA, USA, 26–30 Aug 1991, Vol. 523, pp. 124–144. Springer-Verlag, Berlin, 1991. [21] Robin Milner, Mads Tofte, Robert Harper, and David Macqueen. The Definition of Standard ML - Revised. The MIT Press, May 1997. ˜ [22] Philip S. Mulry. Strong monads, algebras and fixed points. In P.T.Johnstone ˜ M.P.Fourman and A.M. Pitts, editors, Applications of Categories in Computer Science : Proceedings of the London Mathematical Society Symposium, Durham, 1991, No. 177 in London Mathematical Society Lecture Note Series, pp. 202–216. Cambridge University Press, 1992. [23] Andrew M. Pitts. Parametric polymorphism and operational equivalence. Mathematical Structures in Computer Science, Vol. 10, No. 3, pp. 321–359, 2000. [24] Ben Rudiak-Gould, Alan Mycroft, and Simon P. Jones. Haskell is not not ml. 2006. [25] Martin Sulzmann, Manuel Chakravarty, and Simon Peyton Jones. System f with type equality coercions. Submitted to POPL 2007, July 2007. http://research.microsoft. com/∼simonpj/papers/ext-f/. [26] Akihiko Takano and Erik Meijer. Shortcut deforestation in calculational form. In Conf. Record 7th ACM SIGPLAN/SIGARCH Int. Conf. on Functional Programming Languages and Computer Architecture, FPCA’95, La Jolla, San Diego, CA, USA, 25–28 June 1995, pp. 306–313. ACM Press, New York, 1995. [27] Tarmo Uustalu, Varmo Vene, and Alberto Pardo. Recursion schemes from comonads. Nordic Journal of Computing, Vol. 8, No. 3, pp. 366–390, Fall 2001. – 37–

参考文献

[28] Varmo Vene. Categorical programming with inductive and coinductive types. PhD thesis, University of Tartu, August 2000. [29] 長谷川立. チュートリアル パラメトリック・ポリモルフィズム. コンピュータソフトウェア, Vol. 20, No. 2, March 2003. [30] 尾上能之. 融合変換による関数プログラムの最適化. 博士論文 http://www.ipl.t.u-tokyo.ac.jp/∼onoue/pub/drthesis02.pdf.

– 38–