型付きラムダ計算のモデルをデカルト閉圏で作れるのだけど、ちょっとした注意と工夫が必要です。
Cがデカルト閉圏だとして、ラムダ項Mに対して、Mの表示(denotation)をC内に直接作るもんだと思っている人がいるかも知れませんが、それはあんまりウマくないです。閉じたラムダ項に対して直接Cの射を対応付けることもできるし、そういうセマンティクスの流儀もあるでしょうが、お奨めしません。
デカルト閉圏Cの射に対応づける構文的なブツとして「大きなラムダ式」という概念と記法を導入したことがあります。大きなラムダ式は、型理論の型判断(typing judgement)と同じものだし、論理のシーケントとも同じです。大雑把に言えば「大きなラムダ式 = 型判断 = シーケント」。このことは次のエントリーに書いてあります。
小さなラムダ式(単なるラムダ項)ではなくて大きなラムダ式(=型判断=シーケント)を射とみなすべきなんですが、大きなラムダ式にどうやって射を対応付けるかをもう少し詳しく書いておくことにします。
内容:
大きなラムダ式・再論
常識的な型付きラムダ計算の構文を考えて、その構文による式(ラムダ項)をM、Nなどとします。このラムダ計算で使う変数の集合をVarとします。また、式Mに出現する自由変数の集合をFreeVar(M)としましょう。当然に、FreeVar(M)⊆Var です。
型を表す構文形式である型項(type term)を導入せずに、モデル側の存在物を構文側に取り込むという横着な方法を使うことにします。どういうことかと言うと、デカルト閉圏Cを決めて、Cの対象そのものを型項の代わりに使います。
変数集合Varの適当な有限部分集合 {x1, ..., xn} に対して、γ:{x1, ..., xn}→|C| という写像を考えて、このγを変数への型割り当て(type assignment)と呼びます。型割り当てγを、次の形に書いた構文的ブツは型コンテキストです。
- x1:γ(x1), ..., xn:γ(xn)
型割り当てと型コンテキストはほとんど同じものですが、完全に同一視はできません。なぜかと言うと、型割り当てでは、変数の順序を考慮しません(できません)が、型コンテキストはカンマで区切ったリストなので、変数の出現順があります。例えば、次の2つの型コンテキストは別物です。
- x:A, y;B
- y;B, x:A
型割り当てとしては、どちらも γ:{x, y}→|C|, γ(x) = A,γ(y) = B です。「型コンテキスト=型割り当て + 変数の並び順」、同じことですが「型割り当て=型コンテキスト - 変数の並び順」です。空な型割り当て/型コンテキストも許すことに注意してください。
Γを型コンテキスト、Mをラムダ項として、<Γ | M> の形を大きなラムダ式と呼びます。ただし、次の条件を要求します。
- FreeVar(M)⊆(Γに出現する変数の集合)
型付きラムダ計算を仮定しているので、型付け規則(typing rules)があり、Mの型を計算できるはずです。必要があれば、Mの型(それをCとして)も大きなラムダ式に添えて <Γ | M:C> とします。大きなラムダ式 <Γ | M:C> は、型判断 Γ |- M:C や、シーケント Γ ⇒ M:C の形に書いても同じです。書き方の相違しかありません。
大きなラムダ式 <x:A, y:B | M:C> は、通常のラムダ式 λx:A,y:B.M と同じじゃないかと思われるかも知れませんが違います。大きなラムダ式と小さなラムダ式(通常のラムダ項)を混同するのは、型判断と項の混同、シーケントと論理式の混同と同じ過ちです。
このような混同、あるいは意図的に同一視しようとする背景は次のものです。
- 空な型コンテキストを持つ <| M:C> とラムダ項Mは、1:1に対応する。
- <Γ| M:C> を可能な限りカリー化すると、空な型コンテキストを持つ <| N:D> になる。
大きなラムダ式のセマンティクス
型コンテキストΓの一般的な形は、x1, ..., xn∈Var、A1, ..., An∈|C| に対して x1:A1, ..., xn:An となりますが、めんどくさいので、x:A, y:B あたりの事例を使って書くことにします。
<x:A | M:B> のような大きなラムダ式に対して、デカルト閉圏Cのなかで対応する射を Morph(<x:A | M:B>) として、さらに Morph(<x:A | M:B>) = [x:A | M:B] と略記してしまいましょう。ブラケットで囲まれたほうがC内のセマンティクス(表示; denotation)になります。
大きなラムダ式に対応付けられた射のdom/codの例を挙げると:
- dom([x:A | M:B]) = A
- cod([x:A | M:B]) = B
- dom([x:A, y:B | M:C]) = A×B
- cod([x:A, y:B | M:C]) = C
- dom([y:B, x:A | M:C]) = B×A
- cod([y:B, x:A | M:C]) = C
- dom([| M:D]) = 1(1はCの特定された終対象)
- cod([| M:D]) = D
これで、大きなラムダ式に対応する射の域(dom)と余域(cod)は見当がつくでしょう。
射そのものは、ラムダ式の構文的な構成にしたがって(帰納的に)決めていくことになります。単なる変数には恒等か射影を対応させます。例えば、
- [x:A | x:A] = idA
- [x:A, y:B | y:B] = π2A,B (直積の第二射影)
2つのラムダ項の並置は適用(apply)を表すので、そのセマンティクスは次のようにします。右指数の記号は「圏の指数のための中置演算子記号」で導入した B-^A を使います。
- [z:C | (M N):B] = ΔC;([z:C | M:(B-^A) ]×[z:C | N:A ]);applyA,B
ここに出てきた記号を説明しておくと:
- ΔCはCの対角射 C→C×C です。集合圏なら ΔC(z) = (z, z)
- 直積の掛け算記号×は射に対しても使ってよくて、直積によるモノイド積です。集合圏なら (f×g)(x, y) = (f(x), g(y))。
- applyA,Bは、Cのなかの適用射(評価射)。applyA,B : (B-^A)×A → B という射です。集合圏なら、applyA,B(ψ, a) = ψ(a)、ψ∈BA。
ラムダ抽象のセマンティクスについては次の節で述べます。
ラムダ抽象
大きなラムダ式 <x:A, y:B | M:C> に対して構文的なオペレーターとして、ラムダ抽象Λを導入します。次のように定義されます。
- Λ(<x:A, y:B | M:C>) = <x:A | λy:A.M:(C-^A)>
オペレーターΛは、内部のラムダ式Mを普通の意味でラムダ抽象します。次の点に注意してください。
- Λは、型コンテキストの一番右側の変数を束縛する。
- 束縛された変数は型コンテキスト(縦棒の左側)から消える
カリー/ハワード対応を経由して、オペレーターΛの論理的対応物を考えると、それは含意導入規則になります。
大きなラムダ式に働く構文的なオペレーターΛのセマンティクスは、デカルト閉圏C内のカリー化同型です。デカルト閉圏C内のカリー化同型も同じ記号Λで表します。ほんとは区別して違う記号を使うべきでしょうが、もう使う記号が思いつかない。ΛA,B,C : C(A×B, C) → C(A, C-^B) です。
さて、構文的なオペレーターΛが作用した形の大きなラムダ式のCにおける意味 Morph(Λ(<x:A, y:B | M:C>)) は、
- ΛA,B,C([x:A, y:B | M:C]) ∈ C(A, C-^B)
となります。これは次のように書いても同じです。
- ΛA,B,C([x:A, y:B | M:C]) : A→(C-^B) in C
定義より Λ(<x:A, y:B | M:C>) = <x:A | λy:A.M:(C-^A)> なので、次の等式が成立します。
- ΛA,B,C([x:A, y:B | M:C]) = [x:A | λy:A.M:(C-^A)]
これで、小さなラムダ式Mのラムダ抽象の意味が、圏のカリー化(随伴によるホムセットの同型)であることが合理化されます。この事実は、Mを大きなラムダ式に入れて考えないとうまく説明できません。
圏的ラムダ計算の一般化とか
ラムダ計算の枠組みは、デカルト閉圏だけではなく、より一般的なセッティングでも使えます。どこまで一般化できるかはよく分からないのですが、非対称的なモノイド閉圏でもいけそうです。
そうはいっても、やはりお手本となるのはデカルト閉圏における計算なので、デカルト閉圏によるモデル構成はちゃんとやってみたほうが良いんじゃないかな、と思いながらも割とイイカゲンな記述でした。まー、オオスジはこんな感じなので、あとは細部を埋めてください。