OAI/Combinatorics/ContingencyTables/Machines/LiteralProgram.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

Public binary input and output for typed finite programs

Literal packing is independent of the counting algorithm. Its cost includes every packing, execution, and printing step.

  1. def OAI.ContingencyTables.LiteralProgram.pack line 16
  2. def OAI.ContingencyTables.LiteralProgram.erase line 17
  3. def OAI.ContingencyTables.LiteralProgram.unpack line 18
  4. def OAI.ContingencyTables.LiteralProgram.post line 19
  5. def OAI.ContingencyTables.LiteralProgram.packTime line 20
  6. def OAI.ContingencyTables.LiteralProgram.postTime line 22
  7. lemma OAI.ContingencyTables.LiteralProgram.packTime_mono line 26
  8. lemma OAI.ContingencyTables.LiteralProgram.postTime_mono line 30
  9. lemma OAI.ContingencyTables.LiteralProgram.pack_realizes line 34
  10. lemma OAI.ContingencyTables.LiteralProgram.post_realizes line 38
  11. def OAI.ContingencyTables.LiteralProgram.wrap line 52
  12. def OAI.ContingencyTables.LiteralProgram.wrapTime line 55
  13. lemma OAI.ContingencyTables.LiteralProgram.experiment_all_and line 59
  14. lemma OAI.ContingencyTables.LiteralProgram.wrap_realizes line 66
  15. def OAI.ContingencyTables.LiteralProgram.budgetPolynomial line 82

    Source documentation

    A polynomial representing the exact elementary block-map cost.

    noncomputable def budgetPolynomial (w H : ℕ) (p q : Polynomial ℕ) : Polynomial ℕ :=
…
  16. lemma OAI.ContingencyTables.LiteralProgram.eval_budgetPolynomial line 85
  17. theorem OAI.ContingencyTables.LiteralProgram.polynomial_wrap line 91

    Source documentation

    Any polynomial bound on the typed experiment gives a polynomial bound on the complete public binary execution.

    theorem polynomial_wrap {f : List Symbol → Experiment (List Symbol)}
    (F : OnlineTree.Realizer f) (p : Polynomial ℕ)
    (hp : ∀ as,F.cost as+(f as).worst weight ≤ p.eval (weight as)) :
    ∃ q : Polynomial ℕ,∀ as,wrapTime F as ≤ q.eval as.length := by
…

    Mentions: OAI.ContingencyTables.LiteralProgram.wrapTime

  18. theorem OAI.ContingencyTables.LiteralProgram.deterministic_compiles line 127

    Source documentation

    Deterministic typed programs therefore execute on the public binary tape with one fixed finite transition table and a polynomial time bound.

    theorem deterministic_compiles {f : List Symbol → List Symbol}
    (F : TreeTyped.Realizer f) (hF : PolynomialTime F)
    (hout : ∀ as,∀ b∈f as,b≠6 ∧ b≠7) :
    ∃ (A : RandomMachine) (q : Polynomial ℕ),∀ as,(∀ a∈as,a≠0) →
      ∀ t,q.eval as.length ≤ t → ∀ bits : Fin t → Bool,
      (run A as bits).state=none ∧ (run A as bits).tape.right₀=ListBlank.mk (f as) := by
…