Characterizing co-NL by a Group Action

In a recent paper (Girard 2011b), Girard uses the geometry of interaction in the hyperfinite factor (Girard 2011a) in an innovative way to characterize complexity classes. The purpose of this paper is two-fold: to give a detailed explanation of both the choices and the motivations of Girard's definitions, and -since Girard's paper skips over some non-trivial details and only sketches one half of the proof -to provide a complete proof that co-NL can be characterized by an action of the group of finite permutations. We introduce as a technical tool the non-deterministic pointer machine, a concrete model that computes the algorithms represented in this setting