WG211/M24Carette

Partial evaluation works by leveraging what is *static* in a given situation, namely the program itself and part of its input. The Futamura projections go further. For the first projection, one considers not just the program, but its interpreter to also be *static*. Such a view corresponds to taking that language's operational semantics and reifying it as concrete code - which might be a lossy operation. The further projections require the specializer itself to be considered static.

There are many invariants that may well be true and known about a language which can be witnessed on a case-by-case basis via interpretation, but not *in general*, since language interpreters are rarely symbolic. Simply put: a language that implements addition over the integers likely will not have 'commutativity' as something readily apparent in its interpreter, or even its operational semantics.

A good denotational semantics reified as an equational theory, on the other hand, would contain such equations (i.e. commutativity). So rather than reifying a language via its interpreter, why not take as static input a representation of the equational theory of a language? This would let us witness many more invariants, which we've learned is quite beneficial for writing better specializers.