paperbot · PL 论文追踪

全部论文 待读 收藏

P2 Determination Problems for Orbit Closures and Matrix Groups

轨道闭包与矩阵群的判定问题
POPL 10(POPL)2026匹配度 3/10 · 论文属于代数矩阵群、轨道闭包判定与程序合成中循环不变式合成的理论工作,与用户关注的静态分析/AI×PL 交叉仅有非常间接的联系;不涉及 LLM/Agent、浮点程序分析或贝叶斯程序分析,因此匹配度低。引用 1 inbox
Rida Ait El Manssour, George Kenison, Mahsa Shirmohammadi, Anton Varonka, James Worrell
crossref: 2026-09-10

AI 速览

一句话:给出判定一个簇是否为 s-生成交换代数矩阵群作用下点轨道闭包的多项式空间算法。

矩阵群作用下点的轨道与轨道闭包出现在程序分析、复杂度理论、量子计算和自动机理论中。本文研究一类“判定问题”:给定代数簇,判断它是否以及如何作为代数矩阵群或某点轨道闭包出现;其中“如何”问该群能否由 s 个矩阵拓扑生成。主要结果是一个多项式空间过程,输入一个簇和数 s,判定该簇是否为某个点在 s-生成交换代数矩阵群作用下的轨道闭包。方法依赖交换代数矩阵群的结构性质与模论。该问题也关联于在指定程序变量不变量下合成循环;非交换代数矩阵群情形仍开放。

问题
研究给定代数簇能否作为代数矩阵群或某点轨道闭包出现,并在“如何”意义上判断对应群能否由 s 个矩阵拓扑生成。
方法
利用交换代数矩阵群的结构性质和模论,设计判定该表示问题的算法/过程。
评估
主要评估是理论性的:给出多项式空间算法,判定一个簇是否为 s-生成交换代数矩阵群作用下某点的轨道闭包;非交换情形未解决。
原文摘要(Abstract)

Computational problems concerning the orbit of a point under the action of a matrix group occur throughout computer science, including in program analysis, complexity theory, quantum computation, and automata theory. In many cases the focus extends beyond orbits proper to orbit closures under a suitable topology. Typically one starts from a group and a set of points and asks questions about the orbit closure of the set under the action of the group, e.g., whether two given orbit closures intersect. In this paper we consider a collection of what we call determination problems concerning matrix groups and orbit closures. These problems begin with a given variety and seek to understand whether and how it arises either as an algebraic matrix group or as an orbit closure. The how question asks whether the underlying group is s -generated, meaning it is topologically generated by s matrices for a given number s . Among other applications, problems of this type have recently been studied in the context of synthesising loops subject to certain specified invariants on program variables. Our main result is a polynomial-space procedure that inputs a variety and a number s and determines whether the given variety arises as an orbit closure of a point under an s -generated commutative algebraic matrix group. The main tools in our approach are structural properties of commutative algebraic matrix groups and module theory. We leave open the question of determining whether a variety is an orbit closure of a point under an s -generated algebraic matrix group (without the requirement of commutativity).

链接与引用

DOI 原文 · arXiv · PDF(开放获取) · DBLP

BibTeX
@article{abs-2407-04626,
  title = {Determination Problems for Orbit Closures and Matrix Groups},
  author = {Rida Ait El Manssour and George Kenison and Mahsa Shirmohammadi and Anton Varonka and James Worrell},
  journal = {Proceedings of the ACM on Programming Languages},
  volume = {10},
  number = {POPL},
  year = {2026},
  doi = {10.1145/3776698}
}