Computer Science – Logic in Computer Science
Scientific paper
2010-11-16
Computer Science
Logic in Computer Science
26 pages: Final technical report associated to the TLCA2011 paper "Linear lambda calculus and deep inference"
Scientific paper
SBV is a deep inference system that extends the set of logical operators of multiplicative linear logic with the non commutative operator Seq. We introduce the logical system SBVr which extends SBV by adding a self-dual atom-renaming operator to it. We prove that the cut elimination holds on SBVr. SBVr and its cut free subsystem BVr are complete and sound with respect to linear lambda calculus with explicit substitutions. Under any strategy, a sequence of evaluation steps of any linear lambda-term M becomes a process of proof-search in SBVr (BVr) once M is mapped into a formula of SBVr. Completeness and soundness follow from simulating linear beta-reduction with explicit substitutions as processes. The role of the new renaming operator of SBVr is to rename channel-names on-demand. This simulates the substitution that occurs in a beta-reduction. Despite SBVr is a minimal extension of SBV its proof-search can compute all boolean functions, as linear lambda-calculus with explicit substitutions can compute all boolean functions as well. So, proof search of SBVr and BVr is at least ptime-complete.
No associations
LandOfFree
Linear lambda Calculus with Explicit Substitutions as Proof-Search in Deep Inference does not yet have a rating. At this time, there are no reviews or comments for this scientific paper.
If you have personal experience with Linear lambda Calculus with Explicit Substitutions as Proof-Search in Deep Inference, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and Linear lambda Calculus with Explicit Substitutions as Proof-Search in Deep Inference will most certainly appreciate the feedback.
Profile ID: LFWR-SCP-O-464282