Narrowing Data-Structures with Pointers

摘要: We investigate the narrowing relation in a wide class of (cyclic) term-graph rewrite systems. propose new sound and complete narrowing-based algorithm able to solve goals presence data structures with pointers (e.g., circular lists, doubly linked lists etc.). first define systems we consider. Our rules provide features such as pointer (edge) redirections, relabeling existing nodes, addition creation nodes. Moreover, split set nodes term-graphs two (possibly empty) subsets: (i) variables (ii) names. Variable can be mapped against any other node whereas names act constants thus they are supposed match themselves. This distinction between allows us synthesize, through process, data-structures shapes. In second step, rewriting relations. then show soundness completeness narrowing.