Accession Number : ADA324652

Title :   A Linear Spine Calculus,

Corporate Author : CARNEGIE-MELLON UNIV PITTSBURGH PA DEPT OF COMPUTER SCIENCE

Personal Author(s) : Cervesato, Iliano ; Pfenning, Frank

PDF Url : ADA324652

Report Date : 10 APR 1997

Pagination or Media Count : 36

Abstract : We present the spine calculus S(approaches -o&T) as an efficient representation for the linear lambda-calculus lambda(approaches -o&T) which includes intuitionistic functions (approach) Tau linear functions (-o)Tau additive pairing (&Tau) and additive unit (T). S(approaches -o&T) enhances the representation of Church's simply typed lamda-calculus as abstract Bolum trees by enforcing extensionality and by incorporating linear constructs. This approach permits procedures such as unification to retain the efficient head access that characterizes first-order term languages without the overhead of performing n-conversions at run time. Potential applications lie in proof search(Tau) logic programming(Tau) and logical frameworks based on linear type theories. We define the spine calculus(Tau) give translations of lambda(approaches -o&T) into S(approaches -o&T) and vice-versa(Tau) prove their soundness and completeness with respect to typing and reduction(Tau) and shows that the spine calculus is strongly normalizing and admits unique canonical forms.

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

Subject Categories : Operations Research
      Computer Programming and Software

Distribution Statement : APPROVED FOR PUBLIC RELEASE