Quantifier-free logic over word models

The quantifier-free (QF) fragment of the logic of word models. Terms are built from a variable by applying the successor/predecessor partial functions; formulas are boolean combinations of atomic label/equality/definedness tests. Because successor is a function, a QF term reaches a bounded neighbourhood of its variable with no quantifiers — the syntactic counterpart of strict locality (an existential like ∃w,y[succ w x ∧ succ x y ∧ …] collapses to the quantifier-free … (pred x) ∧ … (succ x)). The locality bridge (Logic/LocalityBridge.lean) makes this precise: QF-definable transductions are exactly the Input-Strictly-Local functions of Subregular ([Cha14a], [CJ19]).

Main definitions

• Subregular.Logic.Term — QF terms (var, succ, pred); Term.eval interprets them.
• Subregular.Logic.Atom / QF — atomic and quantifier-free formulas.
• Atom.Realize / QF.Realize — satisfaction in a word model under an assignment, decidable.
• QF.initial / QF.final — edge positions, derived from definedness of pred/succ.

Implementation notes

Realize is Prop-valued (mathlib's model-theory idiom) with a derived Decidable instance, so worked examples close by decide. A Term evaluates to Option ℕ, none once it falls off an edge; atoms over an undefined term are false.

inductive Subregular.Logic.Term (V : Type u_3) : Type u_3

Quantifier-free terms: a variable, or the successor/predecessor of a term. The succ/pred chains give bounded-window reach without quantifiers.

• var {V : Type u_3} : V → Term V
• succ {V : Type u_3} : Term V → Term V
• pred {V : Type u_3} : Term V → Term V

@[implicit_reducible]

instance Subregular.Logic.instDecidableEqTerm {V✝ : Type u_3} [DecidableEq V✝] : DecidableEq (Term V✝)

Equations

• Subregular.Logic.instDecidableEqTerm = Subregular.Logic.instDecidableEqTerm.decEq

def Subregular.Logic.instDecidableEqTerm.decEq {V✝ : Type u_3} [DecidableEq V✝] (x✝ x✝¹ : Term V✝) : Decidable (x✝ = x✝¹)

Equations

• Subregular.Logic.instDecidableEqTerm.decEq (Subregular.Logic.Term.var a) (Subregular.Logic.Term.var b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Subregular.Logic.instDecidableEqTerm.decEq (Subregular.Logic.Term.var a) a_1.succ = isFalse ⋯
• Subregular.Logic.instDecidableEqTerm.decEq (Subregular.Logic.Term.var a) a_1.pred = isFalse ⋯
• Subregular.Logic.instDecidableEqTerm.decEq a.succ (Subregular.Logic.Term.var a_1) = isFalse ⋯
• Subregular.Logic.instDecidableEqTerm.decEq a.succ b.succ = if h : a = b then h ▸ have inst := Subregular.Logic.instDecidableEqTerm.decEq a a; isTrue ⋯ else isFalse ⋯
• Subregular.Logic.instDecidableEqTerm.decEq a.succ a_1.pred = isFalse ⋯
• Subregular.Logic.instDecidableEqTerm.decEq a.pred (Subregular.Logic.Term.var a_1) = isFalse ⋯
• Subregular.Logic.instDecidableEqTerm.decEq a.pred a_1.succ = isFalse ⋯
• Subregular.Logic.instDecidableEqTerm.decEq a.pred b.pred = if h : a = b then h ▸ have inst := Subregular.Logic.instDecidableEqTerm.decEq a a; isTrue ⋯ else isFalse ⋯

def Subregular.Logic.Term.eval {α : Type u_1} {V : Type u_2} (w : WordModel α) (ρ : V → ℕ) : Term V → Option ℕ

Interpret a term in a word model under an assignment ρ of variables to positions; none if it falls off an edge.

Equations

• Subregular.Logic.Term.eval w ρ (Subregular.Logic.Term.var v) = if w.Mem (ρ v) then some (ρ v) else none
• Subregular.Logic.Term.eval w ρ t.succ = (Subregular.Logic.Term.eval w ρ t).bind w.succ?
• Subregular.Logic.Term.eval w ρ t.pred = (Subregular.Logic.Term.eval w ρ t).bind w.pred?

Directed terms and substitution

def Subregular.Logic.Term.Backward {V : Type u_2} : Term V → Prop

A term is backward if it uses no successor — only the variable and predecessors, so it reads positions at or before its variable.

Equations

• (Subregular.Logic.Term.var a).Backward = True
• t.pred.Backward = t.Backward
• a.succ.Backward = False

def Subregular.Logic.Term.Forward {V : Type u_2} : Term V → Prop

A term is forward if it uses no predecessor, so it reads positions at or after its variable.

Equations

• (Subregular.Logic.Term.var a).Forward = True
• t.pred.Forward = False
• a.succ.Forward = a.Forward

def Subregular.Logic.Term.pdepth {V : Type u_2} : Term V → ℕ

The predecessor depth of a term: how far back it reaches.

Equations

• (Subregular.Logic.Term.var a).pdepth = 0
• t.pred.pdepth = t.pdepth + 1
• a.succ.pdepth = a.pdepth

@[implicit_reducible]

instance Subregular.Logic.Term.instDecidableBackward {V : Type u_2} (t : Term V) : Decidable t.Backward

Equations

• (Subregular.Logic.Term.var a).instDecidableBackward = isTrue trivial
• t.pred.instDecidableBackward = t.instDecidableBackward
• a.succ.instDecidableBackward = isFalse not_false

@[implicit_reducible]

instance Subregular.Logic.Term.instDecidableForward {V : Type u_2} (t : Term V) : Decidable t.Forward

Equations

• (Subregular.Logic.Term.var a).instDecidableForward = isTrue trivial
• t.pred.instDecidableForward = isFalse not_false
• a.succ.instDecidableForward = a.instDecidableForward

def Subregular.Logic.Term.comp : Term Unit → Term Unit → Term Unit

Substitution into the single variable: t.comp u is t[u/x].

Equations

• (Subregular.Logic.Term.var a).comp x✝ = x✝
• t.succ.comp x✝ = (t.comp x✝).succ
• t.pred.comp x✝ = (t.comp x✝).pred

inductive Subregular.Logic.Atom (α : Type u_3) (V : Type u_4) : Type (max u_3 u_4)

Atomic quantifier-free formulas: a label test, an equality of positions, or a definedness test on a term.

• label {α : Type u_3} {V : Type u_4} : α → Term V → Atom α V
• eq {α : Type u_3} {V : Type u_4} : Term V → Term V → Atom α V
• defined {α : Type u_3} {V : Type u_4} : Term V → Atom α V

inductive Subregular.Logic.QF (α : Type u_3) (V : Type u_4) : Type (max u_3 u_4)

Quantifier-free formulas: boolean combinations of atoms (no quantifiers).

• atom {α : Type u_3} {V : Type u_4} : Atom α V → QF α V
• tru {α : Type u_3} {V : Type u_4} : QF α V
• fls {α : Type u_3} {V : Type u_4} : QF α V
• neg {α : Type u_3} {V : Type u_4} : QF α V → QF α V
• conj {α : Type u_3} {V : Type u_4} : QF α V → QF α V → QF α V
• disj {α : Type u_3} {V : Type u_4} : QF α V → QF α V → QF α V

def Subregular.Logic.Atom.Realize {α : Type u_1} {V : Type u_2} (w : WordModel α) (ρ : V → ℕ) : Atom α V → Prop

Satisfaction of an atom in w under assignment ρ.

Equations

• Subregular.Logic.Atom.Realize w ρ (Subregular.Logic.Atom.label a t) = ((Subregular.Logic.Term.eval w ρ t).bind w.label? = some a)
• Subregular.Logic.Atom.Realize w ρ (Subregular.Logic.Atom.eq t₁ t₂) = (Subregular.Logic.Term.eval w ρ t₁ = Subregular.Logic.Term.eval w ρ t₂ ∧ Subregular.Logic.Term.eval w ρ t₁ ≠ none)
• Subregular.Logic.Atom.Realize w ρ (Subregular.Logic.Atom.defined t) = (Subregular.Logic.Term.eval w ρ t ≠ none)

@[implicit_reducible]

instance Subregular.Logic.instDecidableRealize {α : Type u_1} {V : Type u_2} [DecidableEq α] (w : WordModel α) (ρ : V → ℕ) (a : Atom α V) : Decidable (Atom.Realize w ρ a)

Equations

• One or more equations did not get rendered due to their size.

def Subregular.Logic.QF.Realize {α : Type u_1} {V : Type u_2} (w : WordModel α) (ρ : V → ℕ) : QF α V → Prop

Satisfaction of a quantifier-free formula in w under assignment ρ.

Equations

• Subregular.Logic.QF.Realize w ρ (Subregular.Logic.QF.atom a) = Subregular.Logic.Atom.Realize w ρ a
• Subregular.Logic.QF.Realize w ρ Subregular.Logic.QF.tru = True
• Subregular.Logic.QF.Realize w ρ Subregular.Logic.QF.fls = False
• Subregular.Logic.QF.Realize w ρ φ.neg = ¬Subregular.Logic.QF.Realize w ρ φ
• Subregular.Logic.QF.Realize w ρ (φ.conj ψ) = (Subregular.Logic.QF.Realize w ρ φ ∧ Subregular.Logic.QF.Realize w ρ ψ)
• Subregular.Logic.QF.Realize w ρ (φ.disj ψ) = (Subregular.Logic.QF.Realize w ρ φ ∨ Subregular.Logic.QF.Realize w ρ ψ)

@[implicit_reducible]

instance Subregular.Logic.QF.instDecidableRealize {α : Type u_1} {V : Type u_2} [DecidableEq α] (w : WordModel α) (ρ : V → ℕ) (φ : QF α V) : Decidable (Realize w ρ φ)

Equations

• Subregular.Logic.QF.instDecidableRealize w ρ (Subregular.Logic.QF.atom a) = Subregular.Logic.QF.instDecidableRealize._aux_1 w ρ a
• Subregular.Logic.QF.instDecidableRealize w ρ Subregular.Logic.QF.tru = isTrue trivial
• Subregular.Logic.QF.instDecidableRealize w ρ Subregular.Logic.QF.fls = isFalse not_false
• Subregular.Logic.QF.instDecidableRealize w ρ φ.neg = instDecidableNot
• Subregular.Logic.QF.instDecidableRealize w ρ (φ.conj ψ) = instDecidableAnd
• Subregular.Logic.QF.instDecidableRealize w ρ (φ.disj ψ) = instDecidableOr

def Subregular.Logic.QF.initial {α : Type u_1} {V : Type u_2} (t : Term V) : QF α V

t is an initial position: in-domain with no predecessor.

Equations

• Subregular.Logic.QF.initial t = (Subregular.Logic.QF.atom (Subregular.Logic.Atom.defined t)).conj (Subregular.Logic.QF.atom (Subregular.Logic.Atom.defined t.pred)).neg

def Subregular.Logic.QF.final {α : Type u_1} {V : Type u_2} (t : Term V) : QF α V

t is a final position: in-domain with no successor.

Equations

• Subregular.Logic.QF.final t = (Subregular.Logic.QF.atom (Subregular.Logic.Atom.defined t)).conj (Subregular.Logic.QF.atom (Subregular.Logic.Atom.defined t.succ)).neg

Worked example

@[implicit_reducible]

instance Subregular.Logic.instDecidableEqSym : DecidableEq Subregular.Logic.Sym✝

Equations

• Subregular.Logic.instDecidableEqSym x✝ y✝ = if h : Subregular.Logic.Sym.ctorIdx✝ x✝ = Subregular.Logic.Sym.ctorIdx✝ y✝ then isTrue ⋯ else isFalse ⋯