Completeness of algebraic CPS simulations

Ali Assaf
(LIG, Université Joseh Fourier and École Polytechnique, France)
Simon Perdrix
(CNRS, LIG, Université de Grenoble, France)

The algebraic lambda calculus and the linear algebraic lambda calculus are two extensions of the classical lambda calculus with linear combinations of terms. They arise independently in distinct contexts: the former is a fragment of the differential lambda calculus, the latter is a candidate lambda calculus for quantum computation. They differ in the handling of application arguments and algebraic rules. The two languages can simulate each other using an algebraic extension of the well-known call-by-value and call-by-name CPS translations. These simulations are sound, in that they preserve reductions. In this paper, we prove that the simulations are actually complete, strengthening the connection between the two languages.

In Elham Kashefi, Jean Krivine and Femke van Raamsdonk: Proceedings 7th International Workshop on Developments of Computational Methods (DCM 2011), Zurich, Switzerland, 3rd July 2011, Electronic Proceedings in Theoretical Computer Science 88, pp. 16–27.
Published: 30th July 2012.

ArXived at: https://dx.doi.org/10.4204/EPTCS.88.2 bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org