Paper Info
Title
Decidability properties for fragments of chr
Abstract
We study the decidability of termination for two CHR dialects which, similarly to the Datalog like languages, are defined by using a signature which does not allow function symbols (of arity 0). Both languages allow the use of the = built-in in the body of rules, thus are built on a host language that supports unification. However each imposes one further restriction. The first CHR dialect allows only range-restricted rules, that is, it does not allow the use of variables in the body or in the guard of a rule if they do not appear in the head. We show that the existence of an infinite computation is decidable for this dialect. The second dialect instead limits the number of atoms in the head of rules to one. We prove that in this case, the existence of a terminating computation is decidable. These results show that both dialects are strictly less expressive1 than Turing Machines. It is worth noting that the language (without function symbols) without these restrictions is as expressive as Turing Machines.
Year
DOI
Venue
2010
10.1017/S1471068410000311
TPLP
Keywords
DocType
Volume
decidability property,range-restricted rule,constraint programming,well-structured transition systems.,expressivity,turing machines,chr dialect,function symbol,infinite computation,host language,turing machine
Journal
10
Issue
ISSN
Citations 
4-6
Theory and Practice of Logic Programming, volume 10, number 4-6, year 2010, pages 611-626
2
PageRank 
References 
Authors
0.39
15
4
Name
Order
Citations
PageRank
Maurizio Gabbrielli181965.35
Jacopo Mauro220926.74
Maria Chiara Meo331528.22
jon sneyers41179.47