Subject Reductionって何だったっけ？という話。

TAPLの索引を見ると、Subject ReductionについてはPreservationを見ろって書いてある。Preservationを見ると、Safety = Progress + Preservationと書いてあって、これは去年の夏どっかで見た話なことを思い出したんだけど、まあそれは良いや。とりあえずTAPL読む。

Types and Programming Languages

We show this in two steps, commonly known as the progress and preservation theorems.

Progress

A well-typed term is not stuck (either it is a value or it can take a step according to the evaluation rules).

Preservation

If a well-typed term takes a step of evaluation, then the resulting term is also well typed.

確かにこの二つの性質が示せれば、well-typedな項を評価していってもstuckしないことが証明できることがわかる。なるほど。

で、後者の性質をSubject Reductionとも言う、と。どういう意味かというと、typing statement(って日本語でなんて言うんだろ) t : Tは「項tは型Tをもつ」といっていて、ここでそのsubjectはt。このsubjectであるところの項tをreductionしても、その表明の正しさは保存される、と。

しかし、わかったようなわからないような説明だこと。

ちなみに私の最初の疑問は、Subject Reductionが何だったか、ということではないんだけど、そっちの疑問についても解消されたので、今回はもう良いことにする。詳しくは大堀先生の教科書で。

プログラミング言語の基礎理論 (情報数学講座)

「プログラミング言語の基礎理論」で検索しても出てこなくて、大堀淳で検索すると出てくるAmazonは、どうかと思うというか、ある意味とても的確かもしれない。