28 Search Results for "Power, James F."


Document
Dependently Sorted Theorem Proving for Mathematical Foundations

Authors: Yiming Xu and Michael Norrish

Published in: LIPIcs, Volume 268, 14th International Conference on Interactive Theorem Proving (ITP 2023)


Abstract
We describe a new meta-logical system for mechanising foundations of mathematics. Using dependent sorts and first order logic, our system (implemented as an LCF-style theorem-prover) improves on the state-of-the-art by providing efficient type-checking, convenient automatic rewriting and interactive proof support. We assess our implementation by axiomatising Lawvere’s Elementary Theory of the Category of Sets (ETCS) [F. William Lawvere, 1964], and Shulman’s Sets, Elements and Relations (SEAR) [Michael Shulman, 2022]. We then demonstrate our system’s ability to perform some basic mathematical constructions such as quotienting, induction and coinduction by constructing integers, lists and colists. We also compare with some existing work on modal model theory done in HOL4 [Yiming Xu and Michael Norrish, 2020]. Using the analogue of type-quantification, we are able to prove a theorem that this earlier work could not. Finally, we show that SEAR can construct sets that are larger than any finite iteration of the power set operation. This shows that SEAR, unlike HOL, can construct sets beyond V_{ω+ω}.

Cite as

Yiming Xu and Michael Norrish. Dependently Sorted Theorem Proving for Mathematical Foundations. In 14th International Conference on Interactive Theorem Proving (ITP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 268, pp. 33:1-33:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)


Copy BibTex To Clipboard

@InProceedings{xu_et_al:LIPIcs.ITP.2023.33,
  author =	{Xu, Yiming and Norrish, Michael},
  title =	{{Dependently Sorted Theorem Proving for Mathematical Foundations}},
  booktitle =	{14th International Conference on Interactive Theorem Proving (ITP 2023)},
  pages =	{33:1--33:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-284-6},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{268},
  editor =	{Naumowicz, Adam and Thiemann, Ren\'{e}},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2023.33},
  URN =		{urn:nbn:de:0030-drops-184085},
  doi =		{10.4230/LIPIcs.ITP.2023.33},
  annote =	{Keywords: first order logic, sorts, structural set theory, mechanised mathematics, foundation of mathematics, category theory}
}
Document
Invited Talk
The Skolem Landscape (Invited Talk)

Authors: James Worrell

Published in: LIPIcs, Volume 261, 50th International Colloquium on Automata, Languages, and Programming (ICALP 2023)


Abstract
The Skolem Problem asks to determine whether a given integer linear recurrence sequence (LRS) has a zero term. This decision problem arises within a number of different topics in computer science, including loop termination, weighted automata, formal power series, and probabilistic model checking, among many other examples. Decidability of the problem is notoriously open, despite having been the subject of sustained interest over several decades [Halava et al., 2005]. More specifically, the problem is known to be decidable for recurrences of order at most 4 - a result obtained some 40 years ago [Mignotte et al., 1984; Vereshchagin, 1985] - while decidability is open already for recurrences of order 5. In this talk we take a wide-ranging view of the Skolem Problem. We survey its history and context, starting with the theorem of Skolem-Mahler-Lech characterising the set of zeros of a LRS over fields of characteristic zero. Here we explain the non-effective nature of the existing proofs of the theorem. Among modern developments, we overview versions of the Skolem-Mahler-Lech theorem for non-linear recurrences and for fields of non-zero characteristic. We also describe two recent directions of progress toward showing decidability of the Skolem Problem subject to classical number theoretic conjectures. The first new development concerns a recent algorithm [Y. Bilu et al., 2022] that decides the problem on the class of simple LRS (those with simple characteristic roots) subject to two classical conjectures about the exponential function. The algorithm is self-certifying: its output comes with a certificate of correctness that can be checked unconditionally. The two conjectures alluded to above are required for the proof of termination of the algorithm. A second new development concerns the notion of Universal Skolem Set [F. Luca et al., 2022]: a recursive set S of positive integers such that it is decidable whether a given non-degenerate linear recurrence sequence has a zero in S. Decidability of the Skolem Problem is equivalent to the assertion that ℕ is a Universal Skolem Set. In lieu of this one can ask whether there exists a Universal Skolem Set of density one. We will present a recent a construction of a Universal Skolem Set that has positive density unconditionally and has density one subject to the Bateman-Horn conjecture in number theory. The latter is a far-reaching generalisation of Hardy and Littlewood’s twin primes conjecture.

Cite as

James Worrell. The Skolem Landscape (Invited Talk). In 50th International Colloquium on Automata, Languages, and Programming (ICALP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 261, pp. 5:1-5:2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)


Copy BibTex To Clipboard

@InProceedings{worrell:LIPIcs.ICALP.2023.5,
  author =	{Worrell, James},
  title =	{{The Skolem Landscape}},
  booktitle =	{50th International Colloquium on Automata, Languages, and Programming (ICALP 2023)},
  pages =	{5:1--5:2},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-278-5},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{261},
  editor =	{Etessami, Kousha and Feige, Uriel and Puppis, Gabriele},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2023.5},
  URN =		{urn:nbn:de:0030-drops-180573},
  doi =		{10.4230/LIPIcs.ICALP.2023.5},
  annote =	{Keywords: Automata, Formal Languages, Linear Recurrence Sequences}
}
Document
On the Complexity of the Escape Problem for Linear Dynamical Systems over Compact Semialgebraic Sets

