「Catamorphism」の版間の差分

削除された内容追加された内容

インライン

2012年4月23日 (月) 11:30時点における版

圏論において、Catamorphism(ギリシャ語: κατά = 下方へ または ～に従って; μορφή = 形式または形)は、始代数から他のいくつかの代数への準同型射を意味する概念である。この概念は関数型プログラミングのfoldに適用されている。

anamorphismはこの双対となる概念である。Hylomorphismも参照。

関数型プログラミングにおけるCatamorphism

関数型プログラミングでは、catamorphismはリストのfoldとして知られる始代数を、任意の代数的データ型で記述できるように一般化したものである。

プログラミングにおいてcatamorphismの概念を導入した最初の出版物の一つは、“Functional Programming with Bananas, Lenses, Envelopes and Barbed Wire”, by Erik Meijer et al.[1]で、Bird-Meertens formalismの文脈であった。

双対であるAnamorphismは、unfoldの一般化である。

例

次の例はHaskellによるもの。

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

type TreeAlgebra a r = (a -> r, r -> r -> r)

foldTree :: TreeAlgebra a r -> Tree a -> r
foldTree (f, g) (Leaf x)     = f x
foldTree (f, g) (Branch l r) = g (foldTree (f, g) l) (foldTree (f, g) r)

treeDepth :: TreeAlgebra a Integer
treeDepth = (const 1, \l r -> 1 + max l r)

sumTree :: (Num a) => TreeAlgebra a a
sumTree = (id, (+))

ここで、foldTree (f, g) はデータ型Tree a のcatamorphismで、 treeDepth とsumTree は代数と呼ばれる。

圏論におけるCatamorphisms

圏論は、全ての基礎的なデータ型に一般的な定義を与えるための必要不可欠な概念を提供する(関数型プログラミングでは関数を識別するのに圏論の射が使われ、集合の圏または、いくつかの関連する圏として構成する)。これはGrant Malcolmによって行われた。^[1]^[2].

上記の例に戻り、rからa + r × rを対応させる関手Fを考える。この特殊な場合はF代数のために、組(r, [f1,f2])、ここでr は対象、そして二つの射 f1 と f2 は

f1: a → r

f2: r × r → r

で定義される。

そのような関手F上のF-代数の圏で、始代数が存在すれば、Tree、またはHaskellの項、(Tree a, [Leaf, Branch])で表現する。

Tree a はF-代数の圏の始対象であり、Tree aから任意のF-代数へ一意な準同型射を与える。この一意な準同型射はcatamorphismと呼ばれる。

一般的な場合

圏論では、catamorphismはanamorphismの圏論的双対である。(そしてanamorphismはcatamorphismの圏論的双対でもある)

この意味は次の通り。

(A, in)はそれ自体、いくつかの圏のいくつかの自己関手Fの始代数と仮定する。従って、inはFAからAへの射で、他のF-代数(X, f)の始対象であると仮定できる。(射fはf : X → Y)

(A, in)から(X, f)への一意な準同型射hがあり、hはh . in = f . Fhであるようなh : A → X。よって、このようなfはcata fで一意に指定された射hによって表す。

言い換えれば、上記はいくつかの固定されたF、A、inによって与えられる次の定義の関係を持つ。

$h=\mathrm {cata} \ f$
$h\circ in=f\circ Fh$

記法

cata f は別の記法 $(\!|f|\!)$ と記されることがある。使用されている開いた括弧は「バナナ括弧」として知られ、Meijer 1991などで記載された後は、catamorphismは時に「バナナ」と呼ばれる。

参考リンク

^ Malcolm, Grant (1990) (Ph.D. Thesis), Algebraic types and program transformation, University of Groningen .
^ Malcolm, Grant (1990), “Data structures and program transformation”, Science of Computer Programming 14 (2-3): 255–279, doi:10.1016/0167-6423(90)90023-7 .

参考文献

Erik Meijer (computer scientist), Maarten Fokkinga, and Ross Paterson. "Functional Programming with Bananas, Lenses, Envelopes, and Barbed Wire".
Ki Yung Ahn and Tim Sheard (2011). "A hierarchy of mendler style recursion combinators: taming inductive datatypes with negative occurrences". Proceedings of the 16th ACM SIGPLAN international conference on Functional programming (ICFP '11).

外部リンク

Catamorphisms page on Haskellwiki
Catamorphisms by Edward Kmett at Google Knol
Catamorphisms in F# (Part 1, 2, 3, 4, 5, 6, 7) by Brian McNamara
Catamorphisms in Haskell

[1] Malcolm, Grant (1990) (Ph.D. Thesis), Algebraic types and program transformation, University of Groningen .

[2] Malcolm, Grant (1990), “Data structures and program transformation”, Science of Computer Programming 14 (2-3): 255–279, doi:10.1016/0167-6423(90)90023-7 .

[1]

[2]