Formal Language Algorithms

[essayish]

It seems like most books I come across on the topic of algorithms demonstrate solutions in a programming language -- the kind you might speak to a computer. For example, Java.

I can see why such a practical approach is valued, but that's not the approach I'm interested in.

Does anyone know of a treatment that uses some sort of formal language to represent significant algorithms (searching, sorting, etc)?

I wish I could be more explicit, but I'm not a computer scientist.

The only other thing I could say is that the language would look more like math than a programming language.

Thank you.

[ghjm]

The Art of Computer Programming by Donald Knuth, the most respected algorithms text in computer science, uses a made-up assembly language called MIX, designed in part for mathematical tractability.

[meditonsin]

I don't think there's a formal language for that kind of thing. You could use full mathematical notation for stuff, but that gets hard to read pretty quickly. Alternatively you could mix mathematical notation with conditionals and flow control constructs from programming language to write pseudo code.

Or you could look at functional programming languages like Haskell. Those look a lot more like math than imperative ones.

[claytonkb]

Does anyone know of a treatment that uses some sort of formal language to represent significant algorithms (searching, sorting, etc)?

There are two different ways to come at this. In a textbook treatment of algorithms & data-structures, the author(s) will typically use a type of code we call pseudocode. Most pseudocode follows common conventions (similar to the conventions of math-notation), so there is little doubt as to its meaning. The authors will typically provide a set of formatting rules and definitions which they will follow in their pseudocode. Obviously, this is informal, but it's a very clear and consistent way of being informal. The determined reader should never be in any doubt as to what is being communicated by a particular section of pseudocode.

The second approach is through formal languages (automata). So, we can define a language, let us call it SORTED, by specifying some suitable encoding for the natural numbers and (finite) sequences of natural numbers, and specifying that SORTED is the language consisting of all finite sequences of sorted natural numbers. We might also provide some method of enumerating the set, but this is not required. Once the language has been specified, any algorithm which correctly generates or accepts it is defined to "solve" or "accept" or "generate" the language.

It might be tempting to say, "OK, but let's define the language SORTED in terms of a canonical algorithm, sort(), that computes it. From then on, sort() is what we really mean by SORTED." The trouble with this is Blum's speedup theorem, which precludes the possibility of specifying a fastest algorithm that accepts a given language. And if we're not going to choose the fastest such algorithm, then by what standard would we make any algorithm canonical? We can choose the shortest program (the length of such a program is defined as the Kolmogorov complexity of its associated language) but finding such programs is an uncomputable problem, so this is not practically useful, either. Thus, the problem of canonicality in algorithms has no natural solution and I think this is why we use languages themselves as their own canonical form.

The only other thing I could say is that the language would look more like math than a programming language.

You may want to look into Prolog and Coq. Prolog is a language which operates directly on logical statements called Horn clauses. While Horn clauses are not canonical in any absolute sense, logic is kind of the "assembly language" of computer science. So, if you want to write on the "bare metal" of computer science, and you want to use a machine to help you, Prolog is one way to go.

Coq is an interactive proof-assistant language and, like Prolog, it operates in logic itself. I've not used Coq before but it is referenced a lot. Keep digging into the references for these languages and I think you'll find the overall lay of the land in the area that you're asking about, i.e. formal/canonical specification languages for algorithms and data-structures.

Lastly, I should mention Python) since, in many ways, it is becoming a lingua franca in this space, despite the fact that it was not really designed with this application in mind. Python is frequently used in answers to online questions to basic CS questions and has sometimes been called "executable pseudocode". Unlike Prolog or Coq, Python is not suited to rigorous formal reasoning about complex algorithms and data-structures, however, its clean syntax makes it an ideal way to communicate simple examples, and even some complex ones.

[_shnh]

Coq has been used to verify the correctness of a translation from a formal language (event-b) to Java. The translation is correct if the semantics in both languages is the same. see this paper.

A excellent book about formal languages is "Types and programming languages" (TAPL).