|
| 1 | +<!-- SPDX-License-Identifier: PMPL-1.0-or-later --> |
| 2 | +<!-- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk> --> |
| 3 | + |
| 4 | +# JTV v2 Reversibility: Canonical Design |
| 5 | + |
| 6 | +Date: 2026-04-12 |
| 7 | + |
| 8 | +## Status |
| 9 | + |
| 10 | +Accepted — canonical model for JTV v2 (Gamma). See also the designed fork |
| 11 | +with 007's Phase 1 implementation documented at the end of this file. |
| 12 | + |
| 13 | +--- |
| 14 | + |
| 15 | +## The Philosophical Commitment |
| 16 | + |
| 17 | +JTV v2's central claim is: **subtraction is not a primitive.** It is the |
| 18 | +inverse of addition, accessed via reversal. This is not a convenience — it |
| 19 | +is the foundational identity of the Gamma stage of JTV's evolution. |
| 20 | + |
| 21 | +`x - v` in JTV v2 does not exist as a grammar production. Instead: |
| 22 | + |
| 23 | +``` |
| 24 | +reverse { x += v } |
| 25 | +``` |
| 26 | + |
| 27 | +This is not approximate. It is not "semantically equivalent in the simple |
| 28 | +case." It IS subtraction, because subtraction IS the reversal of addition. |
| 29 | +The arithmetic identity is preserved at the operation level, not recovered |
| 30 | +by a snapshot. |
| 31 | + |
| 32 | +This commitment places JTV v2 in the tradition of Janus (Lutz & Derby 1982, |
| 33 | +Yokoyama & Glück 2007) — per-operation reversal, step-by-step invertibility, |
| 34 | +genuine connection to Landauer's principle and Bennett's theorem on reversible |
| 35 | +computation. |
| 36 | + |
| 37 | +--- |
| 38 | + |
| 39 | +## The Three Constructs |
| 40 | + |
| 41 | +### `reversible { }` |
| 42 | + |
| 43 | +Marks a block whose operations are reversible. Maintains a reversal log: |
| 44 | + |
| 45 | +``` |
| 46 | +R = [(op₁, inv(op₁)), (op₂, inv(op₂)), ...] |
| 47 | +``` |
| 48 | + |
| 49 | +Each operation inside records its inverse at execution time. The inverses |
| 50 | +are: |
| 51 | + |
| 52 | +| Operation | Inverse | |
| 53 | +|-----------|---------| |
| 54 | +| `x += v` | `x -= v` (i.e. `reverse { x += v }`) | |
| 55 | +| `append(xs, v)` | `remove_last(xs)` | |
| 56 | +| `send_local(h, v)` | handle reverts via snapshot of pre-send state | |
| 57 | + |
| 58 | +### `reverse { }` |
| 59 | + |
| 60 | +Applies the reversal log in reverse order. This is step-by-step inversion — |
| 61 | +not snapshot restore. The log is walked backwards, each inverse applied in |
| 62 | +sequence. The programmer observes intermediate states being undone. |
| 63 | + |
| 64 | +### `irreversible { }` |
| 65 | + |
| 66 | +Explicitly marks operations with no defined inverse: I/O, cross-agent sends, |
| 67 | +external API calls. Attempting to `reverse` an `irreversible` block is a |
| 68 | +static error. |
| 69 | + |
| 70 | +--- |
| 71 | + |
| 72 | +## The Linear Token (Shared with 007) |
| 73 | + |
| 74 | +Both JTV v2 and 007 use the linear `ReversalToken` mechanism for pairing. |
| 75 | +Entering `reversible { }` produces a linear value `tok` of type |
| 76 | +`ReversalToken<S>`. The token must be consumed by `reverse tok` or |
| 77 | +`abandon tok` (explicit commit). Linearity guarantees exactly one |
| 78 | +`reverse`/`abandon` per token — no double-reversal, no lost log. |
| 79 | + |
| 80 | +``` |
| 81 | +reversible { |
| 82 | + x += amount |
| 83 | + append(log, entry) |
| 84 | +} -> tok -- tok : ReversalToken<{ x: Int, log: List<Entry> }> |
| 85 | +
|
| 86 | +reverse tok -- replays: remove_last(log), then x -= amount |
| 87 | +-- OR |
| 88 | +abandon tok -- commits: discards log, operations stand |
| 89 | +``` |
| 90 | + |
| 91 | +In JTV v2, the token's type parameter `S` records the *types* of captured |
| 92 | +variables whose inverses are logged — not their pre-operation values (that |
| 93 | +is the snapshot approach; JTV v2 carries the operation log instead). |
| 94 | + |
| 95 | +### Structural sugar |
| 96 | + |
| 97 | +``` |
| 98 | +reversible { ... } reverse { ... } |
| 99 | +-- desugars to: reversible { ... } -> _tok ; reverse _tok |
| 100 | +``` |
| 101 | + |
| 102 | +--- |
| 103 | + |
| 104 | +## Branch Interaction |
| 105 | + |
| 106 | +At `branch` join points, path-sensitive typing applies: |
| 107 | + |
| 108 | +- Token on **all** arms → `ReversalToken<S>` (must consume) |
| 109 | +- Token on **some** arms → `Option<ReversalToken<S>>` (auto-promoted; `match` forces handling) |
| 110 | +- Token on **no** arms → nothing in scope |
| 111 | + |
| 112 | +The `Option<ReversalToken<S>>` type at asymmetric joins IS the signal. |
| 113 | +`match` forces exhaustive `Some`/`None` handling. No separate lint needed. |
| 114 | + |
| 115 | +--- |
| 116 | + |
| 117 | +## The ExternalHandle Boundary |
| 118 | + |
| 119 | +`send` inside a `reversible` block targeting an `ExternalHandle` (crossing |
| 120 | +an agent boundary) is a **static error** unless inside `irreversible { }`. |
| 121 | + |
| 122 | +This enforces that JTV v2's reversibility is **local reversibility**. True |
| 123 | +distributed reversibility (saga patterns, two-phase commit) is implemented |
| 124 | +at the agent protocol level, not via `reverse`. This is correct: distributed |
| 125 | +reversibility is a distributed systems problem. |
| 126 | + |
| 127 | +--- |
| 128 | + |
| 129 | +## What JTV v2 Does NOT Do |
| 130 | + |
| 131 | +JTV v2 does **not** use whole-block snapshot restore as its reversal |
| 132 | +mechanism. This is the key distinction from 007's Phase 1 implementation. |
| 133 | + |
| 134 | +- **Snapshot restore** (007 Phase 1): captures pre-block `@state` values, |
| 135 | + restores them on `reverse`. Semantically correct at block granularity. |
| 136 | + Not per-operation. Not at the Landauer limit. |
| 137 | + |
| 138 | +- **Operation log + replay** (JTV v2): records `(op, inv(op))` pairs as |
| 139 | + operations execute, replays inverses in reverse order on `reverse`. |
| 140 | + Per-operation. Philosophically aligned with the subtraction-as-inverse claim. |
| 141 | + Closer to the Landauer limit (each operation's energy cost can in principle |
| 142 | + be recouped). |
| 143 | + |
| 144 | +--- |
| 145 | + |
| 146 | +## The Designed Fork with 007 |
| 147 | + |
| 148 | +This divergence from 007's Phase 1 is **deliberate and documented** as a |
| 149 | +designed experiment. See: |
| 150 | + |
| 151 | +- `007/docs/session-2026-04-12-jtv-v2-reversibility-design.adoc` — 007's |
| 152 | + five closed design decisions and Phase 1/Phase 2 distinction |
| 153 | +- `nextgen-languages/docs/design/jtv-007-reversibility-fork.adoc` — the |
| 154 | + portfolio-level experiment design |
| 155 | + |
| 156 | +### Shared foundations (both approaches) |
| 157 | + |
| 158 | +- Linear `ReversalToken` as pairing mechanism |
| 159 | +- `Option<ReversalToken>` at branch joins (path-sensitive typing) |
| 160 | +- `ExternalHandle` static error for agent boundary sends |
| 161 | +- `irreversible { }` escape hatch |
| 162 | +- `reversible { } reverse { }` structural sugar |
| 163 | + |
| 164 | +### What differs |
| 165 | + |
| 166 | +| | JTV v2 | 007 Phase 1 | 007 Phase 2 | |
| 167 | +|--|--------|-------------|-------------| |
| 168 | +| Token carries | Operation log | `@state` field values (snapshot) | Operation log (ref T) | |
| 169 | +| `reverse tok` does | Replay inverse ops in order | Restore snapshot | Replay inverse ops | |
| 170 | +| Subtraction model | `reverse { x += v }` = true inverse | State restore predating `+=` | `reverse ref_x += v` = true inverse | |
| 171 | +| Landauer proximity | Close | Distant (snapshot has memory cost) | Close | |
| 172 | + |
| 173 | +### Convergence point |
| 174 | + |
| 175 | +007 Phase 2 (`ref T` + fine-grained log) converges toward JTV v2's |
| 176 | +per-operation model. At that point the experiment concludes: |
| 177 | + |
| 178 | +- If snapshot proves sufficient for 95% of agent programming use cases, |
| 179 | + JTV v2 may consider a two-tier model (snapshot for simple cases, log for |
| 180 | + complex ones). |
| 181 | +- If per-operation inversion proves essential in 007 Phase 2, the Phase 1 |
| 182 | + snapshot approach is confirmed as a stepping stone only. |
| 183 | + |
| 184 | +Neither outcome compromises the other. The shared token foundation ensures |
| 185 | +findings transfer immediately in either direction. |
0 commit comments