/Я language (β)/Tutorials/Lambda calculus interpreter 5/

Full source code ⋅ Previous chapter

Let's take a look at traced term with identity function from the previous chapter:

\x.x - Regarding context of variable x, it is used in abstraction body with a parameter called x (ABS'VAR).

What if we use another name for a single variable in abstraction body?

In term \x.x variable x is bound and in \x.y variable y is free - we came to this conclusion by just checking if abstraction parameter and variable in abstraction body are equivalent. It's a good start:

Highly likely abstraction parameter and variable in abstraction body would enter separately so let's prepend it with constructing a Product:

If product items are equal - result is one of them, if not - result is the same product of items:

Work in progress...