Initial Semantics for Reduction Rules
We give an algebraic characterization of the syntax and operational semantics of a class of simply-typed languages, such as the language PCF: we characterize simply-typed syntax with variable binding and equipped with reduction rules via a universal property, namely as the initial object of some cat...
| Main Author: | |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Logical Methods in Computer Science e.V.
2019-03-01
|
| Series: | Logical Methods in Computer Science |
| Subjects: | |
| Online Access: | https://lmcs.episciences.org/5027/pdf |
| _version_ | 1797268579272359936 |
|---|---|
| author | Benedikt Ahrens |
| author_facet | Benedikt Ahrens |
| author_sort | Benedikt Ahrens |
| collection | DOAJ |
| description | We give an algebraic characterization of the syntax and operational semantics
of a class of simply-typed languages, such as the language PCF: we characterize
simply-typed syntax with variable binding and equipped with reduction rules via
a universal property, namely as the initial object of some category of models.
For this purpose, we employ techniques developed in two previous works: in the
first work we model syntactic translations between languages over different
sets of types as initial morphisms in a category of models. In the second work
we characterize untyped syntax with reduction rules as initial object in a
category of models. In the present work, we combine the techniques used earlier
in order to characterize simply-typed syntax with reduction rules as initial
object in a category. The universal property yields an operator which allows to
specify translations---that are semantically faithful by construction---between
languages over possibly different sets of types.
As an example, we upgrade a translation from PCF to the untyped lambda
calculus, given in previous work, to account for reduction in the source and
target. Specifically, we specify a reduction semantics in the source and target
language through suitable rules. By equipping the untyped lambda calculus with
the structure of a model of PCF, initiality yields a translation from PCF to
the lambda calculus, that is faithful with respect to the reduction semantics
specified by the rules.
This paper is an extended version of an article published in the proceedings
of WoLLIC 2012. |
| first_indexed | 2024-04-25T01:34:43Z |
| format | Article |
| id | doaj.art-a45c5e5442964a4c976c111dec5174c5 |
| institution | Directory Open Access Journal |
| issn | 1860-5974 |
| language | English |
| last_indexed | 2024-04-25T01:34:43Z |
| publishDate | 2019-03-01 |
| publisher | Logical Methods in Computer Science e.V. |
| record_format | Article |
| series | Logical Methods in Computer Science |
| spelling | doaj.art-a45c5e5442964a4c976c111dec5174c52024-03-08T10:27:56ZengLogical Methods in Computer Science e.V.Logical Methods in Computer Science1860-59742019-03-01Volume 15, Issue 110.23638/LMCS-15(1:28)20195027Initial Semantics for Reduction RulesBenedikt AhrensWe give an algebraic characterization of the syntax and operational semantics of a class of simply-typed languages, such as the language PCF: we characterize simply-typed syntax with variable binding and equipped with reduction rules via a universal property, namely as the initial object of some category of models. For this purpose, we employ techniques developed in two previous works: in the first work we model syntactic translations between languages over different sets of types as initial morphisms in a category of models. In the second work we characterize untyped syntax with reduction rules as initial object in a category of models. In the present work, we combine the techniques used earlier in order to characterize simply-typed syntax with reduction rules as initial object in a category. The universal property yields an operator which allows to specify translations---that are semantically faithful by construction---between languages over possibly different sets of types. As an example, we upgrade a translation from PCF to the untyped lambda calculus, given in previous work, to account for reduction in the source and target. Specifically, we specify a reduction semantics in the source and target language through suitable rules. By equipping the untyped lambda calculus with the structure of a model of PCF, initiality yields a translation from PCF to the lambda calculus, that is faithful with respect to the reduction semantics specified by the rules. This paper is an extended version of an article published in the proceedings of WoLLIC 2012.https://lmcs.episciences.org/5027/pdfmathematics - logiccomputer science - logic in computer sciencef.3.2f.4.3 |
| spellingShingle | Benedikt Ahrens Initial Semantics for Reduction Rules Logical Methods in Computer Science mathematics - logic computer science - logic in computer science f.3.2 f.4.3 |
| title | Initial Semantics for Reduction Rules |
| title_full | Initial Semantics for Reduction Rules |
| title_fullStr | Initial Semantics for Reduction Rules |
| title_full_unstemmed | Initial Semantics for Reduction Rules |
| title_short | Initial Semantics for Reduction Rules |
| title_sort | initial semantics for reduction rules |
| topic | mathematics - logic computer science - logic in computer science f.3.2 f.4.3 |
| url | https://lmcs.episciences.org/5027/pdf |
| work_keys_str_mv | AT benediktahrens initialsemanticsforreductionrules |