Trends in Arithmetic Theories

About

Logical theories of arithmetic such as Presburger arithmetic play an important role in a variety of different areas of computer science and have been studied since the early days of the field. The recent years have seen a lot of progress on all aspects of such theories, ranging from new foundational results, algorithmic advances, more performant decision procedures to novel application domains. This progress has largely been obtained independently without much interaction between researchers working on different aspects of this field. The goal of this workshop is to bring together researchers working in the field to exchange latest trends, understand currently existing challenges and to initiate new collaborations.

Everyone interested in arithmetic theories is invited to attend. The workshop is planned to be a hybrid workshop: we are optimistic that we will be able to livestream talks and plan to make them available online after the event has taken place.

We also plan to hold a short-presentation session, more details to follow.

Invited speakers

• Émilie Charlier, Université de Liège, Belgium
  An introduction to numeration systems : Cobham-like theorems, first-order logic and regular sequences (Slides)
  In this talk, I will present an introduction to numeration systems (mostly for representing integers), and show how first-order logic can be used in order to solve problems in combinatorics on words. The base idea is to translate properties of numbers into combinatorial properties of their representations. As far as I can, I will try to determine which results depends on the numeration systems involved and which do not. On the one hand, Cobham’s theorem and its generalizations tell us that most properties of numbers strongly depend on the chosen numeration system. On the other hand, the use of very general numeration systems, such as abstract numeration systems, allows us to understand how far we can exploit techniques from logic and automata theory. Along the way, we will define the notions of recognizable and definable sets of integers, automatic and regular sequences, morphic sequences and abstract numeration systems. If time allows me to do so, I will also present results generalizing these considerations to real numbers.
• Philipp Hieronymi, University of Bonn, Germany
  A strong version of Cobham’s theorem (and other thoughts on decidability in expansions of Presburger) (Slides)
  Let k,l>1 be two multiplicatively independent integers. A subset X of Nn is k-recognizable if the set of k-ary representations of X is recognized by some finite automaton. Cobham’s famous theorem states that a subset of the natural numbers is both k-recognizable and l-recognizable if and only if it is Presburger-definable (or equivalently: semilinear). We show the following strengthening. Let X be k-recognizable, let Y be l-recognizable such that both X and Y are not Presburger-definable. Then the first-order logical theory of (N,+,X,Y) is undecidable. This is in contrast to a well-known theorem of Büchi that the first-order logical theory of (N,+,X) is decidable. Our work strengthens and depends on earlier work of Villemaire and Bès.

  The essence of Cobham’s theorem is that recognizability depends strongly on the choice of the base k. Our results strengthens this: two non-Presburger definable sets that are recognizable in multiplicatively independent bases, are not only distinct, but together computationally intractable over Presburger arithmetic. This is joint work with Christian Schulz.

• Roberto Sebastiani, Università di Trento, Italy
  From Satisfiability to Optimization Modulo Theories
  
  Satisfiability Modulo Theories (SMT) is the problem of deciding the satisfiability of a (typically quantifier-free) first-order formula with respect to some decidable first-order theory (e.g., that of linear arithmetic over the rationals LRA or the integers LIA and their sub-theories, of Arrays AR, of Bit-Vectors BV and of floating-point numbers FP) and their combinations thereof. SMT engines are widely used as backend engines in many application domains (including, e.g., planning, model checking, requirement engineering, SW and HW verification).

  Many SMT problems of interest, however, require the capability of finding models that are optimal with respect to some objective functions. These problems are grouped under the umbrella term of Optimization Modulo Theories (OMT). This presentation aims at providing an overview of the main problems, techniques, functionalities and applications of OMT, focusing on both expressivity and efficiency. Specific topics include, e.g., supporting objective functions expressed in distinct theories of interest; handling OMT incrementally; dealing with multiple objectives; dealing with important OMT sub-cases like Max-SMT. We briefly describe some interesting applications. Finally, we indicate some open problems and research directions.

• Thomas Sturm, Loria Nancy, France & MPI for Informatics, Germany
  Real Quantifier Elimination by Virtual Substitution
  In 1988, Weispfenning proposed virtual substitution (VS) as a novel quantifier elimination (QE) technique in the linear theory of reals with order. About ten years later, he generalized the method to quadratic occurrences of quantified variables and pointed out its potential for higher degrees. The theoretical development of VS has been accompanied by systematic implementations in the Redlog system, with a focus on the quadratic case plus some heuristics for higher degrees. Quite recently, Kosta provided with his PhD thesis a revised theoretical framework for arbitrary degree bounds and a corresponding generic implementation, which he instantiated up to degree 3. Applications of VS over the reals range from automated proving in geometry via verification and systematic support for satisfiability modulo theory solving (SMT) to qualitative network analysis of biological networks. In comparison to cylindrical algebraic decomposition, VS is particularly interesting for problems with low degrees, few quantifier alternations, and comparatively many parameters. Beyond the reals, VS has been used with valued fields, term algebras, parametric quantified boolean formulas, and extensions of Presburger arithmetic.

  The talk focuses on the theory of real closed fields and gives an overview of the theoretical framework of virtual substitution for regular quantifier elimination and variants like “model-producing” extended QE, generic QE, or local QE. We address theoretical complexity and advantages and disadvantages compared to other methods. On the practical side, we discuss implementation techniques and heuristics, and perspectives for pushing the current generic implementation to higher degrees. We also present an application in verification.

• Sven Verdoolaege, Cerebras Systems, Belgium
  Polyhedral Compilation and the Integer Set Library (Slides)
  Polyhedral compilation is a powerful framework for analyzing and transforming programs that are sufficiently regular. Many research and production compilers use some form of polyhedral compilation to optimize code. This can be either at a high level, mapping a high-level program to low-level code or at a low level, transforming low-level code. The Integer Set Library (isl) is a library for manipulating sets and relations of integer points described by Presburger formulas that supports several operations that are useful for polyhedral compilation and beyond.

  The presentation first illustrates polyhedral compilation in the context of the Cerebras DTG Compiler. The Integer Set Library is then described in terms of the available functionality, the interface(s) and the internal representation, with a focus on some of the design choices and possible extensions.

Click on the triangle below the talk title to view the abstracts.

Timetable

The workshop follows the joint schedule for ICALP’22 satellite workshops. All times are in CEST (UTC+2).

09:00–09:25   Registration
09:25–09:30   Opening
09:30–10:30   Roberto Sebastiani
10:30–11:00   Coffee break
11:00–12:00   Sven Verdoolaege
12:00–12:30   Short presentations
12:30–14:00   Lunch
14:00–15:00   Émilie Charlier
15:00–15:30   Thomas Sturm (Part I)
15:30–16:00   Coffee break
16:00–16:30   Thomas Sturm (Part II)
16:30–17:30   Philipp Hieronymi
17:30–17:35   Closing

Registration

The registration for in-person attendees is handled via the main ICALP registration.

Local information

The workshop takes place in the Saint Père site of the Université Paris Cité at 45, rue des Saints-Pères, 75006 Paris, on the second floor in Wilkins room. Please consult the main ICALP workshops website for further information.

Organisation

Dmitry Chistikov (Univ. Warwick)
Christoph Haase (Univ. Oxford)
Alessio Mansutti (Univ. Oxford)
Jonathan Tanner (Univ. Oxford)

Acknowledgements

This workshop receives support through the ERC project ARiAT.