Abstract
Semi-unification is a common generalization of unification and matching which arose independently in the areas of proof theory, term rewriting, and type theory of programming languages. We introduce semi-unification via the typability problem for polymorphic recursive definitions, present a reduction calculus for semi-unification problems, and discuss partial results on termination of reductions. We prove decidability of semi-unification in two variables.
Cite
CITATION STYLE
Leiß, H. (1990). Polymorphic recursion and semi-unification. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 440 LNCS, pp. 211–224). Springer Verlag. https://doi.org/10.1007/3-540-52753-2_41
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
