In interactive theorem provers (ITPs), extensible syntax is not only crucial
to lower the cognitive burden of manipulating complex mathematical objects, but
plays a critical role in developing reusable abstractions in libraries. Most
ITPs support such extensions in the form of restrictive "syntax sugar"
substitutions and other ad hoc mechanisms, which are too rudimentary to support
many desirable abstractions. As a result, libraries are littered with
unnecessary redundancy. Tactic languages in these systems are plagued by a
seemingly unrelated issue: accidental name capture, which often produces
unexpected and counterintuitive behavior. We take ideas from the Scheme family
of programming languages and solve these two problems simultaneously by
proposing a novel hygienic macro system custom-built for ITPs. We further
describe how our approach can be extended to cover type-directed macro
expansion resulting in a single, uniform system offering multiple abstraction
levels that range from supporting simplest syntax sugars to elaboration of
formerly baked-in syntax. We have implemented our new macro system and
integrated it into the new version of the Lean theorem prover, Lean 4. Despite
its expressivity, the macro system is simple enough that it can easily be
integrated into other systems.
The concept of uniform interpolant for a quantifier-free formula from a given
formula with a list of symbols, while well-known in the logic literature, has
been unknown to the formal methods and automated reasoning community for a long
time. This concept is precisely defined. Two algorithms for computing
quantifier-free uniform interpolants in the theory of equality over
uninterpreted symbols (EUF) endowed with a list of symbols to be eliminated are
proposed. The first algorithm is non-deterministic and generates a uniform
interpolant expressed as a disjunction of conjunctions of literals, whereas the
second algorithm gives a compact representation of a uniform interpolant as a
conjunction of Horn clauses. Both algorithms exploit efficient dedicated DAG
representations of terms. Correctness and completeness proofs are supplied,
using arguments combining rewrite techniques with model theory.
We introduce FRAT, a new proof format for unsatisfiable SAT problems, and its
associated toolchain. Compared to DRAT, the FRAT format allows solvers to
include more information in proofs to reduce the computational cost of
subsequent elaboration to LRAT. The format is easy to parse forward and
backward, and it is extensible to future proof methods. The provision of
optional proof steps allows SAT solver developers to balance implementation
effort against elaboration time, with little to no overhead on solver time. We
benchmark our FRAT toolchain against a comparable DRAT toolchain and confirm
>84% median reduction in elaboration time and >94% median decrease in peak
memory usage.
A Multiplicative-Exponential Linear Logic (MELL) proof-structure can be
expanded into a set of resource proof-structures: its Taylor expansion. We
introduce a new criterion characterizing (and deciding in the finite case)
those sets of resource proof-structures that are part of the Taylor expansion
of some MELL proof-structure, through a rewriting system acting both on
resource and MELL proof-structures. We also prove semi-decidability of the type
inhabitation problem for cut-free MELL proof-structures.
While a mature body of work supports the study of rewriting systems, abstract
tools for Probabilistic Rewriting are still limited. In this paper we study the
question of uniqueness of the result (unique limit distribution), and develop a
set of proof techniques to analyze and compare reduction strategies. The goal
is to have tools to support the operational analysis of probabilistic calculi
(such as probabilistic lambda-calculi) where evaluation allows for different
reduction choices (hence different reduction paths).
We present a constant-round algorithm in the massively parallel computation
(MPC) model for evaluating a natural join where every input relation has two
attributes. Our algorithm achieves a load of $\tilde{O}(m/p^{1/\rho})$ where
$m$ is the total size of the input relations, $p$ is the number of machines,
$\rho$ is the join's fractional edge covering number, and $\tilde{O}(.)$ hides
a polylogarithmic factor. The load matches a known lower bound up to a
polylogarithmic factor. At the core of the proposed algorithm is a new theorem
(which we name the "isolated cartesian product theorem") that provides fresh
insight into the problem's mathematical structure. Our result implies that the
subgraph enumeration problem, where the goal is to report all the occurrences
of a constant-sized subgraph pattern, can be settled optimally (up to a
polylogarithmic factor) in the MPC model.
A class of relational databases has low degree if for all $\delta>0$, all but
finitely many databases in the class have degree at most $n^{\delta}$, where
$n$ is the size of the database. Typical examples are databases of bounded
degree or of degree bounded by $\log n$.
It is known that over a class of databases having low degree, first-order
boolean queries can be checked in pseudo-linear time, i.e.\ for all
$\epsilon>0$ in time bounded by $n^{1+\epsilon}$. We generalize this result by
considering query evaluation.
We show that counting the number of answers to a query can be done in
pseudo-linear time and that after a pseudo-linear time preprocessing we can
test in constant time whether a given tuple is a solution to a query or
enumerate the answers to a query with constant delay.
Proof theory provides a foundation for studying and reasoning about
programming languages, most directly based on the well-known Curry-Howard
isomorphism between intuitionistic logic and the typed lambda-calculus. More
recently, a correspondence between intuitionistic linear logic and the
session-typed pi-calculus has been discovered. In this paper, we establish an
extension of the latter correspondence for a fragment of substructural logic
with least and greatest fixed points. We describe the computational
interpretation of the resulting infinitary proof system as session-typed
processes, and provide an effectively decidable local criterion to recognize
mutually recursive processes corresponding to valid circular proofs as
introduced by Fortier and Santocanale. We show that our algorithm imposes a
stricter requirement than Fortier and Santocanale's guard condition, but is
local and compositional and therefore more suitable as the basis for a
programming language.
The deterministic membership problem for timed automata asks whether the
timed language given by a nondeterministic timed automaton can be recognised by
a deterministic timed automaton. An analogous problem can be stated in the
setting of register automata. We draw the complete decidability/complexity
landscape of the deterministic membership problem, in the setting of both
register and timed automata. For register automata, we prove that the
deterministic membership problem is decidable when the input automaton is a
nondeterministic one-register automaton (possibly with epsilon transitions) and
the number of registers of the output deterministic register automaton is
fixed. This is optimal: We show that in all the other cases the problem is
undecidable, i.e., when either (1) the input nondeterministic automaton has two
registers or more (even without epsilon transitions), or (2) it uses guessing,
or (3) the number of registers of the output deterministic automaton is not
fixed. The landscape for timed automata follows a similar pattern. We show that
the problem is decidable when the input automaton is a one-clock
nondeterministic timed automaton without epsilon transitions and the number of
clocks of the output deterministic timed automaton is fixed. Again, this is
optimal: We show that the problem in all the other cases is undecidable, i.e.,
when either (1) the input nondeterministic timed automaton has two clocks or
more, or (2) it uses epsilon transitions, or (3) the […]
Faces play a central role in the combinatorial and computational aspects of
polyhedra. In this paper, we present the first formalization of faces of
polyhedra in the proof assistant Coq. This builds on the formalization of a
library providing the basic constructions and operations over polyhedra,
including projections, convex hulls and images under linear maps. Moreover, we
design a special mechanism which automatically introduces an appropriate
representation of a polyhedron or a face, depending on the context of the
proof. We demonstrate the usability of this approach by establishing some of
the most important combinatorial properties of faces, namely that they
constitute a family of graded atomistic and coatomistic lattices closed under
interval sublattices. We also prove a theorem due to Balinski on the
$d$-connectedness of the adjacency graph of polytopes of dimension $d$.