論文

査読有り
2011年

Calculating tree navigation with symmetric relational zipper

PERM'11 - Proceedings of the 20th ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation
  • Yuta Ikeda
  • ,
  • Susumu Nishimura

開始ページ
101
終了ページ
110
記述言語
英語
掲載種別
研究論文(国際会議プロシーディングス)
DOI
10.1145/1929501.1929521

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 to derive useful equations by simple calculations. We apply the calculational method to derive certain equalities of XPath expressions. The point-free relational reasoning not only leads to a concise justification of some known results but also establishes equations for a larger class of tree navigation operations, including those specified with negative constraints and those beyond XPath expressibility. © 2011 ACM.

リンク情報
DOI
https://doi.org/10.1145/1929501.1929521
ID情報
  • DOI : 10.1145/1929501.1929521
  • SCOPUS ID : 79952151288

エクスポート
BibTeX RIS