型解析：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を扱うときの基本的な方向性となる。

型解析：SILと公理・規則群

SILは、連言論理の枠組み（汎用）に、SIL固有の公理と推論規則を付け加えた論理システムである。

●連言論理ベースの演繹系としてのSIL

項と簡約計算

Caty(新)スキーマ言語の型表現を型項、あるいは単に項（term）とも呼ぶ。項には変数（型変数）を含んでもよい。S、Tを項だとして、記号'⊆'を使った、S⊆T という記号的図形をSILの原子論理式とする。今出てきた'⊆'は単なる記号で内容的な意味はない。一方で、説明の地の文でも記号'⊆'を内容的に使うので注意（これは、形式的体系を扱うときのいつもの注意）。

SILと関連して、しかし別な計算システムとして項の簡約計算系がある。簡約計算系については今述べないが、S⇒S' は、項SがS'に簡約されることを示す（含意ではないので注意）。S⇒S' であるとき、構文的に、S'はSより簡単な形となっているが、意味的には S = S'（等号）である。S⇒S' という記号的図形もSILの原子論理式として扱う。

正しい簡約計算の例をいくつか挙げる。

1. x&x ⇒ x
2. x∪x ⇒ x
3. x&any ⇒ x
4. x∪never ⇒ x

公理と推論規則

Sが任意の項として、S⊆S の形をした式（原子論理式）はすべて公理として扱うが、後述の変数置換規則があるので、xを変数（型変数）として、x⊆x という形だけに限定しても十分である。S⇒S' が項簡約計算で示せるとき（つまり、正しいとき）S⇒S' はSILの公理である。その他の公理も含めて以下にまとめる：

1. xが変数で、x⊆x
2. xが変数で、never⊆x
3. xが変数で、x⊆any
4. 正しい簡約等式 S⇒S'
5. 以上が公理のすべて

Pが公理なら当然に、|- P となる。念のために、公理を推論図の形で書いておく。

 

  --------[ref; 反射律]

   x⊆x
 

  -----------[never; 最小元]

   never⊆x

 
  ---------[any; 最大元]

   x⊆any


  ---------[eq; 正しい等式]

   S⇒S'

連言論理の推論規則以外に、次の推論を加える。なお、以下の推論図では、カンマの代わりに空白を使い、注目すべき部分以外は省略して描かないことにする。P[S] は、式Pの部分項としてSが含まれることを示す。正確には、Sは単なる部分項ではなくて、位置を特定された（複数出現を許す）出現である。P[S'/S] は、P[S]におけるSの出現をS'で置き換えた式を意味する。変数の出現に関しては、すべての出現を一斉に置き換える。例えば、x⊆x の左右のx（変数）を別々に置き換えることはできない。

   S⊆T  T⊆U

  -------------[trans; 推移律]

     S⊆U
    P[S]  S⇒S'

  --------------[eq-subst-1; 等値置換-1]

      P[S'/S] 
    P[S']  S⇒S'

  --------------[eq-subst-2; 等値置換-2]

      P[S/S'] 
      P[x] （xは変数、すべての出現を扱う）

  -----------------------------------[var-subst; 変数置換]

      P[S/x] （Sは非オプショナル項、すべての出現の同時置換）

SILでは含意'⊃'はないが、P |- Q のとき、P⊃Q が成立すると考えるとして、S⊆T ∧ T⊆S を S = T の定義とすれば、SIL内で次（に相当するメタ定理）が示せる。

1. S⊆S （true ⊃ S⊆S）
2. (S⊆T ∧ T⊆Y) ⊃ S⊆U
3. S = T ⊃ S⊆T
4. S = T ⊃ T⊆S
5. (S⊆T ∧ T⊆S) ⊃ S = U

●分解規則

分解規則とは、推論規則（図）の上下を逆にしたもので、横棒の上が結論、下が仮定となる。結論が先に与えられて、その結論を導く仮定を求める操作が分解である。推論図と分解図を区別するため、分解図には「↑」を添える。分解規則の一部は、上下を逆さまにして推論規則とも考えるが、推論規則と分解規則の統合は後で行う。

それ以上分解できない命題（論理式）を既約命題と呼ぶ。既約命題であることを強調するときはブラケットで囲む（常にブラケットで囲むわけではない）。黒四角■は、そこに真または偽が入る場所を示す。分解図で■のすぐ上の命題は真偽が確定する命題で、確定命題と呼ぶ。白四角□は、真偽値が不定であることを示す。分解図で□のすぐ上の命題は不定命題と呼ぶ。

記号の約束

分解規則のネーミングに次の略号を採用する。

1. s- : scalar (value)
2. st- : scalar type
3. l- : left
4. r- : right
5. b- : both
6. t- : tag

次のメタ変数を用いる。

• a, b はスカラー定数（リテラル）
• X, Y は、integer, number, string, boolean のいずれか
• α, β は、タグ名
• S, T は任意の型

確定命題

    a = b 

 ↑---------[s-eq; スカラー等値]

     ■
    a∈Y 

 ↑---------[s-elem; スカラー所属]

     ■
    X⊆Y

 ↑---------[st-inc; スカラー型の包含]

     ■
   α = β 

 ↑---------[t-eq; タグ名等値]

     ■

不定命題

    x⊆T

 ↑---------[l-var; 左変数]

     □
    S⊆y

 ↑---------[r-var; 右変数]

     □

複合型の分解規則

配列型、オブジェクト型、排他的ユニオン型は、項目／プロパティ／成分（選択肢）の個数が少数の例を記述するが、n個の場合に一般化することができる。数値ワイルドカード'#', 名前ワイルドカード'*'は、不等号と補集合を使った具体的な条件で書き下す必要がある。論理式の冒頭の丸括弧内はロケーションラベルであるが、これについてはいずれ記述。

  (i, p) [S, S'*] ⊆ [T, T'*]

 ↑--------------------------------------[arr; 配列]

    (i, p.0) S⊆T AND (i, p.#) S'⊆T'
   (i, p) {α:S, *:S'] ⊆ {α:T, *:T']

 ↑--------------------------------------[obj; オブジェクト]

    (i, p.α) S⊆T  AND (i, p.*) S'⊆T'
   (i, p)  (@α S) ⊆ (@β T)

 ↑---------------------------------------[tag; タグ]

   (i, p) [α = β] AND (i, p@α) S⊆T
   (i, p)  S ⊆ T?

 ↑------------------[r-opt; 右オプショナル]

    (i, p) S ⊆ T
   (i, p)  S? ⊆ T?

 ↑------------------[b-opt; 両側オプショナル]

    (i, p) S ⊆ T
   (i, p) S ⊆ (T |  T')

 ↑--------------------------------[xuni; 排他的ユニオン]

    (i, p) S⊆T XOR (i, p) S⊆T'
   (i, p) S ⊆ y&T

 ↑-------------------------------[inter; インターセクション]

   (i, p) [S⊆y] AND (i, p) S⊆T 
   (i, p) S∪S' ⊆ T

 ↑------------------------------[join; 集合のジョイン(無制限ユニオン)]

   (i, p) S⊆T AND (i, p) S'⊆T