(National Institute of Informatics, Japan)
Bidirectional transformations provide a novel mechanism for synchronizing and maintaining the consistency of information between input and output. Despite many promising results on bidirectional transformations, these have been limited to lists and trees. We challenge the problem of bidirectional transformations on graphs, by proposing a formal definition of a well-behaved bidirectional semantics for UnCAL, a graph algebra. Our key idea is to treat graphs as compactable infinite trees and to manipulate trees by structural recursion. Specifically, we carefully refine the existing forward evaluation of structural recursion so that it can produce sufficient trace information for later backward evaluation, and we use the trace information for backward evaluation to reflect updates on the view to the source. We prove our bidirectional evaluation is well-behaved.