Document Open Access Logo

Equational Reasoning in Languages with Binders via Permutation Fixed-Points

Authors Ali K. Caires-Santos , Maribel Fernández , Murdoch James Gabbay , Daniele Nantes-Sobrinho

PDF

File

Thumbnail PDF
PDF
LIPIcs.FSCD.2026.10.pdf
  • Filesize: 1 MB
  • 23 pages

Document Identifiers

Subject Classification

ACM Subject Classification
  • Theory of computation → Logic and verification
  • Theory of computation → Lambda calculus
  • Theory of computation → Equational logic and rewriting
Keywords
  • Binding
  • alpha-equivalence
  • nominal algebra
  • permutation fixed-point

Metrics

Abstract

Equational reasoning with binders and structural congruence is difficult due to the interaction between name binding and algebraic laws. Equational theories such as commutativity induce forms of permutation invariance on names that are not captured by standard approaches to the formalisation of syntax with binders. 
We show that in the nominal setting, this limitation can be addressed by using generalised permutation fixed-point constraints to make invariance explicit. This yields a uniform framework for reasoning about equality of nominal terms modulo α-equivalence and arbitrary equational theories. We introduce a proof system and show that it is sound and complete with respect to a nominal-set semantics, which explains how symmetry can be internalised via fixed-point constraints viewed as N-quantified stabiliser conditions. We provide examples in Milner’s π-calculus - a well-known model of concurrent computation that includes binders and non-trivial structural congruences.

Cite As Get BibTex

Ali K. Caires-Santos, Maribel Fernández, Murdoch James Gabbay, and Daniele Nantes-Sobrinho. Equational Reasoning in Languages with Binders via Permutation Fixed-Points. In 11th International Conference on Formal Structures for Computation and Deduction (FSCD 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 378, pp. 10:1-10:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026) https://doi.org/10.4230/LIPIcs.FSCD.2026.10

Author Details

Ali K. Caires-Santos
  • University of Brasília, Brasília, Brazil
Maribel Fernández
  • King’s College London, London, United Kingdom
Murdoch James Gabbay
  • Heriot-Watt University, Edinburgh, United Kingdom
Daniele Nantes-Sobrinho
  • University of Brasília, Brasília, Brazil

Funding

This paper was partially funded by Royal Society IES\R3\243187.

Acknowledgements

We thank the anonymous referees for their valuable comments and suggestions, which have substantially improved the quality of this paper.

