How are Scheme closures formally defined?

Solution 1:

I don't think it's helpful, today, to think of closures as some special magic thing: long ago in languages in the prehistory of Scheme they were, but in modern languages they are not a special thing at all: they just follow from the semantics of the language in an obvious way.

The two important things (these are both quotes from R7RS, both from section 1.1 are these:

Scheme is a statically scoped programming language. Each use of a variable is associated with a lexically apparent binding of that variable.

and

All objects created in the course of a Scheme computation, including procedures and continuations, have unlimited extent.

What this means is that Scheme is a language with lexical scope and indefinite extent: any variable binding exists for as long as there is possibility of reference. And, conveniently, you can always tell statically (ie by reading the code) what bindings a bit of code may refer to.

And the important thing here is that these rules are absurdly simple: there are no weird special cases. If a reference to a variable binding is visible in a bit of code, which you can tell by looking at the code, then it is visible. It's not visible only sometimes, or only during some interval, or only if the Moon is gibbous: it's visible.

But the implication of the rules is that procedures, somehow, need to remember all the bindings that they reference or may reference and which were in scope when they were created. Because scope is static it is always possible to determine which bindings are in scope (disclaimer: I'm not sure how this works formally for global bindings).

So then the very old-fashioned definition of a closure would be a procedure defined in a scope in which bindings to which it refers exist. This would be a closure:

(define x
  (let ((y 1))
    (λ (z)
      (set! y (+ y z))
      y)))

And this procedure would return a closure:

(define make-incrementor
  (λ (val)
    (λ ()
      (let ((v val))
        (set! val (+ val 1))
        v))))

But you can see that in both cases the behaviour of these things just follows immediately from the scope and extent rules of the language: there's no special 'this is a closure' rule.

In the first case the function which ends up as the value of x both refers to and mutates the binding of y as well as referring to the binding of z established when it was called.

In the second case, calling make-incrementor establishes a binding for val, which binding is then referred to and mutated by the function that it returns.

I'm never sure if it helps to understand things to turn all the lets into λs, but the second thing turns into

(define make-incrementor
  (λ (val)
    (λ ()
      ((λ (v)
         (set! val (+ val 1))
         v)
       val))))

And you can see now that the function returned by make-incrementor, when called, now immediately calls another function which binds v solely to its argument, which itself is the value of the binding established by make-incrementor: it's doing this simply to keep hold of the pre-increment value of that binding of course.

Again, the rules are simple: you can just look at the code and see what it does. There is no special 'closure' case.

If you actually do want the formal semantics that gives rise to this, then 7.2 of R7RS has the formal semantics of the language.

Solution 2:

A closure is a pair of a pointer to some code and a pointer to the environment the code should be evaluated in, which is the same as the environment the closure was created in.

The presence of closures in the language makes the environment look like a tree. Without closures the environment is like a stack. This is how the environment was in the first lisp systems. Stallman stated he chose dynamic environment in elisp because the static environment was hard to understand at the time (1986).

The closures are one of the most central concepts of computation and they allow the derivation of many other concepts like coroutines, fibers, continuations, threads, thunks to delay, etc etc.