-2

https://www.cs.cornell.edu/courses/cs4110/2016fa/lectures/lecture15.pdf

One way to avoid the tricky interaction between free and bound names in the substitution operator is to pick a representation for expressions that doesn’t have any names at all! Intuitively, we can think of a bound variable is just a pointer to the λ that binds it. For example, in λx.λy.y x, the y points to the first λ and the x points to the second λ.

The expression λx.λy.y x gets a whitespace between y and x. Should I ignore that whitespace, and see it as λx.(λy.yx) ? Or λx.((λy.y)x) ?

The y points to the first λ and the x points to the second λ.

The first λ on the left, its bound variable is x, why does it say y points to the first λ? And same question for the second λ on the right, why does it say the x points to the second λ while y is its bound variable?

Mr.Wang from Next Door
  • 99

1 Answers1

0

By convention, the scope of a $\lambda$ extends all the way to the right, unless parentheses state otherwise. So, the expression $\lambda x.\lambda y. y\,x$ should be interpreted as $\lambda x.(\lambda y. y\,x)$.

For the de Bruijn representation, you should count the number of nested $\lambda$s from the point where the variable appears and outwards. So, in $\lambda x.\lambda y. y\,x$, from $y$ you count only one $\lambda$ until you reach $\lambda y$, and from $x$, you count two $\lambda$ until you reach $\lambda x$. So, the de Bruijn conversion yields $\lambda.\lambda.0\,1$.

Beware that, when counting, you should exclude $\lambda$s whose scope ends before the variable's occurence. Take for example the expression $\lambda x.(\lambda y. y)\,x$. Like before, from $y$ you count only one $\lambda$ until $\lambda y$, but this time, from $x$ you count again only one $\lambda$ until you reach $\lambda x$, and that is because the scope of $\lambda y$ ends before $x$ appears. So, the de Bruijn conversion yields $\lambda.(\lambda.0)\,0$.

frabala
  • 3,732