Document Open Access Logo

Fixed-Point Constraints for Nominal Equational Unification

Authors Mauricio Ayala-Rincón, Maribel Fernández, Daniele Nantes-Sobrinho

Thumbnail PDF


  • Filesize: 0.63 MB
  • 16 pages

Document Identifiers

Author Details

Mauricio Ayala-Rincón
  • Departments of Mathematics and Computer Science, Universidade de Brasília, Brasília, Brazil
Maribel Fernández
  • Department of Informatics, King’s College London, London, UK
Daniele Nantes-Sobrinho
  • Departments of Mathematics and Computer Science, Universidade de Brasília, Brasília, Brazil

Cite AsGet BibTex

Mauricio Ayala-Rincón, Maribel Fernández, and Daniele Nantes-Sobrinho. Fixed-Point Constraints for Nominal Equational Unification. In 3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 108, pp. 7:1-7:16, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2018)


We propose a new axiomatisation of the alpha-equivalence relation for nominal terms, based on a primitive notion of fixed-point constraint. We show that the standard freshness relation between atoms and terms can be derived from the more primitive notion of permutation fixed-point, and use this result to prove the correctness of the new alpha-equivalence axiomatisation. This gives rise to a new notion of nominal unification, where solutions for unification problems are pairs of a fixed-point context and a substitution. Although it may seem less natural than the standard notion of nominal unifier based on freshness constraints, the notion of unifier based on fixed-point constraints behaves better when equational theories are considered: for example, nominal unification remains finitary in the presence of commutativity, whereas it becomes infinitary when unifiers are expressed using freshness contexts.

Subject Classification

ACM Subject Classification
  • Theory of computation → Equational logic and rewriting
  • Theory of computation → Lambda calculus
  • Theory of computation → Algebraic semantics
  • nominal terms
  • fixed-point equations
  • nominal unification
  • equational theories


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


  1. T. Aoto and K. Kikuchi. A Rule-Based Procedure for Equivariant Nominal Unification. In Pre-proc. of Higher-Order Rewriting (HOR), pages 1-5, 2016. Google Scholar
  2. M. Ayala-Rincón, W. Carvalho-Segundo, M. Fernández, and D. Nantes-Sobrinho. Nominal C-Unification. In Pre-proc. of the 27th Int. Symp. Logic-based Program Synthesis and Transformation (LOPSTR), pages 1-15, 2017. URL:
  3. M. Ayala-Rincón, W. Carvalho-Segundo, M. Fernández, and D. Nantes-Sobrinho. On Solving Nominal Fixpoint Equations. In Proc. of the 11th Int. Symp. on Frontiers of Combining Systems (FroCoS), volume 10483 of Lecture Notes in Computer Science, pages 209-226. Springer, 2017. URL:
  4. M. Ayala-Rincón, W. de Carvalho Segundo, M. Fernández, and D. Nantes-Sobrinho. A formalisation of nominal α-equivalence with A and AC function symbols. Electronic Notes in Theoretical Computer Science, 332:21-38, 2017. URL:
  5. C. F. Calvès. Unifying Nominal Unification. In 24th International Conference on Rewriting Techniques and Applications (RTA 2013), volume 21 of Leibniz International Proceedings in Informatics (LIPIcs), pages 143-157, 2013. URL:
  6. C. F. Calvès and M. Fernández. A Polynomial Nominal Unification Algorithm. Theoretical Computer Science, 403(2-3):285-306, 2008. URL:
  7. J. Cheney. Equivariant unification. Journal of Automated Reasoning, 45(3):267-300, 2010. URL:
  8. M. Fernández and M. J. Gabbay. Nominal Rewriting. Information and Computation, 205(6):917-965, 2007. URL:
  9. M. Fernández, M. J. Gabbay, and I. Mackie. Nominal Rewriting Systems. In Proc. of the 6th Int. Conf. on Principles and Practice of Declarative Programming (PPDP), pages 108-119. ACM Press, 2004. URL:
  10. M. J. Gabbay. A Theory of Inductive Definitions With α-equivalence. PhD thesis, DPMMS and Trinity College, University of Cambridge, 2000. Google Scholar
  11. M. J. Gabbay and A. Mathijssen. Capture-avoiding substitution as a nominal algebra. Formal Aspects of Computing, 20(4-5):451-479, 2008. URL:
  12. M. J. Gabbay and A. M. Pitts. A New Approach to Abstract Syntax with Variable Binding. Formal Aspects of Computing, 13(3-5):341-363, 2002. URL:
  13. A. M. Pitts. Nominal Logic, a First Order Theory of Names and Binding. Information and Computation, 186(2):165-193, 2003. URL:
  14. A. M. Pitts. Nominal Sets: Names and Symmetry in Computer Science. Cambridge University Press, 2013. Google Scholar
  15. M. Schmidt-Schauß, T. Kutsia, J. Levy, and M. Villaret. Nominal Unification of Higher Order Expressions with Recursive Let. In 26th International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR), Revised Selected Papers, volume 10184 of Lecture Notes in Computer Science, pages 328-344, 2016. URL:
  16. C. Urban, A. M. Pitts, and M. J. Gabbay. Nominal Unification. Theoretical Computer Science, 323(1-3):473-497, 2004. URL:
Questions / Remarks / Feedback

Feedback for Dagstuhl Publishing

Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail