LIPIcs.FSCD.2018.7.pdf
- Filesize: 0.63 MB
- 16 pages
Document
Fixed-Point Constraints for Nominal Equational Unification
Authors
-
Part of:
Volume:
3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018)
Series: Leibniz International Proceedings in Informatics (LIPIcs)
Conference: Formal Structures for Computation and Deduction (FSCD) - License:
Creative Commons Attribution 3.0 Unported license
- Publication Date: 2018-07-04
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
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.
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)
0PDF Downloads
References
-
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.
- 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.
- 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.
- 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.
- 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.
- 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.
- J. Cheney. Equivariant unification. Journal of Automated Reasoning, 45(3):267-300, 2010. URL: http://dx.doi.org/10.1007/s10817-009-9164-3.
- 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.
- 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.
-
M. J. Gabbay. A Theory of Inductive Definitions With α-equivalence. PhD thesis, DPMMS and Trinity College, University of Cambridge, 2000.
- 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.
- 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.
- 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.
-
A. M. Pitts. Nominal Sets: Names and Symmetry in Computer Science. Cambridge University Press, 2013.
- 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.
- 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.