Topics related to constraint programming and Constraint Handling Rules

Below is a list of possible topics for practicals and diploma/bachelor/master theses related to constraint programming and Constraint Handling Rules. The topics serve as suggestions and can be adjusted accordingly. Additional topic suggestions are welcome.

 

If you are interested contact Prof. Frühwirth or Daniel Gall.

Justifications in CHR for Logical Retraction in Dynamic Algorithms

CHR with Justifications

When algorithms are written in CHR, constraints represent both data and operations. CHR is already incremental by nature, i.e. constraints can be added at runtime. Logical retraction adds decrementality. Hence any algorithm written in CHR with justifications will become fully dynamic. Operations can be undone and data can be removed at any point in the computation without compromising the correctness of the result.

A straightforward source-to-source transformation can introduce justifications for user-defined constraints into the CHR. Then a scheme of two rules suffices to allow for logical retraction (deletion, removal) of constraints during computation. Without the need to recompute from scratch, these rules remove not only the constraint but also undo all consequences of the rule applications that involved the constraint.

Goal

Further work should investigate implementation, dynamic algorithms and application domains of CHR with justifications:

  • research how logical as well as classical algorithms implemented in CHR behave when they become dynamic.
  • improve the implementation, optimize and benchmark it.
  • support detection and repair of inconsistencies (for error diagnosis), - support nonmonotonic logical behaviors (e.g. default logic, abduction, defeasible reasoning).

References

Non-Termination Analysis of Recursive Rules

Extend the analysis techniques and/or the associated tool from the following two research papers:

Thom Fruehwirth.
A Devil's Advocate against Termination of Direct Recursion, PPDP 2015.
Transformation Tool available (use "Devil" options).

A dynamic program analysis of the non-termination problem for recursion in the Constraint Handling Rules (CHR) language: A simple program transformation for recursive rules in CHR was introduced that produces one or more adversary rules. When the rules are executed together, a non-terminating computation may arise. It was shown that any non-terminating computation of the original rule contains this witness computation.

 Thom Fruehwirth.
Why Can’t You Behave? Non-Termination Analysis of Direct Recursive Rules with Constraints.
RuleML 2016.

A static program analysis of the non-termination problem for recursion in the Constraint Handling Rules (CHR) language: Theorems with so-called misbehavior conditions for potential non-termination and failure (as well as definite termination) of linear direct recursive simplification rules are given. Logical relationships between the constraints in a recursive rule play a crucial role in this kind of program analysis.

Voraussetzung: Vorlesung „Regelbasierte Programmierung“

Typ: Bachelorarbeit, Masterarbeit

Localized Constraint Stores

