Accession Number : ADA332093

Title :   Linear Higher-Order Pre-Unification

Corporate Author : CARNEGIE-MELLON 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 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.

Descriptors :   *COMPUTER PROGRAMMING, ALGORITHMS, LINEAR SYSTEMS, COMPUTER LOGIC, PROGRAMMING LANGUAGES, SEMANTICS.

Subject Categories : Computer Programming and Software

Distribution Statement : APPROVED FOR PUBLIC RELEASE