PhD Defense of Jon Sneyers

Constraint Handling Rules (CHR) is a very-high-level declarative programming language based on concurrent multiset rewrite rules that are conditional, multi-headed, and committed-choice. Originally designed in the early 1990s as a special-purpose programming language for adding user-defined constraint solvers to a host language, CHR has evolved over the last decade into a powerful and elegant general-purpose language with a wide spectrum of application domains.

Computational complexity theory is the study of scalability of computer programs in terms of the computational resources they require — in particular, time (cpu usage) and space (memory usage).

In this dissertation we investigate the CHR programming language from the point of view of computational complexity theory. The first part introduces complexity theory, CHR, and CHR compilation. In the second part, we improve the state of the art by proposing and implementing several compiler optimizations. We confirm experimentally that these optimizations improve both the time and space complexity of CHR programs.

Finally, in the third part of this dissertation, we prove a “complexity-wise completeness” result. We demonstrate that the CHR language and state-of-the-art CHR systems (that implement the compiler optimizations of the previous part) are sufficiently efficient in the following precise sense: every algorithm can be implemented in CHR and be executed with the optimal asymptotic time and space complexity.