Thomas Ehrhard ; Antonio Bucciarelli ; Alberto Carraro ; Giulio Manzonetto - 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 - https://doi.org/10.2168/LMCS-8(4:3)2012
Full Abstraction for the Resource Lambda Calculus with Tests, through Taylor Expansion

Authors: Thomas Ehrhard ; Antonio Bucciarelli ; Alberto Carraro ; Giulio Manzonetto

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.


Volume: Volume 8, Issue 4
Published on: October 10, 2012
Accepted on: June 25, 2015
Submitted on: February 29, 2012
Keywords: Computer Science - Logic in Computer Science,F.4.1


Share

Consultation statistics

This page has been seen 299 times.
This article's PDF has been downloaded 331 times.