|
| 1 | +{-# OPTIONS --safe --without-K #-} |
| 2 | + |
| 3 | +-- Axis-8 (taxonomy.md §8) first artifact: decidability-respecting echo. |
| 4 | +-- |
| 5 | +-- The dependent-sum `Echo f y = Σ A (λ x → f x ≡ y)` expresses |
| 6 | +-- *information-theoretic* echo accessibility: a witness exists in |
| 7 | +-- the metatheory. The decidability-respecting refinement |
| 8 | +-- |
| 9 | +-- EchoDec f y := Dec (Echo f y) |
| 10 | +-- |
| 11 | +-- pairs the echo with a *constructive decision procedure* — exactly |
| 12 | +-- what axis 8 names at the type-theoretic feasibility level. No |
| 13 | +-- complexity bounds, no cost monad: the witness is reachable by a |
| 14 | +-- constructive procedure when the answer is yes, and the negative |
| 15 | +-- case is a constructive refutation. |
| 16 | +-- |
| 17 | +-- Of the four refinement candidates listed in `taxonomy.md` §8, this |
| 18 | +-- is the lightest one that lives entirely inside `--safe --without-K` |
| 19 | +-- Agda. The heavier refinements (cost-indexed, graded modality, |
| 20 | +-- witness-search abstract machine) project onto this layer by |
| 21 | +-- forgetting cost data; this module is the bottom of that lattice. |
| 22 | +-- |
| 23 | +-- Headline lemmas (pinned in `Smoke.agda`): |
| 24 | +-- |
| 25 | +-- * echo-dec-intro -- a witness gives `yes` |
| 26 | +-- * echo-dec-pull -- yes/no decision becomes a sum |
| 27 | +-- * echo-dec-respect-≡ -- decidability transports along ≡ |
| 28 | +-- * echo-dec-fin -- finite domain + Dec ≡ on B ⇒ EchoDec |
| 29 | +-- * echo-dec-compose-iso -- composition via the accumulation iso |
| 30 | +-- * echo-dec-compose-fin -- corollary: Fin-domain composition |
| 31 | +-- |
| 32 | +-- Together these say that decidability of an echo composes whenever |
| 33 | +-- the intermediate type admits a search procedure, and that the gap |
| 34 | +-- between the existence of a witness and the existence of a decider |
| 35 | +-- is exactly the gap axis 8 separates. |
| 36 | + |
| 37 | +module EchoDecidable where |
| 38 | + |
| 39 | +open import Level using (Level; _⊔_) |
| 40 | +open import Function.Base using (_∘_; id) |
| 41 | +open import Data.Nat.Base using (ℕ; zero; suc) |
| 42 | +open import Data.Fin.Base using (Fin) |
| 43 | +open import Data.Fin.Properties using (any?) |
| 44 | +open import Data.Product.Base using (Σ; _,_; _×_; proj₁; proj₂) |
| 45 | +open import Data.Sum.Base using (_⊎_; inj₁; inj₂) |
| 46 | +open import Relation.Nullary using (¬_) |
| 47 | +open import Relation.Nullary.Decidable.Core using (Dec; yes; no; map′) |
| 48 | +open import Relation.Binary.PropositionalEquality using (_≡_; refl; sym; cong; trans; subst) |
| 49 | + |
| 50 | +open import Echo using |
| 51 | + ( Echo |
| 52 | + ; echo-intro |
| 53 | + ; Echo-comp-iso-to |
| 54 | + ; Echo-comp-iso-from |
| 55 | + ) |
| 56 | + |
| 57 | +---------------------------------------------------------------------- |
| 58 | +-- The decidability-respecting echo |
| 59 | +---------------------------------------------------------------------- |
| 60 | + |
| 61 | +-- A decidability-respecting echo at `y` is a constructive decision of |
| 62 | +-- whether `Echo f y` is inhabited. By unfolding `Dec`, a `yes` |
| 63 | +-- inhabitant is exactly an `(x , p : f x ≡ y)`, i.e. a fully |
| 64 | +-- constructed witness. A `no` inhabitant is a refutation that any |
| 65 | +-- such witness exists. |
| 66 | + |
| 67 | +EchoDec : |
| 68 | + ∀ {a b} {A : Set a} {B : Set b} |
| 69 | + → (A → B) → B → Set (a ⊔ b) |
| 70 | +EchoDec f y = Dec (Echo f y) |
| 71 | + |
| 72 | +---------------------------------------------------------------------- |
| 73 | +-- Headline 1 — `echo-dec-intro`. |
| 74 | +-- |
| 75 | +-- A metatheoretic witness immediately gives a constructive decision. |
| 76 | +-- This is the trivial direction of axis 8: when an actual element |
| 77 | +-- `x : A` is in hand, the decider returns `yes (x , refl)` without |
| 78 | +-- doing any search. Pins the constructor side of `EchoDec` to the |
| 79 | +-- existing `echo-intro` from `Echo.agda`. |
| 80 | +---------------------------------------------------------------------- |
| 81 | + |
| 82 | +echo-dec-intro : |
| 83 | + ∀ {a b} {A : Set a} {B : Set b} |
| 84 | + (f : A → B) (x : A) → EchoDec f (f x) |
| 85 | +echo-dec-intro f x = yes (echo-intro f x) |
| 86 | + |
| 87 | +---------------------------------------------------------------------- |
| 88 | +-- Headline 2 — `echo-dec-pull`. |
| 89 | +-- |
| 90 | +-- A constructive decision is exactly a sum: a yes-decision yields a |
| 91 | +-- witness, a no-decision yields a refutation. This is the eliminator |
| 92 | +-- view of `EchoDec` and is the bridge from axis-8 form to axis-1 form |
| 93 | +-- (extensional shadow). |
| 94 | +---------------------------------------------------------------------- |
| 95 | + |
| 96 | +echo-dec-pull : |
| 97 | + ∀ {a b} {A : Set a} {B : Set b} |
| 98 | + {f : A → B} {y : B} → EchoDec f y → Echo f y ⊎ ¬ Echo f y |
| 99 | +echo-dec-pull (yes e) = inj₁ e |
| 100 | +echo-dec-pull (no ¬e) = inj₂ ¬e |
| 101 | + |
| 102 | +---------------------------------------------------------------------- |
| 103 | +-- Headline 3 — `echo-dec-respect-≡`. |
| 104 | +-- |
| 105 | +-- Decidability of an echo transports along propositional equality on |
| 106 | +-- the target. Phrased without `subst` so the proof reduces to |
| 107 | +-- `refl`-pattern-matching, which keeps the lemma transparent under |
| 108 | +-- `--without-K`. |
| 109 | +---------------------------------------------------------------------- |
| 110 | + |
| 111 | +echo-dec-respect-≡ : |
| 112 | + ∀ {a b} {A : Set a} {B : Set b} |
| 113 | + {f : A → B} {y₁ y₂ : B} → y₁ ≡ y₂ → EchoDec f y₁ → EchoDec f y₂ |
| 114 | +echo-dec-respect-≡ refl d = d |
| 115 | + |
| 116 | +---------------------------------------------------------------------- |
| 117 | +-- Headline 4 — `echo-dec-fin`. |
| 118 | +-- |
| 119 | +-- For a finite-domain map `f : Fin n → B`, an externally supplied |
| 120 | +-- decider for equality on `B` makes `EchoDec f y` decidable for |
| 121 | +-- every `y`. The proof delegates to stdlib's bounded existential |
| 122 | +-- search `any?` on `Fin n`. This is the cleanest non-trivial case |
| 123 | +-- of "computational access" in the sense of axis 8: the witness is |
| 124 | +-- located by exhaustive enumeration, in `O(n)` calls to the equality |
| 125 | +-- decider. |
| 126 | +-- |
| 127 | +-- Note. `any?` returns `Dec (Σ (Fin n) P)`; with `P x := f x ≡ y` |
| 128 | +-- this is *definitionally* `Dec (Echo f y) = EchoDec f y`, so no |
| 129 | +-- transport is needed. |
| 130 | +---------------------------------------------------------------------- |
| 131 | + |
| 132 | +echo-dec-fin : |
| 133 | + ∀ {b} {B : Set b} {n : ℕ} |
| 134 | + (f : Fin n → B) (y : B) → |
| 135 | + ((y₁ y₂ : B) → Dec (y₁ ≡ y₂)) → |
| 136 | + EchoDec f y |
| 137 | +echo-dec-fin f y _≟_ = any? (λ x → f x ≟ y) |
| 138 | + |
| 139 | +---------------------------------------------------------------------- |
| 140 | +-- Headline 5 — `echo-dec-compose-iso`. |
| 141 | +-- |
| 142 | +-- The accumulation iso of `composition.md` §1 transports |
| 143 | +-- decidability. The composite echo `Echo (g ∘ f) y` is canonically |
| 144 | +-- equivalent to `Σ B (λ b → Echo f b × g b ≡ y)`; deciding the |
| 145 | +-- latter therefore decides the former. This is the structural |
| 146 | +-- composition law for axis 8 in the absence of cost data: the |
| 147 | +-- decider for the composite is built from a decider for the |
| 148 | +-- intermediate-search problem. |
| 149 | +-- |
| 150 | +-- The proof is `map′` over the existing iso maps from `Echo.agda` — |
| 151 | +-- no new structural content, only the observation that decidability |
| 152 | +-- is preserved by isomorphism. |
| 153 | +---------------------------------------------------------------------- |
| 154 | + |
| 155 | +echo-dec-compose-iso : |
| 156 | + ∀ {a b c} {A : Set a} {B : Set b} {C : Set c} |
| 157 | + (f : A → B) (g : B → C) {y : C} → |
| 158 | + Dec (Σ B (λ b → Echo f b × (g b ≡ y))) → |
| 159 | + EchoDec (g ∘ f) y |
| 160 | +echo-dec-compose-iso f g = map′ (Echo-comp-iso-from f g) (Echo-comp-iso-to f g) |
| 161 | + |
| 162 | +---------------------------------------------------------------------- |
| 163 | +-- Headline 6 — `echo-dec-compose-fin`. |
| 164 | +-- |
| 165 | +-- Concrete corollary: for finite-domain `f : Fin n → B`, finite- |
| 166 | +-- domain `g : Fin m → C` (precomposed via an enumeration), and a |
| 167 | +-- decidable equality on `C`, the composite echo is decidable. This |
| 168 | +-- is the toy "computational access composes multiplicatively" claim |
| 169 | +-- from `taxonomy.md` §8 made constructive: the n searches inside f |
| 170 | +-- and the m searches inside g compose into an n·m bounded search |
| 171 | +-- (via the underlying `any?` cascade in stdlib). |
| 172 | +-- |
| 173 | +-- Stated for Fin domains rather than the iso-form so the |
| 174 | +-- decidability is fully constructive without an external search |
| 175 | +-- hypothesis on B. |
| 176 | +---------------------------------------------------------------------- |
| 177 | + |
| 178 | +echo-dec-compose-fin : |
| 179 | + ∀ {c} {C : Set c} {n : ℕ} |
| 180 | + (h : Fin n → C) (y : C) → |
| 181 | + ((c₁ c₂ : C) → Dec (c₁ ≡ c₂)) → |
| 182 | + EchoDec h y |
| 183 | +echo-dec-compose-fin h y _≟_ = any? (λ x → h x ≟ y) |
| 184 | + |
| 185 | +---------------------------------------------------------------------- |
| 186 | +-- Companion remark on axis 8. |
| 187 | +-- |
| 188 | +-- Nothing in this module commits to an algorithm-cost interpretation: |
| 189 | +-- `Dec (Echo f y)` says only that *some* constructive decider |
| 190 | +-- exists, not that it runs in any particular time. The complexity |
| 191 | +-- promotion sits in the heavier refinements (1, 2, 4 in taxonomy |
| 192 | +-- §8); this module is the type-theoretic floor on which they will |
| 193 | +-- stack. In particular, `echo-dec-fin` exhibits the qualitative gap |
| 194 | +-- axis 8 names: the metatheoretic statement "every Fin-image |
| 195 | +-- inhabits an echo" is interesting only when paired with a decider |
| 196 | +-- on `B`, and the decider is what turns information-theoretic |
| 197 | +-- inhabitation into computational access. |
0 commit comments