Counting logics with a bounded number of variables form one of the central concepts in descriptive complexity theory. Although they restrict the number of variables that a formula can contain, the variables can be nested within scopes of quantified occurrences of themselves. In other words, the variables can be requantified. We study the fragments obtained from counting logics by restricting requantification for some but not necessarily all the variables. Similar to the logics without limitation on requantification, we develop tools to investigate the restricted variants. Specifically, we introduce a bijective pebble game in which certain pebbles can only be placed once and for all, and a corresponding two-parametric family of Weisfeiler-Leman algorithms. We show close correspondences between the three concepts. By using a suitable cops-and-robber game and adaptations of the Cai-F\"urer-Immerman construction, we completely clarify the relative expressive power of the new logics. We show that the restriction of requantification has beneficial algorithmic implications in terms of graph identification. Indeed, we argue that with regard to space complexity, non-requantifiable variables only incur an additive polynomial factor when testing for equivalence. In contrast, for all we know, requantifiable variables incur a multiplicative linear factor. Finally, we observe that graphs of bounded tree-depth and 3-connected planar graphs can be identified using no, respectively, only a very limited number of requantifiable variables.

翻译：变量数目有界的计数逻辑是描述复杂性理论的核心概念之一。尽管它们限制了公式所能包含的变量数量，但这些变量可以在其自身量化出现的作用域内嵌套。换言之，变量可以被重新量化。我们研究通过限制部分（而非全部）变量的重量化而获得的计数逻辑片段。与未限制重量化的逻辑类似，我们开发了研究这些受限变体的工具。具体而言，我们引入了一种双射卵石游戏，其中某些卵石只能被一次性永久放置，并提出了相应的双参数Weisfeiler-Leman算法族。我们证明了这三个概念之间存在紧密对应关系。通过使用合适的警察-强盗游戏以及对Cai-Fürer-Immerman构造的改编，我们完全阐明了新逻辑的相对表达能力。我们证明了重量化限制在图同构判定方面具有有益的算法意义。事实上，我们论证了在空间复杂度层面，当测试等价性时，不可重量化变量仅会产生多项式加性因子；而就我们所知，可重量化变量会产生线性乘性因子。最后，我们观察到有界树深图与3连通平面图可以分别在不使用可重量化变量、或仅使用极少量可重量化变量的情况下完成判定。