Mathematics and Computing

The book "Structure and Interpretation of Computer Programs" by Abelson and Sussman has this to say in the preface to the first edition:

"The computer revolution is a revolution in the way we think and in the way we express what we think. The essence of this change is an emergence of what might best be called *procedural epistemology* -- the study of the structure of knowledge from an imperative point of view, as opposed to the more declarative point of view taken by classical mathematical subjects.
Mathematics provides a framework for dealing precisely with notions of "what is." Computation provides a framework for dealing precisely with notions of "how to.""

This statement has always bothered me. Seemed to me that mathematics and mathematicians were not being given their due. An exchange of ideas with Professor Tim Poston has helped me clarify my position vis a vis this passage.

1. The revolution is not "in the way we think" but in the technology that became available to express what we think. Mathematicians have always bothered about procedures. Whether it is a procedure in Euclidean geometry or a procedure to solve an equation. In fact, Knuth says somewhere that the history of number theory can be seen as the history of algorithms.   Gauss's work and Galois's work were also motivated by an interest in procedures.

However, as Professor Tim Poston pointed out to me, mathematicians did not emphasize procedures as much as they did the statements they arrived at using the procedures. Perhaps this was because mathematicians felt that they were "discovering" an area of (Platonic) reality and their statements represented "truths" about this reality. The procedures that led them to these truths were not considered to be important.

This viewpoint was gradually eroded starting with the discovery of non-Euclidean geometries and climaxing with the work of Godel.

2. The problems with the second sentence in the quotation is about the use of the words "emergence" and "knowledge". If the claim is that "procedural epistemology" *began* in the 20th century as the aftermath of Turing's work, then that is difficult to accept. Also it is difficult to accept that either mathematics or computing is studying "the structure of knowledge". Seems to me that both mathematics and physics have given up any claims they might have had that they were discovering knowledge. They are just playing with models and some of them seem to fit some aspects of reality to a useful level of approximation.

3. And finally the last sentence. As I said above, mathematics has always been interested in dealing precisely with both the notions of "what is" and "how to". What has changed is the meaning of the word "precisely". The idea that this means that a machine should be able to execute the procedure is new.

4. In my presentation on "The Nature of Computing" I have tried to present the concerns of computing as part of a historical continuity.

"On the cruelty of really teaching computing science"

"On the cruelty of really teaching computing science" is an article by Dijkstra in 1988. Wikipedia reviews this and says that  " Dijkstra argues that computer programming should be understood as a branch of mathematics, and that the formal provability of a program is a major criterion for correctness.... Specifically, Dijkstra made a “proposal for an introductory programming course for freshmen” that consisted of Hoare logic as an uninterpreted formal system....Computer science as taught today generally does not follow Dijkstra's advice."

I venture to suggest that one of the  reasons that Dijkstra's advice is not followed could be the fact that learning formal logic requires a  huge overhead of investment of time and energy  on the part of a student.  Instead of using formal logic, if we could convey the same content using the simple set algebra the students any way learn when they take their course on discrete mathematics, then the cruelty may be considerably reduced and Dijkstra's ideals can be made practical realities.

In the last post, we showed how Hoare's axioms may be interpreted as mapcode theorems. In this post we point to the article here that shows how to interpret Dijkstra's wp-formalism in terms of nondeterministic mapcode.

Hoare Logic, Pascal P, and Kesav Nori

Here is a short description of how Prof. Kesav Nori used Hoare logic, in his own words:

"I do not recall what I told you about Hoare logic, but in order to prove correctness of the Pascal P compiler, I proposed Axioms a la Hoare Logic for each P-code instruction (including jumps and conditional jumps) and the rule of inference for sequential composition, and then showed that every axiom and rule of inference of Pascal P was a theorem for the compiler geberated code schema. This way, any proof of a program property for a Pascal Program could be treated as a proof for the generated P code, citing the code generation theorems, and that would be a means of asserting semantic preservation, i.e., a compiler is a bridge between two proof systems, respectively for the source and target languages. Hoare logic (or any specification language for semantics of a Programming Language) is a meta language in which the bridge can be specified."

"... it was clear as mud, but it covered the ground ..." !

Hoare Axioms are Mapcode Theorems

C.A.R. Hoare in 1969 suggested a set of axioms that may be used to build proofs of program correctness. Despite their general acceptability even after a period of 40 years the method suggested by Hoare is not generally taught and used.

Prof. Kesav Nori once suggested a possible reason why correctness proofs of programs are not more popular than they are. Natural languages that  have evolved over the course of years have too complicated a structure to study mathematically.  Programming languages, even though man-made, still are very complicated, and hard to study mathematically. There is a vast variety of programming styles and it is a daunting task to tackle each program and try to reduce it to a series of Hoare logic links.

The mapcode style of programming we suggest uses only a very simple program template: a single while loop. So it may not be so hard to reason about their correctness using Hoare rules. However, we can show that the Hoare rules can be stated and proved as theorems in  mapcode. An exposition is given here. This shows that any program that may be proved correct using Hoare rules, can also be proved correct using mapcode. At the same time this result suggests that we do not need to confine ourselves to Hoare rules: any argument that is correct in terms of set algebra may be used. We thus have a very simple way of proving programs correct.

Knuth's Effective Algorithms

Donald Knuth in the first volume of his book presents a mathematical definition of an algorithm that satisfies the first four criteria for a list of instructions to be an algorithm (finiteness, definiteness, input and output). He defines his fifth criterion as "effectiveness". He explains this to be "computable in principle exactly in a finite amount of time by someone with pencil and paper".

He then gives a method of computation that qualifies for this fifth criterion also. This is a modification of the model that involves symbol manipulation proposed by A.A. Markov.  N.J. Cutland in his book "Computability" says on page 65 that "Markov-computability on N (the set of natural numbers) is defined by using some system of representing numbers in the usual way, and thus coincides with the other approaches to computability". This seems to suggest that the class of Markov-computable functions coincides with the class of, for example, Turing-computable functions. This is probably true of Knuth-computable functions also. Nevertheless, it would be nice to have a direct proof that Knuth-computable functions are the same as partial recursive functions.

An exposition of Knuth-computability is given here.

The Program Dynamics Course - 2009

Last year I had given a semester course based on my book IMCS with the title "Program Dynamics" at the International Institute of Information Technology, Hyderabad, India. This year I am offering it again. On occasion, I hand around some supplementary material to the class. All such material is gathered here.