Lax Lean Archive

Distance logic over partial graphs and distance rank

Lax185574.DistanceLogic · concepts/Lax185574/DistanceLogic.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

    The logic distFO extends first-order logic over partial graphs by distance atoms. Its atoms are

    • the first-order atoms x = y, E(x, y), N(x, y) and Y(x), for colors Y;
    • for each radius r ∈ ℕ, the binary distance atom dist(x, y) ≤ r;
    • for each radius r ∈ ℕ and color Y, the unary distance atom dist(x, Y) < r, equivalent to ∃y (Y(y) ∧ dist(x, y) < r).

    Distances are measured in the Gaifman graph of the partial graph, that is, along resolved pairs. A formula is built from atoms by negation, conjunction and the local quantifier ∃y (dist(xᵢ, y) ≤ s ∧ φ(x̄ y)).

    The horizon functions are ρ⁻(k, q) = 9^((k+q+1)q) and ρ⁺(k, q) = 9^((k+q)(q+1)). A formula has distance rank (k, q) if it is a Boolean combination of

    • first-order atoms,
    • binary distance atoms of radius at most ρ⁻(k, q),
    • unary distance atoms of radius at most ρ⁺(k, q), and
    • formulas ∃y (dist(xᵢ, y) ≤ ρ⁺(k+1, q−1) ∧ φ(x̄ y)), where q ≥ 1, xᵢ is a free variable and φ has distance rank (k+1, q−1).
    Concept map
    10 concepts
    100%
    DefinitionThis conceptRelated conceptA → B: B builds on ADescendants are omitted for concepts with more than 10 descendants.

    In the paper

    • page 40 of this submission's paper

    Lean source view on GitHub

    1import Lax185574.PartialGraphs
    2import Lax185574.Encodings
    3import Lax3.DistFO
    4
    5/-!
    6---
    7title: Distance logic over partial graphs and distance rank
    8type: definition
    9---
    10The logic distFO extends first-order logic over partial graphs by
    11*distance atoms*. Its atoms are
    12
    13- the first-order atoms x = y, E(x, y), N(x, y) and Y(x), for colors Y;
    14- for each radius r ∈ ℕ, the *binary distance atom* dist(x, y) ≤ r;
    15- for each radius r ∈ ℕ and color Y, the *unary distance atom*
    16 dist(x, Y) < r, equivalent to ∃y (Y(y) ∧ dist(x, y) < r).
    17
    18Distances are measured in the Gaifman graph of the partial graph, that
    19is, along resolved pairs. A formula is built from atoms by negation,
    20conjunction and the *local quantifier* ∃y (dist(xᵢ, y) ≤ s ∧ φ(x̄ y)).
    21
    22The horizon functions are ρ⁻(k, q) = 9^((k+q+1)q) and
    23ρ⁺(k, q) = 9^((k+q)(q+1)). A formula has *distance rank (k, q)* if it is
    24a Boolean combination of
    25
    26- first-order atoms,
    27- binary distance atoms of radius at most ρ⁻(k, q),
    28- unary distance atoms of radius at most ρ⁺(k, q), and
    29- formulas ∃y (dist(xᵢ, y) ≤ ρ⁺(k+1, q−1) ∧ φ(x̄ y)), where q ≥ 1, xᵢ is a
    30 free variable and φ has distance rank (k+1, q−1).
    31
    32# Formalization notes
    33
    34As in `Lax3.FirstOrder`, free variables are counted: `DistFO ℓ` has ℓ
    35free variables `Fin ℓ`, and the local quantifier binds the new last
    36variable. The radius of a local quantifier is part of the syntax, and
    37the distance rank requires it to be exactly ρ⁺(k+1, q−1), as in the
    38paper. The horizon functions are those of `Lax3.DistFO`, which are the
    39functions of the paper.
    40
    41"dist(x, y) ≤ r" holds if a walk of length at most r joins the two
    42vertices along resolved pairs. "dist(x, Y) < r" holds if some vertex of
    43color Y is joined to x by a walk of length less than r. In particular
    44it is false for r = 0.
    45
    46The works that the paper cites for this logic also allow the
    47unrestricted quantifier ∃y φ(x̄ y), and call the formulas of distance
    48rank (k, q) *local*. The paper considers only these formulas, and omits
    49the adjective. So the syntax here has the local quantifier only, and the
    50formulas of distance rank (k, q) are the same as in the paper.
    51
    52Formulas are handed to algorithms in the derived encoding of
    53`Lax185574.Encoding`, a prefix code: the number of the constructor,
    54from 0 for `eq` to 8 for `exLocal`, followed by the arguments in order.
    55-/
    56
    57namespace Lax185574.DistanceLogic
    58
    59open Lax185574.PartialGraphs Lax185574.GaifmanGraph Lax185574.Encoding
    60open Lax3.DistFO (rhoMinus rhoPlus)
    61
    62/-- Formulas of distance logic over partial graphs with `ℓ` free
    63variables. -/
    64inductive DistFO : ℕ → Type
    65 /-- `xᵢ = xⱼ`. -/
    66 | eq {ℓ : ℕ} (i j : Fin ℓ) : DistFO ℓ
    67 /-- `E(xᵢ, xⱼ)`. -/
    68 | edge {ℓ : ℕ} (i j : Fin ℓ) : DistFO ℓ
    69 /-- `N(xᵢ, xⱼ)`. -/
    70 | nonEdge {ℓ : ℕ} (i j : Fin ℓ) : DistFO ℓ
    71 /-- `Y(xᵢ)`. -/
    72 | color {ℓ : ℕ} (Y : ℕ) (i : Fin ℓ) : DistFO ℓ
    73 /-- `dist(xᵢ, xⱼ) ≤ r`. -/
    74 | distLe {ℓ : ℕ} (r : ℕ) (i j : Fin ℓ) : DistFO ℓ
    75 /-- `dist(xᵢ, Y) < r`. -/
    76 | distColorLt {ℓ : ℕ} (r Y : ℕ) (i : Fin ℓ) : DistFO ℓ
    77 /-- Negation. -/
    78 | not {ℓ : ℕ} (φ : DistFO ℓ) : DistFO ℓ
    79 /-- Conjunction. -/
    80 | and {ℓ : ℕ} (φ ψ : DistFO ℓ) : DistFO ℓ
    81 /-- `∃y (dist(xᵢ, y) ≤ s ∧ φ(x̄ y))`, binding the new last variable. -/
    82 | exLocal {ℓ : ℕ} (i : Fin ℓ) (s : ℕ) (φ : DistFO (ℓ + 1)) : DistFO ℓ
    83 deriving Encode
    84
    85namespace DistFO
    86
    87/-- The formula is an atom. -/
    88def IsAtom {ℓ : ℕ} : DistFO ℓ → Prop
    89 | .not _ | .and _ _ | .exLocal _ _ _ => False
    90 | _ => True
    91
    92/-- Some walk of length less than `r` joins `u` and `v`. -/
    93def WithinDistLt {W : Type*} (G : SimpleGraph W) (r : ℕ) (u v : W) : Prop :=
    94 ∃ p : G.Walk u v, p.length < r
    95
    96variable {V : Type*}
    97
    98/-- Satisfaction in the partial graph `G` under the assignment `m` of
    99vertices to the free variables. -/
    100def Sat (G : PartialGraph V) : {ℓ : ℕ} → (Fin ℓ → V) → DistFO ℓ → Prop
    101 | _, m, .eq i j => m i = m j
    102 | _, m, .edge i j => G.edge.Adj (m i) (m j)
    103 | _, m, .nonEdge i j => G.nonEdge.Adj (m i) (m j)
    104 | _, m, .color Y i => G.color (m i) = Y
    105 | _, m, .distLe r i j => WithinDist G.resolved r (m i) (m j)
    106 | _, m, .distColorLt r Y i => ∃ v, G.color v = Y ∧ WithinDistLt G.resolved r (m i) v
    107 | _, m, .not φ => ¬ Sat G m φ
    108 | _, m, .and φ ψ => Sat G m φ ∧ Sat G m ψ
    109 | _, m, .exLocal i s φ =>
    110 ∃ v, WithinDist G.resolved s (m i) v ∧ Sat G (Fin.snoc m v) φ
    111
    112/-- `DRank k q φ`: the formula `φ` has distance rank `(k, q)`. -/
    113inductive DRank : ℕ → ℕ → {ℓ : ℕ} → DistFO ℓ → Prop
    114 | eq {k q ℓ : ℕ} (i j : Fin ℓ) : DRank k q (.eq i j)
    115 | edge {k q ℓ : ℕ} (i j : Fin ℓ) : DRank k q (.edge i j)
    116 | nonEdge {k q ℓ : ℕ} (i j : Fin ℓ) : DRank k q (.nonEdge i j)
    117 | color {k q ℓ : ℕ} (Y : ℕ) (i : Fin ℓ) : DRank k q (.color Y i)
    118 | distLe {k q ℓ : ℕ} (r : ℕ) (i j : Fin ℓ) :
    119 r ≤ rhoMinus k q → DRank k q (.distLe r i j)
    120 | distColorLt {k q ℓ : ℕ} (r Y : ℕ) (i : Fin ℓ) :
    121 r ≤ rhoPlus k q → DRank k q (.distColorLt r Y i)
    122 | not {k q ℓ : ℕ} {φ : DistFO ℓ} : DRank k q φ → DRank k q (.not φ)
    123 | and {k q ℓ : ℕ} {φ ψ : DistFO ℓ} :
    124 DRank k q φ → DRank k q ψ → DRank k q (.and φ ψ)
    125 | exLocal {k q ℓ : ℕ} (i : Fin ℓ) {φ : DistFO (ℓ + 1)} :
    126 DRank (k + 1) q φ → DRank k (q + 1) (.exLocal i (rhoPlus (k + 1) q) φ)
    127
    128end DistFO
    129
    130end Lax185574.DistanceLogic
    131
    Formalization notes

    As in Lax3.FirstOrderLax3.FirstOrder, free variables are counted: DistFOℓDistFO ℓ has ℓ free variables FinℓFin ℓ, and the local quantifier binds the new last variable. The radius of a local quantifier is part of the syntax, and the distance rank requires it to be exactly ρ⁺(k+1, q−1), as in the paper. The horizon functions are those of Lax3.DistFOLax3.DistFO, which are the functions of the paper.

    "dist(x, y) ≤ r" holds if a walk of length at most r joins the two vertices along resolved pairs. "dist(x, Y) < r" holds if some vertex of color Y is joined to x by a walk of length less than r. In particular it is false for r = 0.

    The works that the paper cites for this logic also allow the unrestricted quantifier ∃y φ(x̄ y), and call the formulas of distance rank (k, q) local. The paper considers only these formulas, and omits the adjective. So the syntax here has the local quantifier only, and the formulas of distance rank (k, q) are the same as in the paper.

    Formulas are handed to algorithms in the derived encoding of Lax185574.EncodingLax185574.Encoding, a prefix code: the number of the constructor, from 0 for eqeq to 8 for exLocalexLocal, followed by the arguments in order.

    Builds on
    Used by
    From Mathlib

    none

    Discussion

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

    Loading discussion…