线性代数lambda演算

着眼于量子计算模型及/或线性逻辑的解释，我们定义了一种函数式语言，其中所有函数依构造皆为线性算子。以项重写系统的形式给出了该语言的小步操作语义（从而也是一个解释器/模拟器）。由此构造的线性代数 lambda-演算在一种不同（但相关）的意义上是线性的，不同于例如线性 lambda-演算中的线性。在量子编程语言的语境下讨论了这些不同的线性概念。关键词：量子 lambda-演算，线性 lambda-演算，$\lambda$-演算，量子逻辑。