このブログは、旧・はてなダイアリー「檜山正幸のキマイラ飼育記 メモ編」（http://d.hatena.ne.jp/m-hiyama-memo/）のデータを移行・保存したものであり、今後（2019年1月以降）更新の予定はありません。

今後の更新は、新しいブログ http://m-hiyama-memo.hatenablog.com/ で行います。

型解析：型ユニフィケーション

型検査 caty

型ユニフィケーションは、証明ターゲット S⊆T を証明する過程の中心的な処理である。処理の結果として、いくつかの「不定命題＝動的なチェック条件」を出力する。

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

記号の約束：

  1. S, T, U, V, W ：型
  2. a, b ：スカラー定数
  3. x, y ：型変数
  4. X, Y ：スカラー型（integer, number, string, booleanの4種、nullはシングルトン型として扱う）

SとTのユニフィケーションを行うとして、Sはユニフィケーションの左側型、Tはユニフィケーションの右側型と呼ぶ。左側型Sは右辺型、右側型Tが左辺型であるので注意せよ。

ここでは（他では違う用語法を使った気もするが）、証明ターゲット S⊆T が証明できなかったとき（ユニフィケーション＝証明が）「失敗」という。S∩T = never が確認されたときは「完全に失敗」という。失敗しても完全に失敗かどうかはわからない。完全に失敗のときは、目印に×を付ける。ユニフィケーション処理が成功または続行する場合は、○印に続けてその根拠となる公理や分解規則を示す。ユニフィケーションの後にさらに処理が必要な場合は、★を付ける。

1. Sがneverのとき

常に例外やシグナルを投げるコマンドは、プロファイルの右辺がneverなので、このケースは理論的には無意味ではない。（現実的にはほとんど無意味 ^^;）

  • 確定命題 never⊆T を出力。○公理never

never⊆T は公理から常に真だが、neverが出現するときは警告すべきことも多い。

2. Sがanyのとき

  1. Tがneverならば、完全に失敗。×
  2. Tがanyならば、確定命題 any⊆any を出力。○公理any
  3. Tがシングルトン型bならば、確定命題 any⊆b を出力。★
  4. Tがスカラー型Yならば、確定命題 any⊆Y を出力。★
  5. Tが配列型ならば、確定命題 any⊆T を出力。★
  6. Tがオブジェクト型ならば、確定命題 any⊆T を出力。★
  7. Tがタグ付き型 @β W ならば、確定命題 any⊆(@β W) を出力。★
  8. Tがオプショナル型W?ならば、確定命題 any⊆W? を出力。★（any⊆W に還元）
  9. Tが排他的ユニオン型ならば、anyとTの各成分のORユニフィケーション。結果はすべて失敗。○xuni ★
  10. Tがインターセクション型 y&W ならば、不定命題 any⊆y を出力し、anyとWのユニフィケーション。○inter
  11. Tが型変数yのとき、不定命題 any⊆y を出力。○r-var

any⊆any 以外の確定命題はすべて偽になる。しかし、完全な失敗とは限らない。


3. Sがシングルトン型aのとき

  1. Tがneverならば、完全に失敗。×
  2. Tがanyならば、確定命題 a∈any を出力。○公理any
  3. Tがシングルトン型bならば、確定命題 a = b を出力。○s-eq
  4. Tがスカラー型Yならば、確定命題 a ∈ Y を出力。○s-elem
  5. Tが配列型ならば、完全に失敗。×
  6. Tがオブジェクト型ならば、完全に失敗。×
  7. Tがタグ付き型 @β W ならば、完全に失敗。×
  8. Tがオプショナル型W?ならば、aとWのユニフィケーション。○r-opt
  9. Tが排他的ユニオン型ならば、aとTの各成分のORユニフィケーション。結果として、失敗かまたは単一のユニフィケーション。○xuni
  10. Tがインターセクション型 y&W ならば、不定命題 a∈y を出力し、aとWのユニフィケーション。○inter
  11. Tが型変数yのとき、不定命題 a∈y を出力。○r-var

4. Sがスカラー型Xのとき

  1. Tがneverならば、完全に失敗。×
  2. Tがanyならば、確定命題 X⊆any を出力。○公理any
  3. Tがシングルトン型bならば、確定命題X⊆b を出力。★
  4. Tがスカラー型Yならば、確定命題 X⊆Y を出力。○st-inc
  5. Tが配列型ならば、完全に失敗。×
  6. Tがオブジェクト型ならば、完全に失敗。×
  7. Tがタグ付き型 @β W ならば、完全に失敗。×
  8. Tがオプショナル型 W? ならば、XとWのユニフィケーション。○r-opt
  9. Tが排他的ユニオン型ならば、XとTの各成分のORユニフィケーション。結果として、失敗かまたは単一のユニフィケーション。○xuni
  10. Tがインターセクション型 y&W ならば、不定命題 X⊆y を出力し、XとWのユニフィケーション。○inter
  11. Tが型変数yならば、不定命題 X⊆y を出力。○r-var

5. Sが配列型のとき

  1. Tがneverならば、完全に失敗。×
  2. Tがanyならば、確定命題 S⊆any を出力。○公理any
  3. Tがシングルトン型bならば、完全に失敗。×
  4. Tがスカラー型Yならば、完全に失敗。×
  5. Tが配列型ならば、Sの各項目とTの各項目のANDユニフィケーション。○arr
  6. Tがオブジェクト型ならば、完全に失敗。×
  7. Tがタグ付き型 @β W ならば、完全に失敗。×
  8. Tがオプショナル型 W? ならば、SとWのユニフィケーション。○r-opt
  9. Tが排他的ユニオン型ならば、SとTの各成分のORユニフィケーション。結果として、失敗かまたは単一のユニフィケーション。○xuni
  10. Tがインターセクション型 y&W ならば、不定命題 S⊆y を出力し、SとWのユニフィケーション。○inter
  11. Tが型変数yならば、不定命題S⊆yを出力。○r-var

