Semantics and definability in FO(LFP)
Lax751879.FixedPointSemantics · concepts/Lax751879/FixedPointSemantics.lean · lax-751879
No public endorsements yet.
Loading review…
Sign in with ORCIDNatural Language Statement
Definition and theorem
First-order operations have their usual semantics. A fixed-point body, with its parameters held fixed, defines an operator on -ary relations; the fixed-point formula tests membership of its argument tuple in the least fixed point of that operator. Positivity of an admissible body implies monotonicity; this is an explicit proof obligation.
A query is FO(LFP)-definable if one admissible formula defines it on every finite ordered structure and every assignment to its free variables. The formula is chosen once for the query, independently of the structure.
Concept map
Lean source view on GitHub
| 1 | import Lax751879.FixedPointSyntax |
| 2 | import Lax751879.LeastFixedPoints |
| 3 | |
| 4 | /-! |
| 5 | --- |
| 6 | title: Semantics and definability in FO(LFP) |
| 7 | type: definition and theorem |
| 8 | --- |
| 9 | First-order operations have their usual semantics. A fixed-point body, |
| 10 | with its parameters held fixed, defines an operator on -ary relations; |
| 11 | the fixed-point formula tests membership of its argument tuple in the least |
| 12 | fixed point of that operator. Positivity of an admissible body implies |
| 13 | monotonicity; this is an explicit proof obligation. |
| 14 | |
| 15 | A query is FO(LFP)-definable if one admissible formula defines it on every |
| 16 | finite ordered structure and every assignment to its free variables. |
| 17 | The formula is chosen once for the query, independently of the structure. |
| 18 | -/ |
| 19 | |
| 20 | namespace Lax751879.FixedPointSemantics |
| 21 | |
| 22 | open Lax751879.OrderedStructures Lax751879.FixedPointSyntax |
| 23 | open Lax751879.LeastFixedPoints |
| 24 | |
| 25 | abbrev RelationEnv (n : Nat) (ρ : List Nat) := |
| 26 | (r : Fin ρ.length) → Set (Fin (ρ.get r) → Fin n) |
| 27 | |
| 28 | def extend {n k : Nat} {ρ : List Nat} (R : Set (Fin k → Fin n)) |
| 29 | (η : RelationEnv n ρ) : RelationEnv n (k :: ρ) := |
| 30 | Fin.cons R η |
| 31 | |
| 32 | def eval {σ : Vocabulary} {m : Nat} {ρ : List Nat} |
| 33 | (φ : RawFormula σ m ρ) (A : OrderedStructure σ) |
| 34 | (v : Fin m → Fin A.size) (η : RelationEnv A.size ρ) : Prop := |
| 35 | match φ with |
| 36 | | .truth => True |
| 37 | | .equal x y => v x = v y |
| 38 | | .less x y => v x < v y |
| 39 | | .relation r args => A.relation r (v ∘ args) = true |
| 40 | | .variable r args => η r (v ∘ args) |
| 41 | | .neg ψ => ¬ eval ψ A v η |
| 42 | | .conj ψ χ => eval ψ A v η ∧ eval χ A v η |
| 43 | | .exists' ψ => ∃ a, eval ψ A (Fin.cons a v) η |
| 44 | | .lfp _ body args => |
| 45 | leastFixedPoint (fun R => {a | eval body A (Fin.append a v) (extend R η)}) |
| 46 | (v ∘ args) |
| 47 | |
| 48 | def bodyOperator {σ : Vocabulary} {m k : Nat} {ρ : List Nat} |
| 49 | (body : RawFormula σ (k + m) (k :: ρ)) (A : OrderedStructure σ) |
| 50 | (v : Fin m → Fin A.size) (η : RelationEnv A.size ρ) : |
| 51 | Set (Fin k → Fin A.size) → Set (Fin k → Fin A.size) := |
| 52 | fun R => {a | eval body A (Fin.append a v) (extend R η)} |
| 53 | |
| 54 | axiom positiveBodyMonotone {σ : Vocabulary} {m k : Nat} {ρ : List Nat} |
| 55 | (body : RawFormula σ (k + m) (k :: ρ)) |
| 56 | (hbody : body.Admissible) (hpositive : body.positiveAt 0 true) |
| 57 | (A : OrderedStructure σ) (v : Fin m → Fin A.size) |
| 58 | (η : RelationEnv A.size ρ) : Monotone (bodyOperator body A v η) |
| 59 | |
| 60 | def Satisfies {σ : Vocabulary} {k : Nat} (A : PointedStructure σ k) |
| 61 | (φ : Formula σ k) : Prop := |
| 62 | eval φ.val A.structureValue A.tuple (fun r => Fin.elim0 r) |
| 63 | |
| 64 | def Definable {σ : Vocabulary} {k : Nat} (Q : Query σ k) : Prop := |
| 65 | ∃ φ : Formula σ k, ∀ A, Q A ↔ Satisfies A φ |
| 66 | |
| 67 | end Lax751879.FixedPointSemantics |
| 68 |
From Mathlib
none
Discussion
Ask a question or add context. Endorsements and structured flags are kept in the review panel above.
0 comments