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 conditio
This work develops a rate-distortion-based approach to stochastic Chase decoding of algebraic codes over binary memoryless symmetric (BMS) channels, replacing the heuristics traditionally used to determine flip probabilities with information-theoretically grounded flipping rules. In particular, we reinterpret stochastic Chase decoding as a random-coding construction for error-pattern covering codes. Our approach builds on the framework of Nguyen et al., who introduced a rate-distortion formulation of multiple-attempt decoding for Reed-Solomon codes over nonbinary channels. In their formulation, erasure patterns are generated so as to align with, and thereby mask, hard-decision errors. We adapt this framework to the design of bit-flip probabilities for Chase decoding over BMS channels. This yields an explicit characterization of the asymptotically optimal bit-flipping rule, together with the expected list size required to ensure that the transmitted codeword appears in the decoding list with high probability. Moreover, for binary and quaternary symmetric channels, we demonstrate that the optimal bit-flipping rule, determined by exhaustive search, closely matches the information-theo
We formulate and verify a non-Archimedean analogue of Chase's lemma. Following the framework by K.\ Eda removing restriction of cardinality from analogy on direct product between countability and non-$ω_1$-measurability, we extend the non-Archimedean analogue of Chase's lemma to a non-Archimedean counterpart of the extension by K.\ Eda of the extension by M.\ Dugas and B.\ Zimmermann-Huisgen of Chase's lemma.
The chase is a fundamental algorithm with ubiquitous uses in database theory. Given a database and a set of existential rules (aka tuple-generating dependencies), it iteratively extends the database to ensure that the rules are satisfied in a most general way. This process may not terminate, and a major problem is to decide whether it does. This problem has been studied for a large number of chase variants, which differ by the conditions under which a rule is applied to extend the database. Surprisingly, the complexity of the universal termination of the restricted (aka standard) chase is not fully understood. We close this gap by placing universal restricted chase termination in the analytical hierarchy. This higher hardness is due to the fairness condition, and we propose an alternative condition to reduce the hardness of universal termination.
We propose a low-complexity Chase decoder for optical interconnects that formulates test pattern selection as a generalized maximum coverage problem. For concatenated RS-BCH and oFEC codes, our decoder achieves the standard Chase decoding performance with 25% and 61.3% fewer test patterns, respectively.
Chebyshev filtered subspace iteration is a well-known algorithm for the solution of (symmetric/Hermitian) algebraic eigenproblems which has been implemented in several application codes~\cite{Kronik:2006ff, abinit:2020} or in stand alone libraries~\cite{ChASE}. An essential part of the algorithm is the QR-factorization of the array of vectors spanning the active subspace that have been filtered by the Chebyshev filter. Typically such an array has an a-priori unknown high condition number that directly influences the choice of QR-factorization algorithm. In this work we show how such condition number can be bound from above with precise and inexpensive estimates. We then proceed to use these estimates to implement a mechanism for the choice of QR-factorization in the ChASE library. We show how such mechanism enhance the performance of the library without compromising on its accuracy.
The chase is a ubiquitous algorithm in database theory. However, for existential rules (aka tuple-generating dependencies), its termination is not guaranteed, and even undecidable in general. The problem of termination becomes particularly difficult for the restricted (or standard) chase, for which the order of rule application matters. Thus, decidability of restricted chase termination is still open for many well-behaved classes such as linear or guarded multi-headed rules. We make a step forward by showing that all-instances restricted chase termination is decidable in the linear multi-headed case.
The chase is a widely implemented approach to reason with tuple-generating dependencies (tgds), used in data exchange, data integration, and ontology-based query answering. However, it is merely a semi-decision procedure, which may fail to terminate. Many decidable conditions have been proposed for tgds to ensure chase termination, typically by forbidding some kind of "cycle" in the chase process. We propose a new criterion that explicitly allows some such cycles, and yet ensures termination of the standard chase under reasonable conditions. This leads to new decidable fragments of tgds that are not only syntactically more general but also strictly more expressive than the fragments defined by prior acyclicity conditions. Indeed, while known terminating fragments are restricted to PTime data complexity, our conditions yield decidable languages for any k-ExpTime. We further refine our syntactic conditions to obtain fragments of tgds for which an optimised chase procedure decides query entailment in PSpace or k-ExpSpace, respectively.
Standard selective prediction methods typically estimate uncertainty from the output of a single predictive branch. While effective for general uncertainty estimation, these approaches often struggle under partial observability, where local temporal evidence can be contradictory and standard confidence scores become misleading. We introduce CHASE (Competing Hypotheses for Ambiguity-Aware Selective Prediction), a selective prediction framework that explicitly compares structured temporal explanations to determine whether to commit to a decision or abstain. Because genuine ambiguity causes the score gap between competing hypotheses to collapse, CHASE optimizes a ranking-aware selector over these hypothesis margins to globally separate safe commitments from fundamentally uncertain ones. We evaluate this framework on the problem of hidden connectivity inference, utilizing a controlled, physically grounded simulator inspired by the dynamics of giant unilamellar vesicles (GUVs), alongside zero-shot qualitative transfer (without retraining or fine tuning) to representative real GUV videos. Our experiments demonstrate that explicitly reasoning over competing hypotheses provides a superior
The chase procedure, originally introduced for checking implication of database constraints, and later on used for computing data exchange solutions, has recently become a central algorithmic tool in rule-based ontological reasoning. In this context, a key problem is non-uniform chase termination: does the chase of a database w.r.t. a rule-based ontology terminate? And if this is the case, what is the size of the result of the chase? We focus on guarded tuple-generating dependencies (TGDs), which form a robust rule-based ontology language, and study the above central questions for the semi-oblivious version of the chase. One of our main findings is that non-uniform semi-oblivious chase termination for guarded TGDs is feasible in polynomial time w.r.t. the database, and the size of the result of the chase (whenever is finite) is linear w.r.t. the database. Towards our results concerning non-uniform chase termination, we show that basic techniques such as simplification and linearization, originally introduced in the context of ontological query answering, can be safely applied to the chase termination problem.
Iterative decoding is essential in modern communication systems, especially optical communications, where error-correcting codes such as turbo product codes (TPC) and staircase codes are widely employed. A key factor in achieving high error correction performance is the use of soft-decision decoding for component codes. However, implementing optimal maximum a posteriori (MAP) probability decoding for commonly used component codes, such as BCH and Polar codes, is computationally prohibitive. Instead, practical systems rely on approximations, with the Chase-Pyndiah algorithm being a widely used suboptimal method. TPC are more powerful than their component codes and begin to function effectively at low signal-to-noise ratios. Consequently, during the initial iterations, the component codes do not perform well and introduce errors in the extrinsic information updates. This phenomenon limits the performance of TPC. This paper proposes a neural network-aided rollback Chase-Pyndiah decoding method to address this issue. A transformer-based neural network identifies cases where extrinsic updates are likely to introduce errors, triggering a rollback mechanism which prevents the update and k
Querying both structured and unstructured data has become a new paradigm in data analytics and recommendation. With unstructured data, such as text and videos, are converted to high-dimensional vectors and queried with approximate nearest neighbor search (ANNS). State-of-the-art database systems implement vector search as a plugin in the relational query engine, which tries to utilize the ANN index to enhance performance. After investigating a broad range of hybrid queries, we find that such designs may miss potential optimization opportunities and achieve suboptimal performance for certain queries. In this paper, we propose CHASE, a query engine that is natively designed to support efficient hybrid queries on structured and unstructured data. CHASE performs specific designs and optimizations on multiple stages in query processing. First, semantic analysis is performed to categorize queries and optimize query plans dynamically. Second, new physical operators are implemented to avoid redundant computations, which is the case with existing operators. Third, compilation-based techniques are adopted for efficient machine code generation. Extensive evaluations using real-world datasets
The chase procedure is a fundamental algorithmic tool in databases that allows us to reason with constraints, such as existential rules, with a plethora of applications. It takes as input a database and a set of constraints, and iteratively completes the database as dictated by the constraints. A key challenge, though, is the fact that it may not terminate, which leads to the problem of checking whether it terminates given a database and a set of constraints. In this work, we focus on the semi-oblivious version of the chase, which is well-suited for practical implementations, and linear existential rules, a central class of constraints with several applications. In this setting, there is a mature body of theoretical work that provides syntactic characterizations of when the chase terminates, algorithms for checking chase termination, precise complexity results, and worst-case optimal bounds on the size of the result of the chase (whenever is finite). Our main objective is to experimentally evaluate the existing chase termination algorithms with the aim of understanding which input parameters affect their performance, clarifying whether they can be used in practice, and revealing th
In recent years, the widespread adoption of distributed microservice architectures within the industry has significantly increased the demand for enhanced system availability and robustness. Due to the complex service invocation paths and dependencies in enterprise-level microservice systems, it is challenging to locate the anomalies promptly during service invocations, thus causing intractable issues for normal system operations and maintenance. In this paper, we propose a Causal Heterogeneous grAph baSed framEwork for root cause analysis, namely CHASE, for microservice systems with multimodal data, including traces, logs, and system monitoring metrics. Specifically, related information is encoded into representative embeddings and further modeled by a multimodal invocation graph. Following that, anomaly detection is performed on each instance node with attentive heterogeneous message passing from its adjacent metric and log nodes. Finally, CHASE learns from the constructed hypergraph with hyperedges representing the flow of causality and performs root cause localization. We evaluate the proposed framework on two public microservice datasets with distinct attributes and compare wi
In this paper we take closer look at recent developments for the chase procedure, and provide additional results. Our analysis allows us create a taxonomy of the chase variations and the properties they satisfy. Two of the most central problems regarding the chase is termination, and discovery of restricted classes of sets of dependencies that guarantee termination of the chase. The search for the restricted classes has been motivated by a fairly recent result that shows that it is undecidable to determine whether the chase with a given dependency set will terminate on a given instance. There is a small dissonance here, since the quest has been for classes of sets of dependencies guaranteeing termination of the chase on all instances, even though the latter problem was not known to be undecidable. We resolve the dissonance in this paper by showing that determining whether the chase with a given set of dependencies terminates on all instances is coRE-complete. For the hardness proof we use a reduction from word rewriting systems, thereby also showing the close connection between the chase and word rewriting. The same reduction also gives us the aforementioned instance-dependent RE-c
Skeleton-based multi-entity action recognition is a challenging task aiming to identify interactive actions or group activities involving multiple diverse entities. Existing models for individuals often fall short in this task due to the inherent distribution discrepancies among entity skeletons, leading to suboptimal backbone optimization. To this end, we introduce a Convex Hull Adaptive Shift based multi-Entity action recognition method (CHASE), which mitigates inter-entity distribution gaps and unbiases subsequent backbones. Specifically, CHASE comprises a learnable parameterized network and an auxiliary objective. The parameterized network achieves plausible, sample-adaptive repositioning of skeleton sequences through two key components. First, the Implicit Convex Hull Constrained Adaptive Shift ensures that the new origin of the coordinate system is within the skeleton convex hull. Second, the Coefficient Learning Block provides a lightweight parameterization of the mapping from skeleton sequences to their specific coefficients in convex combinations. Moreover, to guide the optimization of this network for discrepancy minimization, we propose the Mini-batch Pair-wise Maximum M
As supercomputers become larger with powerful Graphics Processing Unit (GPU), traditional direct eigensolvers struggle to keep up with the hardware evolution and scale efficiently due to communication and synchronization demands. Conversely, subspace eigensolvers, like the Chebyshev Accelerated Subspace Eigensolver (ChASE), have a simpler structure and can overcome communication and synchronization bottlenecks. ChASE is a modern subspace eigensolver that uses Chebyshev polynomials to accelerate the computation of extremal eigenpairs of dense Hermitian eigenproblems. In this work we show how we have modified ChASE by rethinking its memory layout, introducing a novel parallelization scheme, switching to a more performing communication-avoiding algorithm for one of its inner modules, and substituting the MPI library by the vendor-optimized NCCL library. The resulting library can tackle dense problems with size up to $N=\mathcal{O}(10^6)$, and scales effortlessly up to the full 900 nodes -- each one powered by 4$\times$A100 NVIDIA GPUs -- of the JUWELS Booster hosted at the Jülich Supercomputing Centre.
Chase algorithms are indispensable in the domain of knowledge base querying, which enable the extraction of implicit knowledge from a given database via applications of rules from a given ontology. Such algorithms have proved beneficial in identifying logical languages which admit decidable query entailment. Within the discipline of proof theory, sequent calculi have been used to write and design proof-search algorithms to identify decidable classes of logics. In this paper, we show that the chase mechanism in the context of existential rules is in essence the same as proof-search in an extension of Gentzen's sequent calculus for first-order logic. Moreover, we show that proof-search generates universal models of knowledge bases, a feature also exhibited by the chase. Thus, we formally connect a central tool for establishing decidability proof-theoretically with a central decidability tool in the context of knowledge representation.
The chase procedure for existential rules is an indispensable tool for several database applications, where its termination guarantees the decidability of these tasks. Most previous studies have focused on the skolem chase variant and its termination analysis. It is known that the restricted chase variant is a more powerful tool in termination analysis provided a database is given. But all-instance termination presents a challenge since the critical database and similar techniques do not work. In this paper, we develop a novel technique to characterize the activeness of all possible cycles of a certain length for the restricted chase, which leads to the formulation of a parameterized class of the finite restricted chase, called $k$-$\mathsf{safe}(Φ)$. This approach applies to any class of finite skolem chase identified with a condition of acyclicity. More generally, we show that the approach can be applied to the hierarchy of bounded rule sets previously only defined for the skolem chase. Experiments on a collection of ontologies from the web show the applicability of the proposed methods on real-world ontologies. Under consideration in Theory and Practice of Logic Programming (TPL
The Chinese Hα Solar Explorer (CHASE), dubbed "Xihe" - Goddess of the Sun, was launched on October 14, 2021 as the first solar space mission of China National Space Administration (CNSA). The CHASE mission is designed to test a newly developed satellite platform and to acquire the spectroscopic observations in the Hα waveband. The Hα Imaging Spectrograph (HIS) is the scientific payload of the CHASE satellite. It consists of two observational modes: raster scanning mode and continuum imaging mode. The raster scanning mode obtains full-Sun or region-of-interest spectral images from 6559.7 to 6565.9 Å and from 6567.8 to 6570.6 Å with 0.024 Å pixel spectral resolution and 1 minute temporal resolution. The continuum imaging mode obtains photospheric images in continuum around 6689 Å with the full width at half maximum of 13.4 Å. The CHASE mission will advance our understanding of the dynamics of solar activity in the photosphere and chromosphere. In this paper, we present an overview of the CHASE mission including the scientific objectives, HIS instrument overview, data calibration flow, and first results of on-orbit observations.