Solve Thue equations

[Bodigrim]

Develop a routine to solve Thue equations.

https://en.wikipedia.org/wiki/Thue_equation
https://www.sciencedirect.com/science/article/pii/0022314X89900140?via%3Dihub

[MathiasBartl]

A Thue equation would be a polynomial of the form ax^3 + bx^2y + cxy^2 + dy^3 = e
or similarly of a larger degree, where a,b,c,d,e are rational numbers, and which is irreducible over the rational numbers?

[Bodigrim]

Yep, exactly.

[CarlEdman]

Cool and definitely doable considering that several packages already do it.

But can anybody explain why this theorem is stated in terms of rational numbers, rather than integers? The solutions offered by the algorithm are integers. The parameters are trivially reduced to integers unless I am missing something. So just state the problem and the solution in terms of integers and have a separate trivial function to convert from rationals if users want to compose that.

So I'd propose a Haskell function of the type signature thue :: Integer -> [Integer] -> [(Integer, Integer)] where the first parameter is the e and the second parameter is [a, b, c, d, ...] with the degree implicit in the length of the list. The result is a list of pairs (x, y). Ideally, if the algorithm permits without significant loss of efficiency, the result list would have some ordering property and/or be lazy.

Sound good?

[CarlEdman]

Separate question: What is a good specification if the algorithm detects that the bivariate form is reducible? Unless my quick thought misleads me, that just means that the set of solutions is also separable as a product set of the solutions to the individual solutions of the factors of the bivariate form. In that case, it would seem straightforward to produce a full set of solutions based on the potential factorisations of e. So a good implementation would just drop the restriction and give the full set of solutions, rather than raising an exception, returning a Maybe, or just silently failing.

PS: Forgive me if all of the above is nonsense. This is my first time thinking about Thue equations (though not about Diophantine equations or arithmoi).

[MathiasBartl]

There are two definitions of Thue Equation, one for rational numbers and one for integers, see
https://mathworld.wolfram.com/ThueEquation.html and https://en.wikipedia.org/wiki/Thue_equation

If you look at the rational case: take a Thue equation with rational factors that is irreducible over the rational numbers, and then multiply with the LCM of the factors denominators you will get a Thue equation over the integers. It will be irreducible over the integers, which I think I should be able to prove. And the solutions of both equations in R and Z respectively can be mapped on each other.

In short irreducibility over integers or fractions is pretty much equivalent.

[CarlEdman]

Thanks, @MathiasBartl! That is what I thought.

