Email Gateway (Aug 22 2022 at 16:39): Email Gateway (Aug 22 2022 at 16:39):From: Manfred Kerber <mnfrd.krbr@gmail.com>
Hi,
I was recently confused about expressions such as value "(1::nat)/0"
for which I get the result 0 :: real.
I understand that the logic used in Isabelle/HOL is total. However, I
thought that usually partiality is approximated by leaving the value
of expressions such as 1/0 as unspecified. What is the reason that
this seems not to be the case for 1/0?
Kind regards
Manfred
Email Gateway (Aug 22 2022 at 16:39):From: "Thiemann, Rene" <Rene.Thiemann@uibk.ac.at>
Dear Manfred,
I did not look in the history on why it was defined like this but just make
some comments.
As you already said, Isabelle is a logic of total function, so you have to totally specify
division. Therefore, there also is a special constant “undefined” of each type
which stands for some arbitrary fixed value of that type. So, “undefined :: real”
is a real number, but we don’t know whether it is 0, 1, pi, e, or ….
So in principle, you could define division as
“x / y = (if y = 0 then undefined else THE-unique z such that y * z = x)”
As a consequence, several nice equalities now get preconditions.
For instance, the current lemma times_divide_eq_left
"b / c * a = b * a / c”
with the above definition will only be provable if c is not 0.
This will definitely make formal proofs more verbose, because one now
has to keep track that all divisions are not by 0.
And on the contrary, even if you define “x / y” as above, then you still will be able to prove
that “5 / 0 = 2 / 0” since both sides simplify to the same constant “undefined”.
So even “undefined” behaviour is fully specified and can be exploited for proofs.
(though you can also define “x / y = (if y = 0 then undefined x else …)” where
then “5 / 0 = 2 / 0” simplifies to “undefined 5 = undefined 2” which as far as
I know impossible to proof or to disprove; here, “undefined” is a fixed function
of type real to real.).
I hope this clarifies the situation a bit,
René
Email Gateway (Aug 22 2022 at 16:40):From: Lawrence Paulson <lp15@cam.ac.uk>
A bit of history: the first logic supported within Isabelle was Martin-Löf's constructive type theory, and it is still there (CTT). And while developing arithmetic within that formalisation, I came up with a definition (necessarily primitive recursive and executable) of division. It delivered n/0 = 0. Since then a number of people have noticed that defining x/0 = 0 is convenient. This identity holds in quite a few different proof assistants now.
These things are conventions, exactly the same as announcing that x^-n = 1/x^n and that x^0 = 0.
Larry Paulson
Email Gateway (Aug 22 2022 at 16:41):From: Michael.Norrish@data61.csiro.au
There is a spectrum of possibilities here.
At one end you have the attitude that takes OpenTheory to leave n - m undefined on the natural numbers when m > n (and pre 0 also undefined). At the other, you can try to give "reasonable" values to everything.
Note that if you want to have things be ‘properly’ unspecified, you would definitely take René’s second approach: that consequence (5/0 = 3/0) is horrid.
As with all definitions, the question is what consequences you want to be true.
Michael
Email Gateway (Aug 22 2022 at 16:52):From: Tobias Nipkow <nipkow@in.tum.de>
Programming languages and logics are closely related but not identical. The same
operator may have different meanings in both, although it looks the same, eg
"/". This just means you cannot translate operators verbatim (in both
directions) but have to take their semantics into account. Thus "/" in
Isabelle/HOL is not translated into "/" in (for example) ML but into a modified
version that obeys "1/0 = 0".
Tobias
smime.p7s
Email Gateway (Aug 22 2022 at 16:53):From: Andreas Röhler <andreas.roehler@easy-emacs.de>
Hi,
that makes me some headache. IMHO the freedom of model making is
limited. The task is to represent reality. We know what happens when the
quotient goes towards zero. From there don't see any reason why to
assume zero as result. This looks like a false positive and might make
results unreliable. There should be better ways to deal with.
Best,
Andreas Röhler
Email Gateway (Aug 22 2022 at 16:53):From: Lawrence Paulson <lp15@cam.ac.uk>
Formal systems reveal hidden assumptions. So one might say “1/x is always nonzero", which is certainly true, and we can be more precise and say “1/x is nonzero for all real x", when we may become uneasy that the quantification includes zero. When you formalise that statement in predicate logic, with the usual axioms about the real numbers, it ends up being equivalent to "1/0 is nonzero". And as there are no partial functions in classical predicate logic, any model must give 1/0 some value or other. Then the statement could be true or false.
If you formalise this statement in Isabelle/HOL, it turns out to be false because 1/0 = 0. Similar statements will be false in quite a few other formal systems, in many cases because 1/x cannot be shown to be well-defined. There is a formalism known as free logic that deals explicitly in the concept of a defined value, where 1/0 = 0 is false because 1/0 is undefined, and therefore we can prove 1/0 ≠ 0. But that may not look very natural either.
Larry Paulson
Email Gateway (Aug 22 2022 at 16:53):From: Andreas Röhler <andreas.roehler@easy-emacs.de>
Hi Lawrence,
thanks for your kind response.
That matter seems worth digging in further and probably more fundamental.
Why do we care for math and logic? Because we want to solve real problem
in the world outside, right? From there (the outer world) I guess some
guidance might be derived how the build the model:
Question: Who needs to divide by zero and what does it mean, should that
need arrive? May someone point me to such a real case?
Guess a kind of non-normal state is reached when that necessity arrives.
I.e. that would mean, we can't go on with true/false or some number.
Throwing an exception then must not mean an error --at least being not
sure about that--, but trigger special treatment.
Best,
Andreas Röhler
Email Gateway (Aug 22 2022 at 16:53):From: Lawrence Paulson <lp15@cam.ac.uk>
The advantage of defining x/0 = 0 is that it allows a number of common identities to be used without side conditions. One example (of many) is x/z + y/z = (x+y)/z.
It seems to me you are too focused on programming. You do not throw exceptions in mathematics, and division does not exist in the world outside. If you do want to reason about programming (including exceptions), then you need to formalise the semantics of your language, but that is separate from the formalisation of mathematics itself.
As I mentioned in my previous message, there are a number of formalisms that allow you to reason about things being defined. But they never catch on because they are tiresome to use. Generally they force you to show things to be defined (and if you have a large expression, that means every single subexpression). Proving theorems is difficult, which is why we try to avoid introducing additional complications.
Larry Paulson
Email Gateway (Aug 22 2022 at 16:57):From: Manfred Kerber <mnfrd.krbr@gmail.com>
Dear All,
Many thanks for all your answers; they are very helpful. Yes, I
understand the statement and agree with it that we are free in
defining concepts and that we should do so with the properties we want
to get in mind. As somebody who is interested in the extraction of
code, I am also concerned with the relationship of the Isabelle
definition and that in a programming language. Should it be a goal to
have definitions for partial functions such as division that are close
to the ones taken in programming languages? Or can we convincingly
defend a design decision for 1/0 = 0 to programming language people
who could have also gone the route of defining 1/0 as 0, but had very
good reasons not to do this and are more willing to accept a crash
than the answer 0? Or do we have to accept that Isabelle is for such
cases different from standard programming languages and argue that we
best avoid such expressions?
Best wishes
Manfred
Last updated: Nov 21 2024 at 12:39 UTC