セマンティック駆動な圏的ラムダ計算とシーケント

「型付きラムダ計算のモデルの作り方」の最後において次のように述べました。

デカルト閉圏によるモデル構成はちゃんとやってみたほうが良いんじゃないかな、と思いながらも割とイイカゲンな記述でした。まー、オオスジはこんな感じなので、あとは細部を埋めてください。

往々にして問題は細部にあったりします。「神は細部にやどる」。シーケントの推論規則を2,3書いてみたりしたのですが、自明のように見えていた場所に手強い問題が潜んでいたりします。周辺の足場を固めておかないと、そういう問題に立ち向かうスベがありません。

という次第で、ラムダ計算とデカルト閉圏の関係をもっと細部までハッキリさせることにします。ただし、地雷が埋まっている場所は今回は避けて通り、後で地雷撤去を行うつもりです。

内容：

セマンティック駆動な圏的ラムダ計算とは

ラムダ計算といえば、普通はまず構文をキチンと定義して、その構文に意味を割り当てます。構文領域と意味領域を独立に作って、それらを意味写像で結びつけるわけです。そして、どちらかと言えば構文領域のほうが主題です。

それに対してセマンティック駆動（semantic-driven）というのは、意味領域を先に考えることです。意味領域ありきです。構文は、意味領域上の現象を説明したり計算したりするための道具という位置付けです。構文領域の独立性や純粋性には拘らず、構文と意味を混ぜることを躊躇しません。

その意味領域としてはデカルト閉圏を考えます。デカルト閉圏よりもっと一般的な圏（例えばモノイド閉圏）におけるラムダ計算を視野に入れてはいますが、とりあえずはデカルト閉圏の場合を調べることにします。

「意味領域ありきで、その意味領域とはデカルト閉圏である」ので、「セマンティック駆動」と「圏的」という形容詞を付けたのです。この方針でもラムダ計算と呼べるシロモノが出来るはずです。このテのことは数年前から言ってますね。

「セミナー非参加者にもわかるリアルワールド向けラムダ計算」にて：

ラムダ計算の教科書やコースのほとんど（僕が知る限りすべて）は、ラムダ計算をまずは形式的な記号計算として導入します。記号計算に慣れれば、実在感も生まれる、と、そいういうスタンスですね。僕は「記号操作に慣れてから意味を考える」ことに挫折したので、最初から意味を持つリアルワールドからスタートしたかったのです。

僕のスタンスでは、ラムダ式は実在の直接的な記述であり、ラムダ計算は現に起きている現象に関する実際的な推論に使います。単なる記号ゲームではないのです。

「プログラミング言語の処理系と、デカルト圏の部分閉構造」とそこから参照されているエントリーでも同様な話題について書いています。

「説明したり計算したりするための道具」である構文としては、ラムダ式＋シーケント計算を使います。「圏論の筆算としてのシーケント計算」あたりで提案していたやり方です。

「圏論の筆算としてのシーケント計算」にて：

かけ算九九をおぼえた後、二桁以上の掛け算のために筆算を習いますよね。筆算のおかげで、大きな数の掛け算も遂行できるようになります。シーケント計算は、論理と圏論における筆算のようなもんだと考えることができるでしょう。

今回述べるのは、カリー／ハワード対応を目いっぱい意識した構文です。つまり、論理の計算のなかに型理論の構成要素を可能な限り取り込みます。この構文は、これから使ってみて変える可能性が高いです。なにか叩き台がないと試すことが出来ないので定義をしてみよう、ということです。

型シーケント

「型付きラムダ計算のモデルの作り方」において、大きなラムダ式について述べました。大きなラムダ式と型判断と型シーケントは同じものです。書き方が多少異なるだけです。（以下に出てくる指数の記号「^」については、「圏の指数のための中置演算子記号」を参照。）

• 大きなラムダ式： <x:A | λy:B.(x, y) :(A×B)^B>
• 型判断： x:A |- λy:B.(x, y) :(A×B)^B
• 型シーケント： x:A ⇒ λy:B.(x, y) :(A×B)^B

今回は、一番下側の記法・型シーケントを使います。型シーケントの構文（シンタックス）と意味論（セマンティクス、解釈）については「型付きラムダ計算のモデルの作り方」で概略は説明しています。今回は概略よりもう少し先に進みます。

セマンティック駆動なので、デカルト閉圏Cを最初に選んでおきます。型コンテキストや型シーケントは、この圏C上で解釈することを前提にします。また、「型付きラムダ計算のモデルの作り方」でも述べたように、型変数や型項は使わず、型定数としてCの対象を直接使います。構文領域の型定数記号としてCの対象をそのまんま持って来ちゃうわけです。

