Lambda calculus (maybe simply typed)
\x.f(x) = \y.f(y)
Rename variables. Can be used to de-brujin encode.
(\x.f(x))(T) = f(T)
This is the reduction that is computational in nature.
\x.F(x) = F
Remove redundant lambdas.
https://opendsa-server.cs.vt.edu/ODSA/Books/PL/html/Syntax.html Formally, the lambda caluclus can be described by the following BNF grammar:
expr = var
| lambda var . expr
| (expr expr)
Start enumerating bindings at the outermost scope.
When new variables are bound in the inner scopes then the largest binding in scope gets incremented.
This produces the variable names at each level.