Simple

The simplest BT lattice has just two elements:

bt ::= S | D

dynamic is top, static is bottom (S < D).

Say we are analyzing

(prim r + a b)

In abstract interpretation, the value assigned to r is the abstraction of the + primop (denoted $\\tilde{+}$ ) applied to the values of a and b in the analysis environment.

In my BTA the abstraction of all the generic primops is the same: if any argument is not S then the result is D. Call this function $\\widetilde{prim}$ . Thus if any argument is unknown at compile time, then the prim must be delayed until runtime.