Documentation

Linglib.Core.Computability.Subregular.Logic.ModalMu

The vectorial modal μ-calculus on words #

The modal μ-calculus ([Koz83]) interpreted over word models, in the vectorial presentation of [YC26] §4: a finite system of equations Xⱼ = θⱼ between quantifier-free modal formulas plus a designated variable, evaluated as the least fixed point of the induced monotone operator (Knaster–Tarski). By Bekić's theorem the vectorial form is equivalent to nested μ-binders; formalizing it directly avoids binder bookkeeping and matches the paper's own proofs.

Formulas here are the negation-free fragment μML꜀₊ — the ambient of [YC26] Thm. 8 — extended with negated label atoms (nlabel), which keeps negation off recursion variables (so monotonicity is structural) while covering processes like Warao nasal spreading N′ = μX.(N ∨ (¬T ∧ ♦X)).

◇ (dia) is the forward modality reading the successor position, ♦ (bdia) the backward modality reading the predecessor.

Main definitions #

Main results #

source
inductive Subregular.Logic.ModalMu.Formula (α : Type u_2) (n : ℕ) :
Type u_2

Quantifier-free modal formulas over labels α and n recursion variables: the negation-free fragment, with negation on class atoms only (nlabel) — so recursion variables occur only positively and monotonicity is structural. label/nlabel test the current position's symbol against a Finset class (featural predicates like V or N are single atoms; a symbol test is the singleton case). initial/final are the edge tests (the literature's min/max); dia (◇) reads the successor position, bdia (♦) the predecessor.

