2025年初頭に「カン拡張ラムダ計算化計画」という記事を書きました。そこで述べた“計画”は、カン拡張に関わる概念や計算を、ストリング図(ワイヤーとノード)を使ったグラフィカル・ラムダ計算の枠組みに取り込もう、というものです。この計画は半分忘れてましたが、最近またちょっと考えてみました。過去にやったことをうまくまとめる方法を思いつきました。また、新しいことも少し分かってきました。
この記事では、グラフィカル・ラムダ計算の全体像をキューブ〈立方体〉の図を使ってまとめます。今回強調したい話題のひとつは、小学校で習った掛け算に関する概念を、モノイド圏/2-圏の文脈で徹底的に復習することです。掛け算は大事、掛け算をシッカリ理解しないと(本題である)指数も定義できないのですよ。
カン拡張をラムダ計算として理解しやすくする“地図”としてキューブの説明は詳しくしますが、カン拡張ラムダ計算化計画の眼目である2-ラムダ計算の詳細までは今回説明していません。それは次回以降となります。
記事タイトルに含まれる文字列「カン・ラムダ::」は、カン拡張ラムダ計算化に関わる記事であることを示します。記事内で使う文字の色については「文字の色の約束(再確認)」を参照してください。$`\newcommand{\cat}[1]{\mathcal{#1}}
\newcommand{\mbf}[1]{\mathbf{#1}}
\newcommand{\mrm}[1]{\mathrm{#1}}
%\newcommand{\msf}[1]{\mathsf{#1}}
\newcommand{\mbb}[1]{\mathbb{#1}}
%\newcommand{\mcal}[1]{\mathcal{#1}}
%\newcommand{\msc}[1]{\mathscr{#1}}
\newcommand{\u}[1]{\underline{#1} }
%\newcommand{\o}[1]{\overline{#1} }
\newcommand{\In}{\text{ in } }
\newcommand{\hyp}{\text{-} }
%\newcommand{\Imp}{\Rightarrow }
%\newcommand{\Iff}{\Leftrightarrow}
\newcommand{\T}[1]{ \text{#1} }
\newcommand{\op}{\mathrm{op} }
\newcommand{\id}{\mathrm{id} }
%\newcommand{\pto}{\nrightarrow} % proarrow to
%\newcommand{\dto}{\looparrowright} % dependent to
%\newcommand{\hto}{\rightsquigarrow} % hetero to
%\newcommand{\parto}{\supset\!\to}
\newcommand{\twoto}{\Rightarrow}
\newcommand{\Over}{\text{ over }}
`$
内容:
- YetAnotherラムダ・キューブ
- そもそも、ラムダ計算とは?
- モノイド圏/2-圏における掛け算
- デカルト閉圏における指数算
- 掛け算と指数算の対応はややこしい
- 次元のズレをどう対処するか
- 中途半端な指数算でも役に立つ
- そしてそれから
ハブ記事:
YetAnotherラムダ・キューブ
8種類の型付きラムダ計算を分類・整理して描くために、バレンドレフト〈Henk Barendregt〉のラムダ・キューブと呼ばれる立方体があります。バレンドレフトの立方体とは意味が違いますが、グラフィカル・ラムダ計算を分類するとやはり8種類になるので、キューブ〈立方体〉を使って描くことにします。それは次のようになります。
$`\quad \xymatrix{
% 1
{}
&{\text{Lcoλ/2}} \ar[rr]
&{}
&{\text{Rcoλ/2}}
\\ %2
{\text{Lprλ/2}} \ar[ur] \ar[rr]
&{}
&{\text{Rprλ/2}} \ar[ur]
&{}
\\ %3
{}
&{\text{Lcoλ/M}} \ar[uu] \ar[rr]
&{}
&{\text{Rcoλ/M}} \ar[uu]
\\ %4
{\text{Lprλ/M}} \ar[uu] \ar[ur] \ar[rr]
&{}
&{\text{Rprλ/M}} \ar[uu] \ar[ur]
&{}
}
`$
キューブ〈立方体〉は3方向の軸を持ち、それぞれの軸は二分法〈dichotomy〉による分類を表します。
- 左から右方向へ「L vs. R」の二分法: L は左、R は右
- 手前から奥方向へ「pr vs. co」の二分法: pr は正〈primary〉、co は余〈complementary〉
- 下から上方向へ「M vs. 2」の二分法: M はモノイド的〈Monoidal〉、2 は2-圏的〈2-categorical〉
3方向の軸(3つの二分法)と8つの頂点を持つこのキューブをもうひとつ別のラムダ・キューブ〈Yet Another Lambda Cube〉と呼ぶことにします。「もうひとつ別」とはもちろん、バレンドレフトのラムダ・キューブが本来のラムダ・キューブだからです。もうひとつ別のラムダ・キューブは、“YetAnotherラムダ・キューブ”とも書く(表記する)ことにします。
YetAnotherラムダ・キューブを理解するには、3方向の軸(3つの二分法)がどんなものかを知る必要があります。「カン拡張ラムダ計算化 方針」から辿れる過去記事達を読めば、YetAnotherラムダ・キューブの意味は十分推測できるとは思いますが、この記事や引き続く記事でよりハッキリした説明を与えるつもりです。
以下では、たくさんの名前を出されてウンザリするかも知れませんが、名前を決めないとそれについて語ることが出来ないので、YetAnotherラムダ・キューブに従って名前を決めます。
キューブは、8個の頂点だけでなくて、12本の辺と6つの面も持ちます。これらの辺と面も、グラフィカル・ラムダ計算の分類を与えます。(8 + 12 + 6 = 26) の分類にバラバラの名前を付けると覚えるのが大変です。系統的なネーミング・ルールを決めましょう。
キューブの頂点は xyλ/z の形のラベルが付いています。ここで:
- x は、 L(左) か R(右)
- y は、 pr(正) か co(余)
- z は、 M(モノイド圏) か 2(2-圏)
xyλ/z を「z における xyラムダ計算〈x y lambda calculus on z〉」と呼びましょう。例えば:
- Rprλ/M なら、モノイド圏における右正ラムダ計算〈right primary lambda calculus on monoidal category〉
- Lcoλ/2 なら、2-圏における左余ラムダ計算〈left complementary lambda calculus on 2-category〉
- Rcoλ/2 なら、2-圏における右余ラムダ計算〈right complementary lambda calculus on 2-category〉
「正〈primary〉」は多くの場合省略します。「余〈complementary〉」は、「相補的な」「相方となる」といった意味ですが、complementary は接頭辞 co として短縮します。また、「モノイド圏における~」「2-圏における~」は「モノイド~」「2-~」でもかまいません。
- Rprλ/M は、モノイド右ラムダ計算〈monoidal right lambda calculus〉
- Lcoλ/2 は、2-左余ラムダ計算〈2-left colambda calculus〉
- Rcoλ/2 は、2-右余ラムダ計算〈2-right colambda calculus〉
我々が通常「ラムダ計算」と呼んでいるものは正ラムダ計算〈primary lambda calculus〉なので、正〈primary〉を省略するのは習慣と整合しています。
念のため、8種類のラムダ計算をすべて列挙すると:
- Lprλ/M は、モノイド左ラムダ計算〈monoidal left lambda calculus〉
- Rprλ/M は、モノイド右ラムダ計算〈monoidal right lambda calculus〉
- Lcoλ/M は、モノイド左余ラムダ計算〈monoidal left colambda calculus〉
- Rcoλ/M は、モノイド右余ラムダ計算〈monoidal right colambda calculus〉
- Lprλ/2 は、2-左ラムダ計算〈2-left lambda calculus〉
- Rprλ/2 は、2-右ラムダ計算〈2-right lambda calculus〉
- Lcoλ/2 は、2-左余ラムダ計算〈2-left colambda calculus〉
- Rcoλ/2 は、2-右余ラムダ計算〈2-right colambda calculus〉
アスタリスク('*')はワイルドカード(値が何でもいいことを表す)として、次の呼び名も使います。
- **λ/M(キューブの下の面)は、モノイド・ラムダ計算〈monoidal lambda calculus〉
- **λ/2(キューブの上の面)は、2-ラムダ計算〈2-lambda calculus〉
- L*λ/*(キューブの左の面) は、左ラムダ計算〈left lambda calculus〉
- R*λ/*(キューブの右の面)は、右ラムダ計算〈left lambda calculus〉
- *prλ/*(キューブの前の面)は、正ラムダ計算〈primary lambda calculus〉
- *coλ/*(キューブの奥の面)は、余ラムダ計算〈colambda calculus〉
常識的にラムダ計算と呼ばれているものは、YetAnotherラムダ・キューブの下段前面側の辺、つまりモノイド正ラムダ計算(左と右)です。カン拡張に関わるラムダ計算は、YetAnotherラムダ・キューブの上段左面側の辺、つまり2-左ラムダ計算(正と余)です*1。
過去記事「カリー vs. カン、双対 vs. 随伴」で出したカリー計算〈Curry calculus〉はモノイドラムダ計算の別名(主に正ラムダ計算だが)、カン計算〈Kan calculus〉は2-ラムダ計算の別名です。
歴史的経緯(偶発的事情)から、ラムダ計算の左右とカン拡張の左右は、まったく異なった分類になっています。これは、カン拡張をラムダ計算として理解することを阻害している原因になっているかも知れません。以下の過去記事達でこのこと(困った事態)について説明しています。
上記の過去記事達に載せている図を(図だけを)再掲すると:

そもそも、ラムダ計算とは?
常識的なラムダ計算は、YetAnotherラムダ・キューブのなかの一本の辺(両端に2頂点)に過ぎません。ということは、ラムダ計算を一般化してYetAnotherラムダ・キューブを構成していることになります。一般化しても、それは「ラムダ計算」と呼べると僕は思っています。
それじゃそもそも、ラムダ計算とは何でしょうか? 現時点で僕は、次のように考えています*2。
- ラムダ計算とは、掛け算の随伴である指数算を使った計算術
指数算〈exponentiation〉が、ラムダ計算の中心的テーマです。指数算は、掛け算〈multiplication〉に基づいて定義されます。よって、最初に掛け算がないとラムダ計算を構成することは出来ません。
ここで言う掛け算〈multiplicatio〉とは:
- モノイド圏 $`\cat{C}`$ の場合は、二項関手〈双関手 | bifunctor〉とみなしたモノイド積〈monoidal product〉 $`(\otimes): \cat{C}\times \cat{C} \to \cat{C} \In \mbf{CAT}`$
- 2-圏(弱2-圏含む)$`\cat{K}`$ の場合は、二項関手とみなした横結合〈horizontal composition〉
$`(*) : \cat{K}(A, B)\times \cat{K}(B, C) \to \cat{K}(A, C) \In \mbf{CAT}\: \text{ for }A, B, C \in |\cat{K}|`$
この記事で(というか、このブログ全体で)「モノイド圏」「2-圏」は厳密〈strict〉なものだとは限りません。厳密なものに制限するときは明示的に「厳密」を前置します(「厳密モノイド圏」「厳密2-圏」と)。
モノイド圏のなかでも特にデカルト・モノイド圏のデカルト積〈Cartesian product〉には記号 $`\times`$ を使います。つまり、掛け算記号は3種類使うことになります。
- デカルト積は $`\times`$
- 一般的なモノイド積は $`\otimes`$
- 2-圏の横結合は $`*`$
横結合の記号 $`*`$ は図式順演算子記号〈diagrammatic-order operation symbol〉(左から右に読む)であることに注意してください。
$`\times, \otimes, *`$ の3種類の掛け算記号を使うのは、習慣的・便宜的な事情で、ひとつの記号(例えば $`*`$)に統合できます。後述しますが、モノイド圏は単一対象の2-圏だとみなせます(みなす操作を delooping と呼びます)。よって、モノイド積 $`\otimes`$ は横結合 $`*`$ に統合できます。そして、$`\times`$ は $`\otimes`$ の特別な場合でした。
モノイド圏/2-圏における掛け算
カン拡張をラムダ計算とみなすことを阻害する要因として、前節で「『左・右』の使い方が食い違っている」ことを挙げました。これは偶発的な悲劇です。
他にも、通常のラムダ計算とカン拡張の類似性が見えにくい原因があります。YetAnotherラムダ・キューブでみると、通常のラムダ計算が下段前面側の辺、カン拡張が上段左面側の辺でした。3次元空間内の2本の直線としての位置関係はねじれの位置にあります。交わるでもなく、平行でもなく、縁遠い関係性なのです。これは、アナロジーが取りにくいってことです。
また別な阻害要因として、掛け算と指数算に関する用語・記法が整理されてないこともあるでしょう。用語・記法がグチャグチャなので、説明が大変だし、理解もしにくいでしょう。この記事で、掛け算について整理することにします。
以下に出てくる、大きい集合・圏からなる $`\mbf{SET}, \mbf{CAT}`$ などについては、「圏論的コアージョン // 世界のグリッド構造に基づくコアージョン」を参照してください。n-圏 $`\cat{K}`$ のk-射達の集合は $`|\cat{K}|_k`$ と書くことにします(「集合論、型理論、圏論の微妙な違い // 圏論からの準備」参照)。単に $`|\cat{K}|`$ と書いたら、それは $`|\cat{K}|_0`$ のことです。
前節で述べたとおり、掛け算は二項演算です。圏に対して定義される演算ですから二項関手〈双関手〉ですね。モノイド圏 $`\cat{C}`$ の場合、対象パート〈object part〉と射パート〈morphism part〉に分けると次のようになります。
$`\quad (\otimes_\text{obj}) : |\cat{C}|_0\times |\cat{C}|_0 \to |\cat{C}| \In \mbf{SET}`$
$`\quad (\otimes_\text{mor}) : |\cat{C}|_1 \times |\cat{C}|_1 \to |\cat{C}|_1 \In \mbf{SET}`$
2-圏 $`\cat{K}`$ の場合、特定の対象 $`A, B, C`$ に注目し、1-射パート〈1-morphism part〉と2-射パート〈2-morphism part〉に分ければ:
$`\quad (*_\text{1-mor}) : |\cat{K}(A, B)|_0 \times |\cat{K}(B, C)|_0 \to |\cat{K}(A, C)|_0 \In \mbf{SET}`$
$`\quad (*_\text{2-mor}) : |\cat{K}(A, B)|_1 \times |\cat{K}(B, C)|_1 \to |\cat{K}(A, C)|_1 \In \mbf{SET}`$
$`\cat{K}`$ の1-射/2-射とはいいながら、ホム圏 $`\cat{K}(\hyp, \hyp)`$ で考えれば0-射〈対象〉/1-射です。このように次元がズレてややこしくなる現象は至る所で出現します。この問題は後の節でまた取り上げます。
掛け算 $`\otimes, *`$ は2つの引数〈arguments〉を取ります。第一引数を左因数〈left factor | 左因子〉、第二引数を右因数〈right factor | 右因子〉と呼びます。「因数/右因数/左因数」は、「引数/第一引数/第二引数」に対する掛け算固有の呼び名です。
掛け算は二項演算(二項関手)ですが、左因数または右因数を固定すると単項演算(単項関手)になります。左因数を固定した単項掛け算を左掛け算〈left multiplication〉、右因数を固定した単項掛け算を右掛け算〈rightt multiplication〉と呼びます。単項掛け算において、固定した因数を乗数〈multiplier〉、引数としての因数を被乗数〈multiplicand〉と呼びます。乗数はオペレーター、被乗数がオペランドです。
小学校の掛け算では、左右の因数の区別や乗数〈かける数〉と被乗数〈かけられる数〉の区別は、物議を醸す話題ですが、圏論においては、左因数/右因数、乗数/被乗数の区別は絶対に必要です。モノイド積 $`\otimes`$ は可換(むしろ対称)であるとは限らないし、横結合 $`*`$ が可換(対称)であることはほとんど期待できません。
左因数を乗数 $`T`$ に固定した左掛け算は次のように書きます。
$`\T{For }T \in |\cat{C}|\\
\quad (T\otimes \hyp) : \cat{C} \to \cat{C} \In \mbf{CAT}
`$
単項関手 $`(T\otimes \hyp)`$ の射パートは $`(\id_T \otimes \hyp)`$ ですが、$`T`$ と $`\id_T`$ は区別しないで(オーバーロードして) $`(T\otimes\hyp)`$ と書きます。
右因数を乗数 $`T`$ に固定した右掛け算なら:
$`\T{For }T \in |\cat{C}|\\
\quad (\hyp \otimes T) : \cat{C} \to \cat{C} \In \mbf{CAT}
`$
2-圏 $`\cat{K}`$ における左掛け算と右掛け算は:
$`\T{For }K: A \to B \In \cat{K}\\
\quad (K * \hyp) : \cat{K}(B, C) \to \cat{K}(A, C) \In \mbf{CAT}
`$
$`\T{For }K: B \to C \In \cat{K}\\
\quad (\hyp * K) : \cat{K}(A, B) \to \cat{K}(A, C) \In \mbf{CAT}
`$
横結合 $`*`$ は図式順だったので、左掛け算 $`(K *\hyp)`$ は前結合〈pre-composition〉、右掛け算 $`(\hyp* K)`$ は後結合〈post-composition〉です。反図式順記法(右から左に読む記法)を使うなら、左右と前後の関係は逆になります。「左」「右」という呼び名は、書き方の習慣に依存してしまいます。
掛け算に関して重要な概念をもう一度列挙しておきます。
- (二項の)掛け算〈(binary) multiplication〉
- 左因数〈left factor〉
- 右因数〈right factor〉
- 左掛け算〈left multiplication〉
- 右掛け算〈right multiplication〉
- 乗数〈multiplier〉
- 被乗数〈multiplicand〉
なお、「積〈product〉」は、掛け算の別名でもあり、掛け算の演算結果も意味する曖昧多義語です。
デカルト閉圏における指数算
掛け算の随伴として定義される演算が指数算〈exponentiation〉です。まず、お馴染みで簡単なケースであるデカルト閉圏における指数算から説明します。モノイド正ラムダ計算(YetAnotherラムダ・キューブのラベルは *prλ/M)の話になります。
$`\cat{C} = (\cat{C}, \times, \mbf{1})`$ はデカルト閉圏とします。$`\cat{C}`$ は小さいとは限らず、厳密とも限りませんが、局所小圏〈locally small category〉であるとします。典型的な具体例は集合圏 $`\mbf{Set} = (\mbf{Set}, \times, \mbf{1})`$ です。
デカルト閉圏 $`\cat{C}`$ では、特定の対象 $`T`$ に対して、次の同型が成立します。
$`\T{For }A, B \in |\cat{C}|\\
\quad \cat{C}(A \times T, B) \cong \cat{C}(A, B^T) \; \In \mbf{Set}
`$
実際には、任意の対象 $`A, B \in |\cat{C}|`$ だけでなくて、$`A, B`$ の位置に $`\cat{C}`$ の射を代入することもできます。そうやって、自然変換の自然性四角形が得られます。対象または射を表す変数を $`x, y`$ として、記号 $`\in_*`$ は「対象または射として所属する」という意味だとして、次のように書けます($`\cong`$ の解釈に工夫が必要ですが*3)。
$`\T{For }x, y \in_* \cat{C}\\
\quad \cat{C}(x \times T, y) \cong \cat{C}(x, y^T) \; \In \mbf{Set}
`$
この同型を、非形式的〈インフォーマル〉なラムダ記法を使って書けば:
$`\quad \lambda\,(x, y) \in_* \cat{C}^\op \times \cat{C}.\, \cat{C}(x \times T, y) \cong \lambda\,(x, y) \in_* \cat{C}^\op \times \cat{C}.\,\cat{C}(x, y^T) \\ \quad \In [\cat{C}^\op \times \cat{C}, \mbf{Set}]
`$
ここでの $`\cong`$ は、関手圏 $`[\cat{C}^\op \times \cat{C}, \mbf{Set}]`$ における同型、つまり、反変・共変の二項関手の自然同型です。
圏論では、無名のラムダ変数としてハイフンがよく使われます*4。
$`\quad \cat{C}(\hyp_1 \times T, \hyp_2) := \lambda\,(x, y) \in_* \cat{C}^\op \times \cat{C}.\, \cat{C}(x \times T, y)`$
$`\quad \cat{C}(\hyp_1, {\hyp_2}^T) := \lambda\,(x, y) \in_* \cat{C}^\op \times \cat{C}.\, \cat{C}(x, y^T)`$
ハイフンを使った書き方なら、ホムセット同型は次のように書けます。
$`\quad \cat{C}(\hyp_1 \times T, \hyp_2) \cong \cat{C}(\hyp_1, {\hyp_2}^T) \; \In [\cat{C}^\op\times \cat{C}, \mbf{Set}]`$
このホムセット同型(より正確には、二項関手の自然同型)は、2つの変数 $`\hyp_1`$ と $`\hyp_2`$ に対して自然〈natural〉であり、次のことを意味します。
- 乗数 $`T`$ の右掛け算が定義する関手 $`(\hyp \times T)`$ の右随伴関手が $`(\hyp^T)`$ である。
単項の掛け算 $`(\hyp \times T)`$ の右随伴関手 $`(\hyp^T)`$ は単項の指数算〈unary exponentiation〉と呼びます。掛け算の乗数 $`T`$ は、指数算の指数部〈exponent〉となります。随伴関係は次のように図示できます。
$`\quad \xymatrix@C+2pc{
{\cat{C}} \ar@/^1pc/[r]^{(\hyp\times T)}
\ar@{}[r]|{\bot}
&{\cat{C}} \ar@/^1pc/[l]^{(\hyp^T)}
}\\
\quad \In \mbf{CAT}
`$
デカルト閉圏の掛け算 $`\times`$ は対称〈symmetric〉なので、右掛け算と左掛け算を別々に考える必要はないのですが、ここでは非対称なモノイド圏/2-圏への拡張を視野に入れて、右掛け算と左掛け算を区別して別々に考えることにします。そうすると、乗数 $`T`$ の右掛け算の右随伴関手は、指数部 $`T`$ の(単項の)右指数算〈(unary) right exponentiation〉となります。「右指数算」の「右」は、右掛け算に対応するからであって、右随伴の右とは関係ありません。
乗数 $`T`$ の左掛け算 $`(T \times\hyp)`$ の右随伴関手は、指数部 $`T`$ の(単項の)左指数算〈(unary) left exponentiation〉です。左指数算は右指数算とは区別して、指数部を左上に書きます $`(^T\!\hyp)`$ 。随伴関係を与えるホムセット同型(二項関手の自然同型)は次の形になります。
$`\quad \cat{C}(T\times \hyp_1, \hyp_2) \cong \cat{C}(\hyp_1, {^T\!\hyp_2}) \; \In [\cat{C}^\op \times \cat{C}, \mbf{Set}]`$
デカルト閉圏では、右指数算も左指数算も二項演算〈二項関手〉に仕立てることができます。二項演算である指数算を二項指数算〈binary exponentiation〉と呼びます。二項掛け算が $`\cat{C}\times \cat{C} \to \cat{C}`$ であったのとは違って、二項指数算は $`\cat{C}^\op \times \cat{C} \to \cat{C}`$ という二項関手になります。
掛け算と指数算の対応はややこしい
掛け算と指数算にはアナロジーがあります。また、掛け算と指数算は、随伴を通じて互いに対応します。アナロジーによる対応と随伴による対応は別物です。が、ゴッチャになって混乱することがあります。以下に説明しましょう。
圏論ではなくて、実数を引数にする演算としての指数算を考えてみましょう*5。
$`\quad x, y \mapsto x^y`$
これは、$`\mathbf{R}\times \mathbf{R} \to \mathbf{R}`$ という二変数関数〈二引数関数〉です。第一引数が指数の底〈base〉で、第二引数は指数の指数部〈exponent〉です。「第一引数〈左引数〉 ←→ 底、第二引数〈右引数〉 ←→ 指数部」という結び付きが標準として決まっているわけではありませんが、ここではこの対応で考えます。
掛け算も指数算も $`\mbf{R}\times\mbf{R} \to \mbf{R}`$ だという共通点からアナロジーを追うと、次の対応になります。
- (二項の)掛け算 ←→ (二項の)指数算〈(binary) exponentiation〉
- 左因数 ←→ (二項指数算の)第一引数〈first argument〉 = 底
- 右因数 ←→ (二項指数算の)第二引数〈second argument〉 = 指数部
- 左掛け算 ←→ 底固定指数算〈base-fixed exponentiation〉 = 指数関数
- 右掛け算 ←→ 指数部固定指数算〈exponet-fixed exponentiation〉 = ベキ関数
- 積 ←→ ベキ〈power〉
もし、「左引数 ←→ 指数部、右引数 ←→ 底」と約束したなら、一部の対応は以下のように変わってきます。
- 左掛け算 ←→ 指数部固定指数算〈exponet-fixed exponentiation〉 = ベキ関数
- 右掛け算 ←→ 底固定指数算〈base-fixed exponentiation〉 = 指数関数
前節の左指数算と右指数算は、このアナロジーに基づく命名ではありません。つまり、底固定指数算(指数関数相当)と指数部固定指数算(ベキ関数相当)の区別を「左・右」で表しているのではないのです。
そうではなくて、左掛け算(左因数固定掛け算)の右随伴関手を左指数算、右掛け算(右因数固定掛け算)の右随伴関手を右指数算と呼んでます。左指数算も右指数算も、どちらも指数部固定指数算(ベキ関数相当)です。
二項関手〈双関手〉としての指数算〈二項指数算〉の底固定バージョンを“指数関手”、指数部固定バージョンを“ベキ関手”と呼べば辻褄があってますが、実際には“指数関手”も“ベキ関手”も使われていません*6。二項指数算の演算結果を“ベキ〈冪 | 巾〉”と呼ぶこともありません。“ベキ”の代わりに指数対象〈exponential object〉はよく使われる言葉です。
実数の場合と、モノイド圏/2-圏の場合の用語を比較すると以下のようです。
| 実数の場合 | モノイド圏/2-圏の場合 |
|---|---|
| (二項)指数算〈(binary) exponentiation〉 | 二項指数算 |
| 底〈base〉 | 底 |
| 指数部〈exponent〉 | 指数部 |
| 指数関数〈exponential function〉 | (対応語なし) |
| ベキ関数〈power function〉 | 単項の指数算(指数部固定) |
| (左右の区別はなし) | 左指数算 |
| (左右の区別はなし) | 右指数算 |
この記事では、「指数算〈exponentiation〉」「指数部〈exponent〉」という言葉を使い、単に「指数」を避けましたが、その理由は「指数」がひどい曖昧多義語だからです。「指数」と「ベキ」の曖昧性は次の用語・用法図(用語の曖昧性を示す図、「パンダ用法と用語・用法図」参照)で示せます。
$`\T{「指数」「ベキ」の曖昧性}\\
\quad \xymatrix{
{}
&{\T{二項指数算}}
\\
{\T{【曖昧】指数}} \ar@{|->}[ur] \ar@{|->}[r] \ar@{|->}[dr] \ar@{|->}[ddr]
&{\T{指数部}}
\\
{\T{【曖昧】ベキ}} \ar@{|->}[uur] \ar@{|->}[ur] \ar@{|->}[dr]
&{\T{指数関数}}
\\
{}
&{\T{ベキ}(二項指数算の結果)}
\\
}
`$
要するに、「指数」という語は「二項指数算」「指数部」「指数関数」「演算の結果」のどれを指すかが文脈依存で曖昧なんです。
圏論では、二項指数算または単項指数算(とその結果)を内部ホム〈internal hom〉と呼ぶことが多いですが、ここでは「内部ホム」より「指数算」を使います。指数算の結果は指数対象〈exponential object〉と呼びます(「ホム対象〈hom object〉」は使いません)。ただし、指数算の結果が対象ではなくて1-射のこともあります。そのときは指数1-射〈exponential 1-morphism〉と呼びます。
用語法がかなり錯綜してますが、内容的には“掛け算と指数算の話”なので決して難しくはありません。落ち着いて整理してみてください。
次元のズレをどう対処するか
YetAnotherラムダ・キューブには、下段(部屋で言えば床)と上段(天井)があります。下段がモノイド・ラムダ計算、上段が2-ラムダ計算でした。実は、上段は下段を吸収できて、立方体を四角形に潰すことができます。8頂点の立方体より4頂点の四角形のほうが簡単です。しかし、モノイド圏のこと(下段)と2-圏のこと(上段)は歴史的・習慣的に区別して扱うので、ここでは区別します。
モノイド圏と2-圏を区別すると、次元のズレに悩まされます。このズレを幾分かは解消するために、モノイド圏 $`\cat{C}`$ に(-1)次元の射 $`\bot`$ を導入します。$`\cat{C}`$ の各次元の射の集合は次のようにします。
- $`|\cat{C}|_1 = \mathrm{Mor}(\cat{C})`$
- $`|\cat{C}|_0 = |\cat{C}| = \mathrm{Obj}(\cat{C})`$
- $`|\cat{C}|_{-1} = \{\bot\}`$
過去記事では、(-1)次元の射を $`*`$ や $`\star`$ で表すことが多かったですが、$`*`$ や $`\star`$ は演算子記号に使う可能性があるので $`\bot`$ (ボトム)にします。
$`A\in |\cat{C}|`$ であることを $`A \In \cat{C}`$ とも書きますが、$`\bot`$ も添えて $`A \Over \bot \In \cat{C}`$ とも書くことにします。すべての対象は、地下に居る $`\bot`$ の“上にある”とみなします。
$`f:A \to B \Over \bot \In \cat{C}`$ は次のように分解して解釈します。
- $`A \Over \bot \In \cat{C}`$
- $`B \Over \bot \In \cat{C}`$
- $`f: A \to B \In \cat{C}`$
モノイド圏 $`\cat{C} = (\cat{C}, \otimes, \mathrm{I})`$ の次元を1つ上げた2-圏 $`\cat{C}_\uparrow`$ を次のように定義します。これは、モノイド圏 $`\cat{C}`$ から1つ上の次元へずらした2-圏 $`\cat{C}_\uparrow`$ を作ることです。
- $`|\cat{C}_\uparrow|_0 := |\cat{C}|_{-1} = \{\bot\}`$
- $`|\cat{C}_\uparrow|_1 := |\cat{C}|_0 = \mathrm{Obj}(\cat{C})`$
- $`|\cat{C}_\uparrow|_2 := |\cat{C}|_1 = \mathrm{Mor}(\cat{C})`$
- $`\T{For }A \in |\cat{C}_\uparrow|_1\, , \: \mrm{dom}(A) := \bot`$
- $`\T{For }A \in |\cat{C}_\uparrow|_1\, , \: \mrm{cod}(A) := \bot`$
- $`\T{For }\bot \in |\cat{C}_\uparrow|_0\, , \: \mrm{id}_\bot := \mathrm{I}`$
$`\cat{C}_\uparrow`$ の1-射の横結合はモノイド積 $`\otimes`$ により定義します。$`\cat{C}_\uparrow`$ の2-射の横結合も $`\otimes`$ により定義します。$`\cat{C}_\uparrow`$ の2-射の縦結合は $`\cat{C}`$ の結合 $`;`$($`;`$ は図式順の中置演算子記号)により定義します。1-射の横結合が厳密になるとは限りませんが、$`\cat{C}_\uparrow`$ は2-圏(弱2-圏も含む)になります。
$`\cat{C}_\uparrow`$ と $`\cat{C}`$ のあいだには次の関係があります。
$`\quad \bot \In \cat{C}_\uparrow \iff \bot \in |\cat{C}|_{-1}`$
$`\quad A: \bot \to \bot \In \cat{C}_\uparrow \iff A \Over \bot \In \cat{C}`$
$`\quad f:: A \twoto B : \bot \to \bot \In \cat{C}_\uparrow \iff f: A \to B \Over \bot \In \cat{C}`$
モノイド圏 $`\cat{C}`$ の話をしているときも、$`\bot`$ の存在と 2-圏 $`\cat{C}_\uparrow`$ を意識するようにすると、次元のズレによる違和感や混乱を軽減出来ると思います。
中途半端な指数算でも役に立つ
デカルト閉圏、より一般にモノイド閉圏 $`\cat{C} = (\cat{C}, \otimes, \mathrm{I}, [\hyp, \hyp])`$ の場合は、二項掛け算(モノイド積)と二項指数算(内部ホム)が最初から備わっています。
$`\quad (\hyp\otimes\hyp) :\cat{C} \times \cat{C} \to \cat{C} \In \mbf{CAT}`$
$`\quad ([\hyp, \hyp]) :\cat{C}^\op \times \cat{C} \to \cat{C} \In \mbf{CAT}`$
しかし、モノイド閉とは限らないモノイド圏では、特定の乗数 $`T`$ による右掛け算に対して(単項の)右指数算が存在するだけかも知れません。
$`\quad (\hyp\otimes T) :\cat{C} \to \cat{C} \In \mbf{CAT}`$
$`\quad (\hyp^T) :\cat{C} \to \cat{C} \In \mbf{CAT}`$
左掛け算 $`(T\otimes \hyp)`$ でも事情は同じです。
さらには、単項の指数算さえうまく定義できないこともあります。乗数 $`T`$ と特定の対象 $`B`$ に対して指数対象 $`B^T`$(あるいは $`{^T\! B}`$)が存在するだけのときもあります。
そのような、二項演算(二項関手)ではない指数算、単項演算(単項関手)でさえない指数対象が役に立つのか? 十分役に立ちます。2-圏のセッティングにおけるカン拡張(正・余の2-左ラムダ計算)では、単なる指数1-射(それを $`\mathrm{Ran}_K F`$ や $`\mathrm{Lan}_K F`$ と書く)しか定義できない/しない状況は普通です。
そしてそれから
カン拡張ラムダ計算化計画を遂行するには、以下のラムダ計算の基本概念を、YetAnotherラムダ・キューブの各頂点において定式化します。
- 随伴のホムセット同型(カリー同型)
- カリー化、反カリー化
- 指数算、指数対象/指数1-射
- 評価器〈evaluation | evaluator〉
- ベータ変換、ベータ法則
よく知られたラムダ計算の舞台は対称モノイド閉圏(特にデカルト閉圏)です。対称モノイド閉圏では、対称性により左掛け算と右掛け算を区別する必要がなく、二項指数算(通常は「内部ホム」と呼ぶ)が最初から備わっています。ラムダ計算を一般化するに従って、対称性や大域的な二項指数算は使えなくなります。
実際、カン拡張/カン持ち上げのラムダ計算(2-ラムダ計算)では、左掛け算と右掛け算は別物であり、二項指数算は前提されません。掛け算の随伴として指数算を構成しますが、このとき使う随伴のメカニズムは、単なる随伴系だけでなく、相対余随伴系〈relative coadjunction〉も使います。
対称性も二項指数算もない状況になっても、上に上げたラムダ計算の基本概念はすべて通用します。ちゃんとラムダ計算なのです。
「カン拡張ラムダ計算化 方針」から辿れる過去記事達において、“一般化されたラムダ計算=YetAnotherラムダ・キューブの内容”はだいたい書いてはいるのですが、引き続く記事では、2-ラムダ計算もちゃんとラムダ計算であることにフォーカスして説明したいと思います。
冒頭で「新しいことも少し分かってきました」と言ったのは、特別な状況では、指数算と掛け算のあいだに分合法則〈dissociative law〉(「色付き絵算と分合律」参照)が成立することが分かったことです。分合法則の図示には、クラスピング〈clasping〉(「モノイド閉圏、オダンゴ、留め金、池袋 // 指数と留め金」参照)と再クラスピング〈reclasping〉が効果的です。古い話題が新しい文脈で登場するとちょっと嬉しくなります。このことを書く機会もあるでしょう。
*1:上段右面側の辺はカン持ち上げ〈Kan lift〉に関わるラムダ計算です。
*2:ここでの「ラムダ計算」は、圏論的に定式化された型付きラムダ計算の延長線上にある計算体系のことであり、形無しラムダ計算の系譜は考えていません。
*3:$`x, y`$ が対象のときは $`\mbf{Set}`$ の同型、$`x, y`$ が射のときは自然性四角形、という解釈になります。
*4:$`\hyp_1`$ と $`\hyp_2`$ を区別しましたが、どちらも単に $`\hyp`$ と書くことが多いです。
*5:実数だと $`0^0`$ の定義が問題になりますが、今の話からはどうでもいいので気にしないことにします。
*6:まったく使われてないとはいい切れませんが、使用例があったとしても少数です。