KRF Definitions_Machinery (arXiv 2412.11855 framework layer)

/-
Machinery layer of the KRF formalization: the computability substrate and the
KRF-level definitions (Definitions 5--12 of the paper plus K(M), cl(.) and the
contract of Procedure 1 / the canonical KRF Θ).

Per FORMALIZATION_PLAN §2.8, "effectively checkable" notions are carried at
the code level: a fixed `QA` packaging and a `Coding` (an injection of
QA-pairs into ℕ); recursiveness / r.e.-ness use Mathlib's `Nat.Partrec`. The
concrete Turing-machine construction of M* (Procedure 1, Alg 1) is abstracted
behind `StarContract`: an implementable engine constructor plus its theory
codes — its defining semantic claim is Lemma `star_kb` (landing in
Theorems/, where the Θ-KRF itself is assembled).
-/
import Definitions.Def_KRF_Data
import Mathlib.Computability.Partrec

noncomputable section

open KRFCore
open KRFCore.FStruct

namespace KRF

variable {σD σQ : Sig}

/-! ### Codes and the QA packaging -/

/-- One question-answering task: a (pre-)database together with a query. -/
structure QA (σD σQ : Sig) where
  D : PreDatabase σD
  φ : Fm σQ

/-- A coding injects QA tasks into ℕ. Existence is all the framework needs;
effectiveness obligations are placed on the individual claims (plan §2.8). -/
structure Coding (σD σQ : Sig) where
  enc : QA σD σQ ↪ Nat

/-- A QA-engine is a semantical predicate over QA tasks — the role of the
paper's Turing machines ("M accepts ⟦D,φ⟧"). -/
structure QAEngine (σD σQ : Sig) where
  Sem : QA σD σQ → Prop

/-- 𝕂(M) := { (D,φ) : M accepts ⟦D,φ⟧ } — the paper's K(M), read as a
predicate (plan §2.7). -/
def KM (M : QAEngine σD σQ) : PreDatabase σD → Fm σQ → Prop :=
  fun D φ => M.Sem ⟨D, φ⟩

/-- cl(K): the minimum superclass of K admitting KB-properties 1–5,
constructed as in the paper's appendix (its "sequence S" is exactly this
inductive closure). Constructors keep queries in Q. -/
inductive Closure (Q : QueryLanguage σQ) (K : PreDatabase σD → Fm σQ → Prop) :
    PreDatabase σD → Fm σQ → Prop
  | base {D φ} : K D φ → Closure Q K D φ
  | taut {D φ} : Q.q φ → FStruct.Taut φ → Closure Q K D φ
  | imp {D φ ψ} : Closure Q K D ψ → Q.q φ → FStruct.Entails ψ φ → Closure Q K D φ
  | conj {D φ ψ} : Closure Q K D φ → Closure Q K D ψ → Closure Q K D (Fm.conj φ ψ)
  | ext {D φ D₀} : Closure Q K D₀ φ → Extends D D₀ → Closure Q K D φ
  | ren {D φ} {τ : Nat → Nat} (hinj : Function.Injective τ) :
      Closure Q K D (φ.rename τ) → Closure Q K (renameDB τ hinj D) φ

/-- The contract of Procedure 1 (Alg 1) and the canonical KRF Θ: `star` is
the implementable (-)* constructor, `isTheory` picks exactly the codes of
starred engines (a recursive set — Lemma 1 of the appendix argument). The
concrete Θ-KRF is assembled from these data in Theorems/. -/
structure StarContract (σD σQ : Sig) (Q : QueryLanguage σQ) where
  star : QAEngine σD σQ → QAEngine σD σQ
  isTheory : Nat → Prop
  decTheory : DecidablePred isTheory
  theoryEngine : {π : Nat} → isTheory π → QAEngine σD σQ

/-! ### qKRFs and KRFs (Definition 5) -/

/-- A quasi-KRF over (𝒟,𝒬): an effective (here decidable-regularized, plan
§2.8) theory domain and a KB per theory (Definition 5, properties 1–2). -/
structure QKrf (σD σQ : Sig) (Q : QueryLanguage σQ) where
  dom : Nat → Prop
  dec : DecidablePred dom
  Γ : (π : Nat) → dom π → PreDatabase σD → Fm σQ → Prop

