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

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

安全性判定の分解規則

cathand caty 型検査

式Eの計算が、すべての部分式の計算も含めて安全に行われる（と予測できる）とき、《E》 と書く。式Eのすべての部分式とパイプ記号には、番号（一意的ならなんでもいい）が振ってあるとする。異なる番号が同じ場所を指す可能性がある。（[追記]そんなにイッパイ番号いらねー[/追記]）

分解規則（逆推論規則）を ⇒｜ で示す。□ は空の目印。

基底：コマンド呼び出しと定数

  1. 《f》 ⇒｜ □
  2. 《c》 ⇒｜ □

帰納ステップ：

  1. 《E |i F》 ⇒｜ 《E》 [Cod(E)⊆Dom(F)]i 《F》
  2. 《[E, F]》 ⇒｜ 《E》 《F》
  3. 《{α:E, β:F}》 ⇒｜ 《E》 《F》
  4. 《when {α=>E, β=>F}》 ⇒｜ 《E》 《F》
  5. 《each{E}》 ⇒｜ 《E》
  6. 《@a E》 ⇒｜ 《E》
  • 例外：void規則 《E |i F》 ⇒｜ 《E》 《F》 （Dom(F) = void のとき）

制限付き安全性：iは式の入り口番号、jは式の出口番号

  1. S《E》 ⇒｜ [S⊆Dom(E)]i 《E》
  2. 《E》T ⇒｜ 《F》 [Cod(E)⊆T]j
  3. S《E》T ⇒｜[S⊆Dom(E)]i 《F》 [Cod(E)⊆T]j

[追記]なんであれ、名前を付けてあげないとそれを指し示すことができないので、Caty-Jcentric 型理論／型推論／意味論 - 檜山正幸のキマイラ飼育記 メモ編 で触れている演繹系を SIL と呼ぶことにした。Simple Inclusion Logic 、発音は「汁」。[/追記]

安全性の主張（証明ターゲット）は、SIL（Simple Inclusion Logic）命題の有限集合まで還元される。それぞれのSIL命題には、パイプ番号、式入り口番号、式出口番号が付いている。SIL命題（原子論理式）を、SIL演繹系で証明し、失敗した命題番号に対応する位置にマークして、あとは目的に応じて対処する。