ラムダ計算の「出現位置」

ラムダ抽象を変形していくにあたり、部分項を追跡することになるが、その部分項を特定するための番地

\mathbb{N}^\ast_+の部分集合

定義 p.75

この定義に従うと、任意のラムダ抽象は一意の木を作ることができる

例えばこんな感じ

これを用いることで、一つのラムダ抽象の中の各項を名指しで呼ぶことができる

p.76にある部分項の表記の仕方と組み合わせて

例えば上のラムダ抽象の場合M=(\lambda xy.x)(\lambda y.x)zとすると、

M/1\cdot1\cdot1は\lambda y.xを表す

絶対にツリーの右側が深くなる

ツリーの作り方

以下の3種類であることを知っておく

つまり、木が分岐するのは関数適用のところのみ

あとは結合の強さがわかっていれば書けるはず(?)