型付きラムダ計算のモデルの作り方 - 檜山正幸のキマイラ飼育記 (はてなBlog)

型付きラムダ計算のモデルをデカルト閉圏で作れるのだけど、ちょっとした注意と工夫が必要です。

Cがデカルト閉圏だとして、ラムダ項Mに対して、Mの表示（denotation）をC内に直接作るもんだと思っている人がいるかも知れませんが、それはあんまりウマくないです。閉じたラムダ項に対して直接Cの射を対応付けることもできるし、そういうセマンティクスの流儀もあるでしょうが、お奨めしません。

デカルト閉圏Cの射に対応づける構文的なブツとして「大きなラムダ式」という概念と記法を導入したことがあります。大きなラムダ式は、型理論の型判断（typing judgement）と同じものだし、論理のシーケントとも同じです。大雑把に言えば「大きなラムダ式＝型判断＝シーケント」。このことは次のエントリーに書いてあります。

小さなラムダ式（単なるラムダ項）ではなくて大きなラムダ式（＝型判断＝シーケント）を射とみなすべきなんですが、大きなラムダ式にどうやって射を対応付けるかをもう少し詳しく書いておくことにします。

内容：

大きなラムダ式・再論
大きなラムダ式のセマンティクス
ラムダ抽象
圏的ラムダ計算の一般化とか

大きなラムダ式・再論

常識的な型付きラムダ計算の構文を考えて、その構文による式（ラムダ項）をM、Nなどとします。このラムダ計算で使う変数の集合をVarとします。また、式Mに出現する自由変数の集合をFreeVar(M)としましょう。当然に、FreeVar(M)⊆Var です。

型を表す構文形式である型項（type term）を導入せずに、モデル側の存在物を構文側に取り込むという横着な方法を使うことにします。どういうことかと言うと、デカルト閉圏Cを決めて、Cの対象そのものを型項の代わりに使います。

変数集合Varの適当な有限部分集合 {x₁, ..., x_n} に対して、γ:{x₁, ..., x_n}→|C| という写像を考えて、このγを変数への型割り当て（type assignment）と呼びます。型割り当てγを、次の形に書いた構文的ブツは型コンテキストです。

x₁:γ(x₁), ..., x_n:γ(x_n)

型割り当てと型コンテキストはほとんど同じものですが、完全に同一視はできません。なぜかと言うと、型割り当てでは、変数の順序を考慮しません（できません）が、型コンテキストはカンマで区切ったリストなので、変数の出現順があります。例えば、次の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> になる。

大きなラムダ式のセマンティクス

型コンテキストΓの一般的な形は、x₁, ..., x_n∈Var、A₁, ..., A_n∈|C| に対して x₁:A₁, ..., x_n:A_n となりますが、めんどくさいので、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] = id_A
[x:A, y:B | y:B] = π²_A,B （直積の第二射影）

2つのラムダ項の並置は適用（apply）を表すので、そのセマンティクスは次のようにします。右指数の記号は「圏の指数のための中置演算子記号」で導入した B-^A を使います。

[z:C | (M N):B] = Δ_C;([z:C | M:(B-^A) ]×[z:C | N:A ]);apply_A,B

ここに出てきた記号を説明しておくと：

Δ_CはCの対角射 C→C×C です。集合圏なら Δ_C(z) = (z, z)
直積の掛け算記号×は射に対しても使ってよくて、直積によるモノイド積です。集合圏なら (f×g)(x, y) = (f(x), g(y))。
apply_A,Bは、Cのなかの適用射（評価射）。apply_A,B : (B-^A)×A → B という射です。集合圏なら、apply_A,B(ψ, a) = ψ(a)、ψ∈B^A。

ラムダ抽象のセマンティクスについては次の節で述べます。