Search for: All records

Redox is a unique, programmable modality capable of bridging communication between biology and electronics. Previous studies have shown that theE. coliredox-responsive OxyRS regulon can be re-wired to accept electrochemically generated hydrogen peroxide (H₂O₂) as an inducer of gene expression. Here we report that the redox-active phenolic plant signaling molecule acetosyringone (AS) can also induce gene expression from the OxyRS regulon. AS must be oxidized, however, as the reduced state present under normal conditions cannot induce gene expression. Thus, AS serves as a “pro-signaling molecule” that can be activated by its oxidation—in our case by application of oxidizing potential to an electrode. We show that the OxyRS regulon is not induced electrochemically if the imposed electrode potential is in the mid-physiological range. Electronically sliding the applied potential to either oxidative or reductive extremes induces this regulon but through different mechanisms: reduction of O₂to form H₂O₂or oxidation of AS. Fundamentally, this work reinforces the emerging concept that redox signaling depends more on molecular activities than molecular structure. From an applications perspective, the creation of an electronically programmed “pro-signal” dramatically expands the toolbox for electronic control of biological responses in microbes, including in complex environments, cell-based materials, and biomanufacturing.

Proving the equivalence between SQL queries is a fundamental problem in database research. Existing solvers model queries using algebraic representations and convert such representations into first-order logic formulas so that query equivalence can be verified by solving a satisfiability problem. The main challenge lies in unbounded summations, which appear commonly in a query's algebraic representation in order to model common SQL features, such as projection and aggregate functions. Unfortunately, existing solvers handle unbounded summations in an ad-hoc manner based on heuristics or syntax comparison, which severely limits the set of queries that can be supported.

This paper develops a new SQL equivalence prover called SQLSolver, which can handle unbounded summations in a principled way. Our key insight is to use the theory of LIA^*, which extends linear integer arithmetic formulas with unbounded sums and provides algorithms to translate a LIA^* formula to a LIA formula that can be decided using existing SMT solvers. We augment the basic LIA^* theory to handle several complex scenarios (such as nested unbounded summations) that arise from modeling real-world queries. We evaluate SQLSolver with 359 equivalent query pairs derived from the SQL rewrite rules in Calcite and Spark SQL. SQLSolver successfully proves 346 pairs of them, which significantly outperforms existing provers.

Diversity, group representation, and similar needs often apply to query results, which in turn require constraints on the sizes of various subgroups in the result set. Traditional relational queries only specify conditions as part of the query predicate(s), and do not support such restrictions on the output. In this paper, we study the problem of modifying queries to have the result satisfy constraints on the sizes of multiple subgroups in it. This problem, in the worst case, cannot be solved in polynomial time. Yet, with the help of provenance annotation, we are able to develop a query refinement method that works quite efficiently, as we demonstrate through extensive experiments.