Initial Semantics for Strengthened Signatures
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 sens...
Main Authors: | , |
---|---|
Format: | Article |
Language: | English |
Published: |
Open Publishing Association
2012-02-01
|
Series: | Electronic Proceedings in Theoretical Computer Science |
Online Access: | http://arxiv.org/pdf/1202.3499v1 |
id |
doaj-07906182604c4985a08f8b590ab67bfc |
---|---|
record_format |
Article |
spelling |
doaj-07906182604c4985a08f8b590ab67bfc2020-11-24T22:08:36ZengOpen Publishing AssociationElectronic Proceedings in Theoretical Computer Science2075-21802012-02-0177Proc. FICS 2012313810.4204/EPTCS.77.5Initial Semantics for Strengthened SignaturesAndré HirschowitzMarco MaggesiWe 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. http://arxiv.org/pdf/1202.3499v1 |
collection |
DOAJ |
language |
English |
format |
Article |
sources |
DOAJ |
author |
André Hirschowitz Marco Maggesi |
spellingShingle |
André Hirschowitz Marco Maggesi Initial Semantics for Strengthened Signatures Electronic Proceedings in Theoretical Computer Science |
author_facet |
André Hirschowitz Marco Maggesi |
author_sort |
André Hirschowitz |
title |
Initial Semantics for Strengthened Signatures |
title_short |
Initial Semantics for Strengthened Signatures |
title_full |
Initial Semantics for Strengthened Signatures |
title_fullStr |
Initial Semantics for Strengthened Signatures |
title_full_unstemmed |
Initial Semantics for Strengthened Signatures |
title_sort |
initial semantics for strengthened signatures |
publisher |
Open Publishing Association |
series |
Electronic Proceedings in Theoretical Computer Science |
issn |
2075-2180 |
publishDate |
2012-02-01 |
description |
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. |
url |
http://arxiv.org/pdf/1202.3499v1 |
work_keys_str_mv |
AT andrehirschowitz initialsemanticsforstrengthenedsignatures AT marcomaggesi initialsemanticsforstrengthenedsignatures |
_version_ |
1725815760238936064 |