From Separation Logic to Hyperedge Replacement and Back(Extended Abstract)

摘要

Hyperedge replacement grammars and separation-logic formulas both define classes of graph-like structures. In this paper, we describe two effective translations between restricted hyperedge replacement grammars and formulas in a fragment of separation logic. These translations preserve the semantics of formulas and grammars. Hyperedge-replacement grammars [1] are a natural extension of context-free string grammars to the world of hypergraphs. An HR grammar defines language of structures that can be constructed from an initial graph.