
Accession Number : ADA332093
Title : Linear HigherOrder PreUnification
Corporate Author : CARNEGIEMELLON UNIV PITTSBURGH PA DEPT OF COMPUTER SCIENCE
Personal Author(s) : Cervesato, Iliano ; Pfenning, Frank
PDF Url : ADA332093
Report Date : 20 JUL 1997
Pagination or Media Count : 68
Abstract : 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.
Descriptors : *COMPUTER PROGRAMMING, ALGORITHMS, LINEAR SYSTEMS, COMPUTER LOGIC, PROGRAMMING LANGUAGES, SEMANTICS.
Subject Categories : Computer Programming and Software
Distribution Statement : APPROVED FOR PUBLIC RELEASE