Basic Proof Theory 読書記録 其の一
Troelstra先生とSchwichtenberg先生*1の"Basic Proof Theory"もまあ必読書なのでしょうな。頑張ります。
単純型付ラムダ計算の代入補題についてメモ。
代入は以下のように項の複雑性によって帰納的に定義される。
,
(
でないとき*2),
,
,
(
でないとき。w.l.o.g.(一般性を失わず)
FV(
)とあるけどこれはα変換すればそうなるようにできるからということだろうか。)
で、代入補題は以下。
でなく
FV(
) ならば
.
項の深さに関する帰納法で証明しろとのことである。
まずは が変数のときに成立していることを確認する。
のときは
かつ
なので OK。
のときも
かつ
なので OK。
でも
でもないときは代入が起こらないので左辺も右辺も
で OK。
ということは のときと
のときに代入補題が成り立っていると仮定して
のときにも成り立っていれば項が適用の形のときも OK となる。定義より
で、帰納法の仮定より
だが、これも定義から
のことといえるので OK である。
以下同様。
しかし と
の使い分けに迷ってしまったのだけれどどうしたもんか。
も微妙だ。