Epistemic Intermediate Representations: Contract-Bounded Capability Lowering over an Invariant Data Definition
Compiler intermediate representations (IRs) are traditionally organized around representations: a sequence of languages and transformations rewriting programs from one language to the next. Under this paradigm, the loss of high-level semantic information during lowering occurs as an implicit side effect of rewriting; it is nowhere recorded, leaving the compiler incapable of reporting what it has discarded, where, or why. We propose an alternative foundational abstraction: program knowledge. Throughout compilation, the program resides within a single, invariant data definition. At any stage, it carries an explicit set of capability classes—semantic properties the program is permitted to exploit, such as generic abstraction, logical aggregates, structured control flow, or a logical calling convention. Program knowledge changes strictly via lowering contracts of the form κ' = (κ \ F) ∪ I ⊆ ceil*(d', b'). In such a contract, every discarded class is accompanied by an explicit rationale and a declared preservation status. A contract that would drop a capability without explicitly declaring it is rejected at the time of its declaration. Backends are not consumers of a fixed terminal language; rather, they are observers that declare their required knowledge and admit a program at the stage along the lowering pipeline where that knowledge still exists. We formalize this model, prove the containment invariant and the traceability property (no loss of knowledge occurs without a declared contract and rationale), and show how this approach reduces the M × N frontend–backend problem to a single contract graph with N branching points. Finally, we contrast our model with Nanopass, MLIR dialect conversion, and type-preserving compilation.
Authors
- Daniel Maov
Publication Details
- Journal
- Zenodo (CERN European Organization for Nuclear Research)
- Published
- 2026-09-29
- DOI
- https://doi.org/10.5281/zenodo.23029124
- Primary Topic
- Logic, programming, and type systems
- Type
- preprint