Re: [isabelle] The theory Option

On 14-10-08 14:45, Gottfried Barrow wrote:
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...

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


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