Documentation

Linglib.Phonology.Subregular.QF

Quantifier-free position tests #

The quantifier-free apparatus of the subregular program ([Cha14a], [CJ19]): a Subregular.Term walks successor/predecessor steps from a position, and a Subregular.QF formula is a boolean combination of label and definedness tests on such walks. Because successor and predecessor are functions, a term reaches a bounded neighbourhood of its position with no quantifiers — the syntactic source of strict locality. Satisfaction is decidable, and a formula whose walks are backward with depth ≤ r reads only the r + 1 symbols ending at its position (BackBounded.realize_congr). These formulas are the guards of logical transductions (Transduction.lean) and the term language of boolean monadic recursive schemes (BMRS.lean).

Main definitions #

Main results #

Implementation notes #

The logic is monadic — one position variable, so Term.eval takes a position rather than an assignment — since every consumer (transduction guards, BMRS) is; and there is no equality atom: with a single position variable, two walks from one origin agree exactly when both are defined with equal displacement, so equality tests reduce to definedness tests. It is a bespoke syntax rather than a fragment of FirstOrder.Language: over a relational word signature, quantifier-free formulas cannot leave their variables, so bounded-window reach requires successor and predecessor as function symbols — but a mathlib Structure interprets function symbols totally, whereas falling off an edge is the semantics here (defined, initial, final).

Positions #

source
def Subregular.succ? {α : Type u_1} (w : List α) (n : ℕ) :
Option ℕ

Successor as a partial function: the position after n, defined iff it is in range.

Equations
Instances For
    source
    def Subregular.pred? {α : Type u_1} (w : List α) :
    ℕ → Option ℕ

    Predecessor as a partial function: the position before n, defined iff n > 0.

    Equations
    Instances For
      source
      theorem Subregular.succ?_eq_some_iff {α : Type u_1} {w : List α} {n m : ℕ} :
      succ? w n = some m ↔ m = n + 1 ∧ n + 1 < w.length
      source
      theorem Subregular.pred?_eq_some_iff {α : Type u_1} {w : List α} {n m : ℕ} :
      pred? w n = some m ↔ n = m + 1 ∧ m < w.length
      source
      @[simp]
      theorem Subregular.pred?_zero {α : Type u_1} (w : List α) :
      pred? w 0 = none
      source
      theorem Subregular.pred?_of_pos {α : Type u_1} {w : List α} {m : ℕ} (h0 : 0 < m) (hm : m ≤ w.length) :
      pred? w m = some (m - 1)
      source
      theorem Subregular.succ?_congr {α : Type u_1} {w w' : List α} (h : w.length = w'.length) :
      succ? w = succ? w'

      The successor structure depends only on the length.

      source
      theorem Subregular.pred?_congr {α : Type u_1} {w w' : List α} (h : w.length = w'.length) :
      pred? w = pred? w'

      The predecessor structure depends only on the length.

      Walks #

      source
      inductive Subregular.Term :
      Type

      A term: a walk of successor/predecessor steps from the position variable. Chains of succ/pred give bounded-window reach with no quantifier apparatus.

      Instances For
        source
        @[instance_reducible]
        instance Subregular.instDecidableEqTerm :
        DecidableEq Term
        Equations
        source
        def Subregular.instDecidableEqTerm.decEq (x✝ x✝¹ : Term) :
        Decidable (x✝ = x✝¹)
        Equations
        Instances For
          source
          def Subregular.Term.eval {α : Type u_1} (w : List α) (n : ℕ) :
          Term → Option ℕ

          The position a term reads, walking from position n of w; none once the walk falls off an edge.

          Equations
          Instances For
            source
            @[simp]
            theorem Subregular.Term.eval_succ {α : Type u_1} {w : List α} {n : ℕ} {t : Term} :
            eval w n t.succ = (eval w n t).bind (succ? w)
            source
            @[simp]
            theorem Subregular.Term.eval_pred {α : Type u_1} {w : List α} {n : ℕ} {t : Term} :
            eval w n t.pred = (eval w n t).bind (pred? w)
            source
            theorem Subregular.Term.eval_var_eq_some_iff {α : Type u_1} {w : List α} {n v : ℕ} :
            eval w n var = some v ↔ v = n ∧ n < w.length
            source
            @[simp]
            theorem Subregular.Term.eval_var {α : Type u_1} {w : List α} {n : ℕ} (h : n < w.length) :
            eval w n var = some n

            The variable reads its own in-domain position.

            source
            theorem Subregular.Term.eval_lt {α : Type u_1} {w : List α} {n : ℕ} {t : Term} {v : ℕ} :
            eval w n t = some v → v < w.length

            Terms read in-domain positions.

            source
            @[simp]
            theorem Subregular.Term.eval_succ_var {α : Type u_1} {w : List α} {n : ℕ} :
            eval w n var.succ = succ? w n

            A one-step successor walk reads the successor position.

            source
            theorem Subregular.Term.eval_pred_var {α : Type u_1} {w : List α} {n : ℕ} (h : n < w.length) :
            eval w n var.pred = pred? w n

            A one-step predecessor walk reads the predecessor position (in-domain: off the right edge pred? is still defined at w.length but the variable is not).

            source
            theorem Subregular.Term.eval_congr {α : Type u_1} {w w' : List α} {n : ℕ} (hlen : w.length = w'.length) (t : Term) :
            eval w n t = eval w' n t

            Terms read only the length, so their reads transport across equal-length words.

            source
            def Subregular.Term.comp :
            Term → Term → Term

            Substitution: t.comp u walks u first, then t.

            Equations
            Instances For
              source
              theorem Subregular.Term.eval_comp {α : Type u_1} {w : List α} {n : ℕ} (t u : Term) :
              eval w n (t.comp u) = (eval w n u).bind fun (v : ℕ) => eval w v t

              Composite terms read sequenced positions.

              Directed walks #

              source
              def Subregular.Term.Backward :
              Term → Prop

              A term is backward if it uses no successor — only the variable and predecessors, so it reads positions at or before its variable.

              Equations
              Instances For
                source
                def Subregular.Term.Forward :
                Term → Prop

                A term is forward if it uses no predecessor, so it reads positions at or after its variable.

                Equations
                Instances For
                  source
                  def Subregular.Term.pdepth :
                  Term → ℕ

                  The predecessor depth of a term: how far back it reaches.

                  Equations
                  Instances For
                    source
                    @[instance_reducible]
                    instance Subregular.Term.instDecidableBackward (t : Term) :
                    Decidable t.Backward
                    Equations
                    source
                    @[instance_reducible]
                    instance Subregular.Term.instDecidableForward (t : Term) :
                    Decidable t.Forward
                    Equations
                    source
                    theorem Subregular.Term.eval_le_of_backward {α : Type u_1} {w : List α} {n : ℕ} {t : Term} :
                    t.Backward → ∀ {v : ℕ}, eval w n t = some v → v ≤ n

                    Backward terms only move left.

                    source
                    theorem Subregular.Term.le_eval_of_forward {α : Type u_1} {w : List α} {n : ℕ} {t : Term} :
                    t.Forward → ∀ {v : ℕ}, eval w n t = some v → n ≤ v

                    Forward terms only move right.

                    source
                    theorem Subregular.Term.eval_backward {α : Type u_1} {w : List α} {n : ℕ} (hn : n < w.length) {t : Term} :
                    t.Backward → eval w n t = if t.pdepth ≤ n then some (n - t.pdepth) else none

                    A backward term of predecessor depth j, read from an in-range position n, reads exactly position n - j — defined iff j ≤ n.

                    Quantifier-free formulas #

                    source
                    inductive Subregular.QF (α : Type u_2) :
                    Type u_2

                    A quantifier-free formula: a boolean combination of label and definedness tests on term walks from a single position.

                    Instances For
                      source
                      def Subregular.QF.Realize {α : Type u_1} (w : List α) (n : ℕ) :
                      QF α → Prop

                      Satisfaction of a formula at position n of w; tests on an undefined walk are false.

                      Equations
                      Instances For
                        source
                        @[instance_reducible]
                        instance Subregular.QF.instDecidableRealize {α : Type u_1} [DecidableEq α] (w : List α) (n : ℕ) (φ : QF α) :
                        Decidable (Realize w n φ)
                        Equations
                        source
                        def Subregular.QF.initial {α : Type u_1} (t : Term) :
                        QF α

                        t reads an initial position: in-domain with no predecessor.

                        Equations
                        Instances For
                          source
                          def Subregular.QF.final {α : Type u_1} (t : Term) :
                          QF α

                          t reads a final position: in-domain with no successor.

                          Equations
                          Instances For

                            Backward-bounded formulas read only a left window #

                            source
                            def Subregular.QF.BackBounded {α : Type u_1} (r : ℕ) :
                            QF α → Prop

                            A formula is backward-bounded by r if every term it uses is backward with predecessor depth ≤ r, so it reads only the r + 1 positions ending at its own.

                            Equations
                            Instances For
                              source
                              theorem Subregular.QF.BackBounded.realize_congr {α : Type u_1} {r : ℕ} {w w' : List α} {n n' : ℕ} (hn : n < w.length) (hn' : n' < w'.length) (hlbl : ∀ (j : ℕ), j ≤ r → w[n - j]? = w'[n' - j]?) (hedge : ∀ (j : ℕ), j ≤ r → (j ≤ n ↔ j ≤ n')) {φ : QF α} :
                              BackBounded r φ → (Realize w n φ ↔ Realize w' n' φ)

                              A backward-bounded formula reads only the r + 1 symbols ending at its position: it has the same truth value at (w, n) and (w', n') whenever their bounded left contexts — the labels at offsets 0 … r, and which of those offsets stay in range — agree.

                              Worked example #

                              source
                              @[instance_reducible]
                              instance Subregular.instDecidableEqSym :
                              DecidableEq Subregular.Sym✝
                              Equations