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

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

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

参照用 記事

閉圏、弱いラムダ計算、弱い論理

「モノイド圏、豊饒圏、閉圏と内部ホム」は自分用メモと思って書いたら、トラックバック/コメント欄で色々とやりとりがあって面白かったです。お相手してくださった皆様、ありがとうございます。

でまー、またゴニュゴニョ続けるのですけど、このての話(って、まだ話してないが)は、ランベック(J. Lambek)とかケリー(G. M. Kelly)あたりが大昔にやっていそうで気が引けますが、まー、練習問題ということで。

“そとの人”と“なかの人”

例え話で、閉圏(閉じた対称モノイド圏のこと)のなかに棲む生物を出したのですが、比喩だからピンとこない人もいるでしょう。でも、この比喩に共感できる人は、強烈で具体的なイメージを持てると思います。「そと」とか「なか」が何を意味するか、もう少し説明しましょう。

まず、“そとの人”は、神様のつもりになった我々人間。圏に対して何でもできます(つうか、そういう幻想を抱いている)。集合概念を使って無限個の射を把握したり、目の前の圏を別な圏に(例えば米田埋め込みで)埋め込んで眺めたり、背理法を使ったり、と、やりたい放題。“なかの人”は、非常に制限された行為しかできません。できることは、だいたい次のようなこと。

  1. 個々の対象や個々の射は見える。それらを比較もできる。
  2. 対象の恒等射を見つけることができる。
  3. 2つの射が結合可能かどうか判定し、結合可能なら結合して射を作れる。
  4. 2つの対象/射のモノイド積を作ったり、モノイド単位を見つけることができる。
  5. モノイド積の結合法則や単位法則を知っていて、(自然変換の成分として)使える
  6. 射のカリー化や反カリー化が可能なら、それを作り出せる。

他にたぶん、“なかの神様”がいて、全ての対象/射とか、それらの組み合わせ全てを調べ尽くす能力を持っています。が、“なかの神様”は扱わない。

内部的カリー化と内部的反カリー化の構成

「モノイド圏、豊饒圏、閉圏と内部ホム」にて:

C内に確実に存在する射とか自然変換達をうまく組み合わせて、[A□X, B] → [A, [X, B]] という同型射(可逆射)を具体的に構成できればいいのですが、これはなかなか難しいようです(脚注:難しくないかもしれないけど、僕は全然思いつかなかったです)。

これに対して酒井さんが、具体的な構成を示してくれました。

----------------------- [恒等射]
[A□X,B] → [A□X,B]
----------------------- [反カリー化]
[A□X,B]□(A□X) → B
----------------------- [□の結合性]
([A□X,B]□A)□X → B
----------------------- [カリー化]
[A□X,B]□A → [X,B]
----------------------- [カリー化]
[A□X,B] → [A,[X,B]]

(逆向き)

----------------------- [恒等射]
[A,[X,B]] → [A,[X,B]]
----------------------- [反カリー化]
[A,[X,B]]□A → [X,B]
----------------------- [反カリー化]
([A,[X,B]]□A)□X → B
----------------------- [□の結合性]
[A,[X,B]]□(A□X) → B
----------------------- [カリー化]
[A,[X,B]] → [A□X,B]

横線の上段から下段に移るときの各操作は、“なかの人”でもできることなので、“なかの人”は目的の射を作れます。ただし、そうやって作った内部的カリー化 c: [A□X,B] → [A,[X,B]] と内部的反カリー化 u: [A,[X,B]] → [A□X,B] が互いに逆なことを“なかの人”に納得させる作業は残ります。

弱いラムダ計算なら“なかの人”も使えそう

「モノイド圏、豊饒圏、閉圏と内部ホム」にて:

Cがデカルト閉なら、型付きラムダ計算の結果を翻訳して具体的構成ができるかもしれません(僕はやったことありません)。

