ill formed expression?

[Qian Yun]

x1:=(y-sqrt(y^2))/(x-sqrt(x^2))
x2:=1/(y+sqrt(y^2))*(x+sqrt(x^2))
(x1=x2)$EXPR(INT)
x1-x2


So (x1=x2) was false before my recent commit 7af446cb,
afterwards it becomes true.

I think that is acceptable.

However (x1-x2) is not zero, before/after this commit.

That's caused by the '/' in 'reduc', common gcd factor
is removed from numerator on the first loop.

Shall we try to fix it?

Or reject it because it contains dependent algebraic kernels?

- Qian

[Waldek Hebisch]

Dependent kernels mean that we do not have a field, but basic
things should still work properly. More precisly, sqrt(x^2)
means extention by element s such that s^2 = x^2. This is
well defined and gives ring with zero divisors. For such
ring we may consider full ring of fractions, that is set
of fractions n/d such that d is not a zero divisor. x1
and x2 above are problematic because in both cases denominator
is a zero divisor. Both x1 and x2 make sense if we restrict
branches of square root so that denominators are non zero.
If we do that both for x1 and x2, then we get value zero
for both. So possible result of x1 = x2 could be

[true | x = -sqrt(x^2) and y = sqrt(y^2)]

and for x1 - x2

[0 | x = -sqrt(x^2) and y = sqrt(y^2)]

where I used '[a | b]' to denote that result a is valid under
condition b.

Without conditional expressions (which we do not have ATM) we
could try to reject x1 and x2. This is expensive but doable in
algebraic cases. But if we have logarithms and want to reason
about branches of logarithms, then problem in general is
undecidable (with conditional expressions we could return
problematic conditions to the user, without we need to decide).

Rejecting x1 and x2 is also problematic because we could create
package(s) which do something sensible about branches. If
x1 and x2 were rejected we could not create them as expressions
and pass to such a package, so we would need a new domain
allowing x1 and x2.

Currently probably handling of x1 and x2 does not matter too much,
as current Expression is not able to give sensible result for x1 = x2
or x1 - x2. But rejecting them is also rather unattractive.

--
Waldek Hebisch

[Ralf Hemmecke]

On 6/17/26 22:20, Waldek Hebisch wrote:
> On Wed, Jun 17, 2026 at 05:20:27PM +0800, Qian Yun wrote:
> [true | x = -sqrt(x^2) and y = sqrt(y^2)]
>
> and for x1 - x2
>
> [0 | x = -sqrt(x^2) and y = sqrt(y^2)]
>
> where I used '[a | b]' to denote that result a is valid under
> condition b.

Oh, that looks rather nice to me (apart from the (perhaps) problematic
computation of the conditions).

I wonder how such a type can be programmed and then connected to
Expression(X).

Programming a "conditional type" doesn't sound to complicated. It's and
expression together with another (logic) expression. I feel, however,
that computations with such values may become complicated.
Maybe it would be even enough to have such a type simply to hold values
together with conditions and no further operations except extracting
value and condition.

OK, but someone must work that out and program it, which is certainly
not me at the moment.

Ralf

[Qian Yun]

Thanks for the nice explanation.

Yes, it requires extra care for zero divisors.

In this case, the denominator of x1,x2 does not multiply
to zero, so we can get sensible result if we interpret
that the branch is chosen to avoid division by zero.

For 'reduc', the attached patch changes the evaluation
order: reduction over algebraic kernels first,
do the division at the end.

This will make (x1-x2) return 0, which make the system
a little bit more consistent.

- Qian

[Tim Daly]

The conditional expression idea was called "Provisos" in Axiom.

It could be multi-branched with list of [ condition | expression ]

terms. The idea was mentioned as a project goal in 2003-08.txt

There was extensive debate about the idea. Search the email thread

in the Axiom download, specifically in axiom/book which contains

almost all of the emails up to October 2020.

I tried to make it work but it raised more controversy than expected.

Tim

[Waldek Hebisch]

On Thu, Jun 18, 2026 at 07:12:21AM +0800, Qian Yun wrote:
> Thanks for the nice explanation.
>
> Yes, it requires extra care for zero divisors.
>
> In this case, the denominator of x1,x2 does not multiply
> to zero, so we can get sensible result if we interpret
> that the branch is chosen to avoid division by zero.
>
> For 'reduc', the attached patch changes the evaluation
> order: reduction over algebraic kernels first,
> do the division at the end.
>
> This will make (x1-x2) return 0, which make the system
> a little bit more consistent.

I think that you want to avoid evaluating num and den when
possible. Otherwise it looks OK.

OTOH it is not clear to me how much attention to give to
cases involving zero divisors. Without comprehensive
theory there is risk that better output for some cases
will cause worse output for other ones.


> diff --git a/src/algebra/expr.spad b/src/algebra/expr.spad
> index ed89a42f..cda9f4fa 100644
> --- a/src/algebra/expr.spad
> +++ b/src/algebra/expr.spad
> @@ -386,13 +386,20 @@ Expression(R : Comparable) : Exports == Implementation where
> operator(name op, n@NonNegativeInteger)
>
> reduc(x, l) ==
> + num := numer x
> + den := denom x
> + evaled := false
> for k in l repeat
> p := minPoly k
> - d := degree p
> - -- avoid division when possible
> - if degree(numer x, k) >= d or degree(denom x, k) >= d then
> - x := evl(numer x, k, p) /$Rep evl(denom x, k, p)
> - x
> + num1 := evl(num, k, p)
> + den1 := evl(den, k, p)
> + num := numer(num1)*denom(den1)
> + den := numer(den1)*denom(num1)
> + evaled := true
> + if evaled then
> + num /$Rep den
> + else
> + x
>
> evl0(p, k) ==
> numer univariate(p::Fraction(MP),


--
Waldek Hebisch