INVESTIGADORES
DÍAZ CARO Alejandro
artículos
Título:
The vectorial lambda-calculus
Autor/es:
PABLO ARRIGHI; ALEJANDRO DÍAZ CARO; BENOÎT VALIRON
Revista:
Information and Computation
Editorial:
ACADEMIC PRESS INC ELSEVIER SCIENCE
Referencias:
Año: 2017 vol. 254 p. 105 - 139
ISSN:
0890-5401
Resumen:
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 a weak subject reduction. Finally, we show how to naturally encode matrices and vectors in this typed calculus.
