Document Open Access Logo

First-Order Unification on Compressed Terms

Authors Adrià Gascón, Sebastian Maneth, Lander Ramos

Thumbnail PDF


  • Filesize: 490 kB
  • 10 pages

Document Identifiers

Author Details

Adrià Gascón
Sebastian Maneth
Lander Ramos

Cite AsGet BibTex

Adrià Gascón, Sebastian Maneth, and Lander Ramos. First-Order Unification on Compressed Terms. In 22nd International Conference on Rewriting Techniques and Applications (RTA'11). Leibniz International Proceedings in Informatics (LIPIcs), Volume 10, pp. 51-60, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2011)


Singleton Tree Grammars (STGs) have recently drawn considerable attention. They generalize the sharing of subtrees known from DAGs to sharing of connected subgraphs. This allows to obtain smaller in-memory representations of trees than with DAGs. In the past years some important tree algorithms were proved to perform efficiently (without decompression) over STGs; e.g., type checking, equivalence checking, and unification. We present a tool that implements an extension of the unification algorithm for STGs. This algorithm makes extensive use of equivalence checking. For the latter we implemented two variants, the classical exact one and a recent randomized one. Our experiments show that the randomized algorithm performs better. The running times are also compared to those of unification over uncompressed trees.
  • unification
  • matching
  • grammars
  • compression
  • STG
  • system C++


  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    PDF Downloads
Questions / Remarks / Feedback

Feedback for Dagstuhl Publishing

Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail