Display for lexical scope 2026-10-31
A table of pointers supporting direct access to active lexical environments without traversing a static chain. A conventional display is indexed by lexical level; a procedure-indexed alternative keeps the newest activation of each procedure and saves and restores the previous table entry on entry and return.
For direct calls under lexical scope, the executing activation's static chain contains the newest surviving activations of its enclosing procedures. This follows by mathematical induction on calls and returns: a direct call inherits a suffix of the caller's chain, and a return restores the previous chain after intervening activations finish. With procedural parameters, a passed programming closure can instead refer to an older still-active enclosing activation, so simply consulting the newest-activation table is insufficient.
Nonlocal variable 2026-10-31
A variable used within a procedure but declared outside it. Under lexical scope, its binding is determined by enclosing declarations and the associated runtime environment, often accessed through a static chain or programming closure.
Use mathematical induction on the sequence of call and return events. The invariant concerns the static chain of the currently executing activation: every stack frame on that chain is the most recent surviving activation of the procedure it represents. It need not hold for the saved chain of an arbitrary suspended caller while a recursive callee is running.
Initially only main is active, so the claim holds. Suppose it holds just before a direct call to a procedure , whose lexical parent is . Without procedural parameters, visibility of means that its declaration lies in the current procedure or in a lexically enclosing procedure. Therefore the activation of needed for the call is on the caller's static chain. By the induction hypothesis, it is the newest surviving activation of .
Create a new activation of whose static link points to this activation. The inherited chain is a suffix of the caller's chain, so its stack frames still represent the newest surviving activations of their procedures. Adding does not make any of those inherited activations out of date: cannot be its own lexical ancestor. The new activation itself is plainly the newest activation of . This covers recursive calls too: an older activation of may survive on the dynamic chain, but is absent from the new activation's static chain.
On return, the callee and every call it made have finished. The caller's saved stack frame and static chain are restored. Any temporarily newer activation of a procedure represented on that chain has returned, so each restored activation is again the most recent surviving one. Thus return preserves the invariant as well.
The claim holds for the executing procedure's static chain throughout every execution using direct calls under lexical scope. Equivalently, writing for the procedure represented by a stack frame ,
No: a procedural parameter can carry an older lexical environment past a newer recursive activation. Here is typed, Pascal-like pseudocode; a function-valued parameter is represented by a programming closure, comprising code and its defining environment.
procedure dummy(): integer;
begin return 0 end;

procedure P(n: integer; f: procedure(): integer): integer;
    var x: integer;
    procedure Q(): integer;
    begin return x end;
begin
    x := n;
    if n = 1 then return P(2, Q)
             else return f()
end;

begin print P(1, dummy) end.
Call the first P activation . It sets its own x to and passes the programming closure into a recursive activation . That activation sets its own x to and calls its parameter f. The resulting activation of Q has its static link pointing to , because that is where the passed procedure was defined. Its dynamic link points to , because that is where it was called.
During this call the dynamic chain contains Q, P2, P1, main, while Q's static chain contains Q, P1, main. The newest surviving activation of P is , but the static chain deliberately uses . Correct lexical scope therefore prints ; blindly consulting current[P] would produce . Both enclosing activations remain alive, so no issue of a returned procedure or dangling pointer is involved.
The failed step in part (d) is precisely the assumption that the callee's lexical environment is a suffix of the direct caller's static chain. A passed programming closure can specify a different, still surviving environment. An implementation supporting such calls must preserve that environment; a table implementation requires additional environment installation and restoration rather than merely consulting newest activations.
Use programming closures that receive evaluated arguments and return a computation in the chosen computational monad. A sufficient core of the semantic value domain is:
data Value = IntVal Integer
           | BoolVal Bool
           | Function ([Value] -> M Value)
Additional constructors may represent the other built-in values. Assume a semantic environment abstract data type with operations lookupEnv :: Env -> Ident -> Value and extend :: Env -> [(Ident,Value)] -> Env. The latter simultaneously adds the listed bindings, shadowing old bindings. Parameter names in one binding list are distinct, and calls have the expected arity.
Define programming closure construction separately; it does not run the body:
close :: Expr -> Env -> Value
close (Lambda xs body) rho =
  Function (\args -> eval body (extend rho (zip xs args)))

apply :: Value -> [Value] -> M Value
apply (Function f) args = f args
The four expression forms have the following semantic equations. Function position is evaluated first, followed by argument expressions from left to right:
eval :: Expr -> Env -> M Value

eval (Variable x) rho = result (lookupEnv rho x)

eval (Apply e es) rho =
  bind (eval e rho) (\f ->
    bind (evalArgs es rho) (\args -> apply f args))

eval e@(Lambda xs body) rho = result (close e rho)

eval (Let d body) rho =
  bind (defn d rho) (\rho' -> eval body rho')

evalArgs :: [Expr] -> Env -> M [Value]
evalArgs [] rho = result []
evalArgs (e:es) rho =
  bind (eval e rho) (\v ->
    bind (evalArgs es rho) (\vs -> result (v:vs)))
The two definition forms are:
defn :: Defn -> Env -> M Env

defn (Val x e) rho =
  bind (eval e rho) (\v -> result (extend rho [(x,v)]))

defn (Rec x e@(Lambda xs body)) rho = result rho'
  where
    rho' = extend rho [(x,v)]
    v = close e rho'
The ordinary definition evaluates its right-hand side in the old semantic environment; its own name is not yet bound there. The recursive definition creates a recursive closure in the extended semantic environment containing itself. Because the right-hand side is a lambda abstraction, constructing that programming closure does not evaluate its body. Haskell's lazy evaluation can tie this recursive data structure without requiring any extra fixed-point operation from the arbitrary computational monad.
Lexical scope is explicit: calling a programming closure extends the defining semantic environment, and its parameters shadow bindings in that semantic environment. The six requested constructs are therefore covered by
Procedural parameter 2026-10-31
A procedure passed as an argument to another procedure. For a nested procedure under lexical scope, the argument must preserve both its code and its defining environment, for example as a programming closure.
Semantic environment 2026-10-31
A mapping from identifiers to their semantic values. A programming closure retains its defining semantic environment; extending it for parameters preserves lexical scope and lets those parameters shadow outer bindings.