Ehrhard, Thomas and Bucciarelli, Antonio and Carraro, Alberto and Manzonetto, Giulio - Full Abstraction for the Resource Lambda Calculus with Tests, through Taylor Expansion

lmcs:1047 - Logical Methods in Computer Science, October 10, 2012, Volume 8, Issue 4
Full Abstraction for the Resource Lambda Calculus with Tests, through Taylor Expansion

Authors: Ehrhard, Thomas and Bucciarelli, Antonio and Carraro, Alberto and Manzonetto, Giulio

We study the semantics of a resource-sensitive extension of the lambda calculus in a canonical reflexive object of a category of sets and relations, a relational version of Scott's original model of the pure lambda calculus. This calculus is related to Boudol's resource calculus and is derived from Ehrhard and Regnier's differential extension of Linear Logic and of the lambda calculus. We extend it with new constructions, to be understood as implementing a very simple exception mechanism, and with a "must" parallel composition. These new operations allow to associate a context of this calculus with any point of the model and to prove full abstraction for the finite sub-calculus where ordinary lambda calculus application is not allowed. The result is then extended to the full calculus by means of a Taylor Expansion formula. As an intermediate result we prove that the exception mechanism is not essential in the finite sub-calculus.


Source : oai:arXiv.org:1209.2890
DOI : 10.2168/LMCS-8(4:3)2012
Volume: Volume 8, Issue 4
Published on: October 10, 2012
Submitted on: February 29, 2012
Keywords: Computer Science - Logic in Computer Science,F.4.1


Share

Consultation statistics

This page has been seen 79 times.
This article's PDF has been downloaded 138 times.