Hostname: page-component-cd9895bd7-mkpzs Total loading time: 0 Render date: 2024-12-25T05:17:30.706Z Has data issue: false hasContentIssue false
  • English
  • Français

A Proof Theoretic Study of Soft Concurrent Constraint Programming

Published online by Cambridge University Press:  21 July 2014

ELAINE PIMENTEL ,
CARLOS OLARTE  and
VIVEK NIGAM
ELAINE PIMENTEL
Affiliation:
Universidade Federal do Rio Grande do Norte, Natal, Brazil (e-mail: [email protected])
CARLOS OLARTE
Affiliation:
Pontificia Universidad Javeriana Cali, Colombia, Universidade Federal do Rio Grande do Norte, Natal, Brazil (e-mail: [email protected])
VIVEK NIGAM
Affiliation:
Universidade Federal da Paraíba, João Pessoa, Brazil (e-mail: [email protected])
Get access Rights & Permissions [Opens in a new window]

Abstract

Concurrent Constraint Programming (CCP) is a simple and powerful model for concurrency where agents interact by telling and asking constraints. Since their inception, CCP-languages have been designed for having a strong connection to logic. In fact, the underlying constraint system can be built from a suitable fragment of intuitionistic (linear) logic -ILL- and processes can be interpreted as formulas in ILL. Constraints as ILL formulas fail to represent accurately situations where “preferences” (called soft constraints) such as probabilities, uncertainty or fuzziness are present. In order to circumvent this problem, c-semirings have been proposed as algebraic structures for defining constraint systems where agents are allowed to tell and ask soft constraints. Nevertheless, in this case, the tight connection to logic and proof theory is lost. In this work, we give a proof theoretical meaning to soft constraints: they can be defined as formulas in a suitable fragment of ILL with subexponentials (SELL) where subexponentials, ordered in a c-semiring structure, are interpreted as preferences. We hence achieve two goals: (1) obtain a CCP language where agents can tell and ask soft constraints and (2) prove that the language in (1) has a strong connection with logic. Hence we keep a declarative reading of processes as formulas while providing a logical framework for soft-CCP based systems. An interesting side effect of (1) is that one is also able to handle probabilities (and other modalities) in SELL, by restricting the use of the promotion rule for non-idempotent c-semirings.This finer way of controlling subexponentials allows for considering more interesting spaces and restrictions, and it opens the possibility of specifying more challenging computational systems.

Keywords

Concurrent Constraint ProgrammingLinear LogicSoft Constraints
Type
Regular Papers
Information
Theory and Practice of Logic Programming , Volume 14 , Special Issue 4-5: 30th International Conference on Logic Programming , July 2014 , pp. 649 - 663
Copyright
Copyright © Cambridge University Press 2014 

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

