Well-Typing アルゴリズムとその正当性

• この節では，prefixed expression の well typing を見つけるという 問いに挑戦する．アルゴリズム ${\cal W}$ を提案する．
• ${\cal W}$の文法的健全性と，完全性を示す．
• 健全性のためには ${\cal W}$ が成功するときは，いつも wt． 完全性のためには，wt が存在するときは，いつも ${\cal W}$ が，少なくと も一つ見つけることができる．
• ${\cal W}$ は，(多分)完全であるが簡単な証明は難しい．本論文では， 健全性に絞る．
• ${\cal W}$ をシミュレートする型チェックアルゴリズムは， LCF メタ言語 ML として，2 年間成功している．その有用性が証明されている．
• $W$ は，Robinson の単一化アルゴリズムを基にしている．${\cal W}$ の完全性の証明では，以下の命題の 第二の部分を必要とするが，健全性の証 明では，第一の性質を必要とするのみである．
  命題5(Robinson)
  式のペア$\sigma$ と $\tau$ に対して，以下を満たす置換 $S$ を生ずるアル ゴリズム ${\cal U}$ がある．
  1. もし ${\cal U}(\sigma,\tau)$ が成功したとすると，$U$ は $\sigma$ と $\tau$ を単一化する(i.e., $U\sigma=U\tau$)．
  2. もし $R$ が $\sigma$ と $\tau$ を単一化すると， ${\cal U}(\sigma,\tau)$ が成功し，ある置換 $U$ を生成することができる (ある置換 $S$ に対して $R=SU$ が成立)．
  さらに，$U$ は $\sigma$ と $\tau$ にある変数を含むのみである．
• プログラム $f$ の well typing を見つけるためには，型付けされた prefix $\bar{p}$ を仮定しなければならない．
• ${\cal W}$ は， $\bar{p}\vert\bar{f}$ が wt である $\bar{f}$ を生ずる と期待する．
• ${\cal W}$ は，置換 $T$ を返し，必要な変換を示す．正確には， もし， ${\cal W}(\bar{p},f)$ が成功したとすると，$(T,\bar{f})$ を返し， $(T\bar{p})\vert\bar{f}$ は wt である，とする．
• previously に出現しなかった型変数を必要とする．そのような型変数 を $\beta$ によって表わし，$\beta_i$ とする．
• ${\cal W}(\bar{p},f)$ を $f$ に関して帰納的に定義する．
• 後でより効率的なアルゴリズム ${\cal J}$ を紹介する．
  アルゴリズム ${\cal W}$
  
  
  $${\cal W}(\bar{p},f)=(T,\bar{f})$$
  
  
  以下を満たす．
  1. もし $f$ が $x$ の場合，