feat(language): a model writes its formulations out on request, and a curve prints as the curve it states

docs/about/limits.md

@@ -23,9 +23,13 @@ costs to add.
   `at`, `shift`, and the `where` comparisons. A file cannot add one. Adding one
   here is the expensive kind: every engine that builds models has to implement
   it, and the typesetter has to print it in LaTeX, Typst and Markdown.
-- **A formulation** is a block that expands into ordinary variables and
-  constraints before the model is built. `piecewise:` is the only one. It costs
-  as much as a primitive to build, but composes as freely as a macro.
+- **A formulation** is a block that states ordinary variables and constraints
+  rather than being one. `piecewise:` and `sos:` are the two. It costs as much as
+  a primitive to build, but composes as freely as a macro. A formulation emits
+  variables and constraints, and any parameter it emits it derives — so the same
+  data binds a model and its expansion, and
+  [`spec.expand()`](../reference/language/piecewise.md#writing-a-formulation-out)
+  needs no source a reader has to supply.
 
 A request that is none of the three is refused, and the
 [table of refusals](#deliberate-non-primitives) records it with what to write
@@ -66,11 +70,11 @@ the same model written out by hand.
 
 ### Three kinds of refusal
 
-| The language refuses it because…           | Examples                                                                                                                                                     | Can it change?                             |
-| ------------------------------------------ | ------------------------------------------------------------------------------------------------------------------------------------------------------------ | ------------------------------------------ |
-| **one solver cannot take it**              | indicator constraints; a quadratic constraint. `sos:` was in this group, and entered: a solver with sets takes it as one, and a solver without gets binaries | yes, solver by solver                      |
-| **the file would stop being the artifact** | arbitrary Python, whose content no loader can check and no typesetter can print                                                                              | no                                         |
-| **this project puts the work elsewhere**   | data preparation such as resampling; helpers for one domain; Python that decides which declarations exist                                                    | it could; this project does not want it to |
+| The language refuses it because…           | Examples                                                                                                                                                                        | Can it change?                             |
+| ------------------------------------------ | ------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- | ------------------------------------------ |
+| **one solver cannot take it**              | indicator constraints; a quadratic constraint. `sos:` was in this group, and entered: a solver with sets takes it as one, and a model for a solver without is written out first | yes, solver by solver                      |
+| **the file would stop being the artifact** | arbitrary Python, whose content no loader can check and no typesetter can print                                                                                                 | no                                         |
+| **this project puts the work elsewhere**   | data preparation such as resampling; helpers for one domain; Python that decides which declarations exist                                                                       | it could; this project does not want it to |
 
 Three things never appear inside one model: an `if`, a loop, and a set of
 declarations that depends on the data. A dimension computed before the model
@@ -89,13 +93,14 @@ answer it. If it did, one solver's limits would be written into the language,
 and every other solver would inherit them.
 
 - HiGHS has no special-ordered sets. Gurobi does. An engine handing a model to
-  HiGHS rewrites each set as binaries and big-M rows; one handing it to Gurobi
-  passes the set through.
+  Gurobi passes the set through; one handing it to HiGHS refuses it, and the
+  author writes the set out with `spec.expand('sos')` first.
 - A quadratic constraint is accepted by some solvers only when it is convex,
   and convexity depends on the numbers, which the file does not have.
 
 So `sos:` entered the language on the first question alone. Each engine then
-decides how to hand it to its solver, and reports which it did.
+decides whether it takes a set, and the language decides what a set is written
+out as.
 
 ## What counts as data preparation
 

docs/about/what-counts-as-language.md

@@ -34,8 +34,10 @@ Four rules follow from the test:
 - Degree is decided when the file loads. Whether `x * y` is allowed does not
   depend on which engine builds the model.
 
-A `piecewise:` block expands into ordinary variables and constraints, so the
-language decides that expansion too.
+A `piecewise:` block and a `sos:` block each state ordinary variables and
+constraints, so the language decides what they state, and
+[`spec.expand()`](../reference/language/piecewise.md#writing-a-formulation-out)
+writes it out the same way for every tool.
 
 ## What each tool decides for itself
 

docs/howto/curve-by-hand.md

@@ -26,7 +26,7 @@ file, so it cannot say this. The formulation written out can.
 
    ```yaml
    sos:
-     on_one_segment: { variable: weight, over: bp, type: 2, big_m: 1 }
+     on_one_segment: { variable: weight, over: bp, type: 2 }
    ```
 
 3. **Write the convexity row, and one row per flow.** The row per flow is where

docs/howto/print.md

@@ -47,7 +47,18 @@ keep the document current as the file changes.
    `notation: typst` or none. Without `--standalone` the output is a fragment
    to `\input` or `#include` into a paper.
 
-4. **Keep it current** with a rule in the paper's build:
+4. **Print the rows a solver holds** with `--expand`, where the model states a
+   curve or a set and the reader wants the formulation rather than the
+   construct:
+
+   ```bash
+   python -m math_spec markdown model.yaml --expand
+   ```
+
+   The same table serves both renders: a name the expansion emits, such as
+   `cost_curve_lam`, may be spelled in it.
+
+5. **Keep it current** with a rule in the paper's build:
 
    ```make
    model.tex: model.yaml model.symbols.yaml

docs/reference/language/piecewise.md

@@ -9,6 +9,10 @@ Two blocks state shapes that no `expression:` can, because an expression is
 affine. `piecewise:` states a curve through breakpoints. `sos:` states a family
 of variables of which only one, or only two neighbours, may be non-zero.
 
+Both are **formulations**: each states plain variables and constraints rather
+than being one, and [`spec.expand()`](#writing-a-formulation-out) writes them
+out.
+
 ## `piecewise`
 
 A `piecewise` block ties two or more expressions to one piecewise-linear curve.
@@ -48,11 +52,12 @@ piecewise:
 | `activity` | a binary variable that gates the curve ([below](#activity))                              | default `null`      |
 | `points`   | how far each curve runs, where the curves are not all the same length ([below](#points)) | default `null`      |
 
-A block expands before building, into plain variables and constraints: one
-weight per breakpoint in `[0, 1]`, one row making the weights sum to 1, and one
-row per link tying its expression to the weighted breakpoints. That expansion
-is what the rest of the model sees, and what the
-[typeset output](../typeset.md) prints.
+A block states plain variables and constraints: one weight per breakpoint in
+`[0, 1]`, one row making the weights sum to 1, and one row per link tying its
+expression to the weighted breakpoints. A `Program` holds those rows, because a
+consumer builds them; the [typeset output](../typeset.md) prints the curve
+itself, and [`spec.expand()`](#writing-a-formulation-out) is what writes the
+rows into a model of their own.
 
 The breakpoint order is the declared order of `over`. A curve whose breakpoints
 decrease in that order is refused when the data binds.
@@ -107,15 +112,16 @@ the axis. A gap, or a curve with no points, is refused when the data binds.
 
 `method` says how the weights are restricted once they exist.
 
-| `method`                | What it adds                                                                    |                                                                |
-| ----------------------- | ------------------------------------------------------------------------------- | -------------------------------------------------------------- |
-| `adjacency` _(default)_ | a binary per segment, and `lam <= seg + shift(seg, along=bp, offset=1, edge=0)` | the curve, built                                               |
-| `sos2`                  | an [`sos:`](#sos) block over the same weights                                   | the curve, stated for a solver that branches on the set itself |
-| `convex`                | nothing                                                                         | the hull, which is a pure linear program                       |
-| `lp`                    | no weights at all: one row per segment line, plus two rows holding the domain   | the curve as its own lines                                     |
+| `method`                | What it adds                                                                  |                                                                |
+| ----------------------- | ----------------------------------------------------------------------------- | -------------------------------------------------------------- |
+| `adjacency` _(default)_ | an [`sos:`](#sos) block over the weights, written out as binaries             | the curve, built                                               |
+| `sos2`                  | an [`sos:`](#sos) block over the weights, left as a set                       | the curve, stated for a solver that branches on the set itself |
+| `convex`                | nothing                                                                       | the hull, which is a pure linear program                       |
+| `lp`                    | no weights at all: one row per segment line, plus two rows holding the domain | the curve as its own lines                                     |
 
 `adjacency` and `sos2` state the same restriction and reach the same optimum.
-They differ in what the solver is handed.
+They differ in what the solver is handed: `adjacency` **is** `sos2` with the set
+written out, so the two emit the same rows under the same names.
 
 `convex` is a different model. It is exact only for a curve whose curvature
 matches the optimisation pressure, and that match is checked against the
@@ -154,7 +160,7 @@ sos:
     variable: build # the variable the set is over
     over: size # the dimension it runs along — one set per coordinate of the rest
     type: 1 # 1: at most one non-zero; 2: at most two, and consecutive
-    big_m: 500 # optional, and only read by a solver that has to reformulate
+    bound: 500 # optional: the coefficient the set's own expansion links a member by
 ```
 
 `type: 1` is a choice: at most one member is non-zero. `type: 2` is an
@@ -167,8 +173,74 @@ Membership belongs to the variable. Its `where` decides which coordinates exist,
 so a masked-out member is not in the set. The order is the declared order of
 the `over` dimension.
 
-A solver with no concept of a set is handed binaries and big-M rows instead.
-That rewrite is mixed-integer, so it gives up its duals, and it needs a finite
-M: every member needs a `bounds.upper` or a `big_m:`, and a negative
-`bounds.lower` is refused. A model that fails those conditions still solves on
-a solver that takes the set, and the message says so.
+### What a set is written out as
+
+`spec.expand('sos')` states the set as binaries: one per member for `type: 1`,
+one per segment for `type: 2`. A member the binaries do not admit is held at
+zero, from above and from below. The names are the block's own, and the rows are
+these, for a set `s` over variable `x` along `d`, writing `admitted` for
+`(s_seg)` at `type: 1` and `(s_seg + shift(s_seg, along=d, offset=1, edge=0))`
+at `type: 2`:
+
+| Emitted                                            |                                                   |
+| -------------------------------------------------- | ------------------------------------------------- |
+| `s_seg`                                            | a binary over `x`'s own dims, masked as `x` is    |
+| `s_pick`: `sum(s_seg, over=d) <= 1`                | at most one is picked                             |
+| `s_nonzero` (`type: 1`), `s_adjacency` (`type: 2`) | `x <= upper * admitted`                           |
+| the same name plus `_below`                        | `x >= lower * admitted`, where `lower` is not `0` |
+
+Each coefficient is read off the member's own `bounds:`, and the set's `bound:`
+replaces the one above where it declares one. A binary member's are `0` and `1`,
+from its domain. A row multiplies by its coefficient rather than reading it, so
+a bound the data carries is a coefficient like any other:
+`bounds: {lower: floor, upper: cap}` states `x >= floor * admitted` and
+`x <= cap * admitted`.
+
+Two coefficients are left out rather than printed, because the row would state
+what another row already does: a `1` above, and a `lower` of `0`, which the
+variable's own bound states.
+
+So each side needs a coefficient, and a model is refused at load without one:
+
+- `bounds.lower`, a number or a parameter. An omitted lower bound leaves the
+  member free below zero, which no row can pull back.
+- `bounds.upper`, a number or a parameter, or the set's `bound:`, or
+  `domain: binary`.
+
+A positive `bounds.lower` loads and is infeasible, as it is on a solver that
+takes the set: an unpicked member has to be `0`, and its own bound says it is
+above that.
+
+A name the expansion writes that the file already declares is refused at load
+too.
+
+## Writing a formulation out
+
+`Spec.expand()` returns the same math with its formulations stated as plain
+variables and constraints:
+
+```python
+from math_spec import to_spec
+
+spec = to_spec('curve.yaml')
+spec.expand()  # every formulation
+spec.expand('sos')  # only the sets
+spec.expand('piecewise')  # only the curves
+```
+
+- **The kinds are `'piecewise'` and `'sos'`, and no argument means both.** Any
+  other string is refused, naming the two. Curves go first whatever order they
+  are asked in, because a `method: sos2` curve states a set and no set states a
+  curve.
+- **A model with nothing to write out is the model that comes back.** So is a
+  second call with the same kinds.
+- **The same data binds a model and its expansion.** A set emits no parameter,
+  and every parameter a curve emits it derives
+  ([`derivation`](../reading.md#nodes-and-masks)).
+- **A model that derived parameters prints rather than round-trips.** A derived
+  parameter is filled from the block it came from, which a file cannot state,
+  so `to_yaml()` on such an expansion is refused and
+  [`typeset()`](../typeset.md) is what reads it.
+- **`to_program()` writes the curves out and leaves the sets.** A program
+  carries a set, because a consumer with the concept takes one; a consumer
+  without it refuses the model and names `spec.expand('sos')`.