The vectorial λ-calculus

We describe a type system for the linear-algebraic λ-calculus. The type system accounts for the linear-algebraic aspects of this extension of λ-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 origina...

Full description

Saved in:
Bibliographic Details
Published in:Information and computation 2017-06, Vol.254 (1), p.105-139
Main Authors: Arrighi, Pablo, Díaz-Caro, Alejandro, Valiron, Benoît
Format: Article
Language:English
Subjects:
Computer Science
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!
cited_by cdi_FETCH-LOGICAL-c370t-b47d120766794dd59db1c0aaa3c7e83117bd045854d0e1fbd2e94367dd8d7fd33
cites cdi_FETCH-LOGICAL-c370t-b47d120766794dd59db1c0aaa3c7e83117bd045854d0e1fbd2e94367dd8d7fd33
container_end_page 139
container_issue 1
container_start_page 105
container_title Information and computation
container_volume 254
creator Arrighi, Pablo
Díaz-Caro, Alejandro
Valiron, Benoît
description We describe a type system for the linear-algebraic λ-calculus. The type system accounts for the linear-algebraic aspects of this extension of λ-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 λ-calculus is strongly normalising and features weak subject reduction. Finally, we show how to naturally encode matrices and vectors in this typed calculus.
doi_str_mv 10.1016/j.ic.2017.04.001
format article
fullrecord <record><control><sourceid>elsevier_hal_p</sourceid><recordid>TN_cdi_hal_primary_oai_HAL_hal_01785464v1</recordid><sourceformat>XML</sourceformat><sourcesystem>PC</sourcesystem><els_id>S0890540117300482</els_id><sourcerecordid>S0890540117300482</sourcerecordid><originalsourceid>FETCH-LOGICAL-c370t-b47d120766794dd59db1c0aaa3c7e83117bd045854d0e1fbd2e94367dd8d7fd33</originalsourceid><addsrcrecordid>eNp1kMFKxDAQhoMoWFfveturh9aZNk1ab8uirlDwsp5DmknZlGol2S34bL6Dz2SWijdPMwz_N_D9jF0jZAgo7vrMmSwHlBnwDABPWIJQQ5qLEk9ZAlXcSw54zi5C6GMASy4SdrPd2eVkzX70Tg_L76_U6MEchkO4ZGedHoK9-p0L9vr4sF1v0ubl6Xm9alJTSNinLZeEOUghZM2JyppaNKC1Loy0VYEoWwJeViUnsNi1lNuaF0ISVSQ7KooFu53_7vSgPrx70_5TjdqpzapRx1t0irTgE8YszFnjxxC87f4ABHWsQfXKGXWsQQFX0TIi9zNio8PkrFfBOPtuLDkftRWN7n_4Bx7gYoo</addsrcrecordid><sourcetype>Open Access Repository</sourcetype><iscdi>true</iscdi><recordtype>article</recordtype></control><display><type>article</type><title>The vectorial λ-calculus</title><source>ScienceDirect Journals</source><creator>Arrighi, Pablo ; Díaz-Caro, Alejandro ; Valiron, Benoît</creator><creatorcontrib>Arrighi, Pablo ; Díaz-Caro, Alejandro ; Valiron, Benoît</creatorcontrib><description>We describe a type system for the linear-algebraic λ-calculus. The type system accounts for the linear-algebraic aspects of this extension of λ-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 λ-calculus is strongly normalising and features weak subject reduction. Finally, we show how to naturally encode matrices and vectors in this typed calculus.</description><identifier>ISSN: 0890-5401</identifier><identifier>EISSN: 1090-2651</identifier><identifier>DOI: 10.1016/j.ic.2017.04.001</identifier><language>eng</language><publisher>Elsevier Inc</publisher><subject>Computer Science</subject><ispartof>Information and computation, 2017-06, Vol.254 (1), p.105-139</ispartof><rights>2017 Elsevier Inc.</rights><rights>Distributed under a Creative Commons Attribution 4.0 International License</rights><lds50>peer_reviewed</lds50><oa>free_for_read</oa><woscitedreferencessubscribed>false</woscitedreferencessubscribed><citedby>FETCH-LOGICAL-c370t-b47d120766794dd59db1c0aaa3c7e83117bd045854d0e1fbd2e94367dd8d7fd33</citedby><cites>FETCH-LOGICAL-c370t-b47d120766794dd59db1c0aaa3c7e83117bd045854d0e1fbd2e94367dd8d7fd33</cites><orcidid>0000-0002-1008-5605 ; 0000-0002-3535-1009 ; 0000-0002-5175-6882</orcidid></display><links><openurl>$$Topenurl_article</openurl><openurlfulltext>$$Topenurlfull_article</openurlfulltext><thumbnail>$$Tsyndetics_thumb_exl</thumbnail><link.rule.ids>230,314,780,784,885,27924,27925</link.rule.ids><backlink>$$Uhttps://hal.science/hal-01785464$$DView record in HAL$$Hfree_for_read</backlink></links><search><creatorcontrib>Arrighi, Pablo</creatorcontrib><creatorcontrib>Díaz-Caro, Alejandro</creatorcontrib><creatorcontrib>Valiron, Benoît</creatorcontrib><title>The vectorial λ-calculus</title><title>Information and computation</title><description>We describe a type system for the linear-algebraic λ-calculus. The type system accounts for the linear-algebraic aspects of this extension of λ-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 λ-calculus is strongly normalising and features weak subject reduction. Finally, we show how to naturally encode matrices and vectors in this typed calculus.</description><subject>Computer Science</subject><issn>0890-5401</issn><issn>1090-2651</issn><fulltext>true</fulltext><rsrctype>article</rsrctype><creationdate>2017</creationdate><recordtype>article</recordtype><recordid>eNp1kMFKxDAQhoMoWFfveturh9aZNk1ab8uirlDwsp5DmknZlGol2S34bL6Dz2SWijdPMwz_N_D9jF0jZAgo7vrMmSwHlBnwDABPWIJQQ5qLEk9ZAlXcSw54zi5C6GMASy4SdrPd2eVkzX70Tg_L76_U6MEchkO4ZGedHoK9-p0L9vr4sF1v0ubl6Xm9alJTSNinLZeEOUghZM2JyppaNKC1Loy0VYEoWwJeViUnsNi1lNuaF0ISVSQ7KooFu53_7vSgPrx70_5TjdqpzapRx1t0irTgE8YszFnjxxC87f4ABHWsQfXKGXWsQQFX0TIi9zNio8PkrFfBOPtuLDkftRWN7n_4Bx7gYoo</recordid><startdate>201706</startdate><enddate>201706</enddate><creator>Arrighi, Pablo</creator><creator>Díaz-Caro, Alejandro</creator><creator>Valiron, Benoît</creator><general>Elsevier Inc</general><general>Elsevier</general><scope>AAYXX</scope><scope>CITATION</scope><scope>1XC</scope><scope>VOOES</scope><orcidid>https://orcid.org/0000-0002-1008-5605</orcidid><orcidid>https://orcid.org/0000-0002-3535-1009</orcidid><orcidid>https://orcid.org/0000-0002-5175-6882</orcidid></search><sort><creationdate>201706</creationdate><title>The vectorial λ-calculus</title><author>Arrighi, Pablo ; Díaz-Caro, Alejandro ; Valiron, Benoît</author></sort><facets><frbrtype>5</frbrtype><frbrgroupid>cdi_FETCH-LOGICAL-c370t-b47d120766794dd59db1c0aaa3c7e83117bd045854d0e1fbd2e94367dd8d7fd33</frbrgroupid><rsrctype>articles</rsrctype><prefilter>articles</prefilter><language>eng</language><creationdate>2017</creationdate><topic>Computer Science</topic><toplevel>peer_reviewed</toplevel><toplevel>online_resources</toplevel><creatorcontrib>Arrighi, Pablo</creatorcontrib><creatorcontrib>Díaz-Caro, Alejandro</creatorcontrib><creatorcontrib>Valiron, Benoît</creatorcontrib><collection>CrossRef</collection><collection>Hyper Article en Ligne (HAL)</collection><collection>Hyper Article en Ligne (HAL) (Open Access)</collection><jtitle>Information and computation</jtitle></facets><delivery><delcategory>Remote Search Resource</delcategory><fulltext>fulltext</fulltext></delivery><addata><au>Arrighi, Pablo</au><au>Díaz-Caro, Alejandro</au><au>Valiron, Benoît</au><format>journal</format><genre>article</genre><ristype>JOUR</ristype><atitle>The vectorial λ-calculus</atitle><jtitle>Information and computation</jtitle><date>2017-06</date><risdate>2017</risdate><volume>254</volume><issue>1</issue><spage>105</spage><epage>139</epage><pages>105-139</pages><issn>0890-5401</issn><eissn>1090-2651</eissn><abstract>We describe a type system for the linear-algebraic λ-calculus. The type system accounts for the linear-algebraic aspects of this extension of λ-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 λ-calculus is strongly normalising and features weak subject reduction. Finally, we show how to naturally encode matrices and vectors in this typed calculus.</abstract><pub>Elsevier Inc</pub><doi>10.1016/j.ic.2017.04.001</doi><tpages>35</tpages><orcidid>https://orcid.org/0000-0002-1008-5605</orcidid><orcidid>https://orcid.org/0000-0002-3535-1009</orcidid><orcidid>https://orcid.org/0000-0002-5175-6882</orcidid><oa>free_for_read</oa></addata></record>
fulltext fulltext
identifier ISSN: 0890-5401
ispartof Information and computation, 2017-06, Vol.254 (1), p.105-139
issn 0890-5401
1090-2651
language eng
recordid cdi_hal_primary_oai_HAL_hal_01785464v1
source ScienceDirect Journals
subjects Computer Science
title The vectorial λ-calculus
url http://sfxeu10.hosted.exlibrisgroup.com/loughborough?ctx_ver=Z39.88-2004&ctx_enc=info:ofi/enc:UTF-8&ctx_tim=2025-01-03T22%3A31%3A12IST&url_ver=Z39.88-2004&url_ctx_fmt=infofi/fmt:kev:mtx:ctx&rfr_id=info:sid/primo.exlibrisgroup.com:primo3-Article-elsevier_hal_p&rft_val_fmt=info:ofi/fmt:kev:mtx:journal&rft.genre=article&rft.atitle=The%20vectorial%20%CE%BB-calculus&rft.jtitle=Information%20and%20computation&rft.au=Arrighi,%20Pablo&rft.date=2017-06&rft.volume=254&rft.issue=1&rft.spage=105&rft.epage=139&rft.pages=105-139&rft.issn=0890-5401&rft.eissn=1090-2651&rft_id=info:doi/10.1016/j.ic.2017.04.001&rft_dat=%3Celsevier_hal_p%3ES0890540117300482%3C/elsevier_hal_p%3E%3Cgrp_id%3Ecdi_FETCH-LOGICAL-c370t-b47d120766794dd59db1c0aaa3c7e83117bd045854d0e1fbd2e94367dd8d7fd33%3C/grp_id%3E%3Coa%3E%3C/oa%3E%3Curl%3E%3C/url%3E&rft_id=info:oai/&rft_id=info:pmid/&rfr_iscdi=true