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

From: Lawrence Paulson <lp15@cam.ac.uk>

I don’t think it’s cheating. I think it’s great!

Larry

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

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

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

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

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

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.

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

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

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

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.

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

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

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: Dec 05 2021 at 22:18 UTC