Document Open Access Logo

On Coinduction and Quantum Lambda Calculi

Authors Yuxin Deng, Yuan Feng, Ugo Dal Lago

PDF
Thumbnail PDF

File

LIPIcs.CONCUR.2015.427.pdf
  • Filesize: 0.56 MB
  • 14 pages

Document Identifiers

Author Details

Yuxin Deng
Yuan Feng
Ugo Dal Lago

Cite As Get BibTex

Yuxin Deng, Yuan Feng, and Ugo Dal Lago. On Coinduction and Quantum Lambda Calculi. In 26th International Conference on Concurrency Theory (CONCUR 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 42, pp. 427-440, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015) https://doi.org/10.4230/LIPIcs.CONCUR.2015.427

Abstract

In the ubiquitous presence of linear resources in quantum computation, program equivalence in linear contexts, where programs are used or executed once, is more important than in the classical setting. We introduce a linear contextual equivalence and two notions of bisimilarity, a state-based and a distribution-based, as proof techniques for reasoning about higher-order quantum programs. Both notions of bisimilarity are sound with respect to the linear contextual equivalence, but only the distribution-based one turns out to be complete. The completeness proof relies on a characterisation of the bisimilarity as a testing equivalence.

Subject Classification

Keywords
  • Quantum lambda calculi
  • contextual equivalence
  • bisimulation

Metrics

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

