Skip to Main content Skip to Navigation
Conference papers

Scalar System F for Linear-Algebraic λ-Calculus: Towards a Quantum Physical Logic

Pablo Arrighi 1 Alejandro Díaz-Caro 2, *
* Corresponding author
1 CAPP - Calculs algorithmes programmes et preuves
LIG - Laboratoire d'Informatique de Grenoble
Abstract : The Linear-Algebraic λ-Calculus extends the λ-calculus with the possibility of making arbitrary linear combinations of terms α.t+β.u. Since one can express fixed points over sums in this calculus, one has a notion of infinities arising, and hence indefinite forms. As a consequence, in order to guarantee the confluence, t−t does not always reduce to 0 - only if t is closed normal. In this paper we provide a System F like type system for the Linear-Algebraic λ-Calculus, which guarantees normalisation and hence no need for such restrictions, t−t always reduces to 0. Moreover this type system keeps track of 'the amount of a type'. As such it can be seen as probabilistic type system, guaranteeing that terms define correct probabilistic functions. It can also be seen as a step along the quest toward a quantum physical logic through the Curry-Howard isomorphism.
Complete list of metadata
Contributor : Alejandro Díaz-Caro <>
Submitted on : Tuesday, January 7, 2014 - 11:44:35 AM
Last modification on : Tuesday, November 24, 2020 - 4:06:01 PM

Links full text




Pablo Arrighi, Alejandro Díaz-Caro. Scalar System F for Linear-Algebraic λ-Calculus: Towards a Quantum Physical Logic. QPL 2009 - International Workshop on Quantum Physics and Logic, Apr 2009, Oxford, United Kingdom. pp.219-229, ⟨10.1016/j.entcs.2011.01.033⟩. ⟨hal-00924890⟩



Record views