2007/01/26 by Alain Frisch, Frisch, Alain, Haruo Hosoya +1
Computer Science · #FOS: Computer and information sciences #Logic, programming, and type systems #Model-Driven Software Engineering Techniques #Natural Language Processing Techniques #Programming Languages (cs.PL) #cs.PL
paper · pdf · doi:10.48550/arxiv.cs/0701176
arxiv created 2007/01/26 · openalex publication_date 2007/01/26 · arxiv updated 2009/12/01 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
Macro tree transducers (mtt) are an important model that both covers many useful XML transformations and allows decidable exact typechecking. This paper reports our first step toward an implementation of mtt typechecker that has a practical efficiency. Our approach is to represent an input type obtained from a backward inference as an alternating tree automaton, in a style similar to Tozawa's XSLT0 typechecking. In this approach, typechecking reduces to checking emptiness of an alternating tree automaton. We propose several optimizations (Cartesian factorization, state partitioning) on the backward inference process in order to produce much smaller alternating tree automata than the naive algorithm, and we present our efficient algorithm for checking emptiness of alternating tree automata, where we exploit the explicit representation of alternation for local optimizations. Our preliminary experiments confirm that our algorithm has a practical performance that can typecheck simple transformations with respect to the full XHTML in a reasonable time.