Formalizing Monoid Programs in CircuitComp/CSLib

Stream: CSLib

[Anvit Aggarwal]

Hi, I am interested in formalising circuit complexity theory in Lean and contributing to CSLib. I am doing a Bachelor's project under Prof Balagopal Komarath, a complexity theory researcher at my college (IIT Gandhinagar), on this subject.

I am thinking of formalising a lemma from Heribert Vollmer's Introduction to Circuit Complexity that relates bounded-width branching programs to M-programs over finite Monoids.
The exact statement given in Vollmer is the following:

Let A ⊆ {0,1}*.
There is a family of bounded-width branching programs P of polynomial size
that computes $c_A$ if and only if
there is a finite monoid M, a set F ⊆ M,
and an M-program P' of polynomial size such that A = L(P', F)

I would like to know whether this would be a good contribution to CSLib. I would especially appreciate @Alex Meiburg's view on whether this would be a good addition to his work at CircuitComp.

[Alex Meiburg]

This would be very appropriate and I would appreciate it. :) My repo has a definition of monoid programs (I called them BarringtonProgram, which is another name I've seen in the literature), and I have the conversion from a BarringtonProgram to LayeredBranchingProgram as it works for symmetric groups (which gives a smaller width than the obvious construction for other monoids).

The statement you wrote is slightly stronger, because you allow different (I assume) accepting sets F. So this would be a good stronger thing to have.

The other direction (forward of your implication), that a bounded-width branching program can be converted back to a monoid program, could go "directly" or via the NC0 compilation, which is something I've been looking at doing a bit. I think it would be good.

[Alex Meiburg]

The reverse direction, I think, can be stated in an appropriately general way that gets you the width-5 necessary for Barrington's theorem while also getting you your statement for any arbitrary monoid.

If you have a monoid M with a faithful action on a set S, and then accepting set F of S, then you can get a branching program of width |S|. So for any monoid you can have its own action on itself, for a branching program of width |M|. For the symmetric group S_n, it acts on Fin n, so you get a branching program of width n.

[Alex Meiburg]

This doesn't actually require it to be a monoid at all then.