Thomas Seiller (DIKU, Univ. Copenhagen), Towards a geometric theory of computation(al complexity)

Programme

Résumé

The purpose of this talk is to explain a new approach to complexity theory based on (dynamic) semantics of linear logic, whose aim is to enable techniques and invariants from ergodic theory (e.g. l^2-Betti numbers of a countable Borel equivalence relation) to be used in computational complexity.

The origins of the techniques can be traced to Girard's “geometry of interaction” (GoI) program using von Neumann algebras and the recent GoI-inspired results in complexity. However, this approach reaches its full strength when using the more combinatorial setting of Interaction Graphs models of (fragments of) linear logic. Using techniques akin to game semantics (with a bit of measure theory), we are able to characterise (predicate) complexity classes as the set of programs/proofs interpretations of type Pred[m] := Nat ⇒ Bool. These models are parametrised by a group of measure-preserving maps m (equivalently, by a measurable group action) and provide the first sketches of a conjectured correspondence between measurable group/monoid actions and complexity constraints.