Name
Abstract | ||
|---|---|---|
Nominal rewriting systems (Fernandez, Gabbay, Mackie, 2004;Fernandez, Gabbay, 2007) have been introduced as a new frameworkof higher-order rewriting systems based on the nominal approach(Gabbay, Pitts, 2002; Pitts, 2003), which deals with variablebinding via permutations and freshness conditions on atoms.Confluence of orthogonal nominal rewriting systems has been shown in(Fernandez, Gabbay, 2007). However, their definition of(non-trivial) critical pairs has a serious weakness so that theorthogonality does not actually hold for most of standard nominalrewriting systems in the presence of binders. To overcome thisweakness, we divide the notion of overlaps into the self-rooted andproper ones, and introduce a notion of alpha-stability whichguarantees alpha-equivalence of peaks from the self-rootedoverlaps. Moreover, we give a sufficient criterion for uniformity and alpha-stability. The new definition of orthogonality and thecriterion offer a novel confluence condition effectively applicable to many standard nominal rewriting systems. We also report on animplementation of a confluence prover for orthogonal nominal rewriting systems based on our framework. |
Year | Venue | Field |
|---|---|---|
2015 | RTA | Discrete mathematics,Computer science,Permutation,Algorithm,Orthogonality,Rewriting,Confluence,Gas meter prover |
DocType | Citations | PageRank |
Conference | 5 | 0.55 |
References | Authors | |
6 | 4 | |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Takaki Suzuki | 1 | 7 | 0.94 |
| Kentaro Kikuchi | 2 | 11 | 2.51 |
| Takahito Aoto | 3 | 121 | 17.53 |
| Yoshihito Toyama | 4 | 533 | 49.60 |