${\cal W}$ の健全性

• ${\cal W}$ が健全であることを示すために便利で簡単な定義をする．
• もし $A$ が型で，型付けされた prefix または 型付けされた pe があ る時，
  
  $$\hbox{Vars}(A)\stackrel{\mathrm{def}}{=}\{\alpha\vert\alpha\in A,\alpha\hbox{は型変数である}\}.$$
  
  
  もし $A$ が型づけされた prefix または，型付けされた pe ならば，
  
  $$\hbox{Gen}(A)\stackrel{\mathrm{def}}{=}\{\alpha\vert\alpha\in A,\alpha\hbox{は generic な型変数}\}.$$
  
  
  
  
  $$\hbox{Spec}(A)\stackrel{\mathrm{def}}{=}\hbox{Vars}(A)-\hbox{Gen}(A).$$
  
  
  もし $S$ が置換で，
  $$\begin{eqnarray*} \hbox{Inv}(S)& \stackrel{\mathrm{def}}{=} & \{\alpha\vert S\hb... ...q \beta \hbox {かつ} \alpha\in\{\beta\}\cup\hbox{Vars}(S\beta)\} \end{eqnarray*}$$
  
  
  
  
  

• 以下の簡単な性質を証明することができる(証明は省略)．
  命題6
  1. $\hbox{Inv}(RS)\subseteq\hbox{Inv}(R)\cup\hbox{Inv}(S)$
  2. $\hbox{Vars}(S\tau)\subseteq\hbox{Vars}(\tau)\cup\hbox{Inv}(S).$
  定理2(文法的健全性)
  $\bar{p}$ を standard な prefix とし，$p\vert f$ を閉じた pe とする．その時， もし ${\cal W}(\bar{p},f)=(T,\bar{f}_{\tau})$ ならば，
  1. (A) $T\bar{p}\vert\bar{f}_{\tau}$ は wt.
  2. (B) $\hbox{Inv}(T)\subseteq\hbox{Spec}(\bar{p})\cup New$,
  3. (C) $\hbox{Vars}(\tau)\subseteq\hbox{Spec}(\bar{p})\cup New$
  ここで $New$ とは ${\cal W}$ で使われる新しい型変数の集合を示す．
  証明
  wt の再帰的な定義を使って $f$ の構造による帰納法で証明する． 条件式の場合と $fix$ の場合は省略する．
  1. (i) $f$ が $x$ の場合．$T=I$ より (B) は，すぐにわかる． もし $\lambda x_{\sigma}$ または $fix\:x_{\sigma}$ が $\bar{p}$ の中で active な時， $\bar{f}=x_{\sigma}$ かつ (A)，(C) がわかる． もし $let\:x_{\sigma}$ が active ならば $\tau=[\beta_i/\alpha_i]\sigma$，$\{\alpha_i\}$ は $\sigma$ で generic， $New=\{\beta_i\}$ として $\bar{f}=x_{\tau}$ である． そのため $T\bar{p}\vert\bar{f}=\bar{p}\vert x_{\tau}$ は standard で， (A)，(C) も簡単に証明できる．
  2. (iv) $f$ が $(\lambda x\cdot d)$ の場合． $(R,\bar{d}_{\rho})= {\cal W}(\bar{p}\cdot\lambda x_{\beta},d)$ とする．新しい型変数として， $New$ を使う．帰納法より $R(\bar{p}\cdot\lambda x_{\beta})\vert \bar{d}_{\rho}$ が wt である．よって (A) $f=R\bar{p}\vert(\lambda x_{R\beta}\cdot\bar{d})_{R\beta\rightarrow\rho}$ が wt(wt の定義より)． また，帰納法より
     $$\begin{eqnarray*} \left.\begin{array}{c}\hbox{Inv}(R)\\ \hbox{Vars}(\rho)\end{... ...hbox{Spec}(\bar{p})\cup New\\ & & (New=New_1\cup\{\beta\}より) \end{eqnarray*}$$
     
     
     
     
     
     かつ，$T=R$ より (B) がいえる．(C) のためには，
     $$\begin{eqnarray*} \hbox{Vars}(R\beta\rightarrow\rho) & \subseteq & \hbox{Inv(R)... ... 6}より，上より)\\ & \subseteq & \hbox{Spec}(\bar{p})\cup New \end{eqnarray*}$$
     
     
     
     
     

  3. (vi) $f$ が $(let\:\:x=d\:\:in\:\:e)$ の場合． $(R,\bar{d}_{\rho})={\cal W}(\bar{p},d)$ とする．新しい型変数として $New_1$ を使う．帰納法の仮定より，
     

     $$R\bar{p}\vert\bar{d} \hbox{は} wt$$ (1)

     
     
     
     

     $$\left.\begin{array}{c}\hbox{Inv}(R)\\ \hbox{Vars}(\rho)\end{array}\right\}\subseteq \hbox{Spec}(\bar{p})\cup New_1$$ (2)

     
     
     (2) と命題 6 より，
     

     $$\hbox{Spec}(R\bar{p}) \subseteq \hbox{Inv}(R)\cup\hbox{Spec}(\bar{p})$$

     $$\subseteq \hbox{Spec}(\bar{p})\cup New_1$$ (3)

     
     
     (1) の standardness より，
     

     $$\hbox{Gen}(R\bar{p}\vert\bar{d})\cap\hbox{Spec}(R\bar{p})=\empty.$$ (4)

     
     
     また， $\hbox{Gen}(R\bar{p})=\hbox{Gen}(\bar{p})$ を得，(2) より $\hbox{Vars}(\rho)$ と 独立である．よって， $R\bar{p}\cdot let\:x_{\sigma}$ は standard prefix である．

     そのため $(S,\bar{e}_{\sigma})={\cal W}(R\bar{p}\cdot let\:x_{\sigma},e)$，新しい型変数を $New_2$ とする．帰納法より，
     

     $$S(R\bar{p}\cdot let\:x_{\rho})\vert\bar{e}\:\: \hbox{は wt}$$ (5)

     
     
     
     

     $$\left.\begin{array}{c}\hbox{Inv}(S)\\ \hbox{Vars}(\sigma)\end{array}\right\}\subseteq\hbox{Spec}(R\bar{p}\cdot let\:x_{\sigma})\cup New_2$$ (6)

     
     
     しかし， $\hbox{Spec}(R\bar{p}\cdot let\:x_{\rho})=\hbox{Spec}(R\bar{p})$ なので (6) と (4) いっしょに生ず る($New_2$ は，新しい型変数より)．
     

     $$\hbox{Inv}(S)\cap\hbox{Gen}(R\bar{p}\vert\bar{d})=\empty$$ (7)

     
     
     かつ (1) と命題4 より $S(R\bar{p}\vert\bar{d})$ は wt，そして (5) を使い， wt の定義より，
     $$\begin{eqnarray*}SR\bar{p}\vert(let\:\:x_{S\rho}\:=\:S\bar{d}\:\:in\:\: \bar{e})_{\sigma}\end{eqnarray*}$$
     
     
     
     
     
     が wt. しかし，これは $T\bar{p}\vert\bar{f}$ の形をしているので (A) が証明 したことになる．(B) のためには，
     $$\begin{eqnarray*} \hbox{Inv}(T) & \subseteq &\hbox{Inv}(S)\cup\hbox{Inv}(R)\:\:\... ...Spec}(\bar{p})\cup New_1\cup New_2\:\:\:\hbox{(6) と (2) を使う} \end{eqnarray*}$$
     
     
     
     
     
     そして (C) のためには，同じような理由により((6) より)， この場合は， $New=New_1\cup New_2$ より必要とする結果である．
  4. (ii) $f$ が $(de)$ の場合．