Documentation

DescriptiveComplexity.Problems.Machine.HaltHard.Sim

The assembled simulation #

The dispatch phase (DescriptiveComplexity.HaltHard.sim_norm) and the six pops of SimRet.lean assemble into the correctness statement of the simulating machine: from the resting configuration of a continuation k and value v, the machine reaches an accepting configuration exactly when the abstract evaluation Turing.ToPartrec.Cont.eval of k on v terminates (DescriptiveComplexity.HaltHard.reach_acc_iff_evalDom).

The two directions meet at DescriptiveComplexity.HaltHard.popTarget, the continuation and value the machine rests at after one pop – Turing.ToPartrec.stepRet, one frame at a time. The machine side is DescriptiveComplexity.HaltHard.cycle_counted: a counted run from rest to the rest of the pop target. Its count is positive whenever the pop dispatches a code – the run factors through a dispatch configuration whose state is not the resting state – and the two pops that may in principle be silent (cons₂, and fix on a zero flag) shrink the continuation instead, so both directions recurse along the lexicographic order on (steps, continuation size): forward on the abstract step count, since those two pops do not consume an abstract step, and backward on the machine step count, split along the cycle by determinism (DescriptiveComplexity.HaltHard.stepsTo_det). The abstract side of each pop is DescriptiveComplexity.HaltHard.stepRet_popTarget, and termination of the abstract machine is traded for termination of Turing.ToPartrec.Cont.eval through Turing.ToPartrec.stepRet_eval.

The pop target #

source
def DescriptiveComplexity.HaltHard.popTarget {c : Turing.ToPartrec.Code} :
PCont c → List ℕ → PCont c × List ℕ

The pop target: the continuation and value the machine rests at after popping the top frame of k with value v – Turing.ToPartrec.stepRet, one frame at a time, with the dispatches it triggers carried out by DescriptiveComplexity.HaltHard.pStepNormal. On the empty continuation the machine accepts instead, so that case is junk.

Equations
Instances For
    Dependency graph
    source
    theorem DescriptiveComplexity.HaltHard.stepRet_popTarget {c : Turing.ToPartrec.Code} {k : PCont c} (hk : k ≠ PCont.halt) (v : List ℕ) :
    Turing.ToPartrec.stepRet k.toCont v = Turing.ToPartrec.Cfg.ret (popTarget k v).1.toCont (popTarget k v).2 ∨ Turing.ToPartrec.stepRet k.toCont v = Turing.ToPartrec.stepRet (popTarget k v).1.toCont (popTarget k v).2 ∧ sizeOf (popTarget k v).1 < sizeOf k

    One abstract step reaches the pop target: Turing.ToPartrec.stepRet on k and v is either the Turing.ToPartrec.Cfg.ret of the pop target – when the pop dispatches a code – or, for the two silent pops, definitionally the stepRet of the pop target, whose continuation is then smaller.

    Dependency graph

    Termination of the abstract machine, as counted runs #

    Transfer of termination along one pop #

    The machine cycle #

    source
    theorem DescriptiveComplexity.HaltHard.cycle_counted {c : Turing.ToPartrec.Code} {k : PCont c} (hk : k ≠ PCont.halt) {fr : List (SimSym c)} (hfr : FrameSeg k fr) (g : ℕ) (v : List ℕ) (j t : ℕ) :
    ∃ (m : ℕ) (g' : ℕ) (fr' : List (SimSym c)) (j' : ℕ) (t' : ℕ), FrameSeg (popTarget k v).1 fr' ∧ stepsTo m (restCfg g fr v j t) (restCfg g' fr' (popTarget k v).2 j' t') ∧ (m = 0 → sizeOf (popTarget k v).1 < sizeOf k)

    The counted machine cycle: from the resting configuration of a nonempty continuation, a counted run to the resting configuration of the pop target. The count is zero only if the pop was silent, in which case the continuation shrank – the decrease both lexicographic inductions fall back on.

    Dependency graph

    The two directions #

    The correctness statement #

    source
    theorem DescriptiveComplexity.HaltHard.reach_acc_iff_evalDom {c : Turing.ToPartrec.Code} {k : PCont c} {fr : List (SimSym c)} (hfr : FrameSeg k fr) (g : ℕ) (v : List ℕ) (j t : ℕ) :
    (∃ (x : LCfg c), x.q = SimQ.acc ∧ Reach (restCfg g fr v j t) x) ↔ (k.toCont.eval v).Dom

    Correctness of the simulating machine: from the resting configuration of a continuation k and value v, the machine reaches an accepting configuration exactly when Turing.ToPartrec.Cont.eval of k on v terminates.

    Dependency graph