Abstract | ||
---|---|---|
We design a completion procedure for nominal rewriting systems, based on a generalisation of the recursive path ordering to take into account alpha equivalence. Nominal rewriting generalises first-order rewriting by providing support for the specification of binding operators. Completion of rewriting systems with binders is a notably difficult problem; the completion procedure presented in this paper is the first to deal with binders in rewrite rules. |
Year | DOI | Venue |
---|---|---|
2012 | 10.1007/978-3-642-31585-5_21 | ICALP (2) |
Keywords | Field | DocType |
recursive path,binding operator,difficult problem,nominal completion,completion procedure,account alpha equivalence,completion,rewriting | Path-ordering,Discrete mathematics,Combinatorics,Computer science,Generalization,Equivalence (measure theory),Confluence,Rewriting,Operator (computer programming),Knuth–Bendix completion algorithm,Recursion | Conference |
Volume | ISSN | Citations |
7392 | 0302-9743 | 5 |
PageRank | References | Authors |
0.50 | 23 | 2 |
Name | Order | Citations | PageRank |
---|---|---|---|
Maribel Fernández | 1 | 97 | 10.03 |
Albert Rubio | 2 | 228 | 19.44 |