Authors: Julian D'Costa, Engel Lefaucheux, Eike Neumann, Joël Ouaknine, and James Worrell

Published in: LIPIcs, Volume 202, 46th International Symposium on Mathematical Foundations of Computer Science (MFCS 2021)


Abstract
We study the computational complexity of the Escape Problem for discrete-time linear dynamical systems over compact semialgebraic sets, or equivalently the Termination Problem for affine loops with compact semialgebraic guard sets. Consider the fragment of the theory of the reals consisting of negation-free ∃ ∀-sentences without strict inequalities. We derive several equivalent characterisations of the associated complexity class which demonstrate its robustness and illustrate its expressive power. We show that the Compact Escape Problem is complete for this class.

Cite as

Julian D'Costa, Engel Lefaucheux, Eike Neumann, Joël Ouaknine, and James Worrell. On the Complexity of the Escape Problem for Linear Dynamical Systems over Compact Semialgebraic Sets. In 46th International Symposium on Mathematical Foundations of Computer Science (MFCS 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 202, pp. 33:1-33:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)


Copy BibTex To Clipboard

@InProceedings{dcosta_et_al:LIPIcs.MFCS.2021.33,
  author =	{D'Costa, Julian and Lefaucheux, Engel and Neumann, Eike and Ouaknine, Jo\"{e}l and Worrell, James},
  title =	{{On the Complexity of the Escape Problem for Linear Dynamical Systems over Compact Semialgebraic Sets}},
  booktitle =	{46th International Symposium on Mathematical Foundations of Computer Science (MFCS 2021)},
  pages =	{33:1--33:21},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-201-3},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{202},
  editor =	{Bonchi, Filippo and Puglisi, Simon J.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2021.33},
  URN =		{urn:nbn:de:0030-drops-144734},
  doi =		{10.4230/LIPIcs.MFCS.2021.33},
  annote =	{Keywords: Discrete linear dynamical systems, Program termination, Compact semialgebraic sets, Theory of the reals}
}
Document
On p-Group Isomorphism: Search-To-Decision, Counting-To-Decision, and Nilpotency Class Reductions via Tensors

Authors: Joshua A. Grochow and Youming Qiao

Published in: LIPIcs, Volume 200, 36th Computational Complexity Conference (CCC 2021)


Abstract
In this paper we study some classical complexity-theoretic questions regarding Group Isomorphism (GpI). We focus on p-groups (groups of prime power order) with odd p, which are believed to be a bottleneck case for GpI, and work in the model of matrix groups over finite fields. Our main results are as follows. - Although search-to-decision and counting-to-decision reductions have been known for over four decades for Graph Isomorphism (GI), they had remained open for GpI, explicitly asked by Arvind & Torán (Bull. EATCS, 2005). Extending methods from Tensor Isomorphism (Grochow & Qiao, ITCS 2021), we show moderately exponential-time such reductions within p-groups of class 2 and exponent p. - Despite the widely held belief that p-groups of class 2 and exponent p are the hardest cases of GpI, there was no reduction to these groups from any larger class of groups. Again using methods from Tensor Isomorphism (ibid.), we show the first such reduction, namely from isomorphism testing of p-groups of "small" class and exponent p to those of class two and exponent p. For the first results, our main innovation is to develop linear-algebraic analogues of classical graph coloring gadgets, a key technique in studying the structural complexity of GI. Unlike the graph coloring gadgets, which support restricting to various subgroups of the symmetric group, the problems we study require restricting to various subgroups of the general linear group, which entails significantly different and more complicated gadgets. The analysis of one of our gadgets relies on a classical result from group theory regarding random generation of classical groups (Kantor & Lubotzky, Geom. Dedicata, 1990). For the nilpotency class reduction, we combine a runtime analysis of the Lazard Correspondence with Tensor Isomorphism-completeness results (Grochow & Qiao, ibid.).

Cite as

Joshua A. Grochow and Youming Qiao. On p-Group Isomorphism: Search-To-Decision, Counting-To-Decision, and Nilpotency Class Reductions via Tensors. In 36th Computational Complexity Conference (CCC 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 200, pp. 16:1-16:38, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)


Copy BibTex To Clipboard

