A Linear Spine Calculus,

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.

Open PDF

Document Details

Document Type
Technical Report
Publication Date
Apr 10, 1997
Accession Number
ADA324652

Entities

People

  • Frank Pfenning
  • Iliano Cervesato

Organizations

  • Carnegie Mellon University

Tags

DTIC Thesaurus Topics

  • Abstracts
  • Algorithms
  • Calculus
  • Computations
  • Computer Programming
  • Computer Science
  • Computers
  • Conversion
  • Destructors
  • Invariance
  • Inversion
  • Judgment
  • Language
  • Programming Languages
  • Sequences
  • Theoretical Computer Science
  • Translations

Readers

  • Calculus or Mathematical Analysis
  • Computational Linguistics
  • Traumatic Brain Injury (TBI) and Cognitive Aging in the Guam and Border Populations Affected by Alzheimer's Disease and Tau-Associated Dementias.