Execution models for Constraint Programming: kernel language design through semantics equivalence.

Abstract : Logic programming and constraint programming are two declarative programming paradigms which rely on the identification of programs to theories, and program- ming to modeling. Execution models result from the operational interpretation of logical provability in logic programming, and of constraint propagation in constraint programming. However, the control of execution is crucial for the practicability of these schemes and extra-logical traits are thus added in those programming systems, with the classical slogans "logic program = logical theory + control", "constraint program = constraint model + search". This thesis investigates execution models in which control and search can be shifted into the logic or the constraint model, while preserving the semantics. The three parts of the thesis correspond to the three semantics equivalence that are showed: the first between two committed-choice forward-chaining logic languages, the second between constraint logic programs and constraint models, and the third between guard semantics in angelic settings. Each of these equivalence is constructive in the sense that there exists an encoding that enables the compilation from one of the paradigm to the other. First, we show that simple program transformations exist back and forth be- tween Constraint Handling Rules (CHR) and Linear Logic Concurrent Constraint (LLCC) languages, making them semantically equivalent even if syntactically dif- ferent, which closes the question of implementing a committed-choice semantics for LLCC by using CHR as kernel language. Secondly, we show that a wide variety of search procedures can be internalized in the constraint model with a fixed enumeration strategy. Transforming search procedures into constraint satisfaction problems presents several advantages: (1) it makes search strategies declarative and modeled as constraint satisfaction problems; (2) it makes it possible to express search strategies in existing front-end modeling languages without any extension; (3) it opens up constraint propagation algorithms to search constraints and to the implementation of novel search procedures based on constraint propagation. This is illustrated with the design of the ClpZinc modeling language, with an angelic interpretation of Horn clauses which allows compilation to a reification-based constraint kernel. Finally, in concurrent constraint logic programming, committed-choice semantics create a hierarchy of non-equivalent semantics axed on the expressive power of synchronization mechanism. We show that the hierarchy of guard semantics col- lapses with angelic semantics, allowing the most primitive synchronization mechanism to encode all the others. The main consequence of this collapse is the identification of a kernel language, with a primitive synchronization mechanism and an elementary constraint system which are sufficient to reconstruct the other forms of synchronizations and other constraint systems as modules, in the software engineering sense.
Keywords : no keywords
Document type :
Theses
Complete list of metadatas

Cited literature [76 references]  Display  Hide  Download

https://hal.inria.fr/tel-01251695
Contributor : Sylvain Soliman <>
Submitted on : Wednesday, January 6, 2016 - 3:51:31 PM
Last modification on : Friday, May 25, 2018 - 12:02:07 PM
Long-term archiving on : Thursday, April 7, 2016 - 4:05:36 PM

Identifiers

  • HAL Id : tel-01251695, version 1

Collections

Citation

Thierry Martinez. Execution models for Constraint Programming: kernel language design through semantics equivalence. . Programming Languages [cs.PL]. Paris Diderot, 2015. English. ⟨tel-01251695⟩

Share

Metrics

Record views

258

Files downloads

265