[ Open access | slides ]
doi:10.2168/LMCS-8(1:11)2012

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.

@Article{ArrighiDiazcaroLMCS12,
    author = "Pablo Arrighi and Alejandro D{\'\i}az-Caro",
    title = "A {S}ystem {F} accounting for scalars",
    journal = "Logical Methods in Computer Science",
    volume = "8",
    number = "1:11",
    year = "2012"
}

[ Open access | slides (QuAND) ]
doi:10.4204/EPTCS.81.2

The linear-algebraic λ-calculus and the algebraic λ-calculus are untyped λ-calculi extended with arbitrary linear combinations of terms. The former presents the axioms of linear algebra in the form of a rewrite system, while the latter uses equalities. When given by rewrites, algebraic λ-calculi are not confluent unless further restrictions are added. We provide a type system for the linear-algebraic λ-calculus enforcing strong normalisation, which gives back confluence. The type system allows an interpretation in System F.

@InProceedings{BuirasDiazcaroJaskelioffLSFA11,
    author = "Pablo Buiras and Alejandro D{\'\i}az-Caro and Mauro Jaskelioff,
    title = "Confluence via strong normalisation in an algebraic $\lambda$-calculus with rewriting",
    pages = "16--29",
    year = "2012",
    editor = "Simona {Ronchi della Rocca} and Elaine Pimentel",
    booktitle = "Proceedings of the 6th Workshop on Logical and Semantic Frameworks with Applications (LSFA 2011)",
    series = "Electronic Proceedings in Theoretical Computer Science",
    volume = "81",
    publisher = "Open Publishing Association"
}

[ arXiv (preprint) | full-proofs version | COQ proof advertised in the paper | slides ]

We describe a type system for the linear-algebraic lambda-calculus. The type system accounts for the part of the language emulating linear operators and vectors, i.e. it is able to statically describe the linear combinations of terms resulting from the reduction of programs. This gives rise to an original type theory where types, in the same way as terms, can be superposed into linear combinations. We show that the resulting typed lambda-calculus is strongly normalizing and features a weak subject-reduction.

@InProceedings{ArrighiDiazcaroValironDCM11,
    author = "Pablo Arrighi and Alejandro D{\'\i}az-Caro and Beno{\^\i}t Valiron",
    title = "A type system for the vectorial aspects of the linear-algebraic lambda-calculus",
    booktitle = "Proceedings of the 7th International Workshop on Developments of Computational Methods (DCM 2011)",
    year = "2011",
    address = "Zurich, Switzerland",
    note = "To appear in EPTCS. Preprint at {\tt arXiv:1012.4032}"
}

[ arXiv | slides | http ]
doi:10.1016/j.entcs.2011.01.033

The Linear-Algebraic Lambda-Calculus (arXiv:quant-ph/0612199) extends the lambda-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 Lambda-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.

@InProceedings{ArrighiDiazcaroQPL09,
    author = "Pablo Arrighi and Alejandro D{\'\i}az-Caro",
    title = "Scalar {S}ystem {F} for Linear-Algebraic $\lambda$-Calculus: Towards a Quantum Physical Logic",
    pages = "206--215",
    year = "2011",
    editor = "Bob Coecke and Prakash Panangaden and Peter Selinger",
    booktitle = "Proceedings of the 6th International Workshop on Quantum Physics and Logic ({QPL} 2009)",
    series = "Electronic Notes in Theoretical Computer Science",
    volume = "270/2",
    publisher = "Springer"
}

[ arXiv | http ]
doi:10.1016/j.entcs.2011.01.006

This paper demonstrates how to add a measurement operator to quantum lambda-calculi. A proof of the consistency of the semantics is given through a proof of confluence presented in a sufficiently general way to allow this technique to be used for other languages. The method described here may be applied to probabilistic rewrite systems in general, and to add measurement to more complex languages such as QML or Lineal, which is the subject of further research.

