Translating Finite-Typed Symmetric Pattern Matching into Ket
Resumo
We present a translation procedure from Symmetric Pattern Matching (SPM) isomorphisms to executable quantum programs in Ket. Our approach exploits the preservation structure of pattern-matching clauses to identify control configurations, allowing high-level specifications to be rewritten as controlled quantum operations. Isomorphisms are first interpreted as unitary operators and then translated into Ket through a multiplexer-based decomposition, while singlequbit leaf operations are synthesized via ZYZ decomposition. As a first step toward compiling the full SPM framework, we restrict our attention to finite types and to isomorphisms whose non-controlled leaf operations act on a single qubit. This work contributes to bridging high-level reversible programming abstractions and practical quantum programming frameworks.
Palavras-chave:
Quantum Computing, Quantum Programming Languages, Reversible Computing
Referências
T. Altenkirch and J. Grattage. 2005. A functional quantum programming language. In 20th Annual IEEE Symposium on Logic in Computer Science (LICS’ 05). 249–258. DOI: 10.1109/LICS.2005.1
Pablo Arrighi and Gilles Dowek. 2017. Lineal: A linear-algebraic Lambda-calculus. Logical Methods in Computer Science Volume 13, Issue 1 (03 2017). DOI: 10.23638/LMCS-13(1:8)2017
Ali Assaf, Alejandro Díaz-Caro, Simon Perdrix, Christine Tasson, and Benoît Valiron. 2010. Call-by-value, call-by-name and the vectorial behaviour of the algebraic 𝜆-calculus. Log. Methods Comput. Sci. 10 (2010). [link]
Ville Bergholm, Juha J. Vartiainen, Mikko Möttönen, and Martti M. Salomaa. 2005. Quantum circuits with uniformly controlled onequbit gates. Phys. Rev. A 71 (May 2005), 052330. Issue 5. DOI: 10.1103/PhysRevA.71.052330
Evandro Chagas Ribeiro Da Rosa and Rafael De Santiago. 2021. Ket Quantum Programming. J. Emerg. Technol. Comput. Syst. 18, 1, Article 12 (Oct. 2021), 25 pages. DOI: 10.1145/3474224
Liliane-Joy Dandy, Emmanuel Jeandel, and Vladimir Zamdzhiev. 2023. Type-safe Quantum Programming in Idris. In Programming Languages and Systems: 32nd European Symposium on Programming, ESOP 2023, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2023, Paris, France, April 22–27, 2023, Proceedings (Paris, France). Springer-Verlag, Berlin, Heidelberg, 507–534. DOI: 10.1007/978-3-031-30044-8_19
José Alex de Carvalho, Carlos Batista, Tiago de Veras, Israel Araujo, and Adenilton José da Silva. 2025. Quantum Multiplexer Simplification for State Preparation. ACM Transactions on Quantum Computing 6, 4, Article 26 (Aug. 2025), 12 pages. DOI: 10.1145/3748260
Roshan P. James. 2014. Theseus : A High Level Language for Reversible Computing. [link]
Navin Khaneja and Steffen J. Glaser. 2001. Cartan decomposition of SU(2n) and control of spin systems. Chemical Physics 267, 1 (2001), 11–23. DOI: 10.1016/S0301-0104(01)00318-4
Mikko Möttönen, Juha J. Vartiainen, Ville Bergholm, and Martti M. Salomaa. 2004. Quantum Circuits for General Multiqubit Gates. Phys. Rev. Lett. 93 (Sep 2004), 130502. Issue 13. DOI: 10.1103/PhysRevLett.93.130502
Mikko Möttönen, Juha J. Vartiainen, Ville Bergholm, and Martti M. Salomaa. 2005. Transformation of quantum states using uniformly controlled rotations. Quantum Info. Comput. 5, 6 (Sept. 2005), 467–473.
Michael A. Nielsen and Isaac L. Chuang. 2010. Quantum Computation and Quantum Information: 10th Anniversary Edition. Cambridge University Press.
Jennifer Paykin, Robert Rand, and Steve Zdancewic. 2017. QWIRE: a core language for quantum circuits. In Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages (Paris, France) (POPL ’17). Association for Computing Machinery, New York, NY, USA, 846–858. DOI: 10.1145/3009837.3009894
Amr Sabry, Benoît Valiron, and Juliana Kaizer Vizzotto. 2018. From Symmetric Pattern-Matching to Quantum Control. In Foundations of Software Science and Computation Structures, Christel Baier and Ugo Dal Lago (Eds.). Springer International Publishing, Cham, 348–364.
V.V. Shende, S.S. Bullock, and I.L. Markov. 2006. Synthesis of quantumlogic circuits. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems 25, 6 (2006), 1000–1010.
Benoît Valiron. 2024. On Quantum Programming Languages. DOI: 10.48550/arXiv.2410.13337
André van Tonder. 2004. A Lambda Calculus for Quantum Computation. SIAM J. Comput. 33, 5 (2004), 1109–1135. DOI: 10.1137/S0097539703432165
Andre van Tonder and Miquel Dorca. 2003. Quantum computation, categorical semantics and linear logic. (10 2003). arXiv:quant-ph/0312174
LIONEL VAUX. 2009. The algebraic lambda calculus. Mathematical Structures in Computer Science 19, 5 (2009), 1029–1059. DOI: 10.1017/S0960129509990089
Pablo Arrighi and Gilles Dowek. 2017. Lineal: A linear-algebraic Lambda-calculus. Logical Methods in Computer Science Volume 13, Issue 1 (03 2017). DOI: 10.23638/LMCS-13(1:8)2017
Ali Assaf, Alejandro Díaz-Caro, Simon Perdrix, Christine Tasson, and Benoît Valiron. 2010. Call-by-value, call-by-name and the vectorial behaviour of the algebraic 𝜆-calculus. Log. Methods Comput. Sci. 10 (2010). [link]
Ville Bergholm, Juha J. Vartiainen, Mikko Möttönen, and Martti M. Salomaa. 2005. Quantum circuits with uniformly controlled onequbit gates. Phys. Rev. A 71 (May 2005), 052330. Issue 5. DOI: 10.1103/PhysRevA.71.052330
Evandro Chagas Ribeiro Da Rosa and Rafael De Santiago. 2021. Ket Quantum Programming. J. Emerg. Technol. Comput. Syst. 18, 1, Article 12 (Oct. 2021), 25 pages. DOI: 10.1145/3474224
Liliane-Joy Dandy, Emmanuel Jeandel, and Vladimir Zamdzhiev. 2023. Type-safe Quantum Programming in Idris. In Programming Languages and Systems: 32nd European Symposium on Programming, ESOP 2023, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2023, Paris, France, April 22–27, 2023, Proceedings (Paris, France). Springer-Verlag, Berlin, Heidelberg, 507–534. DOI: 10.1007/978-3-031-30044-8_19
José Alex de Carvalho, Carlos Batista, Tiago de Veras, Israel Araujo, and Adenilton José da Silva. 2025. Quantum Multiplexer Simplification for State Preparation. ACM Transactions on Quantum Computing 6, 4, Article 26 (Aug. 2025), 12 pages. DOI: 10.1145/3748260
Roshan P. James. 2014. Theseus : A High Level Language for Reversible Computing. [link]
Navin Khaneja and Steffen J. Glaser. 2001. Cartan decomposition of SU(2n) and control of spin systems. Chemical Physics 267, 1 (2001), 11–23. DOI: 10.1016/S0301-0104(01)00318-4
Mikko Möttönen, Juha J. Vartiainen, Ville Bergholm, and Martti M. Salomaa. 2004. Quantum Circuits for General Multiqubit Gates. Phys. Rev. Lett. 93 (Sep 2004), 130502. Issue 13. DOI: 10.1103/PhysRevLett.93.130502
Mikko Möttönen, Juha J. Vartiainen, Ville Bergholm, and Martti M. Salomaa. 2005. Transformation of quantum states using uniformly controlled rotations. Quantum Info. Comput. 5, 6 (Sept. 2005), 467–473.
Michael A. Nielsen and Isaac L. Chuang. 2010. Quantum Computation and Quantum Information: 10th Anniversary Edition. Cambridge University Press.
Jennifer Paykin, Robert Rand, and Steve Zdancewic. 2017. QWIRE: a core language for quantum circuits. In Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages (Paris, France) (POPL ’17). Association for Computing Machinery, New York, NY, USA, 846–858. DOI: 10.1145/3009837.3009894
Amr Sabry, Benoît Valiron, and Juliana Kaizer Vizzotto. 2018. From Symmetric Pattern-Matching to Quantum Control. In Foundations of Software Science and Computation Structures, Christel Baier and Ugo Dal Lago (Eds.). Springer International Publishing, Cham, 348–364.
V.V. Shende, S.S. Bullock, and I.L. Markov. 2006. Synthesis of quantumlogic circuits. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems 25, 6 (2006), 1000–1010.
Benoît Valiron. 2024. On Quantum Programming Languages. DOI: 10.48550/arXiv.2410.13337
André van Tonder. 2004. A Lambda Calculus for Quantum Computation. SIAM J. Comput. 33, 5 (2004), 1109–1135. DOI: 10.1137/S0097539703432165
Andre van Tonder and Miquel Dorca. 2003. Quantum computation, categorical semantics and linear logic. (10 2003). arXiv:quant-ph/0312174
LIONEL VAUX. 2009. The algebraic lambda calculus. Mathematical Structures in Computer Science 19, 5 (2009), 1029–1059. DOI: 10.1017/S0960129509990089
Publicado
08/09/2026
Como Citar
BORIN JÚNIOR, Flávio; VIZZOTTO, Juliana Kaizer.
Translating Finite-Typed Symmetric Pattern Matching into Ket. In: SIMPÓSIO BRASILEIRO DE LINGUAGENS DE PROGRAMAÇÃO (SBLP), 30. , 2026, São Paulo/SP.
Anais [...].
Porto Alegre: Sociedade Brasileira de Computação,
2026
.
p. 141-149.
DOI: https://doi.org/10.5753/sblp.2026.29675.
