Expressiveness of multiple heads in CHR

Constraint Handling Rules (CHR) are a committed-choice declarative language which has been designed for writing constraint solvers. A CHR program consists of multi-headed guarded rules which allow one to rewrite constraints into simpler ones until a solved form is reached. Many examples in the vast literature on the subject show that multiple heads are important in order to write programs which solve specific problems. On the other hand, the presence of multiples heads complicates considerably the semantics. Therefore, since restricting to single head rules does not affect the Turing completeness of the language, one can legitimately ask whether multiple heads do indeed augment the expressive power of the language. In this paper we answer positively to this question by showing that, under certain reasonable assumptions, it is not possible to encode the CHR language (with multi-headed rules) into a single head language while preserving the intended meaning of programs.