Logical Algorithms meets CHR: A meta-complexity result for Constraint Handling Rules with rule priorities

TL;DR

This paper establishes a connection between Logical Algorithms and Constraint Handling Rules with rule priorities, providing a translation schema and a new implementation that ensures strong complexity guarantees and extends meta-complexity results.

Contribution

It introduces a translation from Logical Algorithms to CHR with rule priorities and proposes an implementation that guarantees complexity bounds, extending meta-complexity theorems to CHR-rp.

Findings

A translation schema from LA to CHR-rp is developed.

A new CHR-rp implementation achieves strong complexity guarantees.

Meta-complexity results for LA are extended to CHR-rp.

Abstract

This paper investigates the relationship between the Logical Algorithms language (LA) of Ganzinger and McAllester and Constraint Handling Rules (CHR). We present a translation schema from LA to CHR-rp: CHR with rule priorities, and show that the meta-complexity theorem for LA can be applied to a subset of CHR-rp via inverse translation. Inspired by the high-level implementation proposal for Logical Algorithm by Ganzinger and McAllester and based on a new scheduling algorithm, we propose an alternative implementation for CHR-rp that gives strong complexity guarantees and results in a new and accurate meta-complexity theorem for CHR-rp. It is furthermore shown that the translation from Logical Algorithms to CHR-rp combined with the new CHR-rp implementation, satisfies the required complexity for the Logical Algorithms meta-complexity result to hold.