{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,5]],"date-time":"2025-10-05T04:13:41Z","timestamp":1759637621303,"version":"3.41.2"},"reference-count":36,"publisher":"Centre pour la Communication Scientifique Directe (CCSD)","license":[{"start":{"date-parts":[[2012,2,27]],"date-time":"2012-02-27T00:00:00Z","timestamp":1330300800000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/arxiv.org\/licenses\/nonexclusive-distrib\/1.0"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"abstract":"<jats:p>The Algebraic lambda-calculus and the Linear-Algebraic lambda-calculus extend the lambda-calculus with the possibility of making arbitrary linear combinations of terms. In this paper we provide a fine-grained, System F-like type system for the linear-algebraic lambda-calculus. We show that this \"scalar\" type system enjoys both the subject-reduction property and the strong-normalisation property, our main technical results. The latter yields a significant simplification of the linear-algebraic lambda-calculus itself, by removing the need for some restrictions in its reduction rules. But the more important, original feature of this scalar type system is that it keeps track of 'the amount of a type' that is present in each term. As an example of its use, we shown that it can serve as a guarantee that the normal form of a term is barycentric, i.e that its scalars are summing to one.<\/jats:p>","DOI":"10.2168\/lmcs-8(1:11)2012","type":"journal-article","created":{"date-parts":[[2012,9,6]],"date-time":"2012-09-06T10:03:11Z","timestamp":1346925791000},"source":"Crossref","is-referenced-by-count":9,"title":["A System F accounting for scalars"],"prefix":"10.46298","volume":"Volume 8, Issue 1","author":[{"given":"Pablo","family":"Arrighi","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-5175-6882","authenticated-orcid":false,"given":"Alejandro","family":"Diaz-Caro","sequence":"additional","affiliation":[]}],"member":"25203","published-online":{"date-parts":[[2012,2,27]]},"reference":[{"key":"10.2168\/LMCS-8(1:11)2012_ArrighiDowekWRLA04","doi-asserted-by":"crossref","unstructured":"Pablo Arrighi and Gilles Dowek. A computational definition of the notion of vectorial space. In Narciso Mart\u00ed-Oliet, editor,Proceedings of WRLA-2004, volume 117 ofElectronic Notes in Theoretical Computer Science, pages 249-261. Elsevier, 2004.","DOI":"10.1016\/j.entcs.2004.06.013"},{"key":"10.2168\/LMCS-8(1:11)2012_ArrighiDowekRTA08","doi-asserted-by":"crossref","unstructured":"Pablo Arrighi and Gilles Dowek. Linear-algebraic lambda-calculus: higher-order, encodings, and confluence. In Andrei Voronkov, editor,Proceedings of RTA-2008, volume 5117 ofLecture Notes in Computer Science, pages 17-31. Springer, 2008.","DOI":"10.1007\/978-3-540-70590-1_2"},{"key":"10.2168\/LMCS-8(1:11)2012_ArrighiDiazcaroQPL09","doi-asserted-by":"crossref","unstructured":"Pablo Arrighi and Alejandro D\u00edaz-Caro. Scalar System F for linear-algebraiclambda-calculus: Towards a quantum physical logic. In Bob Coecke, Prakash Panangaden, and Peter Selinger, editors,Proceedings of QPL-2009, volume 270\/2 ofElectronic Notes in Theoretical Computer Science, pages 219-229. Elsevier, 2011.","DOI":"10.1016\/j.entcs.2011.01.033"},{"key":"10.2168\/LMCS-8(1:11)2012_ArrighiDiazcaroValironDCM11","unstructured":"Pablo Arrighi, Alejandro D\u00edaz-Caro, and Benoit Valiron. A type system for the vectorial aspects of the linear-algebraic lambda-calculus. InProceedings of the 7th International Workshop on Developments of Computational Methods (DCM 2011), Zurich, Switzerland, 2011. To appear in EPTCS. Draft at http:\/\/www.diaz-caro.info\/vectorial.pdf."},{"issue":"5","key":"10.2168\/LMCS-8(1:11)2012_ArbiserMiquelRiosJFP09","doi-asserted-by":"crossref","first-page":"581","DOI":"10.1017\/S0956796809007369","volume":"19","author":"Ariel Arbiser, Alexandre Miquel, and Ale","year":"2009","journal-title":"Journal of Functional Programming"},{"key":"10.2168\/LMCS-8(1:11)2012_Barendregt92","doi-asserted-by":"crossref","unstructured":"Henk P. Barendregt.Lambda calculi with types. Handbook of Logic in Computer Science: Volume 2. Oxford University Press, 1992.","DOI":"10.1093\/oso\/9780198537618.003.0002"},{"key":"10.2168\/LMCS-8(1:11)2012_BournezHoyrupRTA03","doi-asserted-by":"crossref","unstructured":"Olivier Bournez and Mathieu Hoyrup. Rewriting logic and probabilities. In Robert Nieuwenhuis, editor,Proceedings of RTA-2003, volume 2706 ofLecture Notes in Computer Science, pages 61-75. Springer, 2003.","DOI":"10.1007\/3-540-44881-0_6"},{"issue":"1","key":"10.2168\/LMCS-8(1:11)2012_BoudolIC94","doi-asserted-by":"crossref","first-page":"51","DOI":"10.1006\/inco.1994.1003","volume":"108","author":"G\u00e9rard Boudol","year":"1994","journal-title":"Information and Computation"},{"key":"10.2168\/LMCS-8(1:11)2012_CirsteaKirchnerLiquoriFOSSACS01","doi-asserted-by":"crossref","unstructured":"Horatiu Cirstea, Claude Kirchner, and Luigi Liquori. The Rho Cube. In Furio Honsell and Marino Miculan, editors,Proceedings of FOSSACS-2001, volume 2030 ofLecture Notes in Computer Science, pages 168-183. Springer, 2001.","DOI":"10.1007\/3-540-45315-6_11"},{"key":"10.2168\/LMCS-8(1:11)2012_ManualCOQ","unstructured":"Coq Dev. Team.The Coq proof assistant reference manual. INRIA, 8.2 edition, February 2009."},{"key":"10.2168\/LMCS-8(1:11)2012_DiazcaroPerdrixTassonValironHOR10","unstructured":"Alejandro D\u00edaz-Caro, Simon Perdrix, Christine Tasson, and Benoit Valiron. Equivalence of algebraiclambda-calculi. InInformal Proceedings of the 5th International Workshop on Higher-Order Rewriting, HOR-2010, pages 6-11, Edinburgh, UK, July 14, 2010."},{"issue":"2","key":"10.2168\/LMCS-8(1:11)2012_DipierroHankinWiklickyJLC05","doi-asserted-by":"crossref","first-page":"159","DOI":"10.1093\/logcom\/exi008","volume":"15","author":"Alessandra Di Pierro, Chris Hankin, and","year":"2005","journal-title":"Journal of Logic and Computation"},{"issue":"2","key":"10.2168\/LMCS-8(1:11)2012_DoughertyIC92","doi-asserted-by":"crossref","first-page":"251","DOI":"10.1016\/0890-5401(92)90064-M","volume":"101","author":"Daniel J. Dougherty","year":"1992","journal-title":"Information and Computation"},{"issue":"2","key":"10.2168\/LMCS-8(1:11)2012_deLiguoroPipernoIC95","doi-asserted-by":"crossref","first-page":"149","DOI":"10.1006\/inco.1995.1145","volume":"122","author":"Ugo de'Liguoro and Adolfo Piperno","year":"1995","journal-title":"Information and Computation"},{"key":"10.2168\/LMCS-8(1:11)2012_DalLagoZorzi11","unstructured":"Ugo Dal Lago and Margherita Zorzi. Probabilistic operational semantics for the lambda calculus. Preprint at arXiv:1104.0195, April 2011."},{"issue":"4","key":"10.2168\/LMCS-8(1:11)2012_EhrhardMSCS05","doi-asserted-by":"crossref","first-page":"615","DOI":"10.1017\/S0960129504004645","volume":"15","author":"Thomas Ehrhard","year":"2005","journal-title":"Mathematical Structures in Computer Science 2005"},{"key":"10.2168\/LMCS-8(1:11)2012_EhrhardLICS10","doi-asserted-by":"crossref","unstructured":"Thomas Ehrhard. A finiteness structure on resource terms. InProceedings of LICS-2010, pages 402-410. IEEE Computer Society, 2010.","DOI":"10.1109\/LICS.2010.38"},{"issue":"1","key":"10.2168\/LMCS-8(1:11)2012_EhrhardRegnierTCS03","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/S0304-3975(03)00392-X","volume":"309","author":"Thomas Ehrhard and Laurent Regnier","year":"2003","journal-title":"Theoretical Computer Science"},{"key":"10.2168\/LMCS-8(1:11)2012_GirardSLS71","doi-asserted-by":"crossref","unstructured":"Jean-Yves Girard. Une extension de l'interpretation de G\u00f6del \u00e0 l'analyse, et son application \u00e0 l'\u00e9limination des coupures dans l'analyse et la th\u00e9orie des types. In Jens Erik Fenstad, editor,Proceedings of the 2nd Scandinavian Logic Symposium, volume 63 ofStudies in Logic and the Foundations of Mathematics, pages 63-92. North-Holland, 1971.","DOI":"10.1016\/S0049-237X(08)70843-7"},{"key":"10.2168\/LMCS-8(1:11)2012_GirardPhDThesis","unstructured":"Jean-Yves Girard.Interpr\u00e9tation fonctionnelle et \u00e9limination des coupures dans l'arithm{\u00e9tique d'ordre sup\u00e9rieure}. PhD thesis, Universit\u00e9 Paris Diderot, Paris, France, 1972."},{"key":"10.2168\/LMCS-8(1:11)2012_GroverSTOC96","doi-asserted-by":"crossref","unstructured":"Lov K. Grover. A fast quantum mechanical algorithm for database search. InProceedings of the 28th Annual ACM Symposium on Theory of computing, STOC-96, pages 212-219. ACM, 1996.","DOI":"10.1145\/237814.237866"},{"key":"10.2168\/LMCS-8(1:11)2012_HerescuPalamidessiFOSSACS00","doi-asserted-by":"crossref","unstructured":"Oltea Mihaela Herescu and Catuscia Palamidessi. Probabilistic asynchronouspi-calculus. In Jerzy Tiuryn, editor,Proceedings of FOSSACS-2000, volume 1784 ofLecture Notes in Computer Science, pages 146-160. Springer, 2000.","DOI":"10.1007\/3-540-46432-8_10"},{"issue":"4","key":"10.2168\/LMCS-8(1:11)2012_JouannaudKirchnerSIAM86","doi-asserted-by":"crossref","first-page":"1155","DOI":"10.1137\/0215084","volume":"15","author":"Jean-Pierre Jouannaud and H\u00e9l\u00e8ne Kirchne","year":"1986","journal-title":"SIAM Journal on Computing"},{"key":"10.2168\/LMCS-8(1:11)2012_Krivine90","unstructured":"Jean-Louis Krivine.Lambda-calcul: types et mod\u00e8les. \u00c9tudes et recherches en informatique. Masson, 1990."},{"key":"10.2168\/LMCS-8(1:11)2012_LeBotlanRemySIGPLAN03","doi-asserted-by":"crossref","unstructured":"Didier Le Botlan and Didier R\u00e9my. ML<F: raising ML to the power of System F. InProceedings of the eighth ACM SIGPLAN international conference on Functional programming, ICFP'03, pages 27-38, New York, NY, USA, 2003. ACM.","DOI":"10.1145\/944746.944709"},{"key":"10.2168\/LMCS-8(1:11)2012_PetitTLCA09","doi-asserted-by":"crossref","unstructured":"Barbara Petit. A polymorphic type system for the lambda-calculus with constructors. In Pierre-Louis Curien, editor,Proceedings of TLCA-2009, volume 5608 ofLecture Notes in Computer Science, pages 234-248. Springer, 2009.","DOI":"10.1007\/978-3-642-02273-9_18"},{"issue":"2","key":"10.2168\/LMCS-8(1:11)2012_PetersonStickelACM81","doi-asserted-by":"crossref","first-page":"233","DOI":"10.1145\/322248.322251","volume":"28","author":"Gerald E. Peterson and Mark E. Stickel","year":"1981","journal-title":"Journal of the ACM"},{"key":"10.2168\/LMCS-8(1:11)2012_ReynoldsPS74","unstructured":"John C. Reynolds. Towards a theory of type structure. In Bernard Robinet, editor,Programming Symposium: Proceedings of the Colloque sur la Programmation, volume 19 ofLecture Notes in Computer Science, pages 408-425. Springer, 1974."},{"issue":"5","key":"10.2168\/LMCS-8(1:11)2012_ShorSIAM97","doi-asserted-by":"crossref","first-page":"1484","DOI":"10.1137\/S0097539795293172","volume":"26","author":"Peter W. Shor","year":"1997","journal-title":"SIAM Journal on Computing"},{"issue":"2","key":"10.2168\/LMCS-8(1:11)2012_TaitJSL67","doi-asserted-by":"crossref","first-page":"198","DOI":"10.2307\/2271658","volume":"32","author":"William W. Tait","year":"1967","journal-title":"The Journal of Symbolic Logic"},{"key":"10.2168\/LMCS-8(1:11)2012_TassonTLCA09","doi-asserted-by":"crossref","unstructured":"Christine Tasson. Algebraic totality, towards completeness. In Pierre-Louis Curien, editor,Proceedings of TLCA-2009, volume 5608 ofLecture Notes in Computer Science, pages 325-340. Springer, 2009.","DOI":"10.1007\/978-3-642-02273-9_24"},{"key":"10.2168\/LMCS-8(1:11)2012_Terese03","unstructured":"TeReSe.Term Rewriting Systems, volume 55 ofCambridge Tracts in Theoretical Computer Science. Cambridge University Press, 2003."},{"key":"10.2168\/LMCS-8(1:11)2012_ValironDCM10","doi-asserted-by":"crossref","unstructured":"Benoit Valiron. Semantics of a typed algebraic lambda-calculus. In S. Barry Cooper, Prakash Panangaden, and Elham Kashefi, editors,Proceedings DCM-2010, volume 26 ofElectronic Proceedings in Theoretical Computer Science, pages 147-158. Open Publishing Association, 2010.","DOI":"10.4204\/EPTCS.26.14"},{"key":"10.2168\/LMCS-8(1:11)2012_BenCoqProofVectorial","unstructured":"Benoit Valiron. Coq proof. , 2011."},{"key":"10.2168\/LMCS-8(1:11)2012_VauxRTA07","doi-asserted-by":"crossref","unstructured":"Lionel Vaux. On linear combinations of lambda-terms. In Franz Baader, editor,Proceedings of RTA-2007, volume 4533 ofLecture Notes in Computer Science, pages 374-388. Springer, 2007.","DOI":"10.1007\/978-3-540-73449-9_28"},{"issue":"5","key":"10.2168\/LMCS-8(1:11)2012_VauxMSCS09","doi-asserted-by":"crossref","first-page":"1029","DOI":"10.1017\/S0960129509990089","volume":"19","author":"Lionel Vaux","year":"2009","journal-title":"Mathematical Structures in Computer Science 2009"}],"container-title":["Logical Methods in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/lmcs.episciences.org\/846\/pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/lmcs.episciences.org\/846\/pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,4,28]],"date-time":"2024-04-28T23:52:56Z","timestamp":1714348376000},"score":1,"resource":{"primary":{"URL":"https:\/\/lmcs.episciences.org\/846"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012,2,27]]},"references-count":36,"URL":"https:\/\/doi.org\/10.2168\/lmcs-8(1:11)2012","relation":{"references":[{"id-type":"doi","id":"10.1017\/s0956796809007369","asserted-by":"subject"}],"is-same-as":[{"id-type":"arxiv","id":"0903.3741","asserted-by":"subject"},{"id-type":"doi","id":"10.48550\/arXiv.0903.3741","asserted-by":"subject"}]},"ISSN":["1860-5974"],"issn-type":[{"type":"electronic","value":"1860-5974"}],"subject":[],"published":{"date-parts":[[2012,2,27]]},"article-number":"846"}}