Re: [isabelle] undefined & None



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


	Makarius




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.