Catuscia Palamidessi

Main works - abstracts and links     Note: this document is not updated anymore

Concurrency Theory

Comparing the expressive power of the Synchronous and the Asynchronous pi-calculus. Proc. of the 24th ACM Symposium on Principles of Programming Languages (POPL), pages 256--265, ACM, 1997. Postscript available.

ABSTRACT

The Asynchronous pi-calculus, as recently proposed by Boudol and, independently, by Honda and Tokoro, is a subset of the pi-calculus which contains no explicit operators for choice and output-prefixing. The communication mechanism of this calculus, however, is powerful enough to simulate output-prefixing, as shown by Boudol, and input-guarded choice, as shown recently by Nestmann and Pierce. A natural question arises, then, whether or not it is possible to embed in it the full pi-calculus. We show that this is not possible, i.e. there does not exist any uniform, parallel-preserving, translation from the pi-calculus into the asynchronous pi-calculus, up to any ``reasonable'' notion of equivalence. This result is based on the incapablity of the asynchronous pi-calculus of breaking certain symmetries possibly present in the initial communication graph. By similar arguments, we prove a separation result between the pi-calculus and CCS.

Embedding as a Tool for Language Comparison. (With F.S. de Boer.) Information and Computation, 108(1):128-157, 1994. Postscript available.

ABSTRACT

This paper addresses the problem of defining a formal tool to compare the expressive power of different concurrent languages. We refine the notion of embedding by adding some "reasonable" conditions, suitable for concurrent frameworks. The new notion, called modular embedding, is used to define a preorder among languages, representing different degrees of expressiveness. We show that this preorder is not trivial (i.e. it does not collapse into one equivalence class) by proving that Flat CP cannot be embedded into Flat GHC, and that Flat GHC cannot be embedded into a language without communication primitives in the guards, while the converses hold.

Earlier work of mine on this subject includes the papers:

• Embedding as a tool for language comparison: On the CSP hierarchy (Proc. of CONCUR 91), where an analogous separation result is shown for CSP with input guards wrt full CSP.
• Concurrent logic languages: Asynchronism and language comparison (Proc. of NACLP 90), where the concept of modular embedding was first proposed to compare the expressive power of concurrent logic languages.

A paradigm for asynchronous communication and its application to concurrent constraint programming. (With F.S. de Boer, J.N. Kok, and J.J.M.M. Rutten.) Chapter 4 in K. Apt, J.W. de Bakker, and J.J.M.M. Rutten, editors, Logic Programming Languages: Constraints, Functions, and Objects, pages 82-114. Series in Logic Programming, The MIT Press, 1993. Postscript available.

ABSTRACT

We develop a general semantic theory of asynchronous communication in concurrent logic and concurrent constraint languages. The main characteristic of these languages, from the point of view of the communication mechanism, is that processes interact by querying and updating some common data structure. We abstract from the specific features of the underlying data structure by means of a uniform language of which the actions are interpreted as transformations on an abstract set of states. This approach shows that there exists a basic similarity between concurrent logic (constraint) languages and other languages based on asynchronous communication, like dataflow and asynchronous CSP. Actually, our intention is to capture languages based on asynchronous communication as instances of this uniform language, such an instance being determined by a specific set of states and interpretation of the actions. The computational model of our paradigm is described by a transition system in the style of Plotkin's SOS. A compositional model is presented that is based on reactive sequences, i.e., sequences of pairs of states.

A preliminary version of this paper, with title The failure of failures: Towards a paradigm for asynchronous communication, appeared in the proceedings of CONCUR 91.

The results of this work have been subsequently extended with a notion of block and locality operator, in the paper On Blocks: locality and asynchronous communication.

Asynchronous communication in process algebra. (With F.S. de Boer and J.W. Klop.) In Proc. of the seventh annual IEEE symposium on Logics in Computer Science (LICS), pages 137-147. IEEE Computer Society Press, Los Alamitos, California, 1992. Postscript available.

ABSTRACT

We study the paradigm of asynchronous process communication, as contrasted with the synchronous communication mechanism which is present in process algebra frameworks such as CCS, CSP and ACP. We investigate semantics and axiomatizations with respect to various observability criteria: bisimulation, traces and abstract traces. Our aim is to develop a process theory which can be regarded as a kernel for languages based on asynchronous communication, like data flow, concurrent logic languages and concurrent constraint programming.

Concurrent Constraint Programming

Infinite computations in nondeterministic constraint programming. (With F.S. de Boer and A. Di Pierro.) Theoretical Computer Science, 151:37-78, 1995. Postscript available.

