Editors: Anuj Dawar, Anca Muscholl, Catuscia Palamidessi
Samir Datta ; Anish Mukherjee ; Thomas Schwentick ; Nils Vortmeier ; Thomas Zeume.
In the setting of DynFO, dynamic programs update the stored result of a query
whenever the underlying data changes. This update is expressed in terms of
first-order logic. We introduce a strategy for constructing dynamic programs
that utilises periodic computation of auxiliary data from scratch and the
ability to maintain a query for a limited number of change steps. We show that
if some program can maintain a query for log n change steps after an
AC$^1$-computable initialisation, it can be maintained by a first-order dynamic
program as well, i.e., in DynFO. As an application, it is shown that decision
and optimisation problems defined by monadic second-order (MSO) formulas are in
DynFO, if only change sequences that produce graphs of bounded treewidth are
allowed. To establish this result, a Feferman-Vaught-type composition theorem
for MSO is established that might be useful in its own right.
Benjamin Rossman.
We consider the action of a linear subspace $U$ of $\{0,1\}^n$ on the set of
AC$^0$ formulas with inputs labeled by literals in the set $\{X_1,\overline
X_1,\dots,X_n,\overline X_n\}$, where an element $u \in U$ acts on formulas by
transposing the $i$th pair of literals for all $i \in [n]$ such that $u_i=1$. A
formula is {\em $U$-invariant} if it is fixed by this action. For example,
there is a well-known recursive construction of depth $d+1$ formulas of size
$O(n{\cdot}2^{dn^{1/d}})$ computing the $n$-variable PARITY function; these
formulas are easily seen to be $P$-invariant where $P$ is the subspace of
even-weight elements of $\{0,1\}^n$. In this paper we establish a nearly
matching $2^{d(n^{1/d}-1)}$ lower bound on the $P$-invariant depth $d+1$
formula size of PARITY. Quantitatively this improves the best known
$\Omega(2^{\frac{1}{84}d(n^{1/d}-1)})$ lower bound for {\em unrestricted} depth
$d+1$ formulas, while avoiding the use of the switching lemma. More generally,
for any linear subspaces $U \subset V$, we show that if a Boolean function is
$U$-invariant and non-constant over $V$, then its $U$-invariant depth $d+1$
formula size is at least $2^{d(m^{1/d}-1)}$ where $m$ is the minimum Hamming
weight of a vector in $U^\bot \setminus V^\bot$.
Michael Benedikt ; Pierre Bourhis ; Michael Vanden Boom.
We look at characterizing which formulas are expressible in rich decidable
logics such as guarded fixpoint logic, unary negation fixpoint logic, and
guarded negation fixpoint logic. We consider semantic characterizations of
definability, as well as effective characterizations. Our algorithms revolve
around a finer analysis of the tree-model property and a refinement of the
method of moving back and forth between relational logics and logics over
trees.
Gilles Barthe ; Thomas Espitau ; Justin Hsu ; Tetsuya Sato ; Pierre-Yves Strub.
Recent developments in formal verification have identified approximate
liftings (also known as approximate couplings) as a clean, compositional
abstraction for proving differential privacy. This construction can be defined
in two styles. Earlier definitions require the existence of one or more witness
distributions, while a recent definition by Sato uses universal quantification
over all sets of samples. These notions have each have their own strengths: the
universal version is more general than the existential ones, while existential
liftings are known to satisfy more precise composition principles.
We propose a novel, existential version of approximate lifting, called
$\star$-lifting, and show that it is equivalent to Sato's construction for
discrete probability measures. Our work unifies all known notions of
approximate lifting, yielding cleaner properties, more general constructions,
and more precise composition theorems for both styles of lifting, enabling
richer proofs of differential privacy. We also clarify the relation between
existing definitions of approximate lifting, and consider more general
approximate liftings based on $f$-divergences.
MichaĆ«l Cadilhac ; Olivier Carton ; Charles Paperman.
A word-to-word function is continuous for a class of languages~$\mathcal{V}$
if its inverse maps $\mathcal{V}$_languages to~$\mathcal{V}$. This notion
provides a basis for an algebraic study of transducers, and was integral to the
characterization of the sequential transducers computable in some circuit
complexity classes.
Here, we report on the decidability of continuity for functional transducers
and some standard classes of regular languages. To this end, we develop a
robust theory rooted in the standard profinite analysis of regular languages.
Since previous algebraic studies of transducers have focused on the sole
structure of the underlying input automaton, we also compare the two algebraic
approaches. We focus on two questions: When are the automaton structure and the
continuity properties related, and when does continuity propagate to
superclasses?
Olivier Bournez ; Amaury Pouly.
An astonishing fact was established by Lee A. Rubel (1981): there exists a
fixed non-trivial fourth-order polynomial differential algebraic equation (DAE)
such that for any positive continuous function $\varphi$ on the reals, and for
any positive continuous function $\epsilon(t)$, it has a $\mathcal{C}^\infty$
solution with $| y(t) - \varphi(t) | < \epsilon(t)$ for all $t$. Lee A. Rubel
provided an explicit example of such a polynomial DAE. Other examples of
universal DAE have later been proposed by other authors. However, Rubel's DAE
\emph{never} has a unique solution, even with a finite number of conditions of
the form $y^{(k_i)}(a_i)=b_i$.
The question whether one can require the solution that approximates $\varphi$
to be the unique solution for a given initial data is a well known open problem
[Rubel 1981, page 2], [Boshernitzan 1986, Conjecture 6.2]. In this article, we
solve it and show that Rubel's statement holds for polynomial ordinary
differential equations (ODEs), and since polynomial ODEs have a unique solution
given an initial data, this positively answers Rubel's open problem. More
precisely, we show that there exists a \textbf{fixed} polynomial ODE such that
for any $\varphi$ and $\epsilon(t)$ there exists some initial condition that
yields a solution that is $\epsilon$-close to $\varphi$ at all times.
In particular, the solution to the ODE is necessarily analytic, and we show
that the initial condition is computable from the target function and […]