---
Video Title: Good Circuits Evaluate
Description: Theory of Computation
https://uvatoc.github.io/week3

6.3: Good Circuits Evaluate
- Proving that all property constructed circuits evaluate as expected

David Evans and Nathan Brunelle
University of Virginia
---

Our hope is that if the definition is
correct, at least good circuits,

and actually only good circuits, when we
execute them, we'll get the value we expect.

They'll always finish
executing, and we'll

always get values that
are defined at the end.

Can we prove that?

What strategy are we going to need to
prove this?

And it should have something to do with
the two properties we've set.

It has to not have cycles.

It has to be connected in the right way.

That kind of means there has to be a path
from the inputs.

To the outputs, and there can't be cycles.

And if that's the case, well, this is the
hint.

So the book's definition
has the same property that

depends on there's some
way of layering the circuit.

That we can sort the gates
in some order, such that

at each layer, the inputs
are all in earlier layers.

That you never depend on input in a later
layer.

If you had a cycle, you couldn't do that.

But if you don't have cycles, you can sort
the gates into layers in some way.

So, at each layer, every gate only depends
on inputs from a previous layer.

And if you can define
things in layers, well, then it

seems like we're starting
with an input layer defined.

What are we going to need to do to prove
that eventually we get the outputs defined?

What kind of proof do you think might be
useful here?

Yeah.

Yeah.

So what are we doing induction on?

It has to be a natural number.

Remember, our induction principle only
works for natural numbers.

So what's the natural number that we're
doing induction on?

Yeah.

Good.

Yeah, the layers.

We can number the layers.

The book already did it for us.

It said there's a function
that maps each gate

to a number, which is
the layer of that gate.

We're doing induction.

Where our induction predicate is that for
all gates at layer n or earlier,

the output is defined.

You have a base case, which is the inputs.

So, of course, one is really nice to get
an input.

And our inductive case is always saying if
all the inputs of the previous layer are

defined, we can define the outputs at the
next layer.

Here.

Hello.
If any questions, please try to subscribe.

So with Mooji Takashi, please take a
spreadsheet ahead.