FreeVariables leaks a set builder's %1 placeholder, and only a lambda counts as a binder

[Rafael-SOWNet]

Measured on master at 4ee698da.

1. A set builder leaks its internal placeholder

"{ k : k > 0 }".ToEntity().FreeVariables      // { %1 }

%1 is the fresh name ConditionalSet.InitDirectChildren invents so that the set's variable is not confused with a variable of the same name outside it. It is not in the expression the caller wrote, it cannot be typed, and Variable.CreateTemp will invent a different one for a different predicate — so this is neither the bound name nor a stable answer. FreeVariables recurses through DirectChildren and picks it up.

Whatever the definition of "free" is, this is not it.

2. Only a lambda is treated as a binder

"lambda(k, k)".ToEntity().FreeVariables       // { }        correct
"sum(k, k, 1, 3)".ToEntity().FreeVariables    // { k }
"integral(k, k)".ToEntity().FreeVariables     // { k }
"limit(k, k, 0)".ToEntity().FreeVariables     // { k }
"derivative(k, k)".ToEntity().FreeVariables   // { k }

The XML doc says so plainly — "We call a bound variable a variable which is a parameter of some outer lambda. Then, all other variables are free." — so this is a documented choice rather than an oversight, and I am not filing it as a bug so much as asking whether the choice still holds.

It reads oddly now for two reasons. sum(k, k, 1, 3) is 6: nothing about the answer depends on k, and a caller asking FreeVariables to find out what an expression depends on is told it depends on k. And #986 has just made "these are binders" explicit in the type system — CalculusOperator and ConditionalSet both bind Var, and that is now where the bound name is decided. Six binders exist and one of them is honoured here.

Vars has the same shape ("sum(k, k, 1, 3)".ToEntity().Vars is { k }), but Vars promises less: it is documented as the variables that occur, minus the named constants, and an occurrence is what it counts.

What I think

(1) is a defect on any definition and worth fixing on its own — the placeholder should not escape.

(2) is a design call. Extending "bound" to every binder makes FreeVariables mean what the name means, and it is a breaking change for anyone who reads it as "occurring variables" — which is what VarsAndConsts is for, so the migration exists. I would rather ask than assume; the property is public and old.

Found while restoring three probe cases (vars, freevars, varsconsts) and writing a one-line comment saying what each does. The comment was wrong, which is how the difference turned up.

[Rafael-SOWNet]

§1 is fixed in #1000 — and one sentence in this issue was wrong, in a way that would have halved the fix.

I wrote above that Vars "promises less: it is documented as the variables that occur, minus the named constants, and an occurrence is what it counts", and filed §1 against FreeVariables alone. Measuring it before fixing it showed that is not what is happening:

"{ k : k > 0 }".ToEntity().Vars            // { %1 }
"{ k : k > a }".ToEntity().VarsAndConsts   // { %1, a }

%1 does not occur either. The leak is one channel — DirectChildren — and Vars and VarsAndConsts both walk it, so Vars was not being lenient about occurrence, it was breaking its own promise in both directions at once: the name that occurs (k) was missing, and the name that does not (%1) was there. Fixing only the property I named here would have left the invented name in the more widely used one.

All three now answer for { k : ... } what they already answered for lambda(k, ...):

	lambda(k, k > a)	{ k : k > a } was	{ k : k > a } now
FreeVariables	{ a }	{ %1, a }	{ a }
Vars	{ k, a }	{ %1, a }	{ k, a }

Also worth recording, since the obvious fix is at the source and it is the wrong one: the rename in DirectChildren is load-bearing and #1000 does not touch it. It is what gives alpha-invariance to SortHash, EqualsImprecisely and pattern matching — { x : x > 0 } = { y : y > 0 } is True because of it, and there is now a test saying so. What made the narrow fix safe is that the two rewriting consumers never used it: ConditionalSet.Replace is func(New(Var, Predicate.Replace(func))) and ConditionalSet.Substitute does its own capture-avoiding rename, both working from Var and Predicate directly. Only the reporting properties ever saw %1.