@InProceedings{grochow_et_al:LIPIcs.CCC.2021.16,
  author =	{Grochow, Joshua A. and Qiao, Youming},
  title =	{{On p-Group Isomorphism: Search-To-Decision, Counting-To-Decision, and Nilpotency Class Reductions via Tensors}},
  booktitle =	{36th Computational Complexity Conference (CCC 2021)},
  pages =	{16:1--16:38},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-193-1},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{200},
  editor =	{Kabanets, Valentine},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CCC.2021.16},
  URN =		{urn:nbn:de:0030-drops-142905},
  doi =		{10.4230/LIPIcs.CCC.2021.16},
  annote =	{Keywords: group isomorphism, search-to-decision reduction, counting-to-decision reduction, nilpotent group isomorphism, p-group isomorphism, tensor isomorphism}
}
Document
Track A: Algorithms, Complexity and Games
Quantum Query Complexity with Matrix-Vector Products

Authors: Andrew M. Childs, Shih-Han Hung, and Tongyang Li

Published in: LIPIcs, Volume 198, 48th International Colloquium on Automata, Languages, and Programming (ICALP 2021)


Abstract
We study quantum algorithms that learn properties of a matrix using queries that return its action on an input vector. We show that for various problems, including computing the trace, determinant, or rank of a matrix or solving a linear system that it specifies, quantum computers do not provide an asymptotic speedup over classical computation. On the other hand, we show that for some problems, such as computing the parities of rows or columns or deciding if there are two identical rows or columns, quantum computers provide exponential speedup. We demonstrate this by showing equivalence between models that provide matrix-vector products, vector-matrix products, and vector-matrix-vector products, whereas the power of these models can vary significantly for classical computation.

Cite as

Andrew M. Childs, Shih-Han Hung, and Tongyang Li. Quantum Query Complexity with Matrix-Vector Products. In 48th International Colloquium on Automata, Languages, and Programming (ICALP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 198, pp. 55:1-55:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)


Copy BibTex To Clipboard

@InProceedings{childs_et_al:LIPIcs.ICALP.2021.55,
  author =	{Childs, Andrew M. and Hung, Shih-Han and Li, Tongyang},
  title =	{{Quantum Query Complexity with Matrix-Vector Products}},
  booktitle =	{48th International Colloquium on Automata, Languages, and Programming (ICALP 2021)},
  pages =	{55:1--55:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-195-5},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{198},
  editor =	{Bansal, Nikhil and Merelli, Emanuela and Worrell, James},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2021.55},
  URN =		{urn:nbn:de:0030-drops-141242},
  doi =		{10.4230/LIPIcs.ICALP.2021.55},
  annote =	{Keywords: Quantum algorithms, quantum query complexity, matrix-vector products}
}
Document
Track A: Algorithms, Complexity and Games
Quantum Algorithms for Matrix Scaling and Matrix Balancing

Authors: Joran van Apeldoorn, Sander Gribling, Yinan Li, Harold Nieuwboer, Michael Walter, and Ronald de Wolf

Published in: LIPIcs, Volume 198, 48th International Colloquium on Automata, Languages, and Programming (ICALP 2021)


Abstract
Matrix scaling and matrix balancing are two basic linear-algebraic problems with a wide variety of applications, such as approximating the permanent, and pre-conditioning linear systems to make them more numerically stable. We study the power and limitations of quantum algorithms for these problems. We provide quantum implementations of two classical (in both senses of the word) methods: Sinkhorn’s algorithm for matrix scaling and Osborne’s algorithm for matrix balancing. Using amplitude estimation as our main tool, our quantum implementations both run in time Õ(√{mn}/ε⁴) for scaling or balancing an n × n matrix (given by an oracle) with m non-zero entries to within 𝓁₁-error ε. Their classical analogs use time Õ(m/ε²), and every classical algorithm for scaling or balancing with small constant ε requires Ω(m) queries to the entries of the input matrix. We thus achieve a polynomial speed-up in terms of n, at the expense of a worse polynomial dependence on the obtained 𝓁₁-error ε. Even for constant ε these problems are already non-trivial (and relevant in applications). Along the way, we extend the classical analysis of Sinkhorn’s and Osborne’s algorithm to allow for errors in the computation of marginals. We also adapt an improved analysis of Sinkhorn’s algorithm for entrywise-positive matrices to the 𝓁₁-setting, obtaining an Õ(n^{1.5}/ε³)-time quantum algorithm for ε-𝓁₁-scaling. We also prove a lower bound, showing our quantum algorithm for matrix scaling is essentially optimal for constant ε: every quantum algorithm for matrix scaling that achieves a constant 𝓁₁-error w.r.t. uniform marginals needs Ω(√{mn}) queries.

Cite as

Joran van Apeldoorn, Sander Gribling, Yinan Li, Harold Nieuwboer, Michael Walter, and Ronald de Wolf. Quantum Algorithms for Matrix Scaling and Matrix Balancing. In 48th International Colloquium on Automata, Languages, and Programming (ICALP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 198, pp. 110:1-110:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)


Copy BibTex To Clipboard

