The number written by a Boolean circuit

Lax366625.NumberedCircuits · concepts/Lax366625/NumberedCircuits.lean · lax-366625

definition

Loading review…

Natural Language Statement

Definition

An instance is a Boolean circuit as for the circuit value problem, whose output gates each hold one binary digit, together with a binary relation comparing the output gates. When that relation is a linear order on the output gates, the number written by the circuit is $\sum 2^{r(g)}$ over the output gates $g$ that derive the value $1$ , $r(g)$ being the number of output gates below $g$ ; otherwise it is $0$ .

Concept map

7 concepts; 12 descendants hidden

100%

Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A

Lean source view on GitHub

Show types on hover

1	import Mathlib.Algebra.BigOperators.Finprod
2	import Mathlib.SetTheory.Cardinal.Finite
3	import Mathlib.Order.PiLex
4	import Mathlib.Data.Prod.Lex
5	import Mathlib.Data.Fintype.EquivFin
6	import Mathlib.ModelTheory.Order
7	import Mathlib.ModelTheory.Semantics
8	import Mathlib.ModelTheory.Complexity
9	import Mathlib.Tactic.FinCases
10	import Mathlib.Logic.Equiv.Fin.Basic
11	import Mathlib.ModelTheory.Syntax
12	import Lax535992.CircuitValue
13	import Lax366625.CountingProblems
14
15	/-!
16	---
17	title: The number written by a Boolean circuit
18	type: definition
19	---
20	An instance is a Boolean circuit as for the circuit value problem, whose
21	output gates each hold one binary digit, together with a binary relation
22	comparing the output gates. When that relation is a linear order on the
23	output gates, the number written by the circuit is $\sum 2^{r(g)}$ over the
24	output gates $g$ that derive the value $1$ , $r(g)$ being the number of output
25	gates below $g$ ; otherwise it is $0$ .
26	-/
27
28	namespace Lax366625.NumberedCircuits
29
30	open Lax535992.CircuitValue
31
32	open FirstOrder
33
34	open FirstOrder.Language
35
36	/-- The relation symbols of the language. -/
37	inductive numCircuitRel : ℕ → Type where
38	/-- `isTrue g`: the element `g` is a constant input gate holding `1`. -/
39	\| isTrue : numCircuitRel 1
40	/-- `isFalse g`: the element `g` is a constant input gate holding `0`. -/
41	\| isFalse : numCircuitRel 1
42	/-- `isAnd g`: the element `g` is a conjunction gate. -/
43	\| isAnd : numCircuitRel 1
44	/-- `isOr g`: the element `g` is a disjunction gate. -/
45	\| isOr : numCircuitRel 1
46	/-- `isNot g`: the element `g` is a negation gate, its argument read off
47	`left`. -/
48	\| isNot : numCircuitRel 1
49	/-- `out g`: the element `g` is an output gate, holding one digit. -/
50	\| out : numCircuitRel 1
51	/-- `left g x`: the gate `g` takes `x` as its first argument. -/
52	\| left : numCircuitRel 2
53	/-- `right g x`: the gate `g` takes `x` as its second argument. -/
54	\| right : numCircuitRel 2
55	/-- `below h g`: the digit held by `h` is at most as significant as the one
56	held by `g`. -/
57	\| below : numCircuitRel 2
58	deriving DecidableEq
59
60	/-- The relational language of Boolean circuits writing a number: the symbols
61	of circuits, and a comparison of the output gates. -/
62	def numCircuit : FirstOrder.Language :=
63	⟨fun _ => Empty, numCircuitRel⟩
64
65	instance instIsRelationalNumCircuit : FirstOrder.Language.IsRelational numCircuit := fun _ =>
66	(inferInstance : IsEmpty Empty)
67
68	/-- `isTrue g`: the element `g` is a constant input gate holding `1`. -/
69	abbrev ncIsTrue : numCircuit.Relations 1 :=
70	.isTrue
71
72	/-- `isFalse g`: the element `g` is a constant input gate holding `0`. -/
73	abbrev ncIsFalse : numCircuit.Relations 1 :=
74	.isFalse
75
76	/-- `isAnd g`: the element `g` is a conjunction gate. -/
77	abbrev ncIsAnd : numCircuit.Relations 1 :=
78	.isAnd
79
80	/-- `isOr g`: the element `g` is a disjunction gate. -/
81	abbrev ncIsOr : numCircuit.Relations 1 :=
82	.isOr
83
84	/-- `isNot g`: the element `g` is a negation gate, its argument read off
85	`left`. -/
86	abbrev ncIsNot : numCircuit.Relations 1 :=
87	.isNot
88
89	/-- `out g`: the element `g` is an output gate, holding one digit. -/
90	abbrev ncOut : numCircuit.Relations 1 :=
91	.out
92
93	/-- `left g x`: the gate `g` takes `x` as its first argument. -/
94	abbrev ncLeft : numCircuit.Relations 2 :=
95	.left
96
97	/-- `right g x`: the gate `g` takes `x` as its second argument. -/
98	abbrev ncRight : numCircuit.Relations 2 :=
99	.right
100
101	/-- `below h g`: the digit held by `h` is at most as significant as the one
102	held by `g`. -/
103	abbrev ncBelow : numCircuit.Relations 2 :=
104	.below
105
106	open FirstOrder
107
108	open Language Structure
109
110	/-- Forgetting the comparison of the outputs: the vocabulary of circuits, read
111	in the vocabulary of circuits writing a number. -/
112	def circuitOfNum : circuit →ᴸ numCircuit where
113	onFunction := fun {_} f => isEmptyElim f
114	onRelation := fun {n} R =>
115	match n, R with
116	\| _, .isTrue => ncIsTrue
117	\| _, .isFalse => ncIsFalse
118	\| _, .isAnd => ncIsAnd
119	\| _, .isOr => ncIsOr
120	\| _, .isNot => ncIsNot
121	\| _, .out => ncOut
122	\| _, .left => ncLeft
123	\| _, .right => ncRight
124
125	/-- A circuit writing a number is a circuit. -/
126	instance numCircuitStructure (A : Type) [numCircuit.Structure A] :
127	circuit.Structure A :=
128	circuitOfNum.reduct A
129
130	section Semantics
131
132	variable {A : Type} [numCircuit.Structure A]
133
134	/-- The output gate `g` holds the digit `1`. -/
135	def OutBit (g : A) : Prop :=
136	RelMap ncOut ![g] ∧ GateVal true g
137
138	/-- `h` is an output gate strictly below `g`. -/
139	def LowerOut (g h : A) : Prop :=
140	RelMap ncOut ![h] ∧ h ≠ g ∧ RelMap ncBelow ![h, g]
141
142	/-- The rank of a gate among the outputs: the number of output gates strictly
143	below it. -/
144	noncomputable def outRank (g : A) : ℕ :=
145	Nat.card {h : A // LowerOut g h}
146
147	variable (A) in
148	/-- The comparison of the outputs is a linear order on them: reflexive,
149	transitive, antisymmetric and total among the output gates. -/
150	def OutOrder : Prop :=
151	(∀ p : A, RelMap ncOut ![p] → RelMap ncBelow ![p, p]) ∧
152	(∀ p q r : A, RelMap ncOut ![p] → RelMap ncOut ![q] → RelMap ncOut ![r] →
153	RelMap ncBelow ![p, q] → RelMap ncBelow ![q, r] → RelMap ncBelow ![p, r]) ∧
154	(∀ p q : A, RelMap ncOut ![p] → RelMap ncOut ![q] →
155	RelMap ncBelow ![p, q] → RelMap ncBelow ![q, p] → p = q) ∧
156	∀ p q : A, RelMap ncOut ![p] → RelMap ncOut ![q] →
157	RelMap ncBelow ![p, q] ∨ RelMap ncBelow ![q, p]
158
159	variable (A) in
160	open Classical in
161	/-- The number written by a circuit: each output gate deriving the value
162	`1` contributes two to the power of its rank among the outputs; `0` unless the
163	outputs are linearly ordered. -/
164	noncomputable def circuitNumber : ℕ :=
165	if OutOrder A then ∑ᶠ g : A, if OutBit g then 2 ^ outRank g else 0 else 0
166
167	end Semantics
168
169	open Lax366625.CountingProblems
170
171	/-- The number written by a circuit, as a counting problem. -/
172	noncomputable def CircuitNumber : CountingProblem numCircuit :=
173	CountingProblem.ofFun fun A _ => circuitNumber A
174
175	end Lax366625.NumberedCircuits
176

Discussion

Ask a question or add context. Endorsements and structured flags are kept in the review panel above.

Loading discussion…

Lax Lean Archive

The number written by a Boolean circuit

Flags

Flag this concept

Natural Language Statement

Definition

Lean source view on GitHub

Discussion

Settings

Your comments