bonotakeの日記

元・ソフトウェア工学系研究者、今・AI系エンジニア

カリー化は自然変換?

英語版Wikipediaの記事 "Currying"*1 より。

In category theory, currying can be found in the universal property of an exponential object, which gives rise to the following adjunction: There is a natural isomorphism between the morphisms from a binary product f : X \times Y \to Z and the morphisms to an exponential object  g: X \to Z^Y.

強調は引用者。
何じゃ?と一瞬思ったけど…この記事にかなり好意的な解釈をすれば、(下にも書いたけれど、カルテシアン閉圏 (CCC) なら)カリー化に対応する射curryが、関手 Hom(- \times Y, -) *2 から Hom(-, -^Y) *3 への自然変換になってる、ということですか。

で、curryのinverseとなる射uncurryがあって、こっちは Hom(-, -^Y) から Hom(- \times Y, -) への自然変換。

ということで、(CCCなら)Hom(- \times Y, -)Hom(-, -^Y) は自然同型になっている。つまり、curry / uncurry は全単射になってるって事で、ある関数をカリー化(非カリー化)した結果は常に一意に定まるし、別々の関数をカリー化(非カリー化)した結果が同一になることは無い。

ちなみに、これらの性質は、ある対象Yとの積を得る関手 F = (-) \times Y と、Yによる冪対象を得る関手 G = (-)^Yが随伴 ( F \dashv G ) になっている事に因る。



…と、引用した記事に肯定的な解釈をしてみたけど、元記事はやや不正確なところがあって、常に自然同型かどうかは、実際はちょっと怪しい。元記事が正しくなるためには、CCCである事が前提でなければならないと思われる。

あと厳密には、Homで取っちゃうと、(元の圏を離れて)集合の圏で考える事になるので、純粋なカリー化とは微妙に違っちゃう気もするんだけど…あくまで「カリー化に対応する性質が見られる」という事で、まぁ、これはいいのかなぁ。

*1:2006年12月31日 (日) 08:08 の版

*2:X×Y→Z の型の関数の集合に相当。ただしY固定。

*3:X→(Y→Z) の型の関数の集合に相当。ただしY固定。

注:bonotakeは、amazon.co.jpを宣伝しリンクすることによってサイトが紹介料を獲得できる手段を提供することを目的に設定されたアフィリエイト宣伝プログラムである、 Amazonアソシエイト・プログラムの参加者です。