[go: up one dir, main page]
Skip to main content
Springer Nature Link
Log in

Linear-algebraic λ-calculus: higher-order, encodings, and confluence.

  • Conference paper
Rewriting Techniques and Applications (RTA 2008)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 5117))

Included in the following conference series:

  • 401 Accesses

Abstract

We introduce a minimal language combining higher-order computation and linear algebra. This language extends the λ-calculus with the possibility to make arbitrary linear combinations of terms α.t + β.u. We describe how to “execute” this language in terms of a few rewrite rules, and justify them through the two fundamental requirements that the language be a language of linear operators, and that it be higher-order. We mention the perspectives of this work in the field of quantum computation, whose circuits we show can be easily encoded in the calculus. Finally we prove the confluence of the calculus, this is our main result.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

Similar content being viewed by others

References

  1. Abramsky, S., Coecke, B.: A categorical semantics of quantum protocols LICS. IEEE Computer Society, 415–425 (2004)

    Google Scholar 

  2. Altenkirch, T., Grattage, J., Vizzotto, J.K., Sabry, A.: An Algebra of Pure Quantum Programming. In: Third International Workshop on Quantum Programming Languages. Electronic Notes of Theoretical Computer Science, vol. 170C, pp. 23–47 (2007)

    Google Scholar 

  3. Arrighi, P., Dowek, G.: A computational definition of the notion of vectorial space. ENTCS 117, 249–261 (2005)

    Google Scholar 

  4. Arrighi, P., Dowek, G.: Linear-algebraic lambda-calculus. In: Selinger, P. (ed.) International workshop on quantum programming languages, Turku Centre for Computer Science General Publication, vol. 33, pp. 21–38 (2004)

    Google Scholar 

  5. Arrighi, P., Dowek, G.: Linear-algebraic lambda-calculus: higher-order, encodings, confluence, arXiv:quant-ph/0612199.

    Google Scholar 

  6. Bernstein, E., Vazirani, U.: Quantum Complexity Theory. In: Annual ACM symposium on Theory of Computing, vol. 25 (1993)

    Google Scholar 

  7. Boudol, G.: Lambda-calculi for (strict) parallel functions. Information and Computation 108(1), 51–127 (1994)

    Article  MATH  MathSciNet  Google Scholar 

  8. Bournez, O., Hoyrup, M.: Rewriting Logic and Probabilities. In: Nieuwenhuis, R. (ed.) RTA 2003. LNCS, vol. 2706. Springer, Heidelberg (2003)

    Google Scholar 

  9. Boykin, P., Mor, T., Pulver, M., Roychowdhury, V., Vatan, F.: On universal and fault-taulerant quantum computing, arxiv:quant-ph/9906054

    Google Scholar 

  10. http://cime.lri.fr/

  11. Dershowitz, N., Jouannaud, J.-P.: Rewrite systems. In: Handbook of theoretical computer science. formal models and semantics, vol. B. MIT press, Cambridge (1991)

    Google Scholar 

  12. Deutsch, D., Josza, R.: Rapid solution of problems by quantum computation. Proc. of the Roy. Soc. of London A 439, 553–558 (1992)

    Article  MATH  Google Scholar 

  13. Dougherty, D.: Adding Algebraic Rewriting to the Untyped Lambda Calculus. In: Proc. of the Fourth International Conference on Rewriting Techniques and Applications (1992)

    Google Scholar 

  14. Ehrhard, T., Regnier, L.: The differential lambda-calculus. Theoretical Computer Science 309, 1–41 (2003)

    Article  MATH  MathSciNet  Google Scholar 

  15. Di Pierro, A., Hankin, C., Wiklicky, H.: Probabilistic λ-calculus and quantitative program analysis. J. of Logic and Computation 15(2), 159–179 (2005)

    Article  MATH  Google Scholar 

  16. Girard, J.-Y.: Linear logic. Theoretical Computer Science 50, 1–102 (1987)

    Article  MATH  MathSciNet  Google Scholar 

  17. Grover, L.K.: Quantum Mechanics Helps in Searching for a Needle in a Haystack. Phys. Rev. Lett. 79(2), 325–328 (1997)

    Article  Google Scholar 

  18. Herescu, O.M., Palamidessi, C.: Probabilistic asynchronous pi-calculus. In: Tiuryn, J. (ed.) ETAPS 2000 and FOSSACS 2000. LNCS, vol. 1784, pp. 146–160. Springer, Heidelberg (2000)

    Chapter  Google Scholar 

  19. Jouannaud, J.-P., Kirchner, H.: Completion of a Set of Rules Modulo a Set of Equations. SIAM J. of Computing 15(14), 1155–1194

    Google Scholar 

  20. Newman, M.H.A.: On theories with a combinatorial definition of ”equivalence”. Annals of Mathematics 432, 223–243 (1942)

    Article  Google Scholar 

  21. Nielsen, M.A.: Universal quantum computation using only projective measurement, quantum memory, and preparation of the 0 state. Phys. Rev. A 308, 96–100 (2003)

    MATH  Google Scholar 

  22. Peterson, G.E., Stickel, M.E.: Complete Sets of Reductions for Some Equational Theories. J. ACM 28(2), 233–264 (1981)

    Article  MATH  MathSciNet  Google Scholar 

  23. Perdrix, S.: State transfer instead of teleportation in measurement-based quantum computation. Int. J. of Quantum Information 1(1), 219–223 (2005)

    Article  Google Scholar 

  24. Raussendorf, R., Browne, D.E., Briegel, H.J.: The one-way quantum computer - a non-network model of quantum computation. Journal of Modern Optics 49, 1299 (2002)

    Article  MATH  MathSciNet  Google Scholar 

  25. Selinger, P.: Towards a quantum programming language. Math. Struc. in Computer Science 14(4), 527–586 (2004)

    Article  MATH  MathSciNet  Google Scholar 

  26. Selinger, P., Valiron, B.: A lambda calculus for quantum computation with classical control. Math. Struc. in Computer Science 16(3), 527–552 (2006)

    Article  MATH  MathSciNet  Google Scholar 

  27. Shor, P.W.: Polynomial-Time Algorithms for Prime Factorization and Discrete Logarithms on a Quantum Computer. SIAM J. on Computing 26, 1484–1509 (1997)

    Article  MATH  MathSciNet  Google Scholar 

  28. Van Tonder, A.: A Lambda Calculus for Quantum Computation, arXiv:quant-ph/0307150 (July 2003)

    Google Scholar 

  29. Vaux, L.: On linear combinations of lambda-terms. In: Baader, F. (ed.) RTA 2007. LNCS, vol. 4533, pp. 374–388. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  30. Wooters, W.K., Zurek, W.H.: A single quantum cannot be cloned. Nature 299, 802–803 (1982)

    Article  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Université de Grenoble and IMAG Laboratories, 46 Avenue Félix Viallet, 38031, Grenoble Cedex, France

    Pablo Arrighi

  2. École polytechnique and INRIA, LIX, 91128, Palaiseau Cedex, France

    Gilles Dowek

Authors
  1. Pablo Arrighi
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Gilles Dowek
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Andrei Voronkov

Rights and permissions

Reprints and permissions

Copyright information

© 2008 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Arrighi, P., Dowek, G. (2008). Linear-algebraic λ-calculus: higher-order, encodings, and confluence.. In: Voronkov, A. (eds) Rewriting Techniques and Applications. RTA 2008. Lecture Notes in Computer Science, vol 5117. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-70590-1_2

Download citation

  • DOI: https://doi.org/10.1007/978-3-540-70590-1_2

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-70588-8

  • Online ISBN: 978-3-540-70590-1

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation