file.pdf (560.31 kB)
0/0

Linear Higher-Order Pre-Unification

Download (560.31 kB)
journal contribution
posted on 01.12.2002 by Iliano Cervesato, Frank Pfenning
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.

History

Publisher Statement

All Rights Reserved

Date

01/12/2002

Exports

Exports