@InProceedings{vanapeldoorn_et_al:LIPIcs.ICALP.2021.110,
  author =	{van Apeldoorn, Joran and Gribling, Sander and Li, Yinan and Nieuwboer, Harold and Walter, Michael and de Wolf, Ronald},
  title =	{{Quantum Algorithms for Matrix Scaling and Matrix Balancing}},
  booktitle =	{48th International Colloquium on Automata, Languages, and Programming (ICALP 2021)},
  pages =	{110:1--110:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-195-5},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{198},
  editor =	{Bansal, Nikhil and Merelli, Emanuela and Worrell, James},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2021.110},
  URN =		{urn:nbn:de:0030-drops-141793},
  doi =		{10.4230/LIPIcs.ICALP.2021.110},
  annote =	{Keywords: Matrix scaling, matrix balancing, quantum algorithms}
}
Document
Track B: Automata, Logic, Semantics, and Theory of Programming
A Complexity Approach to Tree Algebras: the Bounded Case

Authors: Thomas Colcombet and Arthur Jaquard

Published in: LIPIcs, Volume 198, 48th International Colloquium on Automata, Languages, and Programming (ICALP 2021)


Abstract
In this paper, we initiate a study of the expressive power of tree algebras, and more generally infinitely sorted algebras, based on their asymptotic complexity. We provide a characterization of the expressiveness of tree algebras of bounded complexity. Tree algebras in many of their forms, such as clones, hyperclones, operads, etc, as well as other kind of algebras, are infinitely sorted: the carrier is a multi sorted set indexed by a parameter that can be interpreted as the number of variables or hole types. Finite such algebras - meaning when all sorts are finite - can be classified depending on the asymptotic size of the carrier sets as a function of the parameter, that we call the complexity of the algebra. This naturally defines the notions of algebras of bounded, linear, polynomial, exponential or doubly exponential complexity... We initiate in this work a program of analysis of the complexity of infinitely sorted algebras. Our main result precisely characterizes the tree algebras of bounded complexity based on the languages that they recognize as Boolean closures of simple languages. Along the way, we prove that such algebras that are syntactic (minimal for a language) are exactly those in which, as soon as there are sufficiently many variables, the elements are invariant under permutation of the variables.

Cite as

Thomas Colcombet and Arthur Jaquard. A Complexity Approach to Tree Algebras: the Bounded Case. In 48th International Colloquium on Automata, Languages, and Programming (ICALP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 198, pp. 127:1-127:13, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)


Copy BibTex To Clipboard

@InProceedings{colcombet_et_al:LIPIcs.ICALP.2021.127,
  author =	{Colcombet, Thomas and Jaquard, Arthur},
  title =	{{A Complexity Approach to Tree Algebras: the Bounded Case}},
  booktitle =	{48th International Colloquium on Automata, Languages, and Programming (ICALP 2021)},
  pages =	{127:1--127:13},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-195-5},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{198},
  editor =	{Bansal, Nikhil and Merelli, Emanuela and Worrell, James},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2021.127},
  URN =		{urn:nbn:de:0030-drops-141966},
  doi =		{10.4230/LIPIcs.ICALP.2021.127},
  annote =	{Keywords: Tree algebra, infinite tree, language theory}
}
Document
Track B: Automata, Logic, Semantics, and Theory of Programming
The Theory of Concatenation over Finite Models

Authors: Dominik D. Freydenberger and Liat Peterfreund

Published in: LIPIcs, Volume 198, 48th International Colloquium on Automata, Languages, and Programming (ICALP 2021)


Abstract
We propose FC, a new logic on words that combines finite model theory with the theory of concatenation - a first-order logic that is based on word equations. Like the theory of concatenation, FC is built around word equations; in contrast to it, its semantics are defined to only allow finite models, by limiting the universe to a word and all its factors. As a consequence of this, FC has many of the desirable properties of FO on finite models, while being far more expressive than FO[<]. Most noteworthy among these desirable properties are sufficient criteria for efficient model checking, and capturing various complexity classes by adding operators for transitive closures or fixed points. Not only does FC allow us to obtain new insights and techniques for expressive power and efficient evaluation of document spanners, but it also provides a general framework for logic on words that also has potential applications in other areas.

Cite as

Dominik D. Freydenberger and Liat Peterfreund. The Theory of Concatenation over Finite Models. In 48th International Colloquium on Automata, Languages, and Programming (ICALP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 198, pp. 130:1-130:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)


Copy BibTex To Clipboard

@InProceedings{freydenberger_et_al:LIPIcs.ICALP.2021.130,
  author =	{Freydenberger, Dominik D. and Peterfreund, Liat},
  title =	{{The Theory of Concatenation over Finite Models}},
  booktitle =	{48th International Colloquium on Automata, Languages, and Programming (ICALP 2021)},
  pages =	{130:1--130:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-195-5},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{198},
  editor =	{Bansal, Nikhil and Merelli, Emanuela and Worrell, James},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2021.130},
  URN =		{urn:nbn:de:0030-drops-141997},
  doi =		{10.4230/LIPIcs.ICALP.2021.130},
  annote =	{Keywords: finite model theory, word equations, descriptive complexity, model checking, document spanners}
}
Document
Algorithmic Persuasion with Evidence

