Title
Parallel Closure Theorem for Left-Linear Nominal Rewriting Systems.
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 Kikuchi1112.51
Takahito Aoto212117.53
Yoshihito Toyama353349.60