Documentation

Linglib.Core.Computability.Subregular.Logic.BMRS

Boolean Monadic Recursive Schemes #

BMRS ([BCJO20]; [BCJ23]; phonological modelling in [CJ21]): programs of mutually recursive Boolean-valued unary predicates over word models, built from if…then…else, the edge tests initial/final (the literature's min/max), input class tests, and recursive calls. Terms are the quantifier-free terms of Logic/QFLogic.lean at a single index variable.

Two symbol types dissolve the literature's sig(P) bookkeeping: input labels α get the lookup rule, rule heads F get the unfolding rule, and a Program is a total map F → Expr α F.

Semantics is the derivation system of [YC26] (Fig. 6–7), 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.Logic.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 single-variable quantifier-free terms of Logic/QFLogic.lean.

Instances For
    source
    @[implicit_reducible]
    instance Subregular.Logic.BMRS.instDecidableEqExpr {α✝ : Type u_3} {F✝ : Type u_4} [DecidableEq α✝] [DecidableEq F✝] :
    DecidableEq (Expr α✝ F✝)
    Equations
    source
    def Subregular.Logic.BMRS.instDecidableEqExpr.decEq {α✝ : Type u_3} {F✝ : Type u_4} [DecidableEq α✝] [DecidableEq F✝] (x✝ x✝¹ : Expr α✝ F✝) :
    Decidable (x✝ = x✝¹)
    Equations
    Instances For
      source
      @[reducible, inline]
      abbrev Subregular.Logic.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.Logic.BMRS.Expr.and {α : Type u_1} {F : Type u_2} (e₁ e₂ : Expr α F) :
        Expr α F

        Conjunction as if…then…else ([Yol25] (3.6)).

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

          Disjunction as if…then…else ([Yol25] (3.7)).

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

            Negation as if…then…else ([Yol25] (3.8)).

            Equations
            Instances For
              source
              def Subregular.Logic.BMRS.Expr.subst {α : Type u_1} {F : Type u_2} :
              Expr α F → Term Unit → 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.Logic.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.Logic.BMRS.Expr.Forward {α : Type u_1} {F : Type u_2} :
                  Expr α F → Prop

                  Forward expressions.

                  Equations
                  Instances For
                    source
                    @[implicit_reducible]
                    instance Subregular.Logic.BMRS.Expr.instDecidableBackward {α : Type u_1} {F : Type u_2} (e : Expr α F) :
                    Decidable e.Backward
                    Equations
                    source
                    @[implicit_reducible]
                    instance Subregular.Logic.BMRS.Expr.instDecidableForward {α : Type u_1} {F : Type u_2} (e : Expr α F) :
                    Decidable e.Forward
                    Equations
                    source
                    def Subregular.Logic.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.Logic.BMRS.Program.Forward {α : Type u_1} {F : Type u_2} (P : Program α F) :
                      Prop

                      BMRSˢ: every rule body is forward.

                      Equations
                      Instances For

                        Term denotation #

                        source
                        def Subregular.Logic.BMRS.tden {α : Type u_1} (w : WordModel α) (i : ℕ) (t : Term Unit) :
                        Option ℕ

                        Denotation of a BMRS term at index i (the judgment w, i ⊢ T → v).

                        Equations
                        Instances For
                          source
                          @[simp]
                          theorem Subregular.Logic.BMRS.tden_succ {α : Type u_1} {w : WordModel α} {i : ℕ} {t : Term Unit} :
                          tden w i t.succ = (tden w i t).bind w.succ?
                          source
                          @[simp]
                          theorem Subregular.Logic.BMRS.tden_pred {α : Type u_1} {w : WordModel α} {i : ℕ} {t : Term Unit} :
                          tden w i t.pred = (tden w i t).bind w.pred?
                          source
                          theorem Subregular.Logic.BMRS.tden_var_eq_some_iff {α : Type u_1} {w : WordModel α} {i v : ℕ} :
                          tden w i (Term.var ()) = some v ↔ v = i ∧ i < List.length w
                          source
                          theorem Subregular.Logic.BMRS.tden_lt {α : Type u_1} {w : WordModel α} {i : ℕ} {t : Term Unit} {v : ℕ} :
                          tden w i t = some v → v < List.length w

                          Term denotations are in-domain.

                          source
                          @[simp]
                          theorem Subregular.Logic.BMRS.tden_var {α : Type u_1} {w : WordModel α} {i : ℕ} (h : i < List.length w) :
                          tden w i (Term.var ()) = some i

                          The variable denotes its own in-domain position.

                          source
                          @[simp]
                          theorem Subregular.Logic.BMRS.tden_succ_var {α : Type u_1} {w : WordModel α} {i : ℕ} :
                          tden w i (Term.var ()).succ = w.succ? i

                          A one-step successor term denotes the successor position.

                          source
                          theorem Subregular.Logic.BMRS.tden_pred_var {α : Type u_1} {w : WordModel α} {i : ℕ} (h : i < List.length w) :
                          tden w i (Term.var ()).pred = w.pred? i

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

                          source
                          theorem Subregular.Logic.BMRS.tden_comp {α : Type u_1} {w : WordModel α} {i : ℕ} (t u : Term Unit) :
                          tden w i (t.comp u) = (tden w i u).bind fun (v : ℕ) => tden w v t

                          Composed terms denote sequenced denotations.

                          The derivation system #

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

                          The derivation system for BMRS expressions ([YC26] Fig. 7): 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.Logic.BMRS.Eval.initial {α : Type u_1} {F : Type u_2} {P : Program α F} {w : WordModel α} {i v : ℕ} {t : Term Unit} (h : tden 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.Logic.BMRS.Eval.final {α : Type u_1} {F : Type u_2} {P : Program α F} {w : WordModel α} {i v : ℕ} {t : Term Unit} (h : tden w i t = some v) :
                            Eval P w i (Expr.final t) (v == List.length w - 1)

                            Boolean-form introduction for the final test.

                            source
                            theorem Subregular.Logic.BMRS.Eval.label {α : Type u_1} {F : Type u_2} {P : Program α F} {w : WordModel α} {i v : ℕ} {t : Term Unit} [DecidableEq α] {s : Finset α} {a : α} (h : tden 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.Logic.BMRS.Eval.deterministic {α : Type u_1} {F : Type u_2} {P : Program α F} {w : WordModel α} {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.Logic.BMRS.Program.TotalOn {α : Type u_1} {F : Type u_2} (P : Program α F) (w : WordModel α) :
                            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.Logic.BMRS.evalFuel {α : Type u_1} {F : Type u_2} [DecidableEq α] (P : Program α F) (w : WordModel α) :
                              ℕ → ℕ → Expr α F → Option Bool

                              Fuel-bounded evaluator: the computable face of Eval.

                              Equations
                              Instances For
                                source
                                theorem Subregular.Logic.BMRS.evalFuel_mono {α : Type u_1} {F : Type u_2} {P : Program α F} {w : WordModel α} {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.Logic.BMRS.evalFuel_sound {α : Type u_1} {F : Type u_2} {P : Program α F} {w : WordModel α} {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.Logic.BMRS.evalFuel_complete {α : Type u_1} {F : Type u_2} {P : Program α F} {w : WordModel α} {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.Logic.BMRS.eval_iff_evalFuel {α : Type u_1} {F : Type u_2} {P : Program α F} {w : WordModel α} {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.Logic.BMRS.Eval.subst {α : Type u_1} {F : Type u_2} {P : Program α F} {w : WordModel α} {i v : ℕ} {u : Term Unit} {e : Expr α F} {b : Bool} (hu : tden 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 denotes.

                                One-sided fragments and locality #

                                BMRSᵖ-programs (successor-free) compute left-subsequentially, BMRSˢ-programs (predecessor-free) right-subsequentially ([BCJO20]). The locality lemmas below are what those inclusions rest on and are the engine of [Yol25]'s negative results: the flags of a one-sided program cannot see across the target. Equal length is load-bearing — min/max atoms read w.length.

                                source
                                theorem Subregular.Logic.BMRS.tden_le_of_backward {α : Type u_1} {w : WordModel α} {i : ℕ} {t : Term Unit} :
                                t.Backward → ∀ {v : ℕ}, tden w i t = some v → v ≤ i

                                Backward terms only move left.

                                source
                                theorem Subregular.Logic.BMRS.le_tden_of_forward {α : Type u_1} {w : WordModel α} {i : ℕ} {t : Term Unit} :
                                t.Forward → ∀ {v : ℕ}, tden w i t = some v → i ≤ v

                                Forward terms only move right.

                                source
                                theorem Subregular.Logic.BMRS.tden_congr {α : Type u_1} {w w' : WordModel α} {i : ℕ} (hlen : List.length w = List.length w') (t : Term Unit) :
                                tden w i t = tden w' i t

                                Term denotations read only the length, so they transport across equal-length words.

                                source
                                theorem Subregular.Logic.BMRS.Eval.congr_agreeUpto {α : Type u_1} {F : Type u_2} {P : Program α F} {w w' : WordModel α} {i : ℕ} {e : Expr α F} {b : Bool} (hP : P.Backward) (hlen : List.length w = List.length w') (h : Eval P w i e b) :
                                e.Backward → AgreeUpto w w' 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.Logic.BMRS.Eval.congr_agreeFrom {α : Type u_1} {F : Type u_2} {P : Program α F} {w w' : WordModel α} {i : ℕ} {e : Expr α F} {b : Bool} (hP : P.Forward) (hlen : List.length w = List.length w') (h : Eval P w i e b) :
                                e.Forward → AgreeFrom w w' 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.

                                Simultaneous application, at the value level #

                                [Yol25] Def. 4.1 (⊙) and Def. 6.5 (⊘) act per input position on the input value and the two programs' output values; the program-level operators lift these pointwise. Stating the algebra ([Yol25] Prop. 4.4) on values keeps it a finite Bool computation and spares the combined-head-space transport.

                                source
                                def Subregular.Logic.BMRS.combine (pin a b : Bool) :
                                Bool

                                Simultaneous application ⊙ on values ([Yol25] Def. 4.1): a change survives iff either program makes it.

                                Equations
                                Instances For
                                  source
                                  def Subregular.Logic.BMRS.combineC (pin a b : Bool) :
                                  Bool

                                  Conjunctive simultaneous application ⊘ on values ([Yol25] Def. 6.5): a change survives iff both programs make it.

                                  Equations
                                  Instances For
                                    source
                                    @[simp]
                                    theorem Subregular.Logic.BMRS.combine_true (a b : Bool) :
                                    combine true a b = (a && b)

                                    On a true input, ⊙ is conjunction.

                                    source
                                    @[simp]
                                    theorem Subregular.Logic.BMRS.combine_false (a b : Bool) :
                                    combine false a b = (a || b)

                                    On a false input, ⊙ is disjunction — the collapse behind [Yol25] (5.15): with no underlying stress the ⊙ of the two stress programs is their disjunction.

                                    source
                                    @[simp]
                                    theorem Subregular.Logic.BMRS.combineC_true (a b : Bool) :
                                    combineC true a b = (a || b)

                                    On a true input, ⊘ is disjunction.

                                    source
                                    @[simp]
                                    theorem Subregular.Logic.BMRS.combineC_false (a b : Bool) :
                                    combineC false a b = (a && b)

                                    On a false input, ⊘ is conjunction — the conjunctive licensing of [Yol25] §6.3.

                                    source
                                    theorem Subregular.Logic.BMRS.combine_ne_iff (pin a b : Bool) :
                                    combine pin a b ≠ pin ↔ a ≠ pin ∨ b ≠ pin

                                    A ⊙-value differs from the input iff one of the components does ([Yol25] Prop. 4.2): the changes of the simultaneous application are the union of the changes.

                                    source
                                    theorem Subregular.Logic.BMRS.combine_comm (pin a b : Bool) :
                                    combine pin a b = combine pin b a
                                    source
                                    theorem Subregular.Logic.BMRS.combine_assoc (pin a b c : Bool) :
                                    combine pin (combine pin a b) c = combine pin a (combine pin b c)
                                    source
                                    theorem Subregular.Logic.BMRS.combine_id (pin a : Bool) :
                                    combine pin a pin = a

                                    The input itself is a ⊙-identity ([Yol25] Prop. 4.4(iii)).

                                    source
                                    theorem Subregular.Logic.BMRS.combineC_eq_not_combine (pin a b : Bool) :
                                    combineC pin a b = !combine pin (!a) !b

                                    ⊘ is the De Morgan dual of ⊙: negate the two output values, not the input.

                                    source
                                    theorem Subregular.Logic.BMRS.combineC_comm (pin a b : Bool) :
                                    combineC pin a b = combineC pin b a
                                    source
                                    theorem Subregular.Logic.BMRS.combineC_assoc (pin a b c : Bool) :
                                    combineC pin (combineC pin a b) c = combineC pin a (combineC pin b c)