5 Search Results for "Nowak, David"

Document
Track A: Algorithms, Complexity and Games
DOI: 10.4230/LIPIcs.ICALP.2022.94
Listing, Verifying and Counting Lowest Common Ancestors in DAGs: Algorithms and Fine-Grained Lower Bounds

Authors: Surya Mathialagan, Virginia Vassilevska Williams, and Yinzhan Xu

Published in: LIPIcs, Volume 229, 49th International Colloquium on Automata, Languages, and Programming (ICALP 2022)

Abstract
The AP-LCA problem asks, given an n-node directed acyclic graph (DAG), to compute for every pair of vertices u and v in the DAG a lowest common ancestor (LCA) of u and v if one exists, i.e. a node that is an ancestor of both u and v but no proper descendent of it is their common ancestor. Recently [Grandoni et al. SODA'21] obtained the first sub-n^{2.5} time algorithm for AP-LCA running in O(n^{2.447}) time. Meanwhile, the only known conditional lower bound for AP-LCA is that the problem requires n^{ω-o(1)} time where ω is the matrix multiplication exponent. In this paper we study several interesting variants of AP-LCA, providing both algorithms and fine-grained lower bounds for them. The lower bounds we obtain are the first conditional lower bounds for LCA problems higher than n^{ω-o(1)}. Some of our results include: - In any DAG, we can detect all vertex pairs that have at most two LCAs and list all of their LCAs in O(n^ω) time. This algorithm extends a result of [Kowaluk and Lingas ESA'07] which showed an Õ(n^ω) time algorithm that detects all pairs with a unique LCA in a DAG and outputs their corresponding LCAs. - Listing 7 LCAs per vertex pair in DAGs requires n^{3-o(1)} time under the popular assumption that 3-uniform 5-hyperclique detection requires n^{5-o(1)} time. This is surprising since essentially cubic time is sufficient to list all LCAs (if ω = 2). - Counting the number of LCAs for every vertex pair in a DAG requires n^{3-o(1)} time under the Strong Exponential Time Hypothesis, and n^{ω(1,2,1)-o(1)} time under the 4-Clique hypothesis. This shows that the algorithm of [Echkardt, Mühling and Nowak ESA'07] for listing all LCAs for every pair of vertices is likely optimal. - Given a DAG and a vertex w_{u,v} for every vertex pair u,v, verifying whether all w_{u,v} are valid LCAs requires n^{2.5-o(1)} time assuming 3-uniform 4-hyperclique requires n^{4-o(1)} time. This defies the common intuition that verification is easier than computation since returning some LCA per vertex pair can be solved in O(n^{2.447}) time.
Cite as

Surya Mathialagan, Virginia Vassilevska Williams, and Yinzhan Xu. Listing, Verifying and Counting Lowest Common Ancestors in DAGs: Algorithms and Fine-Grained Lower Bounds. In 49th International Colloquium on Automata, Languages, and Programming (ICALP 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 229, pp. 94:1-94:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{mathialagan_et_al:LIPIcs.ICALP.2022.94,
  author =	{Mathialagan, Surya and Vassilevska Williams, Virginia and Xu, Yinzhan},
  title =	{{Listing, Verifying and Counting Lowest Common Ancestors in DAGs: Algorithms and Fine-Grained Lower Bounds}},
  booktitle =	{49th International Colloquium on Automata, Languages, and Programming (ICALP 2022)},
  pages =	{94:1--94:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-235-8},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{229},
  editor =	{Boja\'{n}czyk, Miko{\l}aj and Merelli, Emanuela and Woodruff, David P.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2022.94},
  URN =		{urn:nbn:de:0030-drops-164359},
  doi =		{10.4230/LIPIcs.ICALP.2022.94},
  annote =	{Keywords: All-Pairs Lowest Common Ancestor, Fine-Grained Complexity}
}
Document
Artifact
DOI: 10.4230/DARTS.8.2.2
Defining Corecursive Functions in Coq Using Approximations (Artifact)

Authors: Vlad Rusu and David Nowak

Published in: DARTS, Volume 8, Issue 2, Special Issue of the 36th European Conference on Object-Oriented Programming (ECOOP 2022)

Abstract
This is the formalization in the Coq proof assistant of the related conference article shown below.
Cite as

Vlad Rusu and David Nowak. Defining Corecursive Functions in Coq Using Approximations (Artifact). In Special Issue of the 36th European Conference on Object-Oriented Programming (ECOOP 2022). Dagstuhl Artifacts Series (DARTS), Volume 8, Issue 2, pp. 2:1-2:2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@Article{rusu_et_al:DARTS.8.2.2,
  author =	{Rusu, Vlad and Nowak, David},
  title =	{{Defining Corecursive Functions in Coq Using Approximations (Artifact)}},
  pages =	{2:1--2:2},
  journal =	{Dagstuhl Artifacts Series},
  ISSN =	{2509-8195},
  year =	{2022},
  volume =	{8},
  number =	{2},
  editor =	{Rusu, Vlad and Nowak, David},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/DARTS.8.2.2},
  URN =		{urn:nbn:de:0030-drops-162001},
  doi =		{10.4230/DARTS.8.2.2},
  annote =	{Keywords: corecursive function, productiveness, approximation, Coq proof assistant.}
}
Document
DOI: 10.4230/LIPIcs.ECOOP.2022.12
Defining Corecursive Functions in Coq Using Approximations

Authors: Vlad Rusu and David Nowak

Published in: LIPIcs, Volume 222, 36th European Conference on Object-Oriented Programming (ECOOP 2022)

Abstract
We present two methods for defining corecursive functions that go beyond what is accepted by the builtin corecursion mechanisms of the Coq proof assistant. This gain in expressiveness is obtained by using a combination of axioms from Coq’s standard library that, to our best knowledge, do not introduce inconsistencies but enable reasoning in standard mathematics. Both methods view corecursive functions as limits of sequences of approximations, and both are based on a property of productiveness that, intuitively, requires that for each input, an arbitrarily close approximation of the corresponding output is eventually obtained. The first method uses Coq’s builtin corecursive mechanisms in a non-standard way, while the second method uses none of the mechanisms but redefines them. Both methods are implemented in Coq and are illustrated with examples.
Cite as

Vlad Rusu and David Nowak. Defining Corecursive Functions in Coq Using Approximations. In 36th European Conference on Object-Oriented Programming (ECOOP 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 222, pp. 12:1-12:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{rusu_et_al:LIPIcs.ECOOP.2022.12,
  author =	{Rusu, Vlad and Nowak, David},
  title =	{{Defining Corecursive Functions in Coq Using Approximations}},
  booktitle =	{36th European Conference on Object-Oriented Programming (ECOOP 2022)},
  pages =	{12:1--12:24},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-225-9},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{222},
  editor =	{Ali, Karim and Vitek, Jan},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2022.12},
  URN =		{urn:nbn:de:0030-drops-162407},
  doi =		{10.4230/LIPIcs.ECOOP.2022.12},
  annote =	{Keywords: corecursive function, productiveness, approximation, Coq proof assistant}
}
Document
DOI: 10.4230/LIPIcs.TYPES.2020.2
Extending Equational Monadic Reasoning with Monad Transformers

Authors: Reynald Affeldt and David Nowak

Published in: LIPIcs, Volume 188, 26th International Conference on Types for Proofs and Programs (TYPES 2020)

Abstract
There is a recent interest for the verification of monadic programs using proof assistants. This line of research raises the question of the integration of monad transformers, a standard technique to combine monads. In this paper, we extend Monae, a Coq library for monadic equational reasoning, with monad transformers and we explain the benefits of this extension. Our starting point is the existing theory of modular monad transformers, which provides a uniform treatment of operations. Using this theory, we simplify the formalization of models in Monae and we propose an approach to support monadic equational reasoning in the presence of monad transformers. We also use Monae to revisit the lifting theorems of modular monad transformers by providing equational proofs and explaining how to patch a known bug using a non-standard use of Coq that combines impredicative polymorphism and parametricity.
Cite as

Reynald Affeldt and David Nowak. Extending Equational Monadic Reasoning with Monad Transformers. In 26th International Conference on Types for Proofs and Programs (TYPES 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 188, pp. 2:1-2:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{affeldt_et_al:LIPIcs.TYPES.2020.2,
  author =	{Affeldt, Reynald and Nowak, David},
  title =	{{Extending Equational Monadic Reasoning with Monad Transformers}},
  booktitle =	{26th International Conference on Types for Proofs and Programs (TYPES 2020)},
  pages =	{2:1--2:21},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-182-5},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{188},
  editor =	{de'Liguoro, Ugo and Berardi, Stefano and Altenkirch, Thorsten},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2020.2},
  URN =		{urn:nbn:de:0030-drops-138810},
  doi =		{10.4230/LIPIcs.TYPES.2020.2},
  annote =	{Keywords: monads, monad transformers, Coq, impredicativity, parametricity}
}
Document
DOI: 10.4230/LIPIcs.ICALP.2016.62
Amplifiers for the Moran Process

Authors: Andreas Galanis, Andreas Göbel, Leslie Ann Goldberg, John Lapinskas, and David Richerby

Published in: LIPIcs, Volume 55, 43rd International Colloquium on Automata, Languages, and Programming (ICALP 2016)

Abstract
The Moran process, as studied by Lieberman, Hauert and Nowak, is a randomised algorithm modelling the spread of genetic mutations in populations. The algorithm runs on an underlying graph where individuals correspond to vertices. Initially, one vertex (chosen uniformly at random) possesses a mutation, with fitness r > 1. All other individuals have fitness 1. During each step of the algorithm, an individual is chosen with probability proportional to its fitness, and its state (mutant or non-mutant) is passed on to an out-neighbour which is chosen uniformly at random. If the underlying graph is strongly connected then the algorithm will eventually reach fixation, in which all individuals are mutants, or extinction, in which no individuals are mutants. An infinite family of directed graphs is said to be strongly amplifying if, for every r > 1, the extinction probability tends to 0 as the number of vertices increases. Strong amplification is a rather surprising property - it means that in such graphs, the fixation probability of a uniformly-placed initial mutant tends to 1 even though the initial mutant only has a fixed selective advantage of r > 1 (independently of n). The name "strongly amplifying" comes from the fact that this selective advantage is "amplified". Strong amplifiers have received quite a bit of attention, and Lieberman et al. proposed two potentially strongly-amplifying families - superstars and metafunnels. Heuristic arguments have been published, arguing that there are infinite families of superstars that are strongly amplifying. The same has been claimed for metafunnels. We give the first rigorous proof that there is an infinite family of directed graphs that is strongly amplifying. We call the graphs in the family "megastars". When the algorithm is run on an n-vertex graph in this family, starting with a uniformly-chosen mutant, the extinction probability is roughly n^{-1/2} (up to logarithmic factors). We prove that all infinite families of superstars and metafunnels have larger extinction probabilities (as a function of n). Finally, we prove that our analysis of megastars is fairly tight - there is no infinite family of megastars such that the Moran algorithm gives a smaller extinction probability (up to logarithmic factors). Also, we provide a counterexample which clarifies the literature concerning the isothermal theorem of Lieberman et al. A full version [Galanis/Göbel/Goldberg/Lapinskas/Richerby, Preprint] containing detailed proofs is available at http://arxiv.org/abs/1512.05632. Theorem-numbering here matches the full version.
Cite as

Andreas Galanis, Andreas Göbel, Leslie Ann Goldberg, John Lapinskas, and David Richerby. Amplifiers for the Moran Process. In 43rd International Colloquium on Automata, Languages, and Programming (ICALP 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 55, pp. 62:1-62:13, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@InProceedings{galanis_et_al:LIPIcs.ICALP.2016.62,
  author =	{Galanis, Andreas and G\"{o}bel, Andreas and Goldberg, Leslie Ann and Lapinskas, John and Richerby, David},
  title =	{{Amplifiers for the Moran Process}},
  booktitle =	{43rd International Colloquium on Automata, Languages, and Programming (ICALP 2016)},
  pages =	{62:1--62:13},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-013-2},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{55},
  editor =	{Chatzigiannakis, Ioannis and Mitzenmacher, Michael and Rabani, Yuval and Sangiorgi, Davide},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2016.62},
  URN =		{urn:nbn:de:0030-drops-62227},
  doi =		{10.4230/LIPIcs.ICALP.2016.62},
  annote =	{Keywords: Moran process, randomised algorithm on graphs, evolutionary dynamics}
}
  • Refine by Author
  • 3 Nowak, David
  • 2 Rusu, Vlad
  • 1 Affeldt, Reynald
  • 1 Galanis, Andreas
  • 1 Goldberg, Leslie Ann
  • Show More...

  • Refine by Classification
  • 2 Theory of computation → Functional constructs
  • 1 Software and its engineering → Formal software verification
  • 1 Theory of computation → Graph algorithms analysis
  • 1 Theory of computation → Logic and verification

  • Refine by Keyword
  • 2 approximation
  • 2 corecursive function
  • 2 productiveness
  • 1 All-Pairs Lowest Common Ancestor
  • 1 Coq
  • Show More...

  • Refine by Type
  • 5 document

  • Refine by Publication Year
  • 3 2022
  • 1 2016
  • 1 2021

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
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact