Representations

Basic Information

• Paper ID: 2510.11419
• Title: Representations
• Author: Paul Brunet (EPISEN & LACL, Université Paris-Est Créteil Val de Marne)
• Classification: cs.LO (Logic in Computer Science)
• Publication Date: October 14, 2025 (arXiv version)
• Paper Link: https://arxiv.org/abs/2510.11419

Abstract

Formal analysis of automated systems is an important and continuously evolving field. This activity typically requires developing new verification frameworks to handle new programming features or new considerations (bugs of interest). One particularly frustrating aspect is establishing the completeness of logics relative to semantics. In this paper, the author attempts to facilitate such development, with particular focus on completeness. To this end, the author proposes a formal (meta)model of Software Analysis Systems (SAS), namely "Representations" of the same name. This model makes minimal assumptions about the modeled SAS, thereby capturing a large class of such systems. The paper then demonstrates how this approach is productive both for understanding the structure of existing completeness proofs and for leveraging this structure to construct new systems and prove their completeness.

Research Background and Motivation

Problem Description

As automated systems undertake increasingly diverse tasks, formal analysis problems are growing in both importance and diversity. While the field was dominated not long ago primarily by research on critical systems and their potential failures, we now see issues such as quality of service also being addressed through formal analysis.

Core Challenges

The correctness of Software Analysis Systems (SAS) depends on two properties:

1. Soundness: Any valid judgment in the logic is satisfied by the semantics
2. Completeness: Any semantically correct judgment can be established through the logic

Completeness is typically the difficult part of correctness proofs, because while soundness can be established by checking the soundness of individual logical rules, completeness requires the prover to produce derivations for every true semantic fact, and no universal method appears to apply.

Research Motivation

The author wishes to provide a modular meta-system foundation capable of generating sound and complete SAS in a transparent manner. Such a tool would allow formal analysis techniques to be applied to a broader category of systems and a broader category of questions about them.

Core Contributions

1. Proposes a formal model of Representations: A general framework for describing software analysis systems with minimal assumptions
2. Establishes categorical structure of representations: Defines homomorphisms between representations and proves the category of representations is Cartesian
3. Provides a general template for completeness proofs: Through the concept of "reductions," provides a deductive completeness template for establishing completeness
4. Develops higher-order representation theory: Through functors from the category of sets to the category of representations, characterizes parameterized representations
5. Demonstrates practical utility of the theory: Validates the approach through multiple instances of Kleene algebras and their extensions

Methodology Details

Definition of Representations

Definition 1 (Representation): A representation is a quadruple $R = \langle T, E, |=, \leq \rangle$, where:

• $T$ is a set of traces
• $E$ is a set of expressions
• $|=: T \rightharpoonup E$ is the satisfaction relation
• $\leq$ is a preorder on $E$ satisfying $|= ; \leq \subseteq |=$

A representation is called exact when $(|= \backslash |=) \subseteq \leq$.

Relational Algebra Formulation

Using relational algebra, soundness and completeness can be expressed as:

• Soundness: $|= ; \leq \subseteq |=$ (Axiom 1)
• Completeness: $|= \backslash |= \subseteq \leq$ (Axiom 2)

where $|= \backslash |=$ denotes the semantic inclusion relation.

Category of Representations

Definition 2 (Morphism): Given two representations $R_1$ and $R_2$, a morphism from the former to the latter is a pair $\langle \phi, \psi \rangle: R_1 \to R_2$ satisfying:

• $\phi: E_1 \to E_2$ is a function, $\psi: T_2 \rightharpoonup T_1$ is a relation
• $\phi$ preserves order: $\phi^*; \leq_1 \subseteq \leq_2; \phi^*$
• Interpretation compatibility: $|=_2; \phi^* = \psi; |=_1$

Proposition 1: If $R_1$ and $R_2$ are both exact, then their product is also exact.

Reduction Theory

Definition 3 (Reduction): A reduction from representation $R_1$ to $R_2$ is a triple $\langle \phi, \tau, \psi \rangle: R_1 \rightsquigarrow R_2$ satisfying:

• $\phi: E_1 \to E_2$ and $\tau: E_2 \to E_1$ are functions, $\psi: T_2 \rightharpoonup T_1$ is a relation
• $\tau$ preserves order: $\tau^*; \leq_2 \subseteq \leq_1; \tau^*$
• Interpretation compatibility: $|=_2; \phi^* = \psi; |=_1$
• Equivalence: $\tau^* ; \phi^* \subseteq \leq_1$ and $\phi^* ; \tau^* \subseteq \leq_1$

Proposition 2: $R_1$ is exact if and only if there exists an exact representation $R_2$ and a reduction $R_1 \rightsquigarrow R_2$.

Higher-Order Representations

Definition 9 (HOR): A higher-order representation is a structure $R = \langle \mathcal{T}, \mathcal{E}, ||=, \preceq \rangle$, where:

• $\mathcal{E}$ and $\mathcal{T}$ are endofunctors of the category of sets
• $||=: \mathcal{T} \rightharpoonup \mathcal{E}$ is a right-linear relation
• $\preceq: \mathcal{E} \rightharpoonup \mathcal{E}$ is a natural relation
• For each set $A$, $R_A = \langle \mathcal{T}A, \mathcal{E}A, ||=_A, \preceq_A \rangle$ is a representation

