2012/11/17 by Maurizio Dominici, Simona Ronchi Della Rocca, Paolo Tranquilli
Computer Science · #cs.LO
paper · pdf · doi:10.4204/eptcs.101.1
published as EPTCS 101, 2012, pp. 1-11 · In Proceedings LINEARITY 2012, arXiv:1211.3480
arxiv created 2012/11/17 · arxiv updated 2012/11/20
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.