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

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

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

参照用 記事

モノイド閉圏: カリー化からニョロニョロまで

昨日の記事「ラムダ計算の自然性とお絵描き」で、ラムダ計算を行える〈do lambda calculus〉環境としてのモノイド閉圏を紹介しました。モノイド閉圏はカリー化を持ちます。カリー化に関わる素材と法則があれば、そこから指数随伴系〈テンソル・ホム随伴系〉を構成できます。

この記事では、カリー化から出発して、随伴系 -- つまりニョロニョロ等式を満たす2-圏的構造を構成してみます。

内容:

随伴系の指標

随伴系〈adjunction | adjoint system〉の指標を書いてみます。指標については「構造とその素材の書き表し方」を参照してください。

signature Adjunction in CAT {
  sort A
  sort B
  operation F:AB
  operation G:BA
  two-operation η::A^⇒F*G:AA
  two-operation ε::G*F⇒B^:BB

  equation snake-1::: (η*F^);(F^*ε) = F^ :: F⇒F:AB
  equation snake-2::: (G^*η);(ε*G^) = G^ :: G⇒G:BA
}

まず、1行目の 'in CAT' で、この指標を考える場所は(小さいとは限らない)圏の圏 CAT だと分かります。CATは2-圏なので、対象(sort)、射(operation)以外に2-射(two-operation)があります。そして、随伴系の法則として3-射である等式(equation)があります。コロンの個数が射の次元に一致しています(sort=0-射=対象=圏、operation=1-射=射=関手、two-operation=2-射=自然変換、equation=3-射=自然変換の等式)。後置のカレット記号('^')は、“恒等”を作る演算子として使っています。A^ は圏Aの恒等関手、F^ は関手Fの恒等自然変換など。使っている二項演算子記号については、「関手と自然変換の計算に出てくる演算子記号とか // 今後使う予定の演算子記号」を参照してください。

この指標に出てきた2つの等式(snake-1とsnake-2)がニョロニョロ等式〈snake {equation | relation | identity | law}〉です。"snake"を「ニョロニョロ」と訳しはじめた経緯は次の記事を参照。

随伴系のインスタンスΣがあるとして、「構造とその素材の書き表し方」の標準的記法を使えば次のように書けます。

  • Σ = (Σ.A, Σ.B, Σ.F, Σ.G, Σ.η, Σ.ε)

随伴に関する注意事項」に従って書けば:

  • Σ = (Ση, Σε : ΣF -| ΣG, ΣF:ΣAΣB)

ここで、インスタンスΣを示す修飾子は左肩に付けています。右の上下添字は他の目的に使う可能性があるからです。後で、この書き方に近い記法を使います。

指数随伴系

モノイド閉圏Cの特徴は、対象 A∈|C| ごとに指数随伴系〈テンソル・ホム随伴系〉が存在することです。対象Aに対する随伴系を Σ[A] と書きましょう。Σ[A]の構成素に付ける添字はAだけにします。つまり、次のように書きます。

  • Σ[A] = (Aη, Aε : AF -| AG, AF:AAAB)

さらに次の約束をします。

  1. AF は、無名ラムダ変数やHaskell風セクション記法を使って直接書く。AF = (-\otimesA) = (\otimesA)
  2. AG も同様。AG = [A, -]
  3. Aが何であっても AA = AB = C であり、Cは了解されているので省略する。

結局、対象Aに対する指数随伴系Σ[A]は、

  • Σ[A] = (Aη, Aε : (\otimesA) -| [A, -])

指数随伴系Σ[A]の存在を示すには、単位Aηと余単位Aεを定義して、それらがニョロニョロ等式を満たすことを示せばいいわけです。

が、いきなりニョロニョロ等式は難しいことがあるので、カリー化同型写像 ΛX,AY:C(X\otimesA, Y)→C(X, [A, Y]) からボトムアップで指数随伴系を組み上げることが多いでしょう。ここでもボトムアップ・アプローチを採用します。

カリー化と反カリー化の対称性

ラムダ計算では、カリー化〈ラムダ抽象〉、エバル〈evaluator〉*1、ベータ変換等式を主に扱います。反カリー化は積極的には扱いません。しかしここでは、カリー化と反カリー化を対等に対称的に扱います。カリー化Λの逆写像Λ-1、つまり反カリー化をΓと書くことにします。

カリー化/反カリー化に関わる概念(まだ説明してない)を表にまとめておきます。説明は後述します。\newcommand{\id}{\mbox{id}}

