The Vectorial $\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, enabling encoding of matrices and vectors within a strongly normalising, superposable type theory.

Contribution

It presents the first type system for linear-algebraic lambda calculus that captures linear combinations and proves key properties like strong normalization.

Findings

The type system accurately describes linear combinations during reduction.

The calculus is proven to be strongly normalising.

Matrices and vectors can be naturally encoded in the type system.

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.