圏を前提としたシーケント計算を、「圏論からシーケント計算へ」でも定義しています。今回は、「圏論からシーケント計算へ」とは違った定義にしています。色々なスタイルを試してみたいので。

型付きのラムダ式と代入

まず、説明に使うメタ変数：

1. x, y, z とそれらに下付き添字を付けたものは変数を表すメタ変数
2. A, B, C, X, Y, Z とそれらに下付き添字を付けたものは型（Cの対象）を表すメタ変数
3. M, N とそれらに下付き添字を付けたものはラムダ式（項）を表すメタ変数

ラムダ式の構成は常識的なものですが、ペアリング（explicit pair/pairing）を最初から入れておきます。

1. 変数は項である。
2. MとNが項ならば、適用（application） (M N) は項である。
3. MとNが項ならば、ペア（pairing） (M, N) は項である。
4. Mが項、Aが型ならば、ラムダ抽象（lambda abstraction） λx:A.M は項である。

以上の定義では、型付きラムダ式なのに、変数に型が付いていません。これだと、自己適用 (x x) のようにうまく型付けできない項も入ってきます。しかし、気にしなくても大丈夫です。ラムダ項自体に意味を割り当てることはありません。型コンテキストのもとで型付けできない項は、シーケントのなかに出現できないので、どうせ淘汰されます。

ラムダ式（項）に対するもっとも重要な構文的操作は代入（substitution）です。代入の記法が色々あることは「型推論に関わる論理の概念と用語 その6：substitutionの記法」に書いてますが、ここでは M[x:=N] という形式を採用します。「Mに含まれる変数xの自由な出現をすべてNで置き換えること、またその結果」を意味します。

項の構成に沿って、代入を帰納的に定義すれば次のようです。

1. xが変数のとき、x[x:=N] は N。
2. yがxとは異なる変数のとき、y[x:=N] は y。
3. (M₁ M₂)[x:=N] は (M₁[x:=N] M₂[x:=N])。
4. (M₁, M₂)[x:=N] は (M₁[x:=N], M₂[x:=N])。
5. (λx:A.M)[x:=N] は λx:A.M（何も変わらない）。
6. yがxとは異なる変数のとき、(λy:A.M)[x:=N] は λy:A.(M[x:=N])。

注意すべきは束縛変数の扱いで、代入は束縛変数を置換しません。自由な出現しか置換できないのです。

ラムダ計算においてもっとも基本的な操作はベータ変換ですが、ベータ変換は、(λx:A.M N) を M[x:=N] に変換します。その他の場面でも代入は使われるので、とっても重要です。

コンテキストとシーケントに対する構文的操作

型コンテキストは、変数達（すべて異なる変数） x₁, ..., x_n と型達 A₁, ..., A_n を使って x₁:A₁, ..., x_n:A_n と書けます。単一の型宣言 x:A だけでも型コンテキストだし、空な型コンテキストも認めます。型コンテキストをΓやΔで表します。

コンテキストの連接と宣言追加

ΓとΔが型コンテキストのとき、そのリストとしての連接（concatenation）を Γ, Δ と書きます。Γが空なら、Γ, Δ はΔのことだし、Δが空なら Γ, Δ はΓのこと。両方とも空なら Γ, Δ は空です。

型コンテキストΓの右側に x:A という型宣言（型仮定）を加えた型コンテキストは、Γ, x:A と書きます。Γが空のときは、Γ, x:A は x:A のことです。

Γ, Δ や Γ, x:A という記法を使う時は、連接や結果のコンテキストが正しいコンテキスト、つまり出現する変数名に重複がないことを前提します。変数名に重複が出てしまうときは、次に述べるリネームを行います。

変数のリネーム：アルファ変換

ラムダ式にアルファ変換があるのと同様に、型シーケントにもアルファ変換を定義しておきます。

型コンテキストΓが x₁:A₁, ..., x_n:A_n の形をしているとき、x₁, ..., x_n のうちの1個 x_iを y に置き換えたものをΓ'とします。Γ ⇒ M:X に対して、Γ' ⇒ M[x_i:=y]:X をアルファ変換だとします。

シーケント Γ ⇒ M:X とそのアルファ変換（した結果）は、区別しなことにします。変数にどんな名前を使うかは恣意的な選択であり、なんら本質的ではないので、名前を変えても実質には何も影響しません。今後は、いちいち断らなくても必要があればアルファ変換を施すとします。

