このブログの更新は Twitterアカウント @m_hiyama で通知されます。
Follow @m_hiyama

メールでのご連絡は hiyama{at}chimaira{dot}org まで。

はじめてのメールはスパムと判定されることがあります。最初は、信頼されているドメインから差し障りのない文面を送っていただけると、スパムと判定されにくいと思います。

参照用 記事

キュリアの格上げによる総称の解釈

「キュリアの格上げ」とは、圏の対象を関手、圏の射を自然変換とみなす方法です。ピエル=ルイ・キュリア(Pierre-Louis Curien)の "The Joy of String Diagrams"(http://hal.archives-ouvertes.fr/docs/00/69/71/15/PDF/csl-2008.pdf)を読んで初めて知ったのでそう呼んでますが、キュリアが最初の発見者かどうかは定かじゃないです(たぶん違うでしょう)。次の記事のなかで、キュリア流の絵算とキュリアの格上げを説明しています。

キュリアの格上げは、対象、射、関手、自然変換を混ぜるための便利なトリック、とそう考えてました、昨日まで。今日になってふと気がついたのですが、キュリアの格上げはもっと応用範囲が広くて、総称プログラミングの手法としても使えそうです。ここで「総称」とは、「型パラメータを持つ」という程度の意味です。

自然変換に対応する総称関数(例えばzip)と通常の関数が混じって出てくることは普通です。総称関数と通常の関数の中間のようなモノ(例えば、リストの長さ)もあります。異なるメタレベルにあるモノをごちゃ混ぜにして計算するとき、キュリアの格上げで解釈するとスッキリしそうです。

内容:

元ネタと例題

キュリアの格上げを総称(型パラメータ)に応用できそうだ、と思ったきっかけは次の論文です。最初の2ページしか読んでませんけど (苦笑)。

このなかに、ツリーからリストを作って、そのリストの長さにより「ツリーのldepth(左深さ)」を定義する話があるので、これを例題にします。

リストとツリー

リストの定義をBNF風に書けば、

  • List ::= ε | A List

ここで、εは空リスト、Aはリストの項目となる構文要素です。「A List」は「AとListの単なる連接」ですが、プログラミング言語のデータ構造として考えるときは、consオペレータ(生成子、構成子)が必要です。Haskellのデータ定義風に書けば、

  • data List α = Nil | Cons α (List α)

ここでNilは空リスト(あるいはリストの終端記号)を表します(これもデータ構成子です)。Consは、左右の構成要素から二分木を作るオペレータです。そしてαは型パラメータです。αを整数型に具体化して、リストの実例を1つ書けば:

  ・
 / \
1   ・
   / \
  2    ・
        / \
     3   nil

これは、普通 (1 2 3) とか [1, 2, 3] と書かれます。consオペレータを中置のドット演算子(ピリオド)として書けば、(1 . (2 . (3 . nil))) となります。図でも二分木のノードがドット(・)なので、図とドット記法は直接的に対応します。

リストもデータ構造としてはツリーの一種ですが、それとは別にノードに値を持ったツリーを考えましょう。リストが二分木だったので、今度は三分木となります。三分木の基本構成素は次のようです。

    ・
  / | \
左の枝 値 右の枝

値をノードに書き込んだ形にしたほうが図示は簡略になります。

    値
  /   \
左の枝   右の枝

こうすると、ノードに値を持つ二分木として描けます。形状は同じ二分木でも、リストは「・」で示した分岐ノードに値を持ちません。今説明しているツリーはすべてのノードで値を持ちます。

今説明したツリーを、Haskellのデータ定義風で書けば次のようになります。

  • data Tree α = Empty | Node α (Tree α) (Tree α)

Emptyはノードを1つも持たない空ツリー、Nodeは「値、左の枝、右の枝」の3つの引数をとるデータ構成子です。αは、ノードの値の型を表す型パラメータです。

ツリーの左スパインと左深さ

先ほど定義したツリーでは、ノードは左右の枝を持ちますが、「ルート→左の枝→左の枝→ …」とルートから左の枝だけをたどっていきます。出会ったノードの値を並べるとリストになります。出来上がったリストをツリーの左スパイン(left spine )と呼びます。

左スパインはリストなので、その長さを取ることができます。ツリーの左スパインの長さを、そのツリーの左深さ(left depth)と呼ぶことにします。

左スパインも左深さも直感的には難しくない概念です。tがツリーだとして、左深さを ldepth(t) とすると、次の定義の意味は明らかでしょう。

  • ldepth(t) = length(lspine(t))

ldepthのプロファイル(関数の域と余域)をHaskell風(つっても、コロンを2個にするだけ)に書くと、ldepth :: Tree → Int ですが、Treeには型パラメータαが入っていたので、ldepth :: Tree α → Int となります。関数ldepthは、型αがなんであっても同じアルゴリズムで処理できますが、潜在的に型パラメータを持った総称関数と考えることができます。

総称関数と自然変換

ここからは、Haskell風記法にはこだわらないことにします。圏論風の記法に切り替えます。ListとTreeは、適当な圏の上の自己関手と考えます。Tが圏の対象のとき、例えば List(T) は、型がTであるデータをリスト項目とするリスト型です。型パラメータαとは、関手Fを λα.F(α) とラムダ抽象で書いた時の束縛変数のことです。圏論の習慣では、ギリシャ文字は自然変換を表すので、型パラメータにギリシャ文字を使うのはやめて、λT.F(T) のようにします。型定数(具体的な型の名前)と型パラメータに構文上の区別はなくて、ラムダ束縛の状況により型パラメータかそうでないか(自由な型名か)を判断します。

先のlspineは、型パラメータを持つので、それを明示的に書くときは、山形カッコを使って lspine<T> とします。DOTNなら左から右の方向なので T.lspine と書くのですが、行きがかり上、右から左に適用される記法を使います。型パラメータを明示的に書いたlspineのプロファイルは、

  • lspine<T> : Tree(T)→List(T)

山形カッコの代わりに下付き添字にすると、

  • lspineT : Tree(T)→List(T)

自然変換の雰囲気が出てきました。実際、f:S→T に対して次の図式は可換になります。

Tree(S) -(lspine<S>)--> List(S)
  |                       |
(Tree(f))               (List(f))
  |                       |
  v                       v
Tree(T) -(lspine<T>)--> List(T)

ここで、Tree(f) と List(f) は関手の射部分(morphism part)ですが、Tree.map(f)、List.map(f) と書いたほうが分かりやすいでしょう。List.map(f) はお馴染みのマップ関数です。Tree.map(f) も List.map(f) と同様で、ツリーの形状を変えずに、ノードの値にfを適用した結果のツリーを返します。

以上のことから、総称関数(型パラメータを持つ関数)lspineは、関手Treeから関手Listへの自然変換だと分かりました。

リストの長さも自然変換?

lspineはきれいに自然変換になってました。リストの長さはどうでしょうか。

  • length<T> : List(T)→Int

矢印の先は型定数Intなので、型パラメータを持ちません。となると、lengthは自然変換とは考えられない … いやっ、待て、Intはデータ型、つまり圏の対象です。圏の対象はキュリアの格上げをすると関手です。そう、Intは関手とみなせるのです。

考えてみると、これって当たり前でよく使っている事でした。例えば、整数定数1に対して function(){return 1;} という関数を作れます。定数と引数なしの関数は同一視できるのです。それどころか、function(x){return 1;} でも function(x, y){return 1;} でもかまいません。集合Yの要素bは、任意の集合Xに対して、consantb:X→Y という定数関数を定義します。

同様に、圏の対象は、任意の圏からの定数関手とみなせます。だから、対象=型定数であるIntも関手とみなせます。関手とみなしたIntをInt'と書くと:

  • length<T> : List(T)→Int'

そして次の図は可換になります。

List(S) -(length<S>)--> Int'(S)
  |                       |
(List(f))               (Int'(f))
  |                       |
  v                       v
List(T) -(length<T>)--> Int'(T)

ここで、Int'(f) はIntの恒等射です。つまり、リストのマップ関数はリストの長さを変えない、という事実を表しています。

関手List、Tree、自然変換ldepth、lengthなどが働く舞台となる圏をCとすると、次の等式は、Cの自己関手の圏のなかの自然変換に対する等式と解釈できます。

  • ldepth(t) = length(lspine(t))

圏論的に言えば、関手Treeから関手Int'への自然変換ldepthは、関手Treeから関手Listへの自然変換lspineと、関手Listから関手Int'への自然変換lengthの縦結合(vertical composition)で与えられます。

大げさな事

「lengthなんてただの関数なのに、自然変換だなんて大げさ過ぎる」と思うかもしれません。まー、実際大げさなんですよ。「圏論の計算を劇的に簡単にするための考察 (1)」で述べたように、「対象→関手、射→自然変換」という格上げは、メタレベルを一気に三段階昇るという豪快なものです。抽象度がグンと上がります。

大げさな事をするメリットは、本質的に自然変換の特徴を持つlspineやzipのような総称関数と、整数の足し算などのどうってことない関数が、同じ土俵で扱えることです。高いメタレベルに棲んでいる高階の対象物を下の階層に引きずり落とす方法もありますが、下の階層にいる具体物を高いメタレベルに揃えるのがキュリアの格上げです。場合によって、高いメタレベルで計算したほうがスッキリして楽になることもあります。