Standardization in resource lambda-calculus

TL;DR

This paper establishes a standardization theorem for non-deterministic reduction in resource lambda-calculus, enabling better understanding of resource consumption modeling and solvability.

Contribution

It proves a standardization result for non-deterministic reduction in resource lambda-calculus, extending classical lambda-calculus concepts to resource-sensitive computation.

Findings

Non-deterministic reduction admits a standardization theorem.

Parallel reduction has a weaker standardization property.

Operational characterization of may-solvability is achieved.

Abstract

The resource calculus is an extension of the lambda-calculus allowing to model resource consumption. It is intrinsically non-deterministic and has two general notions of reduction - one parallel, preserving all the possible results as a formal sum, and one non-deterministic, performing an exclusive choice at every step. We prove that the non-deterministic reduction enjoys a notion of standardization, which is the natural extension with respect to the similar one in classical lambda-calculus. The full parallel reduction only enjoys a weaker notion of standardization instead. The result allows an operational characterization of may-solvability, which has been introduced and already characterized (from the syntactical and logical points of view) by Pagani and Ronchi Della Rocca.