Thursday, February 26, 2009

A Socratic Dialogue on Theoretical Computer Science

The following piece will appear in a brochure aimed at future (post)graduate students that will be published by my university very soon. I am posting it here in case it may be of interest/use to any of the readers of this blog, and hoping that it won't hurt the cause of TCS too much. I was actually quite surprised that the PR office from my university did not send the piece back to me asking for a complete rewrite :-)

-----------------------

A Socratic Dialogue on Theoretical Computer Science

This dialogue takes place between 23:00 and 24:00 at the counter of the bar in a trendy night club. Alice and Bob have just met and they are sipping a glass of wine. The ice has already been broken and they try to find out more about each other.

Bob: I am a physicist. What do you do?
Alice: I am a computer scientist.
Bob: You are the first woman computer scientist I have met! There aren't many women who like to program or fix computers for a living, aren't there?
Alice: Well, actually I am a theoretical computer scientist.
Bob: (Not hiding a look of surprise on his face.) You must be joking! This surely is a contradiction in terms. There is little that is as practical as, and less theoretical than, computer science! Pardon me for saying so, but, as a scientist myself, I have some level of familiarity with computers, and I know from my daily experience that these machines have dramatically changed many aspects of my work and of my life. I really could not live without my iPod!

I have also read that what we are witnessing today is just the beginning of a digital revolution and that a population of 'effectively invisible' computers around us is embedded in the fabric of our homes, shops, vehicles, farms and some even in our bodies. However, computing is just a technology, not a science.
Alice: (With a smile on her face and sipping her wine.) You are not alone in thinking so. However, the information-technology revolution is a glaring example of how results from basic scientific research, having its roots in subjects such as mathematical logic and computability theory, which once looked very abstract and remote from actual application, lead to technological innovations that cause far-reaching transformations to our society. Because of computer science, logic is the most applied branch of mathematics today.
Bob: I am not easily convinced. What is Theoretical Computer Science (TCS)?
Alice: Let me rest on the shoulders of giants and quote Oded Goldreich and Avi Wigderson, two of the foremost (theoretical) computer scientists of our time:

TCS is the fundamental scientific discipline that aims at understanding general properties of computing, be it natural, man-made, or imaginary.

In fact, in some sense, the whole world of computing arose from Alan Turing's analysis of an imaginary computing device (the Turing machines you might have heard of) that he invented in order to understand the notion of mechanical computation. That imaginary device eventually gave birth to the computers of today and to the software that drives them. So computers arose as the answer to man's quest to understand computation, something that is around us in nature and in our artifacts.
Bob: Yes, I am aware that Nature itself "computes". It is not uncommon these days to see theoretical physicists discuss the information content of black holes or of the universe itself, or the feasibility and power of quantum computation or other computing principles from the physical world. But tell me, how do theoretical computer scientists work? What contributions has the field given to science?
Alice: (Her face becoming brighter with joy.) Research in TCS often starts from the desire to understand the properties of some notion of computation. In particular, we are interested in characterizing what algorithmic problems can be solved, in theory or in practice, using the chosen notion of computation. You know, computers look very powerful, and indeed they are. (Bob nods.) However, they are not omnipotent and there are many precisely formulated problems that they will never be able to solve. Characterizing the notion of computational process and showing the existence of unsolvable problems was one of the early breakthroughs of TCS around 1936, long before any computer existed! Since then, we have learned a lot about the notion of computational complexity of problems. Have you ever watched the TV show Numb3rs?
Bob: (Smiling) Sure, there is a cool physicist in it who walks around with Charlie Eppes.
Alice: (Smiling back) Good. Then you might recall that Charlie Eppes every now and again tries to solve the "P vs NP" problem. This is a problem from computer science that is one of the most fundamental mathematical problems of our time. It is one of the Millennium Problems of the Clay Mathematics Institute (in fact, it is the first such problem) and is the only one amongst them that, apart from its intrinsic scientific interest, has profound practical applications and even philosophical implications!
Bob: (Taken aback) What does that problem have to do with philosophy?
Alice: (Sensing victory) Well, there is a strong sense in which the solution of that problem would allow us to automate efficiently the creative process of finding solutions to a plethora of computational problems in many areas of science. Some people like to say that the "P vs NP" problem can be rephrased as asking whether creativity can be efficiently automated. People in my community tend to believe that the answer is no and that some computational problems are intrinsically hard to solve. Do you shop on line?
Bob: Sure I do, just like anyone else.
Alice: In fact, every time you submit your credit card number for an on-line purchase, you are implicitly trusting that a very basic mathematical problem, the time-honoured decomposition of a number into its prime factors, is computationally hard. The whole of cryptography is a very active branch of TCS.
Bob: Now you really have to tell me more. What are the typical questions people like you work on?
Alice: I am glad you asked, but I do not want to bore you too much.
Bob: (Laughing) Well the night is still young, and I feel that we are on the same wavelength. So, go ahead.
Alice: Well, some of my colleagues still work on understanding what can be possibly computed in principle or with certain bounds on the amount of the resources at our disposal. You know, some problems can in principle be solved using a computer, but in practice this would require more time than the age of the universe. Others develop increasingly sophisticated algorithms for solving computational problems. These are the algorithms that, for instance, allow you to search for a lot of the information you need using Google in less than no time, schedule many of the aspects of the daily life of our city as well as the timetable of the classes that we took at university. Do you drive a car?
Bob: Sure, but not tonight. (Laughs)
Alice: Well, the functioning of many of your car's features relies on the algorithms these colleagues of mine develop as well as on the analysis techniques that others have proposed for making models of the behaviour of the ABS system in your car, say, for describing its expected properties and for checking that the system affords the properties on your wish list. You do expect your car's airbag to inflate immediately after a crash, do you? (Alice smiles.)
Bob: Sure I do! (He smiles back.)
Alice: Then it's on the work of people like me your trust is based. And we haven't even started talking about computational learning theory, information theory, global computing and the design of the internet markets you use and inhabit. Did you know that thanks to innovations in learning theory developed by theoretical computer scientists automated search and data selection methods have become indispensable in a growing number of fields including yours? Computers can "learn"! And I have not yet told you about the theory of programming languages and the study of methods for describing what programs do when they compute.....
Bob: I think I need a little fresh air. Let's get out of here and take a walk. I am ready to hear your stories, but not in this noisy place.

Alice and Bob collect their jackets and head out. A full moon was lighting the sky and heard Alice ask: "Do you know that coding theory allows us to perform error-free transmission of information to and fro the spacecrafts that we send out to explore the solar system and beyond? Coding theory is also a very active area of TCS...."

Friday, February 20, 2009

February 2009 Issue of the BEATCS

The February 2009 issue of the Bulletin of the EATCS is now available, and is freely accessible to anyone interested in perusing it---as it should be for the bulletin of any professional organization whose aim is to further the development of its scientific area.

This issue of the Bulletin features the first contribution to a brand new column, The Algorithmic Game Theory Column, edited by Marios Mavronikolas. In a Greek relay team, Panagiota Fatourou takes over from him as the new editor of the Column on Distributed Computing, whose latest instalment is devoted to a piece on the theory of transactional memory.

There is much to read and enjoy, as usual. Readers might notice, however, that the Concurrency Column is missing. Mea culpa....

Tuesday, February 17, 2009

An Opinion Poll Related to the Bulletin of the EATCS

I append a questionnaire that I have helped put together in my role as chairman of the publication committee of the European Association for Theoretical Computer Science. The questionnaire will be sent out to all the past and present members (so some of you will receive it via email soon), but I'd also like to have the opinion of people in TCS who have never been members of the association. So, if you have time and/or interest in this matter, I'd be happy to receive a filled questionnaire from you or simply your answers to some of the questions. Use the comments section for submitting your input.

In case you wish to have a closer look, the Bulletin is freely available from this web page.

Let me remind you that people who registered for ICALP 2008 become members of the European Association for Theoretical Computer Science for a year. Becoming a member of the association is easy and cheap. See here.

--------------------------- QUESTIONNAIRE ------------------------



PART I: QUESTIONS RELATED TO THE POSSIBLE FUTURE DEVELOPMENTS OF THE BULLETIN OF THE EATCS


Note to the readers: Throughout the questionnaire BEATCS abbreviates Bulletin of the EATCS. Please return your answers in the comments section.
If you are already a member of the EATCS you will receive a copy of this questionnaire via email.
  1. Do you think that the quality of the Bulletin of the EATCS (henceforth, BEATCS) has increased over the last five years? YES/NO/DON'T KNOW
    1. If your answer is YES or NO, please state the reasons behind your answer.
  2. Are you aware that the Bulletin of the EATCS is an open-access publication? YES/NO
    1. If your answer is yes, how did you learn that the BEATCS is open access?
  3. Do you think that the BEATCS should remain open access? YES/NO
  4. Does the open-access status of the BEATCS influence whether you are a member of the EATCS? YES/NO
  5. How often do you read the BEATCS? NEVER/ONE ISSUE per year/TWO ISSUES per year/ALWAYS
  6. What parts of the BEATCS do you read?
  7. What are your areas of scientific interest?
  8. Do you think that the present contents of the BEATCS cater for the need of its readers and of the new generations of the TCS community as whole?
  9. Is there any topic to which you think that the BEATCS should devote a new column?
  10. If you are missing something in the BEATCS, what is it and what are your suggestions?
  11. What do you think of the overall scientific quality of the columns in the BEATCS? VERY LOW/LOW/ACCEPTABLE/GOOD/VERY GOOD/EXCELLENT
    1. Is there any column that you find particularly good?
    2. In your opinion, is there any column whose quality needs to be improved substantially?
  12. What do you think of the overall scientific quality of the contributed research articles? VERY LOW/LOW/ACCEPTABLE/GOOD/VERY GOOD/EXCELLENT
  13. At present, the BEATCS has light reviewing for columns, in the sense that the column editor reviews contributions by guest columnists, and a rather informal reviewing of technical contributions by the Bulletin editor. Do you think that the BEATCS should strive to set up a more formal peer-review process for the contributions that are published as columns and/or for the technical contributions?
  14. Do you think that the BEATCS should be indexed regularly by DBLP, ISI, and MathSciNet?
  15. Should the BEATCS be transformed into a new journal-type publication with peer refereeing etc., and with most newsletter-style content transferred to the EATCS web site?
  16. What could the BEATCS learn from publications like CACM and the Notices of the AMS?
  17. To your mind, what is the flagship journal publication of the TCS community, i.e., the most representative journal mostly devoted to TCS?
  18. To your mind, is the BEATCS suitable as the flagship publication of the EATCS?
  19. To your mind, what is the most useful service that the BEATCS should provide to the TCS community?
PART II: ADDITIONAL QUESTIONS RELATED TO EATCS MEMBERSHIP
  1. If you are a member of the EATCS, please state your main reasons for joining the organization.
  2. If you are not a member of the EATCS, Please state your reasons for not joining the organization.
  3. If you are missing something in the EATCS, what is it and what are your suggestions?

Friday, February 13, 2009

EATCS Award 2009 to Gérard Huet

The EATCS Award for 2009 will go to Gérard Huet. See the official announcement here. The Award will be assigned during a ceremony that will take place in Rhodes (Greece) during ICALP2009 (July 5-12, 2009).

The nomination singles out the following contributions by Huet.
  • In the early 70's, Huet developed both resolution and unification for higher-order logic: these results have became the core of several modern systems that perform deduction in higher-order logic.
  • Huet has done fundamental research in the areas of rewriting and Knuth-Bendix completion. His writings in this area are extensive and elegant. - Between 1982 and 1989, Huet directed and contributed to the design and implementation of the CAML functional programming language. That language and its descendants have given academics and industries an efficient and well structured programming language.
  • In the 1990s, Huet and his students designed and built the first version of the Coq proof assistant. Today, Coq is one of the most used and trusted platforms for formalized mathematics and formal methods.
Congratulations to Huet and to French TCS, which has given and still gives important contributions to our field.

Friday, February 06, 2009

More Reading on Bibliometric Data

In a recent post, I advertised a critical note on the (ab)use of bibliometric data subscribed by all the members of the editorial board of the journal Mathematical Structures in Computer Science.

Similar concerns have been raised by others. See, e.g., the talk "Bibliometric Evaluation of Computer Science - Problems and Pitfalls" by Friedemann Mattern (Institute for Pervasive Computing, Department of Computer Science, ETH Zurich).

There is also a very interesting joint report from three mathematical boards, which is definitely worth reading.

Finally, the "Sector Overview Report from the Computer Science and Informatics Sub-Panel (UoA 23)" after the British nationwide "Research Assessment Exercise 2008" (available at http://www.rae.ac.uk) includes the following passage:

We frequently found that citation counts were poorly correlated with the sub-panel’s assessment of the impact of the work examined. Citations also varied widely between research areas. For instance, much of the highly significant theoretical research, in which the UK is world leading, typically attracts low citation counts. Despite these low citations, the work is often found to have profound long-term impact on practical aspects of the field.

(The emphasis is mine and is not present in the original text.)

I hope that some of you will find these contributions interesting. I thank Catuscia Palamidessi and Vladimiro Sassone for pointing them out to me.

Thursday, February 05, 2009

A Couple of Papers on Structural Operational Semantics

begin rant

I like to think that I am not a procrastinator by nature and I try (but often fail) to apply Littlewood's zero-infinity law in my work, but am I the only one who feels that the number of things to do keeps increasing while the available time to carry them out decreases very fast?

end rant

One of the many things that I have been struggling to get done on time in this hectic early 2009 was a report on the first year for one of my ongoing grants. This reminded me of two papers I recently co-authored that I had meant to mention on this blog. Both papers offer a modest contribution to the meta-theory of Structural Operational Semantics.

Structural Operational Semantics (SOS) was introduced by Gordon Plotkin as a logical and structural approach to defining operational semantics for programming and specification languages. The logical structure of SOS specifications supports a variety of reasoning principles that can be used to prove properties of programs whose semantics is given using SOS. Moreover, SOS language specifications can be used for rapid prototyping of language designs and to provide experimental implementations of computer languages. Thanks to its intuitive appeal and flexibility, SOS has become the de facto standard for defining operational semantics, and a wealth of programming and executable specification languages have been given formal semantics using it.

The meta-theory of SOS provides powerful tools for proving semantic properties for programming and specification languages without investing too much time on the actual proofs; it offers syntactic templates for SOS rules, called rule formats, which guarantee semantic properties once the SOS rules conform to the templates (see, e.g., the papers in this bibliography maintained by MohammadReza Mousavi). In some sense, this is akin to an axiomatic development of the theory of operational semantics. One devises some rule patterns (the aforementioned rule formats) that "axiomatize" sufficient syntactic conditions guaranteeing that all programs in a language afford some desirable semantic property.

There are various rule formats in the literature for many different semantic properties, ranging from basic properties such as commutativity and associativity of operators, and congruence of behavioral equivalences to more technical and involved ones such as non-interference and (semi-)stochasticity.

The most recent paper I wanted to mention here is entitled Rule Formats for Determinism and Idempotency and is coauthored with Arnar Birgisson, Anna Ingolfsdottir, MohammadReza Mousavi and Michel Reniers. (An extended abstract of this work will appear in the Proceedings of Third FSEN: IPM International Conference on Fundamentals of Software Engineering (FSEN09), Iran, April 15-17 2009. Lecture Notes in Computer Science, Springer-Verlag, 2009.) In that paper, we propose rule formats for two properties, namely, determinism and idempotency of binary operators. In hindsight, it is quite surprising that no rule format guaranteeing determism had been proposed before. After all, determinism is a natural and important semantic property, which holds for sub-languages of many process calculi and programming languages, and is also a crucial property for many formalisms for the description of timed systems---where time transitions are required to be deterministic, because the passage of time should not resolve any choice.

Idempotency is a property of binary composition operators requiring that the composition of two identical specifications or programs will result in a piece of specification or program that is equivalent to the original components. Idempotency of a binary operator f is concisely expressed by the following algebraic equation.

f (x, x) = x

Determinism and idempotency may seem unrelated at first sight. However, it
turns out that, in order to obtain a rule format for idempotency that is sufficiently general to cover the special cases we wanted to cover, we need
to have the determinism of certain transition relations in place. Therefore, having a syntactic condition for determinism, apart from its intrinsic value, results in a powerful, yet purely syntactic framework for idempotency.

The second paper, On the Expressibility of Priority (Information Processing Letter 109(1):83-85, 2008), is joint work with Anna Ingolfsdottir. It is more modest in scope and offers results confirming that the priority operator of Baeten, Bergstra and Klop cannot be expressed using positive rule formats for operational semantics. Although expected, this inexpressibility result does not seem to have appeared before in the literature.

Overall, I really enjoyed working on those two papers. Thanks to my coauthors (old and new) for having given me the opportunity to work with them on these projects.