Once more unto the breach!

"In peace there's nothing so becomes a man

As modest stillness and humility."

That is what Shakespeare says in Henry V. Does a modest stillness and humility help us survive in today's academic world? I am informed that  it does not. Hence the return to the blog and website.  Let us see how it goes. 

Please have a look also at my reactivated website https://sites.google.com/view/mapcodecomputing/home.

My thanks to our student Mr. Krishna Singh for his help in reactivation of my website and blog. Also to my colleague Mr. K. Sudheendra.

Posting this after a hiatus of more than two years. Have been studying Labelled Transition Systems which is the work of Milner's students and associates. More recently  the work of Paulo Tabuada on labelled transition systems with output. As noted in this blog earlier this model generalizes the models of Knuth, Dijkstra, and Chandy and Misra. A good candidate to explore in the study of formal methods in computer science and software engineering.

The Technology for Education 2012 conference was held  in IIIT, Hyderabad during 18 July to 20 July 2012.  Dr. Shailey Minocha presented two pre-conference tutorials, one on "Evaluating the Effective Use of Emerging Technologies in Education"and one on "Using Social Media Technologies for Teaching and Research".

I will try to say something here about her  second tutorial. It was very comprehensive and at the same time very detailed. She introduced the essential ideas of social media and spoke about their advantages and disadvantages from the perspective of students, educators, and institutions. She talked about ethical considerations, digital scholarship and digital professionalism. She gave advice on how to and how not to maintain a digital presence and stressed the importance of maintaining a distinction between personal and professional presences. She spoke about ethical  considerations to be kept in mind and what digital scholarship and digital professionalism mean.She explained in detail how to use new technologies. Apart from the well known email, Skype, Google chat and texting,
she described how researchers can use wikis,  blogs, Second Life, Twitter, Ning, Facebook, Elluminate, Cloudworks, Social Learn, Mendeley, Delicious, ScoopIt, Slideshare, Dropbox and some other lesser known technologies.

You need to wait for the release next month of her "Handbook of Social Media for Early Career Researchers and Supervisors" to find out more details Meanwhile you could browse her website http://mcs.open.ac.uk/sm5

Three things I learned from my colleagues at TCS

1. I have spent a lifetime studying and teaching mathematics of many different kinds. When I started working with Prof. Kesav Nori's group at Business Systems and Cybernetics Centre, my understanding was that one could make a mathematical model of a system by writing down the differential equations concerned and analysing them. Much as we do in the prey-predator model. However from Prof. P.N.Murthy I learned that for a any social system that we set out to study initially we do not even know which are the independent and which are the dependent ones. We do not know how the dependent ones vary with the independent ones and which are the positive feedback loops and which are the negative feedback loops. So it is necessary for us first to form this understanding by appropriate "cybernetic influence diagrams". A detailed exposition of these is given here.

2. I thought that my model for mathematical computer science was very simple and easy to understand. However I was puzzled that there was not much eagerness to study it. This despite the fact that all my colleagues were doing difficult work and dealing with complex analytical and logical reasoning and all of them were engineers. Then one day talking to Swami I realized that the resistance was not to my method of approach to computer science but really only to the mathematical notation I was using. It was the abstract formulation and the use of symbols that was making the ideas opaque. So I felt that I had to find a different way of expressing my ideas that engineers could work with, not losing the rigour of expression.

3. What language should I use if not  the mathematical language? I saw Doji and Ravi approaching the organizational problems they were dealing with by looking to the manufacturing domain for inspiration. So then can I think of a way of designing an algorithm so that it is similar to  designing an artefact in a factory? Thus was I led to the Management Model of Computing that is explained here. You need to create an account and then go to the pages on Computational Thinking.

Computing with Multiple Discrete Flows

The nearest in the literature to the model of mapcode is the UNITY work of Chandy and Misra. While mapcode considers a set X together with a map F: X -> X, UNITY considers several maps acting on X. The result is a fascinating theory of parallel and distributed programming. UNITY stands for Unbounded Nondeterministic Iterative Transformation theorY. We interpret this theory purely in mathematical terms as with mapcode. Our first paper on this subject dealing with standard sequential programs that are expected to terminate in a finite number of steps and return a value is given in our paper Computing with Multiple Discrete Flows.

Quantum Formalism and Information Retrieval

In 2004 Keith van Rijsbergen published a book with the title "The Geometry of Information Retrieval". In this book he suggested that quantum formalism can be successfully used to model some of the problems of Information Retrieval. This book was given to me by my colleague Dr. Vasudev Varma of the International Institute of Information Technology, Hyderabad with a request to offer a course on the ideas of the book.

Last semester I did so. I had hoped for senior students who already knew Linear Algebra, but none of those who joined was clear about the basics of Linear Algebra. So almost the entire course was spent teaching them linear algebra and then some of the basics of quantum terminology. At the end I was left with only one class to explain how quantum formalism relates to Information Retrieval.

