|
| 1 | +{-# OPTIONS --safe --without-K #-} |
| 2 | + |
| 3 | +-- ε-indexed approximate echoes over a (pseudo-)metric codomain. |
| 4 | +-- |
| 5 | +-- Axis-2 first artifact (`docs/echo-types/taxonomy.md` §2): |
| 6 | +-- |
| 7 | +-- EchoR ε f y := Σ A (λ x → dist (f x) y ≤ ε) |
| 8 | +-- |
| 9 | +-- where `dist` is a pseudo-metric on the codomain `B` and `ε` lives |
| 10 | +-- in an ordered tolerance monoid. The exact echo `Echo f y = Σ A (λ x → |
| 11 | +-- f x ≡ y)` lifts into `EchoR zero f y` via reflexivity of `dist`. |
| 12 | +-- |
| 13 | +-- Headline lemmas: |
| 14 | +-- |
| 15 | +-- * echo-approx-intro -- exact match is a zero-tolerance approximate echo |
| 16 | +-- * echo-approx-relax -- ε is monotone: ε₁ ≤ ε₂ ⇒ EchoR ε₁ ⊑ EchoR ε₂ |
| 17 | +-- * echo-approx-compose -- non-expansive composition with additive error, |
| 18 | +-- realising the taxonomy §2 conjecture |
| 19 | +-- |
| 20 | +-- The non-expansiveness side condition on the outer leg is the |
| 21 | +-- minimal hypothesis under which tolerances accumulate additively; |
| 22 | +-- without it the conjecture has no general proof (an amplifying |
| 23 | +-- second leg can blow ε₁ up arbitrarily on the way through). |
| 24 | + |
| 25 | +module EchoApprox where |
| 26 | + |
| 27 | +open import Level using (Level; _⊔_; suc) |
| 28 | +open import Function.Base using (_∘_; id) |
| 29 | +open import Data.Product.Base using (Σ; _,_; proj₁; proj₂) |
| 30 | +open import Relation.Binary.PropositionalEquality using (_≡_; refl; sym; subst) |
| 31 | + |
| 32 | +---------------------------------------------------------------------- |
| 33 | +-- Tolerance carrier and pseudo-metric structure |
| 34 | +---------------------------------------------------------------------- |
| 35 | + |
| 36 | +-- A tolerance carrier is an ordered commutative-monoid-flavoured type |
| 37 | +-- with just enough structure to state additive composition: |
| 38 | +-- transitive `≤`, reflexivity at every point, and a binary `+` that |
| 39 | +-- is monotone on each side. |
| 40 | + |
| 41 | +record Tolerance ℓ : Set (suc ℓ) where |
| 42 | + infix 4 _≤_ |
| 43 | + infixl 6 _+_ |
| 44 | + field |
| 45 | + Tol : Set ℓ |
| 46 | + zero : Tol |
| 47 | + _+_ : Tol → Tol → Tol |
| 48 | + _≤_ : Tol → Tol → Set ℓ |
| 49 | + ≤-refl : ∀ {ε} → ε ≤ ε |
| 50 | + ≤-trans : ∀ {ε₁ ε₂ ε₃} → ε₁ ≤ ε₂ → ε₂ ≤ ε₃ → ε₁ ≤ ε₃ |
| 51 | + +-mono-≤ : ∀ {a b c d} → a ≤ b → c ≤ d → (a + c) ≤ (b + d) |
| 52 | + |
| 53 | +-- A pseudo-metric on `B` valued in a tolerance carrier `T`. Self-distance |
| 54 | +-- is zero (definitionally) and the triangle inequality holds. We do not |
| 55 | +-- demand symmetry or separation here; both can be added later if needed. |
| 56 | + |
| 57 | +record PseudoMetric {b ℓ} (B : Set b) (T : Tolerance ℓ) : Set (b ⊔ ℓ) where |
| 58 | + open Tolerance T |
| 59 | + field |
| 60 | + dist : B → B → Tol |
| 61 | + dist-self : ∀ y → dist y y ≡ zero |
| 62 | + dist-tri : ∀ b₁ b₂ b₃ → dist b₁ b₃ ≤ (dist b₁ b₂ + dist b₂ b₃) |
| 63 | + |
| 64 | +---------------------------------------------------------------------- |
| 65 | +-- Approximate echo |
| 66 | +---------------------------------------------------------------------- |
| 67 | + |
| 68 | +module Approx |
| 69 | + {a b ℓ} {A : Set a} {B : Set b} {T : Tolerance ℓ} |
| 70 | + (M : PseudoMetric B T) |
| 71 | + where |
| 72 | + |
| 73 | + open Tolerance T |
| 74 | + open PseudoMetric M |
| 75 | + |
| 76 | + -- EchoR ε f y: a witness x : A whose image f x lies within ε of y. |
| 77 | + EchoR : Tol → (A → B) → B → Set (a ⊔ ℓ) |
| 78 | + EchoR ε f y = Σ A (λ x → dist (f x) y ≤ ε) |
| 79 | + |
| 80 | + ---------------------------------------------------------------------- |
| 81 | + -- Headline 1: exact match ⇒ zero-tolerance approximate match. |
| 82 | + -- |
| 83 | + -- Lifts the constructor of `Echo` (`x , refl`) into the metric setting |
| 84 | + -- with no tolerance budget consumed. The proof rewrites `dist (f x) |
| 85 | + -- (f x)` to `zero` via `dist-self` and then uses `≤-refl` at zero. |
| 86 | + ---------------------------------------------------------------------- |
| 87 | + |
| 88 | + echo-approx-intro : (f : A → B) (x : A) → EchoR zero f (f x) |
| 89 | + echo-approx-intro f x = |
| 90 | + x , subst (_≤ zero) (sym (dist-self (f x))) ≤-refl |
| 91 | + |
| 92 | + ---------------------------------------------------------------------- |
| 93 | + -- Headline 2: tolerance is monotone in `ε`. A tighter approximation |
| 94 | + -- is also a looser one. The proof is one transitivity step. |
| 95 | + ---------------------------------------------------------------------- |
| 96 | + |
| 97 | + echo-approx-relax : |
| 98 | + ∀ {ε₁ ε₂ : Tol} {f : A → B} {y : B} → |
| 99 | + ε₁ ≤ ε₂ → EchoR ε₁ f y → EchoR ε₂ f y |
| 100 | + echo-approx-relax ε₁≤ε₂ (x , dfx≤ε₁) = x , ≤-trans dfx≤ε₁ ε₁≤ε₂ |
| 101 | + |
| 102 | + ---------------------------------------------------------------------- |
| 103 | + -- Headline 3: additive composition under non-expansiveness. |
| 104 | + -- |
| 105 | + -- Realises the taxonomy §2 conjecture |
| 106 | + -- "ε₁-echo(f) + ε₂-echo(g) ⊑ (ε₁ + ε₂)-echo(g ∘ f)". |
| 107 | + -- |
| 108 | + -- Form: an ε₁-echo of `f` at some intermediate `b`, plus a bound |
| 109 | + -- `dist (g b) y ≤ ε₂`, plus non-expansiveness of `g`, yields an |
| 110 | + -- (ε₁ + ε₂)-echo of `g ∘ f` at `y`. |
| 111 | + -- |
| 112 | + -- Outer leg `g` is endomorphic (`B → B`) so that we stay inside the |
| 113 | + -- single supplied metric. A two-metric version is straightforward |
| 114 | + -- but adds bureaucracy without changing the argument. |
| 115 | + ---------------------------------------------------------------------- |
| 116 | + |
| 117 | + NonExpansive : (B → B) → Set (b ⊔ ℓ) |
| 118 | + NonExpansive g = ∀ b₁ b₂ → dist (g b₁) (g b₂) ≤ dist b₁ b₂ |
| 119 | + |
| 120 | + echo-approx-compose : |
| 121 | + ∀ {ε₁ ε₂ : Tol} |
| 122 | + (f : A → B) (g : B → B) → |
| 123 | + NonExpansive g → |
| 124 | + ∀ {b y : B} → |
| 125 | + EchoR ε₁ f b → |
| 126 | + dist (g b) y ≤ ε₂ → |
| 127 | + EchoR (ε₁ + ε₂) (g ∘ f) y |
| 128 | + echo-approx-compose {ε₁} {ε₂} f g g-nonexp {b} {y} (x , dfx≤ε₁) dgby≤ε₂ = |
| 129 | + x , bound |
| 130 | + where |
| 131 | + -- triangle: dist (g (f x)) y ≤ dist (g (f x)) (g b) + dist (g b) y |
| 132 | + leg : dist (g (f x)) y ≤ (dist (g (f x)) (g b) + dist (g b) y) |
| 133 | + leg = dist-tri (g (f x)) (g b) y |
| 134 | + |
| 135 | + -- non-expansiveness contracts the f-side residue, additive monotonicity |
| 136 | + -- carries it through the triangle bound. |
| 137 | + contract : (dist (g (f x)) (g b) + dist (g b) y) ≤ (ε₁ + ε₂) |
| 138 | + contract = +-mono-≤ (≤-trans (g-nonexp (f x) b) dfx≤ε₁) dgby≤ε₂ |
| 139 | + |
| 140 | + bound : dist (g (f x)) y ≤ (ε₁ + ε₂) |
| 141 | + bound = ≤-trans leg contract |
0 commit comments