/-- Property 3 of Definition 5: r.e. checkability of the QA problem against a
coding of the pairs. -/
def Checkable {Q : QueryLanguage σQ} (Γ : QKrf σD σQ Q) (c : Coding σD σQ) : Prop :=
  ∀ (π : Nat) (h : Γ.dom π), ∃ f : Nat →. Nat, Nat.Partrec f ∧
    ∀ a : QA σD σQ, (f (c.enc a)).Dom ↔ Γ.Γ π h a.D a.φ

/-- A KRF (Definition 5, properties 1–3). -/
structure Krf (σD σQ : Sig) (Q : QueryLanguage σQ) where
  code : Coding σD σQ
  dom : Nat → Prop
  dec : DecidablePred dom
  Γ : (π : Nat) → dom π → PreDatabase σD → Fm σQ → Prop
  checkable : Checkable (⟨dom, dec, Γ⟩ : QKrf σD σQ Q) code

/-! ### Expressive completeness, reducibility, universality (Def 6–8) -/

/-- Expressively complete: the range of Γ consists of all r.e. KBs — here:
every KB accepted by some engine is equivalent to Γ at some theory
(Definition 6; 𝒟-slicing read as predicates, plan §2.7). -/
def ExpressiveComplete {Q : QueryLanguage σQ} (Γ : Krf σD σQ Q) : Prop :=
  ∀ (M : QAEngine σD σQ),
    ∃ (π : Nat) (h : Γ.dom π), ∀ D φ, KM M D φ ↔ Γ.Γ π h D φ

/-- A recursive reduction p : dom(Γ) → dom(Γ₀) with Γ = Γ₀ ∘ p (Definition 7). -/
structure Reduction {Q : QueryLanguage σQ} (Γ Γ₀ : Krf σD σQ Q) where
  p : Nat → Nat
  p_rec : Computable p
  maps_in : ∀ {π : Nat} (h : Γ.dom π), Γ₀.dom (p π)
  hdef : ∀ (π : Nat) (h : Γ.dom π) (D : PreDatabase σD) (φ : Fm σQ),
      Γ.Γ π h D φ ↔ Γ₀.Γ (p π) (maps_in h) D φ

/-- Γ is reducible to Γ₀ (Definition 7). -/
def ReducibleTo {Q : QueryLanguage σQ} (Γ Γ₀ : Krf σD σQ Q) : Prop := Nonempty (Reduction Γ Γ₀)

/-- Universality (Definition 8): every KRF is reducible to Γ. -/
def Universal {Q : QueryLanguage σQ} (Γ : Krf σD σQ Q) : Prop := ∀ Γ₀ : Krf σD σQ Q, ReducibleTo Γ₀ Γ

/-- A recursive isomorphism (Definition 10): a recursive bijection p of the
theory domains with Γ = Γ₀ ∘ p. -/
structure RecIsomorphism {Q : QueryLanguage σQ} (Γ Γ₀ : Krf σD σQ Q) where
  p : Nat ≃ Nat
  rec_fwd : Computable (fun n => p n)
  rec_bwd : Computable (fun n => p.symm n)
  dom_map : ∀ π, Γ.dom π ↔ Γ₀.dom (p π)
  hdef : ∀ (π : Nat) (h : Γ.dom π) (D : PreDatabase σD) (φ : Fm σQ),
      Γ.Γ π h D φ ↔ Γ₀.Γ (p π) ((dom_map π).mp h) D φ

/-- Γ and Γ₀ are recursively isomorphic (Definition 10). -/
def RecursivelyIsomorphic {Q : QueryLanguage σQ} (Γ Γ₀ : Krf σD σQ Q) : Prop :=
  Nonempty (RecIsomorphism Γ Γ₀)

/-- Padding property (Definition 11): from each theory one can effectively
produce infinitely many theories with the same KB. -/
def PaddingProperty {Q : QueryLanguage σQ} (Γ : Krf σD σQ Q) : Prop :=
  ∀ (π : Nat) (h : Γ.dom π),
    ∃ S : Set Nat, Set.Infinite S ∧ S ⊆ { ω | Γ.dom ω } ∧
      ∀ (ω : Nat) (hω : Γ.dom ω), ω ∈ S → ∀ D φ, Γ.Γ π h D φ ↔ Γ.Γ ω hω D φ

/-- Equally strong (Definition 12). -/
def EquallyStrong {Q : QueryLanguage σQ} (Γ Γ₀ : Krf σD σQ Q) : Prop :=
  ReducibleTo Γ Γ₀ ∧ ReducibleTo Γ₀ Γ

end KRF