parentheses in free and bound variable in lambda calculus

935 Views Asked by At

I'm now starting the syntax of the lambda calculus, and have a very simple question about the parentheses for free and bound variable.

Are " x1:= λx.x x " and " x2:= (λx.x) x " represent the same? In other word, is the second "x" in x1 free? I know the second "x" in x2 is free for sure, I just wonder what the purpose put parentheses there.

BTW, x3:= λx.x y and x4:= (λy.x) y, I think "y" in x3 is free and "x" in x4 is free, anyone could check for me ? Thanks

3

There are 3 best solutions below

1
On

Yes because $\lambda(x\cdot x)$ is a coefficient and can be substituted.

2
On

It is customary in the $\lambda$-calculus to take $\lambda$-abstraction to have lower precedence than function application. That means that the $\lambda x.y\,z$ is read as $\lambda x.(y\,z)$ and not $(\lambda x.y) z$. So your $\lambda x . x\,x$ is read as $\lambda x . (x\,x)$ (no free variables and the term denotes the operation that applies a term to itself) and you would need to put in the brackets if you meant $(\lambda x. x) x$ (third $x$ is free and the term denotes application of the identity function to $x$).

4
On

The lambda calculus syntax rules/conventions are:

1) application has higher precedence than abstraction. This is:

λx.AB = λx.(AB) ≠ (λx.A)B

2) application is left associative. This means:

ABC = (AB)C ≠ A(BC)

In your specific examples, the semantic difference would be:

  • "x1:= λx.x x" Here x1 is a function that takes a value x and returns x x. So if we apply the function x1 to a free variable z we get: x1 z -reduces to-> z z
  • "x2:= (λx.x) x" Here we have the identity function (λx.x takes an x and returns it as is) applied to the free variable x. So this will reduce to x.

Your guesses about free variables inside x3 and x4 are correct.