|
| 1 | += D-2026-05-20 — Presentation-dependence sub-theory (cluster + meta-pattern) |
| 2 | +:toc: macro |
| 3 | +:toclevels: 2 |
| 4 | +:sectnums: |
| 5 | +:sectnumlevels: 2 |
| 6 | +:icons: font |
| 7 | + |
| 8 | +[.lead] |
| 9 | +Closure note for the `roadmap.md` entry |
| 10 | +"Presentation-dependence sub-theory: examples 5, 9, 10 cluster here; |
| 11 | +write up the common pattern". The verdict is *meta-pattern only — |
| 12 | +no new Agda module needed*: presentation-dependence is the existing |
| 13 | +Axis 4 of `taxonomy.md`, and the three examples instantiate it by |
| 14 | +the same mechanism (intermediate-data residue carried *inside* the |
| 15 | +echo's witness component). The cluster is real but does not refine |
| 16 | +the axis; it sharpens what the axis names. |
| 17 | + |
| 18 | +toc::[] |
| 19 | + |
| 20 | +== The cluster |
| 21 | + |
| 22 | +Three examples in `docs/echo-types/examples.md` are flagged as |
| 23 | +sharing presentation-dependence (cross-cutting observation #2): |
| 24 | + |
| 25 | +* *Example 5 — Database `GROUP BY`* (`examples.md` L88–106). Source |
| 26 | + map `group_by_key : List Row → Map Key Row-Summary`. The echo is |
| 27 | + "the set of input row lists that would produce summary `s` under |
| 28 | + the aggregation"; under K-provenance the echo specialises to a |
| 29 | + semiring element. The summary `s` alone does not pin a unique |
| 30 | + contributing-row multiset — the *presentation* of which rows |
| 31 | + contributed is residue, and that residue depends on the chosen |
| 32 | + provenance semiring (Bag, Why, How, …), not on `group_by_key` |
| 33 | + alone. |
| 34 | +* *Example 9 — Parser error recovery* (`examples.md` L165–183). |
| 35 | + Source map `parse : List Token → Maybe SyntaxTree`. A more |
| 36 | + faithful echo "carries the recovery trace as part of the tree |
| 37 | + itself, making the echo split into a canonical-tree part and an |
| 38 | + error-annotation part". The recovery trace is residue *of the |
| 39 | + parse algorithm chosen*, not of the input/output pair. Examples.md |
| 40 | + explicitly cites this as the example that forces Axis 4. |
| 41 | +* *Example 10 — Abstract interpretation (widening)* (`examples.md` |
| 42 | + L187–202). Source map `α : Values → AbstractValues` (Galois |
| 43 | + connection, e.g. `Int → Sign`). The echo records the concrete |
| 44 | + preimage class; the widening step introduces approximate echoes |
| 45 | + whose tolerance grows with analysis depth, and the analyser's |
| 46 | + *trace information* — what widening choices were made — is part |
| 47 | + of the residue. |
| 48 | + |
| 49 | +All three are flagged *informal* (no Agda anchor), and all three |
| 50 | +have analyser/representation choices that are not determined by the |
| 51 | +abstract source map alone. |
| 52 | + |
| 53 | +== The common pattern |
| 54 | + |
| 55 | +In each example the echo carries information that is *not a function |
| 56 | +of `(f, y)` viewed up to isomorphism* — it depends on the chosen |
| 57 | +implementation, encoding, or analyser. Concretely, the common shape |
| 58 | +is: |
| 59 | + |
| 60 | +[loweralpha] |
| 61 | +. There is an *intermediate datum* `r` (provenance annotation, |
| 62 | + recovery trace, widening trace) that the implementing pipeline |
| 63 | + produces alongside the nominal output. |
| 64 | +. The faithful echo factors as |
| 65 | + `Echo f y ≃ Σ R (λ r → CanonicalEcho f y r)` |
| 66 | + where `R` is the space of implementation choices and |
| 67 | + `CanonicalEcho` is invariant under reparametrisation of `R`. |
| 68 | +. The shadow `image(f)` is presentation-invariant, but the |
| 69 | + intensional core is not: re-presenting `f` along an iso `A ≃ A'` |
| 70 | + or `B ≃ B'` *does* transport canonically (per Axis 4's first |
| 71 | + bullet), but re-implementing `f` via a different choice of `R` |
| 72 | + does *not* — the echo type changes. |
| 73 | + |
| 74 | +The discriminating test for membership in the cluster is therefore: |
| 75 | +"is there a choice the implementer makes that survives in the echo, |
| 76 | +and does that choice live outside the `(A, f, B, y)` data?" For |
| 77 | +examples 5, 9, 10 the answer is yes (semiring, recovery policy, |
| 78 | +widening operator respectively). For examples 1–4 the answer is no |
| 79 | +(the echo is determined up to canonical iso by `(f, y)`). |
| 80 | + |
| 81 | +This is exactly Axis 4's *presentation-dependent* side, with the |
| 82 | +added observation that the cluster's three members all factor |
| 83 | +their presentation-dependence as Σ over an extra parameter `R` |
| 84 | +rather than baking it into the source map's type. |
| 85 | + |
| 86 | +== Where it lives in the axis system |
| 87 | + |
| 88 | +Presentation-dependence is already a numbered axis (Axis 4 of |
| 89 | +`taxonomy.md` L87–107). The cluster does *not* motivate a new |
| 90 | +axis. What it does sharpen is the axis's relation to the others: |
| 91 | + |
| 92 | +* *Axis 1 (extensional/intensional).* The cluster lives entirely on |
| 93 | + the intensional side — every member has `Shadow(f) = image(f)` |
| 94 | + insensitive to presentation, with all presentation-dependence in |
| 95 | + the intensional core. This matches `EchoIndexed`, `EchoChoreo`, |
| 96 | + and `EchoEpistemic` in the cross-classification table |
| 97 | + (`taxonomy.md` L310–321), all of which the table already marks |
| 98 | + `Pres-dep` along axis 4. |
| 99 | +* *Axis 2 (exact/approximate).* Example 10 (widening) crosses both |
| 100 | + axes. Its presentation-dependence (which widening operator) |
| 101 | + parameterises its tolerance evolution — i.e. the choice of |
| 102 | + presentation *is* the choice of approximate-echo schedule. This |
| 103 | + is the only cluster member where axes 2 and 4 entangle; for |
| 104 | + examples 5 and 9 the presentation choice is orthogonal to any |
| 105 | + tolerance. |
| 106 | +* *Axis 5 (compositional/non-compositional).* The cluster predicts |
| 107 | + that presentation-dependent echoes are compositional *only* when |
| 108 | + the presentation parameter `R` itself composes. For |
| 109 | + K-provenance (example 5) it does (semiring multiplication); for |
| 110 | + parser-recovery and widening it is policy-dependent. This is the |
| 111 | + concrete content behind `taxonomy.md`'s Axis 5 "open question" |
| 112 | + about non-compositional echo classes. |
| 113 | +* *Axis 8 (info-theoretic/computational access).* Disjoint from |
| 114 | + the cluster: presentation-dependence is about *which witness |
| 115 | + shape* the echo carries, not about *whether a witness is |
| 116 | + findable*. Example 8 (hash) is not in this cluster precisely |
| 117 | + because the algorithmic choice is hidden from the type. |
| 118 | + |
| 119 | +The cluster therefore projects cleanly onto Axis 4 and reveals |
| 120 | +that the three "Pres-dep" entries in the cross-classification |
| 121 | +table (`EchoIndexed`, `EchoChoreo`, `EchoEpistemic`) are the |
| 122 | +landed-Agda instances of the same meta-pattern that examples 5, |
| 123 | +9, 10 articulate informally. |
| 124 | + |
| 125 | +== What it predicts / what it rules out |
| 126 | + |
| 127 | +[loweralpha] |
| 128 | +. *Presentation-independence is not a theorem to be proved for |
| 129 | + every echo.* Any would-be theorem stated "`Echo f y` is |
| 130 | + isomorphism-invariant under re-presentation of `f`" must |
| 131 | + restrict to canonical (Axis 4 LHS) echoes; the cluster is the |
| 132 | + explicit counterexample family. |
| 133 | +. *The would-be "canonical-form operator" for echoes |
| 134 | + (Axis 4 §"Open question") splits into two sub-questions:* |
| 135 | + (i) for a presentation-dependent echo with parameter `R`, when |
| 136 | + does the quotient `Echo f y / R` reduce to a canonical echo? |
| 137 | + (ii) when does the cluster's Σ-over-`R` factoring exist as a |
| 138 | + type-level decomposition rather than a meta-observation? |
| 139 | + Example 5 with K-provenance is the case where (i) has a clean |
| 140 | + answer (quotient = the semiring's collapse); examples 9 and 10 |
| 141 | + do not yet. |
| 142 | +. *Per-decoration composition lemmas already cover the landed |
| 143 | + Pres-dep cases.* `EchoChoreo.applyChoreo-{comp,compose,via-join}` |
| 144 | + along `_⊑c_` and `EchoEpistemic.knowledge-monotone-{comp,id}` |
| 145 | + (roadmap.md L128–136) are exactly compose-laws against a |
| 146 | + decoration order that *is* the presentation parameter `R`. The |
| 147 | + cluster's "compositional iff R composes" prediction is therefore |
| 148 | + already discharged on the Agda side for the role and epistemic |
| 149 | + decorations. |
| 150 | +. *Prior puzzle dissolved.* The taxonomy table's |
| 151 | + `EchoIndexed`/`EchoChoreo`/`EchoEpistemic` "Pres-dep by role / |
| 152 | + agent" entries are not three independent oddities; they are |
| 153 | + three instances of the same Σ-over-`R` factoring, and they |
| 154 | + compose by the recipe already used in their `*-compose` lemmas. |
| 155 | + |
| 156 | +== Recommended next moves |
| 157 | + |
| 158 | +*Verdict: no new formalisation needed.* The cluster is a meta- |
| 159 | +pattern that is already implicit in (a) Axis 4 as it stands and |
| 160 | +(b) the landed `EchoIndexed`/`EchoChoreo`/`EchoEpistemic` decoration |
| 161 | +modules. The three informal examples (5, 9, 10) are best left as |
| 162 | +informal entries in `examples.md` until a downstream consumer wants |
| 163 | +one of them in Agda; at that point the existing decoration recipe |
| 164 | +(propositional order → join → factoring-free compose → via-join) |
| 165 | +applies directly, with `R` instantiated to the semiring / recovery |
| 166 | +policy / widening lattice. |
| 167 | + |
| 168 | +Concretely: |
| 169 | + |
| 170 | +* *Do not* introduce an `EchoPresentation.agda` module. There is no |
| 171 | + obligation to discharge that is not already discharged by |
| 172 | + `EchoIndexed` (general indexed echoes) and the per-decoration |
| 173 | + composition sweep. |
| 174 | +* *Do* leave Axis 4's "Open question" (canonical-form operator) |
| 175 | + open. The cluster sharpens what that question asks — split into |
| 176 | + (i) and (ii) above — but does not answer it. Example 5 (K- |
| 177 | + provenance quotient) is the natural first test case if and when |
| 178 | + it gets formalised. |
| 179 | +* *Optionally* annotate `examples.md` §"Cross-cutting |
| 180 | + observations" #2 with a back-pointer to this decision document |
| 181 | + so future readers see the cluster has been adjudicated and the |
| 182 | + meta-pattern named. |
| 183 | + |
| 184 | +== Status |
| 185 | + |
| 186 | +[cols="1,3", options="header"] |
| 187 | +|=== |
| 188 | +| Field | Value |
| 189 | +| Verdict | *meta-pattern only* — cluster real, sub-theory unneeded |
| 190 | +| Implication | Axis 4 stands; `EchoIndexed`/`EchoChoreo`/`EchoEpistemic` |
| 191 | + recognised as landed instances of the same Σ-over-presentation |
| 192 | + pattern that examples 5, 9, 10 exhibit informally |
| 193 | +| Open | Axis 4 canonical-form operator (now split into two |
| 194 | + sub-questions); no obligation on the Pres-dep cluster itself |
| 195 | +|=== |
| 196 | + |
| 197 | +== Cross-references |
| 198 | + |
| 199 | +* `docs/echo-types/roadmap.md` — Theory-work entry updated to |
| 200 | + `[landed — see decisions/presentation-dependence.adoc]`. |
| 201 | +* `docs/echo-types/taxonomy.md` §Axis 4 — the existing axis this |
| 202 | + cluster instantiates; its "Open question" is sharpened (not |
| 203 | + closed) by this note. |
| 204 | +* `docs/echo-types/taxonomy.md` §Cross-classification table — the |
| 205 | + three `Pres-dep` entries (`EchoIndexed`, `EchoChoreo`, |
| 206 | + `EchoEpistemic`) are the landed-Agda half of the same pattern. |
| 207 | +* `docs/echo-types/examples.md` §5, §9, §10 — the informal |
| 208 | + cluster members; §"Cross-cutting observations" #2 names the |
| 209 | + cluster. |
| 210 | +* `proofs/agda/EchoChoreo.agda`, |
| 211 | + `proofs/agda/EchoEpistemic.agda`, |
| 212 | + `proofs/agda/EchoIndexed.agda` — landed decoration modules |
| 213 | + whose per-decoration composition lemmas already discharge the |
| 214 | + cluster's "compositional iff `R` composes" prediction for the |
| 215 | + role and epistemic cases. |
0 commit comments