大きなラムダ式／小さなラムダ式 - 檜山正幸のキマイラ飼育記 (はてなBlog)

以前、セミナーでの説明のために、「大きなラムダ式／小さなラムダ式」という記法を使いました。その後も使ってますが、けっこう具合がいいです。紹介しておきます。

大きなラムダ式は圏の射をそのまま表し、小さなラムダ式は指数対象への射を表します。次の推論図風の図式がカリー化を表します。カリー化は、大きなラムダ式から小さなラムダ式への変換になります。

  <x∈X, y∈Y | M >
 -------------------- Λ
  <x∈X | λy∈Y.M >

(C, □, I) がモノイド圏とします。□がモノイド積ですが、対称性を仮定しません。つまり、X□Y と Y□X を関係付ける法則を期待できません。この圏における指数（ベキ）は、右肩指数 Y^X と左肩指数 ^XY の二種類が必要です。カリー化は次のようです。

   X□Y → Z
 -------------- 右カリー化
   X → Z^Y


   X□Y → Z
 -------------- 左カリー化
   Y → ^XZ

上付き添字はめんどくさいので、[Z←Y] = Z^Y, [X→Z] = ^XZ という書き方も使いましょう。この書き方なら：

   X□Y → Z
 ---------------- 右カリー化
   X → [Z←Y]


   X□Y → Z
 ---------------- 左カリー化
   Y → [X→Z]

右カリー化をΛ^R、左カリー化をΛ^L としましょう。正確に書けば、次のようです。

カリー化をより正確に定義するには、Cから作った多圏（polycategory）を使うべきですが、まー、そこまでしなくていいとしましょう。

集合圏は直積×と単元集合1に関してモノイド圏になります。関数集合を指数対象として閉圏になります -- そう、デカルト閉圏ですね。

デカルト積では、対称 σ_X,Y:X×Y → Y×X があるので、右カリー化と左カリー化を互いに交換することができます。習慣として、次の形のカリー化を使うことが多いので、これを単にカリー化と呼び、記号Λで表します。

   X×Y → Z
 ---------------- Λ (カリー化)
   X → [Y→Z]

右カリー化してから、[Z←Y] と [Y→Z] の同型を繋いだものがΛ操作です。対称圏では、左右の問題を気にすることはありません。要するに習慣とか好みの問題ですから。この話は、集合圏でなくても、対称モノイド閉圏なら同じことです。

[追記]以下に出てくるラムダ式は型付きラムダ式ですが、変数や式の型を記述するために、∈ と : が混じっています。これはどっちか一方に統一したほうがよかった気もしますが、僕自身はさほど気にならないのでそのままにしておきます。[/追記]

集合圏Setで考えることにして、「大きなラムダ式」とは、単に圏の射のことです。f:X→Y in Set が、変数xを含む（かも知れない）式Mによって、f(x) := M と定義されているとき次のように表記します。

余域が前もって分かっていたり、あまり重要でないなら省略してもかまいません。

射の域が直積の形をしているとき、次のように書きます。

以下では2番目の書き方を使います。

f = <x∈X, y∈Y | M : Z > のとき、fをカリー化することができます。

   <x∈X, y∈Y | M : Z >
 ------------------------- Λ
   <x∈X | M' : [X→Z] >

式M'は、「Mが表す射をカリー化した射を表す式」です。これが小さいラムダ式 λy∈Y.M です。小さいラムダ式を使ってカリー化を書くと：

   <x∈X, y∈Y | M : Z >
 ------------------------------ Λ
   <x∈X | λy∈Y.M : [X→Z] >

あるいは：

特に X = 1 のときは、

アスタリスク*は、集合1の上を走る変数ですが、変数とはいっても単元集合上では定数です。つまり、*は1の唯一つの要素と思っても同じです。

変数（あるいは定数）*は、たいして意味が無いので省略すると：

これが、式Mをラムダ束縛抽象して λy∈Y.M を作ることの圏論的意味を与えています。