Nominal Equational Problems
| Autor: | Maribel Fernández, Mauricio Ayala-Rincón, Daniele Nantes-Sobrinho, Deivid Vale |
|---|---|
| Rok vydání: | 2021 |
| Předmět: |
Discrete mathematics
Nominal terms Image (category theory) Modulo Atom (order theory) 0102 computer and information sciences 02 engineering and technology Approx 01 natural sciences Term algebra Decidability Alpha (programming language) 010201 computation theory & mathematics 0202 electrical engineering electronic engineering information engineering 020201 artificial intelligence & image processing Mathematics |
| Zdroj: | Lecture Notes in Computer Science ISBN: 9783030719944 FoSSaCS |
| Popis: | We define nominal equational problems of the form $$\exists \overline{W} \forall \overline{Y} : P$$ ∃ W ¯ ∀ Y ¯ : P , where $$P$$ P consists of conjunctions and disjunctions of equations $$s\approx _\alpha t$$ s ≈ α t , freshness constraints $$a\#t$$ a # t and their negations: $$s \not \approx _\alpha t$$ s ≉ α t and "Equation missing", where $$a$$ a is an atom and $$s, t$$ s , t nominal terms. We give a general definition of solution and a set of simplification rules to compute solutions in the nominal ground term algebra. For the latter, we define notions of solved form from which solutions can be easily extracted and show that the simplification rules are sound, preserving, and complete. With a particular strategy for rule application, the simplification process terminates and thus specifies an algorithm to solve nominal equational problems. These results generalise previous results obtained by Comon and Lescanne for first-order languages to languages with binding operators. In particular, we show that the problem of deciding the validity of a first-order equational formula in a language with binding operators (i.e., validity modulo $$\alpha $$ α -equality) is decidable. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|