2020/07/07 by Francisco Noriega, Noriega, Francisco, Alejandro Díaz-Caro +1
Computer Science · #Computability, Logic, AI Algorithms #FOS: Computer and information sciences #Logic in Computer Science (cs.LO) #Polynomial and algebraic computation #Quantum Computing Algorithms and Architecture
paper · doi:10.48550/arxiv.2007.03648
openalex publication_date 2020/07/07 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
We revisit the Vectorial Lambda Calculus, a typed version of Lineal. Vectorial (as well as Lineal) has been originally designed for quantum computing, as an extension to System F where linear combinations of lambda terms are also terms and linear combinations of types are also types. In its first presentation, Vectorial only provides a weakened version of the Subject Reduction property. We prove that our revised Vectorial Lambda Calculus supports the standard version of said property, answering a long standing issue. In addition we also introduce the concept of weight of types and terms, and prove a relation between the weight of terms and of its types.