From 7af68bef95ee5014f04affd187a77e603c5ff125 Mon Sep 17 00:00:00 2001 From: Rafael Vuijk Date: Sun, 23 Aug 2026 23:06:35 +0000 Subject: [PATCH] A bound index is not a free variable FreeVariables knew about Lambda and the set builder and about no other binder. A summation and a product bind their index, so sum(k, k, 1, n) is a function of n alone, and a definite integral binds its variable between its limits. All three reported the bound name as free. The index is bound over the bounds as well as the body, which is what Binding already says of itself -- the name a binder is handed is honoured throughout it, through the summand and the bounds -- so sum(k, k, k, n) is { n } as well. An indefinite integral and a derivative are left alone, and that is the part worth pinning rather than the part worth fixing. The antiderivative of t * b over t is b * t ^ 2 / 2 + C, still a function of t, and d/dt denotes a function of t. They look like the same shape as a summation and are not; a sweep that completes the binder list by adding them makes them wrong, so a test says so. Vars and VarsAndConsts are untouched. They mean every name occurring, bound ones included, which is what their own XML example has always documented by listing a lambda's parameter under variables and constants. Measured on a build of each side; 8070 -> 8080 passed, 0 failed, and no existing test depended on the old answers. --- BREAKING-CHANGES.md | 38 ++++++++++++ .../Core/Entity/Entity.Definition.cs | 33 ++++++++++ .../UnitTests/Common/FreeVariablesTest.cs | 60 +++++++++++++++++++ 3 files changed, 131 insertions(+) diff --git a/BREAKING-CHANGES.md b/BREAKING-CHANGES.md index 8a3449e9b..f39b6cb6b 100644 --- a/BREAKING-CHANGES.md +++ b/BREAKING-CHANGES.md @@ -21,6 +21,8 @@ read first. | Silent? | What | Was | Is | |---|---|---|---| +| **Silent** | `"sum(k, k, 1, n)".ToEntity().FreeVariables`, and `product` | `{ k, n }` — the bound index counted as free | `{ n }` | +| **Silent** | `"integral(t * b, t, 0, 1)".ToEntity().FreeVariables`, and every integral with limits | `{ b, t }` | `{ b }` | | | `"x ^ 3 - x > 0".ToEntity().Solve("x")`, and every polynomial inequality of degree three or more | `NotSufficientlySupportedException: Only linear and quadratic polynomial inequalities are supported` | `(-1; 0) \/ (1; +oo)` — the solution set | | **Silent** | `"a implies (b implies c)".ToEntity().Stringize()` | `a implies b implies c`, which reads back as `(a implies b) implies c` | `a implies (b implies c)` | | | `"(a implies b) implies c".ToEntity().Stringize()` | `(a implies b) implies c` | `a implies b implies c` | @@ -35,6 +37,42 @@ read first. | | `Compile` to a nullable integral return type in a NativeAOT app | `AngouriBugException: IsNaN method expected for type System.Double`, which took the process down | the compiled function | | **Silent** | an app publishing with `PublishTrimmed` or NativeAOT | `AngouriMath.dll` was copied in whole, being unmarked | it is trimmed with the rest, since the assembly now declares `IsTrimmable` | +### A bound index is not a free variable + +`FreeVariables` knew about two binders — `Lambda` and the set builder — and about no others. A +summation and a product bind their index, so `sum(k, k, 1, n)` is a function of `n` alone, and a +definite integral binds its variable between its limits. Both reported the bound name as free. + +Measured on a build of 2.3.0 and a build of this branch: + +| input | 2.3.0 | now | +|---|---|---| +| `sum(k, k, 1, n)` | `{ k, n }` | `{ n }` | +| `product(k, k, 1, n)` | `{ k, n }` | `{ n }` | +| `integral(t * b, t, 0, 1)` | `{ b, t }` | `{ b }` | +| `integral(t * b, t)` | `{ b, t }` | `{ b, t }` | +| `derivative(t * b, t)` | `{ b, t }` | `{ b, t }` | +| `lambda(x, x + y)` | `{ y }` | `{ y }` | +| `{ k : k > a }` | `{ a }` | `{ a }` | + +The index is bound over the **bounds** as well as the body, which is what +[`Binding`](Sources/AngouriMath/Core/Binding.cs) already says of itself: the name a binder is handed +is honoured throughout it, through the summand and the bounds. So `sum(k, k, k, n)` is `{ n }` too. + +**The last three rows are unchanged on purpose, and the distinction is the interesting part.** An +indefinite integral does not bind: the antiderivative of `t * b` over `t` is `b * t ^ 2 / 2 + C`, +which is still a function of `t`. Neither does a derivative — `d/dt` denotes a function of `t`. They +look like the same shape as a summation and are not, and a later sweep that completes the binder list +by adding them would make them wrong. `FreeVariablesTest` pins all of it, including the two that must +stay put. + +**`Vars` and `VarsAndConsts` do not change.** They mean every name *occurring*, bound ones included — +`"sum(k, k, 1, n)".ToEntity().Vars` is still `{ k, n }` — which is what their own XML example has +always documented, listing a lambda's parameter under *variables and constants*. Occurring and free +are different questions and the three properties answer them separately. + +[#1019](https://github.com/asc-community/AngouriMath/issues/1019). + ### A polynomial inequality of degree three or more is answered **Was** — every univariate polynomial inequality above degree two was refused outright, whatever its diff --git a/Sources/AngouriMath/Core/Entity/Entity.Definition.cs b/Sources/AngouriMath/Core/Entity/Entity.Definition.cs index c741c2fd3..2eb8037af 100644 --- a/Sources/AngouriMath/Core/Entity/Entity.Definition.cs +++ b/Sources/AngouriMath/Core/Entity/Entity.Definition.cs @@ -616,6 +616,22 @@ public IReadOnlyList Vars // https://github.com/asc-community/AngouriMath/issues/989 Set.ConditionalSet(var bound, var predicate) => predicate.FreeVariables.Where(v => !bound.VarsAndConsts.Contains(v)).ToList(), + // A summation and a product bind their index, so sum(k, k, 1, n) is a + // function of n alone. The index is bound over the bounds as well as the + // summand, which is what Binding says of itself: the name a binder is + // handed is honoured throughout it, through the summand and the bounds. + // https://github.com/asc-community/AngouriMath/issues/1019 + Summationf(var body, var index, var from, var to) + => BoundBy(index, body, from, to), + Productf(var body, var index, var from, var to) + => BoundBy(index, body, from, to), + // An integral binds its variable only when it has limits to bind it + // between. The indefinite one does not: the antiderivative of t * b over + // t is b * t ^ 2 / 2 + C, which is still a function of t. Nor does a + // derivative -- d/dt denotes a function of t. Their variable stays free + // on purpose, and a sweep that "fixes" that makes them wrong. + Integralf { Range: { } limits } integral + => BoundBy(integral.Var, integral.Expression, limits.from, limits.to), _ => new HashSet(@this.DirectChildren.SelectMany(c => c.FreeVariables)) } , @@ -623,6 +639,23 @@ public IReadOnlyList Vars ); private LazyPropertyA> freeVariables; + /// + /// The free variables of taken together, less whatever + /// binds. is an + /// rather than a because a binder's name position accepts one and + /// the parser is what settles which name it is. + /// + private static IReadOnlyCollection BoundBy(Entity binder, params Entity[] parts) + { + var bound = binder.VarsAndConsts; + var free = new HashSet(); + foreach (var part in parts) + foreach (var v in part.FreeVariables) + if (!bound.Contains(v)) + free.Add(v); + return free; + } + /// Checks if is a subnode inside this tree. /// Optimized for . /// diff --git a/Sources/Tests/UnitTests/Common/FreeVariablesTest.cs b/Sources/Tests/UnitTests/Common/FreeVariablesTest.cs index d3a9b65be..2c64f42bd 100644 --- a/Sources/Tests/UnitTests/Common/FreeVariablesTest.cs +++ b/Sources/Tests/UnitTests/Common/FreeVariablesTest.cs @@ -115,5 +115,65 @@ public void TwoSetBuildersDifferingOnlyInTheBoundNameAreStillEqual() => Assert.Equal( Entity.Boolean.True, "{ x : x > 0 } = { y : y > 0 }".ToEntity().Simplify()); + + /// + /// A summation and a product bind their index: the value of sum(k, k, 1, n) depends on n + /// and not on any k outside it. + /// https://github.com/asc-community/AngouriMath/issues/1019 + /// + [Theory] + [InlineData("sum(k, k, 1, n)")] + [InlineData("product(k, k, 1, n)")] + [InlineData("sum(k * 2, k, 1, n)")] + public void ARangeBinderBindsItsIndex(string exprRaw) + => Assert.Equal(SeqVar("n"), exprRaw.ToEntity().FreeVariables); + + /// + /// The index is bound over the bounds as well as the body, which is what + /// says of itself. + /// + [Fact] + public void TheIndexIsBoundOverTheBoundsToo() + => Assert.Equal(SeqVar("n"), "sum(k, k, k, n)".ToEntity().FreeVariables); + + /// + /// A definite integral binds its variable between its limits. + /// + [Theory] + [InlineData("integral(t * b, t, 0, 1)")] + [InlineData("integral(t, t, 0, b)")] + public void ADefiniteIntegralBindsItsVariable(string exprRaw) + => Assert.Equal(SeqVar("b"), exprRaw.ToEntity().FreeVariables); + + /// + /// And the two that look like the same shape and are not. The antiderivative of + /// t * b over t is b * t ^ 2 / 2 + C, still a function of t; + /// d/dt denotes a function of t as well. Neither binds, and a sweep that + /// makes them bind makes them wrong. + /// + [Theory] + [InlineData("integral(t * b, t)")] + [InlineData("derivative(t * b, t)")] + public void AnIndefiniteIntegralAndADerivativeDoNotBind(string exprRaw) + => Assert.Equal( + SeqVar("b", "t").OrderBy(v => v.Name), + exprRaw.ToEntity().FreeVariables.OrderBy(v => v.Name)); + + /// + /// Binding the index does not hide it from , which means every + /// name occurring and says so. + /// + [Fact] + public void ABoundIndexStillOccurs() + => Assert.Equal( + SeqVar("k", "n").OrderBy(v => v.Name), + "sum(k, k, 1, n)".ToEntity().Vars.OrderBy(v => v.Name)); + + /// Only inside the binder that declares it. + [Fact] + public void AnIndexOutsideItsBinderIsStillFree() + => Assert.Equal( + SeqVar("k", "n").OrderBy(v => v.Name), + "sum(k, k, 1, n) + k".ToEntity().FreeVariables.OrderBy(v => v.Name)); } } \ No newline at end of file