Computer Science Department
School of Computer Science, Carnegie Mellon University


Linear Higher-Order Pre-Unification

Iliano Cervesato, Frank Pfenning

July 1997

Keywords: Linear lambda calculus, linear higher-order unification

We develop a pre-unification algorithm in the style of Huet for the linear lambda-calculus lambda -> -o $ T which includes intuitionistic functions (->), linear functions (-o), additive pairing (&), and additive unit (T). This procedure conveniently operates on an efficient representation of lambda -> -o $ T, the spine calculus S -> -o & T for which we define the concept of weak head-normal form. We prove the soundness and completeness of our algorithm with respect to the proper notion of definitional equality for S -> -o & T, and illustrate the distinctive aspects of linear higher-order unification by means of examples. We also show that, surprisingly, a similar pre-unification algorithm does not exist for certain sublanguages. Applications lie in proof search, logic programming, and logical frameworks based on linear type theories.

66 pages

Return to: SCS Technical Report Collection
School of Computer Science homepage

This page maintained by