Ahrens, Benedikt - Initial Semantics for Reduction Rules

lmcs:5027 - Logical Methods in Computer Science, March 21, 2019, Volume 15, Issue 1
Initial Semantics for Reduction Rules

Authors: Ahrens, Benedikt

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.


Source : oai:arXiv.org:1212.5668
DOI : 10.23638/LMCS-15(1:28)2019
Volume: Volume 15, Issue 1
Published on: March 21, 2019
Submitted on: December 11, 2018
Keywords: Mathematics - Logic,Computer Science - Logic in Computer Science,F.3.2,F.4.3


Share