Hostname: page-component-cd9895bd7-q99xh Total loading time: 0 Render date: 2024-12-18T13:18:24.707Z Has data issue: false hasContentIssue false
  • English
  • Français

Observational equivalences for linear logic concurrent constraint languages*

Published online by Cambridge University Press:  06 July 2011

RÉMY HAEMMERLÉ
RÉMY HAEMMERLÉ*
Affiliation:
Technical University of Madrid, Madrid, Spain
Get access Rights & Permissions [Opens in a new window]

Abstract

Linear logic Concurrent Constraint programming (LCC) is an extension of concurrent constraint programming (CC), where the constraint system is based on Girard's linear logic instead of the classical logic. In this paper, we address the problem of program equivalence for this programming framework. For this purpose, we present a structural operational semantics for LCC based on a label transition system and investigate different notions of observational equivalences inspired by the state of art of process algebras. Then, we demonstrate that the asynchronous π-calculus can be viewed as simple syntactical restrictions of LCC. Finally, we show that LCC observational equivalences can be transposed straightforwardly to classical Concurrent Constraint languages and Constraint Handling Rules, and investigate the resulting equivalences.

Keywords

Concurrent Constraint programminglinear logicobservational equivalencesbisimulationπ-calculusConstraint Handling Rules
Type
Regular Papers
Information
Theory and Practice of Logic Programming , Volume 11 , Special Issue 4-5: 27th International Conference on Logic Programming , July 2011 , pp. 469 - 485
Copyright
Copyright © Cambridge University Press 2011

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)

References