Andreoli, J.-M. 1992. Logic programming with focusing proofs in linear logic. J. Log. Comput. 2, 3, 297–347.CrossRefGoogle Scholar
Bistarelli, S., Gabbrielli, M., Meo, M. C., and Santini, F. 2008. Timed soft concurrent constraint programs. In COORDINATION, LNCS, vol. 5052. Springer, 50–66.Google Scholar
Bistarelli, S., Montanari, U., and Rossi, F. 1997. Semiring-based constraint satisfaction and optimization. J. ACM 44, 2, 201–236.CrossRefGoogle Scholar
Bistarelli, S., Montanari, U., and Rossi, F. 2006. Soft concurrent constraint programming. ACM Trans. Comput. Log. 7, 3, 563–589.Google Scholar
Bistarelli, S., Montanari, U., Rossi, F., Schiex, T., Verfaillie, G., and Fargier, H. 1999. Semiring-based csps and valued csps: Frameworks, properties, and comparison. Constraints 4, 3, 199–240.CrossRefGoogle Scholar
Brunel, A., Gaboardi, M., Mazza, D., and Zdancewic, S. 2014. A core quantitative coeffect calculus. In ESOP, LNCS, vol. 8410. Springer, 351–370.Google Scholar
Chaudhuri, K. 2010. Classical and intuitionistic subexponential logics are equally expressive. In CSL, LNCS, vol. 6247. Springer, 185–199.Google Scholar
Danos, V., Joinet, J.-B., and Schellinx, H. 1993. The structure of exponentials: Uncovering the dynamics of linear logic proofs. In Kurt Gödel Colloq., LNCS, vol. 713. Springer, 159–171.Google Scholar
de Boer, F. S., Gabbrielli, M., and Meo, M. C. 2000. A timed concurrent constraint language. Inf. Comput. 161, 1, 45–83.Google Scholar
de Boer, F. S., Pierro, A. D., and Palamidessi, C. 1995. Nondeterminism and infinite computations in constraint programming. Theoretical Computer Science 151, 1, 37–78.Google Scholar
Fages, F., Ruet, P., and Soliman, S. 2001. Linear concurrent constraint programming: Operational and phase semantics. Inf. Comput. 165, 1, 14–41.CrossRefGoogle Scholar
Ghica, D. R. and Smith, A. 2013. From bounded affine types to automatic timing analysis. CoRR abs/1307.2473.Google Scholar
Girard, J.-Y. 1987. Linear logic. Theor. Comput. Sci. 50, 1–102.Google Scholar
Haemmerlé, R., Fages, F., and Soliman, S. 2007. Closures and modules within linear logic concurrent constraint programming. In FSTTCS, LNCS, vol. 4855. Springer, 544–556.Google Scholar
Knight, S., Palamidessi, C., Panangaden, P., and Valencia, F. D. 2012. Spatial and epistemic modalities in constraint-based process calculi. In CONCUR, LNCS, vol. 7454. Springer, 317–332.Google Scholar
Nigam, V. and Miller, D. 2009. Algorithmic specifications in linear logic with subexponentials. In PPDP, ACM, 129–140.Google Scholar
Nigam, V., Olarte, C., and Pimentel, E. 2013. A general proof system for modalities in concurrent constraint programming. In CONCUR, LNCS, vol. 8052. Springer, 410–424.Google Scholar
Olarte, C., Nigam, V., and Pimentel, E. 2013. Dynamic spaces in concurrent constraint programming. In LSFA'13. To be published in ENTCS.Google Scholar
Olarte, C., Rueda, C., and Valencia, F. D. 2013. Models and emerging trends of concurrent constraint programming. Constraints 18, 4, 535–578.CrossRefGoogle Scholar
Pimentel, E., Olarte, C., and Nigam, V. 2013. A Proof Theoretic Study of Soft CCP. CoRR abs/1405.2329, http://arxiv.org/abs/1405.2329.Google Scholar
Rossi, F., van Beek, P., and Walsh, T., Eds. 2006. Handbook of Constraint Programming. Foundations of Artificial Intelligence, vol. 2. Elsevier.Google Scholar
Saraswat, V. A., Jagadeesan, R., and Gupta, V. 1996. Timed default concurrent constraint programming. J. Symb. Comput. 22, 5/6, 475–520.Google Scholar
Saraswat, V. A., Rinard, M. C., and Panangaden, P. 1991. Semantic foundations of concurrent constraint programming. In POPL, ACM Press, 333–352.Google Scholar
Schiex, T., Fargier, H., and Verfaillie, G. 1995. Valued constraint satisfaction problems: Hard and easy problems. In IJCAI (1). Morgan Kaufmann, 631–639.Google Scholar
Wilson, N. 2006. A logic of soft constraints based on partially ordered preferences. J. Heuristics 12, 4-5, 241–262.Google Scholar
Supplementary material: PDF

PIMENTEL et al.

A Proof Theoretic Study of Soft Concurrent Constraint Programming

Download PIMENTEL et al.(PDF)
PDF 83.7 KB