Lineal: A linear-algebraic Lambda-calculus

Abstract

We provide a computational definition of the notions of vector space and bilinear functions. We use this result to introduce a minimal language combining higher-order computation and linear algebra. This language extends the Lambda-calculus with the possibility to make arbitrary linear combinations of terms alpha.t + beta.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 the field of quantum computation, whose circuits we show can be easily encoded in the calculus. Finally, we prove the confluence of the entire calculus.

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

References in corpus (9)

• Quantum correlations with no causal order
• A Lambda Calculus for Quantum Computation
• State Transfer instead of Teleportation in Measurement-based Quantum Computation
• Quantum entanglement analysis based on abstract interpretation
• A 2 rebit gate universal for quantum computing
• An Algebra of Pure Quantum Programming
• Quantum Computation, Categorical Semantics and Linear Logic
• A logical analysis of entanglement and separability in quantum higher-order functions
• Linear-algebraic lambda-calculus

Cited by in corpus (18)

• Qunity: A Unified Language for Quantum and Classical Computing (Extended Version)
• The Vectorial $\lambda$-Calculus
• Two linearities for quantum computing in the lambda calculus
• A New Connective in Natural Deduction, and its Application to Quantum Computing
• Quantum Control in the Unitary Sphere: Lambda-S1 and its Categorical Model
• A linear linear lambda-calculus
• A concrete model for a typed linear algebraic lambda calculus
• Automating Equational Proofs in Dirac Notation
• A lambda calculus for density matrices with classical and probabilistic controls
• Exponentials as Substitutions and the Cost of Cut Elimination in Linear Logic
• From Symmetric Pattern-Matching to Quantum Control (Extended Version)
• Polymorphic System I
• Towards a Computational Quantum Logic: An Overview of an Ongoing Research Program
• The Vectorial Lambda Calculus Revisited
• Extensional proofs in a propositional logic modulo isomorphisms
• IMALL with a Mixed-State Modality: A Logical Approach to Quantum Computation
• A Quick Overview on the Quantum Control Approach to the Lambda Calculus
• A Quantum-Control Lambda-Calculus with Multiple Measurement Bases