References

  1. Mauricio Ayala-Rincón, Maribel Fernández, and Daniele Nantes-Sobrinho. On Nominal Syntax and Permutation Fixed Points. Log. Methods Comput. Sci., 16(1):19:1-19:36, 2020. URL: https://doi.org/10.23638/LMCS-16(1:19)2020.
  2. Franz Baader and Tobias Nipkow. Term Rewriting and All That. Cambridge University Press, 1998. URL: https://doi.org/10.1017/CBO9781139172752.
  3. Mikolaj Bojanczyk, Bartek Klin, and Slawomir Lasota. Automata theory in nominal sets. Log. Methods Comput. Sci., 10(3), 2014. URL: https://doi.org/10.2168/LMCS-10(3:4)2014.
  4. Stanley Burris and Hanamantagouda P. Sankappanavar. A Course in Universal Algebra, volume 78 of Graduate Texts in Mathematics. Springer, 1981. URL: https://link.springer.com/book/9781461381327.
  5. Ali K. Caires-Santos, Maribel Fernández, and Daniele Nantes-Sobrinho. Equational Reasoning Modulo Commutativity in Languages with Binders. In Automated Deduction – CADE 30: 30th International Conference on Automated Deduction, Stuttgart, Germany, July 28-31, 2025, Proceedings, pages 632-652, Berlin, Heidelberg, 2025. Springer-Verlag. URL: https://doi.org/10.1007/978-3-031-99984-0_33.
  6. Ali K. Caires-Santos, Maribel Fernández, and Daniele Nantes-Sobrinho. Strong Nominal Semantics for Fixed-Point Constraints. Electronic Notes in Theoretical Informatics and Computer Science, Proceedings of MFPS XL., 4, December 2024. URL: https://doi.org/10.46298/entics.14777.
  7. Arthur Charguéraud. The locally nameless representation. J. Autom. Reason., 49(3):363-408, 2012. URL: https://doi.org/10.1007/s10817-011-9225-2.
  8. Manuel Clavel, Francisco Durán, Steven Eker, Patrick Lincoln, Narciso Martí-Oliet, José Meseguer, and Carolyn L. Talcott, editors. All About Maude - A High-Performance Logical Framework, volume 4350 of LNCS. Springer, 2007. URL: https://doi.org/10.1007/978-3-540-71999-1.
  9. N.G de Bruijn. Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the church-rosser theorem. Indagationes Mathematicae (Proceedings), 75(5):381-392, 1972. URL: https://doi.org/10.1016/1385-7258(72)90034-0.
  10. Francisco Durán, Santiago Escobar, Jose Meseguer, and Julia Sapiña. Nuitp: An inductive theorem prover for equational program verification. In Proceedings of the 26th International Symposium on Principles and Practice of Declarative Programming, PPDP '24, New York, NY, USA, 2024. Association for Computing Machinery. URL: https://doi.org/10.1145/3678232.3678236.
  11. Amy P. Felty, Alberto Momigliano, and Brigitte Pientka. The next 700 challenge problems for reasoning with higher-order abstract syntax representations - part 2 - A survey. J. Autom. Reason., 55(4):307-372, 2015. URL: https://doi.org/10.1007/s10817-015-9327-3.
  12. Maribel Fernández and Murdoch James Gabbay. Nominal Rewriting. Inf. Comput., 205(6):917-965, 2007. URL: https://doi.org/10.1016/j.ic.2006.12.002.
  13. Murdoch James Gabbay. Nominal Algebra and the HSP Theorem. J. Log. Comput., 19(2):341-367, 2009. URL: https://doi.org/10.1093/logcom/exn055.
  14. Murdoch James Gabbay. Foundations of Nominal Techniques: Logic and Semantics of Variables in Abstract Syntax. Bull. Symb. Log., 17(2):161-229, 2011. URL: https://doi.org/10.2178/bsl/1305810911.
  15. Murdoch James Gabbay and Aad Mathijssen. Nominal (Universal) Algebra: Equational Logic with Names and Binding. J. Log. Comput., 19(6):1455-1508, 2009. URL: https://doi.org/10.1093/logcom/exp033.
  16. Murdoch James Gabbay and Andrew M. Pitts. A New Approach to Abstract Syntax with Variable Binding. Formal Aspects Comput., 13(3-5):341-363, 2002. URL: https://doi.org/10.1007/s001650200016.
  17. Alexander Kurz and Daniela Petrişan. On universal algebra over nominal sets. Mathematical Structures in Computer Science, 20(2):285-318, 2010. URL: https://doi.org/10.1017/S0960129509990399.
  18. José Meseguer. Inductive reasoning with equality predicates, contextual rewriting and variant-based simplification. J. Log. Algebraic Methods Program., 144:101036, 2025. URL: https://doi.org/10.1016/j.jlamp.2025.101036.
  19. Robin Milner, Joachim Parrow, and David Walker. A Calculus of Mobile Processes, I. Information and Computation, 100(1):1-40, 1992. URL: https://doi.org/10.1016/0890-5401(92)90008-4.
  20. Peter W. O'Hearn, John C. Reynolds, and Hongseok Yang. Local reasoning about programs that alter data structures. In Laurent Fribourg, editor, Computer Science Logic (CSL 2001), volume 2142 of Lecture Notes in Computer Science, pages 1-19, Berlin, Heidelberg, 2001. Springer. URL: https://doi.org/10.1007/3-540-44802-0_1.
  21. F. Pfenning and C. Elliott. Higher-Order Abstract Syntax. SIGPLAN Not., 23(7):199-208, 1988. URL: https://doi.org/10.1145/960116.54010.
  22. Andrew M. Pitts. Nominal Sets: Names and Symmetry in Computer Science. Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 2013. URL: https://doi.org/10.1017/CBO9781139084673.
  23. Andrei Popescu. Nominal recursors as epi-recursors. Proc. ACM Program. Lang., 8(POPL):425-456, 2024. URL: https://doi.org/10.1145/3632857.
  24. John C. Reynolds. Separation logic: A logic for shared mutable data structures. In Proceedings of the 17th Annual IEEE Symposium on Logic in Computer Science (LICS 2002), pages 55-74, Washington, DC, USA, 2002. IEEE Computer Society. URL: https://doi.org/10.1109/LICS.2002.1029817.
  25. Joseph J. Rotman. An Introduction to the Theory of Groups, volume 148 of Graduate Texts in Mathematics. Springer, New York, 4 edition, 1995. URL: https://link.springer.com/book/10.1007/978-1-4612-4176-8.
  26. Christian Urban, Andrew M. Pitts, and Murdoch James Gabbay. Nominal Unification. Theor. Comput. Sci., 323(1-3):473-497, 2004. URL: https://doi.org/10.1016/j.tcs.2004.06.016.
  27. Jan van Brügge, James McKinna, Andrei Popescu, and Dmitriy Traytel. Barendregt convenes with Knaster and Tarski: Strong rule induction for syntax with bindings. Proc. ACM Program. Lang., 9(POPL):1687-1718, 2025. URL: https://doi.org/10.1145/3704893.
Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

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