Abadi, M., Fournet, C. and Gonthier, G. 2000. Authentication primitives and their compilation. In Principles of Programming Languages. ACM Press, 302–315.Google Scholar
Abdennadher, S. and Frühwirth, T. 1998. On completion of constraint handling rules. In Principles and Practice of Constraint Programming. Lecture Notes in Computer Science, vol. 1520, Springer, 25–39.Google Scholar
Abdennadher, S. and Frühwirth, T. W. 1999. Operational equivalence of CHR programs and constraints. In Principles and Practice of Constraint Programming. Lecture Notes in Computer Science, vol. 1713. Springer, 43–57.Google Scholar
Aït-Kaci, H. 1991. Warren's Abstract Machine, A Tutorial Reconstruction. Logic Programming. MIT Press.CrossRefGoogle Scholar
Amadio, R. M., Castellani, I. and Sangiorgi, D. 1998. On bisimulations for the asynchronous pi-calculus. Theoretical Computer Science 195 (2), 291–324.CrossRefGoogle Scholar
Berry, G. and Boudol, G. 1992. The chemical abstract machine. Theoretical Computer Science 96 (1), 217–248.CrossRefGoogle Scholar
Best, E., de Boer, F. and Palamidessi, C. 1997. Partial order and SOS semantics for linear constraint programs. In Proc. of Coordination. Lecture Notes in Computer Science, vol. 1282. Springer, 256–273.Google Scholar
Buscemi, M. G. and Montanari, U. 2007. CC-Pi: A constraint-based language for specifying service level agreements. In European Symposium on Programming. Lecture Notes in Computer Science, vol. 4421. Springer, 18–32.Google Scholar
Díaz, J. F., Rueda, C. and Valencia, F. D. 1998. Pi+- calculus: A calculus for concurrent processes with constraints. CLEI Electronic Journal 1 (2).CrossRefGoogle Scholar
Duck, G. J., Stuckey, P. J., García de la Banda, M. and Christian, H. 2004. The refined operational semantics of Constraint Handling Rules. In Proc. of International Conference on Logic Programming. Lecture Notes in Computer Science, vol. 3132. Springer, 90–104.CrossRefGoogle Scholar
Duck, G. J., Stuckey, P. J. and Sulzmann, M. 2007. Observable confluence for constraint handling rules. In Proc. of International Conference on Logic Programming. Lecture Notes in Computer Science, vol. 4670. Springer, 224–239.CrossRefGoogle Scholar
Fages, F., Ruet, P. and Soliman, S. 2001. Linear concurrent constraint programming: Operational and phase semantics. Information and Computation 165 (1), 14–41.CrossRefGoogle Scholar
Fournet, C. and Gonthier, G. 2005. A hierarchy of equivalences for asynchronous calculi. Journal of Logic Algebra Programming 63 (1), 131–173.CrossRefGoogle Scholar
Frühwirth, T. 2009. Constraint Handling Rules. Cambridge University Press.CrossRefGoogle Scholar
Gilbert, D. and Palamidessi, C. 2000. Concurrent constraint programming with process mobility. In Computational Logic. Lecture Notes in Computer Science, vol. 1861. Springer, 463–477.Google Scholar
Girard, J.-Y. 1987. Linear logic. Theoretical Computer Science 50 (1), 1–101.CrossRefGoogle Scholar
Haemmerlé, R. 2011. Toward Observational Equivalences for Linear Logic Concurrent Constraint Languages. Technical Report CLIP5/2011, Technical University of Madrid (UPM).CrossRefGoogle Scholar
Haemmerlé, R., Fages, F. and Soliman, S. 2007. Closures and modules within linear logic concurrent constraint programming. In Foundations of Software Technology and Theoretical Computer Science. Lecture Notes in Computer Science, vol. 4855. Springer, 554–556.Google Scholar
Honda, K. and Yoshida, N. 1995. On reduction-based process semantics. Theoretical Computer Science 151 (2), 437–486.CrossRefGoogle Scholar
Huet, G. 1980 October. Confluent reductions: Abstract properties and applications to term rewriting systems: Abstract properties and applications to term rewriting systems. Journal of the ACM 27 (4), 797–821.CrossRefGoogle Scholar
Jaffar, J. and Lassez, J.-L. 1987. Constraint logic programming. In Proc. of 14th ACM Symposium on Principles of Programming Languages, Munich, Germany, 111–119.Google Scholar
Kahn, K. M. and Saraswat, V. A. 1990. Actors as a special case of concurrent constraint programming. In Proc. of Object Oriented Programming, Systems, Languages and Applications/European Conference on Object-Oriented Programming, 57–66.Google Scholar
Laneve, C. and Montanari, U. 1992. Mobility in the CC-paradigm. In Mathematical Foundations of Computer Science. Lecture Notes in Computer Science, vol. 629. Springer, 336–345.Google Scholar
Maher, M. J. 1987. Logic semantics for a class of committed-choice programs. In Proc. of International Conference on Logic Programming (ICLP '87). MIT Press.Google Scholar
Martinez, T. 2010. Semantics-preserving translations between linear concurrent constraint programming and constraint handling rules. In Principles and Practice of Declarative Programming. ACM Press, 57–66.Google Scholar
Milner, R. 1989. Communication and Concurrency. Prentice Hall.Google Scholar
Milner, R. and Sangiorgi, D. 1992. Barbed bisimulation. In Proc. of International Colloquium on Automata, Languages and Programming. Lecture Notes in Computer Science, vol. 623. Springer, 685–695.CrossRefGoogle Scholar
Nicola, R. D. and Hennessy, M. 1984. Testing equivalences for processes. Theoretical Computer Science 34, 83–133.CrossRefGoogle Scholar
Parrow, J. and Victor, B. 1998. The fusion calculus: Expressiveness and symmetry in mobile processes. In Logic in Computer Science. IEEE, 176–185.Google Scholar
Ruet, P. and Fages, F. 1997. Concurrent constraint programming and mixed non-commutative linear logic. In Proc. of Annual Conference on Computer Science Logic. Lecture Notes in Computer Science, vol. 1414. Springer, 406–423.Google Scholar
Saraswat, V. A. and Lincoln, P. 1992. Higher-Order Linear Concurrent Constraint Programming. Technical Report, Xerox Parc.CrossRefGoogle Scholar
Saraswat, V. A. and Rinard, M. C. 1990. Concurrent constraint programming. In Principles of Programming Languages. ACM Press, 232–245.Google Scholar
Saraswat, V. A., Rinard, M. C. and Panangaden, P. 1991. Semantic foundations of concurrent constraint programming. In Principles of Programming Languages. ACM, 333–352.Google Scholar
Soliman, S. 2003. Pi-calculus and LCC, a space odyssey. Research Report 4855, Institut National de Recherche en Informatique et en Automatique.Google Scholar
Tamura, N. 1998. User's Guide of a Linear Logic Theorem Prover. [online]. Kobe University. URL: http://bach.istc.kobe-u.ac.jp/llprover/.Google Scholar