The purpose of binding-time analysis is to factor the program into the generating extension and the residual code. The analysis is described here as an abstract interpretation [NN?], with binding times as abstract values. It may be more efficient to implement as a type inference [Henglein91].

The analysis starts with a root language code structure and the binding times of its arguments. The simplest binding times are static (S) and dynamic (D). Static arguments are available to the generated compiler, and are thus considered `program'; dynamic arguments appear as arguments to the code returned by the compiler.

Since there are no infinite ascending chains in the binding-time lattice, termination of cogen is guaranteed.

The set of binding times (the lattice) is described in five steps, each elaborates the previous in order to capture more static information.

1. simple
2. pairs
3. first-order jumps and constants
4. higher order jumps
5. spines

The final, formal definition of the binding times:

bt ::= S | D | (cons bt bt cp is-clo is-sure) | (const v)
cp ::= instruction
is-clo ::= boolean
is-sure ::= boolean
v ::= any-value

I haven't finished the formal definition of the ordering of the lattice. Here's a first approximation:

(const v) < S < (cons a d ...) < D
(cons a1 d1 cp1 ...) <= (cons a2 d2 cp2 ...) <==>
    a1 <= a2 and d1 <= d2 and cp1 = cp2