Authors: Martin Hoefer, Pasin Manurangsi, and Alexandros Psomas

Published in: LIPIcs, Volume 185, 12th Innovations in Theoretical Computer Science Conference (ITCS 2021)


Abstract
We consider a game of persuasion with evidence between a sender and a receiver. The sender has private information. By presenting evidence on the information, the sender wishes to persuade the receiver to take a single action (e.g., hire a job candidate, or convict a defendant). The sender’s utility depends solely on whether or not the receiver takes the action. The receiver’s utility depends on both the action as well as the sender’s private information. We study three natural variations. First, we consider sequential equilibria of the game without commitment power. Second, we consider a persuasion variant, where the sender commits to a signaling scheme and then the receiver, after seeing the evidence, takes the action or not. Third, we study a delegation variant, where the receiver first commits to taking the action if being presented certain evidence, and then the sender presents evidence to maximize the probability the action is taken. We study these variants through the computational lens, and give hardness results, optimal approximation algorithms, as well as polynomial-time algorithms for special cases. Among our results is an approximation algorithm that rounds a semidefinite program that might be of independent interest, since, to the best of our knowledge, it is the first such approximation algorithm for a natural problem in algorithmic economics.

Cite as

Martin Hoefer, Pasin Manurangsi, and Alexandros Psomas. Algorithmic Persuasion with Evidence. In 12th Innovations in Theoretical Computer Science Conference (ITCS 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 185, pp. 3:1-3:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)


Copy BibTex To Clipboard

@InProceedings{hoefer_et_al:LIPIcs.ITCS.2021.3,
  author =	{Hoefer, Martin and Manurangsi, Pasin and Psomas, Alexandros},
  title =	{{Algorithmic Persuasion with Evidence}},
  booktitle =	{12th Innovations in Theoretical Computer Science Conference (ITCS 2021)},
  pages =	{3:1--3:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-177-1},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{185},
  editor =	{Lee, James R.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ITCS.2021.3},
  URN =		{urn:nbn:de:0030-drops-135420},
  doi =		{10.4230/LIPIcs.ITCS.2021.3},
  annote =	{Keywords: Bayesian Persuasion, Semidefinite Programming, Approximation Algorithms}
}
Document
Even the Easiest(?) Graph Coloring Problem Is Not Easy in Streaming!

Authors: Anup Bhattacharya, Arijit Bishnu, Gopinath Mishra, and Anannya Upasana

Published in: LIPIcs, Volume 185, 12th Innovations in Theoretical Computer Science Conference (ITCS 2021)


Abstract
We study a graph coloring problem that is otherwise easy in the RAM model but becomes quite non-trivial in the one-pass streaming model. In contrast to previous graph coloring problems in streaming that try to find an assignment of colors to vertices, our main work is on estimating the number of conflicting or monochromatic edges given a coloring function that is streaming along with the graph; we call the problem Conflict-Est. The coloring function on a vertex can be read or accessed only when the vertex is revealed in the stream. If we need the color on a vertex that has streamed past, then that color, along with its vertex, has to be stored explicitly. We provide algorithms for a graph that is streaming in different variants of the vertex arrival in one-pass streaming model, viz. the Vertex Arrival (VA), Vertex Arrival With Degree Oracle (VAdeg), Vertex Arrival in Random Order (VArand) models, with special focus on the random order model. We also provide matching lower bounds for most of the cases. The mainstay of our work is in showing that the properties of a random order stream can be exploited to design efficient streaming algorithms for estimating the number of monochromatic edges. We have also obtained a lower bound, though not matching the upper bound, for the random order model. Among all the three models vis-a-vis this problem, we can show a clear separation of power in favor of the VArand model.

Cite as

Anup Bhattacharya, Arijit Bishnu, Gopinath Mishra, and Anannya Upasana. Even the Easiest(?) Graph Coloring Problem Is Not Easy in Streaming!. In 12th Innovations in Theoretical Computer Science Conference (ITCS 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 185, pp. 15:1-15:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)


Copy BibTex To Clipboard

@InProceedings{bhattacharya_et_al:LIPIcs.ITCS.2021.15,
  author =	{Bhattacharya, Anup and Bishnu, Arijit and Mishra, Gopinath and Upasana, Anannya},
  title =	{{Even the Easiest(?) Graph Coloring Problem Is Not Easy in Streaming!}},
  booktitle =	{12th Innovations in Theoretical Computer Science Conference (ITCS 2021)},
  pages =	{15:1--15:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-177-1},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{185},
  editor =	{Lee, James R.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ITCS.2021.15},
  URN =		{urn:nbn:de:0030-drops-135544},
  doi =		{10.4230/LIPIcs.ITCS.2021.15},
  annote =	{Keywords: Streaming, random ordering, graph coloring, estimation, lower bounds}
}
Document
Black-Box Uselessness: Composing Separations in Cryptography

