Dipartimento di Informatica e Scienze dell'Informazione
Dipartimento di Informatica e Scienze dell'Informazione
An Effective Fixpoint Semantics for Linear Logic Programs
M. Bozzano,
G. Delzanno,
M. Martelli
In this paper we investigate the theoretical foundation of a new bottom-up semantics for linear logic programs, and more precisely for the fragment of LinLog that consists of the language LO enriched with the constant 1. We use constraints to symbolically and finitely represent possibly infinite collections of provable goals. We define a fixpoint semantics based on a new operator in the style of Tp working over constraints. An application of the fixpoint operator can be computed algorithmically. As sufficient conditions for termination, we show that the fixpoint computation is guaranteed to converge for propositional LO. To our knowledge, this is the first attempt to define an effective fixpoint semantics for linear logic programs. As an application of our framework, we also present a formal investigation of the relations between LO and Disjunctive Logic Programming. Using an approach based on abstract interpretation, we show that DLP fixpoint semantics can be viewed as an abstraction of our semantics for LO. We prove that the resulting abstraction is correct and complete for an interesting class of LO programs encoding Petri Nets.
Download the (gzipped) postscript version.
Fixpoint Semantics for a Fragment of First-Order Linear Logic
M. Bozzano
In this paper we investigate the theoretical foundation of a bottom-up, fixpoint semantics for a subset of Girard's linear logic. More precisely, we consider a first-order formulation of a fragment of LinLog including multiplicative disjunction and universal quantification over goals. The semantics is defined by means of a fixpoint operator which is monotonic and continuous over an extended notion of interpretation lattice. We prove soundness and completeness of this semantics with respect to the usual operational semantics. We discuss some applications and related work.
Download the (gzipped) postscript version.
On the Relations between Disjunctive and Linear Logic Programming
M. Bozzano,
G. Delzanno,
M. Martelli
In this paper we investigate the relationship between Disjunctive Logic Programming and a subset of Linear Logic, namely the fragment of LinLog which corresponds to Andreoli and Pareschi's LO. We analyze the two languages both from a top-down, operational perspective, and from a bottom-up, semantical one. From a proof-theoretical perspective, we show that, modulo a simple mapping between classical and linear connectives, LO can be viewed as a sub-structural fragment of DLP in which the rule of contraction is forbidden on the right-hand side of sequents. We also prove that LO is strictly more expressive than DLP in the propositional case. From a semantical perspective, after recalling the definition of a bottom-up fixpoint semantics for LO we have given in our previous work, we show that DLP fixpoint semantics can be viewed as an abstraction of the corresponding LO semantics, defined over a suitable abstract domain. We prove that the abstraction is correct and complete. Finally, we show that the previous property of the semantics is strictly related to proof-theoretical properties of the classical and linear logic fragments underlying DLP and LO.
Download the (gzipped) postscript version.
An Effective Bottom-Up Semantics for First Order
Linear Logic Programs and its Relationship with Decidability
Results for Timed Petri Nets
M. Bozzano,
G. Delzanno,
M. Martelli
We study the connection between algorithmic techniques for symbolic model checking, and declarative and operational aspects of linear logic programming. Specifically, we show that the construction used to decide verification problems for Timed Petri Nets can be used to define a new fixpoint semantics for the fragment of linear logic called LO. The fixpoint semantics is based on an effective Tp operator. As an alternative to traditional top-down approaches, the effective fixpoint operator can be used to define a bottom-up evaluation procedure for first-order linear logic programs.
Download the (gzipped) postscript version.
An Effective Bottom-Up Semantics for First Order
Linear Logic Programs
M. Bozzano,
G. Delzanno,
M. Martelli
We study the connection between algorithmic techniques for symbolic model checking, and declarative and operational aspects of linear logic programming. Specifically, we show that the construction used to decide verification problems for Timed Petri Nets can be used to define a new fixpoint semantics for the fragment of linear logic called LO. The fixpoint semantics is based on an effective Tp operator. As an alternative to traditional top-down approaches, the effective fixpoint operator can be used to define a bottom-up evaluation procedure for first-order linear logic programs.
Download the (gzipped) postscript version.
A Bottom-up Semantics for Linear Logic Programs
M. Bozzano,
G. Delzanno,
M. Martelli
The operational semantics of linear logic programming languages is given in terms of goal-driven sequent calculi. The proof-theoretic presentation is the natural counterpart of the top-down semantics of traditional logic programs. In this paper we investigate the theoretical foundation of an alternative operational semantics based on a bottom-up evaluation of linear logic programs via a fixpoint operator. The bottom-up fixpoint semantics is important in applications like active databases, and, more in general, for program analysis and verification. As a first case-study, we consider Andreoli and Pareschi's LO enriched with the connective 1. For this language, we give a fixpoint semantics based on an operator defined in the style of Tp. We give an algorithm to compute a single application of the fixpoint operator where constraints are used to represent in a finite way possibly infinite sets of provable goals. Furthermore, we show that the fixpoint semantics for propositional LO without the constant 1 can be computed after finitely many steps. To our knowledge, this is the first attempt to define an effective fixpoint semantics for LO. We hope that our work will open interesting perspectives for the analysis and verification of linear logic programming languages.
Download the (gzipped) postscript version.
A Bottom-up Semantics for LO - Preliminary Results
M. Bozzano,
G. Delzanno,
M. Martelli
The operational semantics of linear logic programming languages is given in terms of goal-driven sequent calculi for fragments of the logic. The proof-theoretic presentation is the natural counterpart of the top-down semantics of traditional logic programs. In this paper we investigate the theoretical foundation of an alternative operational semantics based on a bottom-up evaluation of linear logic programs via a fixpoint operator. The bottom-up fixpoint semantics is important in applications like active databases, and, more in general, for program analysis and verification. As a first case-study, we consider Andreoli and Pareschi's LO enriched with the connective 1. For this language, we give a fixpoint semantics based on an operator defined in the style of Tp. We give an algorithm to compute a single application of the fixpoint operator where constraints are used to represent in a finite way possibly infinite sets of provable goals. Furthermore, we show that the fixpoint semantics for propositional LO without the connective 1 can be computed after finitely many steps. To our knowledge, this is the first attempt to define an effective fixpoint semantics for LO. We hope that our work will open interesting perspectives for the analysis and verification of linear logic programming languages.
Download the (gzipped) postscript version.
A Linear Logic Specification of Chimera
M. Bozzano,
G. Delzanno,
M. Martelli
Forum, a powerful logic formalism based on Higher Order Linear Logic, is particularly suited to specify and reason about complex programs and systems. Ehhf, a subset of Forum, models many interesting logic programming extensions towards O.O. and concurrent systems and can be viewed as a very high level logic programming specification language. The paper presents some results in this direction, namely the specification in Ehhf of Chimera, an Active, Object-Oriented and Deductive Database System.
Download the (gzipped) postscript version.
A Linear Logic Semantics for Object-Oriented, Deductive and Active Databases
M. Bozzano,
G. Delzanno,
M. Martelli
Girard's linear logic provides powerful means for studying state transformations and resource consumption in computations within a completely logical framework. The starting point of this work is Forum, a presentation of higher order linear logic which is an abstract logic programming language, i.e., complete with respect to uniform proofs (cut-free and goal-directed proofs). A subset of Forum's formulas which form the logic programming language Ehhf, have been isolated and proved to be well-suited to encode a notion of state into sequents and proofs, to model state updates, and to provide constructs for parallel execution. In this paper, we will show how it is possible, using the language Ehhf, to define a clean and simple semantics for object-oriented, deductive and active databases in a completely logical setting, that accounts for the various aspects of computation. In order to do this, we will briefly describe the semantics of Chimera, an example of data model and language for DBMS which supports object-oriented, deductive, and active database features.
Download the (gzipped) postscript version.
Objects in a Higher-Order Linear Logic Setting (Extended Abstract)
G. Delzanno,
M. Martelli
In [1] some aspects of object-oriented programming have been
reformulated in the higher-order Linear Logic framework, F&O. based on
the language Forum [2].
In particular, it has been shown how it
could be possible to logically represent objects encapsulating method
definitions and how to describe meta-rules defining message passing and
self-application, according to different computational models.
A language based on such concepts has been designed and implemented in the higher-order language lambdaProlog, adding a form of inheritance which could be
handled at the moment of the objects creation.
In the paper, the above mentioned features are reformulated in the setting
of a more general framework based on the Proof as Computation interpretation of Linear Logic, which seems suitable to describe a many operational aspects of programming languages.
Differently from the authors' previous proposal [1],
inheritance is reconsidered by defining, in logical terms,
a delegation-based mechanism with characteristics
similar to the ones presented in [3,4].
Furthermore, the representation of an object is modified in order to
preserve encapsulation of methods in the newly defined setting where
objects can be dynamically extended.
[1] Objects in Forum - G.Delzanno & M.Martelli -
Proc. ICLP '95
[2] A Multiple-Conclusion Meta-Logic - D.Miller -
Proc. Symp. on Logic in CS '94
[3] A Lambda Calculus of Objects and Method Specification -
K. Fisher & F. Honsell & J.C. Mitchell - Nordic Journal of Computing '94
Download the (gzipped) postscript version.
back to Publications on Linear Logic