Zulip Chat Archive

Stream: new members

Topic: (In)completeness of ring_exp


Kazuhiko Sakaguchi (Feb 10 2022 at 11:57):

Hello. It seems to me that mathlib's ring_exp is incomplete. For example, it does not solve the following goal.

example (a b c : int) (n : nat) : (a * (b + c)) ^ n = a ^ n * (b + c) ^ n :=
begin
ring_exp,
end

Is there any idea on how to fix this issue and guarantee completeness? I'm actually interested in reimplementing ring_exp in Coq (for MathComp) using computational reflection rather than fixing this issue in mathlib. Since I have to prove the correctness of the procedure in that scenario, it would be nice to have a complete procedure first (so that I don't have to fix the procedure and the proof again and again).

Reid Barton (Feb 10 2022 at 12:27):

I think this kind of question is quite subtle, e.g. https://en.wikipedia.org/wiki/Tarski%27s_high_school_algebra_problem

Rob Lewis (Feb 10 2022 at 14:32):

cc @Anne Baanen

Anne Baanen (Feb 10 2022 at 15:15):

Good catch! There's no real support for addition under an exponent, so it doesn't really surprise me something goes wrong here, but it should do better than this so let me see if I can fix it...

Anne Baanen (Feb 10 2022 at 15:27):

Aha, so it rewrites a * (b + c) to a * b + a * c and then gives up because there is no rule for (_ + _) ^ _.

Anne Baanen (Feb 10 2022 at 15:52):

I don't see an easy way to modify the current ring_exp procedure so it solves this goal. :frown:

Mario Carneiro (Feb 10 2022 at 16:49):

Is ring_exp intended to be a decision procedure? Is its range of applicability known?

Mario Carneiro (Feb 10 2022 at 16:50):

Like Reid says, an actual decision procedure for this grammar seems technically challenging at best and provably impossible at worst

Anne Baanen (Feb 11 2022 at 11:10):

It's a simplification procedure extending the language of rings to allow polynomial expressions in the exponents of (products of) variables.

Anne Baanen (Feb 11 2022 at 11:11):

So any additions appearing under an exponentiation will be handled best-effort (which is not very good as you just showed)

Kazuhiko Sakaguchi (Feb 14 2022 at 01:19):

In the case of Tarski's high school algebra problem, the Wikipedia article says that the source of incompleteness is the lack of the opposite operator. So it does not seem to directly apply to ring_exp. But indeed, "this problem is actually undecidable" is one of the answers I expected.
Anyway, thanks for the feedback. The way I see this problem is the rewriting rules are not confluent (modulo AC). So known facts or techniques in term rewriting may answer this question.

Reid Barton (Feb 14 2022 at 02:27):

That's true but if you allow - in the syntax then it becomes a bit unclear what the domain of the decision procedure should even be--after all you can't raise an element of a ring to a negative power.

Kazuhiko Sakaguchi (Feb 14 2022 at 02:40):

My understanding is that the syntax is multi sorted and an exponent must be a natural number. But then, what ring_exp accepts as an exponent is a semiring expression with exponents. Now I see the problem you pointed out.


Last updated: Dec 20 2023 at 11:08 UTC