A Nominal Approach to Equational Problems in Languages with Binders

Equational problems are fundamental in computer science, frequently arising as subproblems across diverse domains, including program analysis and learning from examples and counterexamples. This paper focuses on equational problems in languages with binding operators, formulating them within the nominal framework and referring to them as nominal equational problems (NEPs). We provide a comprehensive definition of solutions for NEPs and introduce a set of simplification rules for computing these solutions within the nominal ground term algebra. We rigorously prove that the simplification rules are sound , solution-preserving , and complete . Moreover, we establish that, under a specific strategy for rule application, the simplification process always terminates, thereby providing an effective algorithm for solving nominal equational problems. Finally, we demonstrate the practical relevance of our results by showcasing how nominal equational problems can serve as a framework for learning from examples and counterexamples. We also illustrate their applicability in addressing sufficient completeness problems, emphasising their utility in theoretical and practical contexts.