Documentation

Linglib.Phonology.Subregular.BMRS

Boolean Monadic Recursive Schemes #

A Boolean monadic recursive scheme ([BCJO20]) is a program of mutually recursive Boolean-valued unary predicates over words, built from if…then…else, the edge tests initial/final (min/max), input class tests, and recursive calls. Its one-sided fragments characterize the left- and right-subsequential functions; [BCJ23] extends the characterization and [CJ21] applies it to phonological modelling. Terms are the position walks of Subregular.Term.

Two symbol types dissolve the usual signature bookkeeping: input labels α get the lookup rule, rule heads F get the unfolding rule, and a Program is a total map F → Expr α F.

Evaluation is an inductive judgment Eval, faithful to partiality: a non-halting program (f := g, g := f) derives nothing. evalFuel is its computable face, related by eval_iff_evalFuel.

Main definitions #

Main results #

Syntax #

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

BMRS expressions: edge tests initial/final (the literature's min(T)/max(T)), input class tests label (the lookup rule; a Finset of symbols, so featural predicates like V or N over a segment alphabet are single atoms — a symbol test is the singleton case), rule-head calls call (the unfolding rule), and if…then…else. Terms are the position walks of Subregular.Term.

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: one defining expression per 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 → Term → Expr α F

              Substitute a term for the variable throughout an expression: e.subst u is e[u/x], the operation the μ-calculus translation writes tr(φ)[s(x)].

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

                Backward expressions: every term is backward.

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

                  Forward expressions.

                  Equations
                  Instances For
                    source
                    @[instance_reducible]
                    instance Subregular.BMRS.Expr.instDecidableBackward {α : Type u_1} {F : Type u_2} (e : Expr α F) :
                    Decidable e.Backward
                    Equations
                    source
                    @[instance_reducible]
                    instance Subregular.BMRS.Expr.instDecidableForward {α : Type u_1} {F : Type u_2} (e : Expr α F) :
                    Decidable e.Forward
                    Equations
                    source
                    def Subregular.BMRS.Program.Backward {α : Type u_1} {F : Type u_2} (P : Program α F) :
                    Prop

                    BMRSᵖ: every rule body is backward (hereditarily, through calls).

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

                      BMRSˢ: every rule body is forward.

                      Equations
                      Instances For

                        The derivation system #

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

                        The derivation system for BMRS expressions: Eval P w i e b is w, i ⊢_P e → b. Partial by design: a non-halting program derives nothing.

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

                          Boolean-form introduction for the edge test: the value is the comparison.

                          source
                          theorem Subregular.BMRS.Eval.final {α : Type u_1} {F : Type u_2} {P : Program α F} {w : List α} {i v : ℕ} {t : Term} (h : Term.eval w i t = some v) :
                          Eval P w i (Expr.final t) (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 : Term} [DecidableEq α] {s : Finset α} {a : α} (h : Term.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.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: an expression has 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

                            The fuel evaluator #

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

                            Fuel-bounded evaluator: the computable face of Eval.

                            Equations
                            Instances For
                              source
                              theorem Subregular.BMRS.evalFuel_mono {α : Type u_1} {F : Type u_2} {P : Program α F} {w : List α} {i n m : ℕ} {e : Expr α F} {b : Bool} [DecidableEq α] (hnm : n ≤ m) (h : evalFuel P w n i e = some b) :
                              evalFuel P w m i e = some b

                              More fuel never changes a defined answer.

                              source
                              theorem Subregular.BMRS.evalFuel_sound {α : Type u_1} {F : Type u_2} {P : Program α F} {w : List α} {i n : ℕ} {e : Expr α F} {b : Bool} [DecidableEq α] (h : evalFuel P w n i e = some b) :
                              Eval P w i e b

                              Soundness of the fuel evaluator against the derivation system.

                              source
                              theorem Subregular.BMRS.evalFuel_complete {α : 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) :
                              ∃ (n : ℕ), evalFuel P w n i e = some b

                              Completeness: every derivation is reached at some fuel.

                              source
                              theorem Subregular.BMRS.eval_iff_evalFuel {α : Type u_1} {F : Type u_2} {P : Program α F} {w : List α} {i : ℕ} {e : Expr α F} {b : Bool} [DecidableEq α] :
                              Eval P w i e b ↔ ∃ (n : ℕ), evalFuel P w n i e = some b

                              Adequacy: the derivation system and the fuel evaluator define the same values.

                              Substitution #

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

                              Transport a derivation through substitution: evaluating e[u/x] at i is evaluating e at the position u reads.

                              One-sided fragments and locality #

                              Successor-free programs compute left-subsequentially, predecessor-free programs right-subsequentially. The locality lemmas below are what those inclusions rest on: the flags of a one-sided program cannot see past their index. Equal length is load-bearing — min/max atoms read w.length.

                              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) :
                              e.Backward → Set.EqOn (fun (x : ℕ) => w[x]?) (fun (x : ℕ) => w'[x]?) (Set.Iic i) → Eval P w' i e b

                              One-sided locality (left): 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) :
                              e.Forward → Set.EqOn (fun (x : ℕ) => w[x]?) (fun (x : ℕ) => w'[x]?) (Set.Ici i) → Eval P w' i e b

                              One-sided locality (right): a predecessor-free program evaluated at i reads only positions ≥ i, so equal-length words agreeing from i on evaluate identically.