@InProceedings{DiazcaroArrighiGadellaGrattageQPLDCM08,
    author = "Pablo Arrighi and Alejandro D{\'\i}az-Caro and Manuel Gadella and Jonathan J. Grattage",
    title = "Measurements and Confluence in Quantum Lambda Calculi With Explicit Qubits",
    pages = "59--74",
    year = "2011",
    editor = "Bob Coecke and Ian Mackie and Prakash Panangaden and Peter Selinger",
    booktitle = "Proceedings of the Joint 5th International Workshop on Quantum Physics and Logic and 4th Workshop on Developments in Computational Models ({QPL/DCM} 2008)",
    series = "Electronic Notes in Theoretical Computer Science",
    volume = "270/1",
    publisher = "Springer"
}

[ arXiv | slides | HOR 2010 site ]

We examine the relationship between the algebraic lambda-calculus λ_alg, a fragment of the differential lambda-calculus, and the linear-algebraic lambda-calculus λ_lin, a candidate lambda-calculus for quantum computation. Both calculi are algebraic: each one is equipped with an additive and a scalar-multiplicative structure, and the set of terms is closed under linear combinations. We answer the conjectured question of the simulation of λ_alg by λ_lin and the reverse simulation of λ_lin by λ_alg. Our proof relies on the observation that λ_lin is essentially call-by-value, while λ_alg is call-by-name. The former simulation uses the standard notion of thunks, while the latter is based on an algebraic extension of the continuation passing style. This result is a step towards an extension of call-by-value / call-by-name duality to algebraic lambda-calculi

@InProceedings{DiazcaroPerdrixTassonValironHOR10,
    author = "Alejandro D{\'\i}az-Caro and Simon Perdrix and Christine Tasson and Beno{\^\i}t Valiron",
    title = "Equivalence of Algebraic $\lambda$-calculi",
    booktitle = "Informal proceedings of {HOR}-2010",
    pages = "6--11",
    year = "2010",
    address = "Edinburgh, UK",
    month = jul # {~14,},
}

