Email Gateway (Aug 22 2022 at 20:20): Email Gateway (Aug 22 2022 at 20:20):From: Dominique Unruh <unruh@ut.ee>
Thanks for the additional context. However, seeing as we do not have
complex vector spaces in Isabelle/HOL to begin with and "norm" in
Isabelle/HOL is, by definition, always the norm of a real vector space,
this is not really an issue.
As a side note: José and I are currently developing an Isabelle/HOL
library for complex functional analysis (as a planned AFP submission),
including complex vector spaces.
https://github.com/dominique-unruh/bounded-operators (Part of which
might perhaps be included in HOL-Analysis when it's ready?) So, while we
don't have complex vector spaces right now, John's argument might apply
once the library is ready.
Best wishes,
Dominique.
Manuel
On 05/08/2019 15:51, John F. Hughes wrote:
(Apologies -- I don't know how to respond to a particular item in the
mailing list).Manuel Eberl writes:
For unknown historic reasons, there is an abbreviation called "cmod"
(complex modulus) for the norm on complex numbers. I have always founds
that somewhat unnecessary and annoying. After talking to Larry Paulson
and Wenda Li about it, we have concluded that it would be best to get
rid of it entirely, i.e. to simply use "norm" for it.[...] Should anyone have good reasons why one should not do this, please
tell us.
In a normed vector space over the complex numbers (e.g., in C^n), there's a
norm for the vectors and there's a modulus function on the scalars. It's
true that in C^1, these coincide, but making the names identical in general
seems like deliberately inviting confusion. In particular, one of the
properties that the vector-norm should have is that ||cv|| = |c| ||v||;
using the proposed terminology, that would be stated "norm(cv) =
norm(c)norm(v)", where the two "norms" on the right-hand side indicate
distinct things.Sure, everyone working on complex normed spaces can probably handle this
particular mathematical "pun" without much effort, but it seems peculiar to
introduce it deliberately. Also, the word "modulus", used within, say, a
first course on complex variables (or even more advanced materials) has a
pretty long tradition; I don't think I can recall a complex-analyst saying
"norm" instead, although I haven't spent a lot of time hanging out with
complex analysts over my mathematical career.
Email Gateway (Aug 22 2022 at 20:21):From: Manuel Eberl <eberlm@in.tum.de>
That is good to know. However, "complex" will still be an instance of
"real_normed_vector". We cannot really get rid of "norm :: complex", we
can only "hide" it by an abbreviation (as it is done now).
I for one think that even in light of this new information, "cmod"
probably does more harm than good. The term "modulus (of a complex
number)" is definitely being used, but so is "norm (of a complex number)".
I still find "cmod" a lot more cryptic than "norm", and just for the
sake of uniformity it makes sense to just call it "norm".
Manuel
Email Gateway (Aug 22 2022 at 20:21):From: Lawrence Paulson <lp15@cam.ac.uk>
I agree in this case, and more generally, introducing an abbreviation that gives a completely different name to a function just because it has a particular type can be confusing.
A contrasting situation concerns the function indicator. The return type of this function is polymorphic, so we have the abbreviation
abbreviation indicat_real :: "'a set ⇒ 'a ⇒ real" where "indicat_real S ≡ indicator S”
to cover the common case where the return value should have type real. But if the user wasn’t expecting this, they at least have a decent chance of figuring out what is going on.
Larry
Email Gateway (Aug 22 2022 at 20:21):From: Manuel Eberl <eberlm@in.tum.de>
I never did like indicat_real (or understand why it exists).
On that note, functions with type variables in their return type that do
not occur in the argument types are a bit of a nightmare. "fact" is
another example, and I routinely stumble over that.
To make matters worse, I vaguely recall that I may have been the one who
made it that way. Perhaps the alternative (gratuitous coercions) is worse.
Manuel
Email Gateway (Aug 22 2022 at 20:24):From: Manuel Eberl <eberlm@in.tum.de>
For unknown historic reasons, there is an abbreviation called "cmod"
(complex modulus) for the norm on complex numbers. I have always founds
that somewhat unnecessary and annoying. After talking to Larry Paulson
and Wenda Li about it, we have concluded that it would be best to get
rid of it entirely, i.e. to simply use "norm" for it.
I just wanted to send out an email to notify people that we intend to do
this. Should anyone have good reasons why one should not do this, please
tell us.
Cheers,
Manuel
Email Gateway (Aug 22 2022 at 20:28):From: "John F. Hughes" <jfh@cs.brown.edu>
(Apologies -- I don't know how to respond to a particular item in the
mailing list).
Manuel Eberl writes:
For unknown historic reasons, there is an abbreviation called "cmod"
(complex modulus) for the norm on complex numbers. I have always founds
that somewhat unnecessary and annoying. After talking to Larry Paulson
and Wenda Li about it, we have concluded that it would be best to get
rid of it entirely, i.e. to simply use "norm" for it.
[...] Should anyone have good reasons why one should not do this, please
tell us.
In a normed vector space over the complex numbers (e.g., in C^n), there's a
norm for the vectors and there's a modulus function on the scalars. It's
true that in C^1, these coincide, but making the names identical in general
seems like deliberately inviting confusion. In particular, one of the
properties that the vector-norm should have is that ||cv|| = |c| ||v||;
using the proposed terminology, that would be stated "norm(cv) =
norm(c)norm(v)", where the two "norms" on the right-hand side indicate
distinct things.
Sure, everyone working on complex normed spaces can probably handle this
particular mathematical "pun" without much effort, but it seems peculiar to
introduce it deliberately. Also, the word "modulus", used within, say, a
first course on complex variables (or even more advanced materials) has a
pretty long tradition; I don't think I can recall a complex-analyst saying
"norm" instead, although I haven't spent a lot of time hanging out with
complex analysts over my mathematical career.
Email Gateway (Aug 22 2022 at 20:29):From: Manuel Eberl <eberlm@in.tum.de>
Thanks for the additional context. However, seeing as we do not have
complex vector spaces in Isabelle/HOL to begin with and "norm" in
Isabelle/HOL is, by definition, always the norm of a real vector space,
this is not really an issue.
Manuel
Last updated: Apr 16 2024 at 12:28 UTC