Authors: Geoffroy Couteau, Pooya Farshim, and Mohammad Mahmoody

Published in: LIPIcs, Volume 185, 12th Innovations in Theoretical Computer Science Conference (ITCS 2021)


Abstract
Black-box separations have been successfully used to identify the limits of a powerful set of tools in cryptography, namely those of black-box reductions. They allow proving that a large set of techniques are not capable of basing one primitive 𝒫 on another 𝒬. Such separations, however, do not say anything about the power of the combination of primitives 𝒬₁,𝒬₂ for constructing 𝒫, even if 𝒫 cannot be based on 𝒬₁ or 𝒬₂ alone. By introducing and formalizing the notion of black-box uselessness, we develop a framework that allows us to make such conclusions. At an informal level, we call primitive 𝒬 black-box useless (BBU) for 𝒫 if 𝒬 cannot help constructing 𝒫 in a black-box way, even in the presence of another primitive 𝒵. This is formalized by saying that 𝒬 is BBU for 𝒫 if for any auxiliary primitive 𝒵, whenever there exists a black-box construction of 𝒫 from (𝒬,𝒵), then there must already also exist a black-box construction of 𝒫 from 𝒵 alone. We also formalize various other notions of black-box uselessness, and consider in particular the setting of efficient black-box constructions when the number of queries to 𝒬 is below a threshold. Impagliazzo and Rudich (STOC'89) initiated the study of black-box separations by separating key agreement from one-way functions. We prove a number of initial results in this direction, which indicate that one-way functions are perhaps also black-box useless for key agreement. In particular, we show that OWFs are black-box useless in any construction of key agreement in either of the following settings: (1) the key agreement has perfect correctness and one of the parties calls the OWF a constant number of times; (2) the key agreement consists of a single round of interaction (as in Merkle-type protocols). We conjecture that OWFs are indeed black-box useless for general key agreement. We also show that certain techniques for proving black-box separations can be lifted to the uselessness regime. In particular, we show that the lower bounds of Canetti, Kalai, and Paneth (TCC'15) as well as Garg, Mahmoody, and Mohammed (Crypto'17 & TCC'17) for assumptions behind indistinguishability obfuscation (IO) can be extended to derive black-box uselessness of a variety of primitives for obtaining (approximately correct) IO. These results follow the so-called "compiling out" technique, which we prove to imply black-box uselessness. Eventually, we study the complementary landscape of black-box uselessness, namely black-box helpfulness. We put forth the conjecture that one-way functions are black-box helpful for building collision-resistant hash functions. We define two natural relaxations of this conjecture, and prove that both of these conjectures are implied by a natural conjecture regarding random permutations equipped with a collision finder oracle, as defined by Simon (Eurocrypt'98). This conjecture may also be of interest in other contexts, such as amplification of hardness.

Cite as

Geoffroy Couteau, Pooya Farshim, and Mohammad Mahmoody. Black-Box Uselessness: Composing Separations in Cryptography. In 12th Innovations in Theoretical Computer Science Conference (ITCS 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 185, pp. 47:1-47:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)


Copy BibTex To Clipboard

@InProceedings{couteau_et_al:LIPIcs.ITCS.2021.47,
  author =	{Couteau, Geoffroy and Farshim, Pooya and Mahmoody, Mohammad},
  title =	{{Black-Box Uselessness: Composing Separations in Cryptography}},
  booktitle =	{12th Innovations in Theoretical Computer Science Conference (ITCS 2021)},
  pages =	{47:1--47:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-177-1},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{185},
  editor =	{Lee, James R.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ITCS.2021.47},
  URN =		{urn:nbn:de:0030-drops-135869},
  doi =		{10.4230/LIPIcs.ITCS.2021.47},
  annote =	{Keywords: Black-Box Reductions, Separations, One-Way Functions, Key Agreement}
}
Document
Computational Complexity of the Hylland-Zeckhauser Scheme for One-Sided Matching Markets

Authors: Vijay V. Vazirani and Mihalis Yannakakis

Published in: LIPIcs, Volume 185, 12th Innovations in Theoretical Computer Science Conference (ITCS 2021)


Abstract
In 1979, Hylland and Zeckhauser [Hylland and Zeckhauser, 1979] gave a simple and general scheme for implementing a one-sided matching market using the power of a pricing mechanism. Their method has nice properties - it is incentive compatible in the large and produces an allocation that is Pareto optimal - and hence it provides an attractive, off-the-shelf method for running an application involving such a market. With matching markets becoming ever more prevalent and impactful, it is imperative to finally settle the computational complexity of this scheme. We present the following partial resolution: 1) A combinatorial, strongly polynomial time algorithm for the dichotomous case, i.e., 0/1 utilities, and more generally, when each agent’s utilities come from a bi-valued set. 2) An example that has only irrational equilibria, hence proving that this problem is not in PPAD. 3) A proof of membership of the problem in the class FIXP. 4) A proof of membership of the problem of computing an approximate HZ equilibrium in the class PPAD. We leave open the (difficult) questions of determining if computing an exact HZ equilibrium is FIXP-hard and an approximate HZ equilibrium is PPAD-hard.

