Semantics for first-order affine inductive data types via slice categories
From MaRDI portal
Publication:2229237
DOI10.1007/978-3-030-57201-3_10zbMATH Open1480.68011arXiv2001.06905OpenAlexW3081905930MaRDI QIDQ2229237FDOQ2229237
Authors: Vladimir Zamdzhiev 
Publication date: 22 February 2021
Abstract: Affine type systems are substructural type systems where copying of information is restricted, but discarding of information is permissible at all types. Such type systems are well-suited for describing quantum programming languages, because copying of quantum information violates the laws of quantum mechanics. In this paper, we consider a first-order affine type system with inductive data types and present a novel categorical semantics for it. The most challenging aspect of this interpretation comes from the requirement to construct appropriate discarding maps for our data types which might be defined by mutual/nested recursion. We show how to achieve this for all types by taking models of a first-order linear type system whose atomic types are discardable and then presenting an additional affine interpretation of types within the slice category of the model with the tensor unit. We present some concrete categorical models for the language ranging from classical to quantum. Finally, we discuss potential ways of dualising and extending our methods and using them for interpreting coalgebraic and lazy data types.
Full work available at URL: https://arxiv.org/abs/2001.06905
Recommendations
- Quantum programming with inductive datatypes: causality and affine type theory
- Strong categorical datatypes II: A term logic for categorical programming
- Semantics for a quantum programming language by operator algebras
- Syntax and semantics of quantitative type theory
- A concrete categorical semantics of lambda-\(\mathcal{S}\)
Quantum computation (81P68) Categorical semantics of formal languages (18C50) Abstract data types; algebraic specification (68Q65)
Cited In (3)
This page was built for publication: Semantics for first-order affine inductive data types via slice categories
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2229237)
