0
$\begingroup$

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$.
$\endgroup$
4
  • $\begingroup$ It's basically the same definition. Or rather, the reverse: lexical scope is the region of the program in which the name is bound. You just need to desugar declarations into lambda abstractions, which will depend on the precise concrete syntax. $\endgroup$
    – rici
    Dec 16, 2020 at 1:22
  • $\begingroup$ @rici Then “to implement lexical scope” means “to implement the region of the program”. :-( $\endgroup$
    – beroal
    Dec 16, 2020 at 14:15
  • 1
    $\begingroup$ I'd say "identify" rather than implement. The implementation, like the implementation of bound variables in the lambda calculus, involves the α-substitution with a unique name of bound variables. (For let -like constructions like declarations with initializers, you also need β-reduction.) $\endgroup$
    – rici
    Dec 16, 2020 at 15:25
  • $\begingroup$ @rici Sorry, I do not think what you are saying is clear enough. $\endgroup$
    – beroal
    Dec 17, 2020 at 9:45

0

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.