In distributed computation, data and processes are distributed over a network of stores and processing units. In a constraint-based programming language paradigm this means that constraints have to be annotated with spatial information defining their whereabouts. Obvious topologies are a distinction between global and local stores as well as trees. Localized constraints can also be used for so-called reified (or meta-)constraints (e.g. https://sicstus.sics.se/sicstus/docs/4.0.8/html/sicstus/Reified-Constraints.html), to store justifications and for spatial reasoning.

In Constraint Handling Rules (CHR), there is a simple source-to-source program transformation that adds local annotations to constraints.

The scope of the work includes implementation of such a transformation, their application and/or static program analysis to derive distribution patterns, i.e. to localize constraint computation while minimizing communication overhead.

References

Edmund S. L. Lam, Iliano Cervesato and Nabeeha Fatima CoMingle: Distributed Logic Programming for Decentralized Mobile Ensembles. In proceedings of International Conference on Distributed Computing Techniques (Coordination'15)

A. Raffaeta and T. Frühwirth, Spatio-Temporal Annotated Constraint Logic Programming, Third International Symposium on Practical Aspects of Declarative Languages (PADL'01), Las Vegas, USA, March 2001.

T. Frühwirth, Entailment Simplification and Constraint Constructors for User-Defined Constraints, Third Workshop on Constraint Logic Programming (WCLP 93),  Marseille, France, March 1993.

Voraussetzung: Vorlesung „Regelbasierte Programmierung“

Typ: Projekt, Bachelorarbeit, Masterarbeit

Invariant Checking and Generation by Confluence and Completion

Invariants (or assertions, properties, conditions) annotate program text and express static and dynamic properties of a program's execution. Invariants can be expressed as logical relations (predicates) over the program's variables. In the context of constraint-programming and Constraint Handling Rules (CHR), they amount to constraints. These can be readily added to the program to enforce the invariants. By comparing the program with and without invariants expressed as constraints using established program analysis techniques for CHR, namely confluence and program equivalence, we can check if the invariants hold in the program.

Furthermore, invariants can be strenghened and even be generated by adapting the so-called completion method (that is normally used to generate additional rules to make a CHR program confluent).

References

Johannes Langbein, Frank Raiser, Thom Frühwirth. A state equivalence and confluence checker for CHR. In P. Van Weert and L. De Koninck, editors, CHR '10: Proc. 7th Workshop on Constraint Handling Rules. K.U.Leuven, Department of Computer Science, Technical report CW 588, July 2010.

Prerequisites: Lecture Rule-based Programming

Type: Bachelor thesis, Master thesis, Dissertation

Program Slicing by Confluence and Completion

Program slicing is a program anaylsis technique whereby one extracts properties and relationships of variables in a program by removing from the program all statements that do not effect the assignments of the variables. In the context of constraint programming and Constraint Handling Rules that deal with logical relations (predicates) this amounts to the logical operation of variable projection. This means that we remove unwanted variables that are not of interest from the program by program transformation. This transformation can be accomplished by adapting the technique of "completion". It is usually used to make a non-confluent program confluent.

Related Work

Johannes Langbein, Frank Raiser, Thom Frühwirth. A state equivalence and confluence checker for CHR. In P. Van Weert and L. De Koninck, editors, CHR '10: Proc. 7th Workshop on Constraint Handling Rules. K.U.Leuven, Department of Computer Science, Technical report CW 588, July 2010.
http://www.uni-ulm.de/fileadmin/website_uni_ulm/iui.inst.170/home/raiser/publications/Langbein2010.pdf

Prerequisites: Lecture Rule-based Programming
Type: Bachelor thesis, Master thesis, Dissertation

Source-to-Source Transformation Engine for Constraint Handling Rules

The CHR research community often prototypes possible extensions of CHR by means of source-to-source transformations, i.e. new features of the language are realized by providing implementations based on the core CHR language.

The task in this thesis is to develop an engine that facilitates prototyping of these source-to-source transformations. The resulting tool should be evaluated by prototypically implementing well-known transformations (e.g. high-level compiler optimizations).

Requirements: Lecture Rule-based Programming

Type: Bachelor thesis, Master thesis

Computational Psychology

Science is based on the notion of a model that faithfully describes an aspect of the reality around us. Often, these models exist only on paper. The aim of the thesis is to identify a well-defined models in the scientific field of Computational Psychology and to implement them using the high-level language CHR. Such an implementation can than be efficiently executed in CHR, compared with experimental results and subjected to the wealth of CHR analysis techniques.

Computational Psychology combines experimental psychology with computer simulation and mathematical modeling. On the basis of well-defined theoretical concepts, computational approaches can provide a unifying language and methodology across disciplines ranging from neurobiology to cognitive science, systems biology, and information technology.

Cognitive science is the interdisciplinary study of the mind and its processes. It includes research on intelligence and behavior, focusing on how information is represented, processed, and transformed (e.g. in perception, language, memory, reasoning, and emotion). Cognitive science touches multiple research disciplines, including psychology, artificial intelligence, philosophy, neuroscience, linguistics, anthropology, sociology, and education.

Type: Bachelors thesis, Masters thesis

CHR Abstract Machine

Prolog (WAM) and then Java (JVM) popularized the concept of an abstract (or virtual) machine to implement programming languages in a systematic, portable yet efficient way. Such a machine shall be developed for CHR.
This means to define the abstract code instructions for CHR and to implement them.

Typ: Masterarbeit

Completion of non-confluent CHR programs

Non-confluent CHR programs, i.e. programs that can yield different results dependent on the order of the rules, can be completed such that they are confluent.

Within this work the student should familiarize herself with CHR and confluence. The completion algorithm should be implemented in a sound and reusable way.

Required knowledge: knowledge about Prolog and CHR. Lectures Constraint Programming and Rule-based Programming are advantageous.

Type: Masters thesis

Project: Collaborative CHR on the Web – SWISH

SWISH is a web-based application that provides easy access to SWI Prolog for the browser. It is used for teaching Prolog, e.g. in interactive tutorials like “Learn Prolog Now!”. The site is popular and can also be used to share example code and collaboration comparable to Google Docs.

Therefore, SWISH offers a web interface where users can interactively edit source code and execute it. The execution is handled by a server that receives both the source code and the query, executes it and sends the result back to the web interface.

Although Constraint Handling Rules (CHR) is a popular and important extension of SWI Prolog, its support in SWISH is limited. Current approaches to make CHR accessible in the web are either outdated (WebCHR) or use another host-language that Prolog (CHR.js). Therefore, this project aims at improving CHR support in SWISH to make it accessible at one of the most important online resources in the Prolog world.

Goals

The goal of this project is to extend the current SWISH implementation by a complete support
of CHR. The following sub-problems have to be
solved:

  • Making as many CHR examples executable as possible.
  • The sandbox handling of Prolog and its CHR implementation should be adapted such that all CHR programs can be compiled and executed by SWISH.
  • Tracer should be adapted to support CHR.

Prerequisites

  • Lecture „Rule-based Programming“/good knowledge of Prolog and CHR
  • Knowledge of JavaScript is helpful.
  • Willingness to understand the internals of the SWISH implementation and practical aspects of Prolog/CHR programming

Notice

Typ: Project