Nominal C-Unification
Programming Languages
2017-09-19 v1 Logic in Computer Science
Abstract
Nominal unification is an extension of first-order unification that takes into account the \alpha-equivalence relation generated by binding operators, following the nominal approach. We propose a sound and complete procedure for nominal unification with commutative operators, or nominal C-unification for short, which has been formalised in Coq. The procedure transforms nominal C-unification problems into simpler (finite families) of fixpoint problems, whose solutions can be generated by algebraic techniques on combinatorics of permutations.
Keywords
Cite
@article{arxiv.1709.05384,
title = {Nominal C-Unification},
author = {Mauricio Ayala-Rincón and Washington de Carvalho-Segundo and Maribel Fernández and Daniele Nantes-Sobrinho},
journal= {arXiv preprint arXiv:1709.05384},
year = {2017}
}
Comments
Pre-proceedings paper presented at the 27th International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR 2017), Namur, Belgium, 10-12 October 2017 (arXiv:1708.07854)