arXiv subjects

Sascha Rechenberger

Publications and source records attributed to Sascha Rechenberger.

4 recordsLinked to original sources

arXiv2025

Optimized Execution of FreeCHR

Constraint Handling Rules (CHR) is a rule-based programming language that rewrites collections of constraints. It is typically embedded into a general-purpose language. There exists a plethora of implementation for numerous host languages. However, the existing implementations often re-invent the method of embedding, which impedes maintenance and weakens assertions of correctness. To formalize and thereby standardize the embedding of a ground subset of CHR into arbitrary host languages, we introduced the framework FreeCHR and proved it to be a valid representation of classical CHR. For the sake of simplicity, abstract implementations of our framework did not yet include a concrete matching algorithm nor optimizations. In this paper, we introduce an improved execution and matching algorithm for FreeCHR. We also provide empirical evaluation of the algorithm.

cs.PL↗

arXiv2025

An instance of FreeCHR with refined operational semantics

Constraint Handling Rules (CHR) is a rule-based programming language which is typically embedded into a general-purpose language. There exists a plethora of implementations of CHR for numerous host languages. However, the existing implementations often reinvent the way to embed CHR, which impedes maintenance and weakens assertions of correctness. To formalize and thereby unify the embedding of CHR into arbitrary host languages, we introduced the framework FreeCHR and proved it to be a valid representation of classical CHR. Until now, this framework only includes a translation of the very abstract operational semantics of CHR which, due to its abstract nature, introduces several practical issues. In this paper, we introduce an execution algorithm for FreeCHR. We derive it from the refined operational semantics of CHR, which resolve the issues introduced by the very abstract semantics. We also prove soundness of the algorithm with respect to the very abstract semantics of FreeCHR. Hereby we provide a unified and an easy to implement guideline for new CHR implementations, as well as an algorithmic definition of the refined operational semantics.

cs.PL↗

arXiv2025

A Refined Operational Semantics for FreeCHR

Constraint Handling Rules (CHR) is a rule-based programming language which is typically embedded into a general-purpose language. There exists a plethora of implementations for numerous host languages. However, the existing implementations often re-invent the way to embed CHR, which impedes maintenance and weakens assertions of correctness. To formalize and thereby standardize the embedding into arbitrary host languages, we introduced the framework FreeCHR and proved it to be a valid representation of classical ground CHR. Until now, this framework only includes a translation of the very abstract operational semantics which, due to its abstract nature, is not a sufficient base for practical implementations. In this paper we present a translation of the refined operational semantics for FreeCHR and prove it to be both a valid concretization of the very abstract semantics of FreeCHR, and an equivalent representation of the refined semantics of CHR. This will establish implementations of FreeCHR as equivalent in behavior and expressiveness to existing implementations of CHR.

cs.PL↗

arXiv2023

FreeCHR: An Algebraic Framework for CHR-Embeddings

We introduce the framework FreeCHR which formalizes the embedding of Constraint Handling Rules (CHR) into a host language, using the concept of initial algebra semantics from category theory. We hereby establish a high-level implementation scheme for CHR as well as a common formalization for both theory and practice. We propose a lifting of the syntax of CHR via an endofunctor in the category Set and a lifting of the very abstract operational semantics of CHR into FreeCHR, using the free algebra, generated by the endofunctor. We give proofs for soundness and completeness w.r.t. its original definition. We also propose a first abstract execution algorithm and prove correctness w.r.t. the operational semantics. Finally, we show the practicability of our approach by giving two possible implementations of this algorithm in Haskell and Python. Under consideration in Theory and Practice of Logic Programming (TPLP).

cs.PL↗