|
| 1 | +{-# OPTIONS --safe --without-K #-} |
| 2 | + |
| 3 | +-- EchoSearch — Axis 8 witness-search abstract machine (thin slice). |
| 4 | +-- |
| 5 | +-- Axis 8 of `docs/echo-types/taxonomy.md` distinguishes |
| 6 | +-- information-theoretic inhabitation of `Echo f y` from a |
| 7 | +-- *computational* witness extracted by an algorithm. Refinement (4) |
| 8 | +-- in that section names the heaviest reading: |
| 9 | +-- |
| 10 | +-- "Witness-search abstract machine. Model the extractor as a |
| 11 | +-- term in a bounded-step abstract machine and pair it with |
| 12 | +-- the echo." |
| 13 | +-- |
| 14 | +-- A faithful "abstract machine" with steps, configurations, and a |
| 15 | +-- semantics would be a sizeable separate development; the *honest* |
| 16 | +-- thin slice of that idea is the enumerator-bounded witness: |
| 17 | +-- |
| 18 | +-- a search strategy = an enumerator `enum : ℕ → A` |
| 19 | +-- a bound-`n` echo = a witness `enum k ≡ x` with `k < n` |
| 20 | +-- together with the usual `f x ≡ y` |
| 21 | +-- |
| 22 | +-- The `ℕ`-bound is the "step budget" of the would-be machine. Every |
| 23 | +-- machine of the heavier refinement (e.g. a Turing-bounded extractor, |
| 24 | +-- a polynomial-time enumeration) projects onto this thin slice by |
| 25 | +-- forgetting everything except the index it queried and the bound it |
| 26 | +-- queried under. So this module sits at the *bottom* of the |
| 27 | +-- axis-8(4) lattice in the same sense that `EchoDecidable` sits at |
| 28 | +-- the bottom of the axis-8(3) lattice (`docs/echo-types/taxonomy.md` |
| 29 | +-- §"Open question / lattice"), and a heavier machine model lands on |
| 30 | +-- top later without renaming or invalidating these lemmas. |
| 31 | +-- |
| 32 | +-- Design choices, in line with `EchoApprox` / `EchoFiberCount`: |
| 33 | +-- |
| 34 | +-- * `SearchStrategy A := ℕ → A`. A total function. Partiality is |
| 35 | +-- not modelled here — that is a separate refinement (axis 8(2)). |
| 36 | +-- A total enumerator is exactly the right shape for a |
| 37 | +-- bound-respecting machine: at step `k` it produces the element |
| 38 | +-- `enum k`; nothing else. |
| 39 | +-- |
| 40 | +-- * `EchoS enum f y n := Σ ℕ λ k → (k < n) × (f (enum k) ≡ y)`. |
| 41 | +-- Crucially `_<_` is stdlib's `Data.Nat.Base._<_`, i.e. |
| 42 | +-- `suc m ≤ n` — the strict form. This is the form `≤-<-trans` / |
| 43 | +-- `<-≤-trans` from `Data.Nat.Properties` operate on without any |
| 44 | +-- conversion glue. |
| 45 | +-- |
| 46 | +-- * Composition: we ship `echo-search-postcompose`, the |
| 47 | +-- "post-compose with `g`" rule. This is the search analogue of |
| 48 | +-- "f x ≡ y ⇒ (g ∘ f) x ≡ g y" — it preserves the bound exactly |
| 49 | +-- (the same k, the same enumerator step, the same `< n` proof). |
| 50 | +-- This is the genuinely-honest compositional content available |
| 51 | +-- without further machinery; a product/sequential composition |
| 52 | +-- under two strategies needs more (a `ℕ × ℕ` index, a paired |
| 53 | +-- bound, and a choice of pairing function on the index set), |
| 54 | +-- which is a separate slice. See "where next" below. |
| 55 | +-- |
| 56 | +-- Where next: |
| 57 | +-- |
| 58 | +-- * Sequential composition `EchoS enum f b n₁ → EchoS enum' g y n₂ |
| 59 | +-- → EchoS (paired-enum) (g ∘ f) y (n₁ * n₂)` under a pairing |
| 60 | +-- enumerator on `ℕ × ℕ`. Honest but needs a bijection |
| 61 | +-- `ℕ × ℕ ↔ ℕ`; defer to the slice that wants it. |
| 62 | +-- |
| 63 | +-- * A real abstract-machine refinement: configurations + a step |
| 64 | +-- relation, with `EchoS` recovered as `∃ trace . trace.length < n |
| 65 | +-- ∧ trace.last ≡ x ∧ f x ≡ y`. The current `EchoS` projects from |
| 66 | +-- that by collapsing the trace to its terminal index. |
| 67 | +-- |
| 68 | +-- * A *bounded-search-is-decidable* lemma in the presence of |
| 69 | +-- decidable equality on `B`: search up to `n` either yields an |
| 70 | +-- `EchoS enum f y n` or proves `¬ EchoS enum f y n`. This is the |
| 71 | +-- concrete bridge to `EchoDecidable`, kept as a separate slice |
| 72 | +-- because it needs a `_≟_` on `B` and a finite-walk recursion. |
| 73 | + |
| 74 | +module EchoSearch where |
| 75 | + |
| 76 | +open import Function.Base using (_∘_; id) |
| 77 | +open import Data.Nat.Base using (ℕ; zero; suc; _≤_; _<_; z≤n; s≤s) |
| 78 | +open import Data.Nat.Properties using (≤-<-trans; <-≤-trans) |
| 79 | +open import Data.Empty using (⊥; ⊥-elim) |
| 80 | +open import Data.Product.Base using (Σ; _,_; _×_; proj₁; proj₂) |
| 81 | +open import Relation.Nullary using (¬_) |
| 82 | +open import Relation.Binary.PropositionalEquality |
| 83 | + using (_≡_; refl; sym; trans; cong) |
| 84 | + |
| 85 | +open import Echo using (Echo) |
| 86 | + |
| 87 | +---------------------------------------------------------------------- |
| 88 | +-- Search strategies and bound-indexed echoes |
| 89 | +---------------------------------------------------------------------- |
| 90 | + |
| 91 | +-- A search strategy on `A` is a total enumeration of its elements |
| 92 | +-- indexed by ℕ. Total, by design — partiality is a separate axis 8(2) |
| 93 | +-- refinement and would obscure the bound semantics here. |
| 94 | +SearchStrategy : ∀ {a} → Set a → Set a |
| 95 | +SearchStrategy A = ℕ → A |
| 96 | + |
| 97 | +-- The witness-search echo at bound `n`: a step index `k < n` at |
| 98 | +-- which the enumerator produced a preimage of `y` under `f`. |
| 99 | +EchoS : |
| 100 | + ∀ {a b} {A : Set a} {B : Set b} |
| 101 | + (enum : SearchStrategy A) (f : A → B) (y : B) (n : ℕ) → Set b |
| 102 | +EchoS enum f y n = Σ ℕ (λ k → (k < n) × (f (enum k) ≡ y)) |
| 103 | + |
| 104 | +---------------------------------------------------------------------- |
| 105 | +-- Headlines |
| 106 | +---------------------------------------------------------------------- |
| 107 | + |
| 108 | +-- Introduction. If at step `k < n` the enumerator returns an element |
| 109 | +-- whose image is `y`, we have a bound-`n` search echo. |
| 110 | +echo-search-intro : |
| 111 | + ∀ {a b} {A : Set a} {B : Set b} |
| 112 | + (enum : SearchStrategy A) (f : A → B) {y : B} |
| 113 | + (k : ℕ) (n : ℕ) (k<n : k < n) → |
| 114 | + f (enum k) ≡ y → |
| 115 | + EchoS enum f y n |
| 116 | +echo-search-intro enum f k n k<n eq = k , k<n , eq |
| 117 | + |
| 118 | +-- Bound monotonicity. A larger budget admits every shorter-budget |
| 119 | +-- search; the same step index, lifted along `<-≤-trans`. |
| 120 | +echo-search-relax : |
| 121 | + ∀ {a b} {A : Set a} {B : Set b} |
| 122 | + (enum : SearchStrategy A) (f : A → B) {y : B} {n m : ℕ} |
| 123 | + (n≤m : n ≤ m) → |
| 124 | + EchoS enum f y n → EchoS enum f y m |
| 125 | +echo-search-relax enum f n≤m (k , k<n , eq) = |
| 126 | + k , <-≤-trans k<n n≤m , eq |
| 127 | + |
| 128 | +-- Forgetful projection. Throw away the step budget and the index |
| 129 | +-- bound and keep only the underlying intensional `Echo`. This is the |
| 130 | +-- canonical "search refines inhabitation" arrow. |
| 131 | +echo-search-forget : |
| 132 | + ∀ {a b} {A : Set a} {B : Set b} |
| 133 | + {enum : SearchStrategy A} {f : A → B} {y : B} {n : ℕ} → |
| 134 | + EchoS enum f y n → Echo f y |
| 135 | +echo-search-forget (k , _ , eq) = _ , eq |
| 136 | + |
| 137 | +-- Empty-budget vacuity. No witness can live at bound 0, because |
| 138 | +-- `k < 0` is uninhabited in stdlib's `Data.Nat._<_`. |
| 139 | +echo-search-bound-zero : |
| 140 | + ∀ {a b} {A : Set a} {B : Set b} |
| 141 | + (enum : SearchStrategy A) (f : A → B) (y : B) → |
| 142 | + ¬ EchoS enum f y 0 |
| 143 | +echo-search-bound-zero enum f y (k , () , eq) |
| 144 | + |
| 145 | +-- Post-composition. The honest compositional rule available without |
| 146 | +-- a product-strategy / pairing-bijection on the index set: a |
| 147 | +-- bound-`n` search witnessing `f` at `y` also witnesses `g ∘ f` at |
| 148 | +-- `g y`, at the *same* step index and the *same* bound. The bound |
| 149 | +-- is preserved exactly because the enumerator and the queried step |
| 150 | +-- have not changed — only what we report as the "answer" has. |
| 151 | +echo-search-postcompose : |
| 152 | + ∀ {a b c} {A : Set a} {B : Set b} {C : Set c} |
| 153 | + (enum : SearchStrategy A) (f : A → B) (g : B → C) {y : B} {n : ℕ} → |
| 154 | + EchoS enum f y n → EchoS enum (g ∘ f) (g y) n |
| 155 | +echo-search-postcompose enum f g (k , k<n , eq) = |
| 156 | + k , k<n , cong g eq |
0 commit comments