Linear-time μ-calculus

InductiveFormulas of the linear-time μ-calculus#✓fully proved

Formulas of the linear-time μ-calculus over atoms Atom, with de Bruijn variables for the fixed-point binders.

inductive LinearMuFormula (Atom : Type u) : Type u where
  | atom : Atom → LinearMuFormula Atom
  | natom : Atom → LinearMuFormula Atom
  | var : ℕ → LinearMuFormula Atom
  | bot : LinearMuFormula Atom
  | top : LinearMuFormula Atom
  | and : LinearMuFormula Atom → LinearMuFormula Atom → LinearMuFormula Atom
  | or : LinearMuFormula Atom → LinearMuFormula Atom → LinearMuFormula Atom
  | next : LinearMuFormula Atom → LinearMuFormula Atom
  | mu : LinearMuFormula Atom → LinearMuFormula Atom
  | nu : LinearMuFormula Atom → LinearMuFormula Atom

Used by 43

Used byClosed linear μ-calculus formula · Closedness of a μ-calculus formula at a binder depth · Depth of a linear μ-calculus formula · Eventually operator in the linear μ-calculus · The linear μ-calculus F is eventuality · Always operator in the linear μ-calculus · The linear μ-calculus G is universality over the future · Formula depth is bounded by its code · Cantor-pairing code of linear μ-calculus formulas · Injectivity of the linear μ-calculus code · Decoding linear μ-calculus codes · Fuelled decoding of linear μ-calculus codes · Fuelled decoding inverts encoding · Decoding inverts the linear μ-calculus encoding · Decoding a linear μ-calculus token list to a formula · Token-list decoding inverts linear μ-calculus token encoding · Fuelled parser for linear μ-calculus token lists · Fuelled parsing inverts linear μ-calculus token encoding · Token-list encoding of linear μ-calculus formulas · Park induction · Least fixed point is a fixed point: lower inclusion · The μ operator as a monotone operator on predicates · Least fixed point is a pre-fixed point · Dual negation of linear μ-calculus formulas · Negation of linear μ-calculus formulas is an involution · Coinduction · Greatest fixed point is a fixed point: upper inclusion · Greatest fixed point is a post-fixed point · Satisfaction of linear μ-calculus formulas · Closed formulas do not depend on the environment · Satisfaction is monotone in the environment · Satisfaction is monotone in the bound variable · μ-formulas denote least fixed points · The μ unfolding · Duality · ν-formulas denote greatest fixed points · The ν unfolding · Linear μ-calculus model checking on a finite Kripke structure · Linear μ-calculus model checking as a decision problem · Satisfiability of a closed linear μ-calculus formula · Linear μ-calculus satisfiability as a decision problem · Validity of a closed linear μ-calculus formula · Linear μ-calculus validity as a decision problem

DefinitionDual negation of linear μ-calculus formulas#✓fully proved

Meta-level negation, swapping each connective with its dual.

def neg : LinearMuFormula Atom → LinearMuFormula Atom
  | .atom a => .natom a
  | .natom a => .atom a
  | .var n => .var n
  | .bot => .top
  | .top => .bot
  | .and φ ψ => .or (neg φ) (neg ψ)
  | .or φ ψ => .and (neg φ) (neg ψ)
  | .next φ => .next (neg φ)
  | .mu φ => .nu (neg φ)
  | .nu φ => .mu (neg φ)

Uses 1 · Used by 2

Statement usesFormulas of the linear-time μ-calculus

Used byNegation of linear μ-calculus formulas is an involution · Duality

TheoremNegation of linear μ-calculus formulas is an involution#✓fully proved

Negation is an involution.

theorem neg_neg : ∀ (φ : LinearMuFormula Atom), (neg (neg φ)) = φ

Uses 2

Statement usesFormulas of the linear-time μ-calculus · Dual negation of linear μ-calculus formulas

DefinitionClosedness of a μ-calculus formula at a binder depth#✓fully proved

φ is closed at depth d when every free variable is below d (de Bruijn): var n needs n < d, and binders increase the depth.

