Defining circuits + proving circuit generation

Stream: general

[Wrenna Robson]

I was just reading the proof that all classical circuits/Boolean functions can be generated by AND and XOR gates along with FANOUT and CROSSOVER operations and the like - and I was wondering how you would prove this in Lean. I was thinking maybe you would want to define some suitable inductive type for circuits, and then show that you have some map from that to Boolean functions and then show that the map is surjective.

But I'm not sure how such a type should be properly defined. Does anyone have any thoughts? Surely something like this has been done before?

[Eric Wieser]

I would guess something like

inductive gate (σ : Type*)
| xor (a b : gate)
| and (a b : gate)
| input (i : σ)

def gate.eval (args : σ → bool) : gate σ → bool
| input i := args i
| and x y := band (x.eval args) (y.eval args)
| xor x y := bxor (x.eval args) (y.eval args)

example : function.surjective gate.eval

[Eric Wieser]

In that example, fanouts and crossovers are encoded in lean's expression tree to make things easier

[Wrenna Robson]

What about functions with multiple outputs? Potentially I guess you could do that as a general case of this...

[Wrenna Robson]

Also I think it wants to be fin n instead of general sigma as the argument I know does an induction.

[Wrenna Robson]

At the very least a fintype (I can't recall if doing an induction on fintypes is a good idea).

[Wrenna Robson]

I'm also pretty sure that FANOUT and CROSSOVER want to be explicit gates because they are part of the content of the circuit (and FANOUT in particular can't exist in a quantum circuit, so it's good to make the distinction explicit).

[Eric Wieser]

A function with multiple outputs is just a collection of single-output functions

[Eric Wieser]

Wrenna Robson said:

Also I think it wants to be fin n instead of general sigma as the argument I know does an induction.

You can always prove the surjectivity for σ = fin n or fintype σ, there's no need to restrict the definition

[Wrenna Robson]

You also need to be able to feed in dummy values.

[Wrenna Robson]

I think that's ok currently

[Scott Morrison]

You might be interested in the description in terms of monoidal categories (circuits with FANOUT and CROSSOVER "live" in a cartesian monoidal category, circuits with CROSSOVER "live" in a symmetric monoidal category, circuits with neither live in a monoidal category). In some sense your inductive type is going to be the construction of the free [cartesian|symmetric| ] monoidal category, but before quotienting by all the relations making the axioms true. (e.g. that CROSSOVER squares to the identity, etc)

[Wrenna Robson]

Yes, I believe this is true.

[Wrenna Robson]

I guess what I'm most struggling with is how you define the operation that is, you know, "I have some circuit with 5 outputs and I want to stick 3 of those outputs into another circuit with 4 inputs, get an input from another circuit, and let the other outputs extend"

[Wrenna Robson]

Which I can't picture with Eric's construction.

[Mario Carneiro]

You can do that by adding what amounts to a monad instance on gate: Given a gate X and a function from X to gate Y you can construct a gate Y by composition

[Mario Carneiro]

In Eric's construction circuits only have one output. A circuit with multiple outputs would be a Output -> gate Input function (a Kleisli arrow).

[Wrenna Robson]

Aha

[Wrenna Robson]

where Output and Input are both themselves kinds of gate?

[Mario Carneiro]

In the last bit Output and Input are finite types that range over the set of wires coming in/out

[Mario Carneiro]

so the input value of type Output is selecting which wire you want to sample

[Mario Carneiro]

You can use Eric's eval function to apply a Output -> gate Input to a Input -> bool function to get an Output -> bool function (this might help explain why everything seems turned around, the input and output are contravariant)

[Eric Wieser]

Output and Input can be thought of as types that hold the names of the wires. Most like you will want to set them to fin n so that you can use ![ ... ] notation, but there's no reason to do so in the definition

[Eric Wieser]

def gate.bind (blocks : σ → gate σ2) : gate σ → gate σ2
| input i := blocks i
| and x y := band (x.bind blocks) (y.bind blocks)
| xor x y := bxor (x.bind blocks) (y.bind blocks)

I couldn't work it out from your initial description; do you want to allow constant values? if so, you can implement eval in terms of bind composed with gate.const. If you only want to permit "dummy" wires with indeterminate values, then I think you can still do this but you'll need to make the return type of eval option bool

[Wrenna Robson]

Yes, I want to allow constant values.

[Wrenna Robson]

So oddly enough, entirely separately to the above I was looking today at this Coq definition (for a different context, but similar context). How would I replicate this in Lean 3/Lean 4?

Inductive ZX : nat -> nat -> Type :=
  | Empty : ZX 0 0
  | X_Spider nIn nOut (α : R) : ZX nIn nOut
  | Z_Spider nIn nOut (α : R) : ZX nIn nOut
  | Cap : ZX 0 2
  | Cup : ZX 2 0
  | Swap : ZX 2 2
  | Stack {nIn0 nIn1 nOut0 nOut1} (zx0 : ZX nIn0 nOut0) (zx1 : ZX nIn1 nOut1) :
      ZX (nIn0 + nIn1) (nOut0 + nOut1)
  | Compose {nIn nMid nOut} (zx0 : ZX nIn nMid) (zx1 : ZX nMid nOut) : ZX nIn nOut.

[Kyle Miller]

I'm not sure what R is (though I recognize the inductive type as being for the ZX graphical calculus), but here's Lean 3:

variables (R : Type)

inductive ZX : ℕ -> ℕ -> Type
| Empty : ZX 0 0
| X_Spider nIn nOut (α : R) : ZX nIn nOut
| Z_Spider nIn nOut (α : R) : ZX nIn nOut
| Cap : ZX 0 2
| Cup : ZX 2 0
| Swap : ZX 2 2
| Stack {nIn0 nIn1 nOut0 nOut1} (zx0 : ZX nIn0 nOut0) (zx1 : ZX nIn1 nOut1) :
    ZX (nIn0 + nIn1) (nOut0 + nOut1)
| Compose {nIn nMid nOut} (zx0 : ZX nIn nMid) (zx1 : ZX nMid nOut) : ZX nIn nOut

[Kyle Miller]

Ah right, R should be the real numbers, recording the phase for the X/Z spider

[Wrenna Robson]

Right I thought it should just work in place.

[Wrenna Robson]

And aye it's the ZX Calculus.

[Wrenna Robson]

Yeah, alright, that does appear to work in Lean 3 - not sure about Lean 4 though.

[Lev Stambler]

Is there any intuition as to why ZX calculus is used over more traditional representations of circuits?