Documentation

Linglib.Phonology.Subregular.WindowFormula

Quantifier-free position tests #

A Subregular.Walk walks successor and predecessor steps from a position, and a Subregular.WindowFormula 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 Walk.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).

References #

Positions #

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

The successor of n is the position after it, defined iff it is in range.

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

    The predecessor of n is the position before it, 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.Walk :
      Type

      A term is a walk of successor and predecessor steps from the position variable. Chains of succ and pred reach a bounded window with no quantifier.

      Instances For
        source
        @[instance_reducible]
        instance Subregular.instDecidableEqWalk :
        DecidableEq Walk
        Equations
        source
        def Subregular.instDecidableEqWalk.decEq (x✝ x✝¹ : Walk) :
        Decidable (x✝ = x✝¹)
        Equations
        Instances For
          source
          def Subregular.Walk.eval {α : Type u_1} (w : List α) (n : ℕ) :
          Walk → 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.Walk.eval_succ {α : Type u_1} {w : List α} {n : ℕ} {t : Walk} :
            eval w n t.succ = (eval w n t).bind (succ? w)
            source
            @[simp]
            theorem Subregular.Walk.eval_pred {α : Type u_1} {w : List α} {n : ℕ} {t : Walk} :
            eval w n t.pred = (eval w n t).bind (pred? w)
            source
            theorem Subregular.Walk.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.Walk.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.Walk.eval_lt {α : Type u_1} {w : List α} {n : ℕ} {t : Walk} {v : ℕ} :
            eval w n t = some v → v < w.length

            Terms read in-domain positions.

            source
            @[simp]
            theorem Subregular.Walk.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.Walk.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, since off the right edge pred? is still defined at w.length but the variable is not).

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

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

            source
            def Subregular.Walk.comp :
            Walk → Walk → Walk

            The substitution t.comp u walks u first, then t.

            Equations
            Instances For
              source
              theorem Subregular.Walk.eval_comp {α : Type u_1} {w : List α} {n : ℕ} (t u : Walk) :
              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.Walk.Backward :
              Walk → 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.Walk.Forward :
                Walk → 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.Walk.pdepth :
                  Walk → ℕ

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

                  Equations
                  Instances For
                    source
                    def Subregular.Walk.sdepth :
                    Walk → ℕ

                    The successor depth of a term is how far forward it reaches.

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

                      Backward terms only move left.

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

                      Forward terms only move right.

                      source
                      theorem Subregular.Walk.eval_backward {α : Type u_1} {w : List α} {n : ℕ} (hn : n < w.length) {t : Walk} :
                      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.

                      Bounded windows #

                      source
                      theorem Subregular.Walk.le_eval_add_pdepth {α : Type u_1} {w : List α} {n : ℕ} {t : Walk} {v : ℕ} :
                      eval w n t = some v → n ≤ v + t.pdepth

                      A walk reaches at most pdepth back.

                      source
                      theorem Subregular.Walk.eval_le_add_sdepth {α : Type u_1} {w : List α} {n : ℕ} {t : Walk} {v : ℕ} :
                      eval w n t = some v → v ≤ n + t.sdepth

                      A walk reaches at most sdepth forward.

                      source
                      theorem Subregular.Walk.eval_bounded {α : Type u_1} {w w' : List α} {n l r n' : ℕ} (hn : n < w.length) (hn' : n' < w'.length) (hleft : ∀ (j : ℕ), j ≤ l → (j ≤ n ↔ j ≤ n')) (hright : ∀ (j : ℕ), j ≤ r → (n + j < w.length ↔ n' + j < w'.length)) {t : Walk} :
                      t.pdepth ≤ l → t.sdepth ≤ r → (Option.map (fun (v : Int) => v - ↑n) do let a ← eval w n t pure ↑a) = Option.map (fun (v : Int) => v - ↑n') do let a ← eval w' n' t pure ↑a

                      Window transport. From two in-range positions whose windows l back and r forward have the same edges — an offset stays in range at one exactly when it does at the other — a walk reaching at most l back and r forward reads the same displacement, or falls off at both.

                      Quantifier-free formulas #

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

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

                      Instances For
                        source
                        def Subregular.WindowFormula.Realize {α : Type u_1} (w : List α) (n : ℕ) :
                        WindowFormula α → 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.WindowFormula.instDecidableRealize {α : Type u_1} [DecidableEq α] (w : List α) (n : ℕ) (φ : WindowFormula α) :
                          Decidable (Realize w n φ)
                          Equations
                          source
                          def Subregular.WindowFormula.initial {α : Type u_1} (t : Walk) :
                          WindowFormula α

                          t reads an initial position, one in the domain with no predecessor.

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

                            t reads a final position, one in the domain with no successor.

                            Equations
                            Instances For

                              Bounded formulas read only a window #

                              source
                              def Subregular.WindowFormula.Bounded {α : Type u_1} (l r : ℕ) :
                              WindowFormula α → Prop

                              A formula is bounded by l back and r forward if every walk it uses reaches at most l positions back and r forward, so it reads only the window from l before its position to r after.

                              Equations
                              Instances For
                                source
                                @[instance_reducible]
                                instance Subregular.WindowFormula.instDecidableBounded {α : Type u_1} (l r : ℕ) (φ : WindowFormula α) :
                                Decidable (Bounded l r φ)
                                Equations
                                source
                                @[reducible, inline]
                                abbrev Subregular.WindowFormula.BackBounded {α : Type u_1} (r : ℕ) (φ : WindowFormula α) :
                                Prop

                                A formula is backward-bounded by r if it reads only the r + 1 positions ending at its own, bounded by r back and nothing forward.

                                Equations
                                Instances For
                                  source
                                  theorem Subregular.WindowFormula.Bounded.realize_congr {α : Type u_1} {l r : ℕ} {w w' : List α} {n n' : ℕ} (hn : n < w.length) (hn' : n' < w'.length) (hleft : ∀ (j : ℕ), j ≤ l → (j ≤ n ↔ j ≤ n') ∧ (j ≤ n → w[n - j]? = w'[n' - j]?)) (hright : ∀ (j : ℕ), j ≤ r → (n + j < w.length ↔ n' + j < w'.length) ∧ w[n + j]? = w'[n' + j]?) {φ : WindowFormula α} :
                                  Bounded l r φ → (Realize w n φ ↔ Realize w' n' φ)

                                  A bounded formula reads only its window: it has the same truth value at (w, n) and (w', n') whenever the windows l back and r forward agree — the same labels at each offset, and the same offsets in range.

                                  source
                                  theorem Subregular.WindowFormula.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')) {φ : WindowFormula α} :
                                  BackBounded r φ → (Realize w n φ ↔ Realize w' n' φ)

                                  A backward-bounded formula reads only the r + 1 symbols ending at its position.

                                  Worked example #