A linear spine calculus
We present the spine calculus S-->-oinverted perpendicular as an efficient representation for the linear lambda-calculus lambda(-->-oinverted perpendicular) which includes unrestricted functions (-->) linear functions (-o) additive pairing (&) and additive unit (inverted perpendicular). S-->&& enhances the representation of Church's simply typed lambda-calculus 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 eta-conversions at run time. Applications lie in proof search, logic programming, and logical frameworks based on linear type theories. It is also related to foundational work on term assignment calculi for presentations of the sequent calculus. We define the spine calculus, give translations of lambda(-->-oinverted perpendicular) into S-->-oinverted perpendicular and vice versa, prove their soundness and completeness with respect to typing and reductions, and show that the typable fragment of the spine calculus is strongly normalizing and admits unique canonical, i.e. betaeta-normal, forms.
linear lambda calculus term assignment systems uniform provability