有限支持结构中的有限上下文语义

中文摘要 AI 辅助

具有名称和数据的系统的语义通常依赖于有限多个特殊值。有限支持结构理论通过固定有限上下文下的置换不变性来处理这种依赖性。我们将这种方法发展到任意置换群和任意无限原子集上的语义。核心困难在于有限支持的谓词空间不一定是完备格。我们证明，对于取值于具有平凡原子作用的完备格中的谓词，每个单调有限支持变换器仍然具有最小和最大不动点。这些不动点位于由变换器上下文确定的完备格中，并且与在其稳定化子下等变的每个兼容单调环境扩展的不动点一致。支持转移界通过语义构造跟踪依赖性，而均匀有限性产生有限收敛性。对于布尔谓词，载体上的$m$个上下文稳定化子轨道足以在至多$m$次迭代后收敛，即使支持的谓词格是轨道无限的。我们将这些结果应用于自动机、操作语义和模态语义、抽象解释以及资源重写。有限关系签名中的超齐次原子结构产生有限单元表示，并通过授权监视器加以说明。所得到的理论区分了语义存在性、有限收敛性和有效计算。

英文摘要

Semantics for systems with names and data often depends on finitely many distinguished values. The theory of finitely supported structures treats this dependence through invariance under permutations fixing a finite context. We develop this approach to semantics over arbitrary permutation groups and arbitrary infinite sets of atoms. The central difficulty is that finitely supported predicate spaces need not be complete lattices. We prove that, for predicates valued in a complete lattice with trivial atom action, every monotone finitely supported transformer nevertheless has least and greatest fixed points. These lie in the complete lattice determined by the transformer's context and coincide with the fixed points of every compatible monotone ambient extension equivariant under its stabilizer. Support-transfer bounds track dependencies through semantic constructions, while uniform finiteness yields finite convergence. For Boolean predicates, $m$ context-stabilizer orbits on the carrier suffice for convergence after at most $m$ iterations, even when the supported predicate lattice is orbit-infinite. We apply these results to automata, operational and modal semantics, abstract interpretation, and resource rewriting. Ultrahomogeneous atom structures in finite relational signatures yield finite cell representations, illustrated by an authorization monitor. The resulting account separates semantic existence, finite convergence, and effective computation.

发表机构

• Romanian Academy, IIT（罗马尼亚科学院，信息技术研究所）

机构由 AI 辅助整理，请以论文原文为准。

补充信息

备注

31 pages, 1 table, no figures