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

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 or...

Full description

Saved in:
Bibliographic Details
Published in:Electronic proceedings in theoretical computer science 2012-07, Vol.88 (Proc. DCM 2011), p.1-15
Main Authors: Arrighi, Pablo, Díaz-Caro, Alejandro, Valiron, Benoît
Format: Article
Language:English
Citations: Items that this one cites
Items that cite this one
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary: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.
ISSN:2075-2180
2075-2180
DOI:10.4204/EPTCS.88.1