ABSTRACT

We investigate the semantics of concurrent constraint programming and of various sublanguages, with particular emphasis on nondeterminism and infinite behavior. The aim is to find out what is the minimal structure which a domain must have in order to capture these two aspects. We show that a notion of observables, obtained by the upward-closure of the results of computations, is relatively easy to model even in presence of synchronization. On the contrary modeling the exact set of results is problematic, even for the simple sublanguage of constraint logic programming. We show that most of the standard topological techniques fail in capturing this more precise notion of observables. The analysis of these failed attempts leads us to consider a categorical approach.

Confluence in Concurrent Constraint Programming. (With M. Falaschi, M. Gabbrielli, and K. Marriott.) Theoretical Computer Science. To appear. Postscript available.

ABSTRACT

Concurrent constraint programming (ccp), like most of the concurrent paradigms, has a mechanism of global choice which makes computations dependent on the scheduling of processes. This is one of the main reasons why the formal semantics of ccp is more complicated than the one of its deterministic and local-choice sublanguages. In this paper we study various subsets of ccp obtained by adding some restriction on the notion of choice, or by requiring confluency, i.e. independency from the scheduling strategy. We show that it is possible to define simple denotational semantics for these subsets, for various notions of observables. Finally, as an application of our results we develop a framework for the compositional analysis of full ccp. The basic idea is to approximate an arbitrary ccp program by a program in the restricted language, and then analyze the latter, by applying the standard techniques of abstract interpretation to its denotational semantics.

A preliminary version of this paper, with title Confluence and Concurrent Constraint Programming, appeared in the proceedings of AMAST 95.

Related work: Constraint Logic Programming with Dynamic Scheduling: A Semantics Based on Closure Operators. (With M. Falaschi, K. Marriott, and M. Gabbrielli.)

Proving Concurrent Constraint Programs Correct. (With F.S. de Boer, M. Gabbrielli, and E. Marchiori.) Submitted to ACM-TOPLAS. Postscript available.

ABSTRACT

We address the problem of proving (partial) correctness of concurrent constraint programs (ccp). We develop a compositional proof-theory on the basis of a denotational approximation of the strongest postcondition semantics. This denotational semantics allows to view programs as theories in a suitable specification logic thus providing a justification of the (claimed) declarative nature of ccp. Concerning completeness, we prove that the system is (relatively) complete for the class of programs in which the denotational semantics characterizes exactly the strongest postcondition. This class includes the so-called confluent ccp, a special case of which is constraint logic programming with dynamic scheduling.

Previous work on this subject appeared in the papers:

• Proving Concurrent Constraint Programs Correct. (With F.S. de Boer, M. Gabbrielli, and E. Marchiori.) Proc. of the twentieth ACM Symposium on Principles of Programming Languages (POPL), 1994.
• Proving Correctness of Constraint Logic Programs with Dynamic Scheduling. (With F.S. de Boer and M. Gabbrielli.) Proc. of SAS 96.

Compositional Analysis for Concurrent Constraint Programming. (With M. Falaschi, M. Gabbrielli, and K. Marriott.) Proc. of the Eight Annual IEEE Symposium on Logic in Computer Science, (LICS), pages 210-221. IEEE Computer Society Press, Los Alamitos, California, 1993. Postscript available.

ABSTRACT

We propose a framework for the analysis of concurrent constraint programming (ccp). Our approach is based on simple denotational semantics which approximate the usual semantics in the sense that they give a superset of the input-output relation of a ccp program. Analyses based on these semantics can be easily and efficiently implemented using standard techniques from the analysis of logic programs.

A Fully Abstract Model for Concurrent Constraint Programming. (With F.S. de Boer.) In S. Abramsky and T.S.E. Maibaum, editors, Proc. of TAPSOFT/CAAP, volume 493 of Lecture Notes in Computer Science, pages 296-319. Springer-Verlag, 1991. Postscript available.

ABSTRACT

Recent results in [BP90] have shown that concurrent Logic programming has a very simple model, based on linear sequences, which is fully abstract with respect to the parallel operator and finite observables. This is intrinsically related to the asynchronous and monotonic nature of the communication mechanism, which consists of asking and telling constraints on a common store. We consider here a paradigm for (asynchronous) concurrent programming, based on the above mechanism, and provided with the standard operators of choice, parallelism, prefixing, and hiding of local variables. It comes out that linear sequences still suffice for a compositional description of all the operators. Moreover, we consider the problem of full abstraction. Since our notion of observables implies the removal of silent steps, the presence of the choice operator induces the same problems (for compositionality) as bisimulation in CCS. We show that in our framework this problem has a simple solution which consists of introducing a semantical distinction between the various ways in which deadlock and failure might occur. The resulting semantics is fully abstract and still based on linear sequences.

