Elementary Complexity and Geometry of Interaction
Elementary Complexity and Geometry of Interaction
复制标题
交互的基本复杂性和几何形状
DOI：
10.1007/3-540-48959-2_4
复制
发表时间：
1999
期刊：
影响因子：
--
通讯作者：
M. Pedicini
中科院分区：
文献类型：
--
作者：
Patrick Baillot;M. Pedicini
我们介绍了由配备分辨率（以下[10]）的代数给出的相互作用模型的几何形状，可以解释基本线性逻辑的证明。为了将交互计算（所谓的执行公式）的几何形状扩展到代数中的一类程序，而不仅仅是来自证明的程序，我们定义了执行的变体（称为弱执行）。它在任何条款程序中的应用都显示出在程序大小中基本的步骤数终止。我们确定弱执行与来自证明的程序的标准执行相吻合。
We introduce a geometry of interaction model given by an algebra of clauses equipped with resolution (following [10]) into which proofs of Elementary Linear Logic can be interpreted. In order to extend geometry of interaction computation (the so called execution formula) to a wider class of programs in the algebra than just those coming from proofs, we define a variant of execution (called weak execution). Its application to any program of clauses is shown to terminate with a bound on the number of steps which is elementary in the size of the program. We establish that weak execution coincides with standard execution on programs coming from proofs.