Functionality

Difficulty: easy — 3 definitions, 6 abbreviations, 1 lemmas, 3 theorems.

definition abbreviation lemma theorem
legend

Now picture a rule that determines from some number of input bits a number of output bits. Even something this ordinary hides an enormous amount of possibility: for each one of the input sequences, the rule can determine any of the possible output sequences, completely independently of what it produces for every other input.

In general, given \(n\)-bits of input and \(m\)-bits of output, there are \(2^{(m\times2^n)}\) different rules.

The 1-bit input has two possibilities for which the 1-bit output has two possibilities, so there are \(2\times 2 = 2^{(1\times2^1)}\) different rules.

Growing the output size increases the space of possibilities fast:

Growing the input size increases the space of possibilities even faster:

Counting up every rule you could have been given, before being told which one you actually have, gives a super-exponential number — one that grows explosively fast as the input grows even slightly. Most such rules are chaotic: there’s no obvious pattern to exploit, so saying which one you have takes about as much information as that whole giant space of possibilities. Only a few rules are orderly instead — always output all zeros, say, or just copy the input straight through.

To feel how large these numbers get, look at a size real machines use often: 32 bits of input and 32 bits of output. The number of different rules of that size is \(2^{(32\times2^{32})}\), a number so large that writing it out in full, digit by digit, would take about forty-one billion digits. For comparison, a rough estimate for the number of atoms in the whole visible universe is a number with only about eighty digits. A single rule table of this very ordinary size already reaches far beyond the number of atoms in the universe.

In practice, people build such a rule out of smaller, understandable pieces, instead of picking one directly from that enormous space. A rule that turns \(n\) bits into \(m\) bits, followed by a rule that turns those \(m\) bits into \(p\) bits, together act as one single rule straight from \(n\) bits to \(p\) bits: feed the first rule’s output straight into the second. Building rules this way, piece by piece, keeps each piece small and understandable, even while the rule they form together reaches into that vast space of possibilities.

A rule like this always has some fixed number of inputs and some fixed number of outputs — its shape. Later files build other things with exactly the same shape (so many inputs, so many outputs) that behave very differently from a fixed rule: remembering something between one use and the next, say, or allowing more than one possible outcome. Naming the shape on its own, apart from what actually fills it, is what lets those very different things still be compared side by side later.

A shape: some number of input wires, and some number of output wires. What actually fills a given shape is left open here — see BitFunction below for one way to fill it.

abbrev Component.Family := Nat  Nat  Type

Outer dependencies: (none)

Lean core dependencies: Nat

The shape with one input wire and one output wire.

abbrev Component.Family.simplex (F : Component.Family) : Type := F 1 1

Outer dependencies: Component.Family

Lean core dependencies: Nat

Used by: (none)

The shape with several input wires feeding a single output wire.

abbrev Component.Family.multiplex (F : Component.Family) (n : Nat) : Type := F n 1

Outer dependencies: Component.Family

Lean core dependencies: Nat

Used by: (none)

The shape with one input wire fanning out to several output wires.

abbrev Component.Family.demultiplex (F : Component.Family) (m : Nat) : Type := F 1 m

Outer dependencies: Component.Family

Lean core dependencies: Nat

Used by: (none)

Filling a shape with a fixed rule: given a value on every input wire, it determines a value on every output wire, the same way every time.

abbrev Component.Func (Input Output : Type) : Component.Family :=
  fun n m => (Fin n  Input)  (Fin m  Output)

Outer dependencies: Component.Family

Lean core dependencies: Fin, Nat

A fixed rule turning any n-bit sequence into some m-bit sequence: the same input, every time, gives the same output.

abbrev BitFunction (n m : Nat) := Component.Func Bit Bit n m

Outer dependencies: (none)

Inner dependencies: Bit, Component.Func

Lean core dependencies: Nat

Copy a single input wire onto two output wires: whichever value comes in, both outputs show that very same value.

def Component.Func.copy (Input : Type) : Component.Func Input Input 1 2 :=
  fun iv _ => iv 0

Outer dependencies: Component.Func

Lean core dependencies: Fin, Nat

Used by: (none)

Discard a single input wire entirely: a rule with no output wires at all, so nothing is left to say what came in.

def Component.Func.discard (Input : Type) : Component.Func Input Input 1 0 :=
  fun _ => Fin.elim0

Outer dependencies: Component.Func

Lean core dependencies: Fin, Fin.elim0, Nat

Used by: (none)

Given a fixed number m of output bits, there are super-exponentially many possible rules from n input bits to m output bits: for each of the 2^n possible inputs, a rule is free to independently choose any of the 2^m possible outputs.

theorem card_BitFunction (n m : Nat) : Fintype.card (BitFunction n m) = 2 ^ (m * 2 ^ n) := by

Dependencies: Bit, BitFunction

Proof dependencies: BitSequence, card_BitSequence

Mathlib dependencies: Fintype.card, Fintype.card_fun, pow_mul

Lean core dependencies: Eq, Eq.mpr, Eq.symm, Fin, Nat, Nat.mul_comm, congrArg, id

With the input held fixed, growing the output by one bit multiplies the number of possible rules by the same fixed factor (2 ^ 2 ^ n) every time, however large m already is — repeatedly multiplying by a fixed factor is exactly what exponential growth means.

theorem card_BitFunction_succ_output (n m : Nat) :
    Fintype.card (BitFunction n (m + 1)) = Fintype.card (BitFunction n m) * 2 ^ 2 ^ n := by

Dependencies: Bit, BitFunction

Proof dependencies: card_BitFunction

Mathlib dependencies: Fintype.card, add_one_mul, pow_add

Lean core dependencies: Eq, Eq.mpr, Fin, Nat, congrArg, id

Used by: (none)

With the output held fixed, growing the input by one bit squares the number of possible rules, rather than multiplying it by some fixed factor: the multiplier itself keeps growing every time the input grows. That’s what makes this super-exponential — growth that outruns every fixed exponential rate, not just some of them.

theorem card_BitFunction_succ_input (n m : Nat) :
    Fintype.card (BitFunction (n + 1) m) = Fintype.card (BitFunction n m) ^ 2 := by

Dependencies: Bit, BitFunction

Proof dependencies: card_BitFunction

Mathlib dependencies: Fintype.card, pow_mul, pow_succ

Lean core dependencies: Eq, Eq.mpr, Eq.symm, Fin, Nat, Nat.mul_assoc, congrArg, id

Used by: (none)

Feeding a rule from n bits to m bits straight into a rule from m bits to p bits gives one single rule from n bits to p bits.

def BitFunction.comp (f : BitFunction n m) (g : BitFunction m p) : BitFunction n p := g  f

Outer dependencies: BitFunction

Inner dependencies: Bit

Lean core dependencies: Fin, Function.comp, Nat

Chaining three rules together gives the same combined rule no matter which neighboring pair you combine first.

theorem BitFunction.comp_assoc (f : BitFunction n m) (g : BitFunction m p) (h : BitFunction p q) :
    BitFunction.comp (BitFunction.comp f g) h = BitFunction.comp f (BitFunction.comp g h) := rfl

Dependencies: BitFunction, BitFunction.comp

Lean core dependencies: Eq, Nat, rfl

Used by: (none)

Dependency diagram

Drag to pan, Ctrl+scroll (or Cmd+scroll) to zoom, click a node to jump to it.

definitionabbreviationlemmatheoremdeclared elsewheredependencyproof dependency
legend