Chris Casinghino が 2010 年に著した Strong Normalization for the Calculus of Constructions という論文を読んだメモです。
本当はノートに書いていて公開するつもりはなかったんですが、何か勿体ないかと思って文字に起こしました。
追記する。
なんと、この論文が 404 エラーでアクセスできなくなっていて手元にしかない状態になっている。
序文[]
CoC は dependency typed programing と higher-order constructive logic のコア言語だよ！ オリジナルは Coquand's 1985 thesis [4] で導入されたよ！ CoC は 25 年間ずっとプログラミング言語と型理論をインスパイアし続けてきたよ！ 今日、 CoC の拡張は Coq と Agda の基礎になっているよ！
CoC の人気は、その表現力と、その嬉しいメタ理論的な性質に起因する。そのような性質の中で最も重要なのは strong normalization, (description) である。この結果は 2 つの重要な情報を持つ。最初に、それは CoC が論理として無矛盾だということを意味している。これは、 CoC を数学の形式化として魅力的な対象とする。二番目に、それは β-convertible であるかどうかをチェックするアルゴリズムの存在を示す。したがって、その型検査は決定可能であり、 CoC はプログラミング言語の実用的な基盤を提供する。
その strong normalization theorem は伝統的に証明することが困難であると考えられている。 Coquand のオリジナルの証明は少なくとも二つのエラーがある。しかし、その後の多くの論文は正しい証明を与えている。その後の年、たくさんの著者はプログラムに役に立つ構造（帰納型……再帰と……可述的な宇宙階層…… large eliminations ）。これらの証明の多くはさらに挑戦的であり、いくつかは全体の論文にまたがっています。
このドキュメントは CoC の strong eliminations の三つの証明をレビューする。それぞれの論文は異なる分野でそのシステムのモデルを構築している。そして、それぞれは CoC のその拡張に対して新奇な貢献をしている。それらのモデルの技術的な詳細は、しばしば威圧的で複雑である。それらの証明を包括的に確認して再現するのではなく、私たちはそれらを支える美しく魅惑的な数学的構造の明瞭な絵を描くことに焦点を当てている。