substitution - lambda演算上下文中“自由变量”和“变量的自由出现”之间的区别

Question

在 lambda 演算的上下文中，自由变量和自由出现的变量之间有什么区别吗？如果是，那么请用一两个例子来解释。实际上，我正在查看 lambda 表达式的转换规则，遇到以下行：

在说明转换规则时，符号E[E'/V]用于表示替换inE'的每个自由出现的结果VE

Answer 1

让我们看一下T这个词：

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

（其中 x\ t 表示 lambda xt - 这是 Lambda-Prolog 表示法）

有一个自由变量：x，和四个绑定变量，其中一个也命名为 x。但是两个“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 有两次自由出现，另一个变量也称为 x 有一次绑定出现。

现在，如果您的问题是“在同一个术语中，同一变量是否可以同时出现自由出现和绑定出现，是绑定的还是自由的？”，我不这么认为。