Standardization in resource lambda-calculus

Maurizio Dominici
(Università di Torino)
Simona Ronchi Della Rocca
(Università di Torino)
Paolo Tranquilli
(Università di Bologna)

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.

In Sandra Alves and Ian Mackie: Proceedings 2nd International Workshop on Linearity (LINEARITY 2012), Tallinn, Estonia, 1 April 2012, Electronic Proceedings in Theoretical Computer Science 101, pp. 1–11.
Published: 15th November 2012.

ArXived at: http://dx.doi.org/10.4204/EPTCS.101.1 bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org