6. Sがオブジェクト型のとき

  1. Tがneverならば、完全に失敗。×
  2. Tがanyならば、確定命題 X⊆any を出力。○公理any
  3. Tがシングルトン型bならば、完全に失敗。×
  4. Tがスカラー型Yならば、完全に失敗。×
  5. Tが配列型ならば、完全に失敗。×
  6. Tがオブジェクト型ならば、Sの各プロパティとTの各プロパティのANDユニフィケーション。○obj
  7. Tがタグ付き型 @β W ならば、完全に失敗。×
  8. Tがオプショナル型 W? ならば、SとWのユニフィケーション。○r-opt
  9. Tが排他的ユニオン型ならば、SとTの各成分のORユニフィケーション。結果として、失敗かまたは単一のユニフィケーション。○xuni
  10. Tがインターセクション型 y&W ならば、不定命題S⊆yを出力し、SとWのユニフィケーション。○inter
  11. Tが型変数yならば、不定命題S⊆yを出力。○r-var

7. Sがタグ付き型@α Vのとき

  1. Tがneverならば、完全に失敗。×
  2. Tがanyならば、確定命題 X⊆any を出力。○公理any
  3. Tがシングルトン型bならば、完全に失敗。×
  4. Tがスカラー型Yならば、完全に失敗。×
  5. Tが配列型ならば、完全に失敗。×
  6. Tがオブジェクト型ならば、完全に失敗。×
  7. Tがタグ付き型 @β W ならば、確定命題 α=β を出力し、VとWのユニフィケーション。○tag（α=β はその場でやってしまうほうが早いな）
  8. Tがオプショナル型 W? ならば、TとWのユニフィケーション。○r-opt
  9. Tが排他的ユニオン型ならば、SとTの各成分のORユニフィケーション。結果として、失敗かまたは単一のユニフィケーション。○xuni
  10. Tがインターセクション型 y&W ならば、不定命題S⊆yを出力し、SとWのユニフィケーション。○inter
  11. Tが型変数yならば、不定命題S⊆yを出力。○r-var


8. Sが変数xのとき

  1. Tがneverならば、完全に失敗。×
  2. Tがanyならば、確定命題 x⊆any を出力。○公理any
  3. Tがシングルトン型bならば、不定命題 x⊆b を出力。○l-var
  4. Tがスカラー型Yならば、不定命題 x⊆Y を出力。○l-var
  5. Tが配列型ならば、不定命題 x⊆T を出力。○l-var
  6. Tがオブジェクト型ならば、不定命題 x⊆T を出力。○l-var
  7. Tがタグ付き型 @β W ならば、不定命題 x⊆(@β W) を出力。○l-var
  8. Tがオプショナル型 W? ならば、不定命題 x ⊆ W? を出力。○l-var ★（x⊆W に還元）
  9. Tが排他的ユニオン型ならば、不定命題 x⊆T を出力。○l-var★（排他的ユニオンの一般処理ができない）
  10. Tがインターセクション型 y&W ならば、不定命題x⊆yを出力し、xとWのユニフィケーション。○inter
  11. Tが型変数yならば、不定命題x⊆yを出力。○r-var, l-var

9. Sがオプショナル型V?のとき

  1. Tがneverならば、完全に失敗。×
  2. Tがanyならば、確定命題 V?⊆any を出力。★
  3. Tがシングルトン型bならば、確定命題 V?⊆b を出力。★
  4. Tがスカラー型Yならば、確定命題 V?⊆Y を出力。★
  5. Tが配列型ならば、確定命題 V?⊆T を出力。★
  6. Tがオブジェクト型ならば、確定命題 V?⊆T を出力。★
  7. Tがタグ付き型 @β W ならば、確定命題 V?⊆(@β W) を出力。★
  8. Tがオプショナル型 W? ならば、VとWのユニフィケーション。○b-opt
  9. Tが排他的ユニオン型ならば、確定命題 V?⊆T を出力。★（排他的ユニオンの一般処理ができない）
  10. Tがインターセクション型 y&W ならば、不定命題V?⊆yを出力し、V?とWのユニフィケーション。○inter
  11. Tが型変数yならば、不定命題V?⊆yを出力。○r-var

確定命題はすべて偽になる。

10. Sが無制限ユニオン型U∪Vのとき

  • (U, T), (V, T)のANDユニフィケーション。○join ★

出力する命題の形

記号の約束：

  1. a, b：スカラー定数
  2. α, β：タグ名
  3. X, Y：スカラー型
  4. x, y：型変数
  5. S, T, V：型

確定命題：

  1. a = b （s-eq; スカラー定数の比較）
  2. α=β （t-eq; ラベル名の比較）
  3. a ∈ Y （s-elem; sing(a)⊆Y； スカラー定数のスカラー型所属）
  4. X⊆Y （st-eq; スカラー型の比較）

不定命題：

  1. a ∈ y （sing(a)⊆y）
  2. T⊆y （Tは任意の型、r-var）
  3. x⊆T （Tは任意の型、l-var）