このオプションの章は、Pierceによる Types and Programming Languages （和訳：型システム入門）の12章に基づいています。 ここでは説明しない非形式的な証明がその章には載っているので、同時に読むと良いでしょう。 この章では、単純型付きラムダ計算の別の基本的な理論的性質を検討します。 型付けされるプログラムの評価は有限回のステップで停止することが保証されるという事実です。 つまり、すべての型付けされた項は正規化可能(normalizable)です。 ここまで考えてきた型安全性とは異なり、正規化性は本格的なプログラミング言語には拡張されません。 なぜなら、本格的な言語ではほとんどの場合、単純型付きラムダ計算に、（MoreStlc章で議論したような）一般再帰や再帰型が拡張され、停止しないプログラムが書けるようになっているからです。 しかし、正規化性の問題は、System F-omegaのように多相なラムダ計算のメタ理論を考える際に、「型のレベル」で再度現れます。 System F-omegaでは、型の表現に事実上単純型付きラムダ計算を含んでおり、型チェックアルゴリズムの停止性は、型の式の「正規化」操作が停止することが保証されていることに依拠しています。 正規化の証明を学習する別の理由は、それが、（ここでやっているように）論理的関係の基本的証明テクニックを含むような型理論の文献において、とても美しく、そして刺激的な数学だからです。 ここで考える計算は、基本型boolと対を持つ単純型付きラムダ計算です。 ここではboolを未解釈基本型として扱う基本ラムダ計算項の処理を細部まで示します。 ブール演算と対の拡張は読者に残しておきます。 この基礎部分でさえ、正規化性は証明が完全に自明ということはありません。 なぜなら、項の各簡約は部分項のリデックスを複製することがあるからです。

練習問題: ★★, standard (norm_fail)

型付けされた項のサイズについての素直な帰納法で正規化性を証明しようとしたとき、どこで失敗するでしょうか？

☐

Exercise: 5 stars, standard, recommended (norm)

The best ways to understand an intricate proof like this is are (1) to help fill it in and (2) to extend it. We've left out some parts of the following development, including some proofs of lemmas and the all the cases involving products and conditionals. Fill them in.

☐

言語

関係する言語の定義から始めます。 MoreStlc章のものと同様です。 そして、型の保存とステップの決定性を含む結果も成立します。 （進行は使いません。） 正規化の節まで飛ばしても構いません...

構文と操作的意味

置換

簡約

型付け

コンテキスト不変性

保存

決定性

正規化

ここからが本当の正規化の証明です。 ゴールはすべての型付けされた項が正規形に簡約されることの証明です。 実際のところ、もうちょっと強いことを証明した方が便利です。 つまり、すべての型付けされた項が値になるということです。 この強い方は、いずれにしろ弱い方から進行補題を使って得ることができますが(なぜでしょう？)、 最初から強い方を証明すれば進行性は必要ありません。 そして、進行性を再び証明することは上では行いませんでした。 これがキーとなる定義です:

あたりまえの事実:

正規化の証明のキーとなる問題は、（多くの帰納法による証明と同様に）十分な強さの帰納法の仮定を見つけることです。 このために、それぞれの型Tに対して型Tの閉じた項の集合R_Tを定義することから始めます。 これらの集合を関係Rを使って定め、tがR_Tの要素であることを R T t と書きます。 （集合R_Tはしばしば飽和集合(saturated sets)あるいは簡約可能性候補(reducibility candidates)と呼ばれます。） 基本言語に対するRの定義は以下の通りです:

• R bool t とは、tが型boolの閉じた項でtが値になって止まることである
• R (T1 -> T2) t とは、tが型 T1 -> T2 の閉じた項で、tが値になり、かつ、 R T1 s となる任意の項sについて、R T2 (t s) となることである。

