Linear Lambda Calculus and Deep Inference

摘要

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 λ-term for a variable in the course of linear j8-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.