Tree models and quantifier-free logic over them

The hierarchical counterpart of Logic/WordModel.lean: the model-theoretic representation of finite labeled trees, the foundation for logical characterizations of tree-to-tree subregular maps. A tree model is a RoseTree L — a node-labeled rose tree — addressed by Gorn indices (List ℕ); its relations are dominance (parent/child) and sibling precedence. Quantifier-free terms navigate by parent/child/sibSucc/sibPred partial functions, giving the bounded reach that, as on strings, underlies tree-local computation.

The model is generic over the label type L; downstream layers instantiate it.

Main definitions

• Subregular.Logic.TreeModel — a labeled tree, addressed by Gorn indices.
• TreeModel.nodeAt / labelAt? — navigate to / read the label at an address.
• TreeTerm / TreeTerm.eval — QF tree terms (parent/child/sibSucc/sibPred) and their interpretation as partial address maps.
• TreeAtom / TreeQF / TreeQF.Realize — atomic and quantifier-free tree formulas, with decidable satisfaction.

@[reducible, inline]

abbrev Subregular.Logic.TreeModel (L : Type u_3) : Type u_3

A tree model: a node-labeled rose tree, addressed by Gorn indices (List ℕ). The carrier is RoseTree L itself — a labeled tree is its model, as a string is its word model.

Equations

• Subregular.Logic.TreeModel L = RoseTree L

def Subregular.Logic.TreeModel.nodeAt {L : Type u_1} : TreeModel L → List ℕ → Option (TreeModel L)

The subtree rooted at a Gorn address, none if the address leaves the tree.

Equations

• x✝.nodeAt [] = some x✝
• x✝.nodeAt (i :: rest) = match (RoseTree.children x✝)[i]? with | none => none | some c => Subregular.Logic.TreeModel.nodeAt c rest

def Subregular.Logic.TreeModel.labelAt? {L : Type u_1} (t : TreeModel L) (a : List ℕ) : Option L

The label at a Gorn address, none off the tree.

Equations

• t.labelAt? a = Option.map RoseTree.value (t.nodeAt a)

def Subregular.Logic.TreeModel.posOf {L : Type u_1} (t : TreeModel L) (a : List ℕ) : Option (List ℕ)

The address, if it names a node of t; otherwise none.

Equations

• t.posOf a = if (t.nodeAt a).isSome = true then some a else none

Quantifier-free tree terms

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

Quantifier-free tree terms: a variable, or a one-step move to the parent, the i-th child, or the next/previous sibling. The moves are the bounded reach of tree-local logic.

• var {V : Type u_3} : V → TreeTerm V
• parent {V : Type u_3} : TreeTerm V → TreeTerm V
• child {V : Type u_3} : ℕ → TreeTerm V → TreeTerm V
• sibSucc {V : Type u_3} : TreeTerm V → TreeTerm V
• sibPred {V : Type u_3} : TreeTerm V → TreeTerm V

def Subregular.Logic.TreeTerm.eval {L : Type u_1} {V : Type u_2} (t : TreeModel L) (ρ : V → List ℕ) : TreeTerm V → Option (List ℕ)

Interpret a tree term in t under an assignment ρ of variables to addresses; none if a move leaves the tree.

Equations

• One or more equations did not get rendered due to their size.
• Subregular.Logic.TreeTerm.eval t ρ (Subregular.Logic.TreeTerm.var v) = t.posOf (ρ v)
• Subregular.Logic.TreeTerm.eval t ρ s.parent = (Subregular.Logic.TreeTerm.eval t ρ s).bind fun (a : List ℕ) => match a with | [] => none | head :: tail => some a.dropLast
• Subregular.Logic.TreeTerm.eval t ρ (Subregular.Logic.TreeTerm.child i s) = (Subregular.Logic.TreeTerm.eval t ρ s).bind fun (a : List ℕ) => t.posOf (a ++ [i])

inductive Subregular.Logic.TreeAtom (L : Type u_3) (V : Type u_4) : Type (max u_3 u_4)

Atomic quantifier-free tree formulas.

