Ahrens, Benedikt - 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: Ahrens, Benedikt

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\'o 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\'o'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.


Source : oai:arXiv.org:1107.4751
DOI : 10.2168/LMCS-8(2:1)2012
Volume: Volume 8, Issue 2
Published on: April 6, 2012
Submitted on: June 25, 2015
Keywords: Computer Science - Logic in Computer Science,Computer Science - Programming Languages,D.3.1, F.4.3


Share

Browsing statistics

This page has been seen 18 times.
This article's PDF has been downloaded 9 times.