lambda微積分上下文中「自由變量」和「變量的自由出現」之間的區別

Question

lambda演算上下文中自由變量和變量自由出現之間是否有區別？如果是的話，請用一兩個例子來解釋。 其實我經​​歷了lambda表達式轉換規則我碰到下面一行哪裏傳來：

在說明的轉換規則的符號E[E'/V]用於意味着在V每個自由出現替代E'的結果E

Answer 1

讓我們術語T：

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

（其中x \ t表示拉姆達X。噸 - 這是λ-Prolog的表示法）

有一個自由變量：x和約束變量，其中之一也被命名爲x。但兩個「×」是不的相同變量（在這個意義上，該術語可以是字母命名爲t\q\p\ (t x (y\ q y) (p q x) 但不是，例如，到：t\q\p\ (t x (y\ q y) (p q y)

在術語T上方，有自由變量x的發生和另一個變量的一個約束出現，也命名爲x。

現在，如果你的問題是「哪有，在同期，既自由出現和約束出現相同 variab是吧，是綁定還是免費？「，我不這麼認爲。