今回は深入りしないこと

変数以外の定数記号・関数記号は今回導入しません。セマンティック駆動の立場だと、定数記号の導入はけっこう難しいです。デルタ変換も手間かも知れません（デルタ変換は調べてないので見積もれないです）。

圏Cの単位対象（デカルト閉圏では終対象でもある）の扱いもやっかいです。単位対象は、定数記号と深く関係します。単位対象の問題は別な機会に述べることにして、今回は触れてません。

関数記号がないので、ペアから射影により成分を取り出す方法がありません。射影（の記号）なしでもなんとかなるものなのか？ 現状、分かりません。

シーケントの右辺が空のときどう解釈すべきか？ これも単位対象の扱い方と関連します。今回は、とりあえず右辺が空を認めないことにします。

「減」（contraction）構造規則も悩んだところです。最初は、x:A, x:A のような型宣言の重複出現を認める方向で考えてましたが、なんかイヤな予感がしてやめました。型宣言の消去と項の代入をセットにする方法にしました。

シーケント計算の伝統に従って、公理を最小限にする方式にしましたが、公理を増やしてみる方向もあるかも知れません。これもやってみないと分かりませんね。

推論規則

型シーケントは、Γ ⇒ M:X のような形でした。Γは空でもよいとして、右辺は空でないとします。推論規則は、もとになる0個、1個、2個のシーケントから、1個のシーケントを導出する仕掛けです。シーケントは圏Cの射に対応し、推論規則はいくつかの射をオペランドとするC上のオペレーターに対応します。

公理

公理は、もとになるシーケントが0個の推論規則です。x:A ⇒ x:A が公理のシーケントですが、この形のシーケントは無から生じると思っていいです。

       *
  -------------[Ident]
   x:A ⇒ x:A 

横線の上段の星印は、「何もない」を示す目印で、特に意味はありません。下段のシーケントは圏の恒等射に対応します。

コンテキストに対する構造規則

シーケント計算で通常用いられる構造規則である「換、増、減」は、コンテキスト（シーケントの左辺）だけに定義します。

    Γ, x:A, y:B, Δ ⇒ M:X
  ---------------------------[Exch x, y]
    Γ, y:B, x:A, Δ ⇒ M:X

↑は、換（exchange）構造規則です。対称モノイド圏の対称射（の前結合）に相当します。

    Γ ⇒ M:X
  -------------------[Thin z:C]
    Γ, z:C ⇒ M:X

↑は、増（thinning, weakening）構造規則です。デカルト圏の終射（終対象への射）、または射影（の前結合）に相当します。

    Γ, x:A, y:A ⇒ M:X
  -----------------------[Cont x, y]
      Γ, x:A ⇒ M[y:=x]:X

↑は、減（contraction）構造規則です。対角付きモノイド圏の対角射（の前結合）に相当します。デカルト圏には標準的な対角射が存在します。

代入規則

圏の（部分的かもしれない）結合（composition）に相当する推論規則を述べます。

   Γ ⇒ M:X   x:X, Δ ⇒ N:Y
  ----------------------------[Subst]
   Γ, Δ ⇒ N[x:=M]:Y

論理ではカット規則ですが、項への代入が発生するので、代入（substitution）規則と呼ぶことにします。

項の構成規則

適用、ペア、ラムダ抽象を構成する規則は次のようになります。

   Γ ⇒ M:Y^X   Δ ⇒ N:X
  --------------------------[Apply]
   Γ, Δ ⇒ (M N):Y

   Γ ⇒ M:X   Δ ⇒ N:Y
  ------------------------[Pair]
   Γ, Δ ⇒ (M, N):X×Y

   Γ, x:A ⇒ M:X
  ----------------------[Abst]
   Γ ⇒ (λx:A.M):X^A

同値な項の置換規則

ラムダ式の変換として、アルファ変換、ベータ変換、イータ変換を考えます。これらの変換で生成される同値関係を「≡」とします。M ≡ N は、MとNが同じ項に変換可能であることを示します。実際には、変換が同値関係を定めるには合流性（チャーチ／ロッサー性）が必要で、難しい話です。ここでは、そういう同値関係を天下りに前提します。

   Γ ⇒ M:X （M ≡ N のとき）
  ------------[Equiv M, N]
   Γ ⇒ N:X 

シーケントと推論規則の意味論

型シーケント Γ ⇒ M:X に対して、圏Cにおける意味を [Γ ⇒ M:X] と書くことにします。シーケントの意味は、圏Cの射です。推論規則の意味は、上段のシーケントの意味である射から、下段の射を作り出す方法となります。

