型解析：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の原子論理式として扱う。

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

x&x ⇒ x
x∪x ⇒ x
x&any ⇒ x
x∪never ⇒ x

公理と推論規則

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

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

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内で次（に相当するメタ定理）が示せる。

S⊆S （true ⊃ S⊆S）
(S⊆T ∧ T⊆Y) ⊃ S⊆U
S = T ⊃ S⊆T
S = T ⊃ T⊆S
(S⊆T ∧ T⊆S) ⊃ S = U

●分解規則

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

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

記号の約束

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

s- : scalar (value)
st- : scalar type
l- : left
r- : right
b- : both
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