Search Procedures — The Core DSL

This file defines SearchProc, the central abstraction of the DSL. A SearchProc captures the pattern:

"Enumerate candidates from a countable domain; test each one; halt when a witness is found."

This is the universal pattern for semi-decision procedures: to check w ∈ L, we enumerate a domain of "proofs/witnesses" and test each one. For grammars, the witnesses are derivation sequences; for other problems they might be computation traces, certificates, etc.

Architecture

  ┌─────────────┐     ┌──────────────┐     ┌──────────┐
  │  Enum α     │────▶│  test : α →  │────▶│  halt if │
  │  (generator)│     │  List T →    │     │  true    │
  │             │     │  Bool        │     │          │
  └─────────────┘     └──────────────┘     └──────────┘

The SearchProc bundles:

1. An Enum α (the generator / candidate enumerator)
2. A test : α → List T → Bool (the decidable test)

It recognizes the language { w | ∃ a ∈ enum.range, test a w = true }.

Composability

Search procedures compose via the Enum combinators:

• To search over pairs, use Enum.product
• To search over lists, use Enum.finLists
• To search with additional structure, use Enum.bind

The test function can be built from decidable predicates using standard Boolean combinators.

Compilation to TM0

The search-to-machine compilation lives in SearchProcToTM0.lean. if the enumeration and test are "TM-computable" (formalized via a computability predicate), then the search procedure compiles to a TM0 machine satisfying is_TM.

Main definitions

• SearchProc — a search procedure
• SearchProc.accepts — whether the procedure accepts a given word
• SearchProc.language — the language recognized
• SearchProc.mk' — convenient constructor from Enum + test
• Composition lemmas

structure SearchProc (T : Type u_1) : Type (max u_1 (u_2 + 1))

A search procedure over alphabet T with witness type α.

A search procedure recognizes a language by systematically enumerating witnesses from a countable domain and testing each one against the input word. It accepts w if and only if some witness passes the test.

This is the core abstraction of the DSL. Every semi-decision procedure for a language can be expressed as a SearchProc (by Rice's theorem, the converse also holds for r.e. languages).

• WitTy : Type u_2

  The type of witnesses / certificates

• enum : Enum self.WitTy

  Enumeration of all candidate witnesses

• test : self.WitTy → List T → Bool

  The test: given a witness and an input word, does the witness certify membership?

def SearchProc.accepts {T : Type u_1} (sp : SearchProc T) (w : List T) : Prop

A search procedure accepts word w if some enumerated witness passes the test.

Equations

• sp.accepts w = ∃ a ∈ sp.enum.range, sp.test a w = true

def SearchProc.language {T : Type u_1} (sp : SearchProc T) : Language T

The language recognized by a search procedure: the set of all accepted words.

Equations

• sp.language = {w : List T | sp.accepts w}

theorem SearchProc.accepts_iff {T : Type u_1} (sp : SearchProc T) (w : List T) : sp.accepts w ↔ ∃ (n : ℕ) (a : sp.WitTy), sp.enum n = some a ∧ sp.test a w = true

A search procedure accepts w iff there exists n : ℕ such that the n-th enumerated witness passes the test.

def SearchProc.step {T : Type u_1} (sp : SearchProc T) (w : List T) (n : ℕ) : Bool

Equivalent "step-based" view: the procedure accepts w iff sp.step w n = true for some n, where step is the composed enumerate-and-test function.

Equations

• sp.step w n = match sp.enum n with | some a => sp.test a w | none => false

theorem SearchProc.accepts_iff_step {T : Type u_1} (sp : SearchProc T) (w : List T) : sp.accepts w ↔ ∃ (n : ℕ), sp.step w n = true

Constructors

def SearchProc.ofEncodable {T : Type u_1} {α : Type u_2} [Encodable α] (test : α → List T → Bool) : SearchProc T

Build a search procedure from an Encodable witness type and a test. Automatically uses the Encodable instance to enumerate all witnesses.

Equations

• SearchProc.ofEncodable test = { WitTy := α, enum := Enum.ofEncodable, test := test }

theorem SearchProc.ofEncodable_language {T : Type u_1} {α : Type u_2} [Encodable α] (test : α → List T → Bool) : (ofEncodable test).language = {w : List T | ∃ (a : α), test a w = true}

def SearchProc.searchNat {T : Type u_1} (test : ℕ → List T → Bool) : SearchProc T

Build a search procedure that searches over all natural numbers.

Equations

• SearchProc.searchNat test = { WitTy := ℕ, enum := Enum.naturals, test := test }

theorem SearchProc.searchNat_language {T : Type u_1} (test : ℕ → List T → Bool) : (searchNat test).language = {w : List T | ∃ (n : ℕ), test n w = true}

Composition

def SearchProc.refine {T : Type u_1} (sp : SearchProc T) (p : sp.WitTy → List T → Bool) : SearchProc T

Refine a search procedure with a stronger test.

Equations

• sp.refine p = { WitTy := sp.WitTy, enum := sp.enum, test := fun (a : sp.WitTy) (w : List T) => sp.test a w && p a w }

theorem SearchProc.refine_language {T : Type u_1} (sp : SearchProc T) (p : sp.WitTy → List T → Bool) (w : List T) : w ∈ (sp.refine p).language → w ∈ sp.language

def SearchProc.mapWitness {T : Type u_1} {β : Type u_2} (sp : SearchProc T) (f : β → sp.WitTy) (enum_β : Enum β) : SearchProc T

Transform the witness type of a search procedure.

Equations

• sp.mapWitness f enum_β = { WitTy := β, enum := enum_β, test := fun (b : β) (w : List T) => sp.test (f b) w }

def SearchProc.existsPair {T : Type u_1} {α : Type u_2} {β : Type u_3} (enumA : Enum α) (enumB : Enum β) (test : α → β → List T → Bool) : SearchProc T

Existential search: search for a pair (a, b) where a comes from one enumeration and b from another.

Equations

• SearchProc.existsPair enumA enumB test = { WitTy := α × β, enum := enumA.product enumB, test := fun (p : α × β) (w : List T) => test p.1 p.2 w }

theorem SearchProc.existsPair_language {T : Type u_1} {α : Type u_2} {β : Type u_3} (enumA : Enum α) (enumB : Enum β) (test : α → β → List T → Bool) : (existsPair enumA enumB test).language = {w : List T | ∃ a ∈ enumA.range, ∃ b ∈ enumB.range, test a b w = true}