Langlib

Langlib.Grammars.Indexed.NormalForm.Aho.Machine.Alphabet

Aho machine alphabet #

Finite marks, work symbols, and their basic structural properties.

The finite marked work alphabet #

source
inductive IndexedGrammar.Aho.IndexMark :
Type

Aho's four marks on a compressed index.

firstPending/firstUsed are the paper's marks 0/1, and laterPending/laterUsed are marks 2/3. "Used" means that a productive terminal or binary event has occurred since the represented index was consumed, so the index may be erased.

Instances For
    source
    instance IndexedGrammar.Aho.instDecidableEqIndexMark :
    DecidableEq IndexMark
    Equations
    source
    instance IndexedGrammar.Aho.instFintypeIndexMark :
    Fintype IndexMark
    Equations
    • One or more equations did not get rendered due to their size.
    source
    def IndexedGrammar.Aho.IndexMark.markUsed :
    IndexMark → IndexMark

    Mark the productive use of an index (Aho's operation alpha ↦ alpha⁺).

    Equations
    Instances For
      source
      def IndexedGrammar.Aho.IndexMark.erasable :
      IndexMark → Bool

      Marks 1 and 3 are precisely the erasable marks.

      Equations
      Instances For
        source
        def IndexedGrammar.Aho.IndexMark.later :
        IndexMark → Bool

        Marks 2 and 3 denote an index which is not the first consumed index of the current copied stack. Only these marks permit Aho's primed continuation after a pop.

        Equations
        Instances For
          source
          @[simp]
          theorem IndexedGrammar.Aho.IndexMark.markUsed_firstPending :
          firstPending.markUsed = firstUsed
          source
          @[simp]
          theorem IndexedGrammar.Aho.IndexMark.markUsed_firstUsed :
          firstUsed.markUsed = firstUsed
          source
          @[simp]
          theorem IndexedGrammar.Aho.IndexMark.markUsed_laterPending :
          laterPending.markUsed = laterUsed
          source
          @[simp]
          theorem IndexedGrammar.Aho.IndexMark.markUsed_laterUsed :
          laterUsed.markUsed = laterUsed
          source
          @[simp]
          theorem IndexedGrammar.Aho.IndexMark.erasable_markUsed (d : IndexMark) :
          d.markUsed.erasable = true
          source
          inductive IndexedGrammar.Aho.WorkSym {T : Type} (g : IndexedGrammar T) :
          Type

          A symbol of Aho's unpadded logical work tape.

          plain A is the paper's A, while live A is A': at least one compressed index to its right is promised to be consumed during the expansion of this occurrence.

          Instances For
            source
            noncomputable instance IndexedGrammar.Aho.WorkSym.instDecidableEq {T : Type} {g : IndexedGrammar T} :
            DecidableEq (WorkSym g)
            Equations
            source
            noncomputable instance IndexedGrammar.Aho.WorkSym.instFintype {T : Type} {g : IndexedGrammar T} [Fintype T] [Fintype g.nt] :
            Fintype (WorkSym g)
            Equations
            • One or more equations did not get rendered due to their size.
            source
            def IndexedGrammar.Aho.WorkSym.isIndex {T : Type} {g : IndexedGrammar T} :
            WorkSym g → Bool

            Does a work symbol carry a compressed index?

            Equations
            Instances For
              source
              def IndexedGrammar.Aho.WorkSym.isDollar {T : Type} {g : IndexedGrammar T} :
              WorkSym g → Bool

              Is a work symbol a $ frame opener?

              Equations
              Instances For
                source
                def IndexedGrammar.Aho.IndexFree {T : Type} {g : IndexedGrammar T} (xs : List (WorkSym g)) :
                Prop

                A list contains no compressed-index symbol.

                Equations
                Instances For
                  source
                  def IndexedGrammar.Aho.DollarFree {T : Type} {g : IndexedGrammar T} (xs : List (WorkSym g)) :
                  Prop

                  A list contains no $ frame opener.

                  Equations
                  Instances For
                    source
                    def IndexedGrammar.Aho.markProductivePrefix {T : Type} {g : IndexedGrammar T} (alpha : List (WorkSym g)) :
                    List (WorkSym g)

                    Mark the rightmost symbol of alpha if it is a compressed index. This is exactly the operation written alpha⁺ by Aho.

                    Equations
                    • One or more equations did not get rendered due to their size.
                    Instances For
                      source
                      @[simp]
                      theorem IndexedGrammar.Aho.markProductivePrefix_nil {T : Type} {g : IndexedGrammar T} :
                      markProductivePrefix [] = []
                      source
                      @[simp]
                      theorem IndexedGrammar.Aho.markProductivePrefix_append_index {T : Type} {g : IndexedGrammar T} (alpha : List (WorkSym g)) (R : CFlag g) (d : IndexMark) :
                      markProductivePrefix (alpha ++ [WorkSym.index R d]) = alpha ++ [WorkSym.index R d.markUsed]
                      source
                      @[simp]
                      theorem IndexedGrammar.Aho.markProductivePrefix_append_nonindex {T : Type} {g : IndexedGrammar T} (alpha : List (WorkSym g)) (z : WorkSym g) (hz : ∀ (R : CFlag g) (d : IndexMark), z ≠ WorkSym.index R d) :
                      markProductivePrefix (alpha ++ [z]) = alpha ++ [z]