Linearity, Non-determinism and Solvability

Issue title: From Mathematical Beauty to the Truth of Nature: to Jerzy Tiuryn on his 60th Birthday

Article type: Research Article

Authors: Pagani, Michele | Rocca, Simona Ronchi Della

Affiliations: Laboratoire d'Informatique de Paris-Nord – Université Paris 13, 99, avenue Jean-Baptiste Clément, 93430 Villetaneuse France. michele.pagani@lipn.univ-paris13.fr | Dipartimento di Informatica – Università di Torino, C.So Svizzera, 185 - 10149 Torino, Italy. ronchi@di.unito.it

Note: [] Address for correspondence: Laboratoire d'Informatique de Paris-Nord – Université Paris 13, 99, avenue Jean-Baptiste Clément, 93430 Villetaneuse France

Abstract: We study the notion of solvability in the resource calculus, an extension of the λ-calculus modelling resource consumption. Since this calculus is non-deterministic, two different notions of solvability arise, one optimistic (angelical, may) and one pessimistic (demoniac, must). We give a syntactical, operational and logical characterization for the may-solvability and only a partial characterization of the must-solvability. Finally, we discuss the open problem of a complete characterization of the must-solvability.

DOI: 10.3233/FI-2010-324

Journal: Fundamenta Informaticae, vol. 103, no. 1-4, pp. 173-202, 2010