Skip to content

Commit 9b3563e

Browse files
hyperpolymathclaude
hyperpolymath
and
claude
committed
docs(formal): L1 closure research — tropical carrier refactor (clean win) + the eliminator fork (choreographic-over-time-segments analysis)
Two planning/research docs grounded in the tropical-resource-typing isomorphism verdict. L1-REGION-REFOUNDATION-PLAN.md: the concrete Coq work-plan to dissolve ADMIT 1 (region_shrink via list->count-map carrier + exit_comm) and repair the FALSE ADMIT 2 (region_liveness, restated graded + provable from count_occ_le_l1_m, with the ~13-site call-site audit). Net 4->2 admits, zero false lemmas. L1-ELIMINATOR-FORK.md: states the remaining challenge precisely (region-liveness is a temporally-extended, non-local dependency the snapshot+result-type ontology cannot express; both prior fixes failed inside that ontology), and assesses choreographic typing across time segments (regions as session-typed resources, scopes as segments, local typing as endpoint projection, preservation as subject reduction for a tropically-graded choreography via TropicalSessionTypes). Verdict: right SHAPE (adds the missing 'time' axis), unifies with the tropical grade, but unproven — can relocate into projection-coherence; specifies the cheap minimal-counterexample experiment that decides close-vs-relocate. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
1 parent 18a2a69 commit 9b3563e

2 files changed

Lines changed: 317 additions & 0 deletions

File tree

‎formal/L1-ELIMINATOR-FORK.md‎

