Informatik-Fachvortrag Confluence Modulo

Fakultät für Ingenieurwissenschaften, Informatik und Psychologie
Informatik-Fachvortrag
Mittwoch, den 23. November 2016, 10:00 Uhr
Universität Ulm, Oberer Eselsberg
Gebäude O27, Raum 411
Herr Prof. Dr. Henning Christiansen und Frau Maja H. Kirkeby
Roskilde University, Denmark
sprechen zum Thema
Confluence Modulo Equivalence for Constraint
Handling Rules
Confluence is an important and desirable property for CHR and other systems with
an inherent nondeterminism. A CHR program being confluent means that the final
result of a computation is independent of the choice and order of the rules applied.
In the present work, we generalize previous results to cover confluence modulo
equivalence: alternative final states need not be identical, but only equivalent with
respect to a programmer-defined equivalence relation. This is a desired extension as
it makes a larger class of CHR programs enjoy the advantages of confluence. This
applies for programs with redundant data representation (e.g., with sets-as-lists), and
for dynamic programming algorithms with pruning (e.g., Viterbi: we need just one
optimal solutions among perhaps several equally good ones). As opposed to
previous work, we handle also CHR programs with extralogical and "problematic"
built-ins such as Prolog's var/1, nonvar/1 and 'is'/2 predicates, by the introduction of
a new operational semantics.
We are currently developing methods for proving confluence modulo given a
equivalence for CHR programs, in automatic or semi-automatic ways.
Es laden ein die Dozenten der Fakultät für Ingenieurwissenschaften,
Informatik und Psychologie.
Ulm, den 15.11.2016
gez. Prof. Dr. T. Frühwirth

Download Report