カリー化 反カリー化
写像 Λ 写像 Γ
エバル ev インス ins
ベータ変換等式 イータ変換等式
ラムダベント \overset{\lambda}{\cap} ガンマベント \underset{\gamma}{\cup}
余単位 ε 単位 η
テンソリング後結合 ホミング前結合
\epsilon = \Gamma(\id_{[A, X]})  \eta = \Lambda(\id_{X \otimes A})

Cの対象 X, A, Y の三つ組ごとに、カリー化/反カリー化のペアが与えられていて、次は成立していると仮定します。

  1. ΛX,AY : C(X\otimesA, Y)→C(X, [A, Y])
  2. ΓXA,Y : C(X, [A, Y])→C(X\otimesA, Y)
  3. ΛX,AYXA,Y = idC(X\otimesA, Y)
  4. ΓXA,YX,AY = idC(X, [A, Y])

\require{AMScd}
\begin{CD}
{\mathcal C}(X \otimes A, Y) @>{\Lambda^{X, A}_Y}>> {\mathcal C}(X, [A, Y]) \\
@|                                                  @| \\
{\mathcal C}(X \otimes A, Y) @<{\Gamma^X_{A, Y}}<< {\mathcal C}(X, [A, Y]) \\
\end{CD}

二変数射と高階射

昨日述べたように、カリー化の典型事例は「二変数関数から一変数高階関数」への変換、反カリー化の典型事例は「一変数高階関数から二変数関数」への変換です。

一般的な議論でも、この典型事例の“雰囲気”を醸し出すために、「二変数射」「高階射」という言葉を使いましょう*2二変数射〈two-variable morphism | morphism of two variables〉とは、適当な対象 X, A, Y に対する X\otimesA→Y というプロファイル(域と余域)を持つ射です。そして高階射〈higher-order morphism〉は、X→[A, Y] という、余域が指数〈内部ホム〉であるプロファイルを持つ射です。

Iをモノイド圏のモノイド単位対象とすれば、どんな射 f:X→Y でも、X\otimesI→Y とみなすことができるので、二変数射だと言えます。また、X→[I, Y] という高階射とみなしてもかまいません。なので、二変数射/高階射という分類は絶対的な意味はないのですが、比喩としての心理的な効果はあり、説明には便利な言葉です。

ここから後の説明では、高階射(とみなしたい射)は、F, G などの大文字で表すことにします。例えば、カリー化Λの結果は高階射なので、G = Λ(f) のように書きます。ΓはΛの逆なので、Γ(G) = f ですね。

エバルとベータ変換等式

ラムダ計算を支配している法則は、ベータ変換等式だと言っていいでしょう。ベータ変換等式には次のモノが登場します。

  1. カリー化 Λ = ΛX,AY:C(X\otimesA, Y)→C(X, [A, Y])
  2. エバル ev = AevX : [A, X]\otimesA→X in C

エバル(evaluatorの略称)と呼ばれる特別な射によって、カリー化の逆が作れることを主張するのがベータ変換等式です。公理的な定義では、ベータ変換等式を満たすような特別な射をエバルと呼び、その存在を公理的に要請します。よって、エバルとベータ変換等式は一緒に導入されます。