Cite as

Vijay V. Vazirani and Mihalis Yannakakis. Computational Complexity of the Hylland-Zeckhauser Scheme for One-Sided Matching Markets. In 12th Innovations in Theoretical Computer Science Conference (ITCS 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 185, pp. 59:1-59:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)


Copy BibTex To Clipboard

@InProceedings{vazirani_et_al:LIPIcs.ITCS.2021.59,
  author =	{Vazirani, Vijay V. and Yannakakis, Mihalis},
  title =	{{Computational Complexity of the Hylland-Zeckhauser Scheme for One-Sided Matching Markets}},
  booktitle =	{12th Innovations in Theoretical Computer Science Conference (ITCS 2021)},
  pages =	{59:1--59:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-177-1},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{185},
  editor =	{Lee, James R.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ITCS.2021.59},
  URN =		{urn:nbn:de:0030-drops-135987},
  doi =		{10.4230/LIPIcs.ITCS.2021.59},
  annote =	{Keywords: Hyland-Zeckhauser scheme, one-sided matching markets, mechanism design, dichotomous utilities, PPAD, FIXP}
}
Document
Quantitative Correlation Inequalities via Semigroup Interpolation

Authors: Anindya De, Shivam Nadimpalli, and Rocco A. Servedio

Published in: LIPIcs, Volume 185, 12th Innovations in Theoretical Computer Science Conference (ITCS 2021)


Abstract
Most correlation inequalities for high-dimensional functions in the literature, such as the Fortuin-Kasteleyn-Ginibre inequality and the celebrated Gaussian Correlation Inequality of Royen, are qualitative statements which establish that any two functions of a certain type have non-negative correlation. We give a general approach that can be used to bootstrap many qualitative correlation inequalities for functions over product spaces into quantitative statements. The approach combines a new extremal result about power series, proved using complex analysis, with harmonic analysis of functions over product spaces. We instantiate this general approach in several different concrete settings to obtain a range of new and near-optimal quantitative correlation inequalities, including: - A {quantitative} version of Royen’s celebrated Gaussian Correlation Inequality [Royen, 2014]. In [Royen, 2014] Royen confirmed a conjecture, open for 40 years, stating that any two symmetric convex sets must be non-negatively correlated under any centered Gaussian distribution. We give a lower bound on the correlation in terms of the vector of degree-2 Hermite coefficients of the two convex sets, conceptually similar to Talagrand’s quantitative correlation bound for monotone Boolean functions over {0,1}ⁿ [M. Talagrand, 1996]. We show that our quantitative version of Royen’s theorem is within a logarithmic factor of being optimal. - A quantitative version of the well-known FKG inequality for monotone functions over any finite product probability space. This is a broad generalization of Talagrand’s quantitative correlation bound for functions from {0,1}ⁿ to {0,1} under the uniform distribution [M. Talagrand, 1996]; the only prior generalization of which we are aware is due to Keller [Nathan Keller, 2012; Keller, 2008; Nathan Keller, 2009], which extended [M. Talagrand, 1996] to product distributions over {0,1}ⁿ. In the special case of p-biased distributions over {0,1}ⁿ that was considered by Keller, our new bound essentially saves a factor of p log(1/p) over the quantitative bounds given in [Nathan Keller, 2012; Keller, 2008; Nathan Keller, 2009]. We also give {a quantitative version of} the FKG inequality for monotone functions over the continuous domain [0,1]ⁿ, answering a question of Keller [Nathan Keller, 2009].

Cite as

Anindya De, Shivam Nadimpalli, and Rocco A. Servedio. Quantitative Correlation Inequalities via Semigroup Interpolation. In 12th Innovations in Theoretical Computer Science Conference (ITCS 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 185, pp. 69:1-69:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)


Copy BibTex To Clipboard

@InProceedings{de_et_al:LIPIcs.ITCS.2021.69,
  author =	{De, Anindya and Nadimpalli, Shivam and Servedio, Rocco A.},
  title =	{{Quantitative Correlation Inequalities via Semigroup Interpolation}},
  booktitle =	{12th Innovations in Theoretical Computer Science Conference (ITCS 2021)},
  pages =	{69:1--69:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-177-1},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{185},
  editor =	{Lee, James R.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ITCS.2021.69},
  URN =		{urn:nbn:de:0030-drops-136081},
  doi =		{10.4230/LIPIcs.ITCS.2021.69},
  annote =	{Keywords: complex analysis, correlation inequality, FKG inequality, Gaussian correlation inequality, harmonic analysis, Markov semigroups}
}
Document
Message Complexity of Population Protocols

Authors: Talley Amir, James Aspnes, David Doty, Mahsa Eftekhari, and Eric Severson

