feat(Computability): add generic circuit model - #841
Conversation
| namespace Cslib.Circuits | ||
|
|
||
| /-- A straight-line program with designated output wires. -/ | ||
| structure Circuit (σ : Signature) (n g m : Nat) where |
There was a problem hiding this comment.
Is it necessary to have the circuit be parametric over the number of internal gates? This seems a bit unintuitive to me, I usually think of types representing computations as having performance parameters like gate count as methods.
There was a problem hiding this comment.
It is not necessary, but it works well for the inductive definition. Basically, every gate corresponds to a line in a straightline program. If you want to have SomeCircuit which abstracts how many internal gates and has a function size you can wrap this with that.
In particular, carrying g around allows you to know exactly which wires you can refer to in this line.
There was a problem hiding this comment.
Right, I guess I was finding this challenging to use. To try it out I wanted to write a circuit to implement Strassen matrix multiplication, but I got stuck when I realized I didn't know the exact recursive formula for the number of gates in the circuit in advance.
There was a problem hiding this comment.
Trying this bundled model you suggested seems to work fine though, I don't see any reason to hold up the PR on this account.
There was a problem hiding this comment.
That is a fair point. Maybe there should be a circuit builder interface for building them.
|
I know this is super generic, but does it make sense to reference some textbooks here? |
| /-! | ||
| # Signatures | ||
|
|
||
| A signature is a collection of finitary operation symbols, each with a fixed |
There was a problem hiding this comment.
The finitariness (?) is not enforced by the definition, is it?
There was a problem hiding this comment.
Nope, I don't think it should though, I'll just remove this text.
| /-- The operation symbols of the signature. -/ | ||
| Op : Type v | ||
| /-- The number of arguments taken by each operation symbol. -/ | ||
| Arity : (op : Op) → Nat |
There was a problem hiding this comment.
I would say either
| Arity : (op : Op) → Nat | |
| Arity (op : Op) : \N |
or
| Arity : (op : Op) → Nat | |
| Arity : Op \to \N |
There was a problem hiding this comment.
Oh yeah, we don't need op here so I'll just do Op \r \N.
| -/ | ||
| module | ||
|
|
||
| public import Cslib.Computability.Circuits.Signature |
There was a problem hiding this comment.
Maybe Signature and Interpretation should be a single file? It's quite a long import chain you have to follow from Circuit.
There was a problem hiding this comment.
That is reasonable.
| namespace Cslib.Circuits | ||
|
|
||
| /-- An interpretation assigns an operation on `Carrier` to every symbol in `σ`. -/ | ||
| abbrev Interpretation (σ : Signature) Carrier := |
There was a problem hiding this comment.
| abbrev Interpretation (σ : Signature) Carrier := | |
| abbrev Interpretation (σ : Signature) (Carrier: Type*) := |
?
There was a problem hiding this comment.
What is the idea behind the term "Carrier"? Shouldn't it be "Value" or something?
There was a problem hiding this comment.
I think "carrier" is a somewhat common term for the type on which a collection of operations act (for example)
We could reference Wigderson's 93 fusion paper, he defines this sort of straightline program variant of circuits. |
|
This change makes heavy use of autoimplicit. I think I would prefer |
crei
left a comment
crei
left a comment
There was a problem hiding this comment.
I haven't read everything yet. It might make sense to split up Program a bit, it is already 500 lines.
| (line.mapWires wireMap).wires argument = wireMap (line.wires argument) := rfl | ||
|
|
||
| /-- A topologically ordered straight-line program of `g` gates. -/ | ||
| inductive Program (σ : Signature) (n : Nat) : Nat → Type v where |
There was a problem hiding this comment.
What about spending some more characters in general to avoid confusion?
| inductive Program (σ : Signature) (n : Nat) : Nat → Type v where | |
| inductive Program (σ : Signature) (inputCnt : Nat) : Nat → Type v where |
There was a problem hiding this comment.
n is the blessed number for input lengths!
BoltonBailey
left a comment
BoltonBailey
left a comment
There was a problem hiding this comment.
This is exciting, I would definitely be interested in a Circuit model like this.
| namespace Cslib.Circuits | ||
|
|
||
| /-- An interpretation assigns an operation on `Carrier` to every symbol in `σ`. -/ | ||
| abbrev Interpretation (σ : Signature) Carrier := |
There was a problem hiding this comment.
I think "carrier" is a somewhat common term for the type on which a collection of operations act (for example)
| · simpa [Program.trace, Function.comp_apply] using congrFun (p.map_eval h x) gate | ||
|
|
||
| /-- The scalar function computed by an internal gate. -/ | ||
| def Program.gateFunction |
There was a problem hiding this comment.
Is there a reason these can't have the input argument before the colon?
There was a problem hiding this comment.
They certainly could!
Good idea.
I don't personally have a strong preference. |
|
I believe I addressed all of the comments cc @BoltonBailey @crei |
3 participants
Adds a generic circuit model we can use for arithmetic and Boolean circuit lower/upper bounds. I have experimented with this definition for upper/lower bounds and it is quite usable, I've got some lower bounds I can PR once this is accepted.
If you want to see how it can be used, you can see: https://github.com/samuelSchlesinger/algebraic-circuits.
Used Codex with GPT 5.6 Sol to refactor this for CSLib, but the underlying definitions and many of the theorems/lemmata were originally authored by me. Some of the examples and documentation bits were added or edited by Codex as well.