The Vectorial $\lambda$-Calculus

Abstract

We describe a type system for the linear-algebraic $\lambda$-calculus. The type system accounts for the linear-algebraic aspects of this extension of $\lambda$-calculus: it is able to statically describe the linear combinations of terms that will be obtained when reducing the programs. This gives rise to an original type theory where types, in the same way as terms, can be superposed into linear combinations. We prove that the resulting typed $\lambda$-calculus is strongly normalising and features weak subject reduction. Finally, we show how to naturally encode matrices and vectors in this typed calculus.

Long and corrected version of arXiv:1012.4032 (EPTCS 88:1-15), to appear in Information and Computation

References in corpus (6)

• A Lambda Calculus for Quantum Computation
• Non-idempotent intersection types and strong normalisation
• Two linearities for quantum computing in the lambda calculus
• Bounding normalization time through intersection types
• Call-by-value non-determinism in a linear logic type discipline
• The probability of non-confluent systems

Cited by in corpus (15)

• Two linearities for quantum computing in the lambda calculus
• Realizability in the Unitary Sphere
• Quantum Control Machine: The Limits of Control Flow in Quantum Programming
• A linear linear lambda-calculus
• A concrete model for a typed linear algebraic lambda calculus
• A lambda calculus for density matrices with classical and probabilistic controls
• The Sup Connective in IMALL: A Categorical Semantics
• The probability of non-confluent systems
• A linear proof language for second-order intuitionistic linear logic
• Polymorphic System I
• From Symmetric Pattern-Matching to Quantum Control (Extended Version)
• The Vectorial Lambda Calculus Revisited
• Extensional proofs in a propositional logic modulo isomorphisms
• A Quick Overview on the Quantum Control Approach to the Lambda Calculus
• An Algebraic Extension of Intuitionistic Linear Logic: The $L_{!}^S$-Calculus and Its Categorical Model