def ClosedAt (d : ℕ) : LinearMuFormula Atom → Prop
  | .atom _ => True
  | .natom _ => True
  | .var n => n < d
  | .bot => True
  | .top => True
  | .and φ ψ => ClosedAt d φ ∧ ClosedAt d ψ
  | .or φ ψ => ClosedAt d φ ∧ ClosedAt d ψ
  | .next φ => ClosedAt d φ
  | .mu φ => ClosedAt (d + 1) φ
  | .nu φ => ClosedAt (d + 1) φ

Uses 1 · Used by 2

Statement usesFormulas of the linear-time μ-calculus

Used byClosed linear μ-calculus formula · Closed formulas do not depend on the environment

DefinitionClosed linear μ-calculus formula#✓fully proved

A formula with no free variables.

def Closed (φ : LinearMuFormula Atom) : Prop := ClosedAt 0 φ

Uses 2 · Used by 3

Statement usesFormulas of the linear-time μ-calculus · Closedness of a μ-calculus formula at a binder depth

Used byLinear μ-calculus model checking as a decision problem · Linear μ-calculus satisfiability as a decision problem · Linear μ-calculus validity as a decision problem

DefinitionDepth of a linear μ-calculus formula#✓fully proved

The depth of a formula: the length of its longest root-to-leaf path, counting each connective once.

def depth : LinearMuFormula Atom → ℕ
  | .atom _ => 0
  | .natom _ => 0
  | .var _ => 0
  | .bot => 0
  | .top => 0
  | .and φ ψ => 1 + max (depth φ) (depth ψ)
  | .or φ ψ => 1 + max (depth φ) (depth ψ)
  | .next φ => 1 + depth φ
  | .mu φ => 1 + depth φ
  | .nu φ => 1 + depth φ

Uses 1 · Used by 2

Statement usesFormulas of the linear-time μ-calculus

Used byFormula depth is bounded by its code · Fuelled decoding inverts encoding

DefinitionExtending an environment under a binder#✓fully proved

Extend an environment under a binder (de Bruijn).

def extendEnv (env : ℕ → ℕ → Prop) (S : ℕ → Prop) :
    ℕ → ℕ → Prop
  | 0 => S
  | n + 1 => env n

Used by 18

Used byComplementing an environment commutes with extension · The linear μ-calculus F is eventuality · The linear μ-calculus G is universality over the future · Park induction · Least fixed point is a fixed point: lower inclusion · The μ operator as a monotone operator on predicates · Least fixed point is a pre-fixed point · Coinduction · Greatest fixed point is a fixed point: upper inclusion · Greatest fixed point is a post-fixed point · Satisfaction of linear μ-calculus formulas · Closed formulas do not depend on the environment · Satisfaction is monotone in the environment · Satisfaction is monotone in the bound variable · The μ unfolding · Duality · ν-formulas denote greatest fixed points · The ν unfolding

41 fully proved

Satisfaction

DefinitionSatisfaction of linear μ-calculus formulas#✓fully proved

Satisfaction of a linear μ-calculus formula at a position of the word val. μ X. φ is the least pre-fixed point of S ↦ ⟦φ⟧[X ↦ S], stated directly as an infimum over pre-fixed points; ν X. φ is the greatest post-fixed point, stated as a supremum over post-fixed points.

def sat (env : ℕ → ℕ → Prop) : LinearMuFormula Atom → (ℕ → Prop)
  | .atom a => fun n => val n a
  | .natom a => fun n => ¬ val n a
  | .var n => env n
  | .bot => fun _ => False
  | .top => fun _ => True
  | .and φ ψ => fun n => sat env φ n ∧ sat env ψ n
  | .or φ ψ => fun n => sat env φ n ∨ sat env ψ n
  | .next φ => fun n => sat env φ (n + 1)
  | .mu φ => fun n => ∀ S : ℕ → Prop,
      (∀ m, sat (extendEnv env S) φ m → S m) → S n
  | .nu φ => fun n => ∃ S : ℕ → Prop,
      (∀ m, S m → sat (extendEnv env S) φ m) ∧ S n

Uses 2 · Used by 20

Statement usesFormulas of the linear-time μ-calculus · Extending an environment under a binder

