带原子的标量与向量 μ-演算

The Vectorial Lambda Calculus Revisited

We revisit the Vectorial Lambda Calculus, a typed version of Lineal. Vectorial (as well as Lineal) has been originally designed for quantum computing, as an extension to System F where linear combinations of lambda terms are also terms and linear combinations of types are also types. In its first presentation, Vectorial only provides a weakened version of the Subject Reduction property. We prove that our revised Vectorial Lambda Calculus supports the standard version of said property, answering a long standing issue. In addition we also introduce the concept of weight of types and terms, and p…

向量$λ$ -微积分

The Vectorial $λ$-Calculus

我们描述了线性代数$λ$演算的一个类型系统。类型系统解释了$λ$ -演算的扩展的线性代数方面：它能够静态地描述当减少程序时将获得的项的线性组合。这就产生了一个原始的类型论，在这个理论中，类型可以像项一样叠加成线性组合。我们证明了所得到的类型$λ$ -演算是强正规化的，并具有弱主题约简的特征。最后，我们将展示如何在这种类型的演算中自然地编码矩阵和向量。

线性代数λ演算向量方面的一个类型系统

A Type System for the Vectorial Aspect of the Linear-Algebraic Lambda-Calculus

我们描述了一个类型系统的线性代数λ演算。类型系统解释了语言中模拟线性运算符和向量的部分，也就是说，它能够静态地描述程序归约所产生的项的线性组合。这就产生了一个原始的类型论，在这个理论中，类型可以像项一样叠加成线性组合。我们表明，所得到的类型的λ演算是强规范化和功能弱主题减少。

代数λ-演算的按值调用、按名称调用和向量行为

Call-by-value, call-by-name and the vectorial behaviour of the algebraic λ-calculus

我们研究了代数演算，微分代数演算的一个片段和线性代数代数演算，量子计算的候选代数代数演算之间的关系。这两个演算都是代数的：每一个都配备有加法和标量乘法结构，并且它们的项集合在线性组合下是封闭的。然而，这两种语言是使用不同的方法构建的：前者是按名称调用的语言，而后者是按值调用的语言;前者考虑代数等式，而后者通过重写规则来处理它们。在本文中，我们分析这些不同的方法是如何相互关联的。为此，我们提出了四个规范语言的基础上，每一个可能的选择：调用的名称与调用的值，代数等式与代数重写。我们表明，各种语言相互模拟。由于beta归约和代数重写之间的微妙相互作用，为了使语言保持一致，可能需要一些额外的假设，如融合或规范化。我们仔细设计了每个证明所需的属性，使它们足够通用，对满足相应属性的任何子语言都有效。

类型代数λ演算的语义

Semantics of a Typed Algebraic Lambda-Calculus

代数代数演算已经以各种方式进行了研究，但它们的语义大多未被触及。本文给出了一个具有向量空间结构的一般单型λ演算的语义分析。我们用两个已建立的向量代数演算来描述这种关系。然后我们研究了不动点组合子的加法所引起的问题以及如何修正方程理论来解决这些问题。我们勾勒出一个代数矢量PCF和它可能的指称解释。

模态μ演算中的守护变换

On Guarded Transformation In The Modal Mu-Calculus

保护范式要求μ演算公式中的不动点变量在模态算子的作用域下出现。文献中包含的保护变换有效地将μ演算公式转化为保护范式。我们发现，已知的守护变换可能会导致公式大小的指数爆破，与现有的多项式行为的索赔。我们还证明了对于更宽松的向量形式的μ演算公式，任何多项式保护变换都可以得到奇偶对策的多项式解算法，其存在性是一个公开问题.我们还研究了μ演算，向量形式和层次方程系统之间的转换，这是交替奇偶树自动机的另一种语法。