Lax Lean Archive

While this submission is a draft, it cannot be used by other submissions.

Reductions in first-order logic with a deterministic transitive closure

Lax945089.TransitiveClosureReductions · concepts/Lax945089/TransitiveClosureReductions.lean · lax-945089

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

    A parameterized walk over a vocabulary is a finite set of modes, an arity kk, a number of parameters, and a step formula for each pair of modes, in two kk-tuples of variables and the parameters; at a valuation of the parameters it defines a graph on the pairs of a mode and a kk-tuple, and its reachability relation. Its determinization keeps only the steps that are alone in leaving their node. A finite family of walks gives one relation variable per walk and pair of modes, holding the reachability relation between two nodes of these modes at given parameters.

    An FO(DTC) reduction from a problem PP to a problem QQ consists of a finite family of walks over the ordered expansion of the vocabulary of PP and a relativized first-order interpretation whose formulas may use, beside the vocabulary and the order, the reachability relations of the determinized walks. For every nonempty finite structure and every linear order on it, the interpreted structure must be nonempty and be a yes-instance of QQ exactly when the structure is a yes-instance of PP. This is Immerman's logical form of a deterministic logarithmic-space reduction.

    Concept map
    6 concepts; 12 descendants hidden
    100%
    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A

    Lean source view on GitHub

    1import Mathlib.ModelTheory.Order
    2import Mathlib.ModelTheory.Semantics
    3import Mathlib.Logic.Relation
    4import Mathlib.Data.Finite.Sigma
    5import Mathlib.Data.Finite.Prod
    6import Lax904597.Problems
    7import Lax904597.Interpretations
    8import Lax904597.Relativized
    9import Lax904597.SecondOrder
    10import Lax535992.InflationaryFixedPoint
    11
    12/-!
    13---
    14title: Reductions in first-order logic with a deterministic transitive closure
    15type: definition
    16---
    17A parameterized walk over a vocabulary is a finite set of modes, an arity
    18kk, a number of parameters, and a step formula for each pair of modes, in
    19two kk-tuples of variables and the parameters; at a valuation of the
    20parameters it defines a graph on the pairs of a mode and a kk-tuple, and
    21its reachability relation. Its determinization keeps only the steps that
    22are alone in leaving their node. A finite family of walks gives one
    23relation variable per walk and pair of modes, holding the reachability
    24relation between two nodes of these modes at given parameters.
    25
    26An FO(DTC) reduction from a problem PP to a problem QQ consists of a
    27finite family of walks over the ordered expansion of the vocabulary of PP
    28and a relativized first-order interpretation whose formulas may use, beside
    29the vocabulary and the order, the reachability relations of the
    30determinized walks. For every nonempty finite structure and every linear
    31order on it, the interpreted structure must be nonempty and be a
    32yes-instance of QQ exactly when the structure is a yes-instance of PP.
    33This is Immerman's logical form of a deterministic logarithmic-space
    34reduction.
    35-/
    36
    37namespace Lax945089.TransitiveClosureReductions
    38
    39open Lax904597.Problems Lax904597.Relativized Lax904597.SecondOrder
    40open Lax535992.InflationaryFixedPoint
    41
    42open FirstOrder
    43
    44open Language Structure
    45
    46/-- A **parameterized transitive-closure specification**: a walk on `k`-tuples
    47carrying a finite mode, whose step formula may mention `par` parameters beside
    48the current and the next tuple. It has no source and target formulas: what it
    49defines is the reachability *relation*. -/
    50structure ParamTCSpec (L : Language.{0, 0}) : Type 1 where
    51 /-- The modes: the finite control the walk carries beside its tuple. -/
    52 Mode : Type
    53 /-- Modes are finite. -/
    54 [modeFinite : Finite Mode]
    55 /-- The walk runs on `k`-tuples of elements. -/
    56 k : ℕ
    57 /-- The number of parameters the step formula may mention. -/
    58 par : ℕ
    59 /-- The step formula, one per pair of modes: the current tuple, the next
    60 tuple, then the parameters. -/
    61 step : Mode → Mode → L.Formula ((Fin k ⊕ Fin k) ⊕ Fin par)
    62
    63namespace ParamTCSpec
    64
    65variable {L : Language.{0, 0}} (s : ParamTCSpec L) {A : Type} [L.Structure A]
    66
    67attribute [instance] modeFinite
    68
    69variable (A) in
    70/-- A node of the walk: a mode together with a `k`-tuple. -/
    71abbrev Node : Type := s.Mode × (Fin s.k → A)
    72
    73/-- One step of the walk, at a valuation of the parameters. -/
    74def StepAt (z : Fin s.par → A) (a b : s.Node A) : Prop :=
    75 (s.step a.1 b.1).Realize (Sum.elim (Sum.elim a.2 b.2) z)
    76
    77/-- Reachability in the walk, at a valuation of the parameters. -/
    78abbrev ReachAt (z : Fin s.par → A) : s.Node A → s.Node A → Prop :=
    79 Relation.ReflTransGen (s.StepAt z)
    80
    81/-- The position of the `i`-th coordinate of the *first* tuple. -/
    82def leftIx (i : Fin s.k) : Fin (s.k + s.k + s.par) := ⟨i, by have := i.isLt; omega⟩
    83
    84/-- The position of the `i`-th coordinate of the *second* tuple. -/
    85def rightIx (i : Fin s.k) : Fin (s.k + s.k + s.par) := ⟨s.k + i, by have := i.isLt; omega⟩
    86
    87/-- The position of the `j`-th parameter. -/
    88def parIx (j : Fin s.par) : Fin (s.k + s.k + s.par) := ⟨s.k + s.k + j, by have := j.isLt; omega⟩
    89
    90end ParamTCSpec
    91
    92/-- A finite family of parameterized walks. Its relation variables – one per
    93walk and ordered pair of that walk's modes – are what an FO(TC) reduction's
    94formulas may read. -/
    95structure TCFamily (L : Language.{0, 0}) : Type 1 where
    96 /-- The index type of the family. -/
    97 Ix : Type
    98 /-- The family is finite. -/
    99 [ixFinite : Finite Ix]
    100 /-- The walk of each index. -/
    101 spec : Ix → ParamTCSpec L
    102
    103namespace TCFamily
    104
    105variable {L : Language.{0, 0}} (F : TCFamily L)
    106
    107attribute [instance] ixFinite
    108
    109/-- The block of relation variables of a family: one variable per walk and
    110ordered pair of modes, of arity “two tuples and the parameters”. -/
    111def block : SOBlock where
    112 ι := Σ i : F.Ix, (F.spec i).Mode × (F.spec i).Mode
    113 arity := fun q => (F.spec q.1).k + (F.spec q.1).k + (F.spec q.1).par
    114
    115variable {F} {A : Type} [L.Structure A]
    116
    117/-- The assignment the block *has*, as opposed to one a second-order
    118quantifier would guess: each variable holds the reachability relation of its
    119walk, at the parameters read off the tuple. -/
    120def reachAssign (F : TCFamily L) (A : Type) [L.Structure A] : F.block.Assignment A :=
    121 fun q w =>
    122 (F.spec q.1).ReachAt (fun j => w ((F.spec q.1).parIx j))
    123 (q.2.1, fun i => w ((F.spec q.1).leftIx i))
    124 (q.2.2, fun i => w ((F.spec q.1).rightIx i))
    125
    126end TCFamily
    127
    128open FirstOrder
    129
    130open Language Structure
    131
    132/-- An **FO(TC) interpretation**: a relativized first-order interpretation
    133whose formulas may read the reachability relations of a finite family of
    134first-order walks over the base structure.
    135
    136Over an ordered base (`L := L₀.sum Language.order`) this is Immerman's FO(TC)
    137reduction, the logical form of a logarithmic-space reduction. -/
    138structure TCInterpretation (L L' : Language.{0, 0}) (Tag : Type) (dim : ℕ) : Type 1 where
    139 /-- The walks whose reachability relations the formulas may read. -/
    140 fam : TCFamily L
    141 /-- The interpretation, over the base vocabulary expanded by the walks'
    142 relation variables. -/
    143 toRel : RelFOInterpretation (L.sum fam.block.lang) L' Tag dim
    144
    145namespace TCInterpretation
    146
    147variable {L L' : Language.{0, 0}} {Tag : Type} {dim : ℕ}
    148
    149variable (I : TCInterpretation L L' Tag dim) (A : Type) [L.Structure A]
    150
    151/-- The base structure expanded by the reachability relations of the walks –
    152the structure the interpretation is read over. -/
    153@[reducible]
    154def expStructure : (L.sum I.fam.block.lang).Structure A :=
    155 SOBlock.structure₁ (L := L) I.fam.block (I.fam.reachAssign A)
    156
    157/-- The universe of the interpreted structure. -/
    158def Map : Type :=
    159 letI := I.expStructure A
    160 I.toRel.MapRel A
    161
    162/-- The `L'`-structure interpreted in `A`. -/
    163instance mapStructure [L'.IsRelational] : L'.Structure (I.Map A) :=
    164 letI := I.expStructure A
    165 RelFOInterpretation.mapRelStructure I.toRel A
    166
    167end TCInterpretation
    168
    169open FirstOrder
    170
    171open Language Structure
    172
    173namespace ParamTCSpec
    174
    175variable {L : Language.{0, 0}} (s : ParamTCSpec L)
    176
    177/-- The renaming used by the uniqueness clause: the step formula is re-read
    178with its first tuple still the current one, its second tuple the freshly
    179quantified `w̄`, and its parameters unchanged. -/
    180def detVar : ((Fin s.k ⊕ Fin s.k) ⊕ Fin s.par) → (((Fin s.k ⊕ Fin s.k) ⊕ Fin s.par) ⊕ Fin s.k)
    181 | Sum.inl (Sum.inl i) => Sum.inl (Sum.inl (Sum.inl i))
    182 | Sum.inl (Sum.inr i) => Sum.inr i
    183 | Sum.inr j => Sum.inl (Sum.inr j)
    184
    185open Classical in
    186/-- **The determinized step formula** at a pair of modes: this step, and no
    187other step out of the current node. As in
    188`TCSpec.detStep`, the competing successor's mode is
    189compared statically, so the uniqueness clause has one conjunct per mode. -/
    190noncomputable def detStep (m n : s.Mode) : L.Formula ((Fin s.k ⊕ Fin s.k) ⊕ Fin s.par) :=
    191 s.step m n ⊓
    192 Formula.iInf fun m' : s.Mode =>
    193 Formula.iAlls (Fin s.k)
    194 (((s.step m m').relabel s.detVar).imp
    195 (if m' = n then
    196 Formula.iInf fun i : Fin s.k =>
    197 Term.equal (Term.var (Sum.inr i)) (Term.var (Sum.inl (Sum.inl (Sum.inr i))))
    198 else ⊥))
    199
    200/-- **The deterministic reading of a walk**: the same modes, arity and
    201parameters, with the step formula replaced by its determinization.
    202
    203Reducible, so that the modes, the arity, and the parameter count of `s.det` are
    204those of `s` transparently – a node of the deterministic reading *is* a node,
    205and the block of a determinized family *is* the block of the family. -/
    206@[reducible]
    207noncomputable def det : ParamTCSpec L where
    208 Mode := s.Mode
    209 k := s.k
    210 par := s.par
    211 step := s.detStep
    212
    213end ParamTCSpec
    214
    215namespace TCFamily
    216
    217variable {L : Language.{0, 0}} (F : TCFamily L)
    218
    219/-- The deterministic reading of a family: every walk read through its
    220determinization. Reducible, so that `F.det.block` *is* `F.block`. -/
    221@[reducible]
    222noncomputable def det : TCFamily L where
    223 Ix := F.Ix
    224 spec := fun i => (F.spec i).det
    225
    226end TCFamily
    227
    228/-- An **FO(DTC) reduction** from `P` to `Q` – a deterministic
    229logarithmic-space reduction, in the logical form of Immerman: an interpretation over the ordered
    230expansion whose formulas may read the reachability relations of a family of
    231walks, each read through its determinization. -/
    232structure DTCReduction {L L' : Language.{0, 0}} [L.IsRelational] [L'.IsRelational]
    233 (P : DecisionProblem L)
    234 (Q : DecisionProblem L') : Type 1 where
    235 /-- The tags used by the underlying interpretation. -/
    236 Tag : Type
    237 /-- Tags are finite, so that finite structures map to finite structures. -/
    238 [tagFinite : Finite Tag]
    239 /-- The dimension of the underlying interpretation. -/
    240 dim : ℕ
    241 /-- The walks the formulas may read – *before* determinization, which is how
    242 they are read. -/
    243 fam : TCFamily (L.sum Language.order)
    244 /-- The interpretation, over the base expanded by the walks' relation
    245 variables. -/
    246 toRel : RelFOInterpretation ((L.sum Language.order).sum fam.block.lang) L' Tag dim
    247 /-- The interpreted structure is nonempty on nonempty finite ordered
    248 inputs. -/
    249 map_nonempty : ∀ (A : Type) [L.Structure A] [LinearOrder A] [Finite A] [Nonempty A],
    250 Nonempty (TCInterpretation.Map ⟨fam.det, toRel⟩ A)
    251 /-- Yes-instances map exactly to yes-instances, whatever the linear order. -/
    252 correct : ∀ (A : Type) [L.Structure A] [LinearOrder A] [Finite A] [Nonempty A],
    253 P A ↔ Q (TCInterpretation.Map ⟨fam.det, toRel⟩ A)
    254
    255end Lax945089.TransitiveClosureReductions
    256
    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…