Specifying Pointer Structures by Graph Reduction

Graph-reduction specifications (GRSs) are a powerful new method for specifying classes of pointer data structures (shapes). They cover important shapes, like various forms of balanced trees, that cannot be handled by existing methods. This report formally defines GRSs as graph-reduction systems with a signature restriction and an accepting graph. We are mainly interested in PGRSs, which are polynomially-terminating GRSs whose graph languages are closed under reduction. PGRS languages have a polynomial membership test, making them a computationally well-behaved formalism for specifying graph languages. We investigate the power of the PGRS framework by presenting example shapes within and beyond its scope and by considering its language closure properties under intersection, union and complement: PGRS languages are closed under intersection; not closed under union (unless we drop the closedness restriction and exclude languages with the empty graph); and not closed under complement. O...

• Type: Conference
• Year: 2003
• Where: AGTIVE
• Authors: Adam Bakewell, Detlef Plump, Colin Runciman
• Keywords: AGTIVE 2003, Balanced Trees, Formal Languages, Graph Languages, PGRS Languages