Computer Science – Logic in Computer Science
Scientific paper
2011-07-26
Computer Science
Logic in Computer Science
compared to v1: - Abstract and Introduction completely rewritten - Addition of examples and remarks in Secs. 1 and 2 - Sec 3 n
Scientific paper
The goal of this article is to give an algebraic characterization of the abstract syntax of functional programming languages, equipped with reduction rules. We introduce a notion of \emph{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 \emph{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 \emph{substitution} operation that is compatible with reduction in a suitable sense. Initiality yields a category--theoretic \emph{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.
No associations
LandOfFree
Modules over relative monads for syntax and semantics does not yet have a rating. At this time, there are no reviews or comments for this scientific paper.
If you have personal experience with Modules over relative monads for syntax and semantics, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and Modules over relative monads for syntax and semantics will most certainly appreciate the feedback.
Profile ID: LFWR-SCP-O-94007