eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2019-06-18
10:1
10:19
10.4230/LIPIcs.FSCD.2019.10
article
A Generic Framework for Higher-Order Generalizations
Cerna, David M.
1
Kutsia, Temur
2
FMV and RISC, Johannes Kepler University Linz, Austria
RISC, Johannes Kepler University Linz, Austria
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.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol131-fscd2019/LIPIcs.FSCD.2019.10/LIPIcs.FSCD.2019.10.pdf
anti-unification
typed lambda calculus
least general generalization