We introduce a deep inference logical system SBVr which extends SBV 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 lambda-calculus with explicit substitutions into formulas of SBVr. Our embedding recalls the one of full lambda-calculus into pi-calculus. The proof-search inside SBVr and BVr is complete with respect to the evaluation of linear lambda-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 lambda-term for a variable in the course of linear beta-reduction. Despite SBVr is a minimal extension of SBV its proof-search can compute all boolean functions, exactly like linear lambda-calculus with explicit substitutions can do.

Linear Lambda Calculus and Deep Inference

ROVERSI, Luca
2011-01-01

Abstract

We introduce a deep inference logical system SBVr which extends SBV 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 lambda-calculus with explicit substitutions into formulas of SBVr. Our embedding recalls the one of full lambda-calculus into pi-calculus. The proof-search inside SBVr and BVr is complete with respect to the evaluation of linear lambda-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 lambda-term for a variable in the course of linear beta-reduction. Despite SBVr is a minimal extension of SBV its proof-search can compute all boolean functions, exactly like linear lambda-calculus with explicit substitutions can do.
2011
TLCA 2011 - 10th Typed Lambda Calculi and Applications, Part of RDP'11
Novi Sad, Serbia
June 1st --- 3rd, 2011
Typed Lambda Calculi and Applications 10th International Conference, TLCA 2011, Novi Sad, Serbia, June 1-3, 2011. Proceedings
Springer
6690
184
197
9783642216909
http://www.di.unito.it/~rover
Lambda calculus; Deep inference; Computational models.
Luca Roversi
File in questo prodotto:
File Dimensione Formato  
10.1007_978-3-642-21691-6_16.pdf

Accesso riservato

Tipo di file: POSTPRINT (VERSIONE FINALE DELL’AUTORE)
Dimensione 317.44 kB
Formato Adobe PDF
317.44 kB Adobe PDF   Visualizza/Apri   Richiedi una copia

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/2318/92530
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 3
  • ???jsp.display-item.citation.isi??? 3
social impact