2026-08-10T11:21:36Z https://drops.dagstuhl.de/oai

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

Higher-Order Equational Pattern Anti-Unification Cerna, David M. Kutsia, Temur Simply typed lambda calculus anti-unification equational theories We consider anti-unification for simply typed lambda terms in associative, commutative, and associative-commutative theories and develop a sound and complete algorithm which takes two lambda terms and computes their generalizations in the form of higher-order patterns. The problem is finitary: the minimal complete set of generalizations contains finitely many elements. We define the notion of optimal solution and investigate special fragments of the problem for which the optimal solution can be computed in linear or polynomial time. Schloss Dagstuhl – Leibniz-Zentrum für Informatik David M. Cerna and Temur Kutsia 2018 Is Part Of LIPIcs, Volume 108, 3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.FSCD.2018.12 urn:nbn:de:0030-drops-91826 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2018.12 eng https://creativecommons.org/licenses/by/3.0/legalcode