2026-07-22T12:14:54Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:4067 2024-03-06T10:34:46Z ddc:004 open_access

Unification Modulo Nonnested Recursion Schemes via Anchored Semi-Unification Smolka, Gert Tebbi, Tobias recursion schemes semi-unification infinitary rewriting A recursion scheme is an orthogonal rewriting system with rules of the form f(x1,...,xn) -> s. We consider terms to be equivalent if they rewrite to the same redex-free possibly infinite term after infinitary rewriting. For the restriction to the nonnested case, where nested redexes are forbidden, we prove the existence of principal unifiers modulo scheme equivalence. We give an algorithm computing principal unifiers by reducing the problem to a novel fragment of semi-unification we call anchored semi-unification. For anchored semi-unification, we develop a decision algorithm that returns a principal semi-unifier in the positive case. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Gert Smolka and Tobias Tebbi 2013 Is Part Of LIPIcs, Volume 21, 24th International Conference on Rewriting Techniques and Applications (RTA 2013) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.RTA.2013.271 urn:nbn:de:0030-drops-40674 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.RTA.2013.271 eng https://creativecommons.org/licenses/by/3.0/legalcode