[ Updated draft | arXiv (out of date) | slides of a preliminar version (TYPES'10) ]

We consider the non-deterministic extension of the call-by-value lambda calculus, which corresponds to the additive fragment of the linear-algebraic lambda-calculus. We define a fine-grained type system, capturing the right linearity present in such formalisms. After proving the subject reduction and the strong normalisation properties, we propose a translation of this calculus into the System F with pairs, which corresponds to a non linear fragment of linear logic. The translation provides a deeper understanding of the linearity in our setting.

@Misc{DiazcaroPetit12,
    author = "Alejandro D{\'\i}az-Caro and Barbara Petit",
    title = "Linearity in the non-deterministic call-by-value setting",
    year = "2012",
    howpublished = "Draft at {\tt http://www.diaz-caro.info/additive.pdf}"
}

[ draft ]

We present a proof system where isomorphic propositions have the same proofs, i.e. we take the quotient of the set of propositions by the relation generated by the isomorphism between types and define proofs for elements in this quotient. The syntax of the system resembles several non-deterministic and algebraic lambda-calculi in the literature. In addition, in order to keep subject reduction, a non-deterministic rewriting is allowed, which outputs one of multiple possibilities, all of them being proof of the same proposition. We supply proofs of subject reduction and strong normalisation of this system.

@Misc{DiazcaroDowek12,
    author = "Alejandro D{\'\i}az-Caro and Gilles Dowek",
    title = "Non determinism through type isomophism",
    year = "2012",
    howpublished = "Draft at {\tt http://www.diaz-caro.info/ndti.pdf}"
}

[ draft ]

We consider the call-by-value λ-calculus extended with a may-convergent non-deterministic choice and a must-convergent parallel composition. Inspired by recent works on the relational semantics of linear logic (LL) and non-idempotent intersection types, we endow this calculus with a type system based on the so-called Girard's second translation of intuitionistic logic into LL. We prove that a term is typable if and only if is converging, and that its typing tree carries enough information to give a bound on the length of its lazy call-by-value reduction. Moreover, when the typing tree is minimal, such a bound becomes the exact length of the reduction.

@Misc{DiazcaroManzonettoPagani12,
    author = "Alejandro D{\'\i}az-Caro and Giulio Manzonetto and Michele Pagani",
    title = "Call-by-value non-determinism in a linear logic type discipline",
    year = "2012",
    howpublished = "Draft at {\tt http://www.diaz-caro.info/dmp12.pdf}"
}

[ arXiv ]

We examine the relationship between the algebraic λ-calculus, a fragment of the differential λ-calculus; and the linear-algebraic λ-calculus, a candidate λ-calculus for quantum computation. Both calculi are algebraic: each one is equipped with an additive and a scalar-multiplicative structure, and their set of terms is closed under linear combinations. However, the two languages were built using different approaches: the former is a call-by-name language whereas the latter is call-by-value; the former considers algebraic equalities whereas the latter approach them through rewrite rules.
"In this paper, we analyse how these different approaches relate one to the other. To this end, we propose four canonical languages based on each of the possible choices: call-by-name versus call-by-value, algebraic equality versus algebraic rewriting. We show that the various languages simulate one another. Due to subtle interaction between beta-reduction and algebraic rewriting, to make the languages consistent some additional hypotheses such as confluence might be required. We carefully devise the required properties for each proof, making them general enough to be valid for any sub-language satisfying the corresponding properties.

@Misc{DiazcaroPerdrixTassonValiron11,
    author = "Alejandro D{\'\i}az-Caro and Simon Perdrix and Christine Tasson and Beno{\^\i}t Valiron",
    title = "Call-by-value, call-by-name and the vectorial behaviour of algebraic $\lambda$-calculus",
    year = "2011",
    howpublished = "Draft at {\tt arXiv:1005.2897}"
}

[ pdf | slides | video (only the dissertation part) | TEL ]

Jury:
Pablo Arrighi	Université de Grenoble	(directeur)
Eduardo Bonelli	Universidad Nacional de Quilmes and CONICET	(rapporteur)
Gilles Dowek	INRIA Centre Paris-Rocquencourt	(rapporteur)
Thomas Ehrhard	Laboratoire Preuves, Programmes et Systèmes	(rapporteur)
Philippe Jorrand	CNRS	(président)
Michele Pagani	Université Paris-Nord	(examinateur)
Laurent Regnier	Université de la Méditerranée	(examinateur)
Lionel Vaux	Université de la Méditerranée	(examinateur)

The objective of this thesis is to develop a type theory for the linear-algebraic λ-calculus, an extension of λ-calculus motivated by quantum computing. This algebraic extension encompass all the terms of λ-calculus together with their linear combinations, so if t and r are two terms, so is α.t + β.r, with α and β being scalars from a given ring. The key idea and challenge of this thesis was to introduce a type system where the types, in the same way as the terms, form a vectorial space, providing the information about the structure of the normal form of the terms. This thesis presents the system Lineal, and also three intermediate systems, however interesting by themselves: Scalar, Additive and λCA, all of them with their subject reduction and strong normalisation proofs.

@phdthesis{Diazcaro11,
    author = "Alejandro D{\'\i}az-Caro",
    title = "Du typage vectoriel",
    school = "Universit\'e de Grenoble",
    year = "2011",
    address = "France",
    month = sep # {~23,},
}

[ pdf | slides ]

This thesis demonstrates how to add a measurement operator to van Tonder\'s quantum lambda-calculus.
Paper [5] is a by-product of this thesis.

@mastersthesis{Diazcaro07,
    author = "Alejandro D{\'\i}az-Caro",
    title = "Agregando medici\'on al c\'alculo de van Tonder",
    school = "Universidad Nacional de Rosario",
    year = "2007",
    address = "Argentina",
    month = dec # {~21,},
}