A Type System for the Vectorial Aspect of the Linear-Algebraic Lambda-Calculus

TL;DR

This paper introduces a novel type system for the linear-algebraic lambda-calculus that can statically describe linear combinations of terms, ensuring strong normalization and weak subject-reduction.

Contribution

It presents an original type theory where types can be superposed into linear combinations, capturing the vectorial aspect of the language.

Findings

The type system accurately models linear combinations of terms.

The calculus is proven to be strongly normalizing.

It exhibits weak subject-reduction.

Abstract

We describe a type system for the linear-algebraic lambda-calculus. The type system accounts for the part of the language emulating linear operators and vectors, i.e. it is able to statically describe the linear combinations of terms resulting from the reduction of programs. This gives rise to an original type theory where types, in the same way as terms, can be superposed into linear combinations. We show that the resulting typed lambda-calculus is strongly normalizing and features a weak subject-reduction.