Linear-algebraic Lambda-calculus: higher-order, encodings and confluence
Pablo Arrighi, Gilles Dowek · arXiv (Cornell University) · 2006
We introduce a minimal language combining both higher-order computation and linear algebra. Roughly, this is nothing else than the Lambda-calculus together with the possibility to make linear combinations of terms a.t+b.u. We describe how to "execute" this language in terms of a few rewrite rules, and justify them through the two fundamental requirements that the language be a language of linear operators, and that it be higher-order. We mention the perspectives of this work in field of quantum computation, which we show can be easily encoded in the calculus, as well as in other domains such as the interpretation of linear logic. Finally we prove the confluence of the calculus, this is our main result. Keywords: quantum programming language, quantum control, quantum logic, probabilistic and quantitative analysis, rewriting techniques.