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