Unification with extended patterns

Research output: Contribution to journalArticlepeer-review

4 Scopus citations

Abstract

An extension of Miller's algorithm for β0-unification of typed λ-terms is presented. The extension considered is the addition of products and polymorphism to β0-unification; the new unification problem is termed β0π-unification. Miller's pattern restriction is generalized by allowing repeated occurrences of variables to appear as arguments to free function variables, provided such variables are prefixed by distinct sequences of projections. This extended pattern restriction has several applications, including the definition of higher-order explicit substitutions. The algorithm is verified to terminate, and is shown to be sound and complete.

Original languageEnglish
Pages (from-to)1-50
Number of pages50
JournalTheoretical Computer Science
Volume206
Issue number1-2
DOIs
StatePublished - 6 Oct 1998

Fingerprint

Dive into the research topics of 'Unification with extended patterns'. Together they form a unique fingerprint.

Cite this