次の等式がベータ変換等式〈equation of beta reduction〉で、そこに登場する射 AevXエバ〈eval | evaluator〉です。 \newcommand{\For}{\mbox{For}\:\:}\newcommand{\cat}[1]{{\mathcal {#1}}}

  • \For f : X\otimes A \to Y \:\mbox{in}\: \cat{C},\\ (\Lambda^{X,A}_Y(f)\otimes \id_A);{^A ev_X} = f

添字を省略して簡略に書けば:

  • (Λ(f)\otimesA^);ev = f (A^ はAの恒等射)

ベータ変換等式を絵で描けば次のようになります。描画の約束は「ラムダ計算の自然性とお絵描き」を参照してください

絵のなかで、小文字'λ'でマークされた部分をラムダベント〈lambda bent〉またはラムダカーブ〈lambda curve〉と呼びましょう。ワイヤー〈ストリング〉をラムダベントの形に曲げることがカリー化の実行になります。

'ε'でマークされたお団子〈ノード〉がエバルです。後で、ev = ε と別名を付けます。絵からの比喩的表現を使えば、ワイヤーAを思いっきり引っ張って真っすぐにすること〈ストレッチング〉がベータ変換です。引っ張ることにより、εが消滅し、ラムダベントは伸びます。

ベータ変換等式は、次のように解釈できます。

  •  G \mapsto (G \otimes \id_A);ev という対応は、カリー化Λの逆写像となる。

カリー化の逆写像は反カリー化Γなので、

  •  \Gamma(G) = (G \otimes \id_A);ev

という、Γの具体的な表示が得られます。Γは、idAによる右テンソリング(モノイド積の意味の掛け算)して、evを後結合〈post-composition〉してます。

  • 反カリー化Γは、テンソリングと後結合で作れる。

逆に反カリー化ありきなら、エバルは反カリー化から作れます。

  •  ev = \Gamma(\id_{[A, X]})

エバルありきから反カリー化を作っても、反カリー化ありきからエバルを作ってもかまいません。いずれにしても、ベータ変換等式が構造と状況を統制しています。

インスとイータ変換等式

カリー化ではなく反カリー化をベースにして、前節と並行的に、インスとイータ変換等式を説明します。文面は、前節のコピーを修正したものです。

イータ変換等式には次のモノが登場します。

  1. 反カリー化 Γ = ΓXA,Y:C(X, [A, Y])→C(X\otimesA, Y)
  2. インス ins = AinsX : X→[A, X\otimesA] in C

インス(inserterの略称)と呼ばれる特別な射によって、反カリー化の逆が作れることを主張するのがイータ変換等式です。公理的な定義では、イータ変換等式を満たすような特別な射をインスと呼び、その存在を公理的に要請します。よって、インスとイータ変換等式は一緒に導入されます。

次の等式がイータ変換等式〈equation of eta reduction〉で、そこに登場する射 AinsXインス〈ins | inserter〉です。

  • \For G : X \to [A, Y] \:\mbox{in}\: \cat{C},\\ {^A ins_X};[\id_A, \Gamma^{X}_{A,Y}(G)] = G

添字を省略して簡略に書けば:

  • ins:[A^, Γ(G)] = G (A^ はAの恒等射)

イータ変換等式を絵で描けば次のようになります。

絵のなかで、小文字'γ'でマークされた部分をガンマベント〈gamma bent〉またはガンマカーブ〈lambda curve〉と呼びましょう。ワイヤー〈ストリング〉をガンマベントの形に曲げることが反カリー化の実行になります。

'η'でマークされたお団子〈ノード〉がインスです。後で、ins = η と別名を付けます。絵からの比喩的表現を使えば、ワイヤーAを思いっきり引っ張って真っすぐにすること〈ストレッチング〉がイータ変換です。引っ張ることにより、ηが消滅し、ガンマベントは伸びます。

イータ変換等式は、次のように解釈できます。

  •  f \mapsto ins;[\id_A, f] という対応は、反カリー化Γの逆写像となる。

反カリー化の逆写像はカリー化Λなので、

  •  \Lambda(f) = ins;[\id_A, f]

という、Λの具体的な表示が得られます。Λは、idAによる左ホミング(内部ホムの意味の累乗)して、insを前結合〈pret-composition〉してます。

  • カリー化Λは、ホミングと前結合で作れる。

逆にカリー化ありきなら、インスはカリー化から作れます。

  •  ins = \Lambda(\id_{X \otimes A})

インスありきからカリー化を作っても、カリー化ありきからインスを作ってもかまいません。いずれにしても、イータ変換等式が構造と状況を統制しています。

随伴系の単位と余単位

前々節と前節において、「エバルとベータ変換等式」と「インスとイータ変換等式」を並行的に扱いました。二種の概念群に対称性(あるいは双対性)があることが分かるでしょう。しかし、ラムダ計算では、「インスとイータ変換等式」はあまり注目しません。言及する場合でも、関数の外延性として紹介されます。そのときは、イータ変換の絵も次のように描かれます。

この暗い写真は2009年に僕が説明しているホワイトボードです。ちなみに、ベータ変換の説明は:

ちょうど10年前ですね(どうでもいけど)。

[補足]
カリー化=ラムダ抽象はインスで表現可能で、反カリー化=ラムダ反抽象はエバルで表現可能です。絵で考えれば、カリー化=ラムダベンディング操作がインス=ηノードのホミング前結合で表現され、反カリー化=ガンマベンディング操作がエバル=εノードのテンソリング後結合で表現されることになります。この状況は次の絵等式で覚えておくと便利です。



[/補足]

さて、今回エバルとインスを並行的/対称的に扱ったのは、随伴系にスムーズに結びつけるためです。次の事実があるのです。

  • エバルは指数随伴系の余単位である。
  • インスは指数随伴系の単位である。

随伴系における記法と合わせるために、次のように別名定義します。

  • Aε = Aev
  • Aη = Ains

Aε, Aη は自然変換となり、次のプロファイルを持ちます。

  • Aε:: [A, -]\otimesA⇒C^:CC
  • Aη:: C^⇒[A, -\otimesA]:CC

対象Xでの成分を取れば:

  • AεX: [A, X]\otimesA→X in C
  • AηX: X→[A, X\otimesA] in C

Aε, Aη が実際に自然変換になることは別途証明が必要ですが割愛します。

エバル(ev = ε)とインス(ins = η)、ベータ変換等式とイータ変換等式、それら全てを使うことによって指数随伴系が構成できます。

ニョロニョロ等式

カリー化 Λ(f) を f と書くと、絵と似ていて便利です。上付き'∩'がラムダベントを表します。 \Lambda(f) = f^{\overset{\lambda}{\cap}} とかすると象形文字としての精度は上がりますが、そこまではしません。

ベータ変換等式は次のように書けます。

  • (f\otimesA^);ε = f

前節の補足説明のように、ラムダベントをηノードのホミング前結合で置き換えていいので、

  • ((η;[A^, f])\otimesA^);ε = f

結合とモノイド積に関する交替律〈interchange law〉を使うと:

  • ((η\otimesA^);([A^, f]\otimesA^);ε = f

このなかの f:X\otimesA→Y を特別に f = idX\otimesA:X\otimesA→X\otimesA (Y = X\otimesA)と置いても等式は成立します。実は、この等式が、指数随伴系のニョロニョロ等式になっています。そのことを絵で説明しましょう。

随伴系のニョロニョロ等式(の片一方)は (η*F^);(F^*ε) = F^ であり。指数随伴系では、F = (\otimesA), G = [A, -] でした。よって示すべき等式は、

  • η*(\otimesA)^;(\otimesA)^*ε = (\otimesA)^

です。絵に描けば:

対象Xでの成分を取ると:

  • X.(η*(\otimesA)^;(\otimesA)^*ε) = X.(\otimesA)^

右辺の X.(\otimesA)^ は、idX\otimesA を意味します。

右辺に注目して絵に描いてみます。

横に三段に分けて、各段のテキスト表現は:

  1. ηX;A^
  2. [A^, f]\otimesA^
  3. εX\otimesY = εY

です。これを縦方向に結合すると、

  • ηX;A^ ; [A^, f]\otimesA^ ; εY
    = (η;A^);([A^, f]\otimesA^);ε

ところが、これは先の等式から f になります。f = idX\otimesA だったので、ニョロニョロ等式が成立することが確認できました。

もうひとつのニョロニョロ等式に関しても同様にできます。

おわりに

この記事では、カリー化と反カリー化の対称性を強調しましたが、実際にはどちらか一方で十分です。例えば次の状況があったとします。

  1. Cはモノイド圏であり、二項関手 [-, -]:Cop×CC が備わっている。
  2. Cの対象 X, A, Y ごとに写像 ΛX, AY:C(X\otimesA, [A, X]) が定義されている。
  3. Cの対象 X, A ごとに特別な射 AevX:[A, X]\otimesA→X が特定さている。
  4. Λとevに関して、ベータ変換等式 (Λ(f)\otimesA^);ev = f が成立している。

ベータ変換等式から、Λの可逆性が保証され、Λ-1 := Γ, ins = Λ(idX\otimesA) と定義すれば、反カリー化/インス/イータ変換等式の議論が展開できます。

ベータ変換等式/イータ変換等式があれば、それからニョロニョロ等式は導けるので、指数随伴系が構成可能です。別な言い方をすれば、カリー化/エバル/ベータ変換等式があれば、必然的に指数随伴系(の族)は存在します。

対象Aごとの指数随伴系達がテンデンバラバラではなくて、全体として体系的に連合していることを保証するには、カリー化の自然性を確認します。

以上のセッティングが揃えば、圏C上で型付きラムダ計算を行うことができます。

*1:"eval"だから「エヴァル」がいいという話があるかも知れませんが、長年「エバル」と言ってきたのでかえって違和感あります。そもそも僕は"b"と"v"をカタカナ表記で区別する必要性を感じません。「ベクトル」でいいし、「ベトナム」でいいよ。

*2:「使いましょう」と言いながら、この記事では使っていません。が、便利な言葉だとは思うので記述を残しておきます。