## Stream: general

### Topic: Defining circuits + proving circuit generation

#### Wrenna Robson (Oct 24 2022 at 08:37):

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 (Oct 24 2022 at 08:45):

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 (Oct 24 2022 at 08:47):

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

#### Wrenna Robson (Oct 24 2022 at 09:04):

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

#### Wrenna Robson (Oct 24 2022 at 09:12):

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

#### Wrenna Robson (Oct 24 2022 at 09:13):

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

#### Wrenna Robson (Oct 24 2022 at 09:38):

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 (Oct 24 2022 at 11:17):

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

#### Eric Wieser (Oct 24 2022 at 11:17):

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 (Oct 24 2022 at 18:59):

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

#### Wrenna Robson (Oct 24 2022 at 18:59):

I think that's ok currently

#### Scott Morrison (Oct 24 2022 at 22:28):

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 (Oct 25 2022 at 10:31):

Yes, I believe this is true.

#### Wrenna Robson (Oct 25 2022 at 10:34):

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 (Oct 25 2022 at 10:35):

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

#### Mario Carneiro (Oct 25 2022 at 10:41):

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 (Oct 25 2022 at 10:44):

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

Aha

#### Wrenna Robson (Oct 25 2022 at 10:45):

where Output and Input are both themselves kinds of gate?

#### Mario Carneiro (Oct 25 2022 at 10:46):

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

#### Mario Carneiro (Oct 25 2022 at 10:46):

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

#### Mario Carneiro (Oct 25 2022 at 10:49):

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 (Oct 25 2022 at 10:57):

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 (Oct 25 2022 at 11:01):

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 (Oct 25 2022 at 11:24):

Yes, I want to allow constant values.

#### Wrenna Robson (Oct 28 2022 at 10:16):

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 (Oct 28 2022 at 10:19):

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 (Oct 28 2022 at 10:22):

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

#### Wrenna Robson (Oct 28 2022 at 10:23):

Right I thought it should just work in place.

#### Wrenna Robson (Oct 28 2022 at 10:23):

And aye it's the ZX Calculus.

#### Wrenna Robson (Oct 28 2022 at 10:34):

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

#### Lev Stambler (Dec 12 2022 at 17:40):

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

Last updated: Dec 20 2023 at 11:08 UTC