Certified synthesis of least-fixed-point formulas

A positive defining formula for a relation transformer gives a defining formula for its least fixed point. The body certificate is uniform over both structures and candidate relations. The polarity certificate is syntactic, so synthesis cannot hide negative recursion behind a semantic monotonicity hypothesis. fo_definable composes the registered body rules and this LFP rule.

Main results

• definable_lfp: synthesize a fixed-point application to arbitrary first-order terms.
• definable_lfp_vars, definable_lfp_unary: forms suited to predicates on free variables.

theorem Cslib.Logic.FO.LFP.definable_lfp {L : FirstOrder.Language} {ι : Type t} {M : ι → Type z} [(i : ι) → L.Structure (M i)] {Γ : List ℕ} {ρ : (i : ι) → Operator.RelEnv Γ (M i)} {α : Type w} {k : ℕ} (F : (i : ι) → (α → M i) → Set (Fin k → M i) →o Set (Fin k → M i)) (args : Fin k → L.Term α) (hF : Operator.PolarityDefinable policy (fun {k_1 : ℕ} => headMark) true (fun (j : (i : ι) × Set (Fin k → M i)) => M j.fst) (fun (x : (i : ι) × Set (Fin k → M i)) => interpretation) (fun (j : (i : ι) × Set (Fin k → M i)) {k_1 : ℕ} => Operator.RelEnv.cons j.snd fun {k_2 : ℕ} => ρ j.fst) fun (j : (i : ι) × Set (Fin k → M i)) (v : α ⊕ Fin k → M j.fst) => v ∘ Sum.inr ∈ (F j.fst (v ∘ Sum.inl)) j.snd) : Operator.Definable policy M (fun (x : ι) => interpretation) ρ fun (i : ι) (v : α → M i) => (fun (j : Fin k) => FirstOrder.Language.Term.realize v (args j)) ∈ OrderHom.lfp (F i v)

A positive body certificate synthesizes an LFP formula defining a given family of monotone operators. The single body witness works for every structure and every candidate relation.

theorem Cslib.Logic.FO.LFP.definable_lfp_vars {L : FirstOrder.Language} {ι : Type t} {M : ι → Type z} [(i : ι) → L.Structure (M i)] {Γ : List ℕ} {ρ : (i : ι) → Operator.RelEnv Γ (M i)} {α : Type w} {k : ℕ} (F : (i : ι) → (α → M i) → Set (Fin k → M i) →o Set (Fin k → M i)) (args : Fin k → α) (hF : Operator.PolarityDefinable policy (fun {k_1 : ℕ} => headMark) true (fun (j : (i : ι) × Set (Fin k → M i)) => M j.fst) (fun (x : (i : ι) × Set (Fin k → M i)) => interpretation) (fun (j : (i : ι) × Set (Fin k → M i)) {k_1 : ℕ} => Operator.RelEnv.cons j.snd fun {k_2 : ℕ} => ρ j.fst) fun (j : (i : ι) × Set (Fin k → M i)) (v : α ⊕ Fin k → M j.fst) => v ∘ Sum.inr ∈ (F j.fst (v ∘ Sum.inl)) j.snd) : Operator.Definable policy M (fun (x : ι) => interpretation) ρ fun (i : ι) (v : α → M i) => v ∘ args ∈ OrderHom.lfp (F i v)

Free-variable tuples provide a directly matching synthesis rule for LFP membership.

theorem Cslib.Logic.FO.LFP.definable_lfp_unary {L : FirstOrder.Language} {ι : Type t} {M : ι → Type z} [(i : ι) → L.Structure (M i)] {Γ : List ℕ} {ρ : (i : ι) → Operator.RelEnv Γ (M i)} {α : Type w} (F : (i : ι) → (α → M i) → Set (Fin 1 → M i) →o Set (Fin 1 → M i)) (a : α) (hF : Operator.PolarityDefinable policy (fun {k : ℕ} => headMark) true (fun (j : (i : ι) × Set (Fin 1 → M i)) => M j.fst) (fun (x : (i : ι) × Set (Fin 1 → M i)) => interpretation) (fun (j : (i : ι) × Set (Fin 1 → M i)) {k : ℕ} => Operator.RelEnv.cons j.snd fun {k : ℕ} => ρ j.fst) fun (j : (i : ι) × Set (Fin 1 → M i)) (v : α ⊕ Fin 1 → M j.fst) => v ∘ Sum.inr ∈ (F j.fst (v ∘ Sum.inl)) j.snd) : Operator.Definable policy M (fun (x : ι) => interpretation) ρ fun (i : ι) (v : α → M i) => ![v a] ∈ OrderHom.lfp (F i v)

Unary fixed-point predicates written with vector notation are synthesized directly.