Email Gateway (Mar 24 2021 at 20:30): Email Gateway (Mar 24 2021 at 20:30):From: Stepan Holub <holub@karlin.mff.cuni.cz>
Hi,
it is true that hd [] = last [] (= undefined):
lemma "hd Nil = last Nil"
unfolding hd_def last_def by simp
This in particular implies that both
lemma hd_rev: "xs ≠ [] ⟹ hd(rev xs) = last xs"
and
lemma last_rev: "xs ≠ [] ⟹ last(rev xs) = hd xs"
happen to hold without the assumption. Is this cheating?
Best regards
Stepan
Email Gateway (Mar 24 2021 at 21:32):From: Lawrence Paulson <lp15@cam.ac.uk>
I don’t think it’s cheating. I think it’s great!
Larry
Email Gateway (Mar 24 2021 at 21:46):From: Manuel Eberl <eberlm@in.tum.de>
Philosophically, I think it is not a good idea to rely on the behaviour
of functions outside their domain. From the point of view of robustness,
this is also the case, since any change in this ‘unspecified behaviour’
will break your proofs.
From a practical point of view, I would say: if it makes your life
easier, go for it. The definitions of hd and tl are highly unlikely to
change.
Experience has shown that while it may seem more "honest" to leave
functions "as unspecified as possible" outside their domain, it just
makes things unnecessarily different. This is why I e.g. like to give
functions some reasonable "dummy" value at points at which they are not
defined, such as "0" for functions that return numbers. This is also
what we do for "x / 0". Every now and then, somebody comes along and
complains about it, but the reality is that it doesn't break anything
and makes some things in practice a little easier.
(for example, if you let ln be completely undefined on the negative
numbers, it would no longer be a unconditionally measurable function,
which confuses the automation for measurability to no end)
Cheers,
Manuel
Email Gateway (Mar 25 2021 at 07:25):From: Stepan Holub <holub@karlin.mff.cuni.cz>
From the practical point of view, this makes the reasoning about the
reversal symmetry a lot easier.
Philosophically, the symmetry suggests that the dummy value for both hd
Nil and last Nil should be the same in any eventual re-definition.
It is interesting to note that the symmetry does not hold for nth. More
precisely, the assumption in
lemma rev_nth:
"n < size xs ⟹ rev xs ! n = xs ! (length xs - Suc n)"
cannot be dropped.
In this case, a dummy constant function for "nth Nil" would help.
Stepan
Email Gateway (Mar 25 2021 at 10:23):From: Tjark Weber <tjark.weber@it.uu.se>
Stronger assumptions allow to prove more theorems, but they hold for
fewer models.
Of course, nothing "breaks" as long as the thing you want to reason
about satisfies these assumptions. But if you want to use Isabelle's hd
and last to formalize something, you'll now have to think twice to make
sure that "hd [] = last []" holds for your application; otherwise, your
formalization is unsound.
Most importantly, you'll have to be aware that this is even an issue. I
think this could be surprising to many users, especially since it is
not obvious from the definitions of hd and last.
(On the other hand, HOL is a logic of total functions, so hd [] and
last [] would still exist even if they were left unspecified. I
acknowledge that this might already be surprising to some users.)
Best,
Tjark
När du har kontakt med oss på Uppsala universitet med e-post så innebär det att vi behandlar dina personuppgifter. För att läsa mer om hur vi gör det kan du läsa här: http://www.uu.se/om-uu/dataskydd-personuppgifter/
E-mailing Uppsala University means that we will process your personal data. For more information on how this is performed, please read here: http://www.uu.se/en/about-uu/data-protection-policy
Email Gateway (Mar 25 2021 at 15:23):From: Manuel Eberl <eberlm@in.tum.de>
That sentence was directed more at the recurring discussion of whether
defining "x / 0 = 0" leads to logical inconsistencies (which it clearly
doesn't).
I agree that these choices do have some potentially negative
consequences. But a total logic like HOL, especially combined with the
lack of dependent types, simply isn't made for dealing with undefined
things properly.
And even in systems that do have dependent types, I think people often
resort to "dummy values" for things like "division by zero" or instead
of restricting the input type.
Manuel
smime.p7s
Email Gateway (Mar 25 2021 at 22:56):From: Jeremy Dawson <Jeremy.Dawson@anu.edu.au>
Maybe it "clearly" doesn't, but that's not the question which bugs me.
the important question to me is: if you say x / 0 = 0, does this enable
you to prove a theorem, which isn't true in ordinary arithmetic, and
which doesn't obviously contain some feature indicating that it relies
on dividing by zero?
If so, it is surely a rather dangerous thing to do.
Jeremy
Email Gateway (Mar 25 2021 at 23:15):From: "John F. Hughes" <jfh@cs.brown.edu>
I was unhappy with this notion of "total functions" from my first moments
learning Isabelle, but I sucked it up and tried anyhow. I'd love to see,
say, two different versions of the most basic parts of Isabelle in which
stuff like this occurs, one of which defines x/0 to be 0, the other of
which defines it to be, say, 17. If the theorems you can prove are all
provable in both situations, then I'd be a lot happier. Sure, it doesn't
ensure Jeremy's criterion, but at least it'd help ease the minds of new
users.
Email Gateway (Mar 25 2021 at 23:34):From: Mario Carneiro <di.gama@gmail.com>
No it doesn't, and it's not hard to prove this either. As long as the
statement does not make direct use of the value of x / 0, you can replace
all occurrences of x / y with x /' y where x /' y has any other value you
like at y=0, and all the same theorems will hold. Regardless of whether x /
y is used in the proof, because it is a definition which is a conservative
extension, it does not enhance the logical strength of the system so you
can prove all the same theorems about x /' y. So for instance, if you prove
FLT relying on this definition of division, then you can also prove FLT
without that definition, or where the definition has some different
behavior at 0, because FLT doesn't have a division sign in it. This is what
it means for a definition to be conservative.
Mario Carneiro
Email Gateway (Mar 25 2021 at 23:35):From: "Norrish, Michael (Data61, Acton)" <Michael.Norrish@data61.csiro.au>
That won’t happen. If inv 0 is defined to be zero, then you get the nice theorem
inv (inv x) = x
without a precondition. Making inv 0 = 17 wrecks this (inv is no longer injective).
Michael
Email Gateway (Mar 26 2021 at 11:01):From: Tjark Weber <tjark.weber@it.uu.se>
On Thu, 2021-03-25 at 19:15 -0400, John F. Hughes wrote:
I was unhappy with this notion of "total functions" from my first
moments learning Isabelle, but I sucked it up and tried anyhow. I'd
love to see, say, two different versions of the most basic parts of
Isabelle in which stuff like this occurs, one of which defines x/0 to
be 0, the other of which defines it to be, say, 17. If the theorems
you can prove are all provable in both situations, then I'd be a lot
happier. [...]
That is (clearly) not the case. For starters, you'll be able to prove
x/0 = 0 in one theory and x/0 = 17 in the other.
If you are willing to accept that x/0 denotes some value (because we
are working in a logic of total functions), but don't want theorems
that depend on the specific value of x/0, the proper solution is to
leave the value of x/0 unspecified.
Without further assumptions about x/0, you'll then only be able to
prove theorems that hold regardless of what the specific value of x/0
is.
Best,
Tjark
On Thu, Mar 25, 2021 at 6:56 PM Jeremy Dawson <
Jeremy.Dawson@anu.edu.au> wrote:
>On 26/3/21 2:23 am, Manuel Eberl wrote:
That sentence was directed more at the recurring discussion of
whether
defining "x / 0 = 0" leads to logical inconsistencies (which it
clearly
doesn't).Maybe it "clearly" doesn't, but that's not the question which bugs
me.the important question to me is: if you say x / 0 = 0, does this
enable
you to prove a theorem, which isn't true in ordinary arithmetic,
and
which doesn't obviously contain some feature indicating that it
relies
on dividing by zero?If so, it is surely a rather dangerous thing to do.
Jeremy
När du har kontakt med oss på Uppsala universitet med e-post så innebär det att vi behandlar dina personuppgifter. För att läsa mer om hur vi gör det kan du läsa här: http://www.uu.se/om-uu/dataskydd-personuppgifter/
E-mailing Uppsala University means that we will process your personal data. For more information on how this is performed, please read here: http://www.uu.se/en/about-uu/data-protection-policy
Email Gateway (Mar 26 2021 at 11:09):From: Thomas Sewell <tals4@cam.ac.uk>
I have a suggestion.
This sort of topic, about the oddness of totality in HOL, comes up at
least three times a year, always provokes a medium-length discussion,
and the examples differ but the content of the discussion is otherwise
largely the same.
Is there some kind of a note, or wiki discussion, or published paper
which we could post as a reference during these discussions, so as to
try to shrink these conversations and the associated effort involved
down closer to novel contributions? I can't think of such a reference,
does anyone know of one? If not, would anyone be interested in writing
one? I guess that one issue is that a good such reference ought to try
to gather the case for and against.
Please don't take this as a rebuke to anyone wanting to think and write
about this issue: HOL seems quite intuitive until one hits this aspect,
which is thoroughly alien to the way most of us were taught mathematics
in school. We all needed to process it for a while, and it's natural
that
this is a social process.
Cheers,
Thomas.
Email Gateway (Mar 26 2021 at 11:19):From: Kevin Kappelmann <kevin.kappelmann@tum.de>
I think the blog post by Joachim Breitner is a good reference:
https://www.joachim-breitner.de/blog/732-Isabelle_functions__Always_total%2C_sometimes_undefined
Kevin
Email Gateway (Mar 26 2021 at 14:22):From: Stepan Holub <holub@karlin.mff.cuni.cz>
Dear Thomas,
I think this is not a question of new waves of surprised newcomers only.
In addition to a wiki for those who need to digest that all functions
are total in HOL, it would be also nice to have a detailed documentation
(or another section on the wiki) for slightly advanced users.
Concerning primrec, for instance, the reference manual is a bit
enigmatic and says:
" For missing constructors, the function is defined to return
a default value, but this equation is made difficult to access for
users." (Indeed!)
Similarly, it is not clear whether "undefined :: 'a ⇒ 'b"
returns "undefined :: 'b" for any value of type 'a or not.
I learned from this list that this is not the case (which is expected),
but I also learned that this has changed at some point (a published
paper could be dangerous!).
How about the unspecified values from "fun" which should be also set to
"undefined" according to the warning? Made even more difficult to access
for users?
Is there any documentation for this that one could easily consult
(instead of spamming this list)?
The blog post by Joachim Breitner is useful to a great extent but it
does not answer the above questions.
Best regards
Stepan
Email Gateway (Mar 29 2021 at 11:36):From: Thomas Sewell <tals4@cam.ac.uk>
I seem to have brought an end to this round of the conversation,
which may or may not be a good thing.
Thanks to Kevin Kappelmann for the link to Joachim Breitner's blog
post. I think that's a good reference, and makes the totality of
functions in HOL very clear.
I think that there are still some common questions to be answered,
and/or lessons to be taught.
The first is that, although it's possible to change things and use the
option type to make undefined values clearer, this is hardly
desirable.
The next is that, given that "0 / 1" and "hd []" must be normal values,
there's not a lot to be gained from setting them to "obscure" values
like 17, and a little bit to be gained by setting them to sensible
defaults which reduce work in the steps of some proofs.
A related point is that definitions are done in a conservative way, so
the definition of the division function in the library is irrelevant to
the truth or provability of any statement that doesn't explicitly
mention
it.
Finally, there's Stepan Holub's more advanced question, which I think
is really about inspecting what the definitional packages have done, and
what hidden facts might exist in the logic. I think that print_theorems
after a definitional step usually answers all of these questions, but I
appreciate that isn't a perfect answer.
Does anyone feel that there are other topics that would be good to cover
in some overview or introduction to this issue?
Cheers,
Thomas.
Last updated: Jul 15 2022 at 23:21 UTC