Email Gateway (Aug 19 2022 at 16:15): Email Gateway (Aug 19 2022 at 16:15):From: "W. Douglas Maurer" <maurer@gwu.edu>
I've been looking at theory Option for some time now, and I've been
wondering why it isn't used more often than it is. If you're going to
have a type with an extra element called None, an obvious use of this
(obvious to me, anyway) would be to interpret None as "undefined."
Division of real numbers, for example, could be a function from (real
option) x (real option) -> real option, with x/0 = None and None/x =
y/None = None. This is in fact exactly how floating point numbers
work on computers today, except that there None is called NaN, which
is an abbreviation for Not a Number.
The advantage of this over the current system of using zero to mean
"undefined" is that there you can't tell the difference, after the
fact, between a zero meaning "undefined" and a real zero. Another
advantage for me is that if I'm trying to explain Isar to
mathematicians who are complex analysts or other non-algebraists, as
I intend to try to do, it could take a lot of explaining to convince
them that defining x/0 to be 0 (rather than None) doesn't lead to
absurdities. I've done complex analysis myself (my theorem says that
if S and S' are countable dense sets on the complex plane, there
exists an entire function taking S onto S') so I should be believable
when talking to complex analysts.
Is there a good reason why this wouldn't work in practice?
Email Gateway (Aug 19 2022 at 16:15):From: Jasmin Christian Blanchette <jasmin.blanchette@gmail.com>
Dear W. Douglas,
Am 07.10.2014 um 22:37 schrieb W. Douglas Maurer <maurer@gwu.edu>:
I've been looking at theory Option for some time now, and I've been
wondering why it isn't used more often than it is. If you're going to
have a type with an extra element called None, an obvious use of this
(obvious to me, anyway) would be to interpret None as "undefined."
Division of real numbers, for example, could be a function from (real
option) x (real option) -> real option, with x/0 = None and None/x =
y/None = None. This is in fact exactly how floating point numbers
work on computers today, except that there None is called NaN, which
is an abbreviation for Not a Number.
The advantage of this over the current system of using zero to mean
"undefined" is that there you can't tell the difference, after the
fact, between a zero meaning "undefined" and a real zero.
Any scheme is bound to have advantages and inconvenients. The difficulty above arises when you pass the result of division to another operator, e.g. "+". Would addition also take two options as argument? If yes, this leads to a number of issues:
If not, this means you must introduce a "case" construct or a "the" each time you have a division inside, say, a "+". (And "the" isn't much better than not using options at all.)
The situation with NaN is illustrative -- how many actual programs work correctly once NaNs have started appearing in computations? Many procedures are written without considering the case where the inputs are NaN, nor is much thought given to when they may arise in much of the programming out there (with some noteworthy exceptions). Why? Because the alternative is clumsy and tedious, and without formal verification or a rich type system it's hard to catch all cases.
Another advantage for me is that if I'm trying to explain Isar to
mathematicians who are complex analysts or other non-algebraists, as
I intend to try to do, it could take a lot of explaining to convince
them that defining x/0 to be 0 (rather than None) doesn't lead to
absurdities.
This doesn't have to be difficult.
As far as absurdities are concerned, there is no risk between "x/0" is defined as meaning something, as opposed to axiomatized. One could also define "2 + 2 = 5" and use it to prove many things; this wouldn't lead to absurdities either (but would give addition different properties than what we are used to). Absurdities start arising when you overconstraint your specification, which can in principle only happen if you use axioms (or re-definitions, which Isabelle forbids).
To take another example: Donald Knuth defines the binomial coefficients also for negative values of either numbers. This is nonstandard, but he won't be able to derive false that way. Problems will only occur if you combine his results with those from Joe Hacker, who also extends the binomial coefficients but in a different, incompatible way. Clearly, one cannot use two different, incompatible definitions for the same symbol and mix-and-match the corresponding theorems naively.
This having been said, there is a slight catch with "x/0 = 0". If your main definitions and theorems use division, this must be born in mind when reading them, communicating them to fellow mathematicians, etc. (The same issue arises with Knuth's theorems about binomial coefficients.) This is regrettable, and much could be said in favor of leaving "x/0" unspecificed or equal to "undefined". Or you could avoid Isabelle's division in your main interface with mathematicians, relying on your own division operator instead that would be unspecified for 0.
In short, if it takes a lot of convincing, this means that either the explanation is unclear or that they don't understand what a definition is. I would presume mathematicians are familiar enough with definitions.
Regards,
Jasmin
Email Gateway (Aug 19 2022 at 16:16):From: Andrew Butterfield <Andrew.Butterfield@scss.tcd.ie>
Dear W. Douglas,
Jasmin is quite right about the disadvantage of Option, but if you still feel the need
to use it, it might be worth looking at “monads” - specifically the technique adopted by
Haskell programmers to handle I/O and structure large programs.
This allows a form of encapsulation of an Option type where the propagation of None
is done “under the hood”
For the Haskell take on monads see : http://www.haskell.org/haskellwiki/Monad
and http://en.wikipedia.org/wiki/Monad_(functional_programming)#The_Maybe_monad
You want the “Maybe Monad” - “Maybe” is Haskell for “Option"
I’m not sure what Isabelle/HOL theory introduces monads, but I am sure one exists.
We did a comparative study reasoning about I/O in pure lazy functional languages
back in the early/mid noughties, looking at both Haskell (uses monads for I/O)
and Clean (uses uniqueness (linear) typing) and found it was easier to reason about
Clean I/O if we cast it into a monadic-style (quite easy to do).
So if you do want to reason about Option,
and are happy for the rule None op * = None = * op None to hold,
then a monadic approach should be the easiest.
Andrew.
Andrew Butterfield Tel: +353-1-896-2517 Fax: +353-1-677-2204
Lero@TCD, Head of Foundations & Methods Research Group
School of Computer Science and Statistics,
Room G.39, O'Reilly Institute, Trinity College, University of Dublin
http://www.scss.tcd.ie/Andrew.Butterfield/
Email Gateway (Aug 19 2022 at 16:16):From: Manuel Eberl <eberlm@in.tum.de>
Hallo,
I’m not sure what Isabelle/HOL theory introduces monads, but I am sure one exists.
there is the Monad_Syntax theory
(http://isabelle.in.tum.de/repos/isabelle/file/1329679abb2d/src/HOL/Library/Monad_Syntax.thy).
However, this provides only syntax – Isabelle doesn't have a
formalisation of the concept ‘monad’ in the way Haskell does. This would
require parametrised typeclasses, which Isabelle doesn't have. It /does/
have specific monads, such as the option monad, the set monad, state
monads, non-deterministic monads, etc.
Even if you do use monads, you still have the problem that you have to
state all of your lemmas in the form ’Just 1 + Just 1 = Just 2‘.
Cheers,
Manuel
Email Gateway (Aug 19 2022 at 16:16):From: Christian Sternagel <c.sternagel@gmail.com>
Just a side remark. Syntax for Haskell-style do notation is made
available by ~~/src/HOL/Library/Monad_Syntax.thy (where also a bind
operation for the option type is registered).
However, at least for this Isabelle/HOL version of monads I would argue
that not much is done "under the hood". It's just notational convenience
(the famous "syntactic sugar") and does not make reasoning any easier.
cheers
chris
Email Gateway (Aug 19 2022 at 16:16):From: Gottfried Barrow <igbi@gmx.com>
It seems to me, division in HOL is another example of the use of types
in Isabelle/HOL, without the benefit of types.
If I knew anything much more about HOL numbers than that the successor
of 0 is 1, I would define a new type, real_minus_zero, using typedef of
course, and then I would define division so that the denominator of
division is of type real_minus_zero. You can't get divide by zero if the
type guarantees no zero in the denominator.
The use of real_minus_zero would be effortless, because it would
automatically get coerced to real. Or maybe it wouldn't be effortless,
because now there would be two types to deal with, instead of just one.
Regards,
GB
Email Gateway (Aug 19 2022 at 16:17):From: Gottfried Barrow <igbi@gmx.com>
An excellent opportunity to reply to myself, since what I have to say is
to no one in particular.
I guess division of real numbers is completely tied into type classes,
so things aren't so simple as I said.
But it's actually a sign of great progress when people can do a lot of
talking about what they don't understand, yet be doing legitimate work
in mathematics.
For example, how is it possible, with "only" a foundation of college
algebra and trig, that many students, with absolutely no previous
exposure to calculus, can blow through so much material in 3 to 4 months
of the first course of the "mother of all foundational math sequence of
courses" (calculus, vector calculus, and differential equations)?
The reason is one single word, "textbooks". Even novices work through
proofs using the delta-epsilon definition of a limit, which was
formalized as recently as about 1820 by Weierstrass.
So how does Isabelle/HOL measure up when it comes to my ability to do
math in Isabelle/HOL? It doesn't. I can't do any of combinatorics,
number theory, or real analysis in Isabelle/HOL. I could do the abstract
part of abstract algebra, but nothing involving concrete mathematics.
The problem is not that I don't know enough. The problem is that I need
to know too much. My lack of knowledge is no obstacle to my being able
to work in math in a traditional manner. I actually understand way more
math that I'm able to use in Isbelle/HOL.
The problem? Concrete numbers. Arithmetic. That's the problem. That's
the road block.
We have this situation. Isabelle/HOL formalizes mathematics up to
complex numbers, which is its standard entry point. Even more, HOL
formalizes the standard number systems, N, Z, Q, R, and C, in a classic
way, therefore making it "very mathematical", as opposed to "computer
sciencey".
You might think that makes me happy. It made me happy, past tense.
Continuing with "the situation", I can't use the number systems for
arithmetic because I don't know the details, and because I don't know
the details, I don't even know that the classic formalizations are
actually sufficient for concrete arithmetic, so that I don't eventually
hit a brick wall, which is an ever present risk when trying to use
Isabelle/HOL.
Now, I go back to that single word, "textbooks". The mechanics of how to
use Isabelle/HOL, as a software product, is documented fairly well, but
the mathematics that makes up the foundation of Isabelle/HOL, it's not
documented at all. A person might take exception to my generalizations,
but they're close enough for me.
Isabelle/HOL is a logic of its own, and it's used to lay a type-theory
foundation of mathematics up to complex numbers. I ask, "After more than
20 years of development of mathematics in HOL, how many textbooks are
there that explain the basic mathematics that's developed in HOL?" The
answer is zero.
It's not like I'm picky. I'm flexible. Combinatorics, number theory,
abstract algebra, or real analysis, I could go with any of those. I just
need to work through some math, as it's developed and proved in HOL,
where there's some heavy use of numbers, and I need to do it in a
methodical manner, as in "textbook manner".
I say I have a need. I don't actually have a need at all. If I had a
need, I'd be in big trouble, because computer scientists who develop
mathematics in HOL, those computer scientists don't write textbooks
about HOL-based mathematics. What they do is develop libraries, and I
think I understand why, because to teach what you know is to spend time
not advancing where you want to go. Just because I understand doesn't
mean I let myself be happy.
It's best to see that someone has published explanations of the details
of where I think I want to go. With HOL, it's not enough that someone
would tell me, "It's all there. The formalization of N, Z, Q, R, and C
in Isabelle/HOL, or in src/HOL, or the AFP, that gives you the
foundation of what you need."
That's not enough. I shouldn't trust someone that much.
The consequence is that I have to start at the bottom, and slowly work
my way up, even though the number systems are already there.
Okay, given that fact, my first choice is to build on what others have
done, so where do I find documented guidance, commonly called
"textbooks", to teach me the details of number systems? (These details,
I wouldn't have to know if I was content working in traditional math, or
if textbooks existed to start me out at a high level of math in HOL,
such as real analysis.)
I don't find the details from computer scientists who have developed
mathematics in Isabelle/HOL, because rather than writing textbooks about
the details they've implemented, they forge ahead, for their own
pleasure and enjoyment, which, I grudgingly admit, has undoubtedly
resulted in better automation tools, which do their own form of teaching.
The details come from electrical engineers, and computer scientists who
do research in computer arithmetic, and who also have taken the time to
write textbooks. I've done the hard work of tracking these down. It
wasn't obvious that these are where the details would come from, and it
could be I won't use any of them to do the required work, just to do
arithmetic:
1) Fundamentals of Digital Logic with Verilog Design, 3rd, by Brown &
Vranesic
2) Computer Arithmetic and Verilog HDL Fundamentals, by Cavanagh
3) Arithmetic and Logic in Computer Systems, by Lu
4) Modern Computer Algebra, 3rd, by Gathen & Gerhard
Regards,
GB
Last updated: Apr 25 2024 at 16:19 UTC