多変数(複数の引数)関数を許す(インフォーマルな)ラムダ計算でやってみると、内部的カリー化cと内部的反カリー化uは次のような感じでしょう。

  • c: f |→ λa.λx.f(a, x) (BA×X → (BX)A
  • u: g |→ λ(a, x).g(a)(x) ((BX)A → BA×X

このラムダ式デカルト閉圏を前提にしていて、そのままでは単なる閉圏では使えない、とたけをさんにコメントしたのですが、考えてみるとそうでもないですね。閉圏(デカルト性は仮定しない)の“なかの人”に次の概念を合理的に教えることができればいいわけです。

  1. a, x, f, gなどの変数
  2. (a, x)のようなペア(一般にはタプル)
  3. f(a, x)、g(a) のような関数の後に丸括弧が付いた形
  4. λa., λ(a, x). などのラムダ抽象
  5. 関数と引数に対する適用・評価

デカルト・ペアはありませんが、A□X とか f□g は作れるので、ペアはモノイド積で解釈できそうです。随伴(外部的なカリー化/反カリー化)があるので、ラムダ抽象もできそう。

デカルト性を仮定しない一般的閉圏でも使える弱いラムダ計算があれば、それを“なかの人”に教えることができるし、“なかの人”はそのラムダ計算を使って、c;u = id などを自分で示すことができるでしょう。

弱い論理なら“なかの人”も使えそう

酒井さんの図は、記号を置き換えれば、簡単なシーケント計算の図になります。

----------------------- [トートロジー]
A∧X ⊃B → A∧X ⊃B
----------------------- [左∧導入(右⊃削除)]
(A∧X ⊃B)∧(A∧X) → B
----------------------- [∧の結合性]
((A∧X ⊃B)∧A)∧X → B
----------------------- [右⊃導入(左∧削除)]
(A∧X ⊃B)∧A → X⊃B
----------------------- [右⊃導入(左∧削除)]
A∧X ⊃B → A⊃(X⊃B)

(逆向き)

----------------------- [トートロジー]
A⊃(X⊃B) → A⊃(X⊃B)
----------------------- [左∧導入(右⊃削除)]
(A⊃(X⊃B))∧A → X⊃B
----------------------- [左∧導入(右⊃削除)]
((A⊃(X⊃B))∧A)∧X → B
----------------------- [∧の結合性]
(A⊃(X⊃B))∧(A∧X) → B
----------------------- [右⊃導入(左∧削除)]
A⊃(X⊃B) → A∧X ⊃B

これを見ると、∧(連言)と⊃(含意)だけの論理のようです。∧とI(単位、真)に関するいくつかの法則は使いますが、事実上の推論規則は「左∧導入」と「右⊃導入」だけみたい。他に、射の結合を表すカットは使うでしょうがね。

今ハッキリと書き下せないのですが、閉圏の“なかの操作”に対応する弱い論理と弱いシーケント計算は存在しそうです(誰かが書き下しているでしょう)。

三位一体説と“なかの人”の能力

たぶん、「閉圏」と「弱いラムダ計算」と「弱い論理」は三位一体で、閉圏の“なかの人”の能力は、「弱いラムダ計算ができる」あるいは「弱い論理の証明図が書ける」という形で述べることができるのでしょう。どなたか、もっとハッキリとしたことをご存知でしたら教えてください。

[追記 date="翌日"]どうやら“弱い論理”は、乗法的直観主義線形論理(Multiplicative Intuitionistic Linear Logic; MILL)というものらしい。MILLの論理計算とラムダ計算はめっかった(↓)んですが、なんかピンとこないなぁ、僕は。

三位一体を確認する方針としては; 対称モノイド閉圏の上で解釈できる論理計算(自然演繹、またはシーケント)とラムダ計算を定義する、その論理が閉圏をモデルと考えて“完全”であることを示す、論理と(型付き)ラムダのあいだはカリー/ハワード対応で結び付ける、と、そんな感じでしょうかね。[/追記]