The Vectorial Lambda Calculus Revisited

TL;DR

This paper revisits the Vectorial Lambda Calculus, a typed extension of Lineal designed for quantum computing, proving it supports standard Subject Reduction and introducing the concept of weight for types and terms.

Contribution

It provides a revised version of Vectorial Lambda Calculus supporting standard Subject Reduction and introduces the concept of weight for types and terms.

Findings

Supports standard Subject Reduction property

Introduces weight of types and terms

Establishes relation between weight of terms and types

Abstract

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.