Abstract | ||
---|---|---|
Nominal rewriting has been introduced as an extension of first-order term rewriting by a binding mechanism based on the nominal approach. In this paper, we extend Huet's parallel closure theorem and its generalisation on confluence of left-linear term rewriting systems to the case of nominal rewriting. The proof of the theorem follows a previous inductive confluence proof for orthogonal uniform nominal rewriting systems, but the presence of critical pairs requires a much more delicate argument. The results include confluence of left-linear uniform nominal rewriting systems that are not alpha-stable and thus are not represented by any systems in traditional higher-order rewriting frameworks. |
Year | DOI | Venue |
---|---|---|
2017 | 10.1007/978-3-319-66167-4_7 | Lecture Notes in Artificial Intelligence |
Field | DocType | Volume |
Discrete mathematics,Generalization,Algorithm,Rewriting,Confluence,Mathematics | Conference | 10483 |
ISSN | Citations | PageRank |
0302-9743 | 0 | 0.34 |
References | Authors | |
12 | 3 |
Name | Order | Citations | PageRank |
---|---|---|---|
Kentaro Kikuchi | 1 | 11 | 2.51 |
Takahito Aoto | 2 | 121 | 17.53 |
Yoshihito Toyama | 3 | 533 | 49.60 |