2025-11-21T20:52:15.308162

Representations

Brunet

The formal analysis of automated systems is an important and growing industry. This activity routinely requires new verification frameworks to be developed to tackle new programming features, or new considerations (bugs of interest). Often, one particular property can prove frustrating to establish: completeness of the logic with respect to the semantics. In this paper, we try and make such developments easier, with a particular attention on completeness. Towards that aim, we propose a formal (meta-)model of software analysis systems (SAS), the eponymous Representations. This model requires few assumptions on the SAS being modelled, and as such is able to capture a large class of such systems. We then show how our approach can be fruitful, both to understand how existing completeness proofs can be structured, and to leverage this structure to build new systems and prove their completeness.

academic

Representations

基本信息

论文ID: 2510.11419
标题: Representations
作者: Paul Brunet (EPISEN & LACL, Université Paris-Est Créteil Val de Marne)
分类: cs.LO (Logic in Computer Science)
发表时间: 2025年10月14日 (arXiv版本)
论文链接: https://arxiv.org/abs/2510.11419

摘要

自动化系统的形式化分析是一个重要且不断发展的行业。这项活动通常需要开发新的验证框架来处理新的编程特性或新的考虑因素（感兴趣的错误）。其中一个特别令人沮丧的性质是建立逻辑相对于语义的完备性。在本文中，作者试图让这样的开发变得更容易，特别关注完备性。为此，作者提出了软件分析系统（SAS）的形式化（元）模型，即同名的"表示"（Representations）。该模型对被建模的SAS要求很少的假设，因此能够捕获大类此类系统。然后展示了该方法如何富有成效，既可以理解现有完备性证明的结构，也可以利用这种结构构建新系统并证明其完备性。

研究背景与动机

问题描述

随着自动化系统承担越来越多样化的任务，形式化分析问题在重要性和多样性方面都在增长。当该领域在不久前还主要由关键系统及其潜在故障的研究主导时，现在我们看到诸如服务质量等问题也通过形式化分析来解决。

核心挑战

软件分析系统（SAS）的正确性依赖于两个性质：

可靠性（Soundness）：逻辑中任何有效判断都被语义满足
完备性（Completeness）：任何语义上正确的判断都可以通过逻辑建立

完备性通常是正确性证明中的困难部分，因为虽然可靠性可以通过检查逻辑各个规则的可靠性来建立，但完备性要求证明者为每个真实的语义事实产生推导，而没有通用方法似乎适用。

研究动机

作者希望提供一个模块化的元系统基础，能够以透明的方式生成可靠且完备的SAS。这样的工具将允许形式化分析技术应用于更广泛的系统类别和关于它们的问题类别。

核心贡献

提出了表示（Representations）的形式化模型：一个通用的框架来描述软件分析系统，要求很少的假设
建立了表示的范畴论结构：定义了表示之间的同态，证明了表示范畴是笛卡尔的
提供了完备性证明的通用模板：通过"归约"（reductions）的概念，给出了建立完备性的演绎完备模板
开发了高阶表示理论：通过函子从集合范畴到表示范畴，刻画了参数化表示
展示了理论的实用性：通过Kleene代数及其扩展的多个实例，验证了方法的有效性

方法详解

表示的定义

定义1（表示）：一个表示是一个四元组 $R = \langle T, E, |=, \leq \rangle$ ，其中：

$T$ 是迹（traces）的集合
$E$ 是表达式的集合
$|=: T \rightharpoonup E$ 是满足关系
$\leq$ 是 $E$ 上的预序，满足 $|= ; \leq \subseteq |=$

当满足 $(|= \backslash |=) \subseteq \leq$ 时，称该表示是精确的。

关系代数表述

使用关系代数，可靠性和完备性可以表述为：

可靠性： $|= ; \leq \subseteq |=$ （公理1）
完备性： $|= \backslash |= \subseteq \leq$ （公理2）

其中 $|= \backslash |=$ 表示语义包含关系。

表示的范畴

定义2（态射）：给定两个表示 $R_1$ 和 $R_2$ ，从前者到后者的态射是一对 $\langle \phi, \psi \rangle: R_1 \to R_2$ ，满足：

$\phi: E_1 \to E_2$ 是函数， $\psi: T_2 \rightharpoonup T_1$ 是关系
$\phi$ 保序： $\phi^*; \leq_1 \subseteq \leq_2; \phi^*$
解释兼容： $|=_2; \phi^* = \psi; |=_1$

命题1：如果 $R_1$ 和 $R_2$ 都是精确的，那么它们的乘积也是精确的。

归约理论

定义3（归约）：从表示 $R_1$ 到 $R_2$ 的归约是三元组 $\langle \phi, \tau, \psi \rangle: R_1 \rightsquigarrow R_2$ ，满足：

$\phi: E_1 \to E_2$ 和 $\tau: E_2 \to E_1$ 是函数， $\psi: T_2 \rightharpoonup T_1$ 是关系
$\tau$ 保序： $\tau^*; \leq_2 \subseteq \leq_1; \tau^*$
解释兼容： $|=_2; \phi^* = \psi; |=_1$
等价性： $\tau^* ; \phi^* \subseteq \leq_1$ 且 $\phi^* ; \tau^* \subseteq \leq_1$

命题2： $R_1$ 是精确的当且仅当存在精确表示 $R_2$ 和归约 $R_1 \rightsquigarrow R_2$ 。

高阶表示

定义9（HOR）：高阶表示是结构 $R = \langle \mathcal{T}, \mathcal{E}, ||=, \preceq \rangle$ ，其中：

$\mathcal{E}$ 和 $\mathcal{T}$ 是集合范畴的内函子
$||=: \mathcal{T} \rightharpoonup \mathcal{E}$ 是右线性关系
$\preceq: \mathcal{E} \rightharpoonup \mathcal{E}$ 是自然关系
对每个集合 $A$ ， $R_A = \langle \mathcal{T}A, \mathcal{E}A, ||=_A, \preceq_A \rangle$ 是表示