Repository navigation
The "pattern operator"(?) #1437
Description
Activity
Triage of what
…means where it is written, and how large each piece is. The reference for #1409 uses it in five ways, and the same five cover what I find elsewhere.where example what it denotes what exists a listed set {1, 2, …, n},{2, 4, 6, …},{…, −1, 0}a range, or a one-sided infinite progression ZZ+ /\ [1; n]since #1435;{ k in ZZ : k <= 0 }a sum or product 1 + 2 + … + n,1 · 2 · … · n,a_1 + … + a_nsum(k, k, 1, n); a sum over an indexed familysum,product(four-argument form)a tuple or an argument list (x_1, …, x_n),f(x_1, …, x_n),[a_1, …, a_n]a family of names of symbolic length nothing: a matrix has a written size, and nnames cannot be listedan index set under a binder ∀ i ∈ {1, …, n},⋃_{i=1}^{n}the range again forall k in ZZ+ /\ [1; n],union(A_k, k in …)a decimal or a continued fraction 0.333…,1 + 1/(1 + 1/(1 + …))a limit nothing, and it is a different …: a limit, not a patternThe semantics of the first four is one thing:
…between shown terms names the sequence the shown terms determine, and the term after it names where it stops. So the pattern operator needs (a) a rule that reads the shown terms into a general term — an arithmetic progression from two terms (2, 4, …, 2ngives2k), a geometric one from two (1, 2, 4, …, 2^n), a shown general term with an index (a_1, a_2, …, a_ngivesa_k;x_1, …, x_nwith one term shown is that too), and refusal otherwise; and (b) a context that says what to build from the general term and the bounds: a set (ZZ+ /\ [1; n]under the general term, i.e. the image of a range), asum/product, a tuple (which is the part with no node today, #330), or a quantifier's index set. Reading a general term from three or more terms with no index shown (1, 4, 9, …) is guessing, and I would refuse it rather than pick the smallest polynomial; two terms of an arithmetic or geometric progression and a shown index are the honest cases, and they are what the books write.Size. Small for the set, the sum/product and the binder cases: a parser rule for
…/...inside a list, a reader of the progression (a hundred lines with tests), and an emittedsum(…),union(…)or range — no new node. Medium for the argument-list case, becausef(x_1, …, x_n)needs a family of names of symbolic length, which is a new kind of node and touches every operation that lists children (#330's tuple design, again). Out of scope for the limit…, which is a different word spelled the same.If the small part is wanted before v3, I can do it against the reference's rows (
{1, …, n},1 + 2 + … + n = n(n+1)/2,∀ i ∈ {1, …, n}); the medium part is a v3 design item next to tuples on #1019.Seems alright. The small case probably fits in 2.8, the medium case can be designed together with v3 together with symbolic length nodes.
I put this in 2.8. When the first part is done reassign milestone.
- added a commit that references this issue
on Sep 21, 2026 The small half landed in #1439 (
6d3c3d9b):{1, 2, ..., n},{2, 4, ..., 2 n},{5, 10, 15, ...},{..., -1, 0},{k - 2, ..., k + 2},1 + 2 + ... + n,1 * 2 * ... * n, also with…; built fromZZ /\ [a; z], a residue class cut by an interval,sumandproduct, with shown terms off the progression refused by name. Milestone moved to 3.0 for the larger half — the general term with an index shown and the argument list of symbolic length — which is v3's family of names (#1019).
See how much we can encode the semantics of … (written out in ASCII as ...)
To be triaged and designed depending on how large this is