Three questions w.r.t. the environment model of ev

问题:

I am reading the SICP book Here about the imperative programming model. I could not understand the illustration in two points:

1. W.r.t. the arrow from square to the "pair" (the two circles): What does this arrow mean? Though throughout this section, an arrow means "enclosing environment", this specific arrow seems not pointing to an environment.(square 's environment is the global env, not the "pair")
2. Is below a correct understanding: in the value of a procedure definition, its "code text" part (the left circle) has no interpretation of the symbols within. They are just "text". Only at procedure application, they gain meaning inside the context / environment of the application.
3. If 2 is correct, Why the arrow from the environment part of the pair (the right circle) to the enclosing environment is necessary? (since there is no meaning to interpret the meaning of symbols within procedure code inside the procedure definition.)

回答1:

SICP's arrow notation is a little overloaded. I'll quote the relevant portion of the text to understand this diagram.

The procedure object is a pair whose code specifies that the procedure has one formal parameter, namely x, and a procedure body (* x x). The environment part of the procedure is a pointer to the global environment, since that is the environment in which the lambda expression was evaluated to produce the procedure. A new binding, which associates the procedure object with the symbol square, has been added to the global frame. In general, define creates definitions by adding bindings to frames.

So, let's analyze each arrow.

1. "global env" → the square. This arrow appears to simply be labeling the square as symbolizing the global environment. Notably, this environment is the only stack frame alive since define was called in the global environment.

2. "square" → the two dots. This arrow appears to be stating that whatever those two dots represent is stored at the name "square" which is found in the global environment.

3. left dot → "parameters"/"body". This arrow indicates that the left dot is an "object" thought to be storing two pieces of data, the "list of formal parameters" and the "procedure body".

4. right dot → the square. This arrow indicates that the right dot contains a "pointer" back to the global environment.

---

This diagram is giving a highly operational POV on how symbols derive meaning in Lisp. In particular, a symbol is "evaluated" in a particular "context". A context is a linked list of "environment frames" each containing some set of name→value mappings. To evaluate a symbol one follows that linked list and returns the first value which is mapped from the symbol's name. Diagrammatically an example would be

"foo" → { "bar" : 3    →  { "foo" : 8 }   →   { "foo" : 10 }
        , "baz" : 4 }

where evaluating foo returns 8 by "skipping" the first frame and finding the value 8 in the second frame while ignoring the third frame. This ignoring feature is important---it suggests that some contexts might have names which shadow values from larger contexts.

---

So the whole picture here is indicating the following:

1. Calling define in the global context adds a new name→value mapping to the global frame.

2. Storing a lambda object stores two pieces of information (two dots)

   • The left dot contains the text of the body of the lambda along with a listing of the symbols which are to be considered "formal parameters".

   • The right dot contains a reference to some stack frame which may or may not be the global frame, although it happens to be the global frame in this picture

Finally, we ought to talk about what it means to evaluate a lambda. To evaluate a lambda you must pass it a list of values. It uses that list of input values and matches them against the formal parameter list it stored in order to generate a new environment frame which maps formal parameters to input values. Then, it evaluates the body of the lambda using that new frame as the primary frame and the linked frame as the follow-up context. Diagrammatically, let's say square looked like

        +--- Formal parameter list
       /   +--- Body of function
       |   |
(left: (x) (* x x))    (right: {global frame})

Then when we evaluate it like (square 3) we create a new frame using 3 and the formal parameter list

{ "x" : 3 }

and evaluate the body. First we look up the name *. Since it's not in our new local frame we have to find it in the global frame.

"*"   →   { "x" : 3 }   →   { global frame }

It turns out to exist there and is the definition of multiplication. We thus need to pass it some values so we look up "x"

"x"   →   { "x" : 3 }   →   { global frame }

since x is stored in the local frame we find it there and pass 3 and 3 as arguments to the multiplication function we found.

The important part is that the local frame shadows the global frame. That means that if x also had meaning in the global frame we would override it in the context of evaluating the body of square.

---

Finally, as I was asked to answer this question in context of questions about what the meaning of "variable" is---it's important to note that the above is a very particular implementation of a very particular semantics of variables. At its surface, you can always say that "variables in lisp mean exactly this process occurs". That can be a little challenging to work with, though.

Another semantics of the word "variable" (one which I and much of mathematics favor) is the idea that a variable in a context stands for a particular, fixed but unknown value in a domain. If we examine the definition of the lambda in the body of square

(lambda (x) (* x x))

we see that this is more-or-less the intended semantics of this phrase---in interpreting (* x x) we see x as being some value value (e.g. a number) but one that we don't know anything about. In interpreting (lambda (x) (* x x)) we see that in order to understand the meaning of the phrase inside of the lambda we must provide it a meaning of x. This is roughly the standard semantics of variables and functions used everywhere.

The challenge is that the stack frame implementation described here is also set up to easily violate this semantics---in fact, it does so very subtly in this example. To be particular: define breaks semantics. The reason is apparent in the following fragment of code

(define foo 3)
foo
(define foo 4)
foo

In this fragment we evaluate each phrase sequentially and see that the (supposedly "fixed but unknown") value of the variable foo changes from line 2 to line 4. This is because define allows us to edit the stack frame that's live in a context rather than merely create a new context which shadows the old one like lambda does. This means that we must consider variables as not "fixed but unknown" but instead a series of mutable slots which cannot be guaranteed to maintain their value over time---a much more sophisticated semantics which perhaps should force us to call foo an "slot" or an "assignable".

We can also see this as a leaky abstraction. We would like variables to have the standard "fixed but unknown" semantics, but due to the mechanism of stack frames and the behavior of define we do not completely adhere to that meaning.

As a final note, Lisps often give you a form called let which can be used to replicate the previous example without throwing away variable semantics:

(let ((foo 3))
  foo
  (let ((foo 4))
    foo)
  foo)

In this case, the foo on line 2 takes the value 3, the foo on line 4 exists within a different variable context and thus only shadows the foo on line 2... and thus takes the different fixed value 4, finally the foo on line 5 is again identical to the foo on line 2 and takes the same value.

In other words, let allows us to create arbitrary local contexts (coincidentally by creating new stack frames behind the scenes as you might expect). The golden rule which lets us know theses semantics are safe is called, slightly misfortunately, α-conversion. This rule states that if you rename a variable everywhere and uniformly within a single context then the meaning of the program does not change.

Thus the previous example is, by α-conversion, identical in meaning to this one

(let ((foo 3))
  foo
  (let ((bar 4))
    bar)
  foo)

and perhaps slightly less confusing since we no longer need to worry about the effects of shadowing foo.

---

So can we make Lisp's define semantics safer? Kind of. You might imagine the following transformation:

1. Disallow cyclic dependencies in sets of define, e.g. (define x y) (define y x) is disallowed while (define x 3) (define y x) isn't.
2. Move all defines up to the very beginning of any given context (stack frame) and put them in dependency order.
3. Make it an error to "redefine" any variable

It turns out that this transformation is a little tricky (code movement is tough and so can be cyclic dependencies) but if you iron out some small problems you'll see that in any context a variable can only take exactly one fixed-but-unknown value.

You'll also find the following to hold---any program of the following, transformed form

(define x ... definition of x ...)
(define y ... definition of y ...)
(define z ... definition of z ...)
... body ...

is equivalent to the following

(let ((x ... definition of x ...))
  (let ((y ... definition of y ...))
    (let ((z ... definition of z ...))
      ... body ...)))

which is another way of showing that our nice, simple "variable as fixed but unknown quantity" semantics hold.