Project

General

Profile

Bug #821

IsTermOrdering

Added by John Abbott over 8 years ago. Updated about 8 years ago.

Status:
Closed
Priority:
Normal
Assignee:
John Abbott
Category:
Tidying
Target version:
CoCoALib-0.99540 Feb 2016
Start date:
25 Nov 2015
Due date:
% Done:

100%

Estimated time:
Spent time:
0.85 h

Description

MatrixForOrdering offers a fn called IsTermOrdering.
The doc says its tests whether the matrix defines a term ordering.
The code simply checks that the first non-zero element in each column is positive; it does not check that the matrix has rank equal to the number of columns. It really tests whether the matrix could be completed into another one which defines a term ordering.

Which is right? The doc or the code?
Decide, and fix which ever needs fixing.

History

#1 Updated by John Abbott over 8 years ago

These matrices for ordering really seem to be a minefield :-(

Who uses NewIntegerOrdMat?

Unfortunately I need to sort this stuff out before I can check in :-(

#2 Updated by John Abbott over 8 years ago

  • Status changed from New to In Progress
  • % Done changed from 0 to 10

Following the principle of "no nasty surprises", I think that IsTermOrdering should do a complete check (incl. correct rank).

If at some point we need a faster version which skips the rank check then that can be done either by a function with a different name, or by this function with an extra arg SkipRankCheck.

Maybe I'll check to see who calls it, to see whether the faster version is already needed.

#3 Updated by John Abbott over 8 years ago

  • Assignee set to John Abbott

Does the 0x0 matrix define a term-ordering?
Do we want to allow users to make a term-ordering on 0 indets?

JAA thinks it should probably be an error -- is there any circumstance where it could be useful to have a term-ordering on 0 indets?

NOTE the PPOrdCtor placeholders call NewLexOrdering etc., and these all throw if the number of indets is not strictly positive.

#4 Updated by Anna Maria Bigatti over 8 years ago

John Abbott wrote:

Does the 0x0 matrix define a term-ordering?
Do we want to allow users to make a term-ordering on 0 indets?

JAA thinks it should probably be an error -- is there any circumstance where it could be useful to have a term-ordering on 0 indets?

NOTE the PPOrdCtor placeholders call NewLexOrdering etc., and these all throw if the number of indets is not strictly positive.

Error! error! (we give error also for PolyRing with no indets)

#5 Updated by John Abbott about 8 years ago

Have we finished this issue? If I recall well, we made some progress, but I no longer recall whether we actually finished.

If finished, we should close. Otherwise we must change the Target Version (to which?)

#6 Updated by Anna Maria Bigatti about 8 years ago

  • Status changed from In Progress to Closed
  • % Done changed from 10 to 100

Also available in: Atom PDF