この定義は必要な強化された帰納法の仮定を与えます。 最初のゴールはすべてのプログラム(つまり、基本型のすべての閉じた項)が停止することを示すことです。 しかし、基本型の閉じた項は関数型の部分項を含むこともできるので、これらについても性質を知ることが必要です。 さらに、これらの部分項が停止することを知るだけでは不十分です。 なぜなら、正規化された関数を正規化された引数へ適用すると置換が行われるため、さらに簡約ステップが発生する可能性があるからです。 これから関数型の項についてより強い条件が必要です。 つまり、自分自身が停止するだけでなく、停止する引数に適用されると停止する結果にならなければならないという条件です。 Rの形は論理的関係(logical relations)証明テクニックの特徴です。 （ここで扱うのは単項関係のみなので、おそらく論理的性質(logical properties)という方がより適切でしょう。） 型Aのすべての閉じた項についてある性質Pを証明したい場合、型についての帰納法により、型Aのすべての項が性質Pを「持ち」、型A->Aのすべての項が性質Pを「保存し」、型(A->A)->(A->A)のすべての項が性質Pを「保存することを保存し」、...ということを証明していきます。 このために型をインデックスとする性質の族を定義します。 基本型Aに対しては、性質は単にPです。 関数型に対しては、その関数が入力の型の性質を満たす値を出力の型の性質を満たす値に写像することを言うものです。 CoqでRの定義を形式化しようとするとき、問題が生じます。 一番自明な形式化は、次のようなパラメータ化された Inductive による命題でしょう：
      Inductive R : ty -> tm -> Prop :=
      | R_bool : forall b t, has_type empty t Bool ->
                      halts t ->
                      R Bool t
      | R_arrow : forall T1 T2 t, has_type empty t (Arrow T1 T2) ->
                      halts t ->
                      (forall s, R T1 s -> R T2 (app t s)) ->
                      R (Arrow T1 T2) t.

残念ながらCoqはこの定義を受け付けません。 なぜなら帰納的定義のstrict positivity requirementを満たさないからです。 strict positivity requirementとは、定義される型がコンストラクタ引数の型の矢印の左に現れてはいけないというものです。 ここで、この規則を破っているのは、R_arrowの第3引数、すなわち、(forall s, R T1 s -> R TS (app t s)) の、特に R T1 s の部分です。 （一番外側のコンストラクタ引数を分離している矢印は規則の対象外です。 そうでなければ、純粋な帰納的性質はまったく定義できません!） この規則がある理由は、正ではない再帰(non-positive recursion)を使って定義された型は停止しない関数を作るのに使うことができ、それがCoqの論理的健全性を脅かすからです。 ここで定義しようとしている関係が完全に問題ないものであるにもかかわらず、strict positivity requirementのテストを通らないので、Coqはこれを拒否します。 幸い、Fixpointを使うとRが定義できます:

この定義からすぐに導かれることとして、すべての集合R_Tについて、そのすべての要素は停止して値となり、また型Tについて閉じていることが言えます:

さて、メインの結果に進みます。 すべての型Tの項がR_Tの要素であることを示すことです。 R_haltsと組み合わせると、すべての型付けされる項は停止して値になることが示されます。

R_T の要素であるか否かは簡約によって変化しない

一種の強保存性を示す予備的補題から始めます。 R_Tの要素であるか否かは簡約によって「不変」(invariant)であるという補題です。 この性質は両方向が必要です。 つまり、R_Tの項がステップを進めてもR_Tにあることを示すことと、ステップ後R_Tの要素になる任意の項が最初からR_Tであることを示すことです。 一番最初に、簡単な予備的補題です。 前向き方法については、言語が決定性を持つという事実に証明が依存していることに注意します。 この補題は非決定的な言語でも成立するかもしれませんが、証明はより難しくなるでしょう!

さてメインの補題ですが、2つの方向に対応する2つの部分から成ります。 それぞれは型Tの構造についての帰納法で進みます。 事実、ここでは型の有限性を本質的な部分で使っています。 ステップを進んだ結果がR_Tの要素であるためには型Tを持つことが必要です。 このことは、前向き方向については、もともとの型保存から得られます。

複数ステップへの一般化については自明です:

逆向き方向については、 tがステップ前に型Tを持つという事実を追加の仮定として加える必要があります。

型Tの項の閉じたインスタンスがR_Tに含まれる

