Documentation

Complexitylib.Models.RandomAccessMachine.Simulation.RegisterStore.Machine.EntryEncode.Defs

Sparse entry emission — definitions #

source
structure Complexity.RAM.RegisterStore.Machine.EntryEncodeTapes (n : ℕ) :
Type

Distinct decoded address and value tapes used to emit one sparse entry.

  • address : Fin n

    Decoded address source.

  • value : Fin n

    Decoded value source.

  • ne : self.address ≠ self.value

    The address and value sources are distinct.

Instances For
    source
    def Complexity.RAM.RegisterStore.Machine.entryEncodeTM {n : ℕ} (tapes : EntryEncodeTapes n) :
    TM n

    Emit one address/value entry as two consecutive self-delimiting words.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      def Complexity.RAM.RegisterStore.Machine.entryEncodeTime (entry : Entry) :
      ℕ

      Compositional time bound for one encoded entry.

      Equations
      Instances For
        source
        def Complexity.RAM.RegisterStore.Machine.rewindEntryEncodeTM {n : ℕ} (tapes : EntryEncodeTapes n) :
        TM n

        Rewind arbitrary decoded address/value cursors and emit the entry.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          def Complexity.RAM.RegisterStore.Machine.rewindEntryEncodeTime (entry : Entry) (addressHeadBound valueHeadBound : ℕ) :
          ℕ

          Composition bound for emitting an entry from arbitrary bounded cursors.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            def Complexity.RAM.RegisterStore.Machine.rewindEntryEncodeRestoreTM {n : ℕ} (tapes : EntryEncodeTapes n) :
            TM n

            Emit an entry from canonical sources and restore both source heads to cell one.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              source
              def Complexity.RAM.RegisterStore.Machine.rewindEntryEncodeRestoreTime (entry : Entry) :
              ℕ

              Compositional bound for entry emission followed by two-source restore.

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