Lax Lean Archive

Type trees and their canonical representation

Lax185574.TypeTrees · concepts/Lax185574/TypeTrees.lean · lax-185574

definition

Loading review…

Community review

Flags

Each flag is tied to a public ORCID identity and explains why this concept may be incorrect.

No flags have been submitted.

    Community review

    Flag this concept

    State precisely what appears incorrect. This explanation will be public under your ORCID name.

    No source line selected.

    Natural Language Statement

    Definition

    Let G be a partial graph, k, q ∈ ℕ and ā a tuple of ℓ vertices. The atomic (k, q)-type atp_{k,q}(ā) is the set of atomic distFO formulas of distance rank (k, q) with free variables among x₁, …, x_ℓ that ā satisfies in G. The (k, q)-type tree of ā is

    tree_{k,q}(ā) = (atp_{k,q}(ā), 𝓔_{k,q}(ā)),

    where 𝓔_{k,0}(ā) = ∅ and, for q ≥ 1,

    𝓔_{k,q}(ā) = {(i, tree_{k+1,q−1}(ā b)) | i ∈ [ℓ], b ∈ V(G), dist(aᵢ, b) ≤ ρ⁺(k+1, q−1)}.

    The members of 𝓔_{k,q}(ā) are the extensions, and i is the guard of the extension. The number ℓ is the arity and (k, q) is the rank of the tree.

    Type trees are represented on the RAM in a canonical form, with all sets sorted and free of duplicates, so that two trees are equal exactly when their representations are. The size ‖τ‖ of a tree is the size of its representation, which includes k, q and ℓ.

    For a type tree ν of arity one, [ν]^G is the set of vertices b with tree_{k,q}(b) = ν, where (k, q) is the rank of ν.

    Concept map
    11 concepts
    100%
    DefinitionThis conceptRelated conceptA → B: B builds on ADescendants are omitted for concepts with more than 10 descendants.

    In the paper

    • page 41 of this submission's paper
    • page 45 of this submission's paper

    Lean source view on GitHub

    1import Lax185574.DistanceLogic
    2import Mathlib.Data.Fin.VecNotation
    3
    4/-!
    5---
    6title: Type trees and their canonical representation
    7type: definition
    8---
    9Let G be a partial graph, k, q ∈ ℕ and ā a tuple of ℓ vertices. The
    10*atomic (k, q)-type* atp_{k,q}(ā) is the set of atomic distFO formulas
    11of distance rank (k, q) with free variables among x₁, …, x_ℓ that ā
    12satisfies in G. The *(k, q)-type tree* of ā is
    13
    14 tree_{k,q}(ā) = (atp_{k,q}(ā), 𝓔_{k,q}(ā)),
    15
    16where 𝓔_{k,0}(ā) = ∅ and, for q ≥ 1,
    17
    18 𝓔_{k,q}(ā) = {(i, tree_{k+1,q−1}(ā b)) | i ∈ [ℓ], b ∈ V(G),
    19 dist(aᵢ, b) ≤ ρ⁺(k+1, q−1)}.
    20
    21The members of 𝓔_{k,q}(ā) are the *extensions*, and i is the *guard*
    22of the extension. The number ℓ is the *arity* and (k, q) is the *rank*
    23of the tree.
    24
    25Type trees are represented on the RAM in a canonical form, with all sets
    26sorted and free of duplicates, so that two trees are equal exactly when
    27their representations are. The size ‖τ‖ of a tree is the size of its
    28representation, which includes k, q and ℓ.
    29
    30For a type tree ν of arity one, [ν]^G is the set of vertices b with
    31tree_{k,q}(b) = ν, where (k, q) is the rank of ν.
    32
    33# Formalization notes
    34
    35A type tree is a Lean object of type `TypeTree`. It records its rank
    36(k, q), its arity ℓ and its root, an element of `Node q ℓ`. A root of
    37depth 0 is its root label, the finite set of its atoms. A root of depth
    38q + 1 is its root label together with the finite set of its extensions,
    39pairs of a guard and a root of depth q and arity ℓ + 1. The trees inside
    40a tree carry no rank and arity, since these are determined by the
    41enclosing tree. Equality of type trees in the paper is equality of
    42these objects.
    43
    44The canonical representation of a type tree is its encoding, in the
    45sense of `Lax185574.Encoding`. It is the header k, q, ℓ, followed by the
    46encoding of the set of atoms of the root and, at depth at least one, the
    47encoding of the set of extensions. An atom is encoded as a formula of
    48`Lax185574.DistanceLogic`, and an extension (i, μ) by i followed by the
    49encoding of μ. Finite sets are encoded sorted and without repetitions,
    50so the encoding is determined by the tree. The size ‖τ‖ is the length of
    51the encoding, `wordLength τ`. The operations of the paper are computed
    52by word RAM programs on these encodings.
    53
    54The algorithms of the model-checking procedure receive and return the
    55family (tree_{k,q}(a) : a ∈ V(G)) of the type trees of all vertices of a
    56partial graph on `Fin n`. It is `family G k q`, a function on `Fin n`,
    57encoded as the list of its members in the order of the vertices.
    58
    59Sets are turned into finite sets by `finsetOf`. On an infinite set it
    60returns the empty set. This case does not occur for partial graphs on a
    61finite vertex type, where all the sets involved are finite. In
    62particular, only finitely many colors occur, and an atom with a color
    63that does not occur is false.
    64-/
    65
    66namespace Lax185574.TypeTrees
    67
    68open Lax185574.PartialGraphs Lax185574.GaifmanGraph Lax185574.Encoding
    69open Lax185574.DistanceLogic Lax185574.DistanceLogic.DistFO
    70open Lax3.DistFO (rhoMinus rhoPlus)
    71
    72/-- `Node q ℓ`: the roots of the type trees of depth `q` and arity `ℓ`.
    73A root of depth `0` is its set of atoms. A root of depth `q + 1` is its
    74set of atoms together with its set of extensions, pairs of a guard and
    75a root of depth `q` and arity `ℓ + 1`. -/
    76def Node : ℕ → ℕ → Type
    77 | 0, ℓ => Finset (DistFO ℓ)
    78 | q + 1, ℓ => Finset (DistFO ℓ) × Finset (Fin ℓ × Node q (ℓ + 1))
    79
    80/-- A root of depth `0` is encoded by its set of atoms. A root of depth
    81`q + 1` is encoded by its set of atoms followed by its set of
    82extensions. `Node` is defined by recursion on the depth and is not an
    83inductive type, so its encoding is given by the same recursion. -/
    84@[instance_reducible] def Node.instEncode : (q ℓ : ℕ) → Encode (Node q ℓ)
    85 | 0, ℓ => inferInstanceAs (Encode (Finset (DistFO ℓ)))
    86 | q + 1, ℓ =>
    87 letI := Node.instEncode q (ℓ + 1)
    88 inferInstanceAs (Encode (Finset (DistFO ℓ) × Finset (Fin ℓ × Node q (ℓ + 1))))
    89
    90instance {q ℓ : ℕ} : Encode (Node q ℓ) := Node.instEncode q ℓ
    91
    92/-- A type tree: its rank `(k, q)`, its arity `ℓ` and its root. -/
    93structure TypeTree where
    94 /-- The first component of the rank. -/
    95 k : ℕ
    96 /-- The depth, the second component of the rank. -/
    97 q : ℕ
    98 /-- The arity. -/
    99 ℓ : ℕ
    100 /-- The root. -/
    101 root : Node q ℓ
    102 deriving Encode
    103
    104variable {V : Type*}
    105
    106/-- The finite set with the elements of `S`, and `∅` if `S` is
    107infinite. -/
    108noncomputable def finsetOf {α : Type*} (S : Set α) : Finset α :=
    109 open Classical in if h : S.Finite then h.toFinset else ∅
    110
    111/-- `atp_{k,q}(a)`: the atoms of distance rank `(k, q)` satisfied by the
    112tuple `a`. -/
    113def atp (G : PartialGraph V) (k q : ℕ) {ℓ : ℕ} (a : Fin ℓ → V) : Set (DistFO ℓ) :=
    114 {φ | IsAtom φ ∧ DRank k q φ ∧ Sat G a φ}
    115
    116/-- The root of `tree_{k,q}(a)`: the atoms of `atp_{k,q}(a)` and, for
    117`q ≥ 1`, the extensions `(i, tree_{k+1,q−1}(a b))`. -/
    118noncomputable def node (G : PartialGraph V) : (k q : ℕ) → {ℓ : ℕ} → (Fin ℓ → V) → Node q ℓ
    119 | k, 0, _, a => finsetOf (atp G k 0 a)
    120 | k, q + 1, ℓ, a =>
    121 (finsetOf (atp G k (q + 1) a),
    122 finsetOf {e | ∃ (i : Fin ℓ) (b : V),
    123 WithinDist G.resolved (rhoPlus (k + 1) q) (a i) b ∧
    124 e = (i, node G (k + 1) q (Fin.snoc a b))})
    125
    126/-- `tree_{k,q}(a)`. -/
    127noncomputable def tree (G : PartialGraph V) (k q : ℕ) {ℓ : ℕ} (a : Fin ℓ → V) : TypeTree :=
    128 ⟨k, q, ℓ, node G k q a⟩
    129
    130/-- `[ν]^G`: the vertices whose type tree is `ν`. The rank is read off
    131`ν`, which records it. -/
    132def realizations (G : PartialGraph V) (ν : TypeTree) : Set V :=
    133 {b | tree G ν.k ν.q ![b] = ν}
    134
    135/-- The family `(tree_{k,q}(a) : a ∈ V(G))` of the type trees of all
    136vertices. -/
    137noncomputable def family {n : ℕ} (G : PartialGraph (Fin n)) (k q : ℕ) : Fin n → TypeTree :=
    138 fun a => tree G k q ![a]
    139
    140/-- The largest size of a tree of the family. -/
    141noncomputable def maxTreeSize {n : ℕ} (G : PartialGraph (Fin n)) (k q : ℕ) : ℕ :=
    142 Finset.univ.sup fun a : Fin n => wordLength (family G k q a)
    143
    144end Lax185574.TypeTrees
    145
    Formalization notes

    A type tree is a Lean object of type TypeTreeTypeTree. It records its rank (k, q), its arity ℓ and its root, an element of NodeqℓNode q ℓ. A root of depth 0 is its root label, the finite set of its atoms. A root of depth q + 1 is its root label together with the finite set of its extensions, pairs of a guard and a root of depth q and arity ℓ + 1. The trees inside a tree carry no rank and arity, since these are determined by the enclosing tree. Equality of type trees in the paper is equality of these objects.

    The canonical representation of a type tree is its encoding, in the sense of Lax185574.EncodingLax185574.Encoding. It is the header k, q, ℓ, followed by the encoding of the set of atoms of the root and, at depth at least one, the encoding of the set of extensions. An atom is encoded as a formula of Lax185574.DistanceLogicLax185574.DistanceLogic, and an extension (i, μ) by i followed by the encoding of μ. Finite sets are encoded sorted and without repetitions, so the encoding is determined by the tree. The size ‖τ‖ is the length of the encoding, wordLengthτwordLength τ. The operations of the paper are computed by word RAM programs on these encodings.

    The algorithms of the model-checking procedure receive and return the family (tree_{k,q}(a) : a ∈ V(G)) of the type trees of all vertices of a partial graph on FinnFin n. It is familyGkqfamily G k q, a function on FinnFin n, encoded as the list of its members in the order of the vertices.

    Sets are turned into finite sets by finsetOffinsetOf. On an infinite set it returns the empty set. This case does not occur for partial graphs on a finite vertex type, where all the sets involved are finite. In particular, only finitely many colors occur, and an atom with a color that does not occur is false.

    Builds on
    Used by
    From Mathlib

    Discussion

    Ask a question or add context. Endorsements and structured flags are kept in the review panel above.

    Loading discussion…