From fe348e3179a1ad6b68eec8568d1843d236d1c81e Mon Sep 17 00:00:00 2001 From: rohan Date: Sat, 28 Mar 2026 21:10:30 +0530 Subject: [PATCH 1/4] docs: add Zargham feedback on constraint promotion to summary --- docs/research/semantic-web-summary.md | 17 +++++++++++++++++ 1 file changed, 17 insertions(+) diff --git a/docs/research/semantic-web-summary.md b/docs/research/semantic-web-summary.md index aba3559..5494fef 100644 --- a/docs/research/semantic-web-summary.md +++ b/docs/research/semantic-web-summary.md @@ -131,6 +131,23 @@ graph, R1) and `U_behav` (constraint predicate, R3) for ontological engineering. Same for `StateMetric` and `TransitionSignature`. The canonical decomposition `h = f . g` IS faithful to the paper. +## Open Question: Promoting Common Constraints to R2 + +Zargham's feedback: *"We can probably classify them as two different +kinds of predicates -- those associated with the model structure +(owl/shacl/sparql) and those associated with the runtime."* + +Currently all `TypeDef.constraint` callables are treated as R3 (lossy). +But many common constraints ARE expressible in SHACL: + +- `lambda x: x >= 0` --> `sh:minInclusive 0` +- `lambda x: 0 <= x <= 1` --> `sh:minInclusive 0` + `sh:maxInclusive 1` +- `lambda x: x in {-1, 0, 1}` --> `sh:in (-1 0 1)` + +A constraint classifier could promote these from R3 to R2, making them +round-trippable through Turtle. The general case (arbitrary callable) +remains R3. See #152 for the design proposal. + ## Files - `packages/gds-owl/` -- the full export/import/SHACL/SPARQL implementation From 486a8d3c30e36f1ce365b723229cd102d4827a27 Mon Sep 17 00:00:00 2001 From: rohan Date: Sat, 28 Mar 2026 21:21:48 +0530 Subject: [PATCH 2/4] docs: fix staleness across research docs and CLAUDE.md MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Findings from parallel audit agents: - paper-implementation-gap.md: added Step 5b (backward reachability) - verification-plan.md: Phase 4 updated (gds-analysis exists, not future); artifact path .tex → .md; Steps 1-5 marked complete - research-boundaries.md: continuous-time DSL and state-space matrices marked as Done (gds-continuous, gds-symbolic) - gds-analysis CLAUDE.md: added gds-continuous optional dependency, backward_reachability.py to module table, reachability.py API updated - Root CLAUDE.md: gds-analysis dependency graph includes gds-continuous[opt] --- CLAUDE.md | 2 +- docs/research/paper-implementation-gap.md | 1 + docs/research/research-boundaries.md | 4 ++-- docs/research/verification-plan.md | 11 +++++++---- packages/gds-analysis/CLAUDE.md | 8 +++++--- 5 files changed, 16 insertions(+), 10 deletions(-) diff --git a/CLAUDE.md b/CLAUDE.md index 7eb0dc7..51397ea 100644 --- a/CLAUDE.md +++ b/CLAUDE.md @@ -87,7 +87,7 @@ gds-framework ← core engine (pydantic only, no upstream deps) gds-sim ← discrete-time simulation (standalone, pydantic only) ↑ - ├── gds-analysis ← spec→sim bridge, reachability (gds-framework + gds-sim) + ├── gds-analysis ← spec→sim bridge, reachability (gds-framework + gds-sim + gds-continuous[opt]) └── gds-psuu ← parameter sweep + Optuna (gds-sim) gds-continuous ← continuous-time ODE engine (standalone, pydantic only) [scipy] diff --git a/docs/research/paper-implementation-gap.md b/docs/research/paper-implementation-gap.md index d50781a..8098415 100644 --- a/docs/research/paper-implementation-gap.md +++ b/docs/research/paper-implementation-gap.md @@ -455,6 +455,7 @@ require external tooling (SymPy, JuliaReach). | 3 (metric) | gds-framework (constraints.py, spec.py) | **Done** — StateMetric, OWL, SHACL | | 4 (R(x)) | gds-analysis (reachability.py) | **Done** — `reachable_set()`, `ReachabilityResult` | | 5 (X_C) | gds-analysis (reachability.py) | **Done** — `configuration_space()` (iterative Tarjan SCC) | +| 5b (B(T)) | gds-analysis (backward_reachability.py) | **Done** — `backward_reachable_set()` + `extract_isochrones()` | | 6 (D'F) | gds-analysis (future) | Research frontier | | 7 (controllability) | gds-analysis (future) | Research frontier | diff --git a/docs/research/research-boundaries.md b/docs/research/research-boundaries.md index 540902d..de3705c 100644 --- a/docs/research/research-boundaries.md +++ b/docs/research/research-boundaries.md @@ -450,9 +450,9 @@ Neither question requires immediate resolution. Both are triggered by concrete f |---|---| | Building a structural controllability analyzer | RQ1 (MIMO semantics) | | Building a shared simulation harness | RQ2 (timestep semantics) | -| Adding a continuous-time DSL | RQ1 + RQ2 | +| Adding a continuous-time DSL | RQ1 + RQ2 | **Done** — `gds-continuous` | | Adding a hybrid systems DSL | RQ1 + RQ2 | -| Extracting state-space matrices (A, B, C, D) | RQ1 | +| Extracting state-space matrices (A, B, C, D) | RQ1 | **Done** — `gds-symbolic` linearize | | Consolidating OGS PatternIR into GDSSpec | RQ3 (refactoring decision) | | Adding a stateless DSL (signal processing, Bayesian networks) | RQ3 (validates X=∅ pattern) | diff --git a/docs/research/verification-plan.md b/docs/research/verification-plan.md index 1a7b0ed..4e0085b 100644 --- a/docs/research/verification-plan.md +++ b/docs/research/verification-plan.md @@ -153,7 +153,7 @@ are inherently coupled. | Artifact | Location | Format | |---|---|---| -| R3 undecidability proof | `docs/research/verification/r3-undecidability.tex` | LaTeX | +| R3 undecidability proof | `docs/research/verification/r3-undecidability.md` | Markdown + LaTeX | | R1/R2 completeness argument | `docs/research/verification/representability-proof.md` | Markdown | ### Dependencies @@ -243,7 +243,9 @@ Prove: if the constraint set `C(x, t; g)` is compact, convex, and continuous, then an attainability correspondence exists. This is a runtime/R3 concern -- it requires evaluating `f` on concrete state. -Implementation target: future `gds-analysis` package. +The `gds-analysis` package now exists with reachability (`reachable_set`, +`configuration_space`, `backward_reachable_set`) but existence proofs +require additional analytical machinery beyond trajectory sampling. ### 4b. Local Controllability (Paper Theorem 4.4) @@ -253,8 +255,9 @@ is 0-controllable from a neighborhood around equilibrium. ### 4c. Connection to Bridge Proposal Steps 3-7 of the bridge proposal in [paper-implementation-gap.md](paper-implementation-gap.md) -map to this phase. Steps 1-2 (AdmissibleInputConstraint, TransitionSignature) -are already implemented and provide the structural skeleton. +map to this phase. Steps 1-5 are complete (AdmissibleInputConstraint, +TransitionSignature, StateMetric, reachable_set, configuration_space). +Steps 6-7 remain open (#142). ### Dependencies diff --git a/packages/gds-analysis/CLAUDE.md b/packages/gds-analysis/CLAUDE.md index c566c2f..f999ac1 100644 --- a/packages/gds-analysis/CLAUDE.md +++ b/packages/gds-analysis/CLAUDE.md @@ -6,17 +6,19 @@ - **Import**: `import gds_analysis` - **Dependencies**: `gds-framework>=0.2.3`, `gds-sim>=0.1.0` +- **Optional**: `[continuous]` for `gds-continuous[scipy]` + numpy (backward reachability) ## Architecture -Four modules, each bridging one aspect of structural specification to runtime: +Five modules, each bridging one aspect of structural specification to runtime: | Module | Function | Paper reference | |--------|----------|-----------------| | `adapter.py` | `spec_to_model(spec, policies, sufs, ...)` → `gds_sim.Model` | — | | `constraints.py` | `guarded_policy(policy_fn, constraint)` → wrapped policy | Def 2.5 | -| `metrics.py` | `trajectory_distances(results, spec)` → distance matrix | — | -| `reachability.py` | `reachable_set(spec, model, state, inputs)` → R(x) | Def 4.1, 4.2 | +| `metrics.py` | `trajectory_distances(results, spec)` → distance matrix | Assumption 3.2 | +| `reachability.py` | `reachable_set(model, state, inputs)` → R(x) | Def 4.1, 4.2 | +| `backward_reachability.py` | `backward_reachable_set(dynamics, ...)` → B(T) | Def 4.1 (backward) | ### spec_to_model adapter From 1a9a3e537ac40819abfc5dd9daaf1497b4548765 Mon Sep 17 00:00:00 2001 From: rohan Date: Sat, 28 Mar 2026 21:26:48 +0530 Subject: [PATCH 3/4] docs: fix all staleness findings from parallel audit agents MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Critical: - paper-implementation-gap.md Section 7: continuous-time marked as implemented (gds-continuous exists), no longer "not needed" Important: - paper-implementation-gap.md Steps 3-5: design signatures updated to match actual implementations (StateMetric fields, reachable_set API, configuration_space API) - formal-representability.md: 8-tuple → 9-tuple (StateMetric added) - semantic-web-summary.md: R1=13, R3=7, SHACL shapes=18 (was 12/6/13) - research-boundaries.md: "three DSLs" → "six DSLs" throughout - representation-gap.md: canonical spectrum table includes software + business domains - verification-plan.md: Phase 1b-c artifacts noted as not yet created --- docs/research/formal-representability.md | 6 +- docs/research/paper-implementation-gap.md | 79 ++++++++++------------- docs/research/representation-gap.md | 4 +- docs/research/research-boundaries.md | 10 +-- docs/research/semantic-web-summary.md | 6 +- 5 files changed, 47 insertions(+), 58 deletions(-) diff --git a/docs/research/formal-representability.md b/docs/research/formal-representability.md index 0788f94..34b4fb7 100644 --- a/docs/research/formal-representability.md +++ b/docs/research/formal-representability.md @@ -175,7 +175,7 @@ Token overlap is the auto-wiring predicate: compatible(p1, p2) := tokenize(p1.name) ∩ tokenize(p2.name) != empty ``` -**Definition 1.3 (GDSSpec).** A specification is an 8-tuple: +**Definition 1.3 (GDSSpec).** A specification is an 9-tuple: ``` S = (T, Sp, E, B, W, Theta, A, Sig) @@ -190,7 +190,7 @@ A : Name -> AdmissibleInputConstraint (state-dependent input constraints) Sig : MechName -> TransitionSignature (mechanism read dependencies) ``` -While presented as an 8-tuple, these components are cross-referencing: +While presented as an 9-tuple, these components are cross-referencing: blocks reference types, wirings reference blocks, entities reference types, admissibility constraints reference boundary blocks and entity variables, transition signatures reference mechanisms and entity variables. @@ -443,7 +443,7 @@ Specifically: ## 4. Layer 1 Representability: Specification Framework -**Property 4.1 (GDSSpec Structure is R1).** The 8-tuple +**Property 4.1 (GDSSpec Structure is R1).** The 9-tuple S = (T, Sp, E, B, W, Theta, A, Sig) round-trips through OWL losslessly for all structural fields. diff --git a/docs/research/paper-implementation-gap.md b/docs/research/paper-implementation-gap.md index 8098415..c0283fc 100644 --- a/docs/research/paper-implementation-gap.md +++ b/docs/research/paper-implementation-gap.md @@ -266,26 +266,21 @@ states are from each other. **Paper reference:** Assumption 3.2 -- d_X : X x X -> R, a metric. -**Concrete design:** +**Implemented** in `gds-framework` (`constraints.py`): ```python -@dataclass(frozen=True) -class StateMetric: - """A metric on the state space, enabling distance-based analysis.""" +class StateMetric(BaseModel, frozen=True): name: str - metric: Callable[[dict, dict], float] # (state_1, state_2) -> distance - covers: list[str] # entity.variable names in scope + variables: list[tuple[str, str]] # (entity, variable) pairs + metric_type: str = "" # annotation: "euclidean", etc. + distance: Callable[[Any, Any], float] | None = None # R3 lossy description: str = "" ``` -For common cases, provide built-in metrics: +Runtime analysis in `gds-analysis` (`metrics.py`): ```python -# Euclidean metric over all numeric state variables -euclidean_state_metric(spec: GDSSpec) -> StateMetric - -# Weighted metric with per-variable scaling -weighted_state_metric(spec: GDSSpec, weights: dict[str, float]) -> StateMetric +trajectory_distances(spec, trajectory, metric_name=None) -> dict[str, list[float]] ``` **Impact:** @@ -307,28 +302,24 @@ set of immediately reachable next states. **Paper reference:** Definition 4.1 -- R(x) = union_{u in U_x} {f(x, u)}. -**Concrete design:** +**Implemented** in `gds-analysis` (`reachability.py`): ```python def reachable_set( - spec: GDSSpec, - state: dict, - f: Callable[[dict, dict], dict], # state update function - input_sampler: Callable[[], Iterable[dict]], # enumerates/samples U_x -) -> set[dict]: - """Compute R(x) by evaluating f(x, u) for all admissible u.""" + model: Model, + state: dict[str, Any], + *, + input_samples: list[dict[str, Any]], + state_key: str | None = None, + exhaustive: bool = False, + float_tolerance: float | None = None, +) -> ReachabilityResult: ``` -For finite/discrete input spaces, this is exact enumeration. For -continuous input spaces, this requires sampling or symbolic analysis. - -**Impact:** -- First dynamical analysis capability -- Enables "what-if" analysis: "from this state, what states can I reach?" -- Foundation for configuration space (Step 5) - -**Prerequisite:** Steps 1 (U_x), 3 (metric for measuring distance). -Requires gds-sim or equivalent runtime. +For discrete input spaces, pass exhaustive samples with `exhaustive=True`. +For continuous spaces, results are approximate (no coverage guarantee). +Returns `ReachabilityResult` with `states`, `n_samples`, `n_distinct`, +`is_exhaustive` metadata. ### Step 5: Configuration Space X_C @@ -338,22 +329,17 @@ the set of states from which any other state in X_C is reachable. **Paper reference:** Definition 4.2 -- X_C subset X such that for each x in X_C, there exists x_0 and a reachable sequence reaching x. -**Concrete design:** +**Implemented** in `gds-analysis` (`reachability.py`): ```python -def configuration_space( - spec: GDSSpec, - f: Callable, - input_sampler: Callable, - initial_states: Iterable[dict], - max_depth: int = 100, -) -> set[frozenset]: - """Compute X_C via BFS/DFS over R(x) from initial states.""" +def reachable_graph(model, initial_states, *, input_samples, max_depth, ...) -> dict +def configuration_space(graph: dict) -> list[set]: + """Iterative Tarjan SCC. Returns SCCs sorted by size (largest = X_C).""" ``` -For finite state spaces, this is graph search over the reachability -graph. For continuous state spaces, this requires approximation -(grid-based, interval arithmetic, or abstraction). +`reachable_graph` builds the adjacency dict via BFS; `configuration_space` +finds strongly connected components. For discrete systems with exhaustive +input samples, the result is exact. **Impact:** - Answers "is the target state reachable from the initial condition?" @@ -476,11 +462,12 @@ gds-framework <-- gds-sim <-- gds-analysis Some paper concepts are intentionally absent for good architectural reasons: -1. **Continuous-time dynamics (xdot = f(x(t)))** -- The paper presents this - as an alternative representation. The software is discrete-time by design. - Continuous-time would require a fundamentally different execution model. - Per RQ2 in research-boundaries.md, temporal semantics should remain - domain-local. +1. ~~**Continuous-time dynamics (xdot = f(x(t)))**~~ -- **Now implemented.** + The `gds-continuous` package provides an ODE engine (RK45, Radau, BDF, + etc.) with event detection and parameter sweeps. `gds-analysis` uses it + for backward reachability. `gds-symbolic` compiles symbolic ODEs to + `gds-continuous` callables via lambdify. The discrete/continuous split + is bridged, not absent. 2. **The full attainability correspondence F as an axiomatic foundation** -- The paper notes (Section 3.2) that Roxin's original work defined GDS via diff --git a/docs/research/representation-gap.md b/docs/research/representation-gap.md index fdb0beb..83502db 100644 --- a/docs/research/representation-gap.md +++ b/docs/research/representation-gap.md @@ -170,11 +170,13 @@ boundary, seen from the outside. The canonical spectrum across five domains revealed a structural divide: -| Domain | |X| | |f| | Form | Character | +| Domain | dim(X) | dim(f) | Form | Character | |---|---|---|---|---| | OGS (games) | 0 | 0 | h = g | Stateless — pure maps | | Control | n | n | h = f . g | Stateful — observation + state update | | StockFlow | n | n | h = f . g | Stateful — accumulation dynamics | +| Software (DFD/SM/C4/ERD) | 0 or n | 0 or n | varies | Diagram-dependent | +| Business (CLD/SCN/VSM) | 0 or n | 0 or n | varies | Domain-dependent | Games compute equilibria. They don't write to persistent state. Even corecursive loops (repeated games) carry information forward as *observations*, not as diff --git a/docs/research/research-boundaries.md b/docs/research/research-boundaries.md index de3705c..2d946b2 100644 --- a/docs/research/research-boundaries.md +++ b/docs/research/research-boundaries.md @@ -6,7 +6,7 @@ ## Status: What Has Been Validated -Three independent DSLs now compile to the same algebraic core: +Six independent DSLs now compile to the same algebraic core: | DSL | Domain | Decision layer (g) | Update layer (f) | Canonical | |---|---|---|---|---| @@ -26,7 +26,7 @@ Key structural facts: - Canonical `h = f ∘ g` has survived three domains with no extensions required. - No DSL uses `ControlAction` — all non-state-updating blocks map to `Policy`. - Role partition (boundary, policy, mechanism) is complete and disjoint in every case. -- Cross-built equivalence (DSL-compiled vs hand-built) has been verified at Spec, Canonical, and SystemIR levels for all three DSLs. +- Cross-built equivalence (DSL-compiled vs hand-built) has been verified at Spec, Canonical, and SystemIR levels for all validated DSLs. - OGS canonical validation confirms `f = ∅`, `X = ∅` — compositional game theory is a **degenerate dynamical system** where `h = g` (pure policy, no state transition). See [RQ3](#research-question-3-ogs-as-degenerate-dynamical-system) below. A canonical composition pattern has emerged across DSLs: @@ -358,7 +358,7 @@ These are view-layer concerns (Layer 4). Whether to consolidate `PatternIR` into ### Background -With three DSLs compiling to GDSSpec, the framework now supports two independent analytical lenses on the same system: +With six DSLs compiling to GDSSpec, the framework now supports two independent analytical lenses on the same system: 1. **Game-theoretic lens** (via PatternIR) — equilibria, incentive compatibility, strategic structure, utility propagation 2. **Dynamical lens** (via GDSSpec/CanonicalGDS) — reachability, controllability, stability, state-space structure @@ -437,7 +437,7 @@ Do not attempt to resolve the tension architecturally. Keep the lenses parallel. These questions mark the boundary between: -- **Structural compositional modeling** — validated by three DSLs, canonical proven stable +- **Structural compositional modeling** — validated by six DSLs, canonical proven stable - **Dynamical execution and control-theoretic analysis** — the next frontier They are the first genuine architectural fork points after validating canonical centrality. @@ -467,7 +467,7 @@ After three independent domains with three distinct canonical profiles (`h = g`, - The role system (Boundary, Policy, Mechanism) covers all three domains without `ControlAction`. - The type/space system handles semantic separation across all three domains. - The temporal loop pattern is structurally uniform and semantically adequate for structural modeling. -- Cross-built equivalence holds at Spec, Canonical, and SystemIR levels for all three DSLs. +- Cross-built equivalence holds at Spec, Canonical, and SystemIR levels for all validated DSLs. The canonical form `(x, u) ↦ x'` with varying dimensionality of X now functions as a **unified transition calculus** — not merely a decomposition of dynamical systems, but a typed algebra of transition structure that absorbs stateless (games), stateful (control), and state-dominant (stockflow) formalisms under one composition substrate. diff --git a/docs/research/semantic-web-summary.md b/docs/research/semantic-web-summary.md index 5494fef..5536e96 100644 --- a/docs/research/semantic-web-summary.md +++ b/docs/research/semantic-web-summary.md @@ -111,10 +111,10 @@ fields survive. Known lossy fields: | Metric | Count | |---|---| -| R1 concepts (fully representable) | 12 | +| R1 concepts (fully representable) | 13 | | R2 concepts (SPARQL-needed) | 3 | -| R3 concepts (not representable) | 6 | -| SHACL shapes | 13 | +| R3 concepts (not representable) | 7 | +| SHACL shapes | 18 | | SPARQL templates | 7 | | Verification checks expressible in SHACL | 6 of 15 | | Verification checks expressible in SPARQL | 6 more | From 54ea5e097db37780847b7117faf9085718502adb Mon Sep 17 00:00:00 2001 From: rohan Date: Sat, 28 Mar 2026 21:34:20 +0530 Subject: [PATCH 4/4] chore: add __marimo__ cache to gitignore --- .gitignore | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/.gitignore b/.gitignore index b1c2ca3..cfe868b 100644 --- a/.gitignore +++ b/.gitignore @@ -42,3 +42,7 @@ Thumbs.db # Pyright .pyright/ + +# Claude Code +.claude/ +__marimo__/