A Quantum interpretation of separating conjunction for local reasoning of Quantum programs based on separation logic

It is well-known that quantum programs are not only complicated to design but also challenging to verify because the quantum states can have exponential size and require sophisticated mathematics to encode and manipulate. To tackle the state-space explosion problem for quantum reasoning, we propose a Hoare-style inference framework that supports local reasoning for quantum programs. By providing a quantum interpretation of the separating conjunction, we are able to infuse separation logic into our framework and apply local reasoning using a quantum frame rule that is similar to the classical frame rule. For evaluation, we apply our framework to verify various quantum programs including Deutsch–Jozsa’s algorithm and Grover's algorithm.

Lower Bounds on OBDD Proofs with Several Orders

This article is motivated by seeking lower bounds on OBDD(∧, w, r) refutations, namely, OBDD refutations that allow weakening and arbitrary reorderings. We first work with 1 - NBP ∧ refutations based on read-once nondeterministic branching programs. These generalize OBDD(∧, r) refutations. There are polynomial size 1 - NBP(∧) refutations of the pigeonhole principle, hence 1-NBP(∧) is strictly stronger than OBDD}(∧, r). There are also formulas that have polynomial size tree-like resolution refutations but require exponential size 1-NBP(∧) refutations. As a corollary, OBDD}(∧, r) does not simulate tree-like resolution, answering a previously open question. The system 1-NBP(∧, ∃) uses projection inferences instead of weakening. 1-NBP(∧, ∃ k is the system restricted to projection on at most k distinct variables. We construct explicit constant degree graphs G n on n vertices and an ε > 0, such that 1-NBP(∧, ∃ ε n ) refutations of the Tseitin formula for G n require exponential size. Second, we study the proof system OBDD}(∧, w, r ℓ ), which allows ℓ different variable orders in a refutation. We prove an exponential lower bound on the complexity of tree-like OBDD(∧, w, r ℓ ) refutations for ℓ = ε log n , where n is the number of variables and ε > 0 is a constant. The lower bound is based on multiparty communication complexity.

Proof Complexity of Modal Resolution

We investigate the proof complexity of modal resolution systems developed by Nalon and Dixon (J Algorithms 62(3–4):117–134, 2007) and Nalon et al. (in: Automated reasoning with analytic Tableaux and related methods—24th international conference, (TABLEAUX’15), pp 185–200, 2015), which form the basis of modal theorem proving (Nalon et al., in: Proceedings of the twenty-sixth international joint conference on artificial intelligence (IJCAI’17), pp 4919–4923, 2017). We complement these calculi by a new tighter variant and show that proofs can be efficiently translated between all these variants, meaning that the calculi are equivalent from a proof complexity perspective. We then develop the first lower bound technique for modal resolution using Prover–Delayer games, which can be used to establish “genuine” modal lower bounds for size of dag-like modal resolution proofs. We illustrate the technique by devising a new modal pigeonhole principle, which we demonstrate to require exponential-size proofs in modal resolution. Finally, we compare modal resolution to the modal Frege systems of Hrubeš (Ann Pure Appl Log 157(2–3):194–205, 2009) and obtain a “genuinely” modal separation.

On the Power of Symmetric Linear Programs

We consider families of symmetric linear programs (LPs) that decide a property of graphs (or other relational structures) in the sense that, for each size of graph, there is an LP defining a polyhedral lift that separates the integer points corresponding to graphs with the property from those corresponding to graphs without the property. We show that this is equivalent, with at most polynomial blow-up in size, to families of symmetric Boolean circuits with threshold gates. In particular, when we consider polynomial-size LPs, the model is equivalent to definability in a non-uniform version of fixed-point logic with counting (FPC). Known upper and lower bounds for FPC apply to the non-uniform version. In particular, this implies that the class of graphs with perfect matchings has polynomial-size symmetric LPs, while we obtain an exponential lower bound for symmetric LPs for the class of Hamiltonian graphs. We compare and contrast this with previous results (Yannakakis 1991), showing that any symmetric LPs for the matching and TSP polytopes have exponential size. As an application, we establish that for random, uniformly distributed graphs, polynomial-size symmetric LPs are as powerful as general Boolean circuits. We illustrate the effect of this on the well-studied planted-clique problem.

The descriptional power of queue automata of constant length

We consider the notion of a constant length queue automaton—i.e., a traditional queue automaton with a built-in constant limit on the length of its queue—as a formalism for representing regular languages. We show that the descriptional power of constant length queue automata greatly outperforms that of traditional finite state automata, of constant height pushdown automata, and of straight line programs for regular expressions, by providing optimal exponential and double-exponential size gaps. Moreover, we prove that constant height pushdown automata can be simulated by constant length queue automata paying only by a linear size increase, and that removing nondeterminism in constant length queue automata requires an optimal exponential size blow-up, against the optimal double-exponential cost for determinizing constant height pushdown automata. Finally, we investigate the size cost of implementing Boolean language operations on deterministic and nondeterministic constant length queue automata.

Non-Self-Embedding Grammars and Descriptional Complexity

