Lineal：一种线性代数 Lambda 演算
量子物理
2019-03-14 v6 计算机科学中的逻辑
编程语言
摘要
我们给出向量空间和双线性函数概念的计算定义。我们利用该结果引入一种结合高阶计算与线性代数的极简语言。该语言扩展了 Lambda 演算，使得能够进行任意项 alpha.t + beta.u 的线性组合。我们描述了如何通过少量重写规则来“执行”此语言，并通过该语言须为线性算子语言且为高阶的两条基本要求来证明其合理性。我们提及本工作在量子计算领域的远景，其电路可被轻易编码于此演算中。最后，我们证明了整个演算的合流性。
引用
@article{arxiv.quant-ph/0612199,
title = {Lineal: A linear-algebraic Lambda-calculus},
author = {Pablo Arrighi and Gilles Dowek},
journal= {arXiv preprint arXiv:quant-ph/0612199},
year = {2019}
}
备注
The complementary note "On the critical pairs of a rewrite system for vector spaces" is provided in the source files. Short version : "Linear-algebraic Lambda-calculus : higher-order and confluence", Proceedings of RTA 08, Hagenberg, July 2008. LNCS 5117, 17, (2008). Long version : LMCS