Document Open Access Logo

Fixed-Point Constraints for Nominal Equational Unification

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

PDF

File

Thumbnail PDF
PDF
LIPIcs.FSCD.2018.7.pdf
  • Filesize: 0.63 MB
  • 16 pages

Document Identifiers

Subject Classification

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

Metrics

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

Abstract

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.

Cite As Get 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) https://doi.org/10.4230/LIPIcs.FSCD.2018.7

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

Funding

  • Ayala-Rincón, Mauricio: Author partially funded by CNPq 307672/2017-4.
  • Nantes-Sobrinho, Daniele: Author partially supported by FAP-DF 0193.001381/2017.

References

  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: https://arxiv.org/abs/1709.05384.
  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: http://dx.doi.org/10.1007/978-3-319-66167-4_12.
  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: http://dx.doi.org/10.1016/j.entcs.2017.04.003.
  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: http://dx.doi.org/10.4230/LIPIcs.RTA.2013.143.
  6. C. F. Calvès and M. Fernández. A Polynomial Nominal Unification Algorithm. Theoretical Computer Science, 403(2-3):285-306, 2008. URL: http://dx.doi.org/10.1016/j.tcs.2008.05.012.
  7. J. Cheney. Equivariant unification. Journal of Automated Reasoning, 45(3):267-300, 2010. URL: http://dx.doi.org/10.1007/s10817-009-9164-3.
  8. M. Fernández and M. J. Gabbay. Nominal Rewriting. Information and Computation, 205(6):917-965, 2007. URL: http://dx.doi.org/10.1016/j.ic.2006.12.002.
  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: http://dx.doi.org/10.1145/1013963.1013978.
  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: http://dx.doi.org/10.1007/s00165-007-0056-1.
  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: http://dx.doi.org/10.1007/s001650200016.
  13. A. M. Pitts. Nominal Logic, a First Order Theory of Names and Binding. Information and Computation, 186(2):165-193, 2003. URL: http://dx.doi.org/10.1016/S0890-5401(03)00138-X.
  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: http://dx.doi.org/10.1007/978-3-319-63139-4_19.
  16. C. Urban, A. M. Pitts, and M. J. Gabbay. Nominal Unification. Theoretical Computer Science, 323(1-3):473-497, 2004. URL: http://dx.doi.org/10.1016/j.tcs.2004.06.016.
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