arXiv subjects

Eion Blanchard

Publications and source records attributed to Eion Blanchard.

4 recordsLinked to original sources

arXiv2022

Model-Guided Synthesis of Inductive Lemmas for FOL with Least Fixpoints

Recursively defined linked data structures embedded in a pointer-based heap and their properties are naturally expressed in pure first-order logic with least fixpoint definitions (FO+lfp) with background theories. Such logics, unlike pure first-order logic, do not admit even complete procedures. In this paper, we undertake a novel approach for synthesizing inductive hypotheses to prove validity in this logic. The idea is to utilize several kinds of finite first-order models as counterexamples that capture the non-provability and invalidity of formulas to guide the search for inductive hypotheses. We implement our procedures and evaluate them extensively over theorems involving heap data structures that require inductive proofs and demonstrate the effectiveness of our methodology.

cs.LO↗

arXiv2022

Decidability bounds for Presburger arithmetic extended by sine

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.

math.LO↗

arXiv2021

A Decoder for the Color Code with Boundaries

We introduce a decoder for the 3D color code with boundaries, which is a variation of the restriction decoder introduced by Kubicka and Delfosse. Specifically, we adapt the lift procedure to efficiently find a correction on qubits adjacent to a boundary. We numerically estimate a threshold of $4\% - 8\%$ for Pauli $X$ errors and a threshold of $0.7\% - 0.8\%$ for Pauli $Z$ errors. Our work is a first step towards characterizing the performance of Bombín's recently proposed "colorful quantum computing."

quant-ph↗

arXiv2018

Measuring Congressional District Meandering

In recent decades, state legislatures have often drawn U.S. Congressional voting districts that look---to the human eye---to be rather twisted. In this paper, we propose a method to measure how much districts "meander" via a computation of the medial axis of the region. We then compare this to the medial axis of the convex hull of the district to obtain the {\em medial-hull ratio}: a dimensionless quantity that captures the district's irregularity. We compute this quantity for many example Congressional districts.

math.HO↗