Non-self-embedding grammars are a subclass of context-free grammars which only generate regular languages. The size costs of the conversion of non-self-embedding grammars into equivalent finite automata are studied, by proving optimal bounds for the number of states of nondeterministic and deterministic automata equivalent to given non-self-embedding grammars. In particular, each non-self-embedding grammar of size s can be converted into an equivalent nondeterministic automaton which has an exponential size in s and into an equivalent deterministic automaton which has a double exponential size in s. These costs are shown to be optimal. Moreover, they do not change if the larger class of quasi-non-self-embedding grammars, which still generate only regular languages, is considered. In the case of letter bounded languages, the cost of the conversion of non-self-embedding grammars and quasi-non-self-embedding grammars into deterministic automata reduces to an exponential of a polynomial in s.

Computational and Proof Complexity of Partial String Avoidability

The partial string avoidability problem is stated as follows: given a finite set of strings with possible “holes” (wildcard symbols), determine whether there exists a two-sided infinite string containing no substrings from this set, assuming that a hole matches every symbol. The problem is known to be NP-hard and in PSPACE, and this article establishes its PSPACE-completeness. Next, string avoidability over the binary alphabet is interpreted as a version of conjunctive normal form satisfiability problem, where each clause has infinitely many shifted variants. Non-satisfiability of these formulas can be proved using variants of classical propositional proof systems, augmented with derivation rules for shifting proof lines (such as clauses, inequalities, polynomials, etc.). First, it is proved that there is a particular formula that has a short refutation in Resolution with a shift rule but requires classical proofs of exponential size. At the same time, it is shown that exponential lower bounds for classical proof systems can be translated for their shifted versions. Finally, it is shown that superpolynomial lower bounds on the size of shifted proofs would separate NP from PSPACE; a connection to lower bounds on circuit complexity is also established.

Pseudo-free families of computational universal algebras

Let Ω be a finite set of finitary operation symbols. We initiate the study of (weakly) pseudo-free families of computational Ω-algebras in arbitrary varieties of Ω-algebras. A family (Hd | d ∈ D) of computational Ω-algebras (where D ⊆ {0, 1}*) is called polynomially bounded (resp., having exponential size) if there exists a polynomial η such that for all d ∈ D, the length of any representation of every h ∈ Hd is at most $\eta (|d|)\left( \text{ resp}\text{., }\left| {{H}_{d}} \right|\le {{2}^{\eta (|d|)}} \right).$ First, we prove the following trichotomy: (i) if Ω consists of nullary operation symbols only, then there exists a polynomially bounded pseudo-free family; (ii) if Ω = Ω0 ∪ {ω}, where Ω0 consists of nullary operation symbols and the arity of ω is 1, then there exist an exponential-size pseudo-free family and a polynomially bounded weakly pseudo-free family; (iii) in all other cases, the existence of polynomially bounded weakly pseudo-free families implies the existence of collision-resistant families of hash functions. In this trichotomy, (weak) pseudo-freeness is meant in the variety of all Ω-algebras. Second, assuming the existence of collision-resistant families of hash functions, we construct a polynomially bounded weakly pseudo-free family and an exponential-size pseudo-free family in the variety of all m-ary groupoids, where m is an arbitrary positive integer.

Revisiting separation: algorithms and complexity

Linear temporal logic (LTL) with Since and Until modalities is expressively equivalent, over the class of complete linear orders, to a fragment of first-order logic known as FOMLO (first-order monadic logic of order). It turns out that LTL, under some basic assumptions, is expressively complete if and only if it has the property, called separation, that every formula is equivalent to a Boolean combination of formulas that each refer only to the past, present or future. Herein we present simple algorithms and their implementations to perform separation of the LTL with Since and Until, over discrete and complete linear orders, and translation from FOMLO formulas into equivalent temporal logic formulas. We additionally show that the separation of a certain fragment of LTL results in at most a double exponential size growth.

THE FLUTED FRAGMENT REVISITED

We study the fluted fragment, a decidable fragment of first-order logic with an unbounded number of variables, motivated by the work of W. V. Quine. We show that the satisfiability problem for this fragment has nonelementary complexity, thus refuting an earlier published claim by W. C. Purdy that it is in NExpTime. More precisely, we consider ${\cal F}{{\cal L}^m}$, the intersection of the fluted fragment and the m-variable fragment of first-order logic, for all $m \ge 1$. We show that, for $m \ge 2$, this subfragment forces $\left\lfloor {m/2} \right\rfloor$-tuply exponentially large models, and that its satisfiability problem is $\left\lfloor {m/2} \right\rfloor$-NExpTime-hard. We further establish that, for $m \ge 3$, any satisfiable ${\cal F}{{\cal L}^m}$-formula has a model of at most ($m - 2$)-tuply exponential size, whence the satisfiability (= finite satisfiability) problem for this fragment is in ($m - 2$)-NExpTime. Together with other, known, complexity results, this provides tight complexity bounds for ${\cal F}{{\cal L}^m}$ for all $m \le 4$.