+**********************************************************************
*
*
*                          Einladung
*
*
*
*                     Informatik-Oberseminar
*
*
*
+**********************************************************************

Zeit:  Mittwoch, 12. Juli 2023, 11:00 Uhr

Ort: Informatikzentrum der RWTH Aachen University, Gebäude E3, 2. Etage, Raum 9222

Referent: Benedikt Pago, M.Sc.
          Mathematische Grundlagen der Informatik

Thema: Limitations of Choiceless Computation

Abstract:

A central open question in finite model theory asks whether there exists a logic that captures the complexity class PTIME. 
Another way of phrasing this is whether every polynomial time algorithm can be efficiently simulated by a choiceless one. 
Choiceless computation models operate on finite structures, such as graphs, and can only perform computation steps which are invariant under
the symmetries of the structure. This guarantees that for any two isomorphic input structures, the outcome of the computation is the same - 
a property which is typically required of logics.
The quest for a logic for PTIME seeks to develop and analyse logics (i.e. choiceless computation models) of increasing expressive power 
within PTIME. One of the most prominent logics that has been suggested and not separated from PTIME within more than 20 years is 
Choiceless Polynomial Time (CPT). Obtaining a better understanding of its expressive power is the aim of this thesis; 
the focus is on its limitations, since only little is known so far in this regard. 

We develop new approaches and techniques towards strong CPT lower bounds. As a promising candidate for separating CPT from PTIME, we propose 
the graph isomorphism problem on Cai-Fürer-Immerman (CFI) graphs over unordered hypercubes. The CFI construction is a well-known tool to prove 
inexpressibility results for logics. Choiceless polynomial time algorithms are known to exist for certain ordered variants of it but we show 
that these fail on unordered CFI graphs. Going further, we study a broader class of CPT-algorithms for this problem and prove that
lower bounds against certain families of symmetric Boolean circuits imply lower bounds for these algorithms. A first lower bound for this kind
of circuits is also presented to demonstrate the feasibility of the approach. It remains open to strengthen it further to get the desired
undefinability result for the CFI problem in CPT.


As an alternative route, we establish a connection to an algebraic proof system called the extended polynomial calculus. 
The power of this and similar proof systems is the subject of active research in the field of proof complexity. We show that suitable proof 
complexity lower bounds would imply the separation of CPT and PTIME, too.


 
Es laden ein: die Dozentinnen und Dozenten der Informatik