Instances For
    source
    @[implicit_reducible]
    instance Subregular.Logic.ModalMu.instDecidableEqFormula {α✝ : Type u_2} {n✝ : ℕ} [DecidableEq α✝] :
    DecidableEq (Formula α✝ n✝)
    Equations
    source
    def Subregular.Logic.ModalMu.instDecidableEqFormula.decEq {α✝ : Type u_2} {n✝ : ℕ} [DecidableEq α✝] (x✝ x✝¹ : Formula α✝ n✝) :
    Decidable (x✝ = x✝¹)
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      def Subregular.Logic.ModalMu.Formula.Realize {α : Type u_1} {n : ℕ} (w : WordModel α) (U : Fin n → Set ℕ) :
      ℕ → Formula α n → Prop

      Satisfaction at a pointed word (w, i) under a valuation U of the recursion variables.

      Equations
      Instances For
        source
        @[simp]
        theorem Subregular.Logic.ModalMu.Formula.realize_tru {α : Type u_1} {n : ℕ} {w : WordModel α} {U : Fin n → Set ℕ} {i : ℕ} :
        Realize w U i tru
        source
        @[simp]
        theorem Subregular.Logic.ModalMu.Formula.realize_fls {α : Type u_1} {n : ℕ} {w : WordModel α} {U : Fin n → Set ℕ} {i : ℕ} :
        ¬Realize w U i fls
        source
        @[simp]
        theorem Subregular.Logic.ModalMu.Formula.realize_initial {α : Type u_1} {n : ℕ} {w : WordModel α} {U : Fin n → Set ℕ} {i : ℕ} :
        Realize w U i initial ↔ i = 0
        source
        @[simp]
        theorem Subregular.Logic.ModalMu.Formula.realize_final {α : Type u_1} {n : ℕ} {w : WordModel α} {U : Fin n → Set ℕ} {i : ℕ} :
        Realize w U i final ↔ i + 1 = List.length w
        source
        @[simp]
        theorem Subregular.Logic.ModalMu.Formula.realize_label {α : Type u_1} {n : ℕ} {w : WordModel α} {U : Fin n → Set ℕ} {i : ℕ} {s : Finset α} :
        Realize w U i (label s) ↔ ∃ a ∈ s, w[i]? = some a
        source
        @[simp]
        theorem Subregular.Logic.ModalMu.Formula.realize_nlabel {α : Type u_1} {n : ℕ} {w : WordModel α} {U : Fin n → Set ℕ} {i : ℕ} {s : Finset α} :
        Realize w U i (nlabel s) ↔ ∀ a ∈ s, w[i]? ≠ some a
        source
        @[simp]
        theorem Subregular.Logic.ModalMu.Formula.realize_var {α : Type u_1} {n : ℕ} {w : WordModel α} {U : Fin n → Set ℕ} {i : ℕ} {X : Fin n} :
        Realize w U i (var X) ↔ i ∈ U X
        source
        @[simp]
        theorem Subregular.Logic.ModalMu.Formula.realize_and {α : Type u_1} {n : ℕ} {w : WordModel α} {U : Fin n → Set ℕ} {i : ℕ} {φ ψ : Formula α n} :
        Realize w U i (φ.and ψ) ↔ Realize w U i φ ∧ Realize w U i ψ
        source
        @[simp]
        theorem Subregular.Logic.ModalMu.Formula.realize_or {α : Type u_1} {n : ℕ} {w : WordModel α} {U : Fin n → Set ℕ} {i : ℕ} {φ ψ : Formula α n} :
        Realize w U i (φ.or ψ) ↔ Realize w U i φ ∨ Realize w U i ψ
        source
        @[simp]
        theorem Subregular.Logic.ModalMu.Formula.realize_dia {α : Type u_1} {n : ℕ} {w : WordModel α} {U : Fin n → Set ℕ} {i : ℕ} {φ : Formula α n} :
        Realize w U i φ.dia ↔ ∃ (j : ℕ), w.succ? i = some j ∧ Realize w U j φ
        source
        @[simp]
        theorem Subregular.Logic.ModalMu.Formula.realize_bdia {α : Type u_1} {n : ℕ} {w : WordModel α} {U : Fin n → Set ℕ} {i : ℕ} {φ : Formula α n} :
        Realize w U i φ.bdia ↔ ∃ (j : ℕ), w.pred? i = some j ∧ Realize w U j φ
        source
        @[implicit_reducible]
        instance Subregular.Logic.ModalMu.Formula.instDecidableRealize {α : Type u_1} {n : ℕ} [DecidableEq α] (w : WordModel α) (U : Fin n → Set ℕ) [(X : Fin n) → DecidablePred fun (x : ℕ) => x ∈ U X] (i : ℕ) (φ : Formula α n) :
        Decidable (Realize w U i φ)
        Equations
        source
        theorem Subregular.Logic.ModalMu.Formula.Realize.mono {α : Type u_1} {n : ℕ} {w : WordModel α} {U V : Fin n → Set ℕ} (hUV : U ≤ V) {φ : Formula α n} {i : ℕ} :
        Realize w U i φ → Realize w V i φ

        Satisfaction is monotone in the valuation: recursion variables occur only positively.

        source
        structure Subregular.Logic.ModalMu.System (α : Type u_2) (n : ℕ) :
        Type u_2

        A vectorial formula ([YC26] §4): a finite system of equations Xⱼ = θⱼ plus a designated variable.

        • eqs : Fin n → Formula α n

          The right-hand side of each equation.

        • out : Fin n

          The designated variable whose satisfaction is the system's.

        Instances For
          source
          def Subregular.Logic.ModalMu.System.op {α : Type u_1} {n : ℕ} (χ : System α n) (w : WordModel α) :
          (Fin n → Set ℕ) →o Fin n → Set ℕ

          The monotone operator a system induces on valuations (the paper's F_w^χ).

          Equations
          Instances For
            source
            @[simp]
            theorem Subregular.Logic.ModalMu.System.mem_op {α : Type u_1} {n : ℕ} (χ : System α n) (w : WordModel α) {U : Fin n → Set ℕ} {X : Fin n} {i : ℕ} :
            i ∈ (χ.op w) U X ↔ Formula.Realize w U i (χ.eqs X)
            source
            noncomputable def Subregular.Logic.ModalMu.System.sem {α : Type u_1} {n : ℕ} (χ : System α n) (w : WordModel α) :
            Fin n → Set ℕ

            The least-fixed-point valuation (Knaster–Tarski).

            Equations
            • χ.sem w = OrderHom.lfp (χ.op w)
            Instances For
              source
              theorem Subregular.Logic.ModalMu.System.op_sem {α : Type u_1} {n : ℕ} (χ : System α n) (w : WordModel α) :
              (χ.op w) (χ.sem w) = χ.sem w

              sem is a fixed point of the system operator.

              source
              theorem Subregular.Logic.ModalMu.System.sem_le {α : Type u_1} {n : ℕ} (χ : System α n) (w : WordModel α) {U : Fin n → Set ℕ} (hU : (χ.op w) U ≤ U) :
              χ.sem w ≤ U

              sem is below every prefixed point.

              source
              theorem Subregular.Logic.ModalMu.System.sem_eq_iterate {α : Type u_1} {n : ℕ} (χ : System α n) (w : WordModel α) {k : ℕ} (h : (χ.op w) ((⇑(χ.op w))^[k] ⊥) = (⇑(χ.op w))^[k] ⊥) :
              χ.sem w = (⇑(χ.op w))^[k] ⊥

              Iteration certificate: an iterate of ⊥ fixed by the operator is sem. The computable route to the least fixed point — no continuity needed.

              source
              def Subregular.Logic.ModalMu.System.Sat {α : Type u_1} {n : ℕ} (χ : System α n) (w : WordModel α) (i : ℕ) :
              Prop

              w, i ⊨ χ: the designated variable holds at i in the least fixed point.

              Equations
              Instances For