Towards practical typechecking for macro forest transducers

Kazuhiro Abe, Keisuke Nakano

Research output: Contribution to journalArticlepeer-review


Macro tree transducers (MTTs) and macro forest transducers (MFTs) have been used as good models of tree-structured data transformations such as XML transformations. Typechecking of transformations in these models is performed to verify if any tree of an input type is always transformed into a tree of an output type, which is useful for validating XML transformations against given XML schemata. In typechecking problems for MTTs and MFTs, each “type” is usually given by a tree automaton. A naive implementation of a typechecking algorithm is very inefficient because its time complexity is beyond exponential to the number of states of tree automata, and a large number of equivalence checking operations over finite maps are required. For typechecking of MTTs, Frisch and Hosoya proposed an efficient and practical algorithm by using alternating tree automata as an internal representation of types and reducing the problem to satisfiability checking over first-order logic formulae. In this paper, we extend their typechecking method to apply it to MFTs that are more expressive than MTTs. Our implementation of the proposed method shows that it performs typechecking for relatively simple cases in a reasonable time.

Original languageEnglish
Pages (from-to)962-974
Number of pages13
JournalJournal of information processing
Publication statusPublished - 2017 Dec
Externally publishedYes


  • Alternating tree automata
  • Macro forest transducers
  • Typechecking

ASJC Scopus subject areas

  • Computer Science(all)


Dive into the research topics of 'Towards practical typechecking for macro forest transducers'. Together they form a unique fingerprint.

Cite this