Reading AI Model Compilation in MLIR Through the Lens of Formal Theories

The problem is that MLIR's design principles, such as match-and-rewrite and staged lowering, are typically derived from engineering intuition rather than formal theory. The method involves mapping these principles to established formal theories, including term-rewriting systems, refinement calculus, and abstract interpretation. The abstract does not disclose experimental results, as it is a conceptual argument rather than an empirical study. This matters because formal theories provide precise vocabulary for evaluating abstraction completeness and ideal design, which becomes critical as coding agents automate implementation but rely on well-structured semantics.