I wonder if there is a formal definition of lexical scope so that people can prove things with respect to it, for example, that an interpreter implements lexical scope. You may ask what level of formality I am talking about. For example, I deem the usual definition of the free variables of a lambda term formal: a variable $x$ is free in a term $N$ iff
- $N$ is a variable $y$ and $x=y$, or
- $N$ is the application $M M'$ and $x$ is free in $M$ or $M'$, or
- $N$ is $\lambda y M$ and $x\neq y$ and $x$ is free in $M$.
let
-like constructions like declarations with initializers, you also need β-reduction.) $\endgroup$