Lines changed: 155 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,155 @@
1+
<!-- SPDX-License-Identifier: MPL-2.0 -->
2+
<!-- Owner: Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk> -->
3+
4+
# The eliminator fork — and whether choreographic typing across time segments closes it
5+
6+
The two admits the tropical re-foundation does **not** dissolve
7+
(`step_pop_disjoint_from_type_l1`, ADMIT 3; `preservation_l1`, ADMIT 4 gated on
8+
it). This note states the challenge precisely, explains why both prior fixes
9+
failed, and assesses the proposal: **type region-liveness choreographically,
10+
across time segments.** Verdict up front: it is the right *shape* — more so than
11+
the grade-in-context patch — but it is unproven and can *relocate* rather than
12+
*close*, so it needs the minimal-counterexample experiment in §5.
13+
14+
## 1. The challenge, precisely
15+
16+
Preservation needs: if `R ; G ⊢ e : T -| R' ; G'` and `(μ,R,e) → (μ',R₂,e')`,
17+
then `R₂ ; G ⊢ e' : T -| … `. It fails on a single shape:
18+
19+
> A **subterm `e_sub` depends on a region `rv`** (its type mentions `rv`, e.g.
20+
> `e_sub : TString rv`), but an **eliminator/context erases `rv` from the
21+
> result type** (`EDrop(·):TUnit`, `Fst`, application, `Let`-body, `Case`-arm),
22+
> and a step **exits `rv`** (`R → R₂`, `rv` gone). Now `e'` still contains
23+
> `e_sub`, which needs `rv` live, but `R₂` no longer has it and `T` never
24+
> showed it.
25+
26+
Minimal Coq-checked witness: `EDrop (EVar j : TString rv)` at `R = [rv]`. It
27+
types; `expr_strictly_free_of_region rv` holds (no syntactic `rv`); the result
28+
type `Unit` satisfies the Tofte–Talpin premise — yet shrinking `rv` leaves the
29+
inner `EVar j` untypable.
30+
31+
**The root is a representational mismatch in *time*.** The judgment expresses
32+
region liveness with:
33+
- a **snapshot** `R` (the live set *at one point*), and
34+
- a **result-type-local** view (`free_regions(T)`),
35+
36+
but the actual obligation is **temporally extended and non-local**: "`rv` must
37+
be live *throughout the evaluation of `e_sub`*". A snapshot cannot say
38+
"throughout"; a result type cannot say "of a subterm whose contribution I
39+
erased". The information needed is *when*, and neither carrier carries time.
40+
41+
## 2. Why both prior fixes failed (the same wall)
42+
43+
- **Leaf-rule strengthening (path 3):** put `free_regions(T) ⊆ R` on `T_Var`.
44+
This forces liveness *at the variable use site*. But region-shrink/exit
45+
*wants to remove* `rv` while that very variable is in scope, so the premise
46+
and `region_shrink` **contradict** — the `EDrop` witness is exactly the
47+
contradiction. It moves the snapshot demand to the leaf; it does not add time.
48+
- **Effect-typed lambdas (A′):** makes a *lambda's* footprint type-visible.
49+
Helps only `S_App_Step2`; the witness is a *free variable under an
50+
eliminator*, no lambda involved. It adds type-visibility for one binder
51+
shape; it does not add time.
52+
53+
Both stay inside the snapshot+result-type ontology. The wall is that ontology.
54+
55+
## 3. The proposal: liveness as a choreography over time segments
56+
57+
Replace "liveness = membership in a snapshot" with "liveness = a position in a
58+
**global protocol over time segments**", and recover the per-subterm rule by
59+
**projection**. Concretely:
60+
61+
- **Time segments.** A region scope `enter rv … exit rv` *is* a segment: the
62+
interval during which `rv` is live. Nesting/re-entry gives nested segments
63+
(depth = the tropical `cnt rv` grade — the two views meet here).
64+
- **Regions as session-typed resources.** Each region is a participant whose
65+
lifecycle is a session `open → use* → close` (exactly a file-handle/typestate
66+
protocol). The whole program is the **choreography**: the interleaving of all
67+
regions' sessions across segments.
68+
- **Local typing = endpoint projection.** A subterm `e_sub` is typed by
69+
*projecting* the choreography onto `e_sub`'s segment. Its dependency on `rv`
70+
is satisfied because the projection places `e_sub` *inside* `rv`'s `open…close`
71+
segment — **not** because `rv` appears in the result type.
72+
- **Preservation = subject reduction for the choreography.** A step advances
73+
the global type to a coherent global type; the snapshot problem dissolves
74+
because the global type carries the *temporal* structure the snapshot lacked.
75+
76+
The eliminator's "hidden" dependency is then **not hidden**: the global type
77+
records that `e_sub` runs in `rv`'s segment, even though the local/erased result
78+
type does not. That is precisely the missing *when*.
79+
80+
## 4. Why this is the right shape — and the estate already has both halves
81+
82+
The dependency is temporal-and-global; choreographies are *the* device for
83+
temporal-global protocols projected to local views. This is a structural match,
84+
not an analogy. And it composes with the tropical re-foundation rather than
85+
competing with it:
86+
87+
- `tropical-resource-typing` already ships **`TropicalSessionTypes.lean`**.
88+
Session types are the *local projections* of a choreography. So region
89+
liveness becomes a **tropical-graded choreography across time segments**: the
90+
grade (MinPlus `cnt`) carries the *resource quantity* (re-entry depth), the
91+
session/choreographic structure carries the *temporal protocol*. One object,
92+
two readings — the same `echo ≡ tropical ≡ epistemic` unification, now
93+
extended to include the *order of events*, not just their magnitude.
94+
- Division of labour becomes clean: **tropical grade** closes the structural
95+
admits (1, 2 — quantity/carrier); **choreography over segments** is aimed at
96+
the eliminator admit (3 — time). `EchoBridge` already measures L3 residues
97+
into the grade; a choreography adds the missing temporal axis to the same
98+
grade.
99+
100+
## 5. The honest risks (why "right shape" ≠ "resolved")
101+
102+
1. **Sequential, not distributed.** Choreographies/session types were built for
103+
*concurrent* systems with communicating participants. The reinterpretation
104+
here — *regions* as participants, *scopes* as segments, region
105+
alloc/use/free as the "communication" — is principled (resource-usage
106+
protocols / typestate are exactly session-shaped) but **non-standard**; it
107+
needs a clean foundation, not an off-the-shelf import.
108+
2. **Projection coherence is where the problem could re-appear.** The whole
109+
method rests on endpoint projection being *coherent* (locals recompose to the
110+
global). The eliminator case might project to a local type that is itself
111+
inconsistent — in which case the difficulty is **relocated** to a coherence
112+
side-condition, not closed. This is the single thing to check first.
113+
3. **Close vs relocate.** Subject reduction for the choreography must genuinely
114+
*carry* "`rv` live throughout `e_sub`'s segment" through the exit step. If it
115+
does, ADMIT 3 closes; if the segment boundary and the exit step don't line up
116+
definitionally, you get a new obligation, not a discharge.
117+
4. **Apparatus cost.** This is a research program (global types, projection,
118+
coherence, subject reduction for the region choreography), not a refactor —
119+
high-reward, high-cost. It should not gate the §`L1-REGION-REFOUNDATION-PLAN`
120+
clean win, which proceeds independently.
121+
122+
## 6. The deciding experiment (cheap, do this before committing)
123+
124+
Do **not** build the general theory first. Formulate the *minimal* choreography
125+
that types just `EDrop (EVar j : TString rv)` over two segments —
126+
`S₁ = [enter rv … (EVar j read) …]`, `S₂ = [exit rv …]` — and ask one question:
127+
128+
> Does the choreography's subject-reduction step for `S_Region_Exit rv`
129+
> transform the global type into a **coherent** global type in which the
130+
> (now-residual) `EVar j` no longer claims `rv`-liveness — *without* a snapshot
131+
> premise?
132+
133+
- **If yes**, the segment carried the *when*, the projection stayed coherent,
134+
and ADMIT 3 closes choreographically → re-grade `region_liveness` *and*
135+
`step_pop` against the global type; the capstone follows. (This is the path
136+
to **0** admits.)
137+
- **If no — i.e. coherence needs an extra side-condition** — the problem has
138+
*relocated* to that condition. Report it; it is likely the *same* eliminator
139+
obligation in choreographic clothing, and the honest count stays **2** until a
140+
different idea (or a restricted language fragment) lands.
141+
142+
Either outcome is decisive and cheap, and tells us whether choreographic typing
143+
*resolves* the eliminator fork or merely *renames* it.
144+
145+
## 7. Verdict
146+
147+
Choreographic typing across time segments is the **best-shaped** candidate for
148+
ADMIT 3 because it is the only proposal that adds the missing axis — *time* —
149+
rather than re-arranging the snapshot. It also unifies cleanly with the tropical
150+
re-foundation via `TropicalSessionTypes` (a tropically-graded choreography:
151+
quantity × order in one structure). It is **not yet a resolution**: it can
152+
relocate the difficulty into projection coherence, and the sequential-language
153+
foundation is non-standard. The §5/§6 experiment is the inexpensive way to
154+
learn which — and it is the recommended next step on the eliminator fork, run in
155+
parallel with (not blocking) the clean-win carrier refactor.

‎formal/L1-REGION-REFOUNDATION-PLAN.md‎

Lines changed: 162 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,162 @@
1+
<!-- SPDX-License-Identifier: MPL-2.0 -->
2+
<!-- Owner: Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk> -->
3+
4+
# L1 region re-foundation — the clean-win Coq work-plan
5+
6+
**Scope.** This plan covers the two admits that the tropical re-foundation
7+
dissolves cleanly: `region_shrink_preserves_typing_l1_gen_m` (ADMIT 1) and the
8+
*false* `region_liveness_at_split_l1_gen` (ADMIT 2). It does **not** cover
9+
`step_pop_disjoint_from_type_l1` (ADMIT 3, the eliminator fork) or the capstone
10+
`preservation_l1` (ADMIT 4, gated on 3) — those are the separate research
11+
problem (see `L1-ELIMINATOR-FORK.md`).
12+
13+
Evidence base: the isomorphism validation against `tropical-resource-typing`
14+
(`docs/applications/ephapax-l1-regions.adoc` in that repo). The carrier
15+
`list region_name` is a `region_name →₀ ℕ` grade vector wearing a list costume;
16+
the admits live where the costume tears.
17+
18+
## Step 0 — the carrier change (single highest-leverage edit)
19+
20+
`Syntax.v:867`:
21+
22+
```coq
23+
(* before *)
24+
Definition region_env := list region_name.
25+
26+
(* after *)
27+
Definition region_env := region_name -> nat. (* cnt r R = re-entry depth of r; 0 = dead *)
28+
```
29+
30+
A total function is preferred over a `FMap`/`list (region_name*nat)` for the
31+
proofs: every region operation becomes a *pointwise `nat` fact*, with no
32+
finiteness obligation and no canonical-form/sortedness bookkeeping. Equality is
33+
`funext` (or work up to pointwise equality with a `region_env_eq` setoid to
34+
avoid axioms — see Step 4 note).
35+
36+
## Step 1 — replace the four operations
37+
38+
| Old (list) | New (count-map) | Definition |
39+
|---|---|---|
40+
| `In r R` | `live R r` | `R r >= 1` |
41+
| `r :: R` (enter) | `enter r R` | `fun r' => if String.eqb r' r then S (R r') else R r'` |
42+
| `remove_first r R` (exit) | `exit r R` | `fun r' => if String.eqb r' r then pred (R r') else R r'` |
43+
| `count_occ _ R r` | `cnt r R` | `R r` |
44+
45+
`remove_first_L1` (the TypingL1 copy) collapses into `exit` — the two are now
46+
literally the same function, removing the list/multiset double-bookkeeping that
47+
PRESERVATION-DESIGN §5.1 flagged.
48+
49+
## Step 2 — the coordinate lemmas (all `nat`-trivial, all become `Qed`)
50+
51+
These replace the list lemmas (`remove_first_comm`, `count_occ_le_l1_m`,
52+
`remove_first_L1_count_eq_self`, `_count_other`). Each is one `unfold` +
53+
`funext` + `destruct (String.eqb …)` + `lia`:
54+
55+
```coq
56+
Lemma exit_comm : forall r1 r2 R, exit r1 (exit r2 R) = exit r2 (exit r1 R).
57+
Lemma cnt_exit_self : forall r R, cnt r (exit r R) = pred (cnt r R).
58+
Lemma cnt_exit_other: forall r r' R, r <> r' -> cnt r' (exit r R) = cnt r' R.
59+
Lemma cnt_enter_self: forall r R, cnt r (enter r R) = S (cnt r R).
60+
Lemma cnt_le_exit : forall r r' R, cnt r' (exit r R) <= cnt r' R. (* monotonicity *)
61+
Lemma live_exit_other: forall r r' R, r <> r' -> live R r' -> live (exit r R) r'.
62+
```
63+
64+
`exit_comm` is the discharge for ADMIT 1's residual sub-cases (:572, :642): the
65+
`rr = r` shadowed `T_Region_Active` case is now `pred (pred (R r))` either way —
66+
order-free by construction. `cnt_le_exit` is grade-monotonicity =
67+
`count_occ_le_l1_m` = the tropical `subsumption_transports` instance.
68+
69+
## Step 3 — re-thread the judgment
70+
71+
In `TypingL1.v` rewrite the region rules' premises/outputs in the new
72+
vocabulary (mechanical):
73+
74+
- `T_Region_L1` / `T_Region_Active_L1`: `In r R` → `live R r`;
75+
output `remove_first_L1 r R_body` → `exit r R_body`;
76+
the Tofte–Talpin premise `~ In r (free_regions T)` is unchanged (it is about
77+
the *type*, not the env).
78+
- `T_Loc_L1` / `T_StringNew_L1`: `In r R` → `live R r`.
79+
- Every step rule in `Semantics_L1.v` / `Semantics.v` touching `r :: R` or
80+
`remove_first r R` → `enter`/`exit`.
81+
82+
This is the bulk of the diff (every `In`/`remove_first`/`count_occ` use across
83+
`TypingL1.v`, `Semantics_L1.v`, `Counterexample_L2*.v`), but it is find-and-
84+
replace plus re-running tactics; the *content* of the proofs is unchanged
85+
except where it was fighting the list (Step 4).
86+
87+
## Step 4 — ADMIT 1 closes
88+
89+
`region_shrink_preserves_typing_l1_gen_m` (:441). The two internal admits
90+
(:572,:642) were the shadowed `T_Region_Active_L1{,_Echo}` `rr = r` case where
91+
list `remove_first` ordering and `remove_first_L1` disagreed. With `exit` and
92+
`exit_comm`, the goal is `pred`-arithmetic on the `rr` coordinate plus
93+
`cnt_exit_other` on the rest. Close with `exit_comm; cnt_exit_*; lia`. **Qed.**
94+
95+
> Axiom note: if `funext` is unwanted in the trusted base, carry a pointwise
96+
> `region_env_eq` and prove the rules respect it (a `Proper` instance). Mild
97+
> extra work; keeps `Print Assumptions` axiom-free. Decide before Step 0.
98+
99+
## Step 5 — ADMIT 2 repaired (the false lemma)
100+
101+
`region_liveness_at_split_l1_gen` (:1904) is **false as written**
102+
(`In rv R -> In rv R'`; witness `ERegion rv (EI32 5)` at `R=[rv]` pops the only
103+
`rv`). Restate as the *graded, conditional* form and prove from monotonicity:
104+
105+
```coq
106+
(* replaces the false lemma *)
107+
Lemma region_liveness_graded_l1 :
108+
forall m R G e T R' G' rv,
109+
R ; G |=L1[m] e : T -| R' ; G' ->
110+
expr_no_exit_of_region rv e -> (* e performs no S_Region_Exit on rv *)
111+
live R rv -> live R' rv.
112+
Proof.
113+
(* cnt rv R' = cnt rv R when e exits rv zero times (from cnt_le_exit + the
114+
exit-count being 0); live = cnt >= 1 is then preserved. *)
115+
Qed.
116+
```
117+
118+
`expr_no_exit_of_region` is the honest side-condition the *false* version
119+
silently dropped. If a usable predicate already exists, reuse
120+
`expr_strictly_free_of_region` (the region-shrink hypothesis is the same shape).
121+
122+
### Step 5a — call-site audit (the real work in ADMIT 2)
123+
124+
The old `region_liveness_at_split_l1_gen` axiom is consumed at ~13 sites in
125+
`subst_typing_gen_l1*` (Semantics_L1.v ~:2140–:2291). Each must be re-checked:
126+
127+
1. **Served cleanly**: the site already steps a sub-expression provably free of
128+
`rv`-exits (it usually carries `expr_strictly_free_of_region rv …`). Thread
129+
`expr_no_exit_of_region` and apply `region_liveness_graded_l1`. Expect the
130+
majority here.
131+
2. **Needs the threaded side-condition**: add `expr_no_exit_of_region rv` to
132+
the *caller's* hypotheses and discharge it from that caller's context.
133+
3. **Genuinely unconditional**: any site that *needed* `In rv R -> In rv R'`
134+
with no no-exit guarantee was relying on a false statement — flag it; it is
135+
really an ADMIT-3 instance (the eliminator fork) in disguise, not closable
136+
here.
137+
138+
Produce a table (site :: class :: discharge) before editing; classes (1)/(2)
139+
close ADMIT 2, class (3) sites get moved to the eliminator-fork backlog.
140+
141+
## Step 6 — verify
142+
143+
- `make -f build.mk clean && make -f build.mk` exits 0.
144+
- `region_shrink_preserves_typing_l1_gen_m` and `region_liveness_graded_l1` end
145+
in `Qed`; the old false lemma is deleted (not `Admitted`).
146+
- `Print Assumptions` for both: no `region_*` self-axioms among them; ideally no
147+
new axioms (modulo the `funext`/setoid decision in Step 4).
148+
- `Counterexample.v`, `Counterexample_L2*.v` still compile (strengthening only
149+
shrinks the typable set; untypability witnesses are preserved).
150+
- Net live-admit count: **4 → 2** (`step_pop` + the gated `preservation_l1`
151+
remain), and **zero false lemmas** (the soundness smell is gone).
152+
153+
## What this buys / does not buy
154+
155+
- **Buys**: ADMIT 1 + ADMIT 2 closed; the false lemma replaced by a true one;
156+
`remove_first_L1`/`remove_first` double-bookkeeping eliminated; the carrier is
157+
now the proven tropical/ℕ-multiset grade (re-foundation done, L1≡L3 wiring via
158+
EchoBridge now possible as an additive follow-on).
159+
- **Does not buy**: closure of `step_pop` (ADMIT 3) or `preservation_l1`
160+
(ADMIT 4). Those are the eliminator fork — a value/eliminator depending on a
161+
region absent from its *result type* — and the naïve `T_Var` premise that
162+
would close them is **proven false**. See `L1-ELIMINATOR-FORK.md`.

0 commit comments

Comments
 (0)