Benedikt Ahrens - Extended Initiality for Typed Abstract Syntax

lmcs:1193 - Logical Methods in Computer Science, April 6, 2012, Volume 8, Issue 2 -
Extended Initiality for Typed Abstract Syntax

Authors: Benedikt Ahrens

Initial Semantics aims at interpreting the syntax associated to a signature as the initial object of some category of 'models', yielding induction and recursion principles for abstract syntax. Zsidó proves an initiality result for simply-typed syntax: given a signature S, the abstract syntax associated to S constitutes the initial object in a category of models of S in monads. However, the iteration principle her theorem provides only accounts for translations between two languages over a fixed set of object types. We generalize Zsidó's notion of model such that object types may vary, yielding a larger category, while preserving initiality of the syntax therein. Thus we obtain an extended initiality theorem for typed abstract syntax, in which translations between terms over different types can be specified via the associated category-theoretic iteration operator as an initial morphism. Our definitions ensure that translations specified via initiality are type-safe, i.e. compatible with the typing in the source and target language in the obvious sense. Our main example is given via the propositions-as-types paradigm: we specify propositions and inference rules of classical and intuitionistic propositional logics through their respective typed signatures. Afterwards we use the category--theoretic iteration operator to specify a double negation translation from the former to the latter. A second example is given by the signature of PCF. For this particular case, we formalize the theorem in the proof assistant Coq. Afterwards we specify, via the category-theoretic iteration operator, translations from PCF to the untyped lambda calculus.

Volume: Volume 8, Issue 2
Published on: April 6, 2012
Submitted on: July 14, 2011
Keywords: Computer Science - Logic in Computer Science,Computer Science - Programming Languages,D.3.1, F.4.3


Consultation statistics

This page has been seen 241 times.
This article's PDF has been downloaded 197 times.