Used byThe linear μ-calculus F is eventuality · The linear μ-calculus G is universality over the future · Park induction · Least fixed point is a fixed point: lower inclusion · The μ operator as a monotone operator on predicates · Least fixed point is a pre-fixed point · Coinduction · Greatest fixed point is a fixed point: upper inclusion · Greatest fixed point is a post-fixed point · Closed formulas do not depend on the environment · Satisfaction is monotone in the environment · Satisfaction is monotone in the bound variable · μ-formulas denote least fixed points · The μ unfolding · Duality · ν-formulas denote greatest fixed points · The ν unfolding · Linear μ-calculus model checking on a finite Kripke structure · Satisfiability of a closed linear μ-calculus formula · Validity of a closed linear μ-calculus formula

TheoremSatisfaction is monotone in the environment#✓fully proved

Satisfaction is monotone in the environment.

theorem sat_mono_env : ∀ (φ : LinearMuFormula Atom) {env env' : ℕ → ℕ → Prop},
    (∀ n, env n ≤ env' n) → sat val env φ ≤ sat val env' φ

Uses 3 · Used by 1

Statement usesFormulas of the linear-time μ-calculus · Satisfaction of linear μ-calculus formulas

Proof usesExtending an environment under a binder

Used bySatisfaction is monotone in the bound variable

TheoremSatisfaction is monotone in the bound variable#✓fully proved

Monotonicity in the bound variable's denotation.

theorem sat_mono_extend {env : ℕ → ℕ → Prop} {S₁ S₂ : ℕ → Prop} (h : S₁ ≤ S₂)
    (φ : LinearMuFormula Atom) :
    sat val (extendEnv env S₁) φ ≤ sat val (extendEnv env S₂) φ

Uses 4 · Used by 5

Statement usesFormulas of the linear-time μ-calculus · Extending an environment under a binder · Satisfaction of linear μ-calculus formulas

Proof usesSatisfaction is monotone in the environment

Used byLeast fixed point is a fixed point: lower inclusion · The μ operator as a monotone operator on predicates · Least fixed point is a pre-fixed point · Greatest fixed point is a fixed point: upper inclusion · Greatest fixed point is a post-fixed point

TheoremLeast fixed point is a pre-fixed point#✓fully proved

The least fixed point is a pre-fixed point.

theorem mu_pre_fixed (env : ℕ → ℕ → Prop) (φ : LinearMuFormula Atom) :
    sat val (extendEnv env (sat val env (.mu φ))) φ ≤ sat val env (.mu φ)

Uses 4 · Used by 3

Statement usesFormulas of the linear-time μ-calculus · Extending an environment under a binder · Satisfaction of linear μ-calculus formulas

Proof usesSatisfaction is monotone in the bound variable

Used byLeast fixed point is a fixed point: lower inclusion · μ-formulas denote least fixed points · The μ unfolding

TheoremLeast fixed point is a fixed point: lower inclusion#✓fully proved

The least fixed point is a fixed point (the lower half).

theorem mu_le_fixed (env : ℕ → ℕ → Prop) (φ : LinearMuFormula Atom) :
    sat val env (.mu φ) ≤ sat val (extendEnv env (sat val env (.mu φ))) φ

Uses 5 · Used by 1

Statement usesFormulas of the linear-time μ-calculus · Extending an environment under a binder · Satisfaction of linear μ-calculus formulas

Proof usesLeast fixed point is a pre-fixed point · Satisfaction is monotone in the bound variable

Used byThe μ unfolding

TheoremThe μ unfolding#✓fully proved

μ X. φ ≡ φ[μ X. φ / X].

theorem sat_mu_unfold (env : ℕ → ℕ → Prop) (φ : LinearMuFormula Atom) :
    sat val env (.mu φ) = sat val (extendEnv env (sat val env (.mu φ))) φ

Uses 5 · Used by 2

Statement usesFormulas of the linear-time μ-calculus · Extending an environment under a binder · Satisfaction of linear μ-calculus formulas

Proof usesLeast fixed point is a fixed point: lower inclusion · Least fixed point is a pre-fixed point

Used byThe linear μ-calculus F is eventuality · Duality

TheoremGreatest fixed point is a post-fixed point#✓fully proved

The greatest fixed point is a post-fixed point (the upper half).

theorem nu_post_fixed (env : ℕ → ℕ → Prop) (φ : LinearMuFormula Atom) :
    sat val env (.nu φ) ≤ sat val (extendEnv env (sat val env (.nu φ))) φ

Uses 4 · Used by 2

Statement usesFormulas of the linear-time μ-calculus · Extending an environment under a binder · Satisfaction of linear μ-calculus formulas

Proof usesSatisfaction is monotone in the bound variable

Used byGreatest fixed point is a fixed point: upper inclusion · The ν unfolding

TheoremGreatest fixed point is a fixed point: upper inclusion#✓fully proved

The greatest fixed point is a fixed point (the upper half).

theorem nu_le_post_fixed (env : ℕ → ℕ → Prop) (φ : LinearMuFormula Atom) :
    sat val (extendEnv env (sat val env (.nu φ))) φ ≤ sat val env (.nu φ)

Uses 5 · Used by 1

Statement usesFormulas of the linear-time μ-calculus · Extending an environment under a binder · Satisfaction of linear μ-calculus formulas

Proof usesGreatest fixed point is a post-fixed point · Satisfaction is monotone in the bound variable

Used byThe ν unfolding

TheoremThe ν unfolding#✓fully proved

ν X. φ ≡ φ[ν X. φ / X].

theorem sat_nu_unfold (env : ℕ → ℕ → Prop) (φ : LinearMuFormula Atom) :
    sat val env (.nu φ) = sat val (extendEnv env (sat val env (.nu φ))) φ

Uses 5 · Used by 2

Statement usesFormulas of the linear-time μ-calculus · Extending an environment under a binder · Satisfaction of linear μ-calculus formulas

Proof usesGreatest fixed point is a fixed point: upper inclusion · Greatest fixed point is a post-fixed point

Used byThe linear μ-calculus G is universality over the future · Duality

TheoremPark induction#✓fully proved

To show μ X. φ ≤ P, it suffices that P is a pre-fixed point.

theorem mu_induction {env : ℕ → ℕ → Prop} {φ : LinearMuFormula Atom}
    {P : ℕ → Prop}
    (hP : sat val (extendEnv env P) φ ≤ P) : sat val env (.mu φ) ≤ P

Uses 3 · Used by 2

Statement usesFormulas of the linear-time μ-calculus · Extending an environment under a binder · Satisfaction of linear μ-calculus formulas

Used byThe linear μ-calculus F is eventuality · Duality

TheoremCoinduction#✓fully proved

Every post-fixed point is below ν X. φ.

theorem nu_coinduction {env : ℕ → ℕ → Prop} {φ : LinearMuFormula Atom}
    {P : ℕ → Prop}
    (hP : P ≤ sat val (extendEnv env P) φ) : P ≤ sat val env (.nu φ)

Uses 3 · Used by 2

Statement usesFormulas of the linear-time μ-calculus · Extending an environment under a binder · Satisfaction of linear μ-calculus formulas

Used byThe linear μ-calculus G is universality over the future · Duality

DefinitionThe μ operator as a monotone operator on predicates#✓fully proved

The μ operator as a monotone operator on predicates.

def muOp (env : ℕ → ℕ → Prop) (φ : LinearMuFormula Atom) :
    (ℕ → Prop) →o (ℕ → Prop) :=
  ⟨fun S => sat val (extendEnv env S) φ, fun _ _ hle => sat_mono_extend val hle φ⟩

Uses 4 · Used by 3

Statement usesFormulas of the linear-time μ-calculus · Extending an environment under a binder · Satisfaction of linear μ-calculus formulas · Satisfaction is monotone in the bound variable

Used byClosed formulas do not depend on the environment · μ-formulas denote least fixed points · ν-formulas denote greatest fixed points

Theoremμ-formulas denote least fixed points#✓fully proved

The μ fixed point is Mathlib's least fixed point of the operator.

theorem sat_mu_eq_lfp (env : ℕ → ℕ → Prop) (φ : LinearMuFormula Atom) :
    sat val env (.mu φ) = (muOp val env φ).lfp

Uses 4 · Used by 1

Statement usesFormulas of the linear-time μ-calculus · The μ operator as a monotone operator on predicates · Satisfaction of linear μ-calculus formulas

Proof usesLeast fixed point is a pre-fixed point

Used byClosed formulas do not depend on the environment

Theoremν-formulas denote greatest fixed points#✓fully proved

The ν fixed point is Mathlib's greatest fixed point of the operator.

theorem sat_nu_eq_gfp (env : ℕ → ℕ → Prop) (φ : LinearMuFormula Atom) :
    sat val env (.nu φ) = (muOp val env φ).gfp

Uses 4 · Used by 1

Statement usesFormulas of the linear-time μ-calculus · The μ operator as a monotone operator on predicates · Satisfaction of linear μ-calculus formulas

Proof usesExtending an environment under a binder

Used byClosed formulas do not depend on the environment

TheoremClosed formulas do not depend on the environment#✓fully proved

A closed formula does not depend on the environment: environments agreeing below the depth give the same denotation.

theorem sat_closed_env : ∀ (φ : LinearMuFormula Atom) (d : ℕ)
    {env env' : ℕ → ℕ → Prop},
    LinearMuFormula.ClosedAt d φ →
    (∀ n, n < d → env n = env' n) →
    sat val env φ = sat val env' φ

Uses 7

Statement usesFormulas of the linear-time μ-calculus · Closedness of a μ-calculus formula at a binder depth · Satisfaction of linear μ-calculus formulas

Proof usesExtending an environment under a binder · The μ operator as a monotone operator on predicates · μ-formulas denote least fixed points · ν-formulas denote greatest fixed points

Duality

TheoremComplementing an environment commutes with extension#✓fully proved

Complementing an environment commutes with extending it.

theorem extendEnv_compl (env : ℕ → ℕ → Prop) (S : ℕ → Prop) :
    (fun n => fun m => ¬ extendEnv env S n m) =
      extendEnv (fun n => fun m => ¬ env n m) (fun m => ¬ S m)

Uses 1 · Used by 1

Statement usesExtending an environment under a binder

Used byDuality

TheoremDouble complement of a predicate#✓fully proved

Complementing a predicate twice returns it.

theorem compl_compl (S : ℕ → Prop) :
    (fun m => ¬ ¬ S m) = S

Used by 1

Used byDuality

TheoremDuality#✓fully proved

⟦¬φ⟧ = (⟦φ⟧)ᶜ when the environment is complemented.

theorem sat_neg : ∀ (φ : LinearMuFormula Atom) (env : ℕ → ℕ → Prop) (n : ℕ),
    sat val (fun k => fun m => ¬ env k m) (LinearMuFormula.neg φ) n ↔
      ¬ sat val env φ n

Uses 10

Statement usesFormulas of the linear-time μ-calculus · Dual negation of linear μ-calculus formulas · Satisfaction of linear μ-calculus formulas

Proof usesDouble complement of a predicate · Extending an environment under a binder · Complementing an environment commutes with extension · Park induction · Coinduction · The μ unfolding · The ν unfolding

Eventually Always

DefinitionEventually operator in the linear μ-calculus#✓fully proved

F p: p holds at some future position.

def F (p : Atom) : LinearMuFormula Atom := .mu (.or (.atom p) (.next (.var 0)))

Uses 1 · Used by 1

Statement usesFormulas of the linear-time μ-calculus

Used byThe linear μ-calculus F is eventuality

DefinitionAlways operator in the linear μ-calculus#✓fully proved

G p: p holds at every future position.

def G (p : Atom) : LinearMuFormula Atom := .nu (.and (.atom p) (.next (.var 0)))

Uses 1 · Used by 1

Statement usesFormulas of the linear-time μ-calculus

Used byThe linear μ-calculus G is universality over the future

TheoremThe linear μ-calculus F is eventuality#✓fully proved

The linear μ-calculus F is eventuality.

theorem F_iff (env : ℕ → ℕ → Prop) (p : Atom) (n : ℕ) :
    sat val env (F p) n ↔ ∃ m, n ≤ m ∧ val m p

Uses 6

Statement usesEventually operator in the linear μ-calculus · Satisfaction of linear μ-calculus formulas

Proof usesFormulas of the linear-time μ-calculus · Extending an environment under a binder · Park induction · The μ unfolding

TheoremThe linear μ-calculus G is universality over the future#✓fully proved

The linear μ-calculus G is universality over the future.

theorem G_iff (env : ℕ → ℕ → Prop) (p : Atom) (n : ℕ) :
    sat val env (G p) n ↔ ∀ m, n ≤ m → val m p

Uses 6

Statement usesAlways operator in the linear μ-calculus · Satisfaction of linear μ-calculus formulas

Proof usesFormulas of the linear-time μ-calculus · Extending an environment under a binder · Coinduction · The ν unfolding

Encoding

DefinitionCantor-pairing code of linear μ-calculus formulas#✓fully proved

An injective encoding of linear μ-calculus formulas over ℕ atoms as natural numbers, via the Cantor pairing function Nat.pair. This is a Nat code only, not a complexity input encoding: repeated pairing squares the code at every unary connective, so the binary length of the code of next^d (atom 0) doubles at each next and is exponential in d. Complexity statements use linearMuTokens / linearMuDecodeList instead.

def linearMuCode : LinearMuFormula ℕ → ℕ
  | .atom a => Nat.pair 0 a
  | .natom a => Nat.pair 1 a
  | .var n => Nat.pair 2 n
  | .bot => Nat.pair 3 0
  | .top => Nat.pair 4 0
  | .and φ ψ => Nat.pair 5 (Nat.pair (linearMuCode φ) (linearMuCode ψ))
  | .or φ ψ => Nat.pair 6 (Nat.pair (linearMuCode φ) (linearMuCode ψ))
  | .next φ => Nat.pair 7 (linearMuCode φ)
  | .mu φ => Nat.pair 8 (linearMuCode φ)
  | .nu φ => Nat.pair 9 (linearMuCode φ)

Uses 1 · Used by 4

Statement usesFormulas of the linear-time μ-calculus

Used byFormula depth is bounded by its code · Injectivity of the linear μ-calculus code · Fuelled decoding inverts encoding · Decoding inverts the linear μ-calculus encoding

TheoremInjectivity of the linear μ-calculus code#✓fully proved

The encoding is injective.

theorem linearMuCode_injective : Function.Injective linearMuCode

Uses 2

Statement usesFormulas of the linear-time μ-calculus · Cantor-pairing code of linear μ-calculus formulas

DefinitionFuelled decoding of linear μ-calculus codes#✓fully proved

Fuelled decoding of a linearMuCode number back to a formula. The fuel bounds the recursion depth; linearMuDecode supplies fuel c + 1, which exceeds every formula's depth (see linearDepth_le_code).

Cslib.Modal.LinearMuCalculus.linearMuDecodeFuel · 25 lines

def linearMuDecodeFuel : ℕ → ℕ → Option (LinearMuFormula ℕ)
  | 0, _ => none
  | fuel + 1, c =>
    match Nat.unpair c with
    | (0, a) => some (.atom a)
    | (1, a) => some (.natom a)
    | (2, n) => some (.var n)
    | (3, _) => some .bot
    | (4, _) => some .top
    | (5, r) =>
      match Nat.unpair r with
      | (c₁, c₂) =>
        match linearMuDecodeFuel fuel c₁, linearMuDecodeFuel fuel c₂ with
        | some f₁, some f₂ => some (.and f₁ f₂)
        | _, _ => none
    | (6, r) =>
      match Nat.unpair r with
      | (c₁, c₂) =>
        match linearMuDecodeFuel fuel c₁, linearMuDecodeFuel fuel c₂ with
        | some f₁, some f₂ => some (.or f₁ f₂)
        | _, _ => none
    | (7, c₁) => .next <$> linearMuDecodeFuel fuel c₁
    | (8, c₁) => .mu <$> linearMuDecodeFuel fuel c₁
    | (9, c₁) => .nu <$> linearMuDecodeFuel fuel c₁
    | (_, _) => none

Uses 1 · Used by 2

Statement usesFormulas of the linear-time μ-calculus

Used byDecoding linear μ-calculus codes · Fuelled decoding inverts encoding

DefinitionDecoding linear μ-calculus codes#✓fully proved

Decode a linearMuCode number back to the formula it encodes.

def linearMuDecode (c : ℕ) : Option (LinearMuFormula ℕ) :=
  linearMuDecodeFuel (c + 1) c

Uses 2 · Used by 1

Statement usesFormulas of the linear-time μ-calculus · Fuelled decoding of linear μ-calculus codes

Used byDecoding inverts the linear μ-calculus encoding

TheoremFormula depth is bounded by its code#✓fully proved

A formula's depth is at most its code: pairing dominates each component (Nat.add_le_pair).

theorem linearDepth_le_code : ∀ φ : LinearMuFormula ℕ,
    LinearMuFormula.depth φ ≤ linearMuCode φ

Uses 3 · Used by 1

Statement usesFormulas of the linear-time μ-calculus · Depth of a linear μ-calculus formula · Cantor-pairing code of linear μ-calculus formulas

Used byDecoding inverts the linear μ-calculus encoding

TheoremFuelled decoding inverts encoding#✓fully proved

Decoding inverts encoding, with enough fuel.

theorem linearMuDecodeFuel_linearMuCode : ∀ (φ : LinearMuFormula ℕ) (fuel : ℕ),
    LinearMuFormula.depth φ ≤ fuel →
    linearMuDecodeFuel (fuel + 1) (linearMuCode φ) = some φ

Uses 4 · Used by 1

Statement usesFormulas of the linear-time μ-calculus · Depth of a linear μ-calculus formula · Cantor-pairing code of linear μ-calculus formulas · Fuelled decoding of linear μ-calculus codes

Used byDecoding inverts the linear μ-calculus encoding

TheoremDecoding inverts the linear μ-calculus encoding#✓fully proved

Decoding inverts encoding.

theorem linearMuDecode_linearMuCode (φ : LinearMuFormula ℕ) :
    linearMuDecode (linearMuCode φ) = some φ

Uses 5

Statement usesFormulas of the linear-time μ-calculus · Cantor-pairing code of linear μ-calculus formulas · Decoding linear μ-calculus codes

Proof usesFormula depth is bounded by its code · Fuelled decoding inverts encoding

DefinitionToken-list encoding of linear μ-calculus formulas#✓fully proved

A polynomial-size token-list encoding of linear μ-calculus formulas over ℕ atoms, used for the complexity statements in WantedExt. Each connective contributes one tag token (Nat.pair of a small tag with 0), and each atom or variable contributes one token Nat.pair tag value, whose binary size is O(log value). The canonical bitstring encoding of a List ℕ delimits each token, so the bitstring for a formula has length linear in the number of connectives plus the total binary size of its atoms: next^d (atom 0) is encoded by exactly d + 1 tokens, unlike its Cantor-paired linearMuCode, whose binary length is exponential in d.

def linearMuTokens : LinearMuFormula ℕ → List ℕ
  | .atom a => [Nat.pair 0 a]
  | .natom a => [Nat.pair 1 a]
  | .var n => [Nat.pair 2 n]
  | .bot => [Nat.pair 3 0]
  | .top => [Nat.pair 4 0]
  | .and φ ψ => Nat.pair 5 0 :: linearMuTokens φ ++ linearMuTokens ψ
  | .or φ ψ => Nat.pair 6 0 :: linearMuTokens φ ++ linearMuTokens ψ
  | .next φ => Nat.pair 7 0 :: linearMuTokens φ
  | .mu φ => Nat.pair 8 0 :: linearMuTokens φ
  | .nu φ => Nat.pair 9 0 :: linearMuTokens φ

Uses 1 · Used by 2

Statement usesFormulas of the linear-time μ-calculus

Used byToken-list decoding inverts linear μ-calculus token encoding · Fuelled parsing inverts linear μ-calculus token encoding

DefinitionFuelled parser for linear μ-calculus token lists#✓fully proved

Fuelled parsing of a linearMuTokens token list back to a formula, returning the formula and the unconsumed suffix. The fuel bounds the recursion depth; linearMuDecodeList supplies fuel l.length + 1, which exceeds the token length of every formula encoded in l.

Cslib.Modal.LinearMuCalculus.linearMuParseFuel · 39 lines

def linearMuParseFuel : ℕ → List ℕ → Option (LinearMuFormula ℕ × List ℕ)
  | 0, _ => none
  | fuel + 1, xs =>
    match xs with
    | [] => none
    | c :: rest =>
      match Nat.unpair c with
      | (0, a) => some (.atom a, rest)
      | (1, a) => some (.natom a, rest)
      | (2, n) => some (.var n, rest)
      | (3, _) => some (.bot, rest)
      | (4, _) => some (.top, rest)
      | (5, _) =>
        match linearMuParseFuel fuel rest with
        | some (φ, rest₁) =>
          match linearMuParseFuel fuel rest₁ with
          | some (ψ, rest₂) => some (.and φ ψ, rest₂)
          | none => none
        | none => none
      | (6, _) =>
        match linearMuParseFuel fuel rest with
        | some (φ, rest₁) =>
          match linearMuParseFuel fuel rest₁ with
          | some (ψ, rest₂) => some (.or φ ψ, rest₂)
          | none => none
        | none => none
      | (7, _) =>
        match linearMuParseFuel fuel rest with
        | some (φ, rest₁) => some (.next φ, rest₁)
        | none => none
      | (8, _) =>
        match linearMuParseFuel fuel rest with
        | some (φ, rest₁) => some (.mu φ, rest₁)
        | none => none
      | (9, _) =>
        match linearMuParseFuel fuel rest with
        | some (φ, rest₁) => some (.nu φ, rest₁)
        | none => none
      | (_, _) => none

Uses 1 · Used by 3

Statement usesFormulas of the linear-time μ-calculus

Used byDecoding a linear μ-calculus token list to a formula · Token-list decoding inverts linear μ-calculus token encoding · Fuelled parsing inverts linear μ-calculus token encoding

DefinitionDecoding a linear μ-calculus token list to a formula#✓fully proved

Decode a linearMuTokens token list back to the formula it encodes, rejecting trailing tokens.

def linearMuDecodeList (l : List ℕ) : Option (LinearMuFormula ℕ) :=
  match linearMuParseFuel (l.length + 1) l with
  | some (φ, []) => some φ
  | _ => none

Uses 2 · Used by 4

Statement usesFormulas of the linear-time μ-calculus · Fuelled parser for linear μ-calculus token lists

Used byToken-list decoding inverts linear μ-calculus token encoding · Linear μ-calculus model checking as a decision problem · Linear μ-calculus satisfiability as a decision problem · Linear μ-calculus validity as a decision problem

TheoremFuelled parsing inverts linear μ-calculus token encoding#✓fully proved

Parsing inverts token encoding, with enough fuel.

theorem linearMuParseFuel_tokens : ∀ (φ : LinearMuFormula ℕ) (rest : List ℕ) (fuel : ℕ),
    (linearMuTokens φ).length ≤ fuel →
    linearMuParseFuel (fuel + 1) (linearMuTokens φ ++ rest) = some (φ, rest)

Uses 3 · Used by 1

Statement usesFormulas of the linear-time μ-calculus · Fuelled parser for linear μ-calculus token lists · Token-list encoding of linear μ-calculus formulas

Used byToken-list decoding inverts linear μ-calculus token encoding

TheoremToken-list decoding inverts linear μ-calculus token encoding#✓fully proved

Decoding inverts token encoding.

theorem linearMuDecodeList_tokens (φ : LinearMuFormula ℕ) :
    linearMuDecodeList (linearMuTokens φ) = some φ

Uses 5

Statement usesFormulas of the linear-time μ-calculus · Decoding a linear μ-calculus token list to a formula · Token-list encoding of linear μ-calculus formulas

Proof usesFuelled parser for linear μ-calculus token lists · Fuelled parsing inverts linear μ-calculus token encoding

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.