# Zulip Chat Archive

## 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).

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

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