Parity is not in AC0

Stream: CSLib

[Alex Meiburg]

Although not directly part of CS Lib, I have a result I think people here might be interested in: over at CircuitComp I now have a Lean proof that Parity is not in AC0. :) :tada:

I think this is the first nontrivial tractability result proved in Lean; with the noncomputability of the Halting problem as (imo) the otherwise most nontrivial complexity-theory result. (There may be other big ones I don't know about -- but we all know how fully end-to-end complexity theory is really hard to formalize...!)

[Alex Meiburg]

In particular I went for this because Turing machines (and their complexity classes) are such a pain, but circuit complexity could be a bit more accessible in this regard.

[Alex Meiburg]

There's still a lot of missing "helpful" facts to make working with circuits more reasonable. A few things I'd like to do:

• NCi (and similar classes) are unchanged by adding any finite set of gates
• So it's obvious that NCi is in ACi, but showing that ACi is in NC_{i+1}, and so NC=AC. I already have that NC1 can compute AND, so it's a matter of setting up appropriate "substitution" of gates (like the above)
• More stuff about composing/substituting circuits

Right now the only definition of circuit is a "layered" circuit where each layer only talks to the previous one. There's other natural logically equivalent structures, like a list of gates where each can refer to any previous gates (and then depth is the maximum length path, etc.), or a layered circuit with skip connections. It would be good to define these and show the natural equivalences.

[Chris Henson]

This looks really interesting! I think it would be great to get a definition of circuit in CSLib, as this has previously come up with someone who was working on Barrington's theorem, and I see you have some work on NC. I would be happy to review any PRs more closely.

[Snir Broshi]

This is amazing!
Regarding the definition, I think it should use docs#Digraph with a [Finite V] and G.IsAcyclic assumptions, plus V → operation and a proof that degrees match operation arity. If we need non-commutative operations (e.g. arithmetic circuits use exponentiation), maybe add (v : V) → { l // G.neighborFinset.toList.Perm l } or something.
(this requires a few Mathlib PRs to beef up Digraph, adding Digraph.IsAcyclic/Digraph.degree/Digraph.neighborFinset to match the existing SimpleGraph definitions)

[Shreyas Srinivas]

Ah this is an interesting way of dealing with circuits. I have been trying to make them work as an inductive type.

[Shreyas Srinivas]

This creates a more general definition but comes at the cost of needing binders to allow out nodes with out degree > 1

[Shreyas Srinivas]

Btw I think it’s just a typo in your message but you probably want to show AC (i) is in NC (i + 1)

[Alex Meiburg]

Shreyas Srinivas said:

Btw I think it’s just a typo in your message but you probably want to show AC (i) is in NC (i + 1)

Aha yes, fixed

[Alex Meiburg]

Shreyas Srinivas said:

This creates a more general definition but comes at the cost of needing binders to allow out nodes with out degree > 1

By out degree you mean a node that computes multiple outputs, like divMod returning two numbers?

[Shreyas Srinivas]

No. In circuit complexity (both boolean and arithmetic), there is a distinction between circuits and formulas. Formulas are trees. Circuits can be DAGs, where a node can provide its output to multiple inputs

[Shreyas Srinivas]

This can make a difference when you are computing size

[Shreyas Srinivas]

An AC0 circuit, which is polynomial size can unfold into an exponential sized formula

[Alex Meiburg]

Yes I'm aware of that, and mine is for circuits, so arbitrary out degree

[Alex Meiburg]

.. Oh! You were saying you have an inductive definition, but it really captures formulas, not circuits. I see, I had misunderstood your message. Makes sense now

[Shreyas Srinivas]

It can capture circuits if we allow metavariables that have to be mapped to circuits

[Shreyas Srinivas]

That just means we have to write substitution. But then you have recursive circuit constructions, so you also have to add recursion

[Shreyas Srinivas]

Btw, how do you construct explicit circuits?

[Alex Meiburg]

At the moment, I give an explicit listing of layers + gates + what their inputs are. It's pretty unwieldly for anything nontrivial, really. I think the better way will be once we have more defs that give ways about modifying or composing circuits. At the moment I have comp, which lets you stack one circuit on top of another, and sum, which lets you run two circuits "in parallel". The main other thing would be substitution, letting you plug in a circuit implementing a gate G1 in terms of gates G0 into another circuit with G0 and G1, in order to get a new circuit with gates only in G1. And then reason about how this affects the depth/width/size of the circuit. With those three primitives I think we could then start proving increasingly more interesting circuits can be built at some size. Sort of like how there's a whole bunch of functions in Mathlib proven to be Nat.Primrec, and it's pretty easy to build them up now to show new ones. (Like, a proof that primality testing is in Primrec would be pretty easy; correspondingly, I would like a world where a proof that primality testing is in coNP/poly should be just a few lines to build up.)

[Alex Meiburg]

Mm, one issue with this definition of circuit is that all wires are of the same type. So you could have an arithmetic circuit with Nat or Int wires just fine, and then you could imagine a substitution-type method that "compiles" that arithmetic circuit down to a Bool circuit with some effective bounds on the sizes of the numbers involved. You could also use this kind of definition to talk about, for instance, a neural network structure, in a reasonable way.

But this definition I have right now doesn't support talking about a circuit with mixed data types, like some Nat wires and some Real wires and some Bool wires.

[Shreyas Srinivas]

I think in your definition you will also find it difficult to do inductive proofs that would be trivial in an inductive type

[Alex Meiburg]

Can you give an example of what this inductive type would look like?

[Shreyas Srinivas]

inductive CTerm (α : Type u) (ID : Type v) where
  | CVar (x: ID) -- Circuit input nodes. important to keep separate.
  | BVar (n : ℕ)
  | Add (g h: CTerm α ID): CTerm α ID
  | Mult (g h: CTerm α ID): CTerm α ID
  | Neg (g : CTerm α ID): CTerm α ID
  | Const (c : α): CTerm α ID

[Shreyas Srinivas]

these were defined for arithmetic circuits of course

[Alex Meiburg]

Okay, so that's reflecting formulas then, yes?

Unless you end up defining "size" as some kind of minimization over identifying equal subterms together, but that sounds terrible

[Ching-Tsun Chou]

What is BVar?

[Shreyas Srinivas]

Bvar is an identifier for circuits

[Shreyas Srinivas]

And circuits are to be evaluated over a context.

[Shreyas Srinivas]

So when common sub circuits become an element of this context. They are supposed to be counted exactly once when size is computed.

[Ching-Tsun Chou]

How is a context expressed in Lean?

[Yuval Filmus]

I think this would be very awkward.
The standard solutions in the literature are visualizing the circuit as a labeled DAG, and thinking of it as a straight-line program (in our case, we can make the line numbers an arbitrary finite linear order).

[Shreyas Srinivas]

Just a heads up, I realised that we can use the cslib#275 approach to build boolean and arithmetic circuit complexity. I'll experiment a bit and post more here.

[Shreyas Srinivas]

The promised update is here:

In cslib#275 , specifically in CircuitProgs.lean I have written an example circuit type

[Shreyas Srinivas]

and I have instantiated it with a circuit on rationals and a circuit on Booleans. This can be used for circuit complexity on arbitrary circuit types

[Shreyas Srinivas]

But most interestingly for arithmetic and boolean circuit complexity

[Shreyas Srinivas]

This is all part of the query model framework.

[Shreyas Srinivas]

The trick to not double counting shared sub-circuits is to assign IDs to each circuit node as we create them, collect all the unique node IDs as a list, and compute its length. Currently this is happening manually, but I do wish there is a more elegant solution to automatically fitting node IDs into the circuit description, but I think this is an excellent start to both describing circuits and circuit complexity inside a monadic DSL

[Shreyas Srinivas]

Thanks to the custom cost structure, we get

1. A list of nodes in the circuit,
2. Its depth
3. Its size (which can be derived trivially from 1)

[Shreyas Srinivas]

I need to sleep now. But if there are questions and suggestions, I am glad to answer them in around 12 to 24 hours

[Shreyas Srinivas]

We definitely need a bunch of API lemmas for size fwiw.

[Chris Henson]

This remains a bit outside my expertise, but I am interested to see what @Alex Meiburg thinks of this approach. I think it might make sense to split this into its own PR until we understand if there are tradeoffs compared to the work Alex has done already. I don't want what seems like work heading in a productive direction to get slowed down by having too many directions from the onset. I think what will make this easiest to merge is if the initial scope of the first PR cleanly subsumes the existing modules using TimeM.

[Shreyas Srinivas]

So Alex represents a circuits as DAGs with explicit edges. In principle one can take this DSL and compile it to such a DAG by using a different model. One drawback in those DAGs is they are incredibly hard to use for constructing circuits explicitly. Another related drawback is that it is hard to perform induction on the formula structure in his method. Conversely, in my work, it is important to assign distinct IDs to nodes for counting size (although we do have a notion of IDs when we draw circuits on paper. We use complex labels).

[Shreyas Srinivas]

In addition to the implied advantages above, in my method, it is relatively trivial to do two things:

1. Construct explicit circuits.
2. Define uniform circuits upto a point. If we define a query type for TMs per a transition function, then this gets even more precise. We can then speak of DLOGTIME-uniform AC0

[Shreyas Srinivas]

Also since @Yuval Filmus has been doing complexity theory for more than a decade I am also hoping to hear this thoughts on this

[Yuval Filmus]

I think this is quite awkward.
Suppose that we want to show that the cost of computing f(x)^2 is at most one plus the cost of computing f(x).
It’s possible but not so convenient.

My preferred solution is straight line programs.
This also has the minor advantage of being able to accommodate multi-output gates.
One disadvantage is that defining depth (and in the arithmetic case, degree) becomes more awkward.

There are other computation models out there (many, in fact), for example branching programs.
They also seem more natural to encode using IDs for computation nodes.

As for formulas, it is more natural to use trees.
However, one can also define them by restricting the fan-out of nodes in a circuit.

[Yuval Filmus]

In addition, the set of gates could be a parameter in the general definition.

[Shreyas Srinivas]

So the circuit type I have defined is an example

[Shreyas Srinivas]

One can fit in almost any inductive type into this framework

[Yuval Filmus]

Not only circuits - also proofs (in proof complexity), where you have the analogs of both formulas and circuits (and less commonly, other objects).

[Shreyas Srinivas]

The key features that this example demonstrates are the following :

1. Using lean code (and therefore lean identifiers and lean functions including recursion) to define circuits

2.reduce one model to another by mapping their query types.

3. Compute size of a DAG even when it is a tree

[Shreyas Srinivas]

For proof complexity you can define a different query type

[Shreyas Srinivas]

This is a lightweight version of the meta model I once described to you. It can express them all an relations between them

[Yuval Filmus]

When reducing one model to another, we often use gadget reductions.
Also not uncommon is operations such as depth balancing.

[Shreyas Srinivas]

Also possible here. I’d even say a bit easier with inductive types

[Shreyas Srinivas]

Strictly speaking, an inductive circuit type (or even branching program) with node IDs is sufficient. What my examples show is how we can write them (including recursively defined circuits) right in lean.

[Yuval Filmus]

For your definition you need to verify another property - circuits with identical IDs coincide.

[Shreyas Srinivas]

Shreyas Srinivas said:

The promised update is here:

In cslib#275 , specifically in CircuitProgs.lean I have written an example circuit type

@Yuval Filmus : when you say you would prefer to just use lean program are you describing Alex’s method or the example I quoted above?

[Shreyas Srinivas]

Yuval Filmus said:

For your definition you need to verify another property - circuits with identical IDs coincide.

That’s true

[Shreyas Srinivas]

But I also think we could just carry it as an assumption in our theorem statements

[Yuval Filmus]

Not Lean programs, but straightline programs, which is one way in which circuits are understood in complexity theory.
We can describe a circuit as a sequence of instructions where each line can only use inputs and outputs from previous lines.

[Shreyas Srinivas]

Doesn’t my approach already fit that?

[Yuval Filmus]

I think it’s very awkward, since you have this condition that nodes with the same ID are identical.
You don’t need this in a straightline program.
One can ask whether we want to think of a straightline program as a list (perhaps with an additional ID field), which you evaluate inductively; or as a mapping from a partial order to instructions, which are constrained to only refer to preceding inputs (though some models allow circular circuits, at least in proof complexity).

[Yuval Filmus]

On the other hand, in some cases (branching programs, switching networks, comparator networks) we want to care about “layers”, which will be awkward in both models unless you add more structure to the ID.

[Shreyas Srinivas]

Adding structure to the ID is certainly possible. I picked natural numbers since they are the easiest to generate new IDs for

[Shreyas Srinivas]

The problem that a monadic DSL like this is solving is

1. Defining variable substitution, especially recursive ones
2. Defining a notion of functions or procedures.

[Shreyas Srinivas]

These are incredibly annoying parts of defining a deeply embedded DSL

[Shreyas Srinivas]

The specific representation of Circuits and IDs inside this monadic framework are very fungible

[Yuval Filmus]

Suppose you want to join two circuits together.
You can do it directly with natural numbers, but it’s a bit artificial.

[Shreyas Srinivas]

You would join them with one of the circuit’s gates right?

[Shreyas Srinivas]

See the second and third examples

[Shreyas Srinivas]

Or do you mean join them and share internal nodes?

[Yuval Filmus]

No, just join

[Chris Henson]

Shreyas Srinivas said:

The problem that a monadic DSL like this is solving is

1. Defining variable substitution, especially recursive ones
2. Defining a notion of functions or procedures.

These are incredibly annoying parts of defining a deeply embedded DSL

Maybe I am more comfortable because I have formalized enough lambda calculi, but I hope to encourage design decisions that do not unnecessarily shy away from binding. I do agree it requires a certain amount of careful setup. I am working on metaprogramming utilities to help in this area, but this is a longer term project.

[Shreyas Srinivas]

There is also the benefit of fitting circuit classes within the free monad framework by reductions

[Shreyas Srinivas]

The ID trick is orthogonal to this. It is simply a mechanism for keeping track of circuit nodes we have already counted in a recursive traversal of the inductive circuit type.

I would still like circuits to be inductive so that inductive proofs don’t become complicated for the kind of manipulations Yuval mentioned above. The only other way I see to make size not double count is to check each sub circuit for equality with every other sub circuit encountered so far.

[Shreyas Srinivas]

@Yuval Filmus : strictly speaking the condition is not “all nodes with the same ID are identical”. The circuit author assigns IDs manually. The correct claim is “all circuits with the same id are counted once collectively when computing the size of the circuit”

[Shreyas Srinivas]

You can always assign the same ID to different subcircuits. It doesn’t affect the correctness of what the circuit computes and the depth of the circuit.

[Yuval Filmus]

What prevents me from cheating, then?
I can use the same ID for all subcircuits.

[Shreyas Srinivas]

Nothing yet. Someone still has to read your spec to see what you label your nodes. I have pointed this out as something to be worked on. Maybe another monad.

[Shreyas Srinivas]

For example a state monad that keeps track of a counter and increments it each time to generate IDs it is used can ensure nobody cheats on Boolean or arithmetic circuits

[Shreyas Srinivas]

But for use cases where you want to use the same ID for different nodes, the option exists

[Shreyas Srinivas]

A stranger idea I had is to maintain a type theory like context and instead of the inductive type of circuits referring to other circuits recursively, they refer to valid IDs

[Shreyas Srinivas]

The problem there is getting recursive definitions.

[Shreyas Srinivas]

It’s basically like ngspice

[Shreyas Srinivas]

After some thinking, I believe this is what you mean by a line description.

[Alex Meiburg]

I dunno, I think this is not the most natural or ergonomic definition of circuits. (And, while there may be multiple good definitions of the same informal concept in Lean, they should either be natural or ergonomic.) I believe you that they might be natural for arithmetic circuit complexity, which I'm passingly familiar with but have never worked on myself. You say that it's easier to construct explicit examples of circuits, and this monadic DSL is nice, but I guess I'm not convinced that it's easy for the cases of interest to me (complexity theory -- as opposed to, say, constructing explicit circuits for a particular function).

[Alex Meiburg]

I've actually been working on branching programs a good bit locally, I have a proof of Barrington's Theorem, that width-5 oblivious BP's are equivalent to NC1.

[Alex Meiburg]

I'd also like to note that the inductive definition doesn't (obviously, to me) generalize to multiple-output circuits. So things like the class FNC or theorems like Uhlig's "mass production of Boolean functions" would seem very hard to get in that form.

[Alex Meiburg]

I think I'm increasingly of the opinion that it may be worth keeping a few different types around, which offer different options for constructions, and then we have the functions to move between them.

For circuits, we have one informal notion: a circuit.
Then there's a few different ways a mathematician might right down a definition (in English):

• A series of layers, which connect one to the next. (the one I linked at the top of this thread)
• A series of of layers, which each connect to any previous layer.
• A DAG
• An inductive construction, with some method of common subexpression elimination -- what you've been describing
• Straight-line-programs

And additionally all of these have two different conventions I'm aware of: do you start with the inputs to the circuit explicitly as the first n nodes? Or, can I add "fresh copies" of the input at later nodes? (A special type of "constant" gate that is always the ith input.)

[Alex Meiburg]

Personally, I believe the best outcome would be having all five of those bullet points as definitions. (I'm not sure about the second point). And then some functions to convert one to the other, and lemmas about how this conversion changes the depth/width/size/weft/etc.

[Alex Meiburg]

I was already running into this with branching programs, that some people really insist on branching programs being layered, and some insist on it being a DAG. And this matters, a lot actually! Because there's interest in what functions you can compute at particular constant widths (width-4 vs width-5) and then these subtle differences give you meaningfully different complexity classes.

[Alex Meiburg]

It's possible that you can take the first bullet point above as just a predicate about the second, but then the types can get messier when you talk about how to refer to earlier layers when you put it in Lean.

Similarly, a straight-line-program can be viewed as the special case of a layered circuit (with skips) where each layer is width 1. This is a correct definition, mathematically. But now the "depth" of your SLP is not what you would expect (the minimum depth over equivalent circuits), but rather the size of the circuit, so you get some extra headache.

For the reason, I think it's better to just keep them separate.

[Alex Meiburg]

I hope the finish cleaning up my branching program stuff soon, then hopefully it will convince you a bit more that this kind of circuit stuff isn't too bad too work with. :)

[Shreyas Srinivas]

Alex Meiburg said:

I dunno, I think this is not the most natural or ergonomic definition of circuits. (And, while there may be multiple good definitions of the same informal concept in Lean, they should either be natural or ergonomic.) I believe you that they might be natural for arithmetic circuit complexity, which I'm passingly familiar with but have never worked on myself. You say that it's easier to construct explicit examples of circuits, and this monadic DSL is nice, but I guess I'm not convinced that it's easy for the cases of interest to me (complexity theory -- as opposed to, say, constructing explicit circuits for a particular function).

I actually wrote this with the intent of using it in complexity theory

[Shreyas Srinivas]

This monadic approach is a method to write the inductive type inside a monad. In principle you can write a different Model in which evalQuery returns just the inductive circuit type as it is, or a DAG like your structure.

[Shreyas Srinivas]

I am still considering how to work with IDs in a more transparent way to get a good size function fwiw.

[Shreyas Srinivas]

Another point to consider is that essentially Prog is a Free monad DSL. You can write your own notion of Branching Programs with its constructors, and retrofit it into this DSL easily

[Shreyas Srinivas]

You can see the examples in ProgExamples.lean to get an idea of how to fit an arbitrary inductive type into Prog

[Johannes Tantow]

Alex Meiburg schrieb:

I think I'm increasingly of the opinion that it may be worth keeping a few different types around, which offer different options for constructions, and then we have the functions to move between them.

For circuits, we have one informal notion: a circuit.
Then there's a few different ways a mathematician might right down a definition (in English):

• A series of layers, which connect one to the next. (the one I linked at the top of this thread)
• A series of of layers, which each connect to any previous layer.
• A DAG
• An inductive construction, with some method of common subexpression elimination -- what you've been describing
• Straight-line-programs

And additionally all of these have two different conventions I'm aware of: do you start with the inputs to the circuit explicitly as the first n nodes? Or, can I add "fresh copies" of the input at later nodes? (A special type of "constant" gate that is always the ith input.)

Do we need an explicit model for dags? I don't see what is simpler than straight-line programs for that. You can still transform a straight line program to a dag, if you want to without having to maintain another definition.

[Johannes Tantow]

In one of my own tries I have defined circuits like this

structure Circuit where
  gates : List (Option (Nat × Nat))
  well_formed : ∀ (i : Fin gates.length) (n1 n2 : Nat), gates[i] = some (n1, n2) → (n1 < i ∧ n2 < i)
  input_length : Fin (gates.length)
  input_well_formed : ∀ (i : Fin gates.length), gates[i] = none ↔ i < input_length
  output : List (Fin gates.length)

to try and validate a reduction. For me everything though is a NAND-gate which makes the straightline program simpler than having to support multiple gate operations with different arities.

[Shreyas Srinivas]

@Alex Meiburg in this DSL the input nodes are simply circuit parameters supplied to a function

[Shreyas Srinivas]

It doesn't matter whether they are constant or not and where they are used first

[Shreyas Srinivas]

Alex Meiburg said:

I'd also like to note that the inductive definition doesn't (obviously, to me) generalize to multiple-output circuits. So things like the class FNC or theorems like Uhlig's "mass production of Boolean functions" would seem very hard to get in that form.

This is also not true. You can change the output type of a prog and generate a tuple of circuits

[Chris Henson]

Alex Meiburg said:

I've actually been working on branching programs a good bit locally, I have a proof of Barrington's Theorem, that width-5 oblivious BP's are equivalent to NC1.

This is very nice, I was specifically hoping to get to Barrington since it has been mentioned before. I'd love to start getting some of this into CSLib.

Here are my thoughts on the different representations. From Alex's comments it sounds like there are some nontrivial decisions, and possibly appetite to support multiple representations like we do for lambda calculi, but at the moment he has reached some nontrivial theorems that indicate some level of usability. My preference is that we:

• continue refining cslib#275 into cleanly subsuming TimeM and can be merged, so that this contribution does not stall with this widening scope
• separately begin (in small chunks at Alex's discretion) PRing material using this layered circuit representation building towards theorems on AC and NC
• revisit what additional representations, such as the monadic one or others Alex mentions, may make sense to additionally support

I'd like to clarify that I am not at all shooting down @Shreyas Srinivas's idea of having this monadic representation of circuits, just trying to make some suggestions about cleanly delineating the scope of PRs. I think what would be convincing is concretely seeing what proofs about complexity look like in the monadic framework, say the proof that Parity is not AC0, so that everyone can directly compare the ergonomics.

[Shreyas Srinivas]

For the latter I would need to work on Alex’s repo. I think the monadic framework can be translated to his representation. I suggest leaving the circuit examples as examples of how flexible the framework can be for now, but not pushing it any further. We definitely need a convenient way to program circuits for circuit complexity. There are far too many important upper bounds that rely on clever constructions.

[Shreyas Srinivas]

We could even choose to have a dual setup where Alex’s definitions are used for lower bound style while the monadic framework is used for upper bounds and we just link them by some equivalence relation

[Chris Henson]

I think leaving the examples is fine, though I might consider moving them to the testing directory.

[Shreyas Srinivas]

@Alex Meiburg : May I try porting the Prog stuff to your repo and compile circuits down to your description?

[Alex Meiburg]

Oh yes, I won't object to anyone trying to PR anything to or from my repo. :) If someone wants to grab it and get it into some other framework, I'll be all the happier!

[Alex Meiburg]

and I do want to understand this Prog stuff better. It just doesn't look very convenient to me but I strongly suspect that it's my lacking some vision of how it can/does scale up.

[Alex Meiburg]

(I think any representation will come with its own pain points, and its own places where it needs extra support/API to make it more usable...)

[Alex Meiburg]

Johannes Tantow said:

Do we need an explicit model for dags? I don't see what is simpler than straight-line programs for that. You can still transform a straight line program to a dag, if you want to without having to maintain another definition.

So, I agree that straight-line programs naturally include DAGs, essentially just throwing away the unneeded information of vertex labels (in some type) and instead just giving canonical Nat labels.

The reason I think DAGs might still be good would be composability. This is a bit far away from what any of us are trying to do now, but I can imagine some scenario where I say:

• I've constructed this circuit for f, that uses as a subroutine this circuit for g.
• I've separately constructed this circuit for h, that also uses as a subroutine this circuit for g.
• Now I'm constructing a new circuit that uses both f and h, and I want to reuse the g part of it.
  That would, I think, be pretty tricky to express in terms of SLPs. But very natural in DAGs, where I could put meaningful labels on my vertices that let me express this kind of thing.

I also think things like "compute these O(n^2) functions, each of depth O(n), in parallel, and then do a final O(n) computation on their outputs --> gives a circuit of depth O(n)" would be annoying to reason about in the SLP model. You will, again, be proving something about these different nodes with meaningful labels (something like (Fin a × Fin b) ⊕ Fin c), but instead you're just doing it all with natural numbers. So you need to relabel through an Equiv to get the labels out, and show that the equivalence respects the ordering correctly; or you need to write down some explicit arithmetic for encoding/decoding the natural number labels to the IDs, which will also be a headache and very easy to mess up.

[Anvit Aggarwal]

Hi. I too have been working on formalising Barrington's Theorem (repo link). I defined Formula in the following way:

class BoolBasis (b : Type) where
(arity : b → ℕ)
(eval (g : b) : (Fin (arity g) → Bool) → Bool)

inductive demorgan_basis where
| not : demorgan_basis
| and : demorgan_basis

instance : BoolBasis demorgan_basis where
  arity
    | demorgan_basis.not => 1
    | demorgan_basis.and => 2

  eval
    | demorgan_basis.not => fun xs => !(xs 0)
    | demorgan_basis.and => fun xs => xs 0 && xs 1

inductive Formula (n : ℕ) (b : Type) [BoolBasis b]: Type where
  | var : Fin n → Formula n b
  | cons (g : b) : (Fin (BoolBasis.arity g) → Formula n b) → Formula n b

def Formula.eval [BoolBasis b] : Formula n b → Input n → Bool
| Formula.var i, env => env i
| Formula.cons (g : b) f, env =>
  let xs : Fin (BoolBasis.arity g) → Bool :=
    fun i => Formula.eval (f i) env
  BoolBasis.eval g xs

And proved a version of Barrington's theorem using {AND, NOT} basis and group programs instead of branching programs.

(f : Input m → Bool)
    (hfcomputed : computed_by_formula demorgan_basis f d) :
    ∀ (α : Equiv.Perm (Fin 5)), Equiv.Perm.IsCycle α → α.support.card = 5 → ∃ (P : GroupProgram (Equiv.Perm (Fin 5)) m),
      P.length ≤ 4 ^ d ∧
      computes_with α P f := by

It seems as though @Alex Meiburg has already formalised the proof of Barrington's theorem. I wanted to ask if my current work could be useful in any way.

Also, I'd like to continue working on formalising circuit complexity theory. I'm not sure if it helps, but I'm currently a sophomore in Computer Science, and only starting out with Circuit Complexity Theory. I'd appreciate any suggestions on directions I could work on now.

[Shreyas Srinivas]

Another Update : I wrote another query model for circuits that compiles down to the previous model, but labels their IDs automatically

[Shreyas Srinivas]

You can see the examples in CircuitProgs.lean in the section section CircuitQuery

[Shreyas Srinivas]

@Yuval Filmus This should remove the concern of cheating

[Alex Meiburg]

@Anvit Aggarwal I think it's definitely still useful. Oftentimes having two different proofs is good, it'll show two different ways of doing the same thing. This is thread is active with us discussing the "right way" to do things.

[Yuval Filmus]

Your definition gives different IDs to the same subcircuit and the same ID to different subcircuits.

Perhaps the best solution is to prove some nontrivial theorems using one of these models — both upper and lower bounds — and see how easy it is.

[Shreyas Srinivas]

Yuval Filmus said:

Your definition gives different IDs to the same subcircuit and the same ID to different subcircuits.

Perhaps the best solution is to prove some nontrivial theorems using one of these models — both upper and lower bounds — and see how easy it is.

It doesn’t. Whether it assigns a different id to equal sub circuits or not depends on how you declare it

[Yuval Filmus]

Perhaps I'm looking at the wrong functions — circQueryEvalAux labels the root with the input id, the left child with id+1, and the right child with id+2. Doesn't that mean that if you use mul z z then the children will get different id's? Similarly, won't the two children of the left child get the id's id+2 (again) and id+3?

[Shreyas Srinivas]

Ah I see what you mean. Yes

[Shreyas Srinivas]

Personally I like the explicit circuit model more because it is trivial to impose the condition that only equal nodes get equal IDs and that is sufficient for boolean circuit complexity.

[Yuval Filmus]

I vote for straight-line programs, but there are probably other issues with them.
That's why it might be best to give things a test run.

[Shreyas Srinivas]

I think straight line programs can also be encoded in this framework.

[Shreyas Srinivas]

I think I know how to recover recursive programs. We have to make the circuit definition recursive on only one argument.

[Alex Meiburg]

I think I can show some of my idea of how these models could fit together, here: https://github.com/Timeroot/CircuitComp/blob/main/CircuitComp/BranchingProgram/Basic.lean

This is for branching programs, not circuits. But I think several of the same ideas apply and it's an easier test ground.

So I've got LayeredBranchingProgram (nodes are in Fin-indexed layers and point only to the next one), BranchingProgram (which is an unstructured DAG), and SkipBranchingProgram (which has layers, but nodes can point to any subsequent one).

The suggested definition that I got from Aristotle for BranchingProgram was actually not what I was initially intending, but it was quite interesting:

structure BranchingProgram (α : Type u) (β : Type v) (γ : Type w) where
  nodes : Type v
  start : nodes
  /-- Every node either returns a value in `γ`, or reads a variable `α` and branches to the next node. -/
  info : nodes → γ ⊕ (α × (β → nodes))
  /-- The relation `child` is well-founded, ensuring no infinite paths. -/
  wellFounded : WellFounded (fun v u ↦ ∃ var next val, info u = .inr (var, next) ∧ next val = v)

so that evaluation comes straight from well-founded recursion. This lets you include interesting cases like a branching program that reads Nat valued variables, and has different depths depending on the values it reads - with no bound on the depth at all! While still having meaningful termination.

[Alex Meiburg]

Then there's LayeredBranchingProgram.toBranchingProgram which turns it into a DAG, and BranchingProgram.toSkip which computes depths and lays them out, and SkipBranchinProgram.toLayered which adds in the missing intermediate nodes to avoid skip connections.

All of these are then backed up with an appropriate proof that their eval functions agree.

[Alex Meiburg]

In Barrington.lean I separately define GroupProgram, and have the conversion from an AND-NOT circuit (a FeedForward) to a GroupProgram over S^5; and then the conversion from GroupProgram to BranchingProgram. I'm working on getting the compilation from BranchingProgram back down to a FeedForward circuit in log-depth, to get the other direction of Barrington's theorem.

[Alex Meiburg]

I really believe that keeping these different definitions around will be helpful.

One of my goals to make sure this is workable is to show that you can convert a non-oblivious (layered) branching program to an oblivious one, with only a modest increase in width. This is very tedious to do with a plain LayeredBranchingProgram, but much more straightforward to do with a SkipBranchingProgram: spread the nodes out so as to group separate nodes reading different variables into different levels. So it's easy to see that you can do this with a SkipBranchingProgram.

To show that you can make a layered program oblivious, you convert to a skip branching program (which doesn't change width), make that oblivious, then convert back (which increases width in a controlled amount, and keeps it oblivious.)

[Alex Meiburg]

I'm still mucking with them enough as I go that I don't think it's PR-ready yet. Also my proofs need to be cleaned up. :) But I think once I hit those ^^ two theorems, I'll try to PR it in some form.

[Shreyas Srinivas]

@Yuval Filmus : I worked on the circuits language a bit and now managed to make it work without IDs

[Shreyas Srinivas]

I have renamed the old Circuit to Formula. The size computation of formulas works as expected.

[Shreyas Srinivas]

Then I provided a model from Circuit to Formula that ensures that a formula is only counted in size when it is evaluated in the monad.

[Shreyas Srinivas]

So I can avoid double counting of repeated circuits.

[Shreyas Srinivas]

See example 6

[Shreyas Srinivas]

Link : https://github.com/Shreyas4991/cslib/blob/d472ff51419c7647457912d60f941264eee9f4b8/Cslib/Algorithms/CircuitProgs.lean#L198

[Shreyas Srinivas]

Also CC : @Alex Meiburg

[Shreyas Srinivas]

I am fixing a mistake right now. I'll ping once it is done. Basically the idea is to turn circuit into a monad in itself.

[Shreyas Srinivas]

I will be moving this model to a separate PR

[Snir Broshi]

FYI Dennj Osele is PRing circuits to Mathlib #34578

[Yuval Filmus]

Or rather, PRing formulas but calling them circuits to skirt the issue…

[Shreyas Srinivas]

Mathlib is really not the best place for this. When there is no agreement on which definition of a circuit to even use, people shouldn’t be PRing a definition to either lib. Concretely the solution is to first prove upper and lower bounds using any given definition/model of circuits, and then, if there is convergence to that model, then PR it to CSLib.

[Snir Broshi]

I agree but I'm not sure what we can do about this other than comment our thoughts in that PR
They don't seem to be active on Zulip, and are not subscribed to the CSLib channel

[Shreyas Srinivas]

Letting a mathlib maintainer know should suffice.

[Chris Henson]

I think we should take care to not dictate what is in scope for Mathlib, and there is no mandate that all contributions to Mathlib's Computability modules should immediately be rerouted. On the other hand if there is a promising Mathlib PR that for whatever reason appears will not be merged, it seems perfectly fine for either a Mathlib or CSLib maintainer to inquire if the author is interested in contributing to CSLib. Conversely, CSLib retains the prerogative to extend, ignore, or otherwise deviate from Mathlib.

[Chris Henson]

Yuval Filmus said:

Or rather, PRing formulas but calling them circuits to skirt the issue…

To be clear however, I do agree on this point. To me it's analogous to when people formalize a "categorical semantics" but really they've worked around the encoding issues by conflating the syntax with its interpretation.

[Yuval Filmus]

The author of the PR actually has a clear vision regarding the formula / circuit issue, articulated in the PR.
I wonder whether there is any reason to duplicate their effort here.

[Chris Henson]

It is a bit unfortunate there was not more coordination here. I've not compared them closely, but my suggestion is that if anyone has comments about the differences between @Alex Meiburg's CircuitComp and #34578 (or any general concerns) that you point them out on the Mathlib PR. It would be ideal that whatever ends up in Mathlib is something we are happy using too.