Experimental Setup

Application Instances

Kleene Algebra

Let $\text{Reg}(A)$ be the set of regular expressions over alphabet $A$. The free Kleene algebra yields an exact representation: $\text{KA}(A) := \langle A^*, \text{Reg}(A), |=_{\text{KA}}, \leq_{\text{KA}} \rangle$ where $w |=_{\text{KA}} e$ is defined as "$w$ belongs to the rational language associated with $e$."

Kleene Algebra with Tests (KAT)

In the completeness proof for KAT, the author transforms each term $p$ into a KAT-equivalent term $\hat{p}$ such that the set of guarded strings $G(\hat{p})$ equals the set of strings under regular expression interpretation $R(\hat{p})$. This constitutes a reduction from the KAT representation to the KA representation.

Synchronous Kleene Algebra (SKA)

The completeness proof for SKA proceeds in two steps:

1. Establish completeness for a subset of expressions
2. Prove that every expression can be translated to this sub-syntax while preserving provable equivalence

Each step is an instance of a reduction, and the entire proof can be understood as a single reduction.

Experimental Results

Theoretical Validation

The paper validates the effectiveness of the theoretical framework through multiple instances of Kleene algebra extensions:

1. KAT Reduction: $\langle \hat{}, \text{id}, 1 \rangle$ constitutes a reduction from KAT to KA
2. SKA Reduction: The composed reduction $\langle \hat{}, \text{id}, \Pi^* \rangle$ establishes completeness
3. CKA Reduction: Reduction is achieved through the syntactic closure function $\downarrow$

Equivalence of Syntactic Closure

Lemma 1: Under the conditions of Definition 4, if additionally $\leq_2 \subseteq \leq_1$, $|=_2 \subseteq |=_1$, and $R_2$ is exact, then for any function $\downarrow: E \to E$, the following are equivalent:

1. $\langle \downarrow, \text{id}, 1 \rangle$ is a reduction
2. $\downarrow$ is a syntactic closure

Application of Higher-Order Representations

The paper demonstrates how to extend relational HOR as functors:

• $\text{PreOrd} \to \text{Repr}$: Handles free monoids over preordered sets
• $\text{Repr} \to \text{Repr}$: Produces representations parameterized by other representations

Related Work

Institution Theory

Institutions also encapsulate syntactic and semantic information in a unified structure, but institutions contain multiple reasoning systems, whereas representations attempt to capture a single reasoning system. The definition of institutions is more restrictive than representations, requiring both syntax and semantics to have categorical structure.

Specification Theories

Specification theories introduced by Fahrenberg and Legay can be understood as structures $\langle T, E, \chi, \leq \rangle$, where $\chi: T \to E$ maps traces to their characteristic expressions. They can be converted to representations by setting $|= = \chi^*; \leq$, thus specification theories are special instances of representations.

Conclusions and Discussion

Main Conclusions

1. Representations provide a general and flexible framework for modeling software analysis systems
2. Reduction theory provides a structured approach to completeness proofs
3. Higher-order representations allow parameterized and modular system construction
4. The theory has been effectively validated in Kleene algebras and their extensions

Limitations

1. Meta-theory Choice: Currently based on Set and Rel categories, but more general abstractions may exist
2. Relational Algebra Fragment: Determining the "correct" fragment of relational algebra is needed
3. Practical Application: More concrete applications to verification tasks are needed to validate practical utility

Future Directions

1. Formal Verification: Formalize results in the Rocq proof system
2. Categorical Study: Identify useful categories of representations
3. Concrete Applications: Apply the theory to concrete verification tasks
4. Meta-theory Abstraction: Define abstract structures capturing exact requirements without additional assumptions

In-Depth Evaluation

Strengths

1. Theoretical Unification: Provides a unified framework for understanding different software analysis systems
2. Completeness Focus: Particularly addresses completeness—a difficult problem—providing a systematic solution
3. Modular Design: Achieves modular proofs and constructions through categorical methods
4. Rich Examples: Validates the theory's applicability through multiple Kleene algebra extensions
5. Mathematical Rigor: Provides strict mathematical foundations using relational algebra and category theory

Weaknesses

1. High Abstraction Level: The theoretical framework is quite abstract, potentially limiting intuitive understanding of practical applications
2. Limited Examples: Main instances concentrate on Kleene algebra; applicability in other domains remains to be verified
3. Lack of Implementation Details: Lacks discussion of concrete implementations or tool support
4. Performance Considerations: Does not address computational complexity implications of the proposed methods

Impact

1. Theoretical Contribution: Provides new theoretical tools for the formal methods community
2. Methodological Value: May influence the structure and methodology of future completeness proofs
3. Cross-domain Potential: The framework's generality enables potential application across multiple verification domains
4. Educational Value: Provides a unified perspective for understanding relationships between different verification systems

Applicable Scenarios

1. New Verification System Development: Provides theoretical guidance for developing new software analysis systems
2. Completeness Proofs: Offers structured methods for establishing completeness of logical systems
3. System Comparative Analysis: Provides unified foundations for comparing different verification frameworks
4. Theoretical Research: Furnishes new tools for theoretical research in formal methods

References

The paper cites 18 important references covering multiple related fields including relational algebra, category theory, Kleene algebras and their extensions, providing a solid foundation for theoretical development.