In the logic programming paradigm, a program is defined by a set of methods, each of which can be executed when specific conditions are met during the current state of an execution. The semantics of these programs can be elegantly represented using sequent calculi, in which each method is linked to an inference rule. In this context, proof search mirrors the program's execution. Previous works introduced a framework in which the process of constructing proof nets is employed to model executions, as opposed to the traditional approach of proof search in sequent calculus. This paper further extends this investigation by focussing on the pure multiplicative fragment of this framework. We demonstrate, providing practical examples, the capability to define logic programming methods with context-sensitive behaviors solely through specific resource-preserving and context-free operations, corresponding to certain generalized multiplicative connectives explored in existing literature. We show how some of these methods, although still multiplicative, escape the purely multiplicative fragment of Linear Logic (MLL).
翻译:在逻辑编程范式中,程序由一组方法定义,每个方法可在当前执行状态满足特定条件时执行。这些程序的语义可通过相继式演算优雅地表示,其中每个方法与一条推理规则相关联。在此语境下,证明搜索模拟了程序的执行过程。先前的研究引入了一种框架,该框架采用构建证明网的过程来建模程序执行,而非传统的相继式演算中的证明搜索方法。本文进一步深化这一研究,聚焦于该框架的纯乘法片段。通过提供实际示例,我们论证了仅通过特定的资源保持型与上下文无关操作(对应于现有文献中探讨的若干广义乘法连接词)即可定义具有上下文敏感行为的逻辑编程方法的能力。我们展示了其中某些方法尽管仍属于乘法类型,却超出了线性逻辑(MLL)的纯乘法片段。