Documentation

DescriptiveComplexity.Problems.Wide.DrawStageAtom

The stage atom's machinery: a random access #

The largest atom subroutine of the EXPSPACE program: to evaluate a stage atom R i' (w̄), the machine saves its mirror, builds the target address – one tuple loop per argument position, copying the source block of VAL or MIRROR into the target's block by named bits – resets to the bottom and seeks the target, reads the stage bit under the head, and comes back: restore the target from the save, reset, seek home.

The sites: two DescriptiveComplexity.Draw.CopyKit trips (save and restore), a DescriptiveComplexity.Draw.ClearKit trip (the target's blocks not written by any loop), the per-argument DescriptiveComplexity.Draw.tupleRule loops chained head to tail, two DescriptiveComplexity.Draw.ResetKit+ClearKit pairs with their erasing entry checkpoints, and two DescriptiveComplexity.Draw.SeekKit instances – the first's verdict exits are the read under the head, branching on the stage track's digit at the sought cell and storing it into the control.

As everywhere in the assembly, the semantic parameters – the loop-variable updates, the stored-bit updates, the verdict store – are dstSt/guard parameters; the shapes and their separation are what this file fixes.

The shapes #

source
inductive DescriptiveComplexity.Draw.StagePh (k : ℕ) :
Type

The phases of a stage atom's machinery.

Instances For
    Dependency graph
    source
    inductive DescriptiveComplexity.Draw.StageSite (k : ℕ) :
    Type

    The sites of a stage atom's machinery.

    Instances For
      Dependency graph
      source
      def DescriptiveComplexity.Draw.StageSh (k : ℕ) :
      StageSite k → Type

      The rule shape of each site.

      Equations
      Instances For
        Dependency graph
        source
        def DescriptiveComplexity.Draw.stageOwn {k : ℕ} :
        StagePh k → StageSite k

        The owner of each phase of a stage atom's machinery.

        Equations
        Instances For
          Dependency graph
          source
          def DescriptiveComplexity.Draw.Data.stageFirstTup {P : Type} {k : ℕ} (emb : StagePh k → P) :
          P

          The phase entering the loops, or the first reset checkpoint when there is no argument.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            Dependency graph
            source
            def DescriptiveComplexity.Draw.Data.stageNextTup {P : Type} {k : ℕ} (emb : StagePh k → P) (ℓ : Fin k) :
            P

            The phase after the ℓ-th loop.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              Dependency graph
              source
              noncomputable def DescriptiveComplexity.Draw.Data.stageRule {L : FirstOrder.Language} (dt : Data L) {A Q P : Type} {k : ℕ} (zero one : A) (emb : StagePh k → P) (srcTrack : Fin k → dt.SlotIx) (srcBlk dstBlk : Fin k → Fin dt.ko ⊕ Fin dt.ki) (coord : Fin dt.dd0 → Q) (bitFlag : (Q → A) → Prop) (setBit : Bool → (Q → A) → (dt.SlotIx → A) → Q → A) (initLv advLv : (Q → A) → (dt.SlotIx → A) → Q → A) (IsMaxLv : (Q → A) → Prop) (oldSlot : dt.SlotIx) (setAv : Bool → (Q → A) → (dt.SlotIx → A) → Q → A) (exitPh : P) (i : StageSite k) :
              StageSh k i → Rule A Q dt.SlotIx P

              The rules of a stage atom's machinery.

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                Dependency graph