Modules over relative monads For Syntax and semantics
Benedikt Ahrens · 2011
The goal of this article is to give an algebraic characterisation of the ab-stract syntax of functional programming languages, equipped with reduction rules. We introduce a notion of 2–signature: such a signature specifies not only the terms of a language, but also reduction rules on those terms. To any 2–signature S we associate a category of “models ” of S, and we prove that this category has an initial object. The initial object deserves the name syntax associated to S, and it is equipped with reductions as specified by S. Thus we obtain a characterisation of abstract syntax with reduction rules via a universal property. By construction of the category in question, its initial object is automatically equipped with a substitution operation that is compatible with reduction in a suitable sense. Initiality yields a category–theoretic iteration operator which allows to specify reduction–preserving maps, i.e. translations, on the syntax. The initiality theorem is formalized in the proof assistant Coq, yielding a machinery which, when fed with a 2–signature, provides the associated syntax, certified substitution and the iteration operator. 1 ar