Higher-order , linear , concurrent constraint programming

Higher-order , linear , concurrent constraint programming
复制标题

高阶、线性、并发约束规划

DOI：
--
复制
发表时间：
1992
期刊：
影响因子：
--
通讯作者：
Vijay Saraswat Xerox
Vijay Saraswat Xerox
中科院分区：
--
文献类型：
--
作者：
Vijay Saraswat Xerox

文献摘要

被引文献

相似文献

我们提出了一个非常简单和强大的框架，不确定的，异步的，高阶计算的基础上公式作为代理和证明作为计算解释（高阶）线性逻辑[Gir87]。该框架以两种基本方式显着细化和扩展了并发约束编程范式[Sar89]的范围：（1）通过允许代理人消费信息，它允许直接建模（不确定的）状态变化的逻辑框架，和（2）通过承认简单类型的条款作为数据对象，它允许建设，在运行时传输和应用程序（的抽象）。然而，更戏剧性的是，这个框架可以被看作是呈现了各种其他异步并发系统的高阶（如果需要的话，也可以是约束丰富的）版本，包括（一阶）演算的异步（“输入保护”）片段、休伊特的演员形式主义、格勒恩特的琳达（的抽象形式）、异步基于分配的语言和Petri网。它也可以被看作是围绕由微积分提供的函数式编程风格的平滑分层，以声明方式获得并发性，同步和不确定性所需的最小数量的额外逻辑机器。此外，有显着简单和直接的翻译无类型演算到高阶线性cc（HLcc）编程范式。我们给出了（1）HLcc的一个简单的操作语义，（2）在证明理论和操作语义之间建立了几种联系，（3）沿着[Tho 89]的路线发展了HLcc的互模拟概念，（4）建立了逻辑的.请将评论发送给作者。
We present a very simple and powerful framework for indeterminate, asynchronous, higher-order computation based on the formula-as-agent and proof-ascomputation interpretation of (higher-order) linear logic [Gir87]. The framework significantly refines and extends the scope of the concurrent constraint programming paradigm [Sar89] in two fundamental ways: (1) by allowing for the consumption of information by agents it permits a direct modelling of (indeterminate) state change in a logical framework, and (2) by admitting simply-typed -terms as dataobjects, it permits the construction, transmission and application of (abstractions of) programs at run-time. Much more dramatically, however, the framework can be seen as presenting higher-order (and if desired, constraint-enriched) versions of a variety of other asynchronous concurrent systems, including the asynchronous (‘‘input guarded”) fragment of the (first-order) -calculus, Hewitt’s actors formalism, (abstract forms of) Gelernter’s Linda, asynchronous assignment-based languages, and Petri nets. It can also be seen as smoothly layering around the functional programming style provided by the -calculus a minimal amount of extra logical machinery needed to obtain concurrency, synchronization and indeterminism declaratively. Additionally, there are remarkably simple and direct translations of the untyped -calculus into the higher-order linear cc (HLcc) programming paradigm. We give (1) a simple operational semantics for HLcc, (2) establish several connections between proof-theory and operational semantics, (3) develop the notion of bisimulation for HLcc, along the lines of [Tho89], (4) establish that logical An abstract of this paper has been submitted for publication. Please send comments to the authors.