型解析：SILへの準備としての連言論理

SIL（Simple Inclusion Logic; 汁）は、Catyの型解析の基盤／背景となる論理システムである。型解析アルゴリズムは、SILを直接的に実装する必要はないが、アルゴリズムの解釈と正当性の主張はSILをベースに行う。

注意：このエントリーは他の関連エントリーとの兼ね合いで大幅に修正したり、場所を移動したりする可能性があります。

●連言論理

SILは、連言論理（conjunctive logic）の一種なので、まず連言論理を一般的に説明する。一般的とは、汎用ということで、世間一般の定式化かどうかは知らない。以下は、オリジナリティはないが檜山が考えた定式化。定義の羅列となるが、型推論において、実例はいくらでも出てくる。

原子論理式を論理結合子∧により結合した記号的図形が連言論理の論理式。ここでは、∧の代わりにカンマを使い、P∧Q∧R ではなく P, Q, R のように書く。原子論理式はローマ大文字、論理式はギリシャ大文字Φ、Ψ、Δなどで表すことにする。論理式（formula）を単に式とも呼ぶ。（Catyスクリプトの式も単に式と呼ぶので、混乱に注意！）空の並び、単一の原子論理式も式に含める。Φ, P, Q, Ψ のような書き方について説明しないが、シーケントの左辺と同じ、と言っておく。

横棒の上下に式を書いた図形を推論図と呼ぶ。推論図は、上が仮定で下が結論である推論規則の表現。まず、論理式を「原子論理式の集合」と解釈していいことを保証する構造規則を導入する。

    Φ, P, Q, Ψ

  ---------------[換]

    Φ, Q, P, Ψ

     Φ, P, Ψ

  ---------------[増]

    Φ, P, P, Ψ


    Φ, P, P, Ψ

  ---------------[減]

     Φ, P, Ψ

P, Q, R のような図形（構文的対象物）としての論理式は、集合 {P, Q, R} とみなしてよい。特に、空な論理式は {}（空集合）、単一の原子論理式からなる論理式は {P}（単元集合、シングルトン） となる。

次は連言論理の基本推論規則である。

    Φ, Ψ

  ----------[射影]

     Φ

Ψは空でもいいので：

    Φ

  --------[恒等]

    Φ

射影の特別な場合として次がある。

    P, Q

  --------[左射影]

     P

構造規則・換と組み合わせれば：

    P, Q

  --------[右射影]

     Q

論理定数、true, false も原子論理式に含まれるとして、次の推論規則も認める。

    

  -----------[true導入]

     true
     false

  -----------[矛盾]

      Φ

falseからは何を推論してもよい。それが矛盾の定義。

以上に挙げた推論図を上下左右に積み重ねて証明図を作ってよい。ΦからΨへの証明図があるとき、ΦからΨが証明可能だといい、Φ |- Ψ と書く。Φ |- Ψ はシーケントと似てるが、次の点が異なるから注意。

1. 右辺のカンマの解釈も∧であり、∨ではない。（古典論理のシーケントの右辺のカンマは∨）
2. 内容的な（メタな）主張であり、形式的な存在（構文的な図形）ではない。

Φ |- Ψ とまったく同じ内容の主張を Ψ -| Φ と書き、次の用語を使う。

• Φ |- Ψ … ΦからΨを証明できる
• Ψ -| Φ … ΨをΦに還元できる

Φ |- Ψ かつ Φ -| Ψ のとき、Φ |-| Ψ と書き、ΦとΨは（論理的に）同値という。Φ |-| Ψ を、Φ≡Ψ と書くこともある。

必要に応じて、論理式を原子論理式の集合とみなすことにすると、射影とtrue/falseに関する推論規則は次の形で述べてもよい。

1. Ψ⊆Φ ならば、Φ |- Ψ
2. {} |- {true}
3. {false} |- Φ

「推論図を上下左右に積み重ねて証明図を作ってよい」の根拠は：

• Φ |- Ψ かつ Ψ |- Δ ならば、Φ |- Δ
• Φ |- Ψ かつ Δ |- Γ ならば、Φ, Δ |- Ψ, Γ

実際の証明図では、区切りにカンマだけでなく空白（間隔）も使い、次の規則を仮定する。

   Φ      Ψ

  -------------

     Φ, Ψ


     Φ, Ψ

  -------------

   Φ      Ψ

その他、図示における省略法やレイアウトの技工があるが、今は説明しない。コツは、連言記号∧、カンマ、空白を適宜使い分けること。論理式をボックス、横棒をワイヤーにした図のほうが描きやすいかもしれない。

●連言的コレクション

今まで、Φ、Ψなどは原子論理式の有限列または有限集合を表わしてきたが、これからは無限列／無限集合も許すとする。原子論理式の無限個の集まりを許した列／集合を連言的コレクション（conjunctive collection）と呼ぶことにする。連言的コレクションは、必要に応じて（文脈ごとに）、カンマで区切られた列、集合、∧で構成された単一論理式、論理式の集まりなどの解釈をする。

連言論理を連言的コレクション（無限を許す）に一般化しておく。構造規則・換を少し修正するが、その他の規則はそのまま通用する。

    Φ, Δ, Γ, Ψ

  ------------------[換]

    Φ, Γ, Δ, Ψ

証明図の仮定、結論、中間の式として無限の連言的コレクションを許すが、証明図が無限になることは許さない。そのため、Φ |- Ψの意味も少し修正する。Φ |- Ψ とは：

• P∈Ψ ごとに、有限のΦ'（Φ'⊆Φ）があって、Φ' から P への有限な証明図がある。

Φ |- Ψ のΦが空の時は、 |- Ψ と書く。この意味は：

• すべての P∈Ψ に対して、仮定を持たない P の有限な証明図がある。

- Ψ のとき、Ψを定理コレクションと呼ぶ。定理コレクションに含まれる原子論理式は、すべて公理だけから証明可能である。

連言的コレクションΦが次の性質を持つときセオリーと呼ぶ。

• Φ |- P ならば P∈Φ

同じことだが、次のようにも言える。

• Φ |- Ψ ならば Ψ⊆Φ

セオリーは、大きなコレクションになりがちで扱いやすいとは言えない。そのため、次の定義をする。

• Φが凖セオリーとは、Φ |- Ψ ならば Ψ≡Ψ' かつ Ψ'⊆Φ となるΨ'が存在する。

与えられた連言的コレクションΔに対して、Δに対する凖セオリーΦを求めることは非常に重要である。Δに対する凖セオリーΦとは次の意味である。

• Δ≡Δ' かつ Δ'⊆Φ となるΔ'がある。
• Φは凖セオリーである。

この定義から、次の性質が出る。

• ΦがΔに対する凖セオリーだとして、Δ |- Γ ならば、Γ'≡ΓかつΓ'⊆ΦとなるΓ'がある。

セオリーは、公理系の同値類の代表元として使える。つまり、論理的に同値な公理系に対するセオリーは一致する。多くの場合、セオリーの代用として凖セオリーを使える。アルゴリズム的には、凖セオリーのほうが（還元／正規化と組み合わせれば）扱いやすい。公理系の同値類に対して、正規化された凖セオリーを一意的に対応させたい -- これがSILを扱うときの基本的な方向性となる。