§2 is untouched and this issue stays open for it. Whether sum, integral, limit and derivative should bind their variable in FreeVariables is still a design call I would rather have answered than assume — it is documented behaviour and a breaking change for anyone reading the property as "occurring variables".

[Rafael-SOWNet]

Re-measured on master at 6b93b401 (2.3.0), .NET 10. Part 1 is fixed; part 2 is untouched, and it is the half that was a question rather than a defect.

1. The placeholder no longer escapes — fixed by #1000.

"{ k : k > 0 }".ToEntity().FreeVariables    // { }        was { %1 }
"{ k : k > 0 }".ToEntity().Vars             // { k }

2. Still only a lambda is treated as a binder. Every line of that block reproduces exactly as filed:

lambda(k, k)          FreeVariables = { }     correct
sum(k, k, 1, 3)       FreeVariables = { k }
integral(k, k)        FreeVariables = { k }
limit(k, k, 0)        FreeVariables = { k }
derivative(k, k)      FreeVariables = { k }

So the question this issue actually asked is still open, and it has got slightly sharper since: sum(k, k, 1, 3) evaluates to 6, and FreeVariables says that value depends on k.

Leaving this open for its second half. It is a breaking change to a public property that has been there a long time, the migration target already exists (VarsAndConsts is what "occurring variables" means), and #746 reserves a decision of this shape for a major — so it wants an answer rather than a patch. Retitling would be reasonable; I have not, since the title still describes what is left if you read past the first clause.

[Happypig375]

VarAndConsts is what it says: free variables and constants (pi and e). "Used variables" looks like another property.

[Rafael-SOWNet]

That settles it, and it makes the answer sharper than the question was — thank you.

Measured against your definition, on master at 6b93b401. The documented example on the property itself is Lambda(x, x * 2 + sin(y * pi)):

	today	free variables and constants
Vars	x, y	—
VarsAndConsts	x, y, pi	y, pi — x is bound by the lambda
FreeVariables	y	y

So VarsAndConsts is not what it says, and it is not a binder-coverage gap either: it is wrong for lambda, the one binder the library already honours in FreeVariables. The XML example pins the wrong answer.

That means my framing above was wrong in a way worth correcting rather than quietly dropping. I wrote that extending "bound" to every binder "is a breaking change for anyone who reads FreeVariables as occurring variables — which is what VarsAndConsts is for, so the migration exists." It does not exist. VarsAndConsts is not the home for "every name that occurs"; by your definition it is a second thing that also has to change, and "used variables" is a third property that does not exist yet.

So the shape is three properties moving together, not one:

• FreeVariables — extend "bound" from lambda to all six binders. Its doc comment still defines bound as "a parameter of some outer lambda", which was true when written and stopped being true when CalculusOperator and ConditionalSet gained a declared Var in Let a binder bind i, in every binder there is (#976) #986.
• VarsAndConsts — free variables and constants, per your definition.
• A new "used variables" — every name that occurs, bound ones included. That is exactly what Vars/VarsAndConsts do today, so no behaviour is lost; it gets a name that describes it.

Since two published properties change what they return, this is a major-version change rather than something to slip into a minor. I have put it on #1019, the pending-breakages docket you asked for on #1009, with the measurement above.

Part 1 of this issue — the %1 placeholder escaping — was a defect on any reading and is fixed (#1000). Leaving this open for part 2, which is now a decision that has been taken rather than one waiting to be.

[Rafael-SOWNet]

Re-measured on master at 69e40108 while sweeping the open issues before a release. Most of this
is done, and one part is left that is smaller and more specific than the issue describes.

	FreeVariables	Vars
{ k : k > 0 }	{ }	{ k }
lambda(k, k)	{ }	{ k }
sum(k, k, 1, 3)	{ }	{ k }
product(k, k, 1, 3)	{ }	{ k }
integral(k, k, 0, 1)	{ }	{ k }
integral(k * b, k, 0, 1)	{ b }	—
integral(k, k)	{ k }	{ k }
derivative(k, k)	{ k }	{ k }
limit(k, k, 0)	{ k }	{ k }

(1), the placeholder leak, is fixed — #1000. { k : k > 0 }.FreeVariables is { }.

(2) was answered — #1045. A summation, a product and a definite integral bind their
variable. An indefinite integral and a derivative deliberately do not, and that commit gives the
reason rather than leaving it implicit: 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. That
is the right call and I am not reopening it. Vars and VarsAndConsts are untouched, as
that issue asked.

What is left: limit

Limitf(Expression, Var, Destination, ApproachFrom) : CalculusOperator(Expression, Var) — the
same shape as Integralf and Derivativef — and it is not in the binder switch
#1045 added. That commit's message enumerates the indefinite integral and the derivative as
deliberate exclusions and does not mention limit at all, so this reads as an omission rather
than a decision.

And unlike those two, a limit does not have the property that justifies excluding them. An
antiderivative and a derivative are still functions of the variable; a limit never is —
lim_{k→0} k is 0, and no limit's value depends on the name it approaches along. So the
variable is consumed exactly as a summation index is.

One line in the same switch, next to Integralf. Happy to send it if that reading is right —
it is a behaviour change on a public property, so it wants the same BREAKING-CHANGES entry
#1045 got.

[Rafael-SOWNet]

Resolved on master at 5aad93d8. Both halves, measured:

	FreeVariables
{ k : k > 0 }	{ }
lambda(k, k)	{ }
sum(k, k, 1, 3)	{ }
product(k, k, 1, 3)	{ }
integral(k, k, 0, 1)	{ }
limit(k, k, 0)	{ }
limitleft(k, k, 0)	{ }
integral(k, k)	{ k } — on purpose
derivative(k, k)	{ k } — on purpose

• (1) the placeholder leak — Do not report a name the expression does not contain (#989) #1000.
• (2) the binders — A bound index is not a free variable (#1019) #1045 for the summation, the product and the definite integral;
  A limit binds the variable it approaches along (#989) #1091 for the limit, which that PR had missed.

The two that still report their variable do so deliberately, and the reason is what separates
them from the limit: an antiderivative of t * b over t is b * t ^ 2 / 2 + C and d/dt
denotes a function of t — both are still functions of the variable, while a limit never is.
lim(t, t, 0) is 0.

Vars and VarsAndConsts are untouched throughout, as this issue asked — they mean every name
occurring.

Leaving it to you to close, since (2) was posed here as a design question rather than a defect
report ("I would rather ask than assume; the property is public and old"). The answer that got
implemented is extend "bound" to every binder whose value cannot depend on the name, which is
narrower than "every binder" and is why the two above are excluded. If that is not the answer you
wanted, the place to say so is before a release goes out with it.

[Rafael-SOWNet]

Measured on master at 9d9b21e4, .NET 10, default settings. Both parts, on the issue's own inputs.

{ k : k > 0 }        -> {  }
lambda(k, k)         -> {  }
sum(k, k, 1, 3)      -> {  }
product(k, k, 1, 3)  -> {  }
integral(k, k, 0, 1) -> {  }
limit(k, k, 0)       -> {  }
integral(k, k)       -> { k }
derivative(k, k)     -> { k }

(1) is fixed. The %1 placeholder no longer escapes: the set builder answers { }, not { %1 }.

(2) is fixed, and the two remaining { k } are correct rather than left over. Every binder is honoured now. What separates the last two rows from the rest is not the node type but whether the variable is actually bound: integral(k, k) is an indefinite integral, so its value is a function of k — as is derivative(k, k). Add bounds and it binds, which is the integral(k, k, 0, 1) -> { } row. So FreeVariables means what the name means on every one of these.

Closing as fixed.