Presentable signatures and initial semantics
We present a device for specifying and reasoning about syntax for datatypes, programming languages, and logic calculi. More precisely, we study a notion of "signature" for specifying syntactic constructions. In the spirit of Initial Semantics, we define the "syntax generated by a si...
| Main Authors: | , , , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Logical Methods in Computer Science e.V.
2021-05-01
|
| Series: | Logical Methods in Computer Science |
| Subjects: | |
| Online Access: | https://lmcs.episciences.org/5136/pdf |
| _version_ | 1797268497046175744 |
|---|---|
| author | Benedikt Ahrens André Hirschowitz Ambroise Lafont Marco Maggesi |
| author_facet | Benedikt Ahrens André Hirschowitz Ambroise Lafont Marco Maggesi |
| author_sort | Benedikt Ahrens |
| collection | DOAJ |
| description | We present a device for specifying and reasoning about syntax for datatypes,
programming languages, and logic calculi. More precisely, we study a notion of
"signature" for specifying syntactic constructions.
In the spirit of Initial Semantics, we define the "syntax generated by a
signature" to be the initial object -- if it exists -- in a suitable category
of models. In our framework, the existence of an associated syntax to a
signature is not automatically guaranteed. We identify, via the notion of
presentation of a signature, a large class of signatures that do generate a
syntax.
Our (presentable) signatures subsume classical algebraic signatures (i.e.,
signatures for languages with variable binding, such as the pure lambda
calculus) and extend them to include several other significant examples of
syntactic constructions.
One key feature of our notions of signature, syntax, and presentation is that
they are highly compositional, in the sense that complex examples can be
obtained by gluing simpler ones. Moreover, through the Initial Semantics
approach, our framework provides, beyond the desired algebra of terms, a
well-behaved substitution and the induction and recursion principles associated
to the syntax.
This paper builds upon ideas from a previous attempt by Hirschowitz-Maggesi,
which, in turn, was directly inspired by some earlier work of
Ghani-Uustalu-Hamana and Matthes-Uustalu.
The main results presented in the paper are computer-checked within the
UniMath system. |
| first_indexed | 2024-04-25T01:33:25Z |
| format | Article |
| id | doaj.art-6dee9c3af7944403a8068cd53b861c21 |
| institution | Directory Open Access Journal |
| issn | 1860-5974 |
| language | English |
| last_indexed | 2024-04-25T01:33:25Z |
| publishDate | 2021-05-01 |
| publisher | Logical Methods in Computer Science e.V. |
| record_format | Article |
| series | Logical Methods in Computer Science |
| spelling | doaj.art-6dee9c3af7944403a8068cd53b861c212024-03-08T10:33:57ZengLogical Methods in Computer Science e.V.Logical Methods in Computer Science1860-59742021-05-01Volume 17, Issue 210.23638/LMCS-17(2:17)20215136Presentable signatures and initial semanticsBenedikt AhrensAndré HirschowitzAmbroise LafontMarco MaggesiWe present a device for specifying and reasoning about syntax for datatypes, programming languages, and logic calculi. More precisely, we study a notion of "signature" for specifying syntactic constructions. In the spirit of Initial Semantics, we define the "syntax generated by a signature" to be the initial object -- if it exists -- in a suitable category of models. In our framework, the existence of an associated syntax to a signature is not automatically guaranteed. We identify, via the notion of presentation of a signature, a large class of signatures that do generate a syntax. Our (presentable) signatures subsume classical algebraic signatures (i.e., signatures for languages with variable binding, such as the pure lambda calculus) and extend them to include several other significant examples of syntactic constructions. One key feature of our notions of signature, syntax, and presentation is that they are highly compositional, in the sense that complex examples can be obtained by gluing simpler ones. Moreover, through the Initial Semantics approach, our framework provides, beyond the desired algebra of terms, a well-behaved substitution and the induction and recursion principles associated to the syntax. This paper builds upon ideas from a previous attempt by Hirschowitz-Maggesi, which, in turn, was directly inspired by some earlier work of Ghani-Uustalu-Hamana and Matthes-Uustalu. The main results presented in the paper are computer-checked within the UniMath system.https://lmcs.episciences.org/5136/pdfcomputer science - logic in computer sciencecomputer science - programming languages |
| spellingShingle | Benedikt Ahrens André Hirschowitz Ambroise Lafont Marco Maggesi Presentable signatures and initial semantics Logical Methods in Computer Science computer science - logic in computer science computer science - programming languages |
| title | Presentable signatures and initial semantics |
| title_full | Presentable signatures and initial semantics |
| title_fullStr | Presentable signatures and initial semantics |
| title_full_unstemmed | Presentable signatures and initial semantics |
| title_short | Presentable signatures and initial semantics |
| title_sort | presentable signatures and initial semantics |
| topic | computer science - logic in computer science computer science - programming languages |
| url | https://lmcs.episciences.org/5136/pdf |
| work_keys_str_mv | AT benediktahrens presentablesignaturesandinitialsemantics AT andrehirschowitz presentablesignaturesandinitialsemantics AT ambroiselafont presentablesignaturesandinitialsemantics AT marcomaggesi presentablesignaturesandinitialsemantics |