Document Open Access Logo

A Rewriting Theory for Quantum λ-Calculus

Authors Claudia Faggian , Gaetan Lopez, Benoît Valiron

PDF

File

Thumbnail PDF
PDF
LIPIcs.CSL.2025.47.pdf
  • Filesize: 1 MB
  • 22 pages

Document Identifiers

Related Versions

Subject Classification

ACM Subject Classification
  • Theory of computation → Quantum computation theory
  • Theory of computation → Operational semantics
  • Theory of computation → Equational logic and rewriting
  • Theory of computation → Linear logic
Keywords
  • quantum lambda-calculus
  • probabilistic rewriting
  • operational semantics
  • asymptotic normalization
  • principles of quantum programming languages

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Abstract

Quantum lambda calculus has been studied mainly as an idealized programming language - the evaluation essentially corresponds to a deterministic abstract machine. Very little work has been done to develop a rewriting theory for quantum lambda calculus. Recent advances in the theory of probabilistic rewriting give us a way to tackle this task with tools unavailable a decade ago. Our primary focus are standardization and normalization results.

Cite As Get BibTex

Claudia Faggian, Gaetan Lopez, and Benoît Valiron. A Rewriting Theory for Quantum λ-Calculus. In 33rd EACSL Annual Conference on Computer Science Logic (CSL 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 326, pp. 47:1-47:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025) https://doi.org/10.4230/LIPIcs.CSL.2025.47

Author Details

Claudia Faggian
  • IRIF, CNRS, Université Paris Cité, France
Gaetan Lopez
  • IRIF, CNRS, Université Paris Cité, France
Benoît Valiron
  • Université Paris-Saclay, CNRS, CentraleSupélec, ENS Paris-Saclay, Inria, Laboratoire Méthodes Formelles, 91190, Gif-sur-Yvette, France

Funding

This work has been partially funded by the French National Research Agency (ANR) by the projects PPS ANR-19-CE48-0014, TaQC ANR-22-CE47-0012 and within the framework of "Plan France 2030", under the research projects EPIQ ANR-22-PETQ-0007, OQULUS ANR-23-PETQ-0013, HQI-Acquisition ANR-22-PNCQ-0001 and HQI-R&D ANR-22-PNCQ-0002.

