CoPLの補助資料で紹介されていた、導出システムEvalRefML3の型安全性の証明が見当たらなかったため、ここに書き残す。

# はじめに

今日は、『プログラミング言語の基礎概念』という、巷では通称CoPLとの略称で知られている、OCamlの操作的意味論を扱っている書籍の内容に沿って、当書では取り扱われてなかったプログラミング言語の参照型機能を備えた言語の型安全性の証明をしていきたいと思います。

参照型がある場合の型安全性の証明については『プログラミング言語の基礎理論』という別の書籍にて解説がされてあったので、今回はその証明をCoPL風のスタイルで書いてみたいと思います。

参照型を備えた言語の操作的意味論については、CoPLの公式サイトにて、導出システムEvalRefML3といった形で紹介されているのでリンク(https://www.fos.kuis.kyoto-u.ac.jp/~igarashi/CoPL/chap13.pdf )のみだけ貼っておくことにして、ここでは説明を省きます。
導出システムEvalRefML3の全規則は、演習システムに置かれてあるrulebook.pdfの中で紹介されてあるので気になる方はそちらで確認してください。(無断転載ｺﾜｲｺﾜｲ(∩´﹏`∩))

この記事ではまず最初に、参照型システムに特有な式に対する型付け規則を紹介して、その次に、ストア型を導入して参照型に対応した値と型の適合性に触れた後、ストア型の拡張についての適合性に関する補題を証明して、最後に型安全性定理の代表的な式の場合について証明をして終わりたいと思います。(実は補題の証明につまづいています。有識者の方どなたか訂正よろしくおねがいします。(｡＞﹏＜)ふぇぇ)

# 参照型の型付け規則
既存の型付け規則に加えて、新たに以下の3つの規則が追加されます。

$$ \frac{\Gamma \vdash e : \tau}{\Gamma \vdash \mbox{ref}　e : \mbox{ref }\tau}\hbox{(T-REF)}$$

$$ \frac{\Gamma \vdash e : \mbox{ref }\tau }{\Gamma \vdash \mbox{!}e : \tau}\hbox{(T-DEREF)}$$

$$\frac{\Gamma \vdash e_1 : \mbox{ref }\tau \quad \Gamma \vdash e_2 : \tau }{\Gamma \vdash e_1 := e_2 : \tau}\hbox{(T-ASSIGN)}$$


# ストア型の導入
EvalRefML3ではロケーション$l$(いわゆるアドレス)も値になります。そしてロケーション$l$の型はストア$S$の内容に依存します。
そこで、ロケーション$l$に型を付けるためには、ストア$S$自身に型を与える必要があります。このストア自身の型をストア型といい、$ST$で表します。
ストア型$ST$は、$l：\tau$という形の表現の列です。

# 値と型の適合性規則
値$v$がストア型$ST$を持つストアのもとで型$\tau$に適合していることを示す関係$ST\models v : \tau$
環境$\epsilon$がストア型$ST$を持つストアのもとで型環境$\Gamma$に適合していることを示す関係$ST\models \epsilon : \Gamma$を次のように同時に再帰的に定義します。

(1) $ST\models v : \tau$は以下のいずれかが成立することと同値である。
　　(a)$\tau&equiv;\mbox{int}$かつ$v&isin;\mathbf{int}$
　　(b)$\tau&equiv;\mbox{bool}$かつ$v&isin;\mathbf{bool}$
　　(c)ある$\tau_1$に対して、$\tau&equiv;\mbox{ref }\tau_1$かつ$v&isin;dom(ST)$かつ$ST(v)=\tau_1$
　　(d)ある$\tau_1,\tau_2,\epsilon,x,e,\Gamma$に対して、$\tau&equiv;\tau_1&rarr;\tau_2$かつ、$v&equiv;(\epsilon)[\mbox{fun}\ x&rarr;e]$かつ、$ST\models\epsilon :\Gamma$かつ、$\Gamma,x:\tau \vdash e : \tau$.
　　(e)ある$\tau_1,\tau_2,\epsilon,x,y,e,\Gamma$に対して、$\tau&equiv;\tau_1&rarr;\tau_2$かつ、$v&equiv;(\epsilon)[\mbox{rec}\ x =\mbox{fun}\ y&rarr;e]$かつ、$ST\models\epsilon :\Gamma$かつ、$\Gamma,x:\tau_1&rarr;\tau_2,y:\tau_1 \vdash e : \tau_2$.
(2) $ST\models \epsilon : \Gamma$は以下のいずれかが成立することと同値である。
　　(a)$\epsilon&equiv;\bullet$かつ$\Gamma&equiv;\bullet$
　　(b)ある$\epsilon',\Gamma',x,v,\tau$に対して、$\epsilon&equiv;(\epsilon',x = v)$かつ$\Gamma&equiv;(\Gamma',x = \tau)$
かつ $ST\models \epsilon' : \Gamma'$かつ$ST\models v : \tau$

以上の定義を踏まえて、次はストアがストア型に適合していることを示す関係性$S\models　ST$を以下のように定義します。

$S\models ST$は、以下が成立することと同値である。
　　　　$dom(S)=dom(ST)かつ任意のl&isin;dom(S)について、ST\models S(l):ST(l)$.

# ストア型の拡張
ストア型$ST_1$と$ST_2$が以下のような関係にあるとき、ストア型$ST_1$は$ST_2$の拡張であるといいます。

$dom(ST_2)&sube;dom(ST_1)$かつ任意の$l&isin;dom(ST_2)$について、$ST_1(l)=ST_2(l)$

型安全性の定理の証明の際に、ストア型の拡張に関する次の補題が必要になります。

#### 補題

$ST\models v : \tau$かつ$ST'$が$ST$の拡張なら、$ST’　\models v : \tau$である。同様に、$ST\models \epsilon : \Gamma$かつ$ST'$が$ST$の拡張なら、$ST’　\models \epsilon : \Gamma$である。

#### 補題の証明
~~前者の命題を証明するには、定義より、$ST\models v : \tau$が(1)(d),(e)の場合には、後者の命題の仮定が必要になる。また、後者の命題を証明するためには、$ST'　\models \epsilon' : \Gamma'$が言えたら$ST’　\models \epsilon',x=v : \Gamma',x=\tau$が言えるという形の帰納法が必要なのだが、この際にもやはり、仮定として前者の命題が必要になる。前者、後者を、それぞれ、仮定必要なしに示す方法がわかりません。
正直言ってお手上げです。無知蒙昧なる私にはどうしたらいいのかわかりません。なので飛ばします。指摘待ちです。~~

追記:

後々考えてみたところ、原論文に書いてあった、"easy induction over v"の記述どおりに、vに関する簡単な帰納法によって証明できることに気がつきました。

#### 前者の証明

$ST\models v : \tau$ならば$ST'\models v : \tau$を証明する。
(1)の各ケースによって場合分けする。

##### (a)の場合
$ST\models v : \tau$より、$\tau&equiv;\mbox{int}$かつ$v&isin;\mathbf{int}$が言えるので、定義より、$ST'\models v : \tau$が言える。

##### (b)の場合
$ST\models v : \tau$より、$\tau&equiv;\mbox{bool}$かつ$v&isin;\mathbf{bool}$が言えるので、定義より、$ST'\models v : \tau$が言える。

##### (c)の場合
$ST\models v : \tau$より、$\tau_1$に対して、$\tau&equiv;\mbox{ref }\tau_1$かつ$v&isin;dom(ST)$かつ$ST(v)=\tau_1$が言える。
ストアの拡張の定義より、$dom(ST)&sube;dom(ST')$かつ任意の$l&isin;dom(ST)$について、$ST(l)=ST'(l)$であるから、
$v&isin;dom(ST')$かつ$ST'(v)=\tau_1$が言えるので、定義より、$ST'\models v : \tau$が言える。

##### (d)の場合
$ST\models v : \tau$より、ある$\tau_1,\tau_2,\epsilon,x,e,\Gamma$に対して、$\tau&equiv;\tau_1&rarr;\tau_2$かつ、$v&equiv;(\epsilon)[\mbox{fun}\ x&rarr;e]$かつ、$ST\models\epsilon :\Gamma$かつ、$\Gamma,x:\tau \vdash e : \tau$である。
任意の$x &isin; dom(\epsilon)$に対して、$ST\models\epsilon(x) :\Gamma(x)$であるから、帰納法の仮定をこれに適用し、任意の$x &isin; dom(\epsilon)$に対して、$ST'\models\epsilon(x) :\Gamma(x)$、つまり、$ST'\models\epsilon :\Gamma$が言える。
よって、ある$\tau_1,\tau_2,\epsilon,x,e,\Gamma$に対して、$\tau&equiv;\tau_1&rarr;\tau_2$かつ、$v&equiv;(\epsilon)[\mbox{fun}\ x&rarr;e]$かつ、$ST'\models\epsilon :\Gamma$かつ、$\Gamma,x:\tau \vdash e : \tau$であることが言えるので、定義より、$ST'\models v : \tau$が言える。

##### (e)の場合
$ST\models v : \tau$より、ある$\tau_1,\tau_2,\epsilon,x,y,e,\Gamma$に対して、$\tau&equiv;\tau_1&rarr;\tau_2$かつ、$v&equiv;(\epsilon)[\mbox{rec}\ x =\mbox{fun}\ y&rarr;e]$かつ、$ST\models\epsilon :\Gamma$かつ、$\Gamma,x:\tau_1&rarr;\tau_2,y:\tau_1 \vdash e : \tau_2$である。
任意の$x &isin; dom(\epsilon)$に対して、$ST\models\epsilon(x) :\Gamma(x)$であるから、帰納法の仮定をこれに適用し、任意の$x &isin; dom(\epsilon)$に対して、$ST'\models\epsilon(x) :\Gamma(x)$、つまり、$ST'\models\epsilon :\Gamma$が言える。
よって、ある$\tau_1,\tau_2,\epsilon,x,y,e,\Gamma$に対して、$\tau&equiv;\tau_1&rarr;\tau_2$かつ、$v&equiv;(\epsilon)[\mbox{rec}\ x =\mbox{fun}\ y&rarr;e]$かつ、$ST'\models\epsilon :\Gamma$かつ、$\Gamma,x:\tau_1&rarr;\tau_2,y:\tau_1 \vdash e : \tau_2$であることが言えるので、定義より、$ST'\models v : \tau$が言える。

（証明終）

#### 後者の証明
(2)の各ケースによって場合分けする。
 $ST\models \epsilon : \Gamma$ならば$ST'\models \epsilon : \Gamma$　　を証明する。
##### (a)の場合
$ST\models \epsilon : \Gamma$より、$\epsilon&equiv;\bullet$かつ$\Gamma&equiv;\bullet$が言える。よって定義より、$ST'\models \epsilon : \Gamma$が言える。
##### (b)の場合
$ST\models \epsilon : \Gamma$より、ある$\epsilon',\Gamma',x,v,\tau$に対して、$\epsilon&equiv;(\epsilon',x = v)$かつ$\Gamma&equiv;(\Gamma',x = \tau)$
かつ $ST\models \epsilon' : \Gamma'$かつ$ST\models v : \tau$が言える。
$ST\models \epsilon' : \Gamma'$に帰納法の仮定を適用して、$ST'\models \epsilon' : \Gamma'$が言える。また、$ST\models v : \tau$に(1)を適用して、$ST'\models v : \tau$が言える。よって定義より、$ST'\models \epsilon : \Gamma$が言える。

（証明終）

# 型安全性定理

以上の定義を使って、EvalRefML3の型安全性定理は以下のように述べることができます。

#### 定理
任意の型環境$\Gamma$、環境$\epsilon$、EvalRefML3式e、型$\tau$、ストア型$ST_1$、実行結果$r$、ストア$S_1$、$S_2$に対して、$\Gamma \vdash e:\tau$かつ$S_1 \models ST_1$かつ$ST_1 \models \epsilon:\Gamma$かつ$S_1/\epsilon \vdash e \Downarrow r/S_2$ならば、$ST_1$の拡張である$ST_2$が存在して、$S_2\models ST_2$かつ$r \not\equiv error$すなわち、ある値$v$について$r\equiv v$、しかも$ST_2\models v :\tau$が成立する。

#### 証明
$S_1/\epsilon \vdash e \Downarrow r/S_2$の導出に関する帰納法で証明します。導出$\mathcal{D}$の結論となる判断が$\mathcal{J}$であることを$\mathcal{D}&isin;\mathcal{J}$と表記します。
また、仮定されている判断$\Gamma \vdash e:\tau$と$S_1/\epsilon \vdash e \Downarrow r/S_2$の導出をそれぞれ$\mathcal{D}_{\tau}$と$\mathcal{D}_r$とする。
$\mathcal{D}_r$の最後の規則について場合分けをします。この記事では、$\mbox{E-INT}$、$\mbox{E-IFT}$、$\mbox{E-VAR}$、$\mbox{E-FUN}$、$\mbox{E-APP}$、$\mbox{E-REF}$、$\mbox{E-DEREF}$、$\mbox{E-ASSIGN}$、$\mbox{E-IFERR1}$の場合のみ示します。

###### 規則 E-INTの場合 :
つまり、ある整数$i$が存在して、
$$\mathcal{D}_r \equiv \frac{}{S/\epsilon \vdash i \Downarrow i/S}(\hbox{E-INT})$$
$$e \equiv i$$
$$r \equiv i$$
$$S_1 \equiv S$$
$$S_2 \equiv S$$
である場合。

示すべきことは、$S_2\models ST_2$かつ$ST_2\models v :\tau$であるような、$ST_1$の拡張である$ST_2$が存在することであるが、$e$の形より、明らかに$\mathcal{D}_{\tau}$の最後の規則は$\mbox{T-INT}$であり、

$$\mathcal{D}_{\tau} \equiv \frac{}{\Gamma \vdash i : \mbox{int}}(\hbox{T-INT})$$
$$\tau \equiv \mbox{int}$$
である。
$ST_2$を$ST_2 \equiv ST_1$として取れば、仮定より、$S_2\models ST_2$が言え、
$\models$の定義より$ST_2\models i:\mbox{int}$が言える。

##### 規則 E-IFTの場合 :
つまり、ある式$e_1$、$e_2$、$e_3$、値$v$、導出$\mathcal{D}_r^{(1)}$、$\mathcal{D}_r^{(2)}$に対して
$$\mathcal{D}_r \equiv \frac{\mathcal{D}_r^{(1)} \quad \mathcal{D}_r^{(2)}}{S_1/\epsilon \vdash \mbox{if } e_1 \mbox{then } e_2 \mbox{else } e_3 \Downarrow v/S_2}(\hbox{E-IFT})$$
$$e \equiv \mbox{if } e_1 \mbox{then } e_2 \mbox{else } e_3$$
$$r \equiv v$$
$$\mathcal{D}_r^{(1)} &isin; S_1 /\epsilon \vdash e_1 \Downarrow \mbox{true} / S_3$$
$$\mathcal{D}_r^{(2)} &isin; S_3 /\epsilon \vdash e_2 \Downarrow v/ S_2$$
である場合。
このとき、式の形から型付け判断の導出の最後の規則は$\mbox{T-IF}$であり、ある導出$\mathcal{D} _\tau^{(1)}$、$\mathcal{D} _\tau^{(2)}$、$\mathcal{D} _\tau^{(3)}$、が存在して

$$\mathcal{D}_ \tau \equiv \frac{\mathcal{D} _\tau^{(1)} \quad \mathcal{D} _\tau^{(2)} \quad \mathcal{D} _\tau^{(3)}}{\Gamma \vdash \mbox{if } e_1 \mbox{then } e_2 \mbox{else } e_3 : \tau}(\hbox{T-IF})$$

$$\mathcal{D} _\tau^{(1)} &isin;\Gamma \vdash e_1:\mbox{bool}$$

$$\mathcal{D} _\tau^{(2)} &isin;\Gamma \vdash e_2:\tau$$

$$\mathcal{D} _\tau^{(3)} &isin;\Gamma \vdash e_3:\tau$$

である。
$\mathcal{D}_r^{(1)}$は$\mathcal{D}_r$の部分導出であるので、帰納法の仮定を$\Gamma \vdash e_1:\mbox{bool}$(の導出$\mathcal{D} _\tau^{(1)}$)と仮定の$S_1\models ST_1$と$ST_1\models\epsilon:\Gamma$に適用して、$S_3\models ST_3$かつ$ST_3\models \mbox{true}:\mbox{bool}$であるような、$ST_1$の拡張$ST_3$が存在することが言える。
よって補題より、$ST_3\models\epsilon:\Gamma$も言える。
同様に、$\mathcal{D}_r^{(2)}$は$\mathcal{D}_r$の部分導出であるので、帰納法の仮定を$\Gamma \vdash e_2:\tau$(の導出$\mathcal{D} _\tau^{(2)}$)と$S_3\models ST_3$と$ST_3\models\epsilon:\Gamma$に適用して、$S_2\models ST_2$かつ$ST_2\models v:\tau$であるような、$ST_3$の拡張$ST_2$が存在することが言える。

###### 規則 E-VARの場合 :
つまり、ある変数$x$が存在して、
$$\mathcal{D}_r \equiv \frac{}{S/\epsilon \vdash x \Downarrow v/S}(\hbox{E-INT})$$
$$e \equiv x$$
$$r \equiv v$$
$$\epsilon(x) = v$$
$$S_1 \equiv S$$
$$S_2 \equiv S$$
である場合。
このとき、式の形から型付け判断の導出の最後の規則は$\mbox{T-VAR}$であり、

$$\mathcal{D}_{\tau} \equiv \frac{}{\Gamma \vdash x : \tau}(\hbox{T-VAR})$$
$$\Gamma(x) = \tau$$
である。
示すべきことは、$S_2\models ST_2$かつ$ST_2\models v :\tau$であるような、$ST_1$の拡張である$ST_2$が存在することであるが、これは仮定の$S_1\models ST_1$と、$ST_1\models\epsilon:\Gamma$、すなわち、$ST_2\models\epsilon:\Gamma$より明らかである。

##### 規則 E-FUN :
つまり、ある変数$x$と式$e_0$が存在して、
$$\mathcal{D}_r \equiv \frac{}{S/\epsilon \vdash \mbox{fun } x &rarr; e_0 \Downarrow (\epsilon)[\mbox{fun}\ x&rarr;e_0]/S}(\hbox{E-FUN})$$
$$e \equiv \mbox{fun}\ x&rarr;e_0$$
$$r \equiv (\epsilon)[\mbox{fun}\ x&rarr;e_0]$$
$$S_1 \equiv S$$
$$S_2 \equiv S$$
である場合。
このとき、式の形から$\mathcal{D} _\tau$の最後の規則は$\mbox{T-FUN}$であり、ある導出$\mathcal{D} _\tau^{(0)}$と型$\tau_1$、$\tau_2$が存在して

$$\mathcal{D}_ \tau \equiv \frac{\mathcal{D} _\tau^{(0)}}{\Gamma 
 \vdash \mbox{fun } x &rarr; e_0 : \tau _1 &rarr; \tau _2}(\hbox{T-FUN})$$

$$\tau &equiv;\tau _1 &rarr; \tau _2$$

$$\mathcal{D} _\tau^{(0)} &isin;\Gamma,x:\tau_1 \vdash e_0:\tau _2$$

である。
仮定より$S_1\models ST_1$かつ$ST_1\models\epsilon:\Gamma$、すなわち、$S_2\models ST_2$かつ$ST_2\models\epsilon:\Gamma$である。
$\Gamma,x:\tau_1 \vdash e_0:\tau _2$とあわせて、$ST_2 \models (\epsilon)[\mbox{fun}\ x&rarr;e_0] : \tau _1 &rarr; \tau _2$がいえる。


##### 規則 E-Appの場合 :
つまり、ある式$e_0$、$e_1$、$e_2$、導出$\mathcal{D}_r^{(1)}$、$\mathcal{D}_r^{(2)}$、$\mathcal{D}_r^{(3)}$、変数$x$、値$v$、$v_1$、環境$\epsilon_0$が存在して、
$$\mathcal{D}_r \equiv \frac{\mathcal{D}_r^{(1)} \quad \mathcal{D}_r^{(2)} \quad \mathcal{D}_r^{(3)}}{S_1/\epsilon \vdash e_1 \ e_2 \Downarrow v/S_2}(\hbox{E-App})$$
$$e \equiv e_1 \ e_2$$
$$r \equiv v$$
$$\mathcal{D}_r^{(1)} &isin; S_1 /\epsilon \vdash e_1 \Downarrow (\epsilon)[\mbox{fun}\ x&rarr;e_0]/ S_3$$
$$\mathcal{D}_r^{(2)} &isin; S_3 /\epsilon \vdash e_2 \Downarrow v_1 /S_4$$
$$\mathcal{D}_r^{(3)} &isin; S_4 /\epsilon,x=v_1 \vdash e_0 \Downarrow v/ S_2$$

である場合。
このとき、式の形から$\mathcal{D} _\tau$の最後の規則は$\mbox{T-App}$であり、ある導出$\mathcal{D} _\tau^{(1)}$、$\mathcal{D} _\tau^{(2)}$、型$\tau _1$が存在して、

$$\mathcal{D}_ \tau \equiv \frac{\mathcal{D} _\tau^{(1)} \quad \mathcal{D} _\tau^{(2)} }{\Gamma \vdash e_1 \ e_2 : \tau}(\hbox{T-App})$$

$$\mathcal{D} _\tau^{(1)} &isin;\Gamma \vdash e_1:\tau _1 &rarr; \tau$$

$$\mathcal{D} _\tau^{(2)} &isin;\Gamma \vdash e_2:\tau _1$$

である。
$\mathcal{D}_r^{(1)}$は$\mathcal{D}_r$の部分導出であるので、帰納法の仮定を$\Gamma \vdash e_1:\tau _1 &rarr; \tau$(の導出$\mathcal{D} _\tau^{(1)}$)と仮定の$S_1\models ST_1$と$ST_1\models\epsilon:\Gamma$に適用して、$S_3\models ST_3$かつ、$ST_3\models (\epsilon)[\mbox{fun}\ x&rarr;e_0]:\tau _1 &rarr; \tau$、すなわち、ある型環境$\Gamma_0$が存在して、$ST_3 \models \epsilon_0 : \Gamma_0$かつ$\Gamma_0,x:\tau_1 \vdash e_0:\tau$
であるような、$ST_1$の拡張$ST_3$が存在することが言える。
よって補題より、$ST_3\models\epsilon:\Gamma$も言える。
同様に、$\mathcal{D}_r^{(2)}$は$\mathcal{D}_r$の部分導出であるので、帰納法の仮定を$\Gamma \vdash e_2:\tau _1$(の導出$\mathcal{D} _\tau^{(2)}$)と$S_3\models ST_3$と$ST_3\models\epsilon:\Gamma$に適用して、$S_4\models ST_4$かつ$ST_4\models v_1:\tau _1$であるような、$ST_3$の拡張$ST_4$が存在することが言える。
よって補題より、$ST_4 \models \epsilon_0 : \Gamma_0$であり、$ST_4 \models \epsilon_0,x=v_1 : \Gamma_0,x=\tau _1$が言える。
さらに、$\mathcal{D}_r^{(3)}$は$\mathcal{D}_r$の部分導出であるので、帰納法の仮定を$\Gamma_0,x:\tau_1 \vdash e_0:\tau$と$S_4\models ST_4$と$ST_4 \models \epsilon_0,x=v_1 : \Gamma_0,x=\tau _1$に適用して、$S_4\models ST_4$かつ$ST_4\models v_1:\tau _1$であるような、$ST_3$の拡張$ST_4$が存在することが言える。

##### 規則 E-REFの場合 :
つまり、ある式$e_1$、値$l$、導出$\mathcal{D}_r^{(1)}$に対して
$$\mathcal{D}_r \equiv \frac{\mathcal{D}_r^{(1)} \quad (l &isin; dom(S_3)) }{S_1/\epsilon \vdash \mbox{ref } e_1 \Downarrow l/S_3,l=v}(\hbox{E-REF})$$
$$e \equiv \mbox{ref } e_1$$
$$r \equiv l$$
$$\mathcal{D}_r^{(1)} &isin; S_1 /\epsilon \vdash e_1 \Downarrow v / S_3$$

である場合。
このとき、式の形から型付け判断の導出の最後の規則は$\mbox{T-REF}$であり、ある導出$\mathcal{D} _\tau^{(1)}$が存在して

$$\mathcal{D}_ \tau \equiv \frac{\mathcal{D} _\tau^{(1)} }{\Gamma \vdash \mbox{ref } e_1  : \mbox{ref }\tau _1}(\hbox{T-REF})$$

$$\mathcal{D} _\tau^{(1)} &isin;\Gamma \vdash e_1:\tau _1$$

である。
$\mathcal{D}_r^{(1)}$は$\mathcal{D}_r$の部分導出であるので、帰納法の仮定を$\Gamma \vdash  e_1: \tau _1$(の導出$\mathcal{D} _\tau^{(1)}$)と仮定の$S_1\models ST_1$と$ST_1\models\epsilon:\Gamma$に適用して、$S_3\models ST_3$かつ$ST_3\models v:\tau _1$であるような、$ST_1$の拡張$ST_3$が存在することが言える。
よって補題より、$ST_3\models\epsilon:\Gamma$も言える。
$S_2 \equiv S_3,l=v$、$ST_2 \equiv ST_3,l:\tau _1$と取れば、$ST_2$は$ST_3$の拡張であり、$S_2 \models ST_2$かつ$ST_2 \models l : \mbox{ref } \tau_1$である。

##### 規則 E-DEREFの場合 :
つまり、ある式$e_1$、値$l$、導出$\mathcal{D}_r^{(1)}$に対して
$$\mathcal{D}_r \equiv \frac{\mathcal{D}_r^{(1)} \quad S_2(l)=v }{S_1/\epsilon \vdash \mbox{!} e_1 \Downarrow v/S_2}(\hbox{E-DEREF})$$
$$e \equiv \mbox{!} e_1$$
$$r \equiv v$$
$$\mathcal{D}_r^{(1)} &isin; S_1 /\epsilon \vdash e_1 \Downarrow v _1 / S_2$$

である場合。
このとき、式の形から型付け判断の導出の最後の規則は$\mbox{T-DEREF}$であり、ある導出$\mathcal{D} _\tau^{(1)}$が存在して

$$\mathcal{D}_ \tau \equiv \frac{\mathcal{D} _\tau^{(1)} }{\Gamma \vdash \mbox{!}e_1:\tau _1}(\hbox{T-DEREF})$$

$$\mathcal{D} _\tau^{(1)} &isin;\Gamma \vdash e_1  : \mbox{ref }\tau _1$$

である。
$\mathcal{D}_r^{(1)}$は$\mathcal{D}_r$の部分導出であるので、帰納法の仮定を$\Gamma \vdash  e_1: \mbox{ref } \tau _1$(の導出$\mathcal{D} _\tau^{(1)}$)と仮定の$S_1\models ST_1$と$ST_1\models\epsilon:\Gamma$に適用して、$S_2\models ST_2$かつ$ST_2\models l:\mbox{ref }\tau _1$であるような、$ST_1$の拡張$ST_2$が存在することが言える。
また、$S_2(l)=v$である。
$ST\models v:\tau$の定義より、$l&isin;dom(ST_2)$かつ$ST_2(l)=\tau _1$である。
よって$S_2\models ST_2$より、$ST_2 \models S_2(l) : ST_2(l)$、すなわち、$ST_2 \models v : \tau _1$である。

##### 規則 E-ASSIGNの場合 :
つまり、ある式$e_1$、$e_2$、値$v$、導出$\mathcal{D}_r^{(1)}$、$\mathcal{D}_r^{(2)}$に対して
$$\mathcal{D}_r \equiv \frac{\mathcal{D}_r^{(1)} \quad \mathcal{D}_r^{(2)} \quad S_2 = S_4[l=v]}{S_1/\epsilon \vdash  e_1 \mbox{ := } e_2 \Downarrow v/S_4}(\hbox{E-ASSIGN})$$
$$e \equiv e_1 \mbox{ := } e_2 $$
$$r \equiv v$$
$$\mathcal{D}_r^{(1)} &isin; S_1 /\epsilon \vdash e_1 \Downarrow l / S_3$$
$$\mathcal{D}_r^{(2)} &isin; S_3 /\epsilon \vdash e_2 \Downarrow v/ S_4$$
である場合。
このとき、式の形から型付け判断の導出の最後の規則は$\mbox{T-ASSIGN}$であり、ある導出$\mathcal{D} _\tau^{(1)}$、$\mathcal{D} _\tau^{(2)}$、が存在して

$$\mathcal{D} _\tau \equiv \frac{\mathcal{D} _\tau^{(1)} \quad \mathcal{D} _\tau^{(2)} }{\Gamma \vdash e_1 \mbox{ := } e_2: \tau}(\hbox{T-ASSIGN})$$

$$\mathcal{D} _\tau^{(1)} &isin;\Gamma \vdash e_1:\mbox{ref } \tau$$

$$\mathcal{D} _\tau^{(2)} &isin;\Gamma \vdash e_2:\tau$$

である。
$\mathcal{D}_r^{(1)}$は$\mathcal{D}_r$の部分導出であるので、帰納法の仮定を$\Gamma \vdash e_1:\mbox{ref } \tau$(の導出$\mathcal{D} _\tau^{(1)}$)と仮定の$S_1\models ST_1$と$ST_1\models\epsilon:\Gamma$に適用して、$S_3\models ST_3$かつ$ST_3\models l:\mbox{ref } \tau$であるような、$ST_1$の拡張$ST_3$が存在することが言える。
よって補題より、$ST_3\models\epsilon:\Gamma$も言える。
同様に、$\mathcal{D}_r^{(2)}$は$\mathcal{D}_r$の部分導出であるので、帰納法の仮定を$\Gamma \vdash e_2:\tau$(の導出$\mathcal{D} _\tau^{(2)}$)と$S_3\models ST_3$と$ST_3\models\epsilon:\Gamma$に適用して、$S_4\models ST_4$かつ$ST_4\models v:\tau$であるような、$ST_3$の拡張$ST_4$が存在することが言える。
よって、$S2 = S4[l=v] \models ST_4$であるから、$ST_2$として$ST_4$を取れば、$S_2\models ST_2$かつ$S2 \models ST_2$である。

##### 規則 E-IFERR1の場合 :
つまり、ある式$e_1$、$e_2$、$e_3$、値$v$、導出$\mathcal{D}_r^{(1)}$に対して
$$\mathcal{D}_r \equiv \frac{\mathcal{D}_r^{(1)}}{S_1/\epsilon \vdash \mbox{if } e_1 \mbox{then } e_2 \mbox{else } e_3 \Downarrow error/S_2}(\hbox{E-IFERR1})$$
$$e \equiv \mbox{if } e_1 \mbox{then } e_2 \mbox{else } e_3$$
$$r \equiv \mbox{error}$$
$$\mathcal{D}_r^{(1)} &isin; S_1 /\epsilon \vdash e_1 \Downarrow r_1 / S_3$$
$$r_1 &notin; \mbox{bool}$$
である場合。
このとき、式の形から導出$\mathcal{D} _\tau$の最後の規則は$\mbox{T-IF}$であり、ある導出$\mathcal{D} _\tau^{(1)}$、$\mathcal{D} _\tau^{(2)}$、$\mathcal{D} _\tau^{(3)}$、が存在して

$$\mathcal{D}_ \tau \equiv \frac{\mathcal{D} _\tau^{(1)} \quad \mathcal{D} _\tau^{(2)} \quad \mathcal{D} _\tau^{(3)}}{\Gamma \vdash \mbox{if } e_1 \mbox{then } e_2 \mbox{else } e_3 : \tau}(\hbox{T-IF})$$

$$\mathcal{D} _\tau^{(1)} &isin;\Gamma \vdash e_1:\mbox{bool}$$

$$\mathcal{D} _\tau^{(2)} &isin;\Gamma \vdash e_2:\tau$$

$$\mathcal{D} _\tau^{(3)} &isin;\Gamma \vdash e_3:\tau$$

である。
$\mathcal{D}_r^{(1)}$は$\mathcal{D}_r$の部分導出であるので、帰納法の仮定を$\Gamma \vdash e_1:\mbox{bool}$(の導出$\mathcal{D} _\tau^{(1)}$)と仮定の$S_1\models ST_1$と$ST_1\models\epsilon:\Gamma$に適用して、$S_3\models ST_3$かつ$ST_3\models r_1:\mbox{bool}$であるような、$ST_1$の拡張$ST_3$が存在、すなわち、$r_1 &isin; \mbox{bool}$となり、これは$r_1 \equiv \mbox{error}$に矛盾するので、実はこの場合(すなわち$\mathcal{D}_r$の最後の規則がE-IFERR1であること)はあり得ない。


（証明終）

# まとめ
上記のpdf内には型安全性の証明には触れていなかったので、不完全燃焼の状態が続いてました。
参照を言語機能として含む操作的意味論の型安全性を証明する手法はいろいろあるみたいですが、当記事で取り扱った手法は、"Xavier Leroy. Polymorphic typing of an algorithmic language. Research report 1778, INRIA, 1992."によるものです。
~~補題の証明がわからないままなので、指摘お待ちしております。~~
追記：ようやくわかりました。なにか間違いがあれば、遠慮なくご指摘ください。
ここまで読んでくださりましてありがとうございました。