tapl_533.md

tapl_533.md

Types and Programming Languages Exercise 5.3.3

Give a careful proof that |FV(t)| ≦ size(t)

t のサイズについての帰納法で解く。 自由変数の定義(5.3.2)に場合分けして証明する。

• t = x の場合

  自明

  |FV(t)| = |{x}| = 1 = size(t).

• t = λx.t1 の場合

  定義(5.3.2)でラムダ項の自由変数のsetが導ける

  |FV(t)| = |FV(t1)\{x}|

  差集合の定義により

  |FV(t1) \ {x}| ≦ |FV(t1)|

  仮定により |FV(t)| ≦ size(t) なので

  |FV(t1)| ≦ size(t1)

  定義3.3.2よりsizeは小さくなることがわかる(*1)

  size(t1) < size(t)

  よって

  |FV(t)| ≦ size(t)

• t = t1 t2 の場合

  t = λx.t1 とほとんど同じです...

  |FV(t)| = |FV(t1) ∪ FV(t2)|

  |FV(t1)| ∪ FV(t2)| ≦ |FV(t1)| + |FV(t2)|

  |FV(t1)| + |FV(t2)| ≦ size(t1) + size(t2)

  size(t1) + size(t2) ≦ < size(t)

  よって

  |FV(t)| ≦ size(t)

*1 : ラムダ項に包まれてるるのでsizeが減るって事なのだと思いますが、ラムダ項のsizeについて定義が与えられて無い気が...