Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] Ordering of the complex numbers


view this post on Zulip Email Gateway (Aug 26 2021 at 20:57):

From: Dominique Unruh <unruh@ut.ee>
Dear all,

I wanted to raise the question of instantiating the complex numbers as a
partially ordered set. It came up when discussing the inclusion of a new
theory for infinite sums into the Isabelle/HOL standard library because
my current development relies on having such an instantiation.

The current situation in Isabelle/HOL is as follows:

The standard library has no instantiation "complex :: order".
Jordan_Normal_Form (JNF) on AFP instantiates "complex :: order" via the
definition "a <= b" iff "Re a <= Re b /\ Im a = Im b". I don't know
whether there are other libraries which instantiate "complex :: order",
but if there are, then it will be impossible to import both of them at
the same time (even if the definitions are compatible!)

Therefore I would suggest to incorporate the instantiation of "complex
:: order" into the standard library. I would advocate for using the same
definition as in JNF (or at least a logically equivalent one). I believe
this is the "right" ordering on complex numbers for the following reasons:

* It makes the complex numbers "almost" into a pre-ordered field. A
pre-ordered field is a field with a set of positive elements such
that the sum and the product of positive elements are positive, and
that squares are positive. (See e.g. Lam, Tsit-Yuen (2005).
Introduction to Quadratic Forms over Fields.) a <= b is then defined
by "b-a is positive". The complex numbers with the JNF-ordering are
a pre-ordered field if we mean by a "square" of /a/ the product of
/a/ with its complex conjugate. (An operation that is a natural
analogue to squaring over real. Compare for example with the
operation "adjoint(A)*A" for complex-valued matrices.) In
particular, we have the natural laws that "a<=b ==> a+c <= b+c" and
"a>=0 /\ b >= 0 ==> a*b >= 0".

* It coincides with the ordering of the real numbers (when we see the
reals as a subset of the complex numbers.)

* If we see complex numbers as 1x1-matrices, then this ordering will
coincide with the Loewner ordering on complex matrices. In
particular, a>=0 will mean that a is real and nonnegative, and
analogously for matrices, A>=0 is very common notation to mean that
A is Hermitian and positive semidefinite, which for 1x1 matrices
means real and nonnegative.

* In Conway, "A course in functional analysis", the notation "a>=0" is
used in the complex case to mean real and nonnegative. (Explanation
after Def. 1.1 in Chapter I.1.) The definition from JNF is, as far
as I can tell, the only natural definition that has this special
case. (Conway's book is the first and only that I checked. Not the
result of cherry-picking a book.)

* While other definitions of <= on complex numbers are definitely
possible (e.g., the lexicographic order), I cannot think of any that
comes even close to this one in mathematical naturalness. (Of
course, that is somewhat subjective.)

Of course, specific applications might work better with other
definitions (Manuel Eberl told me they used the lexicographic ordering
in one situation). But I can't think of any other definition that would
qualify as a potential candidate for the "standard definition". Then
basically we have two choices for the Isabelle/HOL standard library:
Include the JNF instantiation, or have no "complex :: order"
instantiation. I think the latter case would be worse because it means
that no user-developed theory can use any "complex :: order"
instantiation anyway without losing the ability to be imported at the
same time with other theories. So not defining the instantiation does
not give any additional freedom anyway, at least not to "well-behaved"
developments.

(Note also that any instantiation that is different from the JNF
instantiation will break JNF which is, afaik, one of the more widely
used AFP entries.)

I would like to hear everyone's opinion on this.

Best wishes,
Dominique.

view this post on Zulip Email Gateway (Aug 30 2021 at 17:47):

From: Wenda Li <wl302@cam.ac.uk>
Dear Dominique,

Then basically we have two choices for the Isabelle/HOL standard library: Include the JNF instantiation, or have no "complex :: order" instantiation. I think the latter case would be worse because it means that no user-developed theory can use any "complex :: order" instantiation anyway without losing the ability to be imported at the same time with other theories. So not defining the instantiation does not give any additional freedom anyway, at least not to "well-behaved" developments.

I agree with your proposal.

The only question I have is whether we should include this ordering in Complex_Main or as a separate theory file (say in HOL-Library) so that the user can have the freedom to exclude this ordering (assuming most of complex number users start with Complex_Main).

Cheers,
Wenda

view this post on Zulip Email Gateway (Aug 30 2021 at 18:19):

From: "John F. Hughes" <jfh@cs.brown.edu>
As a (semi)-practicing mathematician who sometimes works with complex
manifolds, I'd prefer to see it excluded from Complex_Main. If I happen to
use an order on the complexes in something I'm doing, it's almost certainly
a mistake, and I'd rather see that mistake get flagged than have some
not-at-all-natural-to-me order get used. (I've nothing against the proposed
order ... but I also see including it as a way to induce me to make stupid
mistakes, like assuming there's an order when I don't intend there to be,
while omitting it helps me avoid those mistakes. Dominique is probably
right that not defining it gives no additional freedom, but freedom (for me
at least) is not the only goal.

--John

view this post on Zulip Email Gateway (Aug 31 2021 at 10:29):

From: Lawrence Paulson <lp15@cam.ac.uk>
It should be separate, so that users have the choice whether to use this ordering, no ordering or possibly some other ordering. We already do this for lists (Library/List_Lenlexorder.thy vs Library/List_Lexorder.thy).

Larry

view this post on Zulip Email Gateway (Aug 31 2021 at 12:57):

From: Manuel Eberl <eberlm@in.tum.de>
I am a bit sceptical about such orphan instances. If two AFP authors
decide to import incompatible instances of such an order, that means
that no future entry can ever import both of these at the same time, and
there is no workaround for this.

I am generally not a big fan of this particular order instance of the
complex numbers for similar reasons as were already discussed, although
I think my opposition is more of a vague "philosophical" nature than
anything practical.

And yes, indeed, I recently had to use a very different ordering on them
(the lexicographic one) in my proof of the Lindemann–Weierstraß theorem.
I decided against introducing an orphan instance there and instead
simply interpreted the "order" locale.

The locale approach gives you almost everything that a class instance
does, except that the notation is not quite as convenient and that you
don't get the "order" sort, of course, so you cannot use constants that
require it.

So, in summary:
– "Pick-and-choose" orphan instances are, in my opinion, a ticking time
bomb and a bad idea.

– Non-canonical instances such as the one suggested in this thread are,
in my opinion, not a great idea, but I am not absolutely opposed to
it. However, if one goes down that path, one should at least have one
(and only one) official one. It can be made optional (i.e. an optional
import); we have some other similar "optional" instances, but that has
the disadvantage that it may lead to people rolling their own
"unofficial" instantiations after all.

Cheers,

Manuel
smime.p7s

view this post on Zulip Email Gateway (Sep 01 2021 at 06:41):

From: "YAMADA, Akihisa" <ayamada@trs.cm.is.nagoya-u.ac.jp>
Dear all,

in developing the JNF library, we respected and utilized the "a >= 0
<--> a is real nonnegative" convention indeed. I'd say there's no other
natural way to extend this to a >= b.

Nevertheless, I agree this should be separate from Complex_Main, as I
don't know there's enough merit in this ordering alone to convince
others. In JNF, the merit is observed only after having conjugate as a
class operation and introducing a class assuming "a * conjugate a >= 0"
(e.g. the almost preordered field Dominique mentions).

Best regards,
Akihisa


Last updated: Dec 08 2021 at 08:24 UTC