Scalar system F for linear-algebraic λ-calculus: Towards a quantum physical logic

ARRIGHI, PABLO; DÍAZ-CARO, ALEJANDRO

Electronic Notes in Theoretical Computer Science

Elsevier

Año: 2011 vol. 270 p. 219 - 229

1571-0661

The Linear-Algebraic λ-Calculus [Arrighi, P. and G. Dowek, Linear-algebraic λ-calculus: higher-order, encodings and confluence, Lecture Notes in Computer Science (RTA´08) 5117 (2008), pp. 17-31] 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 [Sørensen, 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]. © 2011 Elsevier B.V. All rights reserved.