There was another difficulty. The book of Rijsbergen used the physics notation for the inner product according to which it is the second term of the inner product that is linear and the first term antilinear. The mathematics text books have the opposite convention. So there was a need to rewrite the basics of Hilbert Space theory in the mathematical tradition but using the physics notation. This is now summarized in a document and attached here as Review of Hilbert Space Theory. Also attached is my write-up on the Hilbert Space Model for Information Retrieval.

Fifth meeting of the Formal Methods Reading Group

Chapter 3 was concluded by me and Dr. Venkatesh began discussing the concept of concurrency in Chapter 4. My notes of the part of my lecture are here as FMRG-5. Dr. Venkatesh will also put up his notes soon at the wiki of http://enhanceedu.iiit.ac.in. You may send mail to choppell@gmail.com for the login name and password that are necessary to access the wiki.

Fourth Meeting of the Formal Methods Reading Group

The fourth set of notes is up as FMRG-4. In this we study automata for which there is no start state specified and all states are considered to be accepting states. This is defined as a set together with a collection of choice maps on the set. We define the notion of a strong simulation as a choice map that carries a transition between states to a transition between sets of states. Other ideas of Milner are expressed in similar terms. Would like to know from the readers if this makes it easier to understand Milner's ideas.

Third Meeting of the Formal Methods Reading Group

The third meeting took place on 3rd March. Most of the time was spent discussing the example of the faulty vending machine given by Milner as motivation for the notion of bisimilarity. It became clear that the example needs to be discussed more fully than in the earlier meeting. Accordingly the set of notes were written up. They are available here as FMRG-3. Lesson 3 is in the form of a story: "The Case of the Faulty Vending Machine - An Allegory for Software Engineers".

Second meeting of the formal methods reading group

In the second meeting we discussed the second chapter of the book. In the notes I have posted on my web site at pi-calculus I have omitted the state space diagrams. Have made do with tables describing the state diagrams. A little patience and practice will help the reader feel comfortable with them. If the readers really miss the         diagrams,  when I find some time I will try to draw and upload them at the appropriate places.

Formal Methods Reading Group

Dr. Venkatesh Choppella and I, supported by several of our colleagues, have started a Formal Methods Reading Group. We plan to have meetings once a week to pursue a learning path. To begin with we have chosen Robin Milner's 1999 book on "Communicating and Mobile Systems: the pi-calculus". Skeletal notes of the first lecture are posted on my web site as pi-calculus-1. Comments by readers, and corrections where needed, are welcome.

TCS Excellence in Computer Science Week in Pune

Haven't posted in a while.  Been busy with my course on  Program Dynamics and preparing lectures for two workshops. Attended the TCS Excellence in Computer Science (TECS) week in Pune during Jan.3 to Jan.8. The theme this year was "Formal Methods in Software Verification, Testing, and Debugging". For details the reader may go to http://121.241.184.234:8000/tecsweek/tecsweek_home.html. Shankar Natarajan's lectures were especially exciting as also his method of lecturing.  He also drew my attention to the work of Dick Lipton. I am surprised by the following item from the wikipedia article on Richard Lipton: "De Millo, Lipton and Peris criticized  the idea of formal verification of programs and argued that Formal verifications in computer science will not play the same key role as proofs do in mathematics. Absence of continuity, the inevitability of change, and the complexity of specification of real programs will make formal verification of programs difficult to justify and manage."  How about that! All power to the mathematical proofs of mapcode! All power to further research to scale it up to industrial strength! It was a treat to hear Sir Tony Hoare speak about the importance of taking the initiative and going ahead with one's plans even if they appear to be not in step with what others are doing. A boost for Prof. Nori and me. That is exactly what we have been doing over the last few years. Interactions with Prof. Jayadev Misra and Prof. C.R.Muthukrishnan were illuminating and enlightening. At the conclusion of the programme I was given an opportunity to present mapcode ideas. The slides of the presentation have been uploaded here. The novelty of the approach received a good response from some of the younger participants especially. Looks like there is a gap in pedagogics that mapcode fills. Definitely encouraging.

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.

Egyptian Multiplication and Chinese Division

These are two simple algorithms which have been derived using the Dijkstra-Gries methodology in the book. The easiest way to understand the reasoning behind them is by the use of appropriate calculation methods on paper. Such methods are presented here.

Text and Context of Computer Science

This blog is the record of an exploration. What is the academic content of computer science? Is computer science a mushroom that burst upon the landscape of science in the 20th century or does it have roots in classical mathematics and physics? What is the nature of the activity of computing?

Groping towards some answers. The slide presentation Nature of Computing tries to locate
the context of computer science firmly in the area of classical mathematical problems. At
the same time it tries to say that computing may be understood as the game of constructing
required structures from specified pieces using specified methods, much like LEGO.

The slide presentation Dynamical Systems tries to show that the concepts of attractors,
chaos, fractals, artificial life, and models for evolution, memory, and dreams all arise
from the study of special cases of the program "repeat x := F(x)".