definition of lexical closure

[PGS%MIT-OZ@MIT-MC.ARPA]

I was talking to someone today about the Common Lisp notion of a closure, and
I noticed that the definition of a lexical closure on page 87 of the CL
manual is sort of vague and unsatisfactory.  It says that a lexical closure
is the object returned by FUNCTION, that is, a function which, when invoked,
obeys the rules for lexical scoping.

The problem with this definition is that it makes it difficult to explain why
the thing referred to is called a closure.  It's hard to relate the definition
even vaguely to the set-theoretic notion of a closure, because it doesn't
describe a set, so one can't explain the term as coming from the notion of
`closing over' a set of bindings.

If you say that the reason why lexical closures are functions in Common Lisp,
and not just sets of bindings, is because there is this sense of a closure
not only of the bindings in the definition environment, but of the bindings
of the formals to the actuals in the invocation of a function, you create
this other pedagogical problem, which is that the thing returned by FUNCTION
isn't a lexical closure then, because it can't include the bindings created
by function invocation, because those bindings are created afresh whenever
the function is invoked, and don't even exist when the object is returned.

It was easier to explain what a Lisp Machine Lisp closure was, because there
was an idea that a closure existed as something separate from a function.  One
could do more than invoke the closure's function; there were things like
SYMEVAL-IN-CLOSURE, for example.  So a closure could be explained as a set of
bindings, which is much more palatable than saying that it is a function.

Those were sets of dynamic bindings.  What I would like to say to people who
ask what a lexical closure is in Common Lisp is that it is a set of lexical
bindings; that is, the set of lexical bindings in the environment in which a
function is defined.  Then we could say that FUNCTION returns, not a lexical
closure, but an object that includes a lexical closure, and that the
environment in which the function text is evaluated is the union of that
lexical closure with the bindings of the formals to the actuals.

I'd like to see this definition in a future edition of the CL manual, on the
grounds that it's cleaner and therefore easier to teach.  Would anyone object?