What is an Algorithm?
Introduction to Behavioral Computation Theory

Yuri Gurevich (6. Logic colloquium)
Microsoft Research, Redmond, WA


One may think that the title problem was solved long ago by Church and Turing but it wasn't; there is more to an algorithm than the function it computes. (Besides, what function does an operating system compute?) The interest to the problem is not only theoretical; applications include specification and verification of software and hardware.

In the main part of the talk, we formalize the notion of sequential algorithm, recall the definition of sequential abstract state machines (ASMs), and then state precisely the Sequential Characterization Theorem according to which, for every sequential algorithm A, there exists a sequential ASM B indistinguishable from A as far as behavior is concerned; in particular B simulates A step-for-step. The full proof of the theorem is found in the ACM Transactions on Computational Logic 1:1 (2000) or on the author's webpage (article 141).

If time allows, we will also discuss (a) generalizations of the Sequential Characterization Theorem to parallel and interactive algorithms? (b) the applications of the ASM approach at Microsoft.

Yuri Gurevich is Sr. Researcher at Microsoft Research in Redmond, WA. He is also Professor Emeritus of the University of Michigan, ACM Fellow, Guggenheim Fellow, and Dr. Honoris Causa of Limburg University in Belgium.