Solvability in Resource Lambda-Calculus
Solvability in Resource Lambda-Calculus
复制标题
资源 Lambda 演算的可解性
DOI：
10.1007/978-3-642-12032-9_25
复制
发表时间：
2010
影响因子：
0.3
通讯作者：
S. D. Rocca
中科院分区：
文献类型：
--
作者：
Michele Pagani;S. D. Rocca
资源演算是λ计算的扩展，允许对资源消耗进行建模。用正式的总和表示，我们称可解决的术语可以与环境相互作用：可解决的术语代表有意义的程序。在这里的资源计算中，我们可以研究乐观的概念（天使般的）概念。我们给出了这种解决性的句法，操作和逻辑表征。
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.