修士論文

題目

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

Title

Fusion Transformations Applicable to Non-Strict Functions

概要

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

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

しかし、CPOと正格な連続関数の圏では再帰的データ型を始代数として解釈可能であるが、CPOと(正格なものに制限されない全ての)連続関数の圏では一般には再帰的データ型を始代数と解釈できるとは限らない。 一方、プログラム変換の中にはデータ型が始代数であることを利用するものが存在する。 そのような変換は対象となる関数が正格である場合に制限されてしまう。

そこで本論文では正格性の条件を必要とせずに変換を行うことを目的として、 非正格な関数の存在する圏であってもデータ型が始代数になるための条件を示す。 そのために、一般的な定理として 「圏Cと圏Dの間に関手 F: C→D と 関手G: D→Cが与えられたとき、 FG: D→C の始代数が存在することと GF: C→D の始代数が存在することとが同値であること」を示す。 そして、それを用いて「任意の関数 f: A→B に対して F(f) が常に正格であるならば、FはCPOと連続関数の圏においても始代数を持つ」ことを示す。 関数型言語で通常使われている多くのデータ型はこの条件を満たす。

さらに、その条件をHaskellにおけるデータ型に適用する。 また、入れ子データ型が関手圏の変種で始代数となる条件についても述べる。

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 data 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 FG: 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.

bibtex

@mastersthesis { sakai2007fusion ,
  author = "酒井 政裕",
  yomi   = "Masahiro Sakai",
  title  = "非正格関数に対して適用可能な融合変換",
  year   = "2007",
  month  = "January",
  school = "慶應義塾大学 政策・メディア研究科",
  url    = "https://msakai.jp/hiki/?MasterThesis",
}
Last modified:2015/02/06 17:08:55
Keyword(s):
References:[Writings]