2026-07-23T18:08:53Z https://drops.dagstuhl.de/oai

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

A Generic Framework for Higher-Order Generalizations Cerna, David M. Kutsia, Temur anti-unification typed lambda calculus least general generalization We consider a generic framework for anti-unification of simply typed lambda terms. It helps to compute generalizations which contain maximally common top part of the input expressions, without nesting generalization variables. The rules of the corresponding anti-unification algorithm are formulated, and their soundness and termination are proved. The algorithm depends on a parameter which decides how to choose terms under generalization variables. Changing the particular values of the parameter, we obtained four new unitary variants of higher-order anti-unification and also showed how the already known pattern generalization fits into the schema. Schloss Dagstuhl – Leibniz-Zentrum für Informatik David M. Cerna and Temur Kutsia 2019 Is Part Of LIPIcs, Volume 131, 4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.FSCD.2019.10 urn:nbn:de:0030-drops-105175 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2019.10 eng https://creativecommons.org/licenses/by/3.0/legalcode