The Vectorial Lambda Calculus Revisited
share
We revisit the Vectorial Lambda Calculus, a typed version of Lineal. Vectorial (as well as Lineal) was originally meant 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. 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.
READ FULL TEXT