Linear lambda calculus and deep inference

Abstract

We introduce a deep inference logical system SBVr which extends SBV [6] with Rename, a self-dual atom-renaming operator. We prove that the cut free subsystem BVr of SBVr exists. We embed the terms of linear λ-calculus with explicit substitutions into formulas of SBVr. Our embedding recalls the one of full λ-calculus into π-calculus. The proof-search inside SBVr and BVr is complete with respect to the evaluation of linear λ-calculus with explicit substitutions. Instead, only soundness of proof-search in SBVr holds. Rename is crucial to let proof-search simulate the substitution of a linear λ-terms for a variable in the course of linear β-reduction. Despite SBVr is a minimal extension of SBV its proof-search can compute all boolean functions, exactly like linear λ-calculus with explicit substitutions can do. © 2011 Springer-Verlag Berlin Heidelberg.