• label {L : Type u_3} {V : Type u_4} : L → TreeTerm V → TreeAtom L V
• eq {L : Type u_3} {V : Type u_4} : TreeTerm V → TreeTerm V → TreeAtom L V
• defined {L : Type u_3} {V : Type u_4} : TreeTerm V → TreeAtom L V

inductive Subregular.Logic.TreeQF (L : Type u_3) (V : Type u_4) : Type (max u_3 u_4)

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

• atom {L : Type u_3} {V : Type u_4} : TreeAtom L V → TreeQF L V
• tru {L : Type u_3} {V : Type u_4} : TreeQF L V
• fls {L : Type u_3} {V : Type u_4} : TreeQF L V
• neg {L : Type u_3} {V : Type u_4} : TreeQF L V → TreeQF L V
• conj {L : Type u_3} {V : Type u_4} : TreeQF L V → TreeQF L V → TreeQF L V
• disj {L : Type u_3} {V : Type u_4} : TreeQF L V → TreeQF L V → TreeQF L V

def Subregular.Logic.TreeAtom.Realize {L : Type u_1} {V : Type u_2} (t : TreeModel L) (ρ : V → List ℕ) : TreeAtom L V → Prop

Satisfaction of a tree atom in t under assignment ρ.

Equations

• One or more equations did not get rendered due to their size.
• Subregular.Logic.TreeAtom.Realize t ρ (Subregular.Logic.TreeAtom.label l s) = ((Subregular.Logic.TreeTerm.eval t ρ s).bind t.labelAt? = some l)
• Subregular.Logic.TreeAtom.Realize t ρ (Subregular.Logic.TreeAtom.defined s) = (Subregular.Logic.TreeTerm.eval t ρ s ≠ none)

@[implicit_reducible]

instance Subregular.Logic.instDecidableRealize {L : Type u_1} {V : Type u_2} [DecidableEq L] (t : TreeModel L) (ρ : V → List ℕ) (a : TreeAtom L V) : Decidable (TreeAtom.Realize t ρ a)

Equations

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

def Subregular.Logic.TreeQF.Realize {L : Type u_1} {V : Type u_2} (t : TreeModel L) (ρ : V → List ℕ) : TreeQF L V → Prop

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

Equations

• Subregular.Logic.TreeQF.Realize t ρ (Subregular.Logic.TreeQF.atom a) = Subregular.Logic.TreeAtom.Realize t ρ a
• Subregular.Logic.TreeQF.Realize t ρ Subregular.Logic.TreeQF.tru = True
• Subregular.Logic.TreeQF.Realize t ρ Subregular.Logic.TreeQF.fls = False
• Subregular.Logic.TreeQF.Realize t ρ φ.neg = ¬Subregular.Logic.TreeQF.Realize t ρ φ
• Subregular.Logic.TreeQF.Realize t ρ (φ.conj ψ) = (Subregular.Logic.TreeQF.Realize t ρ φ ∧ Subregular.Logic.TreeQF.Realize t ρ ψ)
• Subregular.Logic.TreeQF.Realize t ρ (φ.disj ψ) = (Subregular.Logic.TreeQF.Realize t ρ φ ∨ Subregular.Logic.TreeQF.Realize t ρ ψ)

@[implicit_reducible]

instance Subregular.Logic.TreeQF.instDecidableRealize {L : Type u_1} {V : Type u_2} [DecidableEq L] (t : TreeModel L) (ρ : V → List ℕ) (φ : TreeQF L V) : Decidable (Realize t ρ φ)

Equations

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

def Subregular.Logic.TreeQF.isRoot {L : Type u_1} {V : Type u_2} (s : TreeTerm V) : TreeQF L V

s is the root: it has no parent.

Equations

• Subregular.Logic.TreeQF.isRoot s = (Subregular.Logic.TreeQF.atom (Subregular.Logic.TreeAtom.defined s)).conj (Subregular.Logic.TreeQF.atom (Subregular.Logic.TreeAtom.defined s.parent)).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 ⋯