Documentation

Linglib.Phonology.Subregular.BMRS

Boolean monadic recursive schemes #

A boolean monadic recursive scheme (BMRS) is a program of mutually recursive boolean-valued unary predicates over words, built from if…then…else, the edge tests min and max, input class tests, and calls of the program's rule heads. Its one-sided fragments characterize the left- and right-subsequential functions, a characterization later extended to the rational functions and applied to phonological analysis.

Input labels α get the lookup rule and rule heads F the unfolding rule, so a Program is a total map F → Expr α F. Eval is the derivation system w, i ⊢_P e → b. It is partial: a program that does not halt derives nothing. Program.approx computes it in rounds, each rerunning every rule body against the values the previous rounds found, and on a word of length n the rounds settle by round card F * n, so evaluation is decidable.

Main definitions #

Main statements #

Implementation notes #

References #

Syntax #

source
inductive Subregular.BMRS.Expr (α : Type u_3) (F : Type u_4) :
Type (max u_3 u_4)

A BMRS expression is an edge test initial or final (the literature's min(T), max(T)), an input class test label (the lookup rule, over a Finset of symbols, so that featural predicates like V or N are single atoms), a rule-head call call (the unfolding rule), or an if…then…else.

Instances For
    source
    def Subregular.BMRS.instDecidableEqExpr.decEq {α✝ : Type u_3} {F✝ : Type u_4} [DecidableEq α✝] [DecidableEq F✝] (x✝ x✝¹ : Expr α✝ F✝) :
    Decidable (x✝ = x✝¹)
    Equations
    Instances For
      source
      @[instance_reducible]
      instance Subregular.BMRS.instDecidableEqExpr {α✝ : Type u_3} {F✝ : Type u_4} [DecidableEq α✝] [DecidableEq F✝] :
      DecidableEq (Expr α✝ F✝)
      Equations
      source
      @[reducible, inline]
      abbrev Subregular.BMRS.Program (α : Type u_3) (F : Type u_4) :
      Type (max u_4 u_3)

      A BMRS program assigns one defining expression to each rule head.

      Equations
      Instances For
        source
        def Subregular.BMRS.Expr.and {α : Type u_1} {F : Type u_2} (e₁ e₂ : Expr α F) :
        Expr α F

        Conjunction as if…then…else.

        Equations
        Instances For
          source
          def Subregular.BMRS.Expr.or {α : Type u_1} {F : Type u_2} (e₁ e₂ : Expr α F) :
          Expr α F

          Disjunction as if…then…else.

          Equations
          Instances For
            source
            def Subregular.BMRS.Expr.not {α : Type u_1} {F : Type u_2} (e : Expr α F) :
            Expr α F

            Negation as if…then…else.

            Equations
            Instances For
              source
              def Subregular.BMRS.Expr.subst {α : Type u_1} {F : Type u_2} :
              Expr α F → Walk → Expr α F

              e.subst u substitutes the term u for the variable throughout e, the e[u/x] that the μ-calculus translation writes tr(φ)[s(x)].

              Equations
              Instances For
                source
                def Subregular.BMRS.Expr.AllWalks {α : Type u_1} {F : Type u_2} (p : Walk → Prop) :
                Expr α F → Prop

                e.AllWalks p holds when every walk occurring in e satisfies p.

                Equations
                Instances For
                  source
                  @[instance_reducible]
                  instance Subregular.BMRS.Expr.instDecidableAllWalks {α : Type u_1} {F : Type u_2} (p : Walk → Prop) [DecidablePred p] (e : Expr α F) :
                  Decidable (AllWalks p e)
                  Equations
                  source
                  def Subregular.BMRS.Program.Backward {α : Type u_1} {F : Type u_2} (P : Program α F) :
                  Prop

                  A program is backward, BMRSᵖ, when the successor occurs in none of its rules.

                  Equations
                  Instances For
                    source
                    def Subregular.BMRS.Program.Forward {α : Type u_1} {F : Type u_2} (P : Program α F) :
                    Prop

                    A program is forward, BMRSˢ, when the predecessor occurs in none of its rules.

                    Equations
                    Instances For
                      source
                      @[instance_reducible]
                      instance Subregular.BMRS.Program.instDecidableBackwardOfFintype {α : Type u_1} {F : Type u_2} [Fintype F] (P : Program α F) :
                      Decidable P.Backward
                      Equations
                      source
                      @[instance_reducible]
                      instance Subregular.BMRS.Program.instDecidableForwardOfFintype {α : Type u_1} {F : Type u_2} [Fintype F] (P : Program α F) :
                      Decidable P.Forward
                      Equations

                      The derivation system #

                      source
                      inductive Subregular.BMRS.Eval {α : Type u_1} {F : Type u_2} (P : Program α F) (w : List α) :
                      ℕ → Expr α F → Bool → Prop

                      Eval P w i e b is the derivation w, i ⊢_P e → b of a BMRS expression. It is partial by design, a non-halting program deriving nothing.

                      Instances For
                        source
                        theorem Subregular.BMRS.Eval.initial {α : Type u_1} {F : Type u_2} {P : Program α F} {w : List α} {i v : ℕ} {t : Walk} (h : Walk.eval w i t = some v) :
                        Eval P w i (Expr.initial t) (decide (v = 0))

                        Boolean-form introduction for the initial test.

                        source
                        theorem Subregular.BMRS.Eval.final {α : Type u_1} {F : Type u_2} {P : Program α F} {w : List α} {i v : ℕ} {t : Walk} (h : Walk.eval w i t = some v) :
                        Eval P w i (Expr.final t) (decide (v = w.length - 1))

                        Boolean-form introduction for the final test.

                        source
                        theorem Subregular.BMRS.Eval.label {α : Type u_1} {F : Type u_2} {P : Program α F} {w : List α} {i v : ℕ} {t : Walk} [DecidableEq α] {s : Finset α} {a : α} (h : Walk.eval w i t = some v) (hl : w[v]? = some a) :
                        Eval P w i (Expr.label s t) (decide (a ∈ s))

                        Boolean-form introduction for the class test.

                        source
                        theorem Subregular.BMRS.Eval.and {α : Type u_1} {F : Type u_2} {P : Program α F} {w : List α} {i : ℕ} {e₁ e₂ : Expr α F} {b₁ b₂ : Bool} (h₁ : Eval P w i e₁ b₁) (h₂ : Eval P w i e₂ b₂) :
                        Eval P w i (e₁.and e₂) (b₁ && b₂)

                        Boolean-form introduction for conjunction.

                        source
                        theorem Subregular.BMRS.Eval.or {α : Type u_1} {F : Type u_2} {P : Program α F} {w : List α} {i : ℕ} {e₁ e₂ : Expr α F} {b₁ b₂ : Bool} (h₁ : Eval P w i e₁ b₁) (h₂ : Eval P w i e₂ b₂) :
                        Eval P w i (e₁.or e₂) (b₁ || b₂)

                        Boolean-form introduction for disjunction.

                        source
                        theorem Subregular.BMRS.Eval.not {α : Type u_1} {F : Type u_2} {P : Program α F} {w : List α} {i : ℕ} {e : Expr α F} {b : Bool} (h : Eval P w i e b) :
                        Eval P w i e.not !b

                        Boolean-form introduction for negation.

                        source
                        theorem Subregular.BMRS.Eval.deterministic {α : Type u_1} {F : Type u_2} {P : Program α F} {w : List α} {i : ℕ} {e : Expr α F} {b b' : Bool} (h : Eval P w i e b) (h' : Eval P w i e b') :
                        b = b'

                        The derivation system is deterministic, giving an expression at most one value.

                        source
                        def Subregular.BMRS.Program.TotalOn {α : Type u_1} {F : Type u_2} (P : Program α F) (w : List α) :
                        Prop

                        A program is total on w when every rule head is defined at every position.

                        Equations
                        Instances For

                          Substitution #

                          source
                          theorem Subregular.BMRS.Eval.subst {α : Type u_1} {F : Type u_2} {P : Program α F} {w : List α} {i v : ℕ} {u : Walk} {e : Expr α F} {b : Bool} (hu : Walk.eval w i u = some v) (h : Eval P w v e b) :
                          Eval P w i (e.subst u) b

                          Evaluating e[u/x] at i is evaluating e at the position u reads.

                          Locality #

                          Evaluation reads only the positions its walks reach. Successor-free programs compute left-subsequentially and predecessor-free programs right-subsequentially, and the one-sided locality below is what those inclusions rest on. Equal length is load-bearing: walks and the max test read w.length.

                          source
                          theorem Subregular.BMRS.Eval.congr_of_allWalks {α : Type u_1} {F : Type u_2} {P : Program α F} {w w' : List α} {i : ℕ} {e : Expr α F} {b : Bool} {p : Walk → Prop} {r : ℕ → ℕ → Prop} [IsTrans ℕ r] (hp : ∀ {t : Walk} {j v : ℕ}, p t → Walk.eval w j t = some v → r v j) (hP : ∀ (f : F), Expr.AllWalks p (P f)) (hlen : w.length = w'.length) (h : Eval P w i e b) :
                          Expr.AllWalks p e → Set.EqOn (fun (x : ℕ) => w[x]?) (fun (x : ℕ) => w'[x]?) {v : ℕ | r v i} → Eval P w' i e b

                          Locality. If every walk of P and of e satisfies p, and a p-walk read from j reaches only positions r-related to j for a transitive r, then equal-length words agreeing on the positions r-related to i evaluate e at i alike.

                          source
                          theorem Subregular.BMRS.Eval.congr_eqOn_Iic {α : Type u_1} {F : Type u_2} {P : Program α F} {w w' : List α} {i : ℕ} {e : Expr α F} {b : Bool} (hP : P.Backward) (hlen : w.length = w'.length) (h : Eval P w i e b) :
                          Expr.AllWalks Walk.Backward e → Set.EqOn (fun (x : ℕ) => w[x]?) (fun (x : ℕ) => w'[x]?) (Set.Iic i) → Eval P w' i e b

                          A successor-free program evaluated at i reads only positions ≤ i, so equal-length words agreeing up to i evaluate identically.

                          source
                          theorem Subregular.BMRS.Eval.congr_eqOn_Ici {α : Type u_1} {F : Type u_2} {P : Program α F} {w w' : List α} {i : ℕ} {e : Expr α F} {b : Bool} (hP : P.Forward) (hlen : w.length = w'.length) (h : Eval P w i e b) :
                          Expr.AllWalks Walk.Forward e → Set.EqOn (fun (x : ℕ) => w[x]?) (fun (x : ℕ) => w'[x]?) (Set.Ici i) → Eval P w' i e b

                          A predecessor-free program evaluated at i reads only positions ≥ i, so equal-length words agreeing from i on evaluate identically.

                          Evaluation in rounds #

                          A round reruns every rule body with its calls read from a table of the values found so far, starting from the empty table. Values only accumulate, a round reads the table only at positions of the word, and until the rounds settle each one values a new pair of a head and a position, so on a word of length n they settle by round card F * n.

                          source
                          def Subregular.BMRS.Expr.evalWith {α : Type u_1} {F : Type u_2} [DecidableEq α] (w : List α) (V : F → ℕ → Option Bool) (i : ℕ) :
                          Expr α F → Option Bool

                          e.evalWith w V i evaluates e at i in one round, reading each rule-head call from the table V instead of unfolding it.

                          Equations
                          Instances For
                            source
                            def Subregular.BMRS.Program.approx {α : Type u_1} {F : Type u_2} [DecidableEq α] (P : Program α F) (w : List α) :
                            ℕ → F → ℕ → Option Bool

                            P.approx w k is the table after k rounds of evaluation. The first round starts from the empty table, and each round reruns every rule body against the table before it.

                            Equations
                            Instances For
                              source
                              theorem Subregular.BMRS.Expr.evalWith_mono {α : Type u_1} {F : Type u_2} {w : List α} {i : ℕ} {e : Expr α F} {b : Bool} [DecidableEq α] {V V' : F → ℕ → Option Bool} (hV : ∀ (f : F) (j : ℕ) (b : Bool), V f j = some b → V' f j = some b) :
                              evalWith w V i e = some b → evalWith w V' i e = some b

                              A round against a larger table finds the same values.

                              source
                              theorem Subregular.BMRS.Expr.evalWith_congr {α : Type u_1} {F : Type u_2} {w : List α} {i : ℕ} [DecidableEq α] {V V' : F → ℕ → Option Bool} (hV : ∀ (f : F), ∀ j < w.length, V f j = V' f j) (e : Expr α F) :
                              evalWith w V i e = evalWith w V' i e

                              A round reads its table only at positions of the word.

                              source
                              theorem Subregular.BMRS.Program.approx_succ_of_eq_some {α : Type u_1} {F : Type u_2} {P : Program α F} {w : List α} [DecidableEq α] {k : ℕ} {f : F} {j : ℕ} {b : Bool} :
                              P.approx w k f j = some b → P.approx w (k + 1) f j = some b
                              source
                              theorem Subregular.BMRS.Program.approx_mono {α : Type u_1} {F : Type u_2} {P : Program α F} {w : List α} {b : Bool} [DecidableEq α] {k m : ℕ} (hkm : k ≤ m) {f : F} {j : ℕ} (h : P.approx w k f j = some b) :
                              P.approx w m f j = some b

                              Rounds only add values.

                              source
                              theorem Subregular.BMRS.Program.evalWith_approx_mono {α : Type u_1} {F : Type u_2} {P : Program α F} {w : List α} {i : ℕ} {e : Expr α F} {b : Bool} [DecidableEq α] {k m : ℕ} (hkm : k ≤ m) :
                              Expr.evalWith w (P.approx w k) i e = some b → Expr.evalWith w (P.approx w m) i e = some b
                              source
                              theorem Subregular.BMRS.Program.eval_of_evalWith {α : Type u_1} {F : Type u_2} {P : Program α F} {w : List α} {i : ℕ} {e : Expr α F} {b : Bool} [DecidableEq α] {V : F → ℕ → Option Bool} (hV : ∀ (f : F) (j : ℕ) (b : Bool), V f j = some b → Eval P w j (P f) b) :
                              Expr.evalWith w V i e = some b → Eval P w i e b

                              A round against a table of derived values derives every value it finds.

                              source
                              theorem Subregular.BMRS.Program.eval_of_approx {α : Type u_1} {F : Type u_2} {P : Program α F} {w : List α} [DecidableEq α] {k : ℕ} {f : F} {j : ℕ} {b : Bool} :
                              P.approx w k f j = some b → Eval P w j (P f) b

                              Every value a round finds is derived.

                              source
                              theorem Subregular.BMRS.Program.exists_evalWith_approx {α : Type u_1} {F : Type u_2} {P : Program α F} {w : List α} {i : ℕ} {e : Expr α F} {b : Bool} [DecidableEq α] (h : Eval P w i e b) :
                              ∃ (k : ℕ), Expr.evalWith w (P.approx w k) i e = some b

                              Every derived value is found by some round.

                              source
                              theorem Subregular.BMRS.Program.approx_eq_approx_card_mul_length {α : Type u_1} {F : Type u_2} {P : Program α F} {w : List α} [DecidableEq α] {k : ℕ} [Fintype F] (hk : Fintype.card F * w.length ≤ k) (f : F) (j : ℕ) :
                              j < w.length → P.approx w k f j = P.approx w (Fintype.card F * w.length) f j

                              On a word of length n the rounds settle by round card F * n, since each round before they settle gives a value to a new pair of a head and a position.

                              source
                              def Subregular.BMRS.Program.eval {α : Type u_1} {F : Type u_2} [DecidableEq α] [Fintype F] (P : Program α F) (w : List α) (i : ℕ) (e : Expr α F) :
                              Option Bool

                              The value of e at i under P, from the round by which the rounds settle; none where P does not halt.

                              Equations
                              Instances For
                                source
                                theorem Subregular.BMRS.Program.eval_eq_some_iff {α : Type u_1} {F : Type u_2} {P : Program α F} {w : List α} {i : ℕ} {e : Expr α F} {b : Bool} [DecidableEq α] [Fintype F] :
                                P.eval w i e = some b ↔ Eval P w i e b

                                The rounds settle on the derivation system.

                                source
                                @[instance_reducible]
                                instance Subregular.BMRS.Program.instDecidableEvalOfFintype {α : Type u_1} {F : Type u_2} {P : Program α F} {w : List α} {i : ℕ} {e : Expr α F} {b : Bool} [DecidableEq α] [Fintype F] :
                                Decidable (Eval P w i e b)
                                Equations
                                source
                                @[instance_reducible]
                                instance Subregular.BMRS.Program.instDecidableTotalOnOfFintype {α : Type u_1} {F : Type u_2} {P : Program α F} {w : List α} [DecidableEq α] [Fintype F] :
                                Decidable (P.TotalOn w)
                                Equations
                                • One or more equations did not get rendered due to their size.