[BP90] Concurrent logic languages: Asynchronism and language comparison.

See also From Concurrent Logic Programming to Concurrent Constraint Programming and A paradigm for asynchronous communication and its application to concurrent constraint programming.

Abstract Interpretation

Complementation in Abstract Interpretation. (With A. Cortesi, G. File', R. Giacobazzi, and F. Ranzato.) ACM-TOPLAS, 19(1), 1997. Postscript available.

ABSTRACT

The reduced product of abstract domains is a rather well known operation for domain composition in abstract interpretation. In this paper, we study its inverse operation, introducing a notion of domain complementation in abstract interpretation. Complementation provides a systematic way to design new abstract domains, and it allows to systematically decompose domains. Also, such an operation allows to simplify domain verification problems, and it yields space saving representations for complex domains. We show that the complement exists in most cases, and we apply complementation to three well known abstract domains, notably to Cousot and Cousot's interval domain for integer variable analysis, to Cousot and Cousot's comportment domain for analysis of functional languages and to the complex domain Sharing for aliasing analysis of logic languages.

A preliminary version of this paper, with the same title, appeared in the proceedings of SAS 95.

The foundations of this work are provided by the results of the paper Weak Relative Pseudo-Complements of Closure Operators.

See also Confluence in Concurrent Constraint Programming and Compositional Analysis for Concurrent Constraint Programming.

Lattice Theory

Weak Relative Pseudo-Complements of Closure Operators. (With R. Giacobazzi and F. Ranzato.) Algebra Universalis, 36(3): 405--412, 1996. Postscript available.

(For more details and examples see the Report version.)

ABSTRACT

We define the notion of weak relative pseudo-complement, and we show that, for an arbitrary lattice, the property of weak relative pseudo-complementation is strictly weaker than relative pseudo-complementation, but stronger than pseudo-complementation. Our main interest for this notion is in relation with the theory of closure operators. We prove that if a complete lattice L is completely inf-distributive with respect to chains, then every closure operator on L admits weak relative pseudo-complements with respect to continuous closure operators on L.

Constraint Logic Programming

An algebraic perspective of constraint logic programming. (With F.S. de Boer and A. Di Pierro.) Journal of Logic and Computation, 7(1): 1--38, 1997. Postscript available.

ABSTRACT

We develop a denotational, fully abstract semantics for constraint logic programming (clp) with respect to successful and failed observables. The denotational approach turns out very useful for the definition of new operators on the language as the counterpart of some abstract operations on the denotational domain. In particular, by defining our domain as a cylindric Heyting algebra, we can exploit, to this aim, operations of both cylindric algebras (such as cylindrification), and Heyting algebras (such as implication and negation). The former allows us to generalize the clp language by introducing an explicit hiding operator; the latter allows us to define a notion of negation which extends the classical negation used in Logic Programming. In particular, we show that our notion subsumes both Negation as Failure and Negation as Instantiation.

A preliminary version of this paper, with title A Logical Denotational Semantics for Constraint Logic Programming, appeared in the proceedings of ESOP 94.

Semantics of Logic Programming

A Declarative Approach for First-Order Built-in's of Prolog. (With K.R. Apt and E. Marchiori.) Applicable Algebra in Engineering, Communication and Computing, 5(3/4):159-191, 1994. Postscript available.

ABSTRACT

We provide here a framework for studying Prolog programs with various built-in's that include arithmetic operations, and such metalogical relations like var and ground. To this end we propose a new, declarative semantics and prove completeness of the Prolog computation mechanism w.r.t. this semantics. We also show that this semantics is fully abstract in an appropriate sense. Finally, we provide a method for proving termination of Prolog programs with built-in's which uses this semantics. The method is shown to be modular and is illustrated by proving termination of a number of programs including the UNIFY program of Sterling and Shapiro.

A preliminary version of this paper, with title A Theory of First-Order Built-in's of Prolog, appeared in the proceedings of ALP 92.

A model-theoretic reconstruction of the operational semantics of logic programs. (With M. Falaschi, G. Levi, and M. Martelli.) Information and Computation}, 103(1):86-113, 1993.

ABSTRACT

