Scalar System F for Linear-Algebraic λ-Calculus: Towards a Quantum Physical Logic
| Autor: | Alejandro Díaz-Caro, Pablo Arrighi |
|---|---|
| Přispěvatelé: | Calculs algorithmes programmes et preuves (CAPP), Laboratoire d'Informatique de Grenoble (LIG), Institut polytechnique de Grenoble - Grenoble Institute of Technology (Grenoble INP )-Institut National Polytechnique de Grenoble (INPG)-Centre National de la Recherche Scientifique (CNRS)-Université Pierre Mendès France - Grenoble 2 (UPMF)-Université Joseph Fourier - Grenoble 1 (UJF)-Institut polytechnique de Grenoble - Grenoble Institute of Technology (Grenoble INP )-Institut National Polytechnique de Grenoble (INPG)-Centre National de la Recherche Scientifique (CNRS)-Université Pierre Mendès France - Grenoble 2 (UPMF)-Université Joseph Fourier - Grenoble 1 (UJF), Institut polytechnique de Grenoble - Grenoble Institute of Technology (Grenoble INP )-Institut National Polytechnique de Grenoble (INPG)-Centre National de la Recherche Scientifique (CNRS)-Université Pierre Mendès France - Grenoble 2 (UPMF)-Université Joseph Fourier - Grenoble 1 (UJF), Bob Coecke and Prakash Panangaden and Peter Selinger |
| Rok vydání: | 2011 |
| Předmět: |
Pure mathematics
General Computer Science Curry-Howard 0102 computer and information sciences Fixed point 01 natural sciences Dependent type Quantum logic Curry–Howard correspondence Theoretical Computer Science [PHYS.QPHY]Physics [physics]/Quantum Physics [quant-ph] Computer Science::Logic in Computer Science Calculus 0101 mathematics Mathematics [INFO.INFO-PL]Computer Science [cs]/Programming Languages [cs.PL] Type inhabitation Type Theory System F 010102 general mathematics [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO] Probabilistic Lambda Calculus Pure type system Type theory 010201 computation theory & mathematics Quantum Logic Computer Science(all) |
| Zdroj: | QPL 2009-International Workshop on Quantum Physics and 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⟩ |
| ISSN: | 1571-0661 |
| DOI: | 10.1016/j.entcs.2011.01.033 |
| Popis: | The Linear-Algebraic @l-Calculus [Arrighi, P. and G. Dowek, Linear-algebraic @l-calculus: higher-order, encodings and confluence, Lecture Notes in Computer Science (RTA'08) 5117 (2008), pp. 17-31] extends the @l-calculus with the possibility of making arbitrary linear combinations of terms @a.t+@b.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 @l-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 [Sorensen, M. H. and P. Urzyczyn, ''Lectures on the Curry-Howard Isomorphism, Volume 149 (Studies in Logic and the Foundations of Mathematics),'' Elsevier Science Inc., New York, NY, USA, 2006]. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|
Full Text from ScienceDirect