A major challenge for transformers is generalizing to sequences longer than those observed during training. While previous works have empirically shown that transformers can either succeed or fail at length generalization depending on the task, theoretical understanding of this phenomenon remains limited. In this work, we introduce a rigorous theoretical framework to analyze length generalization in causal transformers with learnable absolute positional encodings. In particular, we characterize those functions that are identifiable in the limit from sufficiently long inputs with absolute positional encodings under an idealized inference scheme using a norm-based regularizer. This enables us to prove the possibility of length generalization for a rich family of problems. We experimentally validate the theory as a predictor of success and failure of length generalization across a range of algorithmic and formal language tasks. Our theory not only explains a broad set of empirical observations but also opens the way to provably predicting length generalization capabilities in transformers.

We investigate the feasibility of a topological method for proving separations of non-uniform circuit classes. Thereto, we chose a rather simple class of circuits: non-uniform constant size circuit classes with gate types underlying certain restrictions. In particular, we consider gate types admitting for a description through regular and commutative varieties of languages. Given a variety of regular languages V describing the gate types, we proceed by giving an alternative characterisation of the class of languages recognised by constant size circuits with the respective gates. This alternative description mainly relies on the block product principle (or substitution principle), which we extend to work with non-regular languages. The extended version of the block product principle is then used as the main tool to derive ultrafilter equations for the languages recognised by non-uniform constant size circuits with gates described by V, depending on the profinite equations that define the variety of regular languages V.

In earlier work (LICS 2016), the authors introduced two-variable first-order logic supplemented by a binary relation that allows one to say that a letter appears between two positions. We found an effective algebraic criterion that is a necessary condition for definability in this logic, and conjectured that the criterion is also sufficient, although we proved this only in the case of two-letter alphabets. Here we prove the general conjecture. The proof is quite different from the arguments in the earlier work, and required the development of novel techniques concerning factorizations of words. We extend the results to binary relations specifying that a factor appears between two positions.

It is an open problem whether definability in Propositional Dynamic Logic (PDL) on forests is decidable. Based on an algebraic characterization by Bojańczyk, et. al., (2012) in terms of forest algebras, Straubing (2013) described an approach to PDL based on a k-fold iterated distributive law. A proof that all languages satisfying such a k-fold iterated distributive law are in PDL would settle decidability of PDL. We solve this problem in the case k = 2: All languages recognized by forest algebras satisfying a 2-fold iterated distributive law are in PDL. Furthermore, we show that this class is decidable. This provides a novel nontrivial decidable subclass of PDL, and demonstrates the viability of the proposed approach to deciding PDL in general.

In this paper we relate two generalisations of the finite monoid recognisers of automata theory for the study of circuit complexity classes: Boolean spaces with internal monoids and typed monoids. Using the setting of stamps, this allows us to generalise a number of results from algebraic automata theory as it relates to Büchi's logic on words. We obtain an Eilenberg theorem, a substitution principle based on Stone duality, a block product principle for typed stamps and, as our main result, a topological semidirect product construction, which corresponds to the application of a general form of quantification. These results provide tools for the study of language classes given by logic fragments such as the Boolean circuit complexity classes.

Bounded context switching (BCS) is an under-approximate method for finding violations to safety properties in shared-memory concurrent programs. Technically, BCS is a reachability problem that is known to be NP-complete. Our contribution is a parameterized analysis of BCS. The first result is an algorithm that solves BCS when parameterized by the number of context switches (cs) and the size of the memory (m) in O*(m^(cs)2^(cs)). This is achieved by creating instances of the easier problem Shuff which we solve via fast subset convolution. We also present a lower bound for BCS of the form m^o(cs / log(cs)), based on the exponential time hypothesis. Interestingly, the gap is closely related to a conjecture that has been open since FOCS'07. Further, we prove that BCS admits no polynomial kernel. Next, we introduce a measure, called scheduling dimension, that captures the complexity of schedules. We study BCS parameterized by the scheduling dimension (sdim) and show that it can be solved in O*((2m)^(4sdim)4^t), where t is the number of threads. We consider variants of the problem for which we obtain (matching) upper and lower bounds.

