ACM Transactions on Mathematical Software

Transcription

Dr. Robert van de Geijn: This video has two purposes. On the one hand, we want to impress upon you the importance of the principle of mathematical induction to programming and computer science. On the other hand, we want to show you a glimpse of the frontier by discussing how some of what you've seen so far relates to our current research. So who's this famous Texan? Well, actually he isn't a Texan at all. He's from the Netherlands. This is Edsger Dijkstra, who is probably one of the most influential computer scientists. He was a Texan for a little while. He was a professor in our department towards the end of his career, and I strongly suggest that you read up on Edsger W. Dijkstra on Wikipedia. Dijkstra received a Turing award in 1972, and as part of receiving the Turing award, one gives a lecture called a Turing lecture. His Turing lecture was titled The Humble Programmer, and we provide a link to the original manuscript that he wrote for this. In it, you will find the following quote. "Today a usual technique is to make a program and to test it. But: program testing can be a very effective way to show the presence of bugs, but is hopelessly inadequate for showing their absence. The only effective way to raise the confidence level of a program significantly is to give a convincing proof of its correctness." And then he goes on. "But one should not first make the program and then prove its correctness, because then the requirement of providing the proof would only increase the poor programmers burden. On the contrary: the programmer should let correctness proof and program go hand in hand." Now what's significant here is the following. Dijkstra did some foundational work when it came to how to prove a loop correct. What you're going to find out in this course is that many of the algorithms in linear algebra use loops. So, clearly it's very important in our field to be able to develop loop-based programs hand in hand with their correctness if we are to follow what Dijkstra proclaimed. The big problem is that no one really knew how to systematically do this for loops. So around the year 2000, within our research group, we actually figured out how to do this for linear algebra algorithms, and the key is the slicing and dicing that you learned about last week. And the other key is the principle of mathematical induction. A significant paper in this research is the paper The Science of Deriving Dense Linear Algebra Algorithms, which we published in 2005. If you want to download this, you go to this website where we collect our recent publications, and what you notice is a whole list of various publications, and you go down to Journal Publications. And if you then go to Journal Publication Number Three, you find this paper, The Science Of Deriving Dense Linear Algebra Algorithms. If you click on this link right here-- the name of the paper itself-- then you get to ACM's Digital Library, and if you then click on PDF, and then you actually get a free copy of this paper. Now, the problem with this paper is that you probably won't understand very much of it until a little later in the semester. Fortunately, we've also written a book that is meant to introduce beginners to these ideas. It's called The Science Of Programming Matrix Computations, and if you go to lulu.com-- which is a self-publishing site-- then you can download a PDF of this for free. So what I want you to do is go directly to Chapter two, and when you do that, what you find is that one of the examples is just a Dot product that you learned about last week. What you also find is that in this book, we use exactly the slicing and dicing notation for expressing algorithms that you learned last week. And finally, what you learn is that if you understand how to slice and dice vectors, then you can actually very systematically derive algorithms for this operation to be correct. Now the rest of the book then deals with how to derive more sophisticated operations, and most of those operations, you will see later in the semester, but it starts very simple with just vector operations like the Dot and the axby. Now, that material goes beyond the scope of this course, but we mention it because we really want you to understand that we're trying to expose you not only to the foundations of linear algebra but also to some of the latest research. So in summary, last week we introduced you to a notation for expressing algorithms that used slicing and dicing. This week we introduced you to the Principle of Mathematical Induction. In the Science of Programming Matrix Computations, you will see how mathematical induction and computation by loops are related, how you can use mathematical induction to prove loops correct, and how to systematically derive algorithms to be correct. What I'm trying to get across is that with what we've already taught you, you can understand what it is that Dijkstra actually meant by that.