2026-07-18T10:44:07Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:17994 2024-03-06T11:00:48Z ddc:004 open_access

E-Unification for Second-Order Abstract Syntax Kudasov, Nikolai E-unification higher-order unification second-order abstract syntax Higher-order unification (HOU) concerns unification of (extensions of) λ-calculus and can be seen as an instance of equational unification (E-unification) modulo βη-equivalence of λ-terms. We study equational unification of terms in languages with arbitrary variable binding constructions modulo arbitrary second-order equational theories. Abstract syntax with general variable binding and parametrised metavariables allows us to work with arbitrary binders without committing to λ-calculus or use inconvenient and error-prone term encodings, leading to a more flexible framework. In this paper, we introduce E-unification for second-order abstract syntax and describe a unification procedure for such problems, merging ideas from both full HOU and general E-unification. We prove that the procedure is sound and complete. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Nikolai Kudasov 2023 Is Part Of LIPIcs, Volume 260, 8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.FSCD.2023.10 urn:nbn:de:0030-drops-179944 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2023.10 eng https://creativecommons.org/licenses/by/4.0/legalcode