In this work we consider the term evaluation problem which is, given a term over some algebra and a valid input to the term, computing the value of the term on that input. In contrast to previous methods we allow the algebra to be completely general and consider the problem of obtaining an efficient upper bound for this problem. Many variants of the problems where the algebra is well behaved have been studied. For example, the problem over the Boolean semiring or over the semiring (N,+,*). We extend this line of work. Our efficient term evaluation algorithm then serves as a tool for obtaining polylogarithmic depth upper bounds for various well-studied problems. To demonstrate the utility of our result we show new bounds and reprove known results for a large spectrum of problems. In particular, the applications of the algorithm we consider include (but are not restricted to) arithmetic formula evaluation, word problems for tree and visibly pushdown automata, and various problems related to bounded tree-width and clique-width graphs.

Cost register automata (CRAs) are one-way finite automata whose transitions have the side effect that a register is set to the result of applying a state-dependent semiring operation to a pair of registers. Here it is shown that CRAs over the tropical semiring (N U {infinity},\min,+) can simulate polynomial time computation, proving along the way that a naturally defined width-k circuit value problem over the tropical semiring is P-complete. Then the copyless variant of the CRA, requiring that semiring operations be applied to distinct registers, is shown no more powerful than NC^1 when the semiring is (Z,+,x) or (Gamma^*,max,concat). This relates questions left open in recent work on the complexity of CRA-computable functions to long-standing class separation conjectures in complexity theory, such as NC versus P and NC^1 versus GapNC^1.

We give an algebraic characterization, based on the bilateral semidirect product of finite monoids, of the quantifier alternation hierarchy in two-variable first-order logic on finite words. As a consequence, we obtain a new proof that this hierarchy is strict. Moreover, by application of the theory of finite categories, we are able to make our characterization effective: that is, there is an algorithm for determining the exact quantifier alternation depth for a given language definable in two-variable logic.

We study an extension of FO2[<], first-order logic interpreted in finite words, in which formulas are restricted to use only two variables. We adjoin to this language two-variable atomic formulas that say, 'the letter a appears between positions x and y'. This is, in a sense, the simplest property that is not expressible using only two variables.

Given a connected graph G and its vertex x, let U(G,x) denote the universal cover of G obtained by unfolding G into a tree starting from x. Let T=T(n) be the minimum number such that, for graphs G and H with at most n vertices each, the isomorphism of U(G,x) and U(H,y) surely follows from the isomorphism of these rooted trees truncated at depth T. Motivated by applications in theory of distributed computing, Norris [Discrete Appl. Math. 1995] asks if the value of T(n) is bounded by n. We answer this question in the negative by establishing that T(n)=(2-o(1))n. Our solution uses basic tools of finite model theory such as a bisimulation version of the Immerman-Lander 2-pebble counting game. The graphs G and H we construct for each n to prove the lower bound for T(n) also show some other tight lower bounds. Both having n vertices, G and H can be distinguished in 2-variable counting logic only with quantifier depth (1-o(1))n. It follows that color refinement, the classical procedure used in isomorphism testing and other areas for computing the coarsest equitable partition of a graph, needs (1-o(1))n rounds to achieve color stabilization on each of G and H. Somewhat surprisingly, this number of rounds is not enough for color stabilization on the disjoint union of G and H, where (2-o(1))n rounds are needed.

We examine visibly counter languages, which are languages recognized by visibly counter automata (a.k.a. input driven counter automata). We are able to effectively characterize the visibly counter languages in AC^0 and show that they are contained in FO[+].

The aim of this study is to understand the inherent expressive power of CTL operators. We investigate the complexity of model checking for all CTL fragments with one CTL operator and arbitrary Boolean operators. This gives us a fingerprint of each CTL operator. The comparison between the fingerprints yields a hierarchy of the operators that mirrors their strength with respect to model checking.

We introduce two variants of computation tree logic CTL based on team semantics: an asynchronous one and a synchronous one. For both variants we investigate the computational complexity of the satisfiability as well as the model checking problem. The satisfiability problem is shown to be EXPTIME-complete. Here it does not matter which of the two semantics are considered. For model checking we prove a PSPACE-completeess for the synchronous case, and show P-completeness for the asynchronous case. Furthermore we prove several interesting fundamental properties of both semantics.

Given two structures G and H distinguishable in FO k (first-order logic with k variables), let A k ( G , H ) denote the minimum alternation depth of a FO k formula distinguishing G from H . Let A k ( n ) be the maximum value of A k ( G , H ) over n -element structures. We prove the strictness of the quantifier alternation hierarchy of FO 2 in a strong quantitative form, namely A 2 ( n ) > n /8 − 2, which is tight up to a constant factor. For each k ⩾ 2, it holds that A k ( n ) > log k + 1 n − 2 even over colored trees, which is also tight up to a constant factor if k ⩾ 3. For k ⩾ 3, the last lower bound holds also over uncolored trees, whereas the alternation hierarchy of FO 2 collapses even over all uncolored graphs. We also show examples of colored graphs G and H on n vertices that can be distinguished in FO 2 much more succinctly if the alternation number is increased just by one: Whereas in Σ i it is possible to distinguish G from H with bounded quantifier depth, in Π i this requires quantifier depth Ω( n 2 ). The quadratic lower bound is best possible here because, if G and H can be distinguished in FO k with i quantifier alternations, this can be done with quantifier depth n 2 k − 2 + 1 and the same number of alternations.

Given two structures G and H distinguishable in FO^k (first-order logic with k variables), let A^k(G,H) denote the minimum alternation depth of a FO^k formula distinguishing G from H. Let A^k(n) be the maximum value of A^k(G,H) over n-element structures. We prove the strictness of the quantifier alternation hierarchy of FO^2 in a strong quantitative form, namely A^2(n) >= n/8-2, which is tight up to a constant factor. For each k >= 2, it holds that A^k(n) > log_(k+1) n-2 even over colored trees, which is also tight up to a constant factor if k >= 3. For k >= 3 the last lower bound holds also over uncolored trees, while the alternation hierarchy of FO^2 collapses even over all uncolored graphs. We also show examples of colored graphs G and H on n vertices that can be distinguished in FO^2 much more succinctly if the alternation number is increased just by one: while in Sigma_i it is possible to distinguish G from H with bounded quantifier depth, in Pi_i this requires quantifier depth Omega(n2). The quadratic lower bound is best possible here because, if G and H can be distinguished in FO^k with i quantifier alternations, this can be done with quantifier depth n^(2k-2).

We define DLOGTIME proof systems, DLTPS, which generalize NC0 proof systems. It is known that functions such as Exact_k and Majority do not have NC0 proof systems. Here, we give a DLTPS for Exact_k (and therefore for Majority) and also for other natural functions such as Reach and Cliquek. Though many interesting functions have DLTPS, we show that there are languages in NP which do not have DLTPS. We consider the closure properties of DLTPS and prove that they are closed under union and concatenation but are not closed under intersection and complement. Finally, we consider a hierarchy of polylogarithmic time proof systems and show that the hierarchy is strict.

We consider first-order logic with monoidal quantifiers over words. We show that all languages with a neutral letter, definable using the addition predicate are also definable with the order predicate as the only numerical predicate. Let S be a subset of monoids. Let L be the logic closed under quantification over the monoids in S. Then we prove that L[<;,+] and L[<;] define the same neutral letter languages. Our result can be interpreted as the Crane Beach conjecture to hold for the logic L[<;,+]. As a consequence we get the result of Roy and Straubing that FO+MOD[<;,+] collapses to FO+MOD[<;]. For cyclic groups, we answer an open question of Roy and Straubing, proving that MOD[<;,+] collapses to MOD[<;]. Our result also shows that multiplication as a numerical predicate is necessary for Barrington's theorem to hold and also to simulate majority quantifiers. All these results can be viewed as separation results for highly uniform circuit classes. For example we separate FO[<;,+]-uniform CC0 from FO[<;,+]-uniform ACC0.