Skip to content

Instantly share code, notes, and snippets.

@fujimura
Created September 12, 2012 09:02
Show Gist options
  • Save fujimura/3705395 to your computer and use it in GitHub Desktop.
Save fujimura/3705395 to your computer and use it in GitHub Desktop.
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について定義が与えられて無い気が...

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment