基于片类别的一阶仿射归纳数据类型的语义
Semantics for first-order affine inductive data types via slice categories
摘要：
仿射类型系统是子结构类型系统，其中信息的复制受到限制，但在所有类型中允许丢弃信息。这种类型系统非常适合描述量子程序设计语言，因为量子信息的复制违反了量子力学定律。本文考虑了一个具有归纳数据类型的一阶仿射类型系统，并给出了它的一个新的范畴语义.这种解释最具挑战性的方面来自于为我们的数据类型构造适当的丢弃映射的需求，这些数据类型可能是由相互/嵌套递归定义的.我们展示了如何实现这一点，为所有类型的一阶线性类型系统的原子类型是可扩展的模型，然后提出了一个额外的仿射解释的类型内的切片类别的模型与张量单位。我们提出了一些具体的分类模型的语言，从经典的量子。最后，我们讨论了潜在的方法的二元化和扩展我们的方法，并使用它们来解释coalgebraic和懒惰的数据类型。
英文摘要：
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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
