This thesis intends to investigate two aspects of Constraint Handling Rules (CHR). It
proposes a compositional semantics and a technique for program transformation.
CHR is a concurrent committed-choice constraint logic programming language consisting
of guarded rules, which transform multi-sets of atomic formulas (constraints) into
simpler ones until exhaustion [Frü06] and it belongs to the declarative languages family.
It was initially designed for writing constraint solvers but it has recently also proven to be
a general purpose language, being as it is Turing equivalent [SSD05a].
Compositionality is the first CHR aspect to be considered. A trace based compositional
semantics for CHR was previously defined in [DGM05]. The reference operational
semantics for such a compositional model was the original operational semantics for CHR
which, due to the propagation rule, admits trivial non-termination.
In this thesis we extend the work of [DGM05] by introducing a more refined trace
based compositional semantics which also includes the history. The use of history is a
well-known technique in CHR which permits us to trace the application of propagation
rules and consequently it permits trivial non-termination avoidance [Abd97, DSGdlBH04].
Naturally, the reference operational semantics, of our new compositional one, uses history
to avoid trivial non-termination too.
Program transformation is the second CHR aspect to be considered, with particular
regard to the unfolding technique. Said technique is an appealing approach which allows
us to optimize a given program and in more detail to improve run-time efficiency or spaceconsumption.
Essentially it consists of a sequence of syntactic program manipulations
which preserve a kind of semantic equivalence called qualified answer [Frü98], between
the original program and the transformed ones. The unfolding technique is one of the
basic operations which is used by most program transformation systems. It consists in the
replacement of a procedure-call by its definition. In CHR every conjunction of constraints
can be considered as a procedure-call, every CHR rule can be considered as a procedure
and the body of said rule represents the definition of the call. While there is a large body
of literature on transformation and unfolding of sequential programs, very few papers
have addressed this issue for concurrent languages.
We define an unfolding rule, show its correctness and discuss some conditions in
which it can be used to delete an unfolded rule while preserving the meaning of the original
program. Finally, confluence and termination maintenance between the original and
transformed programs are shown.
This thesis is organized in the following manner. Chapter 1 gives some general notion
about CHR. Section 1.1 outlines the history of programming languages with particular
attention to CHR and related languages. Then, Section 1.2 introduces CHR using examples.
Section 1.3 gives some preliminaries which will be used during the thesis. Subsequentely,
Section 1.4 introduces the syntax and the operational and declarative semantics
for the first CHR language proposed. Finally, the methodologies to solve the problem of
trivial non-termination related to propagation rules are discussed in Section 1.5.
Chapter 2 introduces a compositional semantics for CHR where the propagation rules
are considered. In particular, Section 2.1 contains the definition of the semantics. Hence,
Section 2.2 presents the compositionality results. Afterwards Section 2.3 expounds upon
the correctness results.
Chapter 3 presents a particular program transformation known as unfolding. This
transformation needs a particular syntax called annotated which is introduced in Section
3.1 and its related modified operational semantics !0t is presented in Section 3.2.
Subsequently, Section 3.3 defines the unfolding rule and prove its correctness. Then, in
Section 3.4 the problems related to the replacement of a rule by its unfolded version are
discussed and this in turn gives a correctness condition which holds for a specific class of
rules. Section 3.5 proves that confluence and termination are preserved by the program
modifications introduced.
Finally, Chapter 4 concludes by discussing related works and directions for future
work.
| Identifer | oai:union.ndltd.org:unibo.it/oai:amsdottorato.cib.unibo.it:912 |
| Date | 28 April 2008 |
| Creators | Tacchella, Paolo <1976> |
| Contributors | Gabbrielli, Maurizio |
| Publisher | Alma Mater Studiorum - Università di Bologna |
| Source Sets | Università di Bologna |
| Language | English |
| Detected Language | English |
| Type | Doctoral Thesis, PeerReviewed |
| Format | application/pdf |
| Rights | info:eu-repo/semantics/openAccess |
Page generated in 0.0016 seconds