Full Abstraction for the Resource Lambda Calculus with Tests, through Taylor Expansion

TL;DR

This paper establishes full abstraction for a resource-sensitive lambda calculus with tests by leveraging Taylor expansion, extending the model with exception handling and parallel composition.

Contribution

It introduces a novel semantic framework for a resource lambda calculus with tests, incorporating exception mechanisms and parallel composition, and proves full abstraction via Taylor expansion.

Findings

Full abstraction achieved for the finite sub-calculus.

Exception mechanism shown to be non-essential in the finite sub-calculus.

Taylor expansion extends results to the full calculus.

Abstract

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.