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 π.X ≈?, X where π 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.
CITATION STYLE
Ayala-Rincón, M., de Carvalho-Segundo, W., Fernández, M., & Nantes-Sobrinho, D. (2017). On solving nominal fixpoint equations. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 10483 LNAI, pp. 209–226). Springer Verlag. https://doi.org/10.1007/978-3-319-66167-4_12
Mendeley helps you to discover research relevant for your work.