Langlib

Langlib.Automata.LinearBounded.CertifiedRowSystem.LBA

Linear-bounded automata as certified row systems #

This file presents the computation graph of a marker-free nondeterministic LBA as a CertifiedRowSystem. A configuration is represented by one row of cells. The control state is repeated in every cell and a Boolean marks the unique head position; this makes one LBA step checkable by a finite left-to-right scan.

source
inductive LBA.RowCell (I : Type u_4) (Γ : Type u_5) (Λ : Type u_6) :
Type (max (max u_4 u_5) u_6)

A raw input cell, or one cell of an encoded LBA configuration. Configuration rows repeat the control state in every cell and mark the unique head position with head = true.

Instances For
    source
    def LBA.instDecidableEqRowCell.decEq {I✝ : Type u_4} {Γ✝ : Type u_5} {Λ✝ : Type u_6} [DecidableEq I✝] [DecidableEq Γ✝] [DecidableEq Λ✝] (x✝ x✝¹ : RowCell I✝ Γ✝ Λ✝) :
    Decidable (x✝ = x✝¹)
    Equations
    Instances For
      source
      instance LBA.instDecidableEqRowCell {I✝ : Type u_4} {Γ✝ : Type u_5} {Λ✝ : Type u_6} [DecidableEq I✝] [DecidableEq Γ✝] [DecidableEq Λ✝] :
      DecidableEq (RowCell I✝ Γ✝ Λ✝)
      Equations
      source
      instance LBA.instFintypeRowCell {I : Type u_1} {Γ : Type u_2} {Λ : Type u_3} [Fintype I] [Fintype Γ] [Fintype Λ] :
      Fintype (RowCell I Γ Λ)
      Equations
      • One or more equations did not get rendered due to their size.
      source
      inductive LBA.RowCert :
      Type

      A certificate only has to identify the direction used at the source head.

      Instances For
        source
        def LBA.instDecidableEqRowCert.decEq (x✝ x✝¹ : RowCert) :
        Decidable (x✝ = x✝¹)
        Equations
        Instances For
          source
          instance LBA.instDecidableEqRowCert :
          DecidableEq RowCert
          Equations
          source
          instance LBA.instFintypeRowCert :
          Fintype RowCert
          Equations
          source
          inductive LBA.RowScan (Λ : Type u_4) :
          Type u_4

          State of the left-to-right verifier for one row transition.

          Instances For
            source
            instance LBA.instDecidableEqRowScan {Λ✝ : Type u_4} [DecidableEq Λ✝] :
            DecidableEq (RowScan Λ✝)
            Equations
            source
            def LBA.instDecidableEqRowScan.decEq {Λ✝ : Type u_4} [DecidableEq Λ✝] (x✝ x✝¹ : RowScan Λ✝) :
            Decidable (x✝ = x✝¹)
            Equations
            Instances For
              source
              instance LBA.instFintypeRowScan {Λ : Type u_3} [Fintype Λ] :
              Fintype (RowScan Λ)
              Equations
              • One or more equations did not get rendered due to their size.
              source
              inductive LBA.RowFinal (Λ : Type u_4) :
              Type u_4

              State of the regular accepting-row checker.

              Instances For
                source
                instance LBA.instDecidableEqRowFinal {Λ✝ : Type u_4} [DecidableEq Λ✝] :
                DecidableEq (RowFinal Λ✝)
                Equations
                source
                def LBA.instDecidableEqRowFinal.decEq {Λ✝ : Type u_4} [DecidableEq Λ✝] (x✝ x✝¹ : RowFinal Λ✝) :
                Decidable (x✝ = x✝¹)
                Equations
                Instances For
                  source
                  instance LBA.instFintypeRowFinal {Λ : Type u_3} [Fintype Λ] :
                  Fintype (RowFinal Λ)
                  Equations
                  • One or more equations did not get rendered due to their size.
                  source
                  noncomputable def LBA.RowScan.transitionOK {Γ : Type u_2} {Λ : Type u_3} (M : Machine Γ Λ) (q : Λ) (a : Γ) (q' : Λ) (b : Γ) (d : DLBA.Dir) :
                  Bool
                  Equations
                  Instances For
                    source
                    noncomputable def LBA.RowScan.scanFirst {Γ : Type u_2} {Λ : Type u_3} (M : Machine Γ Λ) (a : Γ) (h : Bool) (q : Λ) (b : Γ) (h' : Bool) (q' : Λ) (cert : RowCert) :
                    RowScan Λ

                    Scan the first pair of configuration cells.

                    Equations
                    Instances For
                      source
                      noncomputable def LBA.RowScan.scanBefore {Γ : Type u_2} {Λ : Type u_3} (M : Machine Γ Λ) (q q' : Λ) (a : Γ) (h : Bool) (r : Λ) (b : Γ) (h' : Bool) (r' : Λ) (cert : RowCert) :
                      RowScan Λ

                      Scan a pair strictly before the source head.

                      Equations
                      Instances For
                        source
                        noncomputable def LBA.RowScan.scanCell {I : Type u_1} {Γ : Type u_2} {Λ : Type u_3} [DecidableEq I] [DecidableEq Γ] [DecidableEq Λ] (M : Machine Γ Λ) (embed : I → Γ) :
                        RowScan Λ → RowCell I Γ Λ → RowCell I Γ Λ → RowCert → RowScan Λ

                        The cellwise verifier. Interior left and right moves use one pending scanner state so the destination head is checked on the adjacent cell.

                        Equations
                        Instances For
                          source
                          def LBA.RowScan.done {Λ : Type u_3} :
                          RowScan Λ → Bool
                          Equations
                          Instances For
                            source
                            def LBA.RowFinal.next {I : Type u_1} {Γ : Type u_2} {Λ : Type u_3} [DecidableEq Λ] :
                            RowFinal Λ → RowCell I Γ Λ → RowFinal Λ
                            Equations
                            Instances For
                              source
                              def LBA.RowFinal.done {Γ : Type u_2} {Λ : Type u_3} (M : Machine Γ Λ) :
                              RowFinal Λ → Bool
                              Equations
                              Instances For
                                source
                                noncomputable def LBA.certifiedRowSystem {I : Type u_1} {Γ : Type u_2} {Λ : Type u_3} [DecidableEq I] [DecidableEq Γ] [DecidableEq Λ] (M : Machine Γ Λ) (embed : I → Γ) :
                                CertifiedRowSystem I (RowCell I Γ Λ) RowCert (RowScan Λ) (RowFinal Λ)

                                The certified row system whose reachable rows are precisely the configurations reachable by M from the canonically embedded, nonempty input.

                                Equations
                                • One or more equations did not get rendered due to their size.
                                Instances For
                                  source
                                  @[simp]
                                  theorem LBA.certifiedRowSystem_stepCell {I : Type u_1} {Γ : Type u_2} {Λ : Type u_3} [DecidableEq I] [DecidableEq Γ] [DecidableEq Λ] (M : Machine Γ Λ) (embed : I → Γ) :
                                  (certifiedRowSystem M embed).stepCell = RowScan.scanCell M embed
                                  source
                                  @[simp]
                                  theorem LBA.certifiedRowSystem_stepDone {I : Type u_1} {Γ : Type u_2} {Λ : Type u_3} [DecidableEq I] [DecidableEq Γ] [DecidableEq Λ] (M : Machine Γ Λ) (embed : I → Γ) :
                                  (certifiedRowSystem M embed).stepDone = RowScan.done
                                  source
                                  @[simp]
                                  theorem LBA.certifiedRowSystem_finalCell {I : Type u_1} {Γ : Type u_2} {Λ : Type u_3} [DecidableEq I] [DecidableEq Γ] [DecidableEq Λ] (M : Machine Γ Λ) (embed : I → Γ) :
                                  (certifiedRowSystem M embed).finalCell = RowFinal.next
                                  source
                                  @[simp]
                                  theorem LBA.certifiedRowSystem_finalDone {I : Type u_1} {Γ : Type u_2} {Λ : Type u_3} [DecidableEq I] [DecidableEq Γ] [DecidableEq Λ] (M : Machine Γ Λ) (embed : I → Γ) :
                                  (certifiedRowSystem M embed).finalDone = RowFinal.done M

                                  Semantic row relations #

                                  source
                                  def LBA.noHeadCells {I : Type u_1} {Γ : Type u_2} {Λ : Type u_3} (q : Λ) (xs : List Γ) :
                                  List (RowCell I Γ Λ)

                                  A block of non-head configuration cells carrying the same control state.

                                  Equations
                                  Instances For
                                    source
                                    inductive LBA.RowMove {I : Type u_1} {Γ : Type u_2} {Λ : Type u_3} (M : Machine Γ Λ) (embed : I → Γ) :
                                    List (RowCell I Γ Λ) → List (RowCell I Γ Λ) → Prop

                                    The intended semantic transition between rows.

                                    Instances For
                                      source
                                      theorem LBA.certifiedRowSystem_rowStep_iff {I : Type u_1} {Γ : Type u_2} {Λ : Type u_3} [DecidableEq I] [DecidableEq Γ] [DecidableEq Λ] (M : Machine Γ Λ) (embed : I → Γ) (old new : List (RowCell I Γ Λ)) :
                                      (certifiedRowSystem M embed).RowStep old new ↔ RowMove M embed old new

                                      The local scanner accepts exactly the intended raw initialization or one LBA row move.

                                      Bisimulation with bounded-tape configurations #

                                      source
                                      def LBA.configCells {I : Type u_1} {Γ : Type u_2} {Λ : Type u_3} (q : Λ) (left : List Γ) (a : Γ) (right : List Γ) :
                                      List (RowCell I Γ Λ)

                                      A well-formed configuration row, split immediately before and after its unique head.

                                      Equations
                                      Instances For
                                        source
                                        def LBA.tapeList {Γ : Type u_2} {Λ : Type u_3} {n : ℕ} (cfg : DLBA.Cfg Γ Λ n) :
                                        List Γ

                                        The tape contents of a bounded configuration as an ordinary list.

                                        Equations
                                        Instances For
                                          source
                                          def LBA.leftSymbols {Γ : Type u_2} {Λ : Type u_3} {n : ℕ} (cfg : DLBA.Cfg Γ Λ n) :
                                          List Γ

                                          Symbols strictly to the left of the head.

                                          Equations
                                          Instances For
                                            source
                                            def LBA.rightSymbols {Γ : Type u_2} {Λ : Type u_3} {n : ℕ} (cfg : DLBA.Cfg Γ Λ n) :
                                            List Γ

                                            Symbols strictly to the right of the head.

                                            Equations
                                            Instances For
                                              source
                                              def LBA.configRow {I : Type u_1} {Γ : Type u_2} {Λ : Type u_3} {n : ℕ} (cfg : DLBA.Cfg Γ Λ n) :
                                              List (RowCell I Γ Λ)

                                              Canonical row encoding of a bounded-tape configuration.

                                              Equations
                                              Instances For
                                                source
                                                @[simp]
                                                theorem LBA.configRow_length {I : Type u_1} {Γ : Type u_2} {Λ : Type u_3} {n : ℕ} (cfg : DLBA.Cfg Γ Λ n) :
                                                (configRow cfg).length = n + 1
                                                source
                                                theorem LBA.rowMove_configRow_of_step {I : Type u_1} {Γ : Type u_2} {Λ : Type u_3} [DecidableEq I] [DecidableEq Γ] [DecidableEq Λ] (M : Machine Γ Λ) (embed : I → Γ) {n : ℕ} {cfg cfg' : DLBA.Cfg Γ Λ n} (hstep : Step M cfg cfg') :
                                                RowMove M embed (configRow cfg) (configRow cfg')

                                                Every bounded-tape LBA step is represented by one semantic row move.

                                                source
                                                theorem LBA.step_of_rowMove_configRow {I : Type u_1} {Γ : Type u_2} {Λ : Type u_3} [DecidableEq I] [DecidableEq Γ] [DecidableEq Λ] (M : Machine Γ Λ) (embed : I → Γ) {n : ℕ} (cfg : DLBA.Cfg Γ Λ n) {row : List (RowCell I Γ Λ)} (hmove : RowMove M embed (configRow cfg) row) :
                                                ∃ (cfg' : DLBA.Cfg Γ Λ n), Step M cfg cfg' ∧ row = configRow cfg'

                                                Soundness of semantic row moves from a well-formed configuration row.

                                                source
                                                @[simp]
                                                theorem LBA.certifiedRowSystem_final_configRow_iff {I : Type u_1} {Γ : Type u_2} {Λ : Type u_3} [DecidableEq I] [DecidableEq Γ] [DecidableEq Λ] (M : Machine Γ Λ) (embed : I → Γ) {n : ℕ} (cfg : DLBA.Cfg Γ Λ n) :
                                                (certifiedRowSystem M embed).Final (configRow cfg) ↔ M.accept cfg.state = true

                                                A canonical configuration row is final exactly when its LBA state is accepting.

                                                source
                                                theorem LBA.configRow_initCfgList {I : Type u_1} {Γ : Type u_2} {Λ : Type u_3} (M : Machine Γ Λ) (embed : I → Γ) (i : I) (is : List I) (hw : List.map embed (i :: is) ≠ []) :
                                                configRow (initCfgList M (List.map embed (i :: is)) hw) = RowCell.cfg (embed i) true M.initial :: noHeadCells M.initial (List.map embed is)

                                                The canonical initial configuration row is the initialization target of the raw input row.

                                                source
                                                theorem LBA.rowReach_configRow_of_reaches {I : Type u_1} {Γ : Type u_2} {Λ : Type u_3} [DecidableEq I] [DecidableEq Γ] [DecidableEq Λ] (M : Machine Γ Λ) (embed : I → Γ) {n : ℕ} {cfg cfg' : DLBA.Cfg Γ Λ n} (hreach : Reaches M cfg cfg') :
                                                Relation.ReflTransGen (certifiedRowSystem M embed).RowStep (configRow cfg) (configRow cfg')

                                                Lift an LBA run pointwise to the certified row relation.

                                                source
                                                theorem LBA.certifiedRowSystem_rowReachLanguage {I : Type u_1} {Γ : Type u_2} {Λ : Type u_3} [DecidableEq I] [DecidableEq Γ] [DecidableEq Λ] (M : Machine Γ Λ) (embed : I → Γ) :
                                                (certifiedRowSystem M embed).rowReachLanguage = LanguageViaEmbed M embed

                                                The certified row system presents exactly the nonempty language of the original LBA.