Abstract
In nominal syntax, variable binding is specified using atom-abstraction constructors, and alpha-equivalence is formalised using freshness constraints and atom swappings, which implement variable renamings. Composition of swappings gives rise to atom permutations. Algorithms to check equivalence, match and unify nominal terms have been extended to deal with terms where some operators are associative and/or commutative. In the case of nominal C-unification, problems are transformed into finite and complete families of fixpoint equations of the form 
, where \(\pi \) is a permutation. To generate nominal C-unifiers, a technique to obtain a sound and complete set of solutions for these equations is needed. In this work we show how complete sets of solutions for nominal fixpoint problems are built and discuss efficient techniques to generate solutions based on algebraic properties of permutations.
M. Ayala-Rincón—Partially supported by CNPq 307009/2013-0 and FAPDF 0193001369/2016 grants.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
References
Aoto, T., Kikuchi, v: A rule-based procedure for equivariant nominal unification. In: Pre-proceeding of Higher-Order Rewriting (HOR), pp. 1–5 (2016)
Aoto, T., Kikuchi, K.: Nominal confluence tool. In: Olivetti, N., Tiwari, A. (eds.) IJCAR 2016. LNCS (LNAI), vol. 9706, pp. 173–182. Springer, Cham (2016). doi:10.1007/978-3-319-40229-1_12
Ayala-Rincón, M., Carvalho-Segundo, W., Fernández, M., Nantes-Sobrinho, D.: A formalisation of nominal equivalence with associative-commutative function symbols. ENTCS 332, 21–38 (2017). Post-proceeding of Eleventh Logical and Semantic Frameworks with Applications (LSFA)
Ayala-Rincón, M., Carvalho-Segundo, W., Fernández, M., Nantes-Sobrinho, D.: Nominal C-Unification. Av (2017). http://ayala.mat.unb.br/publications.html
Ayala-Rincón, M., Fernández, M., Nantes-Sobrinho, D.: Nominal narrowing. In: Proceedings of 1st International Conference on Formal Structures for Computation and Deduction (FSCD), vol. 52 of LIPIcs, pp. 1–16. Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2016)
Ayala-Rincón, M., Fernández, M., Rocha-oliveira, A.C.: Completeness in PVS of a nominal unification algorithm. ENTCS 323, 57–74 (2016)
Baader, F., Nipkow, T.: Term Rewriting and All That. CUP, Cambridge (1998)
Cheney, J.: Equivariant unification. J. Autom. Reason. 45, 267–300 (2010)
Fernández, M., Gabbay, M.J.: Nominal rewriting. Inf. Comput. 205(6), 917–965 (2007)
Schmidt-Schauß, M., Kutsia, T., Levy, J., Villaret, M.: Nominal unification of higher order expressions with recursive let. CoRR, abs/1608.03771 (2016)
Pitts, A.M.: Nominal logic, a first order theory of names and binding. Inf. Comput. 186(2), 165–193 (2003)
Sagan, B.E.: The Symmetric Group: Representations, Combinatorial Algorithms, and Symmetric Functions. Graduate Texts in Mathematics, vol. 203, 2nd edn. Springer, New York (2001)
Siekmann, J.: Unification of commutative terms. In: Ng, E.W. (ed.) Symbolic and Algebraic Computation. LNCS, vol. 72, pp. 22–22. Springer, Heidelberg (1979). doi:10.1007/3-540-09519-5_53
Urban, C.: Nominal unification revisited. In: Proceedings of International Workshop on Unification (UNIF), vol. 42 of EPTCS, pp. 1–11 (2010)
Urban, C., Pitts, A.M., Gabbay, M.J.: Nominal unification. Theor. Comput. Sci. 323(1–3), 473497 (2004)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2017 Springer International Publishing AG
About this paper
Cite this paper
Ayala-Rincón, M., de Carvalho-Segundo, W., Fernández, M., Nantes-Sobrinho, D. (2017). On Solving Nominal Fixpoint Equations. In: Dixon, C., Finger, M. (eds) Frontiers of Combining Systems. FroCoS 2017. Lecture Notes in Computer Science(), vol 10483. Springer, Cham. https://doi.org/10.1007/978-3-319-66167-4_12
Download citation
DOI: https://doi.org/10.1007/978-3-319-66167-4_12
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-66166-7
Online ISBN: 978-3-319-66167-4
eBook Packages: Computer ScienceComputer Science (R0)