References

  1. Samson Abramsky. The lazy lambda calculus. In Research Topics in Functional Programming, pages 65-116. Addison-Wesley, 1999. Google Scholar
  2. Raphaëlle Crubillé and Ugo Dal Lago. On probabilistic applicative bisimulation and call-by-value λ-calculi. In ESOP'14, volume 8410 of LNCS, pages 209-228. Springer, 2014. Google Scholar
  3. Ugo Dal Lago and Alessandro Rioli. Applicative bisimulation and quantum λ-calculi (long version). CoRR, abs/1506.06661, 2015. Google Scholar
  4. Ugo Dal Lago, Davide Sangiorgi, and Michele Alberti. On coinductive equivalences for higher-order probabilistic functional programs. In POPL'14, pages 297-308. ACM, 2014. Google Scholar
  5. Timothy A.S. Davidson. Formal verification techniques using quantum process calculus. PhD thesis, University of Warwick, 2011. Google Scholar
  6. Yuxin Deng. Semantics of Probabilistic Processes: An Operational Approach. Springer, 2014. Google Scholar
  7. Yuxin Deng, Rob van Glabbeek, Matthew Hennessy, and Carroll Morgan. Testing finitary probabilistic processes (extended abstract). In CONCUR'09, volume 5710 of LNCS, pages 274-288. Springer, 2009. Google Scholar
  8. Yuxin Deng and Yu Zhang. Program equivalence in linear contexts. Theoretical Computer Science, 585:71-90, 2015. Google Scholar
  9. Josée Desharnais. Labelled Markov Processes. PhD thesis, McGill University, 1999. Google Scholar
  10. Yuan Feng, Yuxin Deng, and Mingsheng Ying. Symbolic bisimulation for quantum processes. ACM Transactions on Computational Logic, 15(2):1-32, 2014. Google Scholar
  11. Yuan Feng, Runyao Duan, Zheng-Feng Ji, and Mingsheng Ying. Probabilistic bisimulations for quantum processes. Information and Computation, 205(11):1608-1639, 2007. Google Scholar
  12. Yuan Feng, Runyao Duan, and Mingsheng Ying. Bisimulation for quantum processes. ACM Transactions on Programming Languages and Systems, 34(4):17, 2012. Google Scholar
  13. Yuan Feng and Lijun Zhang. When equivalence and bisimulation join forces in probabilistic automata. In FM'14, volume 8442 of LNCS, pages 247-262. Springer, 2014. Google Scholar
  14. Andrew M. Gordon. A tutorial on co-induction and functional programming. In Glasgow Workshop on Functional Programming, pages 78-95. Springer, 1995. Google Scholar
  15. Alexander S. Green, Peter LeFanu Lumsdaine, Neil J. Ross, Peter Selinger, and Benoît Valiron. Quipper: a scalable quantum programming language. In PLDI'13, pages 333-342. ACM, 2013. Google Scholar
  16. Lov K. Grover. A fast quantum mechanical algorithm for database search. In STOC'96, pages 212-219. ACM, 1996. Google Scholar
  17. Lov K. Grover. Quantum mechanics helps in searching for a needle in a haystack. Physical Review Letters, 79:325-328, 1997. Google Scholar
  18. Holger Hermanns, Jan Krcál, and Jan Kretínský. Probabilistic bisimulation: Naturally on distributions. In CONCUR'14, volume 8704 of LNCS, pages 249-265. Springer, 2014. Google Scholar
  19. Douglas J. Howe. Proving congruence of bisimulation in functional programming languages. Information and Computation, 124(2):103-112, 1996. Google Scholar
  20. Emanuel Knill. Conventions for quantum pseudocode. Technical Report LAUR-96-2724, Los Alamos National Laboratory, 1996. Google Scholar
  21. Marie Lalire. Relations among quantum processes: bisimilarity and congruence. Mathematical Structures in Computer Science, 16(3):407-428, 2006. Google Scholar
  22. Kim G. Larsen and Arne Skou. Bisimulation through probabilistic testing. Information and Computation, 94(1):1-28, 1991. Google Scholar
  23. James H. Morris. Lambda Calculus Models of Programming Languages. PhD thesis, MIT, 1969. Google Scholar
  24. Michele Pagani, Peter Selinger, and Benoît Valiron. Applying quantitative semantics to higher-order quantum computing. In POPL'14, pages 647-658. ACM, 2014. Google Scholar
  25. Andrew M. Pitts. Operationally-based theories of program equivalence. In Semantics and Logics of Computation, pages 241-298. Cambridge University Press, 1997. Google Scholar
  26. Andrew M. Pitts. Howe’s method for higher-order languages. In Advanced Topics in Bisimulation and Coinduction, pages 197-232. Cambridge University Press, 2011. Google Scholar
  27. Joshua Sack and Lijun Zhang. A general framework for probabilistic characterizing formulae. In VMCAI'12, volume 7148 of LNCS, pages 396-411. Springer, 2012. Google Scholar
  28. Peter Selinger. Towards a quantum programming language. Mathematical Structures in Computer Science, 14(4):527-586, 2004. Google Scholar
  29. Peter Selinger and Benoît Valiron. A lambda calculus for quantum computation with classical control. Mathematical Structures in Computer Science, 16(3):527-552, 2006. Google Scholar
  30. Peter Selinger and Benoît Valiron. A linear-non-linear model for a computational call-by-value lambda calculus (extended abstract). In FOSSACS'08, volume 4962 of LNCS, pages 81-96. Springer, 2008. Google Scholar
  31. Peter Selinger and Benoît Valiron. On a fully abstract model for a quantum linear functional language (extended abstract). Electronic Notes in Theoretical Computer Science, 210:123-137, 2008. Google Scholar
  32. Peter W. Shor. Algorithms for quantum computation: Discrete logarithms and factoring. In FOCS'94, pages 124-134. IEEE Computer Society, 1994. Google Scholar
  33. Franck van Breugel, Michael W. Mislove, Joël Ouaknine, and James Worrell. Domain theory, testing and simulation for labelled markov processes. Theoretical Computer Science, 333(1-2):171-197, 2005. Google Scholar
  34. Dave Wecker and Krysta M. Svore. LIQUi|greater: A software design architecture and domain-specific language for quantum computing. CoRR, abs/1402.4467, 2014. Google Scholar
  35. Mingsheng Ying. Quantum recursion and second quantisation: Basic ideas and examples. CoRR, abs/1405.4443, 2014. Google Scholar
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-2024 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact