Polynomial equality constraints

Google Group
1

I am just curious if grobner basis methods (e.g.
http://math.ucsd.edu/~ncalg/StrategyPaper/node60.html,
http://en.wikipedia.org/wiki/Gröbner_basis#Solving_equations) would be
a useful method for solving some of the non-linear constraints
(specifically, polynomial system of equations) found in ATS, in addition to
the currently used Fourier Motzkin elimination method. These algorithms
are analogous to Quine–McCluskey, but for a more class of algebras than the
boolean algebra. At the least, it should give an easy method to test to see
if the constraints as given are not solvable (i.e. the ideal of constraints
contains 1, that is, and equation asserting 1==0). Perhaps a printout of
constraints could help show the programmer any remaining relations that
must be proven.

Note: I’m not even to the point where I am familiar with the proof solving
capabilities in ATS, though I have read the chapters in the book (I really
need practice for it to sink in), so I am not very familiar with what kind
of errors one will always get during failed proofs.

There are some quite stable, fast, and open source packages for working
easily with these algebraic tools like Macualay2. I believe, though it is
compiled with C, it has its own internal “type-safe” language (don’t know
the details) that much of it is written in - not unlike ATS in this small
regard. However, iirc, that may be just the language interpreter, etc. The
core algorithms may still be written in C or C++. The point I’m trying to
make is that despite this, there are likely not too many bugs in the core
algorithms due to careful planning and long testing.

I believe the methods are not currently well-equipped to deal with
inequalities, though it seems like there may be some ongoing interest in
the area. I confess I’m not an expert in these methods, but I had an
applied interest in them in the past, and wouldn’t mind looking in to them
again someday (if potentially useful). So, given the current lack of
support with inequalities, I suppose it is possible that the payoff may not
be worth the effort.

2

You’re right, but I wanted to look in to it a bit more before having a
serious discussion on it. Also, I need to get to the point where I use the
proof system some in ATS.

As for constraint solving, well, I know very little either about its use in
programming languages - I was exposed to grobner bases in an
undergrad-level math class I took, and did a little additional reading on
them.

There is a good intro book available online (if you’re behind the paywall)
on these topics, which we used in class:

3

Brandon,

This is very interesting. Could you raise this question on the mailing
list? I think it would probably be a better place to discuss that.

(I never had any interest in constraint solving, so all of this is way over
my head. So, don’t expect any input from me. :))

4

Here’s a somewhat related example
http://www.stanford.edu/~danlass/esslli2011stus/petrovic.pdfusing Isabellahttp://www.cl.cam.ac.uk/research/hvg/Isabelle/overview.html,
which has a functional programming language.

5

Regarding inequalities, it may not be always be of interest to determine
the exact value of a constraint variable (only if it is bounded above or
below). Say the termination variable is x (it could be a polynomial as well
instead of a single variable). Then you can maximize and minimize the
objective function f(x)=x subject to all polynomial constraints using thelagrange multipliers with GBshttp://grobner.nuigalway.ie/grobner/hints.html.
If the GB ideal is found to contain 1, then the constraints cannot be
solved … more work on the proof is needed.

It may be possible to explicitly test for unboundedness using projective
varietieshttp://www.mathematik.uni-kl.de/~gathmann/class/alggeom-2002/chapter-3.pdf,
but I’d definitely have to think about that more since I never studied
these much. And of course, there may be simpler or better methods to do
this, I have no idea.