TY - JOUR
T1 - Unification with extended patterns
AU - Duggan, Dominic
PY - 1998/10/6
Y1 - 1998/10/6
N2 - 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.
AB - 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.
UR - http://www.scopus.com/inward/record.url?scp=0342923324&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=0342923324&partnerID=8YFLogxK
U2 - 10.1016/S0304-3975(97)00141-2
DO - 10.1016/S0304-3975(97)00141-2
M3 - Article
AN - SCOPUS:0342923324
SN - 0304-3975
VL - 206
SP - 1
EP - 50
JO - Theoretical Computer Science
JF - Theoretical Computer Science
IS - 1-2
ER -