Bidirectionalizing graph transformations

Abstract

Bidirectional transformations provide a novel mechanism for syn-chronizing and maintaining the consistency of information between input and output. Despite many promising results on bidirectional transformations, these have been limited to the context of relational or XML (tree-like) databases. We challenge the problem of bidirec-tional transformations within the context of graphs, by proposing a formal definition of a well-behaved bidirectional semantics for UnCAL, i.e., a graph algebra for the known UnQL graph query language. The key to our successful formalization is full utiliza-tion of both the recursive and bulk semantics of structural recur-sion on graphs. We carefully refine the existing forward evaluation of structural recursion so that it can produce sufficient trace infor-mation for later backward evaluation. We use the trace information for backward evaluation to reflect in-place updates and deletions on the view to the source, and adopt the universal resolving algorithm for inverse computation and the narrowing technique to tackle the difficult problem with insertion. We prove our bidirectional evalu-ation is well-behaved. Our current implementation is available on-line and confirms the usefulness of our approach with nontrivial applications.