{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,14]],"date-time":"2026-03-14T09:03:30Z","timestamp":1773479010031,"version":"3.50.1"},"reference-count":25,"publisher":"Cambridge University Press (CUP)","issue":"1","license":[{"start":{"date-parts":[[2023,11,21]],"date-time":"2023-11-21T00:00:00Z","timestamp":1700524800000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":["cambridge.org"],"crossmark-restriction":true},"short-container-title":["Math. Struct. Comp. Sci."],"published-print":{"date-parts":[[2024,1]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>We give an adequate, concrete, categorical-based model for Lambda-<jats:inline-formula><jats:alternatives><jats:inline-graphic xmlns:xlink=\"http:\/\/www.w3.org\/1999\/xlink\" mime-subtype=\"png\" xlink:href=\"S0960129523000361_inline1.png\"\/><jats:tex-math>\n${\\mathcal S}$\n<\/jats:tex-math><\/jats:alternatives><\/jats:inline-formula>, which is a typed version of a linear-algebraic lambda calculus, extended with measurements. Lambda-<jats:inline-formula><jats:alternatives><jats:inline-graphic xmlns:xlink=\"http:\/\/www.w3.org\/1999\/xlink\" mime-subtype=\"png\" xlink:href=\"S0960129523000361_inline2.png\"\/><jats:tex-math>\n${\\mathcal S}$\n<\/jats:tex-math><\/jats:alternatives><\/jats:inline-formula> is an extension to first-order lambda calculus unifying two approaches of non-cloning in quantum lambda-calculi: to forbid duplication of variables and to consider all lambda-terms as algebraic linear functions. The type system of Lambda-<jats:inline-formula><jats:alternatives><jats:inline-graphic xmlns:xlink=\"http:\/\/www.w3.org\/1999\/xlink\" mime-subtype=\"png\" xlink:href=\"S0960129523000361_inline3.png\"\/><jats:tex-math>\n${\\mathcal S}$\n<\/jats:tex-math><\/jats:alternatives><\/jats:inline-formula> has a superposition constructor <jats:italic>S<\/jats:italic> such that a type <jats:italic>A<\/jats:italic> is considered as the base of a vector space, while <jats:italic>SA<\/jats:italic> is its span. Our model considers <jats:italic>S<\/jats:italic> as the composition of two functors in an adjunction relation between the category of sets and the category of vector spaces over <jats:inline-formula><jats:alternatives><jats:inline-graphic xmlns:xlink=\"http:\/\/www.w3.org\/1999\/xlink\" mime-subtype=\"png\" xlink:href=\"S0960129523000361_inline4.png\"\/><jats:tex-math>\n$\\mathbb C$\n<\/jats:tex-math><\/jats:alternatives><\/jats:inline-formula>. The right adjoint is a forgetful functor <jats:italic>U<\/jats:italic>, which is hidden in the language, and plays a central role in the computational reasoning.<\/jats:p>","DOI":"10.1017\/s0960129523000361","type":"journal-article","created":{"date-parts":[[2023,11,21]],"date-time":"2023-11-21T06:49:09Z","timestamp":1700549349000},"page":"1-44","update-policy":"https:\/\/doi.org\/10.1017\/policypage","source":"Crossref","is-referenced-by-count":2,"title":["A concrete model for a typed linear algebraic lambda calculus"],"prefix":"10.1017","volume":"34","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-5175-6882","authenticated-orcid":false,"given":"Alejandro","family":"D\u00edaz-Caro","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Octavio","family":"Malherbe","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"56","published-online":{"date-parts":[[2023,11,21]]},"reference":[{"key":"S0960129523000361_ref15","author":"D\u00edaz-Caro","year":"2012"},{"key":"S0960129523000361_ref3","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2005.1"},{"key":"S0960129523000361_ref10","doi-asserted-by":"publisher","DOI":"10.1016\/j.biosystems.2019.104012"},{"key":"S0960129523000361_ref6","first-page":"8","article-title":"Lineal: A linear-algebraic lambda-calculus","volume":"13","author":"Arrighi","year":"2017","journal-title":"Logical Methods in Computer Science"},{"key":"S0960129523000361_ref17","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0092872"},{"key":"S0960129523000361_ref16","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(87)90045-4"},{"key":"S0960129523000361_ref20","unstructured":"Moggi, E. (1988). Computational lambda-calculus and monads. Technical Report ECS-LFCS-88-66, Lab. for Foundations of Computer Science, University of Edinburgh."},{"key":"S0960129523000361_ref9","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-71069-3_22"},{"key":"S0960129523000361_ref11","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2019.8785834"},{"key":"S0960129523000361_ref5","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2017.04.001"},{"key":"S0960129523000361_ref12","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2019.07.006"},{"key":"S0960129523000361_ref18","doi-asserted-by":"publisher","DOI":"10.1145\/2499370.2462177"},{"key":"S0960129523000361_ref21","doi-asserted-by":"publisher","DOI":"10.1145\/2578855.2535879"},{"key":"S0960129523000361_ref22","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2006.12.018"},{"key":"S0960129523000361_ref25","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129514000425"},{"key":"S0960129523000361_ref4","first-page":"11","article-title":"A System F accounting for scalars","volume":"8","author":"Arrighi","year":"2012","journal-title":"Logical Methods in Computer Science"},{"key":"S0960129523000361_ref14","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2018.10.008"},{"key":"S0960129523000361_ref8","author":"Benton","year":"1994"},{"key":"S0960129523000361_ref7","first-page":"8","article-title":"Call-by-value, call-by-name and the vectorial behaviour of the algebraic","volume":"10","author":"Assaf","year":"2014","journal-title":"Logical Methods in Computer Science"},{"key":"S0960129523000361_ref13","doi-asserted-by":"publisher","DOI":"10.1007\/s10485-020-09598-7"},{"key":"S0960129523000361_ref24","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129509990089"},{"key":"S0960129523000361_ref1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(93)90181-R"},{"key":"S0960129523000361_ref2","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2004.1319636"},{"key":"S0960129523000361_ref23","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129506005238"},{"key":"S0960129523000361_ref19","volume-title":"Categories for the Working Mathematician","author":"Mac Lane","year":"1998"}],"container-title":["Mathematical Structures in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0960129523000361","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,1,24]],"date-time":"2024-01-24T09:27:13Z","timestamp":1706088433000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0960129523000361\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,11,21]]},"references-count":25,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2024,1]]}},"alternative-id":["S0960129523000361"],"URL":"https:\/\/doi.org\/10.1017\/s0960129523000361","relation":{},"ISSN":["0960-1295","1469-8072"],"issn-type":[{"value":"0960-1295","type":"print"},{"value":"1469-8072","type":"electronic"}],"subject":[],"published":{"date-parts":[[2023,11,21]]},"assertion":[{"value":"\u00a9 The Author(s), 2023. Published by Cambridge University Press","name":"copyright","label":"Copyright","group":{"name":"copyright_and_licensing","label":"Copyright and Licensing"}}]}}