Calculating tree navigation with symmetric relational zipper

Navigating through tree structures is a core operation in tree processing programs. Most notably, XML processing programs intensively use XPath, the path specification language that locates particular nodes in a given document structure. This paper develops a theory for reasoning about equalities of tree navigation programs. In functional programming languages, tree navigation operations can be cleanly implemented as functions operating over the data structure known as Huet’s zipper. The tree navigation functions are expected to have certain nice symmetric properties (e.g., a function going one-level down in the tree structure would be the inverse of another function coming back the other way around, and vice versa), but they are not indeed a perfect symmetry, due to partiality and non-injectivity of the functions. In order to fully exploit the symmetry indicated by tree navigation operations, we model them by relations, instead of functions. The relational specification allows us...

• Type: Journal
• Year: 2011
• Where: PEPM
• Authors: Yuta Ikeda, Susumu Nishimura
• Keywords: Functional Programming Languages, Navigation Operations, PEPM 2011, Relational Reasoning, Software Engineering