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

Pablo Arrighi 1 Alejandro Díaz-Caro 2, *
* Auteur correspondant
1 CAPP
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.
Type de document :
Communication dans un congrès
Bob Coecke and Prakash Panangaden and Peter Selinger. QPL 2009 - International Workshop on Quantum Physics and Logic, Apr 2009, Oxford, United Kingdom. Elsevier, 270(2), pp.219-229, 2011, Proceedings of the 6th International Workshop on Quantum Physics and Logic (QPL 2009). 〈10.1016/j.entcs.2011.01.033〉
Liste complète des métadonnées

https://hal.inria.fr/hal-00924890
Contributeur : Alejandro Díaz-Caro <>
Soumis le : mardi 7 janvier 2014 - 11:44:35
Dernière modification le : jeudi 11 janvier 2018 - 06:26:30

Lien texte intégral

Identifiants

Collections

Citation

Pablo Arrighi, Alejandro Díaz-Caro. Scalar System F for Linear-Algebraic λ-Calculus: Towards a Quantum Physical Logic. Bob Coecke and Prakash Panangaden and Peter Selinger. QPL 2009 - International Workshop on Quantum Physics and Logic, Apr 2009, Oxford, United Kingdom. Elsevier, 270(2), pp.219-229, 2011, Proceedings of the 6th International Workshop on Quantum Physics and Logic (QPL 2009). 〈10.1016/j.entcs.2011.01.033〉. 〈hal-00924890〉

Partager

Métriques

Consultations de la notice

123