Philipp Hieronymi

dblp:125/3255 · DBLP profile ↗
← Back
13ranked-venue papers
9as first author
5since 2021 · last 2024
—ORCID · none

Domains — the database's venue-derived domains; a paper can count in several

Theory of computation · 13 · 9 first-author · 5 since 2021
YearPublicationVenuePosition
2024 Decidability bounds for Presburger arithmetic extended by sine
abstract
We consider Presburger arithmetic extended by the sine function, call this extension sine-Presburger arithmetic (sin-PA), and systematically study decision problems for sets of sentences in sin-PA. In particular, we detail a decision algorithm for existential sin-PA sentences under assumption of Schanuel's conjecture. This procedure reduces decisions to the theory of the ordered additive group of real numbers extended by sine, which is decidable under Schanuel's conjecture. On the other hand, we prove that four alternating quantifier blocks suffice for undecidability of sin-PA sentences. To do so, we explicitly interpret the weak monadic second-order theory of the grid, which is undecidable, in sin-PA.
Eion Blanchard, Philipp Hieronymi
Ann. Pure Appl. Log.2
2024 Decidability for Sturmian words
abstract
We show that the first-order theory of Sturmian words over Presburger arithmetic is decidable. Using a general adder recognizing addition in Ostrowski numeration systems by Baranwal, Schaeffer and Shallit, we prove that the first-order expansions of Presburger arithmetic by a single Sturmian word are uniformly $\omega$-automatic, and then deduce the decidability of the theory of the class of such structures. Using an implementation of this decision algorithm called Pecan, we automatically reprove classical theorems about Sturmian words in seconds, and are able to obtain new results about antisquares and antipalindromes in characteristic Sturmian words.
Philipp Hieronymi, Dun Ma, Reed Oei, Luke Schaeffer, Christian Schulz 0013, Jeffrey Shallit
Log. Methods Comput. Sci.1
2022 Decidability for Sturmian Words
Philipp Hieronymi, Dun Ma, Reed Oei, Luke Schaeffer, Christian Schulz 0013, Jeffrey Shallit
CSL1
2022 A strong version of Cobham's theorem
abstract
Let k,ℓ≥ 2 be two multiplicatively independent integers. Cobham’s famous theorem states that a set X⊆ ℕ is both k-recognizable and ℓ-recognizable if and only if it is definable in Presburger arithmetic. Here we show the following strengthening: let X⊆ ℕm be k-recognizable, let Y⊆ ℕn be ℓ-recognizable such that both X and Y are not definable in Presburger arithmetic. Then the first-order logical theory of (ℕ,+,X,Y) is undecidable. This is in contrast to a well-known theorem of Büchi that the first-order logical theory of (ℕ,+,X) is decidable.
Philipp Hieronymi, Christian Schulz 0013
STOC1
2021 Presburger Arithmetic with algebraic scalar multiplications
abstract
We consider Presburger arithmetic (PA) extended by scalar multiplication by an algebraic irrational number $\alpha$, and call this extension $\alpha$-Presburger arithmetic ($\alpha$-PA). We show that the complexity of deciding sentences in $\alpha$-PA is substantially harder than in PA. Indeed, when $\alpha$ is quadratic and $r\geq 4$, deciding $\alpha$-PA sentences with $r$ alternating quantifier blocks and at most $c\ r$ variables and inequalities requires space at least $K 2^{\cdot^{\cdot^{\cdot^{2^{C\ell(S)}}}}}$ (tower of height $r-3$), where the constants $c, K, C>0$ only depend on $\alpha$, and $\ell(S)$ is the length of the given $\alpha$-PA sentence $S$. Furthermore deciding $\exists^{6}\forall^{4}\exists^{11}$ $\alpha$-PA sentences with at most $k$ inequalities is PSPACE-hard, where $k$ is another constant depending only on~$\alpha$. When $\alpha$ is non-quadratic, already four alternating quantifier blocks suffice for undecidability of $\alpha$-PA sentences.
Philipp Hieronymi, Danny Nguyen, Igor Pak
Log. Methods Comput. Sci.1
2020 Continuous Regular Functions
abstract
Following Chaudhuri, Sankaranarayanan, and Vardi, we say that a function $f:[0,1] \to [0,1]$ is $r$-regular if there is a B\"{u}chi automaton that accepts precisely the set of base $r \in \mathbb{N}$ representations of elements of the graph of $f$. We show that a continuous $r$-regular function $f$ is locally affine away from a nowhere dense, Lebesgue null, subset of $[0,1]$. As a corollary we establish that every differentiable $r$-regular function is affine. It follows that checking whether an $r$-regular function is differentiable is in $\operatorname{PSPACE}$. Our proofs rely crucially on connections between automata theory and metric geometry developed by Charlier, Leroy, and Rigo.
Alexi Block Gorman, Philipp Hieronymi, Elliot Kaplan, Ruoyu Meng, Erik Walsberg, Ziqin Xiong, Hongru Yang
Log. Methods Comput. Sci.2
2019 When is scalar multiplication decidable?
Philipp Hieronymi
Ann. Pure Appl. Log.1
2018 Wild theories with o-minimal open core
Philipp Hieronymi, Travis Nell, Erik Walsberg
Ann. Pure Appl. Log.1
2017 Distal and non-distal Pairs
abstract
Abstract The aim of this note is to determine whether certain non-o-minimal expansions of o-minimal theories which are known to be NIP, are also distal. We observe that while tame pairs of o-minimal structures and the real field with a discrete multiplicative subgroup have distal theories, dense pairs of o-minimal structures and related examples do not.
Philipp Hieronymi, Travis Nell
J. Symb. Log.1
2016 Expansions of the Ordered additive Group of Real numbers by two discrete Subgroups
abstract
Abstract The theory of (ℝ, <, +, ℤ, ℤa) is decidable ifais quadratic. Ifais the golden ratio, (ℝ, <, +, ℤ, ℤa) defines multiplication bya. The results are established by using the Ostrowski numeration system based on the continued fraction expansion ofato define the above structures in monadic second order logic of one successor. The converse that (ℝ, <, +, ℤ, ℤa) defines monadic second order logic of one successor, will also be established.
Philipp Hieronymi
J. Symb. Log.1
2015 A Fundamental Dichotomy for definably Complete expansions of Ordered Fields
abstract
Abstract An expansion of a definably complete field either defines a discrete subring, or the image of every definable discrete set under every definable map is nowhere dense. As an application we show a definable version of Lebesgue’s differentiation theorem.
Antongiulio Fornasiero, Philipp Hieronymi
J. Symb. Log.2
2013 An analogue of the Baire category theorem
abstract
Abstract Every definably complete expansion of an ordered field satisfies an analogue of the Baire Category Theorem.
Philipp Hieronymi
J. Symb. Log.1
2011 Dependent pairs
abstract
Abstract We prove that certain pairs of ordered structures are dependent. Among these structures are dense and tame pairs of o-minimal structures and further the real field with a multiplicative subgroup with the Mann property, regardless of whether it is dense or discrete.
Ayhan Günaydin, Philipp Hieronymi
J. Symb. Log.2