Email Gateway (Aug 19 2022 at 11:30): Email Gateway (Aug 19 2022 at 11:30):From: Henri DEBRAT <Henri.Debrat@loria.fr>
Hi all,
I try to discover where the undefined value is ... defined. I could not find any undefined_def lemma or axiom.
In particular, is it polymorphic ? What are its properties ? What are the mathematical foundations and consequences of how it has been defined ?
I also wonder why the "None" option types constructor does not point to undefined in some way or another. Furthermore, I do not understand whether None is typed of not.
This all sounds rather simple questions but I am a little ill at ease with using a keyword without its precise semantics in mind !
Thanks in advance
H.
Email Gateway (Aug 19 2022 at 11:30):From: Stephan Merz <Stephan.Merz@loria.fr>
Henri,
On Jul 13, 2013, at 11:17 PM, Henri DEBRAT <Henri.Debrat@loria.fr> wrote:
I try to discover where the undefined value is ... defined. I could not find any undefined_def lemma or axiom.
In particular, is it polymorphic ? What are its properties ? What are the mathematical foundations and consequences of how it has been defined ?
grepping for undefined in src/HOL yields
HOL.thy:axiomatization undefined :: 'a
As you can see, the constant is not defined but declared as a polymorphic constant for arbitrary type. This is logically unproblematic because types in HOL must be non-empty. The value denotes some unspecified value of arbitrary type, this is sometimes useful when no particular property of the value is required.
Note that in theory Hilbert_Choice one could actually define
definition undefined where "(undefined::'a) = Some (x::'a). True"
I also wonder why the "None" option types constructor does not point to undefined in some way or another. Furthermore, I do not understand whether None is typed of not.
Since "undefined" is polymorphic, it exists for any option type. Defining "undefined :: 'a option" to be None would be more specific than what is required.
Hope this helps,
Stephan
Email Gateway (Aug 19 2022 at 11:30):From: Henri DEBRAT <Henri.Debrat@loria.fr>
Hi Stephan,
Thanks a lot for your clear answer. Just to be sure: I suppose you mean SOME ?
==> "(undefined::'a) = SOME (x::'a). True") ?
H.
Email Gateway (Aug 19 2022 at 11:30):From: Stephan Merz <Stephan.Merz@loria.fr>
Oops, of course! -s
Email Gateway (Aug 19 2022 at 11:30):From: Lars Noschinski <noschinl@in.tum.de>
On 13.07.2013 23:17, Henri DEBRAT wrote:
I try to discover where the undefined value is ... defined. I could not find any undefined_def lemma or axiom.
In particular, is it polymorphic ? What are its properties ? What are the mathematical foundations and consequences of how it has been defined ?
You can see whether a term is polymorphic or not by simply printing it
with "term" -- iff its type contains type variables, it is polymorphic
(in the global context).
"undefined :: 'a" has exactly those properties any value of type 'a has.
I also wonder why the "None" option types constructor does not point to undefined in some way or another. Furthermore, I do not understand whether None is typed of not.
Every value in Isabelle has exactly one concrete type, so None is
"typed". A polymorphic constant like None can be used to refer to
various values, depending on its type.
I.e., you can have e.g. "None :: nat option" and "None :: int option"
but if you write "(None :: nat option) = (None :: int option)" you get
a type error.
-- Lars
Email Gateway (Aug 19 2022 at 11:30):From: Lars Noschinski <noschinl@in.tum.de>
That would be an equivalent definition, as would be
"SOME x. False" or "THE x. x = x".
However, mind that we cannot prove "undefined :: 'a" and "SOME x :: 'a.
True" to be equal (except for 'a = unit, of course).
-- Lars
Email Gateway (Aug 19 2022 at 11:31):From: Lars Noschinski <noschinl@in.tum.de>
Stephan alerted me that "equivalent" is misleading here: They are
"equivalent" in the sense that both can fill the same role, i.e., they
represent an arbitrary value of type 'a. They are not "equivalent" in
that we cannot prove any relation between "undefined :: 'a" and "SOME (x
:: 'a). True.
-- Lars
Email Gateway (Aug 19 2022 at 11:31):From: John Wickerson <johnwickerson@cantab.net>
Further to Stephan's response...
The type of "None" is "T option", for any type T. Suppose T has elements {a,b,c,d}. Then "T option" will contain the elements {None, Some a, Some b, Some c, Some d}. "None" is just an extra element added to the type.
"None" is often used when defining partial functions: an input is sent to "None" when the partial function is not defined for that input. But otherwise "None" and the special "undefined" constant are completely unrelated.
There are other uses of "None", unrelated to definedness. For instance, None could represent an error in a calculation. A division function might return "Some 10" when asked to divide 50 by 5, and "None" when a division-by-zero is attempted. Another use is to represent natural-numbers-with-infinity. The type "nat" only includes finite numbers, but if you use "nat option" then you can use "None" to stand for infinity.
In short, None is just an extra element added to an existing type.
john
Email Gateway (Aug 19 2022 at 11:51):From: Henri Debrat <henri.debrat@loria.fr>
Hi all,
Sorry if I come back to this topic quite late. Why undefined and None must be different things is still not clear to me.
First, taken from Stephan's answer:
(1) what do you mean when saying: Defining "undefined :: 'a option" to be None would be more specific than what is required.
More precisely, I do not understand why the actual definition is more general (in what meaning ?) and indeed, I do not understand what /is/ required on what purpose.
(2) Let's say that Isabelle do not define "undefined" thanks to the axiomatization command, but with Hilbert's Choice operator, as you suggest. Would it make no difference ? Does it mean that using a type variable already makes the Hilbert's Choice operator implicitly admitted ? Then, I suppose that such a construction is then inherently linked to classical logic (since Hilbert's Choice makes the logic classical according to Diaconescu, cf hop-logic.pdf page 8) ?
Then, answering to John who said: otherwise "None" and the special "undefined" constant are completely unrelated.
My question is: why aren't they related more closely ? It appears to me that every usage of None you describe would remain possible if None was related to undefined as in (1).
H.
Le 14 juil. 2013 à 12:18, John Wickerson <johnwickerson@cantab.net> a écrit :
Further to Stephan's response...
The type of "None" is "T option", for any type T. Suppose T has elements {a,b,c,d}. Then "T option" will contain the elements {None, Some a, Some b, Some c, Some d}. "None" is just an extra element added to the type.
"None" is often used when defining partial functions: an input is sent to "None" when the partial function is not defined for that input. But otherwise "None" and the special "undefined" constant are completely unrelated.
There are other uses of "None", unrelated to definedness. For instance, None could represent an error in a calculation. A division function might return "Some 10" when asked to divide 50 by 5, and "None" when a division-by-zero is attempted. Another use is to represent natural-numbers-with-infinity. The type "nat" only includes finite numbers, but if you use "nat option" then you can use "None" to stand for infinity.
In short, None is just an extra element added to an existing type.
john
On 14 Jul 2013, at 10:22, Stephan Merz wrote:
Henri,
On Jul 13, 2013, at 11:17 PM, Henri DEBRAT <Henri.Debrat@loria.fr> wrote:
I try to discover where the undefined value is ... defined. I could not find any undefined_def lemma or axiom.
In particular, is it polymorphic ? What are its properties ? What are the mathematical foundations and consequences of how it has been defined ?
grepping for undefined in src/HOL yields
HOL.thy:axiomatization undefined :: 'a
As you can see, the constant is not defined but declared as a polymorphic constant for arbitrary type. This is logically unproblematic because types in HOL must be non-empty. The value denotes some unspecified value of arbitrary type, this is sometimes useful when no particular property of the value is required.
Note that in theory Hilbert_Choice one could actually define
definition undefined where "(undefined::'a) = Some (x::'a). True"
I also wonder why the "None" option types constructor does not point to undefined in some way or another. Furthermore, I do not understand whether None is typed of not.
Since "undefined" is polymorphic, it exists for any option type. Defining "undefined :: 'a option" to be None would be more specific than what is required.
Hope this helps,
Stephan
Email Gateway (Aug 19 2022 at 11:51):From: Stephan Merz <stephan.merz@loria.fr>
Henri,
I'm sorry if the replies were not clear for you. Let me try again.
The purpose of the constant "undefined" is to have a name for an element of the underlying type for which you have no other information than just that it denotes an unspecified value of that type. Giving any definition (such as it being equal to None when we are talking about an option type or defining it using Hilbert's epsilon or a definite description) gives you more equalities for the value than you care to have.
Similarly, when John says undefined and None are unrelated he really meant to say that we have no way to know if there is a relationship between these values. Obviously, any usage of an unspecified value remains possible for a more specified one, but the purpose is to keep "undefined" as far apart from known values as possible.
Hope this will be clearer.
Regards,
Stephan
Email Gateway (Aug 19 2022 at 11:51):From: John Wickerson <johnwickerson@cantab.net>
Hi Henri,
If I may donate a few more words to this interesting topic...
HOL is a logic of total functions. Whenever you have a function, say f :: nat => bool, then f corresponds to a particular function. If you say
definition "f :: nat => bool" where "f 5 == True"
then, at least in my head, f becomes a particular function, with a boolean value for every nat, but the only thing we know about the function is that it maps 5 to True.
Pushing this idea to its limits, "undefined" is a term we know nothing about.
Then "None" is a completely different kettle of fish. It's often handy to extend a set by one extra element, say to add infinity to the set of naturals, or to add a special "undefined" return value. This is done in Isabelle using the option type. "None" is the extra element you add to the set, and you prepend all the other elements in the set with the tag "Some" in order to make sure that they are all different from "None".
John
Email Gateway (Aug 19 2022 at 11:51):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Hi Henri,
You can use the type 'a option such that None models undefinedness, but there are other
uses, too. Take, e.g., a type foo with an order <=. Then, you can lift this order to "foo
option" and make None the least or greatest element in "foo option". And there are
hundreds of other uses of "'a option" that you could imagine. Now, for all these uses, it
would be fairly unnatural to require that undefined always denotes the largest / smallest
element or whatever specific element.
A long time ago (before Isabelle2009), "undefined" was called "arbitrary", and "arbitrary"
reflected the specification of the element better: it was some element of the type.
However, as definitional packages (and some users) used undefined for cases when the
desired specification of a constant did not say anything, it got renamed to undefined. But
logically, it still is just an arbitrary element of the type. And None would be a very
special element of that type.
Hope this helps,
Andreas
Email Gateway (Aug 19 2022 at 11:51):From: Ramana Kumar <rk436@cam.ac.uk>
On Mon, Sep 30, 2013 at 3:39 PM, Andreas Lochbihler <
andreas.lochbihler@inf.ethz.ch> wrote:
Take, e.g., a type foo with an order <=. Then, you can lift this order to
"foo option" and make None the least or greatest element in "foo option".
And there are hundreds of other uses of "'a option" that you could imagine.
Now, for all these uses, it would be fairly unnatural to require that
undefined always denotes the largest / smallest element or whatever
specific element.
Indeed, it would actually be impossible to use undefined for that purpose,
since undefined might not be the largest / smallest element - it might be
equal to some element in the middle (but not provably so).
On 30/09/13 16:15, Henri Debrat wrote:
Hi all,
Sorry if I come back to this topic quite late. Why undefined and None
must be different things is still not clear to me.First, taken from Stephan's answer:
(1) what do you mean when saying: Defining "undefined :: 'a option" to be
None would be more specific than what is required.
More precisely, I do not understand why the actual definition is more
general (in what meaning ?) and indeed, I do not understand what /is/
required on what purpose.(2) Let's say that Isabelle do not define "undefined" thanks to the
axiomatization command, but with Hilbert's Choice operator, as you suggest.
Would it make no difference ? Does it mean that using a type variable
already makes the Hilbert's Choice operator implicitly admitted ? Then, I
suppose that such a construction is then inherently linked to classical
logic (since Hilbert's Choice makes the logic classical according to
Diaconescu, cf hop-logic.pdf page 8) ?Then, answering to John who said: otherwise "None" and the special
"undefined" constant are completely unrelated.My question is: why aren't they related more closely ? It appears to me
that every usage of None you describe would remain possible if None was
related to undefined as in (1).H.
Le 14 juil. 2013 à 12:18, John Wickerson <johnwickerson@cantab.net> a
écrit :Further to Stephan's response...
The type of "None" is "T option", for any type T. Suppose T has elements
{a,b,c,d}. Then "T option" will contain the elements {None, Some a, Some b,
Some c, Some d}. "None" is just an extra element added to the type."None" is often used when defining partial functions: an input is sent to
"None" when the partial function is not defined for that input. But
otherwise "None" and the special "undefined" constant are completely
unrelated.There are other uses of "None", unrelated to definedness. For instance,
None could represent an error in a calculation. A division function might
return "Some 10" when asked to divide 50 by 5, and "None" when a
division-by-zero is attempted. Another use is to represent
natural-numbers-with-infinity. The type "nat" only includes finite numbers,
but if you use "nat option" then you can use "None" to stand for infinity.In short, None is just an extra element added to an existing type.
john
On 14 Jul 2013, at 10:22, Stephan Merz wrote:
Henri,
On Jul 13, 2013, at 11:17 PM, Henri DEBRAT <Henri.Debrat@loria.fr>
wrote:
I try to discover where the undefined value is ... defined. I could not
find any undefined_def lemma or axiom.
In particular, is it polymorphic ? What are its properties ? What are
the mathematical foundations and consequences of how it has been defined ?
grepping for undefined in src/HOL yields
HOL.thy:axiomatization undefined :: 'a
As you can see, the constant is not defined but declared as a polymorphic
constant for arbitrary type. This is logically unproblematic because types
in HOL must be non-empty. The value denotes some unspecified value of
arbitrary type, this is sometimes useful when no particular property of the
value is required.Note that in theory Hilbert_Choice one could actually define
definition undefined where "(undefined::'a) = Some (x::'a). True"
I also wonder why the "None" option types constructor does not point to
undefined in some way or another. Furthermore, I do not understand whether
None is typed of not.
Since "undefined" is polymorphic, it exists for any option type. Defining
"undefined :: 'a option" to be None would be more specific than what is
required.Hope this helps,
Stephan
Email Gateway (Aug 19 2022 at 11:51):From: Henri Debrat <henri.debrat@loria.fr>
Thanks for all your answers !
I understand it better now, I believe. To sum it up :
Hence, I think I understand in which meaning "None" is of a different usage than "undefined".
However, focusing on what Andreas says, because undefined is polymorphic, I do not see why it would be a problem to state that, for some specific type the user defines, "undefined" is such that so additional constraints hold. And we could say that, in an option type, undefined is such that any other element is different from all the others.
What I suggest here is not to make "undefined" and "None" be one and the same, but to define "None" as being a peculiar case of "undefined", by adding a constraint to "undefined" when considering an option type so that it's always different from any "Some y".
I hope I am not being boring by going further in this discussion...
H.
----- Mail original -----
Email Gateway (Aug 19 2022 at 11:51):From: Tjark Weber <webertj@in.tum.de>
I like to say that too. At the same time, it is worth pointing out that
we do know certain (trivial) things about "undefined": for instance,
"undefined = undefined".
Best,
Tjark
Email Gateway (Aug 19 2022 at 11:51):From: Jasmin Blanchette <jasmin.blanchette@gmail.com>
The renaming from "arbitrary" to "undefined" was very unfortunate. Perhaps it's not too late to rename it one last time, to "unspecified". What do you think?
Jasmin
Email Gateway (Aug 19 2022 at 11:52):From: Lawrence Paulson <lp15@cam.ac.uk>
I agree that the renaming was unfortunate, but I'm not convinced that a further renaming would be that useful.
Although it would be easier than changing from sets to predicates and back again :-)
We just need to be very clear about what this constant actually denotes.
Larry
Email Gateway (Aug 19 2022 at 11:52):From: Jasmin Blanchette <jasmin.blanchette@gmail.com>
My experience is that it's much easier to explain what something is when its name is not positively confusing.
Imagine you need to name a constant for the color green. There are three levels of naming:
Good naming: green
Neutral naming: kijani [*]
Confusing naming: red
It's easy to train one's brain to map "kijani" to "green", but having to teach the whole world that "red" means "green" just adds one layer of obfuscation.
If it was possible to muster the courage to perform such an unfortunate renaming in the first place, surely it shouldn't be too hard to do it again in favor of a good name -- and I would be happy to actually perform the renaming.
Jasmin
[*] unless you know Swahili, in which case this becomes a good name
Email Gateway (Aug 19 2022 at 11:52):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Hi Henri,
However, focusing on what Andreas says, because undefined is polymorphic, I do not see why it would be a problem to state that, for some specific type the user defines, "undefined" is such that so additional constraints hold.
And we could say that, in an option type, undefined is such that any other element is different from all the others.
You can do that in your own theories by asserting the appropriate axioms. The simplest way
to do so is:
lemma undefined_my_type_option: "undefined :: my_type option = None"
sorry
What I suggest here is not to make "undefined" and "None" be one and the same, but to define "None" as being a peculiar case of "undefined", by adding a constraint to "undefined" when considering an option type so that it's always different from any "Some y".
But then they are the same. HOL has equality for every type, and you can do case
distinctions about every option type. Thus: From "!!x. undefined ~= Some x", you can
derive "undefined = None".
Inside Isabelle, there would be no problem with saying that None and undefined are the
same, the logic would still be consistent. But take a step back and think about what you
are doing in Isabelle: You create mathematical descriptions of the real world by
specifying appropriate constants, and then you prove properties about your model. Now,
these theorems apply to every real-world instance that satisfies the specification of your
constants, i.e., if you make your specifications stronger, your theorems apply to less
instances.
10-15 years ago, when there were only few definitional packages available, many people
axiomatized the model rather than defined them. Often, one just dealt with underspecified
functions. However, one always runs the risk of introducing logical inconsistencies this
way. So, nowadays, it is more popular to define your constants (and types) in terms of
existing constants (this is the definitional principle in the HOL community). Then, you
prove lemmas that your constants meet the specification that you care about; and ideally,
your theorems only use the specifications lemmas. But Isabelle will not stop you from
exploiting all the properties that your definitional method accidentially has introduced.
So, in general, nowadays, the theorems that we prove apply to less real-world instances
than in the old days, but we can be sure that at least there are no logical
inconsistencies in our specifications.
The constant undefined is one of the cases where we still care about "relaxing the
specification as far as possible". Undefined is used by many packages internally, and it
is important from a modelling perspective that it remains this way. Consider, for example,
the function nth from List (written infix as !): xs ! n returns the n-th element of the
list xs. If n is greater than the length of xs, xs ! n returns "undefined n", i.e, an
arbitrary value of the right type, but that might be different for every list index. And
this captures fairly well what you would get when you interpret lists as arrays and nth as
array access: If you access a cell outside the bounds of the array, you might get a
different value for every index (assuming that your imperative language does not enforce
range checks).
Some time ago, undefined had a constraint for function types: !!x. undefined x = undefined
This meant that an unspecified function is a constant function. I myself was not happy
when this constraint was removed, because it allowed all sorts of short-cuts in my proofs.
But in the end, I am happy that it no longer is there: it has unnecessarily reduced the
faithfulness of many models. And the same would happen if "undefined :: 'a option" would
be constrained to None. For example, you could prove that the head of the empty list
always is None, but that might be a realistic assumption.
Best,
Andreas
Email Gateway (Aug 19 2022 at 11:52):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Hi Jasmin,
I agree that undefined is unfortunate, and unspecified would probably be a better name.
But before you set out to rename it, let's first discuss it in a larger context.
The NEWS file describes the replacement as follows:
- Constants "undefined" and "default" replace "arbitrary". Usually
"undefined" is the right choice to replace "arbitrary", though
logically there is no difference. INCOMPATIBILITY.
So there are actually two constants: undefined and default. And actually, there is quire
some difference between them: "undefined" is frequently used by packages (primrec,
function, partial_function) in cases where the user has not given a full specification of
a constant. Moreover, some Isabelle users use it in their own definitions when they need
don't care or an arbitrary value. There are also some instances where you just need some
value in some proof and it's easier to use undefined instead of obtaining one via "obtain
x :: my_type".
In contrast, default is a parameter of the type class default. As there are hardly any
instances of default (see
https://lists.cam.ac.uk/mailman/htdig/cl-isabelle-users/2013-June/msg00044.html for a
brief discussion), regular Isabelle users hardly ever come across it.
In my latest AFP entry (which will be accessible only after the release), I heavily use
undefined to model partially specified API functions of the target languages of the code
generator. Here, soundness relies on "undefined" really being an unspecified value of the
right type.
What I have described so far would fit into the proposed renaming: unspecified captures
the intent better than undefined.
But maybe other people know of further usages for undefined.
Best,
Andreas
Email Gateway (Aug 19 2022 at 11:52):From: Lawrence Paulson <lp15@cam.ac.uk>
I would argue that "undefined" and "unspecified" mean essentially the same thing, and it would be a bit like renaming "azure" to "blue". It is only a problem for people who imagine that "undefined" designates some sort of magical nothingness. There is no such thing in mathematics.
Larry
Email Gateway (Aug 19 2022 at 11:52):From: Jasmin Blanchette <jasmin.blanchette@gmail.com>
But it's better style, and hardly more typing, to write the following:
axiomatization where
undefined_my_type_option: "(undefined :: my_type option) = None"
Then you make your intentions clear, and tools like Nitpick will work correctly:
lemma "f (undefined :: my_type option) = f None"
nitpick
Nitpick found no counterexample.
Jasmin
Email Gateway (Aug 19 2022 at 11:52):From: Michael Fourman <Michael.Fourman@ed.ac.uk>
There are however non-terminating programs that can give rise to terms that have no denotation.
Sent from my iPhone
Email Gateway (Aug 19 2022 at 12:02):From: Tobias Nipkow <nipkow@in.tum.de>
I was not happy when "arbitrary" was changed to "undefined" because I saw the
confusion this would cause. I would support a new name (after the release) and
"unspecified" seems a good candidate.
Concerning Larry's nothingness: just like Michael Fourman I have to point out
that there are many approaches to logics with partial functions where terms may
simply not denote. In fact, that is how many mathematicians would explain 1/0.
Tobias
Email Gateway (Aug 19 2022 at 12:03):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Indeed the maior issue was the introduction of a separate »default«
beside »arbitrary«, where »default« is a type class parameter. It seems
that only proof extraction does really use »default«, so this might
count as argument ot move »default« to Extraction.thy.
Concerning the naming of the constant now named »undefined«, my opinion
is just unspecified ;-).
Cheers,
Florian
signature.asc
Email Gateway (Aug 19 2022 at 12:03):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
AFAIR this (and similar formulations) is due to Alex Krauss.
Florian
signature.asc
Email Gateway (Aug 19 2022 at 12:13):From: Tjark Weber <webertj@in.tum.de>
On Mon, 2013-09-30 at 18:06 +0200, Andreas Lochbihler wrote:
I agree that undefined is unfortunate, and unspecified would probably
be a better name.
+1
"undefined" is frequently used by packages (primrec, function,
partial_function) in cases where the user has not given a full
specification of a constant.
I am not sure how widespread this usage still is in Isabelle. But where
it happens, I consider it a (minor) shortcoming, because it leads to
spurious equations: the user arguably never intended to specify that,
e.g., "hd [] = last []".
Best,
Tjark
Email Gateway (Aug 19 2022 at 12:18):From: Peter Lammich <lammich@in.tum.de>
However, this comes in handy in some cases. Consider, e.g., the
following lemma:
lemma map_eq_nth_eq:
assumes A: "map f l = map f l'"
shows "f (l!i) = f (l'!i)"
without knowing that nth is undefined if the index is out of bounds,
this lemma would have a precondition (i<length l) which makes it harder
to be used by the simplifier.
Email Gateway (Aug 19 2022 at 12:19):From: Tjark Weber <webertj@in.tum.de>
Obviously, stronger assumptions allow us to prove stronger theorems. But
the real issue is whether our models are still sound.
Best,
Tjark
Email Gateway (Aug 19 2022 at 12:21):From: Makarius <makarius@sketis.net>
This is an important observation. In a system like HOL, where most
specifications are actually definitions, "not specified" and "not defined"
means essentially the same.
It is computer-science that has changed the literal meaning of "undefined"
and introduced a bias to mean something like "crash" or "NPE".
HOL as a total logic has its own traditions to make creative use with
seemingly "undefined" things. 1/0 was mentioned already, but without an
explanation of the theories built around it, notably by John Harrison.
This greatly simplifies many proofs, at the cost of semantic confusion
about what specifications mean. Subtraction on nat is handled similarly.
In 1996, when "undefined" was still called "arbitrary" someone giving a
talk about an Isabelle/HOL formalization had it on one of the introductory
slides about the logic. Since the audience was not HOL-istic that started
a very long discussion about what it really means, and it was hard to get
to the main topic of the talk. That incident has become one of the many
Isabelle in-jokes, until it was replaced by this formal one by Florian
Haftmann around 2005:
if arbitrary = undefined then SOME x. True else SOME x. False
Makarius
Email Gateway (Aug 19 2022 at 12:23):From: Makarius <makarius@sketis.net>
Here is a vaguely related thread on the Scala internals mailing list:
https://groups.google.com/forum/#!topic/scala-internals/VkIVISmaxFQ/discussion[1-25-false]
Odersky ultimately calls his version of "undefined" with the symbolic name
"???". Semantically it is of the "crash" / "NPE" kind, since this is
programming, not logic.
Makarius
Email Gateway (Aug 19 2022 at 12:24):From: Joachim Breitner <breitner@kit.edu>
Hi,
I can confirm this observation from a few weeks ago, when I talked about
a Isabelle formalization of mine to a group that work on the same
proofs, but without a proof assistant. I think I got the idea behind
undefined across, but I’m not sure about that, and it certainly did not
make a good impression on the audience.
I sometimes wish for better support for partially defined things, where
I have the vague idea that when, for example, I write "a ⊔ b" somewhere,
then the compatibility of a and b in their order either comes as an
implicit fact, or an implicit proof obligation. But I’m not even sure
how to detect which of the two I want...
Greetings,
Joachim
signature.asc
Last updated: Apr 19 2024 at 16:20 UTC