[Facets-of-complexity] Invitation & Link to Monday Lecture & Colloquium - June 28 2021.

[Ita Brunke <i.brunke@inf.fu-berlin.de>]

You are cordially invited to our next Monday Lecture & Colloquium on June 28 th.

Time is back to normal. 

Monday's Lecture & Colloquium will be online via Zoom, as used to.

Invitation link:
https://tu-berlin.zoom.us/j/69716124232?pwd=dzFlcTFHMmFXRTE5QmZLaEV5N0FRUT09
No password is required.

Online via:
Zoom - Invitation

Time: Monday, June 28th - 14:15 h

Lecture: Xavier Allamigeon (Inria and Ecole Polytechnique)

Title: Formalizing the theory of polyhedra in a proof assistant

Abstract:

In this talk, I will present the project Coq-Polyhedra that aims at formalizing the theory of polyhedra as well as polyhedral computations in the proof assistant Coq.
I will explain how the intuitionistic nature of the logic of a proof assistant like Coq requires to define basic properties of polyhedra in a quite different way than is usually done, by relying on a formal proof of the simplex method. I will also focus on the formalization of the faces of polyhedra, and present a mechanism which automatically introduces an appropriate representation of a polyhedron or a face, depending on the context of the proof. I will 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, as well as Balinski’s theorem on the d-connectedness of the graph of d-polytopes. Finally, I will discuss recent progress on the formal computation of the graph of a polytope directly within the proof assistant, thanks to a certified algorithm that checks a posteriori the output of Avis’ vertex enumeration library lrslib.
Joint work with Quentin Canu, Ricardo D. Katz and Pierre-Yves Strub.

Coffee Break!

Time: Monday, June 28th - 16:00 h s.t.

Colloquium: Gorav Jindal (Technische Universität Berlin)

Title: Arithmetic Circuit Complexity of Division and Truncation

Abstract:

Given n-variate polynomials f,g,h such that f=g/h, where both g and h are computable by arithmetic circuits of size s, we show that f can be computed by a circuit of size poly(s, deg(h)). This solves a special case of division elimination for high-degree circuits (Kaltofen’87 & WACT’16). This result is an exponential improvement over Strassen’s classic result (Strassen’73) when deg(h) is poly(s) and deg(f) is exp(s), since the latter gives an upper bound of poly(s, deg(f)).
The second part of this work deals with the complexity of computing the truncations of uni-variate polynomials or power series. We first show that the truncations of rational functions are easy to compute.  We also prove that the truncations of even very simple algebraic functions are hard to compute,unless integer factoring is easy.
This is a joint work with Pranjal Dutta, Anurag Pandey and Amit Sinhababu. A pre-print can be found at https://eccc.weizmann.ac.il/report/2021/072/ .