Solvability in Resource Lambda-Calculus

Abstract. The resource calculus is an extension of the λ-calculus allowing to model resource consumption. Namely, the argument of a function comes as a finite multiset of resources, which in turn can be either linear or reusable, giving rise to non-deterministic choices, expressed by a formal sum. Using the λ-calculus terminology, we call solvable a term that can interact with the environment: solvable terms represent meaningful programs. Because of the non-determinism, different definitions of solvability are possible in the resource calculus. Here we study the optimistic (angelical, or may) notion, and so we define a term solvable whenever there is a simple head context reducing the term into a sum where at least one addend is the identity. We give a syntactical, operational and logical characterization of this kind of solvability.

• Type: Conference
• Year: 2010
• Where: FOSSACS
• Authors: Michele Pagani, Simona Ronchi Della Rocca
• Keywords: Applied Computing, FOSSACS 2010, Resource Calculus, Resource Consumption, Solvable Terms