Разница между "свободной переменной" и "свободным появлением переменной" в контексте лямбда-исчисления

Question

Есть ли разница между свободной переменной и свободным вхождением переменной в контексте лямбда-исчисления? Если да, то, пожалуйста, объясните с примером или двумя. На самом деле я проходил правила преобразования лямбда-выражения, где наткнулся на следующую строку:

При указании правил преобразования обозначение E[E'/V] используется для обозначения результата замены E' за каждое бесплатное вхождение V в E

Answer 1

Давайте возьмем термин Т:

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

(где x\ t означает лямбда xt - это запись лямбда-пролога)

Существует одна свободная переменная: 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.

Теперь, если ваш вопрос "могут ли быть одним и тем же термином как свободные вхождения, так и связанные вхождения одной и той же переменной, будь то связанные или свободные?", Я так не думаю.