A Linear Spine Calculus
Iliano Cervesato · Journal of Logic and Computation · 2003
We present the spine calculus S→⊸&⊤ as an efficient representation for the linear λ-calculus λ→⊸&⊤ which includes unrestricted functions (→) linear functions (⊸) additive pairing (&) and additive unit (⊤). S→⊸&⊤ enhances the representation of Church's simply typed λ-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 η-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 λ→⊸&⊤ into S→⊸&⊤ 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. βη-normal, forms.