Initiality for Typed Syntax and Semantics

By Benedikt Ahrens. 2012

17 citations recorded by the source corpus.

We give an algebraic characterization of the syntax and semantics of a class of simply–typed languages, such as the language PCF: we characterize simply–typed binding syntax equipped with reduction rules via a universal property, namely as the initial object of some category. For this purpose, we employ techniques developed in two previous works: in [2], we model syntactic translations between languages over different sets of types as initial morphisms in a category of models. In [1], we characterize untyped syntax with reduction rules as initial object in a category of models. In the present work, we show that those techniques are modular enough to be combined: we thus 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.

Subfields: Artificial Intelligence, Cultural Studies, Language and Linguistics

How researchers see this paper

The researchers whose trusted networks rank it highest, strongest advocate first. Every researcher gets a different order.

In Artificial Intelligence

1. Tarmo Uustalu
2. Thorsten Altenkirch
3. James Chapman
4. Ralph Matthes

In Cultural Studies

1. Tarmo Uustalu
2. Thorsten Altenkirch
3. James Chapman

In Language and Linguistics

1. Tarmo Uustalu
2. Thorsten Altenkirch
3. James Chapman

Citations in the corpus

• Heterogeneous substitution systems revisited (2016, neutral): “…and categories as considered in [7]: in intensional type theory, categories are usually defined to come with a custom equivalence relation on the types of morphisms, which is to be read as equality relation on morphisms, specified for each category individually (see, e.g., [20], [6, Chapter 6]).”
• Monads need not be endofunctors (2010, methodology): “roach leads to new programming structures supporting a greater reusability of concepts and programs. Indeed, relative monads have already been used by Ahrens to model syntax with a reduction relation [3, 4]. Orchard [28] has generalized monads to relative monads in Haskell using constraint kinds and”