Lists Home |
Date Index |
Miles Sabin wrote:
> Of _course_ there are subsets of arithmetic which are decidable.
Now we're making progress. According to my limited research, first order
diophantine equations are decidable. Which is to say that it IS likely
possible to put a constraint of the form "height*width*depth=area".
> The first question relates to expressive power: make the restrictions
> too severe and it can be impossible or very difficult to say the things
> you want to say.
Of course. But business documents tend to use very simple equations. Add
up some numbers and multiply by the sales tax. I think that first order
equations do fall on the right side of the 80/20 rule.
> The second points to the fact that the 'finite' in 'finite decision
> procedure' can be very, very, very big indeed. Who cares if a decision
> procedure will terminate in finite time if we'll all be long dead
> before it's done? Practically speaking, the system might as well be
> undecidable: decidability != feasibility.
Of course. But I do not believe that solving linear equations in N
variables is computationally infeasible!
By the way, you accused me of using a paper to demonstrate something
that was contrary to the authors intent. I responded demonstrating that
I was saying the same thing he was. Do you now agree? I was not happy
with the implication that I would abuse someone's work to prove
something unrelated to what they were saying.