In this paper we define a new notion of truth on Herbrand interpretations extended with variables which allows us to capture, by means of suitable models, various observable properties, such as the ground success set, the set of atomic consequences, and the computed answer substitutions. The notion of truth extends the classical one to account for non-ground formulas in the interpretations. The various operational semantics are all models. An ordering on interpretations is defined to overcome the problem that the intersection of a set of models is not necessarily a model. The set of interpretations with this partial order is shown to be a complete lattice, and the greatest lower bound of any set of models is shown to be a model. Thus there exists a least model, which is the least herbrand model and therefore the ground success set semantics. Richer operational semantics are non-least models, which can, however, be effectively defined by fixpoint constructions. The model corresponding to the computed answer substitutions operational semantics is the most primitive one (the other can be easily obtained from it).

This work continues the investigation about the semantics of Logic Programming following ideas firstly proposed in the paper Declarative modeling of the operational behaviour of logic languages.

Declarative modeling of the operational behaviour of logic languages. (With M. Falaschi, G. Levi, and M. Martelli.) Theoretical Computer Science, 69(3):289-318, 1989.

ABSTRACT

The paper defines a new declarative semantics for logic programs, which is based on interpretations containing (possibly) non ground atoms. Two different interpretation notions are introduced and the corresponding models are defined and compared. The classical results on the Herbrand model semantics of logic programs are shown to hold in the new models too (i.e. existence of a minimal model, fixpoint characterization, etc.). With the new notion of model, we have a stronger soundness and completeness result for SLD-resolution. In particular, one of the two models allows to precisely characterize the set of computed answer substitutions.

A preliminary version of this paper, with title A new declarative semantics for logic languages, appeared in the proceedings of ICSLP 88.

Negation in Logic Programming

Negation as Instantiation. (With A. Di Pierro and M. Martelli.) Information and Computation, 120(2):263-278, 1995. Postscript available.

ABSTRACT

We propose a new negation rule for logic programming which derives existentially closed negative literals, and we define a version of completion for which this rule is sound and complete. The rule is called "Negation As Instantiation" (NAI). According to it, a negated atom succeeds whenever all the branches of the SLD-tree for the atom either fail or instantiate the atom. The set of the atoms whose negation is inferred by the NAI rule is proved equivalent to the complement of $T_c\!\downarrow\!\omega$, where $T_c$ is the immediate consequence operator extended to non-ground atoms (Falaschi et al., 1989). The NAI rule subsumes negation as failure on ground atoms, it excludes floundering and can be efficiently implemented. We formalize this way of handling negation in terms of SLDNI-resolution (SLD-resolution with Negation as Instantiation). Finally, we amalgamate SLDNI-resolution and SLDNF-resolution, thus obtaining a new resolution procedure which is able to treat negative literals with both existentially quantified variables and free variables, and we prove its correctness.

A preliminary version of this paper, with title Negation As Instantiation: a New Rule for the Treatment of Negation in Logic Programming, appeared in the proceedings of ICLP 91.

See also An algebraic perspective of constraint logic programming.

Concurrent Logic Programming

From Concurrent Logic Programming to Concurrent Constraint Programming. (With F.S. de Boer.) Chapter 2 in G. Levi, editor, Advances in logic programming theory, pages 55-113. Oxford University Press, 1994. Postscript available.

ABSTRACT

The endeavor to extend logic programming to a language suitable for concurrent systems has stimulated in the last decade an intensive research, resulting in a large variety of proposals. A common feature of the various approaches is the attempt to define mechanisms for concurrency within the logical paradigm, the driving ideal being the balance between expressiveness and declarative reading. In this survey we present the motivations, the principal lines along which the field has developed, the various paradigms which have been proposed, and the main approaches to the semantic foundations.

Integration of Logic and Functional Programming

Kernel LEAF: a logic plus functional language. (With E. Giovannetti, G. Levi, and C. Moiso.) Journal of Computer and System Sciences, 42(2):139-185, 1991.

ABSTRACT

Kernel-LEAF is a logic plus functional language based on the flattening technique. It differs from other similar languages because it is able to cope with partial (undefined or non terminating) functions. This is achieved by introducing the distinction between data structures and (functional) term structures, and by using two kinds of equality. The language has a clean model-theoretic semantics, where the domains of the interpretations are the algebraic CPOÕs. In these domains the difference between the two equalities corresponds to a different behaviour with respect to continuity. The operational semantics (based on SLD-resolution) is proved correct and complete with respect to the model-theoretic one. Finally, an outermost strategy, more efficient than unrestricted SLD-resolution, but still complete, is presented.

A preliminary version of this paper, with title A complete semantic characterization of K-LEAF, a logic language with partial functions, appeared in the proceedings of ISLP 87.