论文标题
次结构lambda calculi的计算充足性
Computational Adequacy for Substructural Lambda Calculi
论文作者
论文摘要
诸如Aggine（和线性）类型系统之类的亚结构类型系统是对变量复制（和丢弃）施加限制的类型系统，并且他们发现了包括量子编程在内的计算机科学中的许多应用。我们描述了一种线性和一种仿射类型系统，并为它们都为声音和计算足够的它们制定了抽象的分类模型。我们还在基本假设下还表明，通过单体封闭结构（一种流行的线性类型系统的流行方法）来解释Lambda抽象必须导致逐渐呼叫的仿射类型系统的模型退化和不足的模型。在我们的分类治疗中，明确提出了解决此问题的解决方案。 我们的分类模型比用于研究线性逻辑的线性/非线性模型更通用，我们在逐个价值设置中介绍了线性和仿射类型系统的均匀分类。我们还提供了许多混凝土模型，包括经典和量子的示例。
Substructural type systems, such as affine (and linear) type systems, are type systems which impose restrictions on copying (and discarding) of variables, and they have found many applications in computer science, including quantum programming. We describe one linear and one affine type systems and we formulate abstract categorical models for both of them which are sound and computationally adequate. We also show, under basic assumptions, that interpreting lambda abstractions via a monoidal closed structure (a popular method for linear type systems) necessarily leads to degenerate and inadequate models for call-by-value affine type systems with recursion. In our categorical treatment, a solution to this problem is clearly presented. Our categorical models are more general than linear/non-linear models used to study linear logic and we present a homogeneous categorical account of both linear and affine type systems in a call-by-value setting. We also give examples with many concrete models, including classical and quantum ones.
