de Bruijn indexの実装に関するQ&A（7章）

[keigo.imai]

https://twitter.com/existy3/status/317480816894689280 より転載・補足しました（文責：今井敬吾）。

[Q] §7.2の termShiftの実装（65ページ）で、 TmVarの場合に第３引数に必ず（打ち切り値cに関わらず）dを足しているのは正しいですか？

[A] はい、正しいです。 本文中で説明されているとおり、TmVar(fi,x,n) の n はその変数が出現する位置における文脈の長さ（＝構文木の根までの経路上にあるλの個数）を表しています。

代入termSubst j s tが返す項において、この文脈の長さが正しい値に保たれるよう、termShift d t は自由変数をシフト(+d)するだけでなく、文脈の長さにもdを足しています。

具体的な項でやってみるとすぐわかると思います。

例えば [2→λ.0](λ.λ.2) = λ.λ.λ.0 について、代入前において0が出現する位置の文脈の長さは1ですが、代入後は3になります。