2026-07-26T19:18:21Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:3126 2024-03-06T10:33:50Z ddc:004 open_access

First-Order Unification on Compressed Terms Gascón, Adrià Maneth, Sebastian Ramos, Lander unification matching grammars compression STG system C++ 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Adrià Gascón and Sebastian Maneth and Lander Ramos 2011 Is Part Of LIPIcs, Volume 10, 22nd International Conference on Rewriting Techniques and Applications (RTA'11) (2011) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.RTA.2011.51 urn:nbn:de:0030-drops-31263 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.RTA.2011.51 eng https://creativecommons.org/licenses/by-nc-nd/3.0/legalcode