カン拡張とラムダ計算の関係をはじめて意識したのは2013年のことです。以下の記事に書いてあります。
次の絵が2013年記事にあります。
このとき、次のようなことを言ってます。
runは自然変換ですが、ある種の実行エンジンで、ラムダ計算のeval（apply）とよく似た働きをします。
どうも、右カン拡張は、自然変換のラムダ計算における指数型を与える仕掛けのようです。
去年〈2024年〉、カン拡張とラムダ計算の関係について、かなり詳しい記事を書きました。
左右のカン拡張／カン持ち上げ、左右の内部ホム／内部コホムの関係は次の2つの表（上記2024年記事より）にまとめることができます。
カン拡張とラムダ計算の比較対照はしてきたのですが、どうもこれでは物足りなくて、カン拡張とラムダ計算を同じ枠組み内で展開したい気がしてきました。つまり、「カン拡張とラムダ計算は似てる」ではなくて「カン拡張とラムダ計算は同じだ」と言いたいのです。カン拡張のラムダ計算化、あるいはラムダ計算のカン拡張化です。
そのためのキーワードが幾つかあります。
- モノイド圏（対称とは限らない）
- 2-圏化、次元シフト
- 1-双対と2-双対
- テンソル・ホム随伴系
- 仮想二重圏化
オリジナルのラムダ計算はデカルト閉圏を舞台にします。まずは、デカルト圏をモノイド圏〈monoidal category〉（対称性は仮定しない）に一般化し、モノイド圏ベースのラムダ計算を組み立てます。これはそれほど難しい話ではありません。
次に、モノイド圏を2-圏に変換します。この操作は通常脱ループ化〈delooping〉と呼ばれますが、ここではより直接的に次元シフト〈dimension shift〉と呼ぶことにします。次元シフトにより、モノイド圏の対象は1-射になり、モノイド圏の射は2-射になります。モノイド圏を次元シフトにより2-圏化〈2-categorification〉することにより、ラムダ計算とカン拡張を同じ舞台で議論する準備が整います。
上に挙げた2024年記事の表が示唆するように、カン拡張にもラムダ計算にも双対性が備わっています。互いに双対であるナニカを区別するために、「左と右」とか「形容詞無しと余〈コ〉」とか「形容詞無しと反〈オプ〉」などの呼び方を使っているわけです。双対性は、明白にニ種類に分けられます。1-射の向きを逆転する双対と2-射の向きを逆転する双対です。それぞれ、1-双対〈1-dual〉、2-双対〈2-dual〉と呼びましょう。
ラムダ計算もカン拡張も随伴系〈adjunction | adjoint system〉を巡る話です。その随伴系はテンソル・ホム随伴系〈tensor-hom adjunction〉と呼べます。基本となるテンソル・ホム随伴系に対して、1-双対と2-双対を考えると、全部で四種類の随伴系が現れます。1-双対は「左と右」で区別して、2-双対は「形容詞無しと余〈コ〉」で区別して呼ぶなら次のようです。
- 左テンソル・左ホム随伴系
- 右テンソル・右ホム随伴系
- 左コホム・左テンソル随伴系
- 右コホム・右テンソル随伴系
これらの随伴系に対して随伴系の一般論を適用すれば、ラムダ計算とカン拡張に関する様々な概念・結果が出てきます。
さて、最後のステップは、2-圏から仮想二重圏〈virtual double category〉へと舞台を移すことです。最近、モナド、相対モナド、随伴系などの理論を仮想二重圏内で展開することが多くなりました。ラムダ計算とカン拡張も仮想二重圏化〈virtual double categorification〉したいですね。
この記事ではこれ以上の内容は述べませんが、引き続く記事達でカン拡張ラムダ計算化計画をちょっとずつ実行する予定です。この記事はハブ記事（リンク集）として使います。
（ここから下に関連記事へのリンク）