型コンテキストΓが x₁:A₁, ..., x_n:A_n の形のとき、[Γ] = A₁× ... ×A_n です。[x:A] = A、[空] = I（Iは単位対象）とします。

すぐ後の意味規則で出てくる記号を説明しておきます。

• σ_A,Bは、対称モノイド圏としてのCの対称射（AとBの入れ替え）、σ_A,B:A×B→B×A 。
• !_A は、単位対象（＝終対象）への射、!_A:A→1 。
• ρ_A はモノイド圏としてのCの右単位律構造射（「豊饒圏をちゃんと定義したい」の「モノイド圏」の所を参照）、ρ_A:A×I→A 。
• Δ_Aは、対角付きモノイド圏としてのCの対角射、Δ_A:A→A×A 。
• apply_A,Bは、デカルト閉圏の適用射（評価射）、apply_A,B:(B^A)×A→B 。
• Λ_A,B,Cは、デカルト閉圏のカリー化の写像、Λ_A,B,C:C(A×B, C)→C(A, C^B) 。

意味規則は次のようになります。

1. 公理の意味： [x:A ⇒ x:A] = id_A
2. 換・構造規則の意味：[Γ, x:A, y:B, Δ ⇒ M:X] = (f:[Γ]×A×B×[Δ]→X) のとき、[Γ, y:B, x:A, Δ ⇒ M:X] = (id_[Γ]×σ_A,B×id_[Δ]);f
3. 増・構造規則の意味： [Γ ⇒ M:X] = (f:[Γ]→X) のとき、[Γ, z:C ⇒ M:X] = (id_[Γ]×!_C);ρ_[Γ];f
4. 減・構造規則の意味： [Γ, x:A, y:A ⇒ M:X] = (f: [Γ]×A×A→X) のとき、[Γ, x:A ⇒ M[y:=x]:X] = (id_[Γ]×Δ_A);f
5. 代入規則の意味： [Γ ⇒ M:X] = (f:[Γ]→X)、[x:X, Δ ⇒ N:Y] = (g:X×[Δ]→Y) のとき、[Γ, Δ ⇒ N[x:=M]:Y] = (f×id_[Γ]);g
6. 適用の構成規則の意味： [Γ ⇒ M:Y^X] = (f:[Γ]→Y^X)、[Δ ⇒ N:X] = (g:[Δ]→X) のとき、[Γ, Δ ⇒ (M N):Y] = (f×g);apply_X,Y
7. ペアの構成規則の意味： [Γ ⇒ M:X] = (f:[Γ]→X)、[Δ ⇒ N:Y] = (g:[Δ]→Y) のとき、[Γ, Δ ⇒ (M, N):X×Y] = f×g
8. ラムダ抽象の構成規則の意味： [Γ, x:A ⇒ M:X] = (f:[Γ]×A→X) のとき、[Γ ⇒ (λx:A.M):X^A] = Λ_[Γ],A,X(f)
9. 同値な項の置換規則の意味： [Γ ⇒ M:X] = (f:[Γ]→X) のとき、[Γ ⇒ N:X] = f

以上の意味規則がwell-definedであるかどうかは細かいチェックを必要とします。例えば、M ≡ N ならば [Γ ⇒ M:X] = [Γ ⇒ N:X] が成立しないと、同値な項の置換規則と意味規則が整合しません。なかなかに面倒な話です。

シーケントの推論規則と、デカルト閉圏の構造を与える射／オペレーターとの対応をまとめると、次の表のようになります。

推論規則	デカルト閉圏の射
公理	idA
換・構造規則	σA,B
増・構造規則	!A, ρA
減・構造規則	ΔA
代入規則	;
適用の構成規則	applyA,B
ペアの構成規則	×
ラムダ抽象の構成規則	ΛA,B,C

課題など

セマンティック駆動の立場だと、最初にデカルト閉圏Cを決めて、Cの状況をできるだけ記号の世界に移そうとします。記号の計算や推論で、Cの性質を調べたいわけです。

この目的でラムダ式＋シーケント計算を組み立ててみると、記号の計算能力がなんか不足している感じがします。例えば、指数の計算がほとんど出来ないのです。他の方法（主に絵算だけど）から出てくる結果を形式的記号計算のなかで再現しようとしてもうまくいかない事があります。これは、練習や工夫が不足しているせいか？ 構文の拡張をすべきなのか？ まー、課題ですね。