You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
{{ message }}
Repository navigation
Commit 4b105e6
Browse filesBrowse the repository at this point in the historyBrowse files
Collects means never larger, and Common declares sixteen more growths (#1195)
* Collects means never larger, and Common declares sixteen more growths
#746 tier 2's next item is a declared growth for the rules still at Unknown, because
the growth ceiling protects only an inverse pair whose directions are declared. A
census of the 152 over the corpus, then Common's 22 read in terms of hole sizes,
found that thirteen of them are one shape: a hole matched twice and written once
beside one new node -- a + a = 2 * a, a * a = a ^ 2, a + a * b = a * (1 + b),
(v - a) * (v + a) = v ^ 2 - a ^ 2 and their relatives. Every one is 1 - |a|: exactly
as large at a leaf and smaller everywhere else. That is the commonest collecting
shape there is, and the contract could not say it: Collects was "always fewer" and
Rearranges "always the same", so the family sat at Unknown as a finding, and the
guide listed it among the shapes that look declarable and are not.
Nothing consumed the strict reading. RulesUpTo(Rearranges) wants "never grows", the
selector-cost proxy test asks for a majority, and the only check that read Collects
as strict was the corpus test's own. So the contract is refined rather than the
family left out: Collects promises never larger and smaller for some input;
Rearranges the same size for every input; Expands larger for every input. The
ninety-seven existing declarations -- "exactly -2", "at most -4" -- stay true, the
corpus contradicts Collects only on a firing that grew, and the enum, the guide and
the corpus test say so in the same words.
Under it Common declares sixteen: the thirteen above as Collects, each with its
count in the comment; the sign-times-absolute-value cancellation as Collects, since
it is -1 - 2|a| outright; and the reciprocal-factor pair as exactly Rearranges and
exactly Expands, because IsWholeReciprocal is `entity is Rational(...)` and admits
the literal only -- the guide said it also took a written 1 / c and was wrong. The
six that stay Unknown say why beside the rule: five attach a condition sized by
their own operands, and a + a / b = a * (1 + 1 / b) is 3 - |a|, two nodes larger at
a leaf, which the corpus had never fired. Six shapes join the corpus so that every
newly declared rule fires on it at least once.
Two pins moved and are re-recorded rather than loosened. The safe ceiling now moves
two of the five ordinary inputs, not one: (x + 1) * (x - 1) goes to x ^ 2 - 1 ^ 2,
and stops there because no safe rule folds a numeric power. And the narrow ceiling
brings the difference of squares together, which a test asserted only the widest
could -- renamed to what it shows now. The census is 111 collect, 46 rearrange, 31
expand, 136 unjudged; the safe ceiling admits 157 of 324.
The relatives in Power and Factorization -- a ^ n * a, a / b / b and theirs -- are
next, each on its own count.
Part of #746.
Full suite 9579 passed, 0 failed -- one of them a throwaway census probe, not committed.
Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_012sonx8iAspMiwRwokT1Ura
* Record the answers the sixteen declarations change
Measured on a build of master (72676b0) and of this branch, with one throwaway probe
run on each. Transformation.CanonicalizationOverGraph(budget), public and at the safe
ceiling by default, now collects what the rules collect: (x + y) * (x - y) was
(-y + x) * (x + y) and is -y ^ 2 + x ^ 2, the tree x ^ 2 - y ^ 2 reaches; x + x was
left as written and is 2 * x; x + x * y is (1 + y) * x. Entity.Canonicalize() runs the
rule pass rather than the graph and is unchanged on every input probed. The growth of
sixteen rules of RewriteRules.Common moves from Unknown, and what Collects promises
moves from "fewer for every input" to "never more, fewer for some".
Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_012sonx8iAspMiwRwokT1Ura
---------
Co-authored-by: Claude Fable 5.1 <noreply@anthropic.com>
Copy file name to clipboardExpand all lines: BREAKING-CHANGES.md
+35Lines changed: 35 additions & 0 deletions
Display the source diff
Display the rich diff
Original file line number
Diff line number
Diff line change
@@ -70,6 +70,10 @@ read first.
70
70
|**Silent**|`"1/x - 1/x".ToEntity().Simplify()`, and every difference of a term from itself where that term can be undefined |`0`, including at `x = 0` where neither side has a value |`0 provided not x = 0`|
71
71
|**Silent**|`"(x + 1)!/(x + 1)!".ToEntity().Simplify()`, and every cancelled quotient whose repeated part can be undefined |`1 provided not (1 + x)! = 0`|`1 provided 1 + x in RR and (1 + x >= 0 or not 1 + x in ZZ)` — the same value everywhere, a condition that says why |
72
72
||`"ln(x)/ln(x)".ToEntity().Simplify()`, and every quotient divided out by a divisor that can be undefined |`1 provided not ln(x) = 0` — which is `1` at `x = 0`, where the quotient has no value |`1 provided not ln(x) = 0 and not x = 0`|
73
+
||`Transformation.CanonicalizationOverGraph(budget).ApplyOrKeep("(x + y) * (x - y)")`, and every input one of `Common`'s sixteen newly declared rules collects |`(-y + x) * (x + y)` — not the tree `x ^ 2 - y ^ 2` reaches |`-y ^ 2 + x ^ 2` — one tree for both |
74
+
|| the same on `x + x`, and `x + x * y`|`x + x`, `x * y + x` — left as written |`2 * x`, `(1 + y) * x`|
75
+
|**Silent**|`RewriteRules.Common.Rules[i].Growth`, for sixteen rules |`Unknown`|`Collects` for fourteen, `Rearranges` and `Expands` for the reciprocal-factor pair |
76
+
|**Silent**| what `RewriteRuleGrowth.Collects` promises | fewer nodes for every input | never more, and fewer for some — every rule that was `Collects` still is |
73
77
74
78
### A cancelled quotient says its operand is defined, not only non-zero
75
79
@@ -865,6 +869,37 @@ the middle of a rewrite. It is a bound where there was none, not a tight one.
865
869
[#896](https://github.com/asc-community/AngouriMath/issues/896) said a caller could not previously
866
870
find out.
867
871
872
+
### `Collects` promises never larger, and `Common` declares sixteen growths
873
+
874
+
`RewriteRuleGrowth.Collects` used to mean the replacement is written with fewer nodes than the
875
+
pattern for every input. It now means **never more, and fewer for some** — `Rearranges` is still
876
+
the same size for every input and `Expands` still larger for every input. Every rule that was
877
+
`Collects` still is, and every count written beside one ("exactly −2", "at most −4") still holds; the
878
+
promise is weaker only where nothing relied on the strong one. The reason is the commonest
879
+
collecting shape in the library: a hole matched twice and written once beside one new node,
880
+
`a + a = 2 * a`, `a * a = a ^ 2`, `a + a * b = a * (1 + b)`, which is `1 − |a|` — exactly as large
881
+
at a leaf and smaller everywhere else. Under the strict reading it could not be declared at all,
882
+
and thirteen of `Common`'s rules sat at `Unknown` for it.
883
+
884
+
Sixteen of `Common`'s rules declare a growth now, so `RewriteRules.Common.Rules[i].Growth` changes
885
+
for them, and `Saturation.RulesUpTo(Rearranges)` — the ceiling `Transformation.CanonicalizationOverGraph`
886
+
runs at by default — admits fifteen more rules, 157 of 324 where it was 142. What that changes on
887
+
ordinary input is what those rules do: a repeated term collects over the graph where it used to be
888
+
left as written, and the difference of squares reaches the tree its expansion reaches.
889
+
`Entity.Canonicalize()` runs `Transformation.Canonicalization`, the rule pass rather than the graph,
890
+
and answers exactly as before on every input below.
891
+
892
+
|| Was | Is |
893
+
|---|---|---|
894
+
|`Transformation.CanonicalizationOverGraph(budget).ApplyOrKeep("(x + y) * (x - y)")`|`(-y + x) * (x + y)` — not the tree `x ^ 2 - y ^ 2` reaches, `-y ^ 2 + x ^ 2`|`-y ^ 2 + x ^ 2` — one tree for both |
895
+
| the same on `(x + 1) * (x - 1)`|`(1 + x) * (-1 + x)`|`-1 + x ^ 2`|
896
+
| the same on `x + x`|`x + x` — left as written |`2 * x`|
897
+
| the same on `x + x * y`|`x * y + x` — reordered, not collected |`(1 + y) * x`|
898
+
|`RewriteRules.Common.Rules[i].Growth`, for sixteen rules |`Unknown`|`Collects` for fourteen; `Rearranges` for `a-reciprocal-rational-factor-is-a-division`, `Expands` for its negated twin |
Copy file name to clipboardExpand all lines: Sources/AngouriMath/Docs/Contributing/WritingARule.md
+21-10Lines changed: 21 additions & 10 deletions
Display the source diff
Display the rich diff
Original file line number
Diff line number
Diff line change
@@ -135,7 +135,7 @@ A pattern replacement gets:
135
135
-**an exact growth**, counted from the two patterns rather than declared.
136
136
137
137
A code replacement gets neither, and its growth is `Unknown` unless you declare one. That is the
138
-
honest default — **152** rules sit at `Unknown` — but declare it where you can justify it:
138
+
honest default — **136** rules sit at `Unknown` — but declare it where you can justify it:
139
139
140
140
```csharp
141
141
// The Chebyshev expansion of sin(n * a) is a sum of n terms where the pattern is one node,
@@ -157,30 +157,41 @@ cannot argue the claim from the code, leave it `Unknown`.
157
157
158
158
**Count the pattern against the replacement in terms of the holes**, and the answer is usually one
159
159
of a few shapes. A hole matched twice and written once gives `-(1 + |a|)`, which is a `Collects`
160
-
stronger than the corpus will show you, since the corpus fills its holes with single nodes. A
160
+
stronger than the corpus will show you, since the corpus fills its holes with single nodes. The same
161
+
hole beside one new node — `a + a = 2 * a`, `a * a = a ^ 2`, `a + a * b = a * (1 + b)` — gives
162
+
`1 - |a|`: exactly as large at a leaf and smaller everywhere else, and that is `Collects` too.
163
+
**`Collects` promises never larger, and smaller for some input**; `Rearranges` promises the same
164
+
size for every input. "Never larger" is the half the growth ceiling relies on, and the corpus checks
165
+
`Collects` by looking for a firing that grew, not for one that failed to shrink. A
161
166
replacement holding no hole at all — a constant, or `pi/2` — collects by the whole of the pattern.
162
167
Operators mapping one for one with every hole used once is `Rearranges`. A pattern that binds
163
168
nothing — `arctan(sqrt(3)) = pi/3`, `{ True, False }` — has a fixed size on both sides, so its delta
164
169
is a number and there is nothing to argue. And two numbers combined with `Number` arithmetic **fold
165
170
into one node** as the replacement is built, which is worth two on its own: `(c * v) * d` collects
166
171
where the same rule written without the cast would only rearrange.
167
172
168
-
**Four shapes look declarable and are not.** Each of these measured a clean, constant delta over the
173
+
**Two shapes look declarable and are not.** Each of these measured a clean, constant delta over the
169
174
corpus, and each is false:
170
175
171
176
|||
172
177
|---|---|
173
178
| the replacement is built with `<`, `>` and their kin | they **chain**: `(x > y) < 0` is `x > y and y < 0`, so a three-node replacement becomes seven. `EqualTo` does not chain, which is why the `equals` rules are declared and their comparison twins are not |
174
-
| the replacement attaches a `Provided` built from the operands | its size grows with them while the pattern's shrinks away, so the delta changes sign: `2 - |c|` for the shared-factor cancellation, `4 - |a| - |b|` for `(a - b) / (b - a)` |
175
-
| a hole can be filled by two spellings of one thing |`IsWholeReciprocal` takes the literal `1/3`, which is one node, and a written `1 / c`, which is three — so the delta is 0 in one and −2 in the other |
176
-
| a hole is repeated and the replacement squares it |`a * (a * b) = a^2 * b` is `1 - |a|`: zero for a leaf and negative for anything bigger |
179
+
| the replacement attaches a `Provided` built from the operands | its size grows with them while the pattern's shrinks away, so the delta changes sign: `2 - |c|` for the shared-factor cancellation, `3 - |a| - |b|` for `(a - b) / (b - a)`, and `3 - |a|` for `a + a / b = a * (1 + 1 / b)`, which is *larger* at a leaf though the corpus never fired it |
180
+
181
+
Two more used to be listed here and are not. The repeated hole that pays a literal to be gathered —
182
+
`a * (a * b) = a ^ 2 * b`, `k + k = 2 * k` and their relatives, every one `1 - |a|` — was
183
+
undeclarable only while `Collects` was read as "always fewer"; it is the commonest collecting shape
184
+
there is, and `Collects` promises never larger. `Common`'s thirteen are declared, with the count in
185
+
each one's comment; the relatives in `Power` and `Factorization` — `a ^ n * a`, `a / b / b` and
186
+
theirs — are the next to declare, each on its own count. And the reciprocal-factor rules were said
187
+
to admit two spellings of one thing; `IsWholeReciprocal` is `entity is Rational(...)`, so it admits
188
+
the literal only, and the pair is exactly `Rearranges` and exactly `Expands`.
177
189
178
190
**Every rule still at `Unknown` has been looked at, and each falls into one of the shapes above.**
179
191
Most of them compute their answer through a helper, so there is nothing to count; the rest either
180
-
build a comparison, attach a `Provided` sized by their own operands, or are the repeated hole that
181
-
pays a literal to be gathered — `a ^ n * a`, `a / b / b`, `a * a`, `k + k` and their two dozen
182
-
relatives, every one of them `1 - |a|`. So `Unknown` here is a finding rather than a gap, and a new
183
-
`Unknown` should be one too.
192
+
build a comparison or attach a `Provided` sized by their own operands. So `Unknown` here is a
193
+
finding rather than a gap, and a new `Unknown` should be one too — written beside the rule, as
194
+
`Common`'s six are.
184
195
185
196
**The comparison set is settled, and settled as `Unknown`.** Its sixty-odd rules were gone through
186
197
one at a time and all but seven fall into the shapes above: most build their replacement with `<` or
0 commit comments