Provided simplification

In https://github.com/asc-community/AngouriMath/blob/master/Sources/AngouriMath/Docs/Usage/Comparison.md#2-the-same-task-put-to-both it is claimed that

All four rows where Math.NET is shorter are rows where this library attached a provided clause, which is the trade the table is really showing.

However, two of the differentiation results ln(x)/x -> (1 - ln(x)) / x ^ 2 provided not x = 0 and x^x -> (1 + ln(x)) * x ^ x provided not x = 0 should really be simplified further because (1 - ln(x)) / x ^ 2 is already undefined at x = 0 (division by 0) and (1 + ln(x)) * x ^ x is also undefined at x = 0 (0 to the power of 0), so this should really be further simplified.

Meanwhile how the notion of undefined (NaN) interacts with the proposed complex infinity (#217) should also need its investigation. Is this an issue of codomain?

Done in #1396: a provided whose condition the expression proves on its own is dropped from Simplify's answer — (1 − ln(x))/x^2 and (1 + ln(x)) x^x come back bare, since the quotient, the logarithm and the 0^0 are undefined at zero already. Proven structurally (a quotient by d, a negative power, a logarithm, d^f with f vanishing, for d the condition's expression, a power or a product holding it, or a polynomial that vanishes with it), never guessed, and only at the answer's top: inside a piecewise a predicate decides which case is taken, and inside the simplifier's search a provided is what rules read as "this candidate needs a condition" — dropping it there made x/sin(x) run for a minute where it declines in half a second.

On the two questions: the drop is sound whichever way "undefined" is read — NaN today, a complex infinity under #217 — because a provided says the expression has no value where the condition fails, and nothing changes where it has none anyway; the two notions differ in what the value at the point is called, which a condition never gave. And it is a question of the domain (where the expression is defined), not the codomain: the codomain setting picks the branch or the real form that is written (ln|x| against ln x), and a condition dropped or kept is the same statement under either. One consequence worth knowing: lim (x + sin x)/x at infinity is answered 1 now, because after the division the condition no longer stands between the descent and the squeeze theorem on sin(x)/x; two tests that pinned the decline pin the answer.

A condition the answer states on its own is no longer repeated beside…

Do we treat complex infinity as a proper replacement for NaN once v3 redesign drops EDecimal usage? Is complex infinity conceptually equal to "no value"? Are they even equivalent to begin with?

Not equivalent, and the difference lands on exactly this rule.

On the Riemann sphere 1/0 is a value — the point ∞̃, with a·∞̃ = ∞̃ for a ≠ 0, a + ∞̃ = ∞̃, 1/∞̃ = 0 — while 0/0, 0·∞̃, ∞̃ − ∞̃, ∞̃/∞̃ and 0^0 have no value there either. So complex infinity replaces "no value" for poles and only for poles; the indeterminate forms still need a distinct "undefined" (Mathematica keeps both, ComplexInfinity and Indeterminate; ln 0 is -∞ on the reals and ∞̃ on the sphere). It is not tied to EDecimal either: MathS.NaN today is a Real carrying EDecimal.NaN, which is a representation, and a v3 kernel needs a symbolic undefined whatever numeric type sits underneath — the same node whether it is spelled NaN or Indeterminate.

And I overstated the independence above. With today's semantics 1/x has no value at 0, so provided not x = 0 beside it says nothing new and #1396 drops it. Under #217, 1/x at 0 is ∞̃, so the same condition removes a value, and the quotient, negative-power and logarithm arms of #1396 would be dropping a genuine restriction. The 0^0 and x/x arms stay sound, since those are indeterminate on the sphere too. So the two have to be decided together, one of:

provided means "defined and finite": the drop stays, ∞̃ is a value the condition excludes by design, and Simplify's contract says so; or
provided means "has a value": the three pole arms go when Complex Infinity #217 lands, and 1/x provided not x = 0 is again a different expression from 1/x.

I would leave the rule as it is until #217 is decided, since today's answers are right under today's semantics, and note this trade on #217 so it is decided there rather than rediscovered. Do you have a preference between the two readings?

I think "has a value" is more semantically correct for what we are trying to do. We have both signed infinities from the extended real number line and the complex infinity from the Riemann sphere, they themselves get operated on like any real or complex number. For #217, the interaction between signed infinities and the complex infinity also needs its own specification - for example in the Wolfram language,

Infinity or ∞ is a symbol that represents a positive infinite quantity.

Use as iterator limit:
In[1]:=Sum[1/n^2, {n, Infinity}]
Out[1]=π^2/6
Do arithmetic with infinite quantities:
In[1]:=1/Infinity
Out[1]=0

DirectedInfinity[] represents an infinite numerical quantity whose direction in the complex plane is unknown.
DirectedInfinity[z] represents an infinite numerical quantity that is a positive real multiple of the complex number z.

Use as an expansion point and direction:
In[1]:=Series[ArcSin[z], {z, DirectedInfinity[I], 1}]
Out[1]=1/2 (π + i Log[4] - 2 i Log[1/z]) + (O[1/z])^2
Use as an integration limit:
In[1]:=Integrate[Exp[-x^2], {x, 0, DirectedInfinity[1 + I]}]
Out[1]=sqrt(π)/2
Use as a limiting point:
In[1]:=Limit[(x - 1)/(2x + 3), x->DirectedInfinity[]]
Out[1]=1/2

ComplexInfinity represents a quantity with infinite magnitude, but undetermined complex phase.

Division by 0:
In[1]:=1/0
Out[1]=ComplexInfinity
In[2]:=1/%
Out[2]=0

Indeterminate is a symbol that represents a numerical quantity whose magnitude cannot be determined.

Indeterminate is returned when a value cannot be unambiguously defined:
In[1]:=0/0
Out[1]=Indeterminate
Any numeric function of Indeterminate also gives Indeterminate:
In[1]:=Sin[Indeterminate]
Out[1]=Indeterminate

Missing[] represents data that is missing.
Missing["reason"] specifies a reason for the data's being missing.
Missing["reason", expr] associates the expression expr with the missing data.

When properties are missing, a Missing object is returned: 
In[1]:=ElementData[F, SoundSpeed]
Out[1]=Missing[NotAvailable]
In[2]:=ElementData[117, MeltingPoint]
Out[2]=Missing[NotAvailable]
Missing is generated when an association does not contain the specified key:
In[1]:=<|a->b, c->d|>[q]
Out[1]=Missing[KeyAbsent, q]
In[2]:=Lookup[<|1->a, 2->b, 3->c|>, d]
Out[2]=Missing[KeyAbsent, d]
Missing elements can be filtered out using DeleteCases: 
In[1]:=DeleteCases[ElementData[#, SoundSpeed]&/@ElementData[], _Missing]
Out[1]={1270. m/s, 970. m/s, 6000. m/s, 13000. m/s, 16200. m/s, 18350. m/s, 333.6 m/s, 317.5 m/s, 936. m/s, 3200. m/s, 4602. m/s, 5100. m/s, 2200. m/s, 206. m/s, 319. m/s, 2000. m/s, 3810. m/s, 4140. m/s, 4560. m/s, 5940. m/s, 5150. m/s, 4910. m/s, 4720. m/s, 4970. m/s, 3570. m/s, 3700. m/s, 2740. m/s, 5400. m/s, 3350. m/s, 1120. m/s, 1300. m/s, 3300. m/s, 3800. m/s, 3480. m/s, 6190. m/s, 5970. m/s, 4700. m/s, 3070. m/s, 2600. m/s, 2310. m/s, 1215. m/s, 2500. m/s, 3420. m/s, 2610. m/s, 1090. m/s, 1620. m/s, 2475. m/s, 2100. m/s, 2280. m/s, 2330. m/s, 2130. m/s, 2680. m/s, 2620. m/s, 2710. m/s, 2760. m/s, 2830. m/s, 1590. m/s, 3010. m/s, 3400. m/s, 5174. m/s, 4700. m/s, 4940. m/s, 4825. m/s, 2680. m/s, 1740. m/s, 1407. m/s, 818. m/s, 1260. m/s, 1790. m/s, 2490. m/s, 3155. m/s, 2260. m/s}

None is a setting used for certain options.

For ContourPlot, use None to only show the contour lines:
In[1]:=ContourPlot[Sin[x y], {x, -1, 1}, {y, -1, 1}, ContourShading->None]
Out[1]=
Plot only mesh lines:
In[1]:=ParametricPlot3D[{Cos[x] Cos[y], Cos[x] Sin[y], Sin[x]}, {x, 0, Pi}, {y, 0, Pi}, PlotStyle->None]
Out[1]=
Use None to indicate holes or no content for mesh regions: 
In[1]:=Plot3D[Sin[x y], {x, 0, 3}, {y, 0, 3}, Mesh->8, MeshShading->{{Orange, None}, {None, Blue}}]
Out[1]=

Nothing represents an element of a list that will automatically be removed.
Nothing[...] gives Nothing.

Any occurrence of Nothing is automatically removed in a list:
In[1]:={a, b, Nothing, c, d, Nothing}
Out[1]={a, b, c, d}
Replace an element of a list with Nothing to remove it:
In[1]:={a, b, c, d}/.c->Nothing
Out[1]={a, b, d}

Null is a symbol used to indicate the absence of an expression or a result. When it appears as a complete output expression, no output is printed.

When a sequence of commands ends with a semicolon, no output is shown:
In[1]:=null = (a=1 + 2;b=a + 3;)
The full form of the output is Null:
In[2]:=FullForm[null]
Out[2]=Null
If you forget a semicolon in a program you may see output with Null in it:
In[1]:=f[x_]:=Module[{y = x}, While[y > 2, y=Sqrt[y]]
y
]
In[2]:=f[100.]
Out[2]=1.77828 Null
This is because the whitespace is interpreted as multiplication. Redefine with a semicolon:
In[3]:=f[x_]:=Module[{y = x}, While[y > 2, y=Sqrt[y]];
y
]
In[4]:=f[100.]
Out[4]=1.77828

while each of these values have their own nuances, not all of them are about mathematics. Yet, they coexist in the Wolfram Language and we should consider how we want to structure the concepts of infinity and undefined around.

Then the consequence for #1396, stated so you can decide it: under "has a value" only the indeterminate forms make an expression undefined at a point, so of the shapes the rule reads, d^f with f vanishing too (0^0) and a factor that cancels (x/x) stay, and a quotient by d, a negative power of d and a logarithm of d go — 1/x and ln x at 0 are ∞̃ and -∞, values both. That reverses the first example of this issue: (1 - ln(x))/x^2 provided not x = 0 is right to keep its condition, since the quotient has the value ∞̃ at zero and the condition removes it, while (1 + ln(x)) x^x still drops it, 0^0 being indeterminate on the sphere as well.

I would narrow the rule now rather than when #217 lands: it is a day old, nothing builds on it, and the semantics of provided should be decided once — narrowing later would be a second BREAKING-CHANGES entry undoing part of the first. If you agree I will cut it to the two indeterminate arms and record the reading ("a provided says where the expression has a value; a pole is a value") in the simplification contract, so the next rule does not have to rediscover it.

On the taxonomy, I read Wolfram's list as two layers. Mathematical values: ±∞ (the ends of the real line, already here as +oo/-oo), DirectedInfinity[z] generalising them to a direction in the plane, ComplexInfinity as the one point of the sphere with no direction, and Indeterminate as the absence of a value — the only one of the four that is not a value, and what NaN stands for today. Everything else — Missing, None, Nothing, Null — is about data and API shape, not about numbers, and belongs to the library's surface (an empty set, an optional result) rather than to Entity. The relations that need specifying are the arithmetic between the four: ∞ + ∞̃, DirectedInfinity[i] · DirectedInfinity[1], 0 · ∞̃, and which of them each function maps to. That is #217's specification, and the v3 pass is the place to write it, since it touches every evaluation arm.

Seems right. It may surprise some people that an expression that produces 1/0 at some point is considered to have a value but will be undifferentiable on that point (thus needing "provided"), so the website should reflect this behavior somewhere.

Also #217 needs to find the notation for "directed infinity", and whether we need a different codomain to disallow infinities, because signed infinities are really the extended real number line and not real numbers. The default should still allow all infinities.

So maybe if the codomain is limited to complex numbers properly, this provided clause would drop, because we will no longer have infinities to use.

And if the codomain is further restricted to reals or integers, more provided clauses should drop too.

Done as #1402: the rule now reads 0^0 and 0/0 only, (1 - ln(x))/x^2 keeps its condition again, x^x's derivative stays bare, and the reading is written into the Providedf section of SimplificationContract.md with your codomain point as the caveat — under a codomain that admits no infinities the pole half changes, and today's all admit them. For the website: the pages come from the repository wiki, so the Simplification page gains a section on provided with the three examples run on that build (x/x, and the derivatives of x^x and ln(x)/x); it goes up once #1402 merges, since the wiki has no branches.

As commented above, it's about codomains rather than just the zeroes. Under a codomain without infinities, provided clauses that would check against infinities should be omitted, so it's really validating "under the codomain". This may need a proper codomain separation of real vs extended reals vs complex vs extended complex first.

Then I had the mechanism wrong in #1402 and the reading right: the rule should not hard-code which shapes are undefined, it should ask the codomain what the node is worth at the excluded point. Reworking #1402 that way:

a quotient by d, a negative power of d, a logarithm of d — each is checked by evaluating its singular value, 1/0, 0^(-1), ln 0, and the condition is redundant exactly when that value is not one the ambient codomain admits: NaN, or an infinity under a codomain without them;
0^0 and 0/0 are redundant on any reading and stay structural.

Measured today: 1/0 and 0^(-1) are NaN in every codomain, so (1 - ln(x))/x^2 and x^n n/x lose their condition, as #1396 had it and as this issue asked; ln 0 is -oo, which CC and RR admit (+oo in CC is True), so ln(x) provided not x = 0 keeps its condition — the one row that changes from #1396. When #217 gives 1/0 a value the quotient's condition stays by itself, with no change to the rule, and a codomain that excludes infinities drops all three, which is your "validating under the codomain". I will push that to #1402 and rewrite the contract paragraph the same way.

Like, is the contained expression's domain condition (under the given codomain) not enough here? The domain condition should really express what values it accepts under the given codomain.

And have you updated #217 with the context above?

It is enough, and it is the right tool — I was rebuilding it. DomainConditionIn(codomain) already says what each node accepts under the reading it is asked in (a nonzero divisor; a nonzero base or a positive exponent; a nonzero antilogarithm over CC, a positive one over RR; cos ≠ 0 for a tangent), so the rule becomes one line: a provided not e = 0 is redundant where the answer's own domain condition, read in the ambient codomain, already excludes the zeros of e — a conjunct not d = 0 or d > 0 with d vanishing there, or a disjunction every side of which does (x^x's not x = 0 or x > 0). No shapes in the rule, and #217 changes nothing here: when a quotient's domain condition under a codomain with a complex infinity stops excluding zero, the condition beside 1/x stops being redundant by itself.

What that gives today is #1396's answers, the logarithm included, since ln's domain condition over CC excludes zero — that is the library's own statement that ln 0 is a limit and not a value, and the rule now defers to it rather than to my evaluation of ln 0. Plus the shapes the hard-coded list missed: tan(x) provided not cos(x) = 0 and sin(x)/x provided not x = 0 drop too. Reworking #1402 to that now.

On #217: the note is there (#217 (comment)); I will add the codomain point from this thread — that which codomains admit the complex infinity is what decides a quotient's domain condition at zero, and so what provided means beside it.

Simplify drops a condition the answer's own domain condition states, …

Pushed to #1402 (c041138): the rule asks the answer's own DomainConditionIn(MathS.Settings.Codomain) and nothing else; #1396's answers stand, tan(x) provided not cos(x) = 0 and sin(x)/x provided not x = 0 drop theirs too, and the contract, the comparison page and the BREAKING-CHANGES entry describe the mechanism rather than a list. The #217 note has the codomain point.

Simplify drops a condition the answer's own domain condition states, …

#1402 is merged and the wiki's Simplification page has the provided section (https://github.com/asc-community/AngouriMath/wiki/Simplification#conditions-on-the-answer-provided), which the site mirrors. Leaving this open in case you want it to track #217's half; otherwise it can close.

#1402 says that this expression "x/x provided not x = 0" is unchanged. But it doesn't seem right - it seems as if the division already tells that the denominator should not be 0.

If everything relevant in this issue to #217 is already put to #217 then this issue can close.

On that row: x/x provided not x = 0 simplifies to 1 provided not x = 0 — the same as x/x alone — and "unchanged" in the table meant the condition stays, not that the quotient does. The division does say the denominator is not zero, and that is exactly why the condition has to survive the rewrite: once x/x has become 1, the answer no longer says it, and 1 without the clause would have a value at zero that x/x never had. The rule reads the answer's domain condition, after simplification, and 1's says nothing — so 1/x provided not x = 0 loses its clause (the answer 1/x still states it) while x/x provided not x = 0 keeps it (the answer 1 does not). That is the contract's own example, x/x -> 1 provided not x = 0, from the other side.

Everything from here that bears on #217 is on #217 (the codomain point and the ln 0 = -oo pair), so closing.

Navigation Menu

Repository navigation

Provided simplification #1394

Metadata

Assignees

Labels

Type

Projects

Milestone

Relationships

Development

Provided simplification #1394

Description

Activity

Rafael-SOWNet commented on Sep 17, 2026

Happypig375 commented on Sep 17, 2026

Rafael-SOWNet commented on Sep 17, 2026

Happypig375 commented on Sep 17, 2026

Rafael-SOWNet commented on Sep 17, 2026

Happypig375 commented on Sep 17, 2026

Rafael-SOWNet commented on Sep 17, 2026

Happypig375 commented on Sep 17, 2026

Rafael-SOWNet commented on Sep 17, 2026

Happypig375 commented on Sep 17, 2026

Rafael-SOWNet commented on Sep 17, 2026

Rafael-SOWNet commented on Sep 17, 2026

Rafael-SOWNet commented on Sep 17, 2026

Happypig375 commented on Sep 17, 2026

Rafael-SOWNet commented on Sep 17, 2026

Metadata

Metadata

Assignees

Labels

Type

Projects

Milestone

Relationships

Development

Issue actions