The Chase in Lean -- Crafting a Formal Library for Existential Rule Research

TL;DR

This paper introduces a formal Lean library for existential rules and the chase, aiming to improve correctness verification and unify termination conditions within a proof assistant framework.

Contribution

It presents a formalization of the chase in Lean, unifies various termination conditions, and extends support for constants in rules, enhancing theoretical and practical understanding.

Findings

The chase produces a universal model and can be a core without alternative matches.

Unified multiple chase termination conditions into a single framework.

Extended chase formalization to include constants in rules.

Abstract

The chase is a sound, complete, but possibly non-terminating algorithm for reasoning with existential rules (aka. tuple-generating dependencies), a highly expressive knowledge representation language. Although the procedure appears simple, research on theoretical properties and optimization for practical implementations has grown to a point where verifying correctness and reproducing proofs becomes challenging and intuition can sometimes be misleading. Lean is a purely functional programming language and interactive theorem prover whose community actively develops formal libraries for mathematics (Mathlib) and computer science (CSLib). In this work, we present our own endeavor of crafting a Lean framework around existential rules and the chase. We discuss design decisions concerning the nuances of chase definitions commonly found in the literature and show how these translate into Lean. To illustrate the framework's capabilities using known results, we show that the result of a chase is a universal model and outline the formalization for proving that without so-called "alternative matches" it is even a core. Beyond existing literature, we unify sufficient chase termination conditions in the likeness of Model-Faithful Acyclicity (MFA) into a common framework while also adding support for constants in rules.