Generic universal-machine interfaces -- proof internals #
Proofs supporting the public API in
Complexitylib.Models.TuringMachine.Universality.
theorem
Complexity.TM.isComputable_comp_internal
{first second : List Bool → List Bool}
(hfirst : IsComputable first)
(hsecond : IsComputable second)
:
IsComputable (second ∘ first)
theorem
Complexity.TM.simulates_comp_internal
{firstTapes secondTapes thirdTapes : ℕ}
{first : TM firstTapes}
{second : TM secondTapes}
{third : TM thirdTapes}
{compileFirst compileSecond : List Bool → List Bool}
(hFirst : first.Simulates second compileFirst)
(hSecond : second.Simulates third compileSecond)
:
theorem
Complexity.TM.additiveProgramOverhead_mono_internal
{compile : List Bool → List Bool}
{first second : ℕ}
(hbound : first ≤ second)
(hoverhead : HasAdditiveProgramOverhead compile first)
:
HasAdditiveProgramOverhead compile second
theorem
Complexity.TM.additiveProgramOverhead_comp_internal
{compileFirst compileSecond : List Bool → List Bool}
{first second : ℕ}
(hFirst : HasAdditiveProgramOverhead compileFirst first)
(hSecond : HasAdditiveProgramOverhead compileSecond second)
:
HasAdditiveProgramOverhead (compileFirst ∘ compileSecond) (second + first)
theorem
Complexity.TM.simulatesInTime_refl_internal
{firstTapes : ℕ}
(machine : TM firstTapes)
:
machine.SimulatesInTime machine id fun (x : List Bool) (sourceTime : ℕ) => sourceTime
theorem
Complexity.TM.simulatesInTime_mono_internal
{firstTapes secondTapes : ℕ}
{simulator : TM firstTapes}
{source : TM secondTapes}
{compile : List Bool → List Bool}
{firstClock secondClock : TimeOverhead}
(hclock : ∀ (program : List Bool) (sourceTime : ℕ), firstClock program sourceTime ≤ secondClock program sourceTime)
(hsim : simulator.SimulatesInTime source compile firstClock)
:
simulator.SimulatesInTime source compile secondClock
theorem
Complexity.TM.simulatesInTime_comp_internal
{firstTapes secondTapes thirdTapes : ℕ}
{first : TM firstTapes}
{second : TM secondTapes}
{third : TM thirdTapes}
{compileFirst compileSecond : List Bool → List Bool}
{clockFirst clockSecond : TimeOverhead}
(hFirst : first.SimulatesInTime second compileFirst clockFirst)
(hSecond : second.SimulatesInTime third compileSecond clockSecond)
:
first.SimulatesInTime third (compileFirst ∘ compileSecond) fun (program : List Bool) (sourceTime : ℕ) =>
clockFirst (compileSecond program) (clockSecond program sourceTime)
theorem
Complexity.TM.polynomialTimeOverhead_identity_internal :
PolynomialTimeOverhead fun (_program : List Bool) (sourceTime : ℕ) => sourceTime
theorem
Complexity.TM.polynomialTimeOverhead_comp_internal
{compileInner : List Bool → List Bool}
{additive : ℕ}
{clockOuter clockInner : TimeOverhead}
(hlength : HasAdditiveProgramOverhead compileInner additive)
(hOuter : PolynomialTimeOverhead clockOuter)
(hInner : PolynomialTimeOverhead clockInner)
:
PolynomialTimeOverhead fun (program : List Bool) (sourceTime : ℕ) =>
clockOuter (compileInner program) (clockInner program sourceTime)
theorem
Complexity.TM.efficientlyUniversalFor_isUniversal_internal
{firstTapes : ℕ}
{simulator : TM firstTapes}
{admissible : TimeOverhead → Prop}
(h : simulator.IsEfficientlyUniversalFor admissible)
:
simulator.IsUniversal
theorem
Complexity.TM.efficientlyUniversalFor_mono_internal
{firstTapes : ℕ}
{simulator : TM firstTapes}
{firstPolicy secondPolicy : TimeOverhead → Prop}
(hpolicy : ∀ (clock : TimeOverhead), firstPolicy clock → secondPolicy clock)
(h : simulator.IsEfficientlyUniversalFor firstPolicy)
:
simulator.IsEfficientlyUniversalFor secondPolicy
theorem
Complexity.TM.simulates_isUniversal_internal
{firstTapes secondTapes : ℕ}
{first : TM firstTapes}
{second : TM secondTapes}
{compile : List Bool → List Bool}
(hcompile : IsComputable compile)
(hsim : first.Simulates second compile)
(huniversal : second.IsUniversal)
:
first.IsUniversal