圏論の筆算としてのシーケント計算 - 檜山正幸のキマイラ飼育記 (はてなBlog)

うううう、寒い。寒いのダメ。

それはともかく：
シーケント計算について初めて知ったのは、竹内さん（a.k.a ガイシ）の論理の本だったと思います。が、最近は、論理とあまり関係ないところでもシーケント計算を使ってますね。「シーケント計算は論理で使うもの」という意識を捨ててしまうと、けっこう使い所はあるように思えます。特に、トレース付きモノイド圏やコンパクト閉圏における計算では、シーケント計算を使うとラクチンです。

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

内容：

シーケントとその意味
推論規則
自然演繹風の推論も一緒に使う

シーケントとその意味

シーケントの定義は、先日の記事「古典論理のシーケントとコマンド：カリー／ハワード対応」に書いたので参照して下さい。シーケントは次の形をしています。

A₁, ..., A_n ⇒ X₁, ..., X_m

最初から圏C上の意味論を考えることにします。A_i（i = 1, ..., n）、X_j（j = 1, ..., m）は、論理なら命題変数や論理式ですが、ここでは、圏Cの対象だと考えます。圏Cの対象をカンマで区切って並べたものをΓ、Δなどのギリシャ大文字で表します。

対象の並びにも圏Cの対象としての意味を与えます。シーケントの左辺に出現したΓの圏Cにおける解釈を【Γ】_left、右辺に出現したΔの解釈は【Δ】_right とします。左右でカンマの解釈が違うことがあるので、【-】_left = 【-】_right とは限りません。

圏Cとして集合圏Setを選んだとして、例えば次のように定義することができます。

【Γ】_left = 【A₁, ..., A_n】_left = A₁× ... ×A_n
【Δ】_right = 【X₁, ..., X_m】_right = X₁ + ... + X_m

ここで、「×」は直積、「+」は直和です。

左右の解釈を同じにしてもかまいません。Cがモノイド積「*」をひとつだけ持つモノイド圏のときは、左右共にA₁ * ... * A_n のように定義することになります。コンパクト論理のシーケントですね、「Alloy、コンパクト論理、関係圏」に例があります。

さて、シーケント Γ ⇒ Δ の意味ですが、次のどちらかの解釈をしましょう。

シーケント Γ ⇒ Δ に、圏Cの射 f:【Γ】_left→【Δ】_right を割り当てる。
シーケント Γ ⇒ Δ に、圏Cのホムセット C(【Γ】_left, 【Δ】_right) を割り当てる。

論理の場合は、圏Cとしてやせた圏（プレ順序集合）を取る場合が多いので、射でもホムセットでも同じになります。一般の圏の場合でも、f:A→B in C という任意の射について考える事と、ホムセット C(A, B) を持ち出すことはだいたい同じです。

まーいずれにしても、シーケントは「Cの射、または射の集合」を表すことになります。

推論規則

次は推論規則の実例です。

  A ⇒ X
 -----------
  A ⇒ X, Y


  A, B ⇒ X   X, Y ⇒ Z, W
 --------------------------
  A, B, Y ⇒ Z, W

このような推論規則を圏C上で解釈するとどうなるのでしょうか。シーケントが射だったので、推論規則はいくつか（普通は0個、1個、2個）の射から、新しい射を作り出す方法を表します。ちゃんと解釈しようとすると、多圏と高次圏を導入することになりますが、だいたいの話ならホムセットだけでも説明できます。

C = Set として、左側のカンマは直積、右側のカンマは直和と解釈するなら、推論図は次のような図に書き換えられます。

   C(A, X)
 -------------[ρ]
  C(A, X + Y)


  C(A×B, X)  C(X×Y, Z +  W)
 -----------------------------[ψ]
  C(A×B×Y, Z + W)

この図で、上から下に向かって、ホムセットのあいだの写像があるとみなします。つまり、次のような写像ρ、ψを考えるのです。

ρ:C(A, X) → C(A, X + Y)
ψ:C(A×B, X)×C(X×Y, Z + W) → C(A×B×Y, Z + W)

この場合、ρやψの事例を具体的に書き下すことができます。i¹_X,Y:X → (X + Y) を直和への第一標準入射とすると、ρ(f) = f;i¹_X,Y と書けます。ψのほうは（インフォーマルな）ラムダ式で書いてみると、ψ = λ(f, g).λ(a, b, y).g(f(a, b), y) 。

推論規則は、いくつかの射から新しい射を作り出す「射に対する操作」となります。証明は推論の繰り返しなので、やはり「射に対する操作」です。公理シーケントも特殊な推論規則とみなせます。例えば、A ⇒ A という公理は次のような推論規則です。

    *
  -------[ι]
  A ⇒ A

これは、1 を単元集合 {*} として、ι:1 → C(A, A) という写像であり、ι(*) = id_A と定義されているとみなせます。

自然演繹風の推論も一緒に使う

僕は、シーケント計算のなかで自然演繹風の推論図も一緒に使っています。まず例を挙げましょう。

   A
 ------↑
  A  B


   X
 ------↓
  X  Y

これは、上下にシーケントではなくて対象（論理なら命題）を置いた形です。脇に付いている矢印↑、↓は意味があります。上の2つの自然演繹風の推論図は、次のシーケント推論図と同じ意味です。

      *
 -----------
  A, B ⇒ A


     *
 -----------
  X ⇒ X, Y

横棒の上側に何もないので推論とはいえ公理ですね。これらは、次のような使い方をします。

↑がついた推論は、下から上に向けて読み、シーケント推論の左側に適用する。
↓がついた推論は、上から下に向けて読み、シーケント推論の右側に適用する。

具体的には、一番目の自然演繹風推論は直積の射影 π¹:A×B→A、ニ番目の自然演繹風推論は直和の入射 ι¹:X→(X + Y) を表します。次の推論は、上側の A ⇒ B に、2つの自然演繹風推論を適用したもので、その意味は ψ(f) = π¹;f;ι¹ で与えられます。

     A ⇒ X
 --------------[ψ]
  A, B ⇒ X, Y

左下 → 左上 → 右上 → 右下の順で読むとわかりやすと思います。

π¹: A×B → A
f: A → X
ι¹: X → X + Y

もう少し話したい内容もあるのですが、今日はここまで。寒くてダメだ。