References

  1. Beniamino Accattoli, Claudia Faggian, and Giulio Guerrieri. Factorize factorization. In 29th EACSL Annual Conference on Computer Science Logic, CSL 2021, January 25-28, 2021, Ljubljana, Slovenia (Virtual Conference), volume 183 of LIPIcs, pages 6:1-6:25. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2021. URL: https://doi.org/10.4230/LIPIcs.CSL.2021.6.
  2. Zena M. Ariola and Stefan Blom. Skew confluence and the lambda calculus with letrec. Annals of Pure and Applied Logic, 117(1):95-168, 2002. URL: https://doi.org/10.1016/S0168-0072(01)00104-X.
  3. Victor Arrial, Giulio Guerrieri, and Delia Kesner. The benefits of diligence. International Joint Conference on Automated Reasoning, IJCAR 2024,, 2024. Google Scholar
  4. Pablo Arrighi, Alejandro Díaz-Caro, and Benoît Valiron. The vectorial lambda-calculus. Information and Computation, 254:105-139, 2017. URL: https://doi.org/10.1016/j.ic.2017.04.001.
  5. Pablo Arrighi and Gilles Dowek. Lineal: A linear-algebraic lambda-calculus. Logical Methods in Computer Science, 13(1), 2017. URL: https://doi.org/10.23638/LMCS-13(1:8)2017.
  6. Martin Avanzini, Ugo Dal Lago, and Akihisa Yamada. On probabilistic term rewriting. Sci. Comput. Program., 185, 2020. URL: https://doi.org/10.1016/J.SCICO.2019.102338.
  7. Hendrik Pieter Barendregt. The Lambda Calculus - Its Syntax and Semantics, volume 103 of Studies in logic and the foundations of mathematics. North-Holland, 1984. Google Scholar
  8. Benjamin Bichsel, Maximilian Baader, Timon Gehr, and Martin T. Vechev. Silq: a high-level quantum language with safe uncomputation and intuitive semantics. In Alastair F. Donaldson and Emina Torlak, editors, Proceedings of the 41st ACM SIGPLAN International Conference on Programming Language Design and Implementation, PLDI'20, pages 286-300. ACM, 2020. URL: https://doi.org/10.1145/3385412.3386007.
  9. Olivier Bournez and Florent Garnier. Proving positive almost sure termination under strategies. In Rewriting Techniques and Applications, RTA, pages 357-371, 2006. URL: https://doi.org/10.1007/11805618_27.
  10. Antonio Bucciarelli, Delia Kesner, Alejandro Ríos, and Andrés Viso. The bang calculus revisited. Inf. Comput., 293:105047, 2023. URL: https://doi.org/10.1016/J.IC.2023.105047.
  11. Christophe Chareton, Sébastien Bardin, Franccois Bobot, Valentin Perrelle, and Benoît Valiron. An automated deductive verification framework for circuit-building quantum programs. In Nobuko Yoshida, editor, Proceedings of the 30th European Symposium on Programming Languages and Systems, ESOP 2021, volume 12648 of Lecture Notes in Computer Science, pages 148-177. Springer, 2021. URL: https://doi.org/10.1007/978-3-030-72019-3_6.
  12. Ugo Dal Lago, Claudia Faggian, Benoît Valiron, and Akira Yoshimizu. The geometry of parallelism: classical, probabilistic, and quantum effects. In Giuseppe Castagna and Andrew D. Gordon, editors, Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2017, Paris, France, January 18-20, 2017, pages 833-845. ACM, 2017. URL: https://doi.org/10.1145/3009837.
  13. Ugo Dal Lago, Andrea Masini, and Margherita Zorzi. On a measurement-free quantum lambda calculus with classical control. Math. Struct. Comput. Sci., 19(2):297-335, 2009. URL: https://doi.org/10.1017/S096012950800741X.
  14. Ugo Dal Lago, Andrea Masini, and Margherita Zorzi. Confluence results for a quantum lambda calculus with measurements. Electr. Notes Theor. Comput. Sci., 270(2):251-261, 2011. URL: https://doi.org/10.1016/j.entcs.2011.01.035.
  15. Ugo Dal Lago and Margherita Zorzi. Probabilistic operational semantics for the lambda calculus. RAIRO Theor. Informatics Appl., 46(3):413-450, 2012. URL: https://doi.org/10.1051/ita/2012012.
  16. Ugo de'Liguoro and Adolfo Piperno. Non deterministic extensions of untyped lambda-calculus. Inf. Comput., 122(2):149-177, 1995. URL: https://doi.org/10.1006/INCO.1995.1145.
  17. Alessandra Di Pierro, Chris Hankin, and Herbert Wiklicky. Probabilistic lambda-calculus and quantitative program analysis. J. Log. Comput., 15(2):159-179, 2005. URL: https://doi.org/10.1093/LOGCOM/EXI008.
  18. Alejandro Díaz-Caro, Mauricio Guillermo, Alexandre Miquel, and Benoît Valiron. Realizability in the unitary sphere. In Proceedings of the 34th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS'19, pages 1-13. IEEE, 2019. URL: https://doi.org/10.1109/LICS.2019.8785834.
  19. Alejandro Díaz-Caro and Guido Martinez. Confluence in probabilistic rewriting. Electr. Notes Theor. Comput. Sci., 338:115-131, 2018. Google Scholar
  20. Thomas Ehrhard and Giulio Guerrieri. The bang calculus: an untyped lambda-calculus generalizing call-by-name and call-by-value. In Proceedings of the 18th International Symposium on Principles and Practice of Declarative Programming (PPDP 2016), pages 174-187. ACM, 2016. URL: https://doi.org/10.1145/2967973.2968608.
  21. Thomas Ehrhard, Michele Pagani, and Christine Tasson. The computational meaning of probabilistic coherence spaces. In Proceedings of the 26th Annual IEEE Symposium on Logic in Computer Science, LICS 2011, June 21-24, 2011, Toronto, Ontario, Canada, pages 87-96. IEEE Computer Society, 2011. URL: https://doi.org/10.1109/LICS.2011.29.
  22. Claudia Faggian. Probabilistic rewriting: Normalization, termination, and unique normal forms. In Herman Geuvers, editor, 4th International Conference on Formal Structures for Computation and Deduction, FSCD 2019, June 24-30, 2019, Dortmund, Germany, volume 131 of LIPIcs, pages 19:1-19:25. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2019. URL: https://doi.org/10.4230/LIPICS.FSCD.2019.19.
  23. Claudia Faggian. Probabilistic rewriting and asymptotic behaviour: on termination and unique normal forms. Log. Methods Comput. Sci., 18(2), 2022. URL: https://doi.org/10.46298/LMCS-18(2:5)2022.
  24. Claudia Faggian and Giulio Guerrieri. Factorization in call-by-name and call-by-value calculi via linear logic. In Foundations of Software Science and Computation Structures - 24th International Conference, FOSSACS 2021, volume 12650 of Lecture Notes in Computer Science, pages 205-225. Springer, 2021. URL: https://doi.org/10.1007/978-3-030-71995-1_11.
  25. Claudia Faggian, Gaetan Lopez, and Benoît Valiron. A rewriting theory for quantum λ-calculus. CoRR, abs/2411.14856, 2024. URL: https://arxiv.org/abs/2411.14856.
  26. Claudia Faggian and Simona Ronchi Della Rocca. Lambda calculus and probabilistic computation. In 34th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2019, Vancouver, BC, Canada, June 24-27, 2019, pages 1-13. IEEE, 2019. URL: https://doi.org/10.1109/LICS.2019.8785699.
  27. Francesco Gavazzo and Claudia Faggian. A relational theory of monadic rewriting systems, part I. In 36th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2021, Rome, Italy, June 29 - July 2, 2021, pages 1-14. IEEE, 2021. URL: https://doi.org/10.1109/LICS52264.2021.9470633.
  28. Simon J. Gay. Quantum programming languages: survey and bibliography. Mathematical Structures in Computer Science, 16(4):581-600, 2006. URL: https://doi.org/10.1017/S0960129506005378.
  29. Jean-Yves Girard. Linear logic. Theor. Comput. Sci., 50:1-102, 1987. URL: https://doi.org/10.1016/0304-3975(87)90045-4.
  30. Alexander S. Green, Peter LeFanu Lumsdaine, Neil J. Ross, Peter Selinger, and Benoît Valiron. Quipper: A scalable quantum programming language. In Hans-Juergen Boehm and Cormac Flanagan, editors, Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI'13, pages 333-342. ACM, 2013. URL: https://doi.org/10.1145/2491956.2462177.
  31. Giulio Guerrieri and Giulio Manzonetto. The bang calculus and the two Girard’s translations. In Proceedings Joint International Workshop on Linearity & Trends in Linear Logic and Applications (Linearity-TLLA 2018), volume 292 of EPTCS, pages 15-30, 2019. URL: https://doi.org/10.4204/EPTCS.292.2.
  32. Jan-Christoph Kassing, Florian Frohn, and Jürgen Giesl. From innermost to full almost-sure termination of probabilistic term rewriting. In Naoki Kobayashi and James Worrell, editors, Foundations of Software Science and Computation Structures - 27th International Conference, FoSSaCS 2024, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2024, Luxembourg City, Luxembourg, April 6-11, 2024, Proceedings, Part II, volume 14575 of Lecture Notes in Computer Science, pages 206-228. Springer, 2024. URL: https://doi.org/10.1007/978-3-031-57231-9_10.
  33. Maja H. Kirkeby and Henning Christiansen. Confluence and convergence in probabilistically terminating reduction systems. In Logic-Based Program Synthesis and Transformation - 27th International Symposium, LOPSTR 2017, pages 164-179, 2017. URL: https://doi.org/10.1007/978-3-319-94460-9_10.
  34. Emanuel H. Knill. Conventions for quantum pseudocode. Technical Report LAUR-96-2724, Los Alamos National Laboratory, Los Alamos, New Mexico, US., 1996. Google Scholar
  35. Dongho Lee, Valentin Perrelle, Benoît Valiron, and Zhaowei Xu. Concrete categorical model of a quantum circuit description language with measurement. In Mikolaj Bojanczyk and Chandra Chekuri, editors, Proceedings of the 41st IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2021, volume 213 of LIPIcs, pages 51:1-51:20, 2021. URL: https://doi.org/10.4230/LIPIcs.FSTTCS.2021.51.
  36. M.H.A. Newman. On theories with a combinatorial definition of equivalence. Annals of Mathematics, 43(2), 1942. Google Scholar
  37. Michael A. Nielsen and Isaac L. Chuang. Quantum Computation and Quantum Information. Cambridge University Press, 2002. Google Scholar
  38. Michele Pagani, Peter Selinger, and Benoît Valiron. Applying quantitative semantics to higher-order quantum computing. In Suresh Jagannathan and Peter Sewell, editors, Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL'14), pages 647-658. ACM, 2014. URL: https://doi.org/10.1145/2535838.2535879.
  39. Luca Paolini, Mauro Piccolo, and Margherita Zorzi. qPCF: higher-order languages and quantum circuits. Journal of Automated Reasoning, 63(4):941-966, 2019. URL: https://doi.org/10.1007/s10817-019-09518-y.
  40. Jennifer Paykin, Robert Rand, and Steve Zdancewic. QWIRE: a core language for quantum circuits. In Giuseppe Castagna and Andrew D. Gordon, editors, Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL'17, pages 846-858. ACM, 2017. URL: https://doi.org/10.1145/3009837.3009894.
  41. Gordon D. Plotkin. Call-by-name, call-by-value and the lambda-calculus. Theor. Comput. Sci., 1(2):125-159, 1975. URL: https://doi.org/10.1016/0304-3975(75)90017-1.
  42. Peter Selinger and Benoît Valiron. A lambda calculus for quantum computation with classical control. Mathematical Structures in Computer Science, 16:527-552, 2006. URL: https://doi.org/10.1017/S0960129506005238.
  43. Alex K. Simpson. Reduction in a linear lambda-calculus with applications to operational semantics. In Term Rewriting and Applications, 16th International Conference (RTA 2005), volume 3467 of Lecture Notes in Computer Science, pages 219-234, 2005. URL: https://doi.org/10.1007/978-3-540-32033-3_17.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact