Papers for

compiler designers

Papers whose findings have a practical use for this group, as judged from the abstract. Open a paper to read what it means in practice.

Formalizing the omega test to check systems of inequalities accurately

Formalizing the Omega Test in Dafny

Abstract: We present a formalization in Dafny of the Omega Test, an algorithm used to decide the satisfiability of a system of inequalities. The implementation defines executable representations for rational numbers, linear expressions, inequalities, equalities, divisibility constraints, and systems of constraints, together with their semantic interpretation through valuations. We fully specify and verify the implementation in Dafny. We describe the lessons learned and how the formalization process led to new insights into the algorithm.

Mon 28 SeptLogic in Computer ScienceProgramming LanguagesSymbolic Computation
The gist
Some computer problems involve figuring out if sets of inequalities can all be true at the same time. The authors describe how they wrote and verified a computer program in Dafny that carefully implements the omega test algorithm to do this checking precisely. They also explain what they learned about the algorithm by formalizing it, making the process more reliable and understandable.
Open → 2609.34882v1

Regular languages with fixed circuit size have exact logical and algebraic descriptions

Rational Reductions and Regular Languages of Constant Circuit Complexity

Abstract: We study the circuit complexity of regular languages in terms of unbounded fan-in Boolean circuit families. We characterize the regular languages of constant circuit complexity in terms of the one-variable fragment of first-order logic with regular predicates, in terms of the pseudovariety of stamps $\mathbf{QEJ}_\mathbf{1}$, suitable word congruences and regular expressions. We analogously characterize the neutral letter regular languages of constant circuit complexity. Our lower bound result implies that the class of regular languages of sublogarithmic circuit complexity coincides with the one of constant circuit complexity. In addition we show that deciding whether a regular language, given as a nondeterministic finite automaton, has constant circuit complexity is $\mathbf{PSPACE}$-complete. We introduce a strong notion of reduction, called rational truth-table reduction, that is tailored towards algebraically defined classes of languages. We show that, for a class of functions we call mild, rational truth-table reductions preserve both upper and lower bounds on circuit complexity. We show that the class of regular languages, whose circuit complexity is bounded by a mild function, is in fact a length-multiplying variety of languages. Slightly extending the class of regular languages of constant circuit complexity, we analogously characterize the class of regular languages that are in the pseudovariety $\mathbf{QEACom}$. For these we derive logarithmic circuit complexity upper bounds.

Wed 16 SeptComputational ComplexityFormal Languages and Automata TheoryLogic in Computer Science
The gist
The authors studied simple computer circuits that decide whether words belong to certain regular languages, which are patterns recognizable by small machines. They found precise logical rules and algebraic structures that exactly describe which languages can be recognized by circuits of constant size. They also showed how hard it is to tell if a given pattern can be recognized with such small circuits and introduced a new way to compare languages that preserves these complexity bounds. This work clarifies the boundaries between very efficient and slightly more complex recognition of regular languages.
Open → 2609.18484v1

Complexity limits of simple semi conditional grammars revealed

Non-Terminal Complexity of Simple Semi-Conditional Grammars

Abstract: We study the complexity of simple semi-conditional grammars (SSCGs) in terms of the number of their terminals and non-terminals. We show that SSCGs with three non-terminals can generate all RE languages; two non-terminals suffice for linear languages; and one suffices for unary regular languages. We also determine both upper bounds and fundamental limitations of SSCGs: while certain one-non-terminal SSCGs can generate non-context-free languages, every language generated by a one-non-terminal SSCG is in non-deterministic linear space. We also prove that there exists a regular language of alphabet size at least 3 which cannot be generated by any one-non-terminal SSCG. Finally, we prove that membership testing for SSCGs of two non-terminals is already NP-hard.

Sat 12 SeptFormal Languages and Automata Theory
The gist
This paper looks at a special kind of grammar called simple semi-conditional grammars (SSCGs), which are rules that describe how languages form. The authors find out how many building blocks (called non-terminals) these grammars need to create different types of languages, from very simple to very complicated ones. They also show that some SSCGs with only one non-terminal can still make languages that are tricky to recognize, but there are limits to this power. Finally, the paper finds that checking whether a word belongs to a language described by an SSCG with two non-terminals is already a tough problem for computers.
Open → 2609.14181v1