Sequentiality by Linear Implication and Universal Quantification

Abstract

In this paper we address the issue of understanding sequential and parallel composition of agents from a logical viewpoint. In particular we use methods of abstract logic programming in linear logic, i.e. computations are modeled as proof searches in a suitable fragment of linear logic. While parallel composition has a straightforward treatment in this setting, sequential composition is much more difficult to be obtained. We study a case, directly inspired by Mon- teiro’s distributed logic, in which the causality relation among agents forms a series-parallel order; top agents may be recursively rewritten by series-parallel structures of new agents. We show a very declarative and simple treatment of sequentialization, which smoothly integrates with parallelization, by translating our formal system into linear logic in a complete way. This means that we obtain a full two ways correspondence between proofs and computations; thus we have full correspondence between the two formalisms. Our case study is very general per se, but it should be clear that the methodology adopted should be extensible to orderings more general than the series-parallel ones. The expected outcomes of this research are at least twofold: having some new insights in the design of concurrent languages and formalisms and having a strong starting point for relating linear logic semantics to concurrency semantics.