To clarify my second point: Assume that our bivariate form is reducible to two irreducible forms (the general cases is left as an exercise to the author): f(x,y) = g(x,y) h(x,y) (And I'll use the integral formulation for simplicity).

Then there must exist integers s and t so that r = s t and g(x,y) = s and h(x,y) = t. Given s and t, the latter problems can be solved by the algorithm for irreducible forms. All the candidates for s and t can be found by divisorPairs r.

So to solve the problem for a reducible form, just use the algorithm for the irreducible form on candidate pairs and find the intersection of solutions for each pair. The solution for the generalized problem which does not require irreducibility is just the conjunction of the solutions for all candidate pairs.

I like general functions which give correct answers in all cases that there is one that can be found, rather than throwing exceptions, making unchecked assumptions, returning Maybes or the like. When possible without too much trouble.

[Bodigrim]

@CarlEdman I agree with both your points.

I think that working with rational coefficients is probably simpler from the theoretical viewpoint, but we may just as well (and IMHO preferably) use Integer for API.

Certainly, it would be nice to make an attempt to factorise a polynomial, but this is a difficult problem itself and the topic of #175. So while I do not like unchecked assumptions, I would accept a PR which relies on irreducibility.

[MathiasBartl]

According to the PARI/GP documentation "Reducible polynomials are in fact much easier to handle".

[MathiasBartl]

@CarlEdman I'd curry it the other way around: Polynomial -> Integer -> List of Solutions

[MathiasBartl]

So I was thinking of doing the test cases using Quickcheck, but first one could use Liquid Haskell to specify the correctness properties of the function.

1. Every output pair is in fact a solution of the equation.

This is fairly straightforward to specify and can be tested easily: Generate a large number of Thue equations.

2. Forall x,y in Z : x,y solve the equation => they are in the returnvalues
   I haven't looked into Liquid Haskell too much, but I assume that it is expressive enough for this.
   Testing this property is seemingly less straightforward but it can be done by Quickcheck by massivly shaving down random inputs, respectively finding solutions to the equation by brute force.

So basically: Generate Thue equations, and for each equation generate by random/brute force solutions.
The alternative is to generate a Thue equation from a given set of solutions.

3. The results are unique.
   This is simply requiring the output to be well formed

4. The number of results.
   The output list should be of finite length.
   This is a property of Thue equations and is actually included in conditions 1&2
   Both 3&4 are fairly easily testable.

Now If we have 1,2,3 specified I think we could actually input them into the Synquid code generator,
and see if it is powerful enough to find a solution.

Other than that testing would include, checking the results against a small number of Thue equations gleaned from literature, wiki etc.
Writing a wrapper around an existing implementation and use Quick check to compare results;
and as well do comparative performance measurements.

Lastly an analysis of algorithmic complexity in O notation.

[Bodigrim]

1. I have not been following the evolution of Liquid Haskell, but I don't think that these invariants are easily expressible.
2. Even if Sinquid (or other code generator) would be applicable, it will most certainly just generate a brute force algorithm. Because it is the shortest one and it satisfies all invariants.

[CarlEdman]

I am not familiar with Synquid and only slightly with Liquid Haskell. But thinking in terms of QuickCheck , you could do the following:

Don't generate the Thue equation by randomly picking parameters. Instead randomly pick the solutions and then generate the parameters from that, give those to the library function, and then check the solutions against your known set!

The part I have not yet figured out is how to pick the solutions for the full problem. It is pretty easy to do for linear bivariate forms a x + b y = r (use Bézout's identity) and you can generate higher forms with known solutions by just multiplying any number of linear bivariate forms together (taking care to either deal with or avoid the creation of additional solutions in the product).

The problem is that (a) this only applies to the part of the solution space for reducible forms, which we may or may not deal with, and (b) it doesn't cover irreducible forms of higher degree. I need to think about how hard it is to generate irreducible bivariate forms of higher degree with a given solution. Maybe you can generate them as product, as you definitely can over algebraic numbers by the fundamental theorem of algebra, but irreducible over the integers. More thought needed.

[Bodigrim]

We can probably use PARI/GP as a reference and generate some unit tests.

[MathiasBartl]

Regarding property No.1: for a Thue equation of degree d=3 I believe it can be expressed such as:

{-@ thue :: a : Int -> b : Int -> c : Int -> d : Int -> e : Int -> { x, y : (Int,Int) | a * x ^3 + b *x^2 * y + c * x * y^2 + d * y^3 = e } @-}

I believe one can put any Haskell expression of boolean type into this type signature. Not that this only checks on result, checking a list of results should just be a simple case for map reduce.

We need an auxilary function, that for any Thue equation and Integers x,y determines if these are solution. This is actually pretty straightforward, and furthermore because Thue equations are just Diophine equations, we can, if we derive the type from an exiting type use an existing function that operates on a wider class of polynominals.

Regarding property No.2 I would think that there is an upper limit L for the height of the solutions such that for all x,y: -L < x,y < L this is in fact a corrolary to saying that there are only fintely many solutions. If L can now determined for each solution and that determination is expressible in LH, then we can write No.2 by mapping over a finite set of Integers, which unlike an umlimited forall expression is actually testable. A test in this case would then work by brute force solving the problem, and as you said a code generator without any further input would then generate the brute force algorithm.

I am looking into this report: https://webusers.imj-prg.fr/~michel.waldschmidt/articles/pdf/ProcHRI2017ThueEquations.pdf

It has a discussion about upper bounds for

If we simplify things and assume again that d=3 and further that then we have an upper bound for x (more speciffically the bound for the absolut value of x) of:

|x| <= ((2|b| / min(|c -b|,|d-b|) ) +1) (e/a)^(1/3)

I should read this closer, because this bound does not seem to exist for certain equations, such as with c=b
For a given x then the upper bound of y can be determined as:

|b - x/y| <= (4 |e| / |y|^3 a |c -b| |d -b|)

Or something like that, I should read this closer, because this bound does not seem to exist for certain equations, such as with c=b

A couple of comments for research purposes:
A Thue-Mahler equation is similar to a Thue equation with some additional degrees of freedom.
The left hand side of a Thue equation is called an homogenous polynomial.

[Bodigrim]

I should read this closer, because this bound does not seem to exist for certain equations,

If you are quoting page 5, then this bound is conditional by y.