Ptime canonization for two variables with counting

We consider infinitary logic with two variable symbols and counting quantifiers, C², and its intersection with PTIME on finite relational structures. In particular we exhibit a PTIME canonization procedure for finite relational structures which provides unique representatives up to equivalence in C². As a consequence we obtain a recursive presentation for the class of all those queries on arbitrary finite relational structures which are both PTIME and definable in C². The proof renders a succinct normal form representation of this non-trivial semantically defined fragment of PTIME. Through specializations of the proof techniques similar results apply with respect to the logic L², infinitary logic with two variable symbols, itself