Published in: LIPIcs, Volume 179, 34th International Symposium on Distributed Computing (DISC 2020)


Abstract
The standard population protocol model assumes that when two agents interact, each observes the entire state of the other. We initiate the study of message complexity for population protocols, where an agent’s state is divided into an externally-visible message and externally-hidden local state. We consider the case of O(1) message complexity. When time is unrestricted, we obtain an exact characterization of the stably computable predicates based on the number of internal states s(n): If s(n) = o(n) then the protocol computes semilinear predicates (unlike the original model, which can compute non-semilinear predicates with s(n) = O(log n)), and otherwise it computes a predicate decidable by a nondeterministic O(n log s(n))-space-bounded Turing machine. We then introduce novel O(polylog(n)) expected time protocols for junta/leader election and general purpose broadcast correct with high probability, and approximate and exact population size counting correct with probability 1. Finally, we show that the main constraint on the power of bounded-message-size protocols is the size of the internal states: with unbounded internal states, any computable function can be computed with probability 1 in the limit by a protocol that uses only 1-bit messages.

Cite as

Talley Amir, James Aspnes, David Doty, Mahsa Eftekhari, and Eric Severson. Message Complexity of Population Protocols. In 34th International Symposium on Distributed Computing (DISC 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 179, pp. 6:1-6:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)


Copy BibTex To Clipboard

@InProceedings{amir_et_al:LIPIcs.DISC.2020.6,
  author =	{Amir, Talley and Aspnes, James and Doty, David and Eftekhari, Mahsa and Severson, Eric},
  title =	{{Message Complexity of Population Protocols}},
  booktitle =	{34th International Symposium on Distributed Computing (DISC 2020)},
  pages =	{6:1--6:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-168-9},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{179},
  editor =	{Attiya, Hagit},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.DISC.2020.6},
  URN =		{urn:nbn:de:0030-drops-130848},
  doi =		{10.4230/LIPIcs.DISC.2020.6},
  annote =	{Keywords: population protocol, message complexity, space-optimal}
}
Document
Track B: Automata, Logic, Semantics, and Theory of Programming
On Polynomial Recursive Sequences

Authors: Michaël Cadilhac, Filip Mazowiecki, Charles Paperman, Michał Pilipczuk, and Géraud Sénizergues

Published in: LIPIcs, Volume 168, 47th International Colloquium on Automata, Languages, and Programming (ICALP 2020)


Abstract
We study the expressive power of polynomial recursive sequences, a nonlinear extension of the well-known class of linear recursive sequences. These sequences arise naturally in the study of nonlinear extensions of weighted automata, where (non)expressiveness results translate to class separations. A typical example of a polynomial recursive sequence is b_n = n!. Our main result is that the sequence u_n = nⁿ is not polynomial recursive.

Cite as

Michaël Cadilhac, Filip Mazowiecki, Charles Paperman, Michał Pilipczuk, and Géraud Sénizergues. On Polynomial Recursive Sequences. In 47th International Colloquium on Automata, Languages, and Programming (ICALP 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 168, pp. 117:1-117:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)


Copy BibTex To Clipboard

@InProceedings{cadilhac_et_al:LIPIcs.ICALP.2020.117,
  author =	{Cadilhac, Micha\"{e}l and Mazowiecki, Filip and Paperman, Charles and Pilipczuk, Micha{\l} and S\'{e}nizergues, G\'{e}raud},
  title =	{{On Polynomial Recursive Sequences}},
  booktitle =	{47th International Colloquium on Automata, Languages, and Programming (ICALP 2020)},
  pages =	{117:1--117:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-138-2},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{168},
  editor =	{Czumaj, Artur and Dawar, Anuj and Merelli, Emanuela},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2020.117},
  URN =		{urn:nbn:de:0030-drops-125240},
  doi =		{10.4230/LIPIcs.ICALP.2020.117},
  annote =	{Keywords: recursive sequences, expressive power, weighted automata, higher-order pushdown automata}
}
  • Refine by Author
  • 2 Worrell, James
  • 1 Abraham, Ittai
  • 1 Amir, Talley
  • 1 Aspnes, James
  • 1 Baryshnikov, Yuliy
  • Show More...

  • Refine by Classification
  • 3 Theory of computation → Design and analysis of algorithms
  • 3 Theory of computation → Distributed algorithms
  • 2 Computing methodologies → Algebraic algorithms
  • 2 Mathematics of computing → Stochastic processes
  • 2 Theory of computation → Logic and verification
  • Show More...

  • Refine by Keyword
  • 2 distributed algorithms
  • 1 Amoebots
  • 1 Analytic combinatorics
  • 1 Approximation Algorithms
  • 1 Automata
  • Show More...

  • Refine by Type
  • 28 document

  • Refine by Publication Year
  • 11 2021
  • 9 2018
  • 2 2020
  • 2 2023
  • 1 2005
  • Show More...

Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail