
CMUCS97160
Computer Science Department
School of Computer Science, Carnegie Mellon University
CMUCS97160
Linear HigherOrder PreUnification
Iliano Cervesato, Frank Pfenning
July 1997
CMUCS97160.ps
Keywords: Linear lambda calculus, linear higherorder unification
We develop a preunification algorithm in the style of Huet for the linear
lambdacalculus 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 headnormal 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 higherorder unification by means of examples.
We also show that, surprisingly, a similar preunification algorithm does not
exist for certain sublanguages. Applications lie in proof search, logic
programming, and logical frameworks based on linear type theories.
66 pages
