Foundational Semantics of Dynamically Scheduled Attribute Grammar Evaluation

The similarities and differences between attribute grammar systems are obscured by their implementations. A formalism that captures the essence of such systems would allow for equivalence, correctness, and other analyses to be formally framed and proven. We present Saiga, a core language and small-step operational semantics that precisely captures the fundamental concepts of the evaluation of dynamically scheduled attribute grammars. We also present and discuss evaluation semantics for reference, parameterised, cached, and higher order attribute grammars. Saiga’s utility is demonstrated through proofs about the system’s operation, equivalence proofs between distinct Saiga attribute grammar programs, and “step count” comparisons between such programs. The language, semantics and proofs have been mechanised in Lean.