Re: [isabelle] undefined & None
- To: cl-isabelle-users at lists.cam.ac.uk
- Subject: Re: [isabelle] undefined & None
- From: Tobias Nipkow <nipkow at in.tum.de>
- Date: Tue, 01 Oct 2013 09:34:31 +0200
- In-reply-to: <24A8DB07-27B1-4189-8E5D-A125816D292D@cam.ac.uk>
- References: <17586634.60.1380549789223.JavaMail.Henri@Hammerklavier.local> <52498D1C.email@example.com> <987B82FE-C1A6-4549-84BB-66F1C655163B@gmail.com> <4C59F544-D15D-4A76-B4B6-AF8B62F4ECFB@cam.ac.uk> <2AF62C01-C7BB-4877-9615-7AA23B614854@gmail.com> <24A8DB07-27B1-4189-8E5D-A125816D292D@cam.ac.uk>
- User-agent: Mozilla/5.0 (Macintosh; Intel Mac OS X 10.8; rv:17.0) Gecko/20130801 Thunderbird/17.0.8
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.
Am 30/09/2013 18:11, schrieb Lawrence Paulson:
> 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.
> On 30 Sep 2013, at 16:45, Jasmin Blanchette <jasmin.blanchette at gmail.com> wrote:
>> Am 30.09.2013 um 17:16 schrieb Lawrence Paulson <lp15 at cam.ac.uk>:
>>> We just need to be very clear about what this constant actually denotes.
>> 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.
>> [*] unless you know Swahili, in which case this becomes a good name
This archive was generated by a fusion of
Pipermail (Mailman edition) and