substitution - ラムダ計算の文脈における「自由変数」と「変数の自由発生」の違い

Question

ラムダ計算のコンテキストで自由変数と変数の自由発生の間に違いはありますか? はいの場合は、例を 1 つまたは 2 つ挙げて説明してください。実際、次の行に出くわしたラムダ式の変換規則を調べていました。

変換規則を述べる際に、表記法は、の各自由出現をE[E'/V]代入した結果を意味するために使用されますE'VE

Answer 1

項 T を取りましょう:

t\q\p\ (t x (x\ q x) (p q x)

(ここで、x\ t はラムダ xt を意味します - これは Lambda-Prolog 表記法です)

自由変数 xが1 つと、束縛変数が4つあり、そのうちの 1 つに x という名前が付いています。ただし、2 つの「x」は同じ変数ではありません(用語の名前を alpha に変更できるという意味では 、たとえば、次のようにはできません。t\q\p\ (t x (y\ q y) (p q x)t\q\p\ (t x (y\ q y) (p q y)

上記の用語 T には、変数 x の2 つの自由な出現と、x という名前の別の変数の 1 つの束縛された出現があります。

さて、あなたの質問が「同じ項に、同じ変数の自由な出現と束縛された出現の両方が存在する可能性はありますか?」という場合、私はそうは思いません。