これから、型Tのすべての項がR_Tに含まれることを示すことに取りかかります。 ここで使う帰納法は型付け導出についてのものです（もし、型付け導出の帰納法と全く関係がない型付けされた項についての証明があったら驚くでしょう!）。 ここで技術的に難しいのは、関数抽象の場合だけです。 帰納法で議論していることから、項 abs x T1 t2 がR_(T1->T2)に属していることを示すことにはt2がR_(T2)に属するという帰納法の仮定を含みます。 しかしR_(T2)は「閉じた」項の集合である一方、t2はxを自由変数として含む可能性があるので、これは筋が通りません。 この問題は帰納法の仮定を適度に一般化するという標準的なトリックを使うことで解決されます。 閉じた項を含む主張を証明する代わりに、開いた項tのすべての閉じたインスタンス(instances)をカバーするように一般化します。 非形式的には、補題の主張は次のようになります: もし x1:T1,..xn:Tn |- t : T かつ、 v1,...,vn が R T1 v1, R T2 v2, ..., R Tn vn となる値ならば、 R T ([x1:=v1][x2:=v2]...[xn:=vn]t) である。 証明は、型付け x1:T1,..xn:Tn |- t : T の導出についての帰納法で進みます。 一番興味深いのは、関数抽象の場合です。

多重置換、多重拡張、インスタンス化

しかしながら、主張と補題の証明の形式化に進む前に、項tの多重置換(multiple substitutions)と型付けコンテキストの多重拡張(multiple extensions)についての事実を扱う、ある(かなり退屈な)機構を構築する必要があります。 特に、置換が現れる順序とそれらの相互関係を正確にする必要があります。 これらの詳細は非形式的な紙の証明では単に省略されるのが通常です。 しかしもちろん、Coqはそうはしません。 ここでは閉じた項を置換していることから、1つの置換が他の置換によってできた項に影響するかどうかを心配する必要はありません。 しかしそれでも置換の順序については考慮する必要があります。 なぜなら、x1,...xnに同じ識別子が複数回出現しそれらが違うviやTiと関連付けされている可能性があるからです。 すべてを正確にするために、環境は左から右へ拡張されることとし、多重置換は右から左へ実行されることとします。 これが整合的であることを見るために、...,y:bool,...,y:nat,... と書かれる環境と、対応する ...[y:=(tbool true)]...[y:=(const 3)]...t と書かれる項の置換があるとします。 環境は左から右に拡張されることから、y:natはy:boolを隠します。 置換は右から左に実行されることから、y:=(const 3) が最初に実行され、y:=(tbool true) は何の作用もしません。 これから置換は項の型を正しく保存します。 このポイントを覚えておくと、次の定義が理解できます。 多重置換(multisubstitution)は置換のリストの適用結果です。 置換のリストは環境と呼ばれます(environment)。

(識別子、型)の対のリストを使った型付けコンテキストの継続的拡張についても同様の機構が必要です。 この型付けコンテキストを「型割当て」(type assignment)と呼びます。

環境と型割当てに同様にはたらくいくつかの簡単な操作が必要です。

インスタンス化(instantiation)は型割当てと値環境を同じ定義域で結合します。 この定義域の要素はRに含まれます。

これから、これらの定義についてのいろいろな性質を証明します。

置換についてのさらなる事実

最初に（もともとの）置換について、ある追加の補題が必要です。

多重置換の性質

閉じた環境とは、閉じた項のみを含む環境です。

次は、閉じた項についてのmsubstがどのようにsubst や各項の形に分配されるかを特徴づける一連の補題です。

他の項コンストラクタに対しても同様の関数が必要になるでしょう。

多重拡張の性質

型割当てのふるまいを、対応するコンテキストのふるまいと結合する必要があります。

インスタンス化の性質

以下は簡単です。

multistep(==>*)についての合同補題

これらのいくつかだけが必要になります。必要が生じた時点で追加しなさい。

R補題

最後にすべてをまとめます。 置換についての型付けの保存についてのキーとなる補題は、 多重置換に対応する形にすることができます:

そして一番最後に、メインの補題です。

正規化定理

そして最後の定理です。