A System F accounting for scalars

Pablo Arrighi; Alejandro Diaz-Caro

doi:10.2168/LMCS-8(1:11)2012

Pablo Arrighi ; Alejandro Diaz-Caro - A System F accounting for scalars

lmcs:846 - Logical Methods in Computer Science, February 27, 2012, Volume 8, Issue 1 - https://doi.org/10.2168/LMCS-8(1:11)2012

A System F accounting for scalarsArticle

Authors: Pablo Arrighi ; Alejandro Diaz-Caro

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.

https://doi.org/10.2168/LMCS-8(1:11)2012

Source: arXiv.org:0903.3741

Volume: Volume 8, Issue 1

Published on: February 27, 2012

Imported on: June 10, 2011

Keywords: Computer Science - Logic in Computer Science,Computer Science - Programming Languages,Quantum Physics,F.4.1

Licence: arXiv.org - Non-exclusive license to distribute

Classifications

Mathematics Subject Classification 2020¹

Sources:

[1] zbMATH Open.

Bibliographic References

10 Documents citing this article

Alejandro Díaz-Caro, 2022, A Quick Overview on the Quantum Control Approach to the Lambda Calculus, arXiv (Cornell University), 357, pp. 1-17, 10.4204/eptcs.357.1.

Alejandro Diaz-Caro;Mauricio Guillermo;Alexandre Miquel;Benoit Valiron, Realizability in the Unitary Sphere, pp. 1-13, 2019, Vancouver, BC, Canada, 10.1109/lics.2019.8785834, https://hal.archives-ouvertes.fr/hal-02175168.

Luca Paolini;Mauro Piccolo;Margherita Zorzi, 2019, QPCF: Higher-Order Languages and Quantum Circuits, Institutional Research Information System University of Turin (University of Turin), 63, 4, pp. 941-966, 10.1007/s10817-019-09518-y, http://hdl.handle.net/2318/1715460.

Margherita Zorzi, 2019, Quantum Calculi—From Theory to Language Design, Applied Sciences, 9, 24, pp. 5472, 10.3390/app9245472, https://doi.org/10.3390/app9245472.

Alejandro Díaz-Caro, arXiv (Cornell University), A Lambda Calculus for Density Matrices with Classical and Probabilistic Controls, pp. 448-467, 2017, 10.1007/978-3-319-71237-6_22, https://arxiv.org/abs/1705.00097.

Alejandro Díaz-Caro;Gilles Dowek, Americanae (AECID Library), Typing Quantum Superpositions and Measurement, pp. 281-293, 2017, 10.1007/978-3-319-71069-3_22, http://hdl.handle.net/11336/42228.

Alejandro Díaz-Caro;Pablo E. Martínez López, arXiv (Cornell University), Isomorphisms considered as equalities, pp. 1-11, 2015, Koblenz Germany, 10.1145/2897336.2897346, http://arxiv.org/abs/1511.09324.

MARGHERITA ZORZI, 2014, On quantum lambda calculi: a foundational perspective, Mathematical Structures in Computer Science, 26, 7, pp. 1107-1195, 10.1017/s0960129514000425.

Alejandro Díaz-Caro;Gilles Dowek, 2013, Non determinism through type isomorphism, arXiv (Cornell University), 113, pp. 137-144, 10.4204/eptcs.113.13.

Alejandro Díaz-Caro;Giulio Manzonetto;Michele Pagani, Call-by-Value Non-determinism in a Linear Logic Type Discipline, pp. 164-178, 2013, 10.1007/978-3-642-35722-0_12, https://hal.inria.fr/hal-00919463.

Sources : OpenCitations, OpenAlex & Crossref

Share and export

Consultation statistics

This page has been seen 2046 times.

This article's PDF has been downloaded 541 times.