[plt-scheme] PLAI question (closures)

I'm reading PLAI (p. 46) and have come across something that seems a
bit mysterious. Starting with the example

{with {x 3}
  fun {y}
  {+ x y }}}

the text points out that evaluation of f (applied to a value) requires
knowledge of the binding associated with x (which makes sense), and by
analogy with Scheme, I'd expect the binding in effect to the that
introduced by with {x 3} at when the function is defined.

Now, quoting the text:

"The moral is, to properly defer substitution, the value of the
function should be not only its text, but also the substitutions that
were due to be performed on it."

The phrase "the substitutions that were due to be performed on it"
seems rather mysterious to me. But I take it to mean substitutions of
already bound variables (beta reductions?) that could occur given the
bindings in effect at that time, and not (say) a substitution that
might occur for a variable free in the expression being considered, but
possibly bound in a larger expression containing it? Is that right?

My intuitive idea of closures was something like this: In

(\x . x + y ) 3

I can reduce by subsituting 3 for x, but y remains unbound. So, if I
want to maintain something like a symbol table to keep track of
bindings that I can look up at "run time" to facilitate evaluation, the
closure is the expression paired with bindings for its bound variables.
Something like

\x . x + y

paired with

[ x <- 3 ]

(a table with one element.)

I guess I'm just asking whether this is correct. I find the type
definition in the text

(define-type FAE-Value
[numV (number?)]
[closureV (param symbol?)
   (body FAE?)
   (ds DefnSub?)]

hard to follow (because I haven't seen this language spelled out, I
suppose). But in the context of the above example (in my own ad hoc
notation), I take \x . x + y to be body and the "table" [x <- 3] to be
ds. I'm also guessing that FAE? and DefnSub? are type predicates, and
closureV is being defined as the product of the types defined by the
predicates, and that "body" and "ds" are essentially field names.

===
Gregory Woodhouse  <gregory.woodhouse at sbcglobal.net>
"All truth passes through three stages: First, it is ridiculed.
Second, it is violently opposed. Third, it is accepted as
being self-evident."
--Arthur Schopenhauer