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

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

Bibliographic Details
Main Authors: Pablo Arrighi, Alejandro Díaz-Caro, Benoît Valiron
Format: Article
Language:English
Published: Open Publishing Association 2012-07-01
Series:Electronic Proceedings in Theoretical Computer Science
Online Access:http://arxiv.org/pdf/1012.4032v4
id doaj-c49df8d48e134ea8a36ef1f2f4293c4f
record_format Article
spelling doaj-c49df8d48e134ea8a36ef1f2f4293c4f2020-11-24T20:41:32ZengOpen Publishing AssociationElectronic Proceedings in Theoretical Computer Science2075-21802012-07-0188Proc. DCM 201111510.4204/EPTCS.88.1A Type System for the Vectorial Aspect of the Linear-Algebraic Lambda-CalculusPablo ArrighiAlejandro Díaz-CaroBenoît ValironWe 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.http://arxiv.org/pdf/1012.4032v4
collection DOAJ
language English
format Article
sources DOAJ
author Pablo Arrighi
Alejandro Díaz-Caro
Benoît Valiron
spellingShingle Pablo Arrighi
Alejandro Díaz-Caro
Benoît Valiron
A Type System for the Vectorial Aspect of the Linear-Algebraic Lambda-Calculus
Electronic Proceedings in Theoretical Computer Science
author_facet Pablo Arrighi
Alejandro Díaz-Caro
Benoît Valiron
author_sort Pablo Arrighi
title A Type System for the Vectorial Aspect of the Linear-Algebraic Lambda-Calculus
title_short A Type System for the Vectorial Aspect of the Linear-Algebraic Lambda-Calculus
title_full A Type System for the Vectorial Aspect of the Linear-Algebraic Lambda-Calculus
title_fullStr A Type System for the Vectorial Aspect of the Linear-Algebraic Lambda-Calculus
title_full_unstemmed A Type System for the Vectorial Aspect of the Linear-Algebraic Lambda-Calculus
title_sort type system for the vectorial aspect of the linear-algebraic lambda-calculus
publisher Open Publishing Association
series Electronic Proceedings in Theoretical Computer Science
issn 2075-2180
publishDate 2012-07-01
description 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.
url http://arxiv.org/pdf/1012.4032v4
work_keys_str_mv AT pabloarrighi atypesystemforthevectorialaspectofthelinearalgebraiclambdacalculus
AT alejandrodiazcaro atypesystemforthevectorialaspectofthelinearalgebraiclambdacalculus
AT benoitvaliron atypesystemforthevectorialaspectofthelinearalgebraiclambdacalculus
AT pabloarrighi typesystemforthevectorialaspectofthelinearalgebraiclambdacalculus
AT alejandrodiazcaro typesystemforthevectorialaspectofthelinearalgebraiclambdacalculus
AT benoitvaliron typesystemforthevectorialaspectofthelinearalgebraiclambdacalculus
_version_ 1716824782955085824

Similar Items