Initial Semantics for Strengthened Signatures

André Hirschowitz
(Laboratoire J.-A. Dieudonné, Université de Nice - Sophia Antipolis)
Marco Maggesi
(Dipartimento di Matematica "U. Dini", Università degli Studi di Firenze)

We give a new general definition of arity, yielding the companion notions of signature and associated syntax. This setting is modular in the sense requested by Ghani and Uustalu: merging two extensions of syntax corresponds to building an amalgamated sum. These signatures are too general in the sense that we are not able to prove the existence of an associated syntax in this general context. So we have to select arities and signatures for which there exists the desired initial monad. For this, we follow a track opened by Matthes and Uustalu: we introduce a notion of strengthened arity and prove that the corresponding signatures have initial semantics (i.e. associated syntax). Our strengthened arities admit colimits, which allows the treatment of the λ-calculus with explicit substitution.

In Dale Miller and Zoltán Ésik: Proceedings 8th Workshop on Fixed Points in Computer Science (FICS 2012), Tallinn, Estonia, 24th March 2012, Electronic Proceedings in Theoretical Computer Science 77, pp. 31–38.
Published: 14th February 2012.

ArXived at: bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to:
For website issues: