Re: [isabelle] undefined & None
- To: Lawrence Paulson <lp15 at cam.ac.uk>
- Subject: Re: [isabelle] undefined & None
- From: Makarius <makarius at sketis.net>
- Date: Wed, 2 Oct 2013 11:26:30 +0200 (CEST)
- Cc: USR Isabelle Mailinglist <isabelle-users at cl.cam.ac.uk>
- In-reply-to: <24A8DB07-27B1-4189-8E5D-A125816D292D@cam.ac.uk>
- References: <17586634.60.1380549789223.JavaMail.Henri@Hammerklavier.local> <52498D1C.firstname.lastname@example.org> <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: Alpine 2.00 (LNX 1167 2008-08-23)
On Mon, 30 Sep 2013, Lawrence Paulson wrote:
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.
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
This archive was generated by a fusion of
Pipermail (Mailman edition) and