0

Is there any difference between free variable and free occurrence of a variable in context of lambda calculus? If yes, then please explain with an example or two. Actually I was going through the conversion rules for lambda expression where I came across the following line:

In stating the conversion rules the notation E[E'/V] is used to mean the result of substituting E' for each free occurrence of V in E

Cactus
  • 27,075
  • 9
  • 69
  • 149
Ankit Shubham
  • 2,989
  • 2
  • 36
  • 61

1 Answers1

1

Let's take the term T:

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

(where x\ t means lambda x.t - this is Lambda-Prolog notation)

There is one free variable: x, and four bound variables, one of which is also named x. But the two "x" are not the same variable (in the sense that the term can be alpha renamed to t\q\p\ (t x (y\ q y) (p q x) but not, for example, to: t\q\p\ (t x (y\ q y) (p q y)

In the term T above, there are two free occurrences of the variable x and one bound occurrence of another variable, also named x.

Now, if your question is "can there be, in the same term, both free occurrences and bound occurrences of the same variable, be it bound or free?", I don't think so.

ZakC
  • 479
  • 3
  • 11