6.4. Formalization of the algorithm concept

Earlier, the basic requirements for algorithms were formulated. However, the concepts used in these formulations (such as clarity, clarity, elementarity) themselves need to be clarified. Algorithms in the intuitive sense are not mathematical objects, formal methods of research and evidence are not applicable to them. Therefore, in the XX century, attempts were made to formalize the concept of an algorithm. The formalization of the concept of an algorithm is necessary for various reasons. For example, a comparison of two algorithms in terms of efficiency, verification of their equivalence, etc., are possible only on the basis of their formal representation.

For the first time, the need for a formal concept of an algorithm arose in connection with the problem of the algorithmic insolubility of certain problems. For a long time, mathematicians believed in the possibility that all strictly posed mathematical problems could be solved algorithmically; all that was needed was to find an algorithm to solve them. The belief in the universality of algorithmic methods was undermined by the work of Kurt Gödel (1931), in which it was shown that certain mathematical problems could not be solved using algorithms from a certain class. This class of algorithms is determined by some formal specification of the concept of an algorithm. The question arose: are these problems algorithmically unsolvable only within the framework of the algorithm model used by Gödel, or is it impossible to come up with any algorithm to solve these problems in any sense? The generality of Gödel's result depends on whether the class of algorithms used by him coincides with the class of all algorithms in the intuitive sense. Therefore, the search and analysis of various refinements and formalization of the algorithm and the ratio of these formalizations with the intuitive concept of the algorithm is practically important.

To date, a number of formal models of the algorithm has been proposed. Kurt Gödel defined the algorithm as a sequence of rules for constructing complex mathematical functions from simpler ones, Alonzo Church used a formalism called λ-calculus , Alan Turing suggested a hypothetical automatic device, which is now called the Turing machine, and defined the algorithm as a program for this machine, A. A Markov defined the normal algorithm as a finite set of rules for substitutions of chains of characters, and so on.

An amazing scientific result is the proof of the equivalence of all these and several other formal definitions of the algorithm. The equivalence of two abstract models of the algorithm is that any class of problems that can be solved with the help of models of one type can be solved on models of another type (in fact, others can be expressed in one model). It turned out that all algorithms in the exact sense for these formal models are algorithms in the intuitive sense, and all known algorithms can be represented by algorithms in the exact sense (within these formalisms).

Based on these results, the following statement has been recognized in computer science: “Any reasonable definition of an algorithm that may be proposed in the future will turn out to be equivalent to already known definitions,” which means, in essence, the assumption that the concepts of an algorithm are adequate in an intuitive sense in one of the listed equivalent formalisms . This position is now widely used as a hypothesis, justified by the fact that it was not possible to find examples that contradict it. This hypothesis, however, cannot be rigorously proved, since the concept of an algorithm in an intuitive sense is informal.

Historically, Alonzo Church was the first to identify the intuitive concept of an algorithm with one of the exact definitions equivalent to each other. Alan Turing independently suggested that any algorithm in an intuitive sense can be represented by a Turing machine (and therefore, in any other equivalent form). This assumption is known as the Church –Turing thesis.

The definition of a Turing machine, among other equivalent definitions, seems most convenient for a formal definition of the concept of an algorithm.