Algorithms Fit for Compilation?

Most researchers differ in their workflow.  For researchers in the algorithms world (or at least, those I know), the work is in the design. Our hours are spent at the blueprint stage. Algorithms are designed, improved, reformulated, or reapplied in different problems, mostly on paper. But this is unarguably only the first stage in successfully developing a new algorithm. There are still the matters of proving and testing the algorithm, and submitting the result to the public. When are we done drafting our blueprint? How do we package and ship the blueprint to the engineers and construction team?

Let’s address the more straight-forward question first. What is the best way to present an algorithm? How descriptive and specific should it be? Should it be entirely self-contained or, for instance, could we have a pointer to a “… subroutine of choice”? Is implementability more important than readability?

In an introductory algorithms course, algorithms are often described as recipes, step-by-step instructions for obtaining the result of a calculation. However, it is often made explicit that algorithms are not pseudocode. Leslie Lamport developed the PlusCal algorithm language to address this notion explicitly. According to the description on his Microsoft Research page, the PlusCal language is for writing algorithms, as programming languages are meant for writing programs. Many LaTeX packages for writing algorithms specify that they should not be used to write pseudocode (although this might not be coincidental considering Lamport himself wrote LaTeX). His solution uses the language of mathematics, giving descriptions of procedures in terms of logical constructs. PlusCal is different from programming languages two important ways: it allows for nondeterminism and it makes analysis easy by keeping track of atomic steps. Lamport highlights these as some distinguishing features between algorithms and programs.

Of course, there is no need to present an algorithm unless we are sure of its correctness and power. This question may very well be the fire behind the algorithm/pseudocode distinction question. Without a mechanism for testing an algorithm, we are subject to proving its correctness only by hand. This leaves much room for error. So then, what are the tools for testing? Well, programs.

Lamport has a solution to this as well. Along with the PlusCal language, Lamport has designed the TLA+ specification language with tools for model checking and a TLAPS proof system. It is part of the Tools for Proofs project at Microsoft Research. During a recent talk at UCSD, Lamport explained that the model checking system of TLA+ has vastly improved his own work process and also makes collaboration much more comfortable.

Aside from attending his talk, I find myself asking these questions because, in writing an algorithm down, I almost reliably find errors in its design. Transcribing inevitably enables debugging. Even better is implementation! How can I be so sure of my algorithm if I myself cannot use it? So, this is part of my workflow. But what does this mean for my readers? Do I spare these details for a more pleasurable reading experience? After all, everyone has their own flavor of implementation. Or should I let the details given in the algorithm speak for themselves?

Lamport has his own answers to all of these questions. I am personally still in the development phase, but I feel it is important to begin a dialogue within the community. Developing a standard in the way of algorithms languages would improve productivity and remove ambiguity. A common language for algorithmists could even open up new doors of collaboration. If nothing else, it will some questions I have.

One thought on “Algorithms Fit for Compilation?

  1. Nice post. The language is well documented.

    ps: funnier than the phd comics at this magazine edition was the advertising of the NSA behind the “complexities of privacy and anonymity”.

Leave a Reply

Your email address will not be published. Required fields are marked *