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

ARRIGHI, PABLO; DÍAZ-CARO, ALEJANDRO; VALIRON, BENOÎT

Electronic Proceedings in Theoretical Computer Science

Open Publishing Association

Año: 2012 vol. 88 p. 1 - 15

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