Lecture
Logic in computer science spans the overlapping fields of logic and computer science. In essence, this subject can be divided into three main areas:
Logic plays a fundamental role in computer science. Some of the key areas of logic that are of particular importance are computability theory (formerly called recursion theory), modal logic and category theory. The theory of computation is based on concepts defined by logicians and mathematicians such as Alonzo Church and Alan Turing. Church first showed the existence of algorithmically unsolvable problems using his notion of lambda-definability. Turing gave the first convincing analysis of what may be called a mechanical procedure, and Kurt Gödel asserted that he found Turing's analysis «perfect». In addition, some other core areas of the theoretical intersection of logic and computer science are:
One of the first applications to use the term «artificial intelligence» was the Logic Theorist system, developed by Allen Newell, J. C. Shaw and Herbert Simon in 1956. One of the things a logician does is take a set of logical statements and derive their conclusions (additional statements) that must conform to the laws of logic. For example, given a logical system that states «All men are mortal» and «Socrates is a man», the correct conclusion would be «Socrates is mortal». Of course, this is a trivial example. In real logical systems the statements can be numerous and complex. From the very beginning it became clear that this kind of analysis could be significantly aided by the use of computers. The Logic Theorist confirmed the theoretical work of Bertrand Russell and Alfred North Whitehead in their influential work on mathematical logic titled Principia Mathematica. In addition, logicians used subsequent systems to verify and discover new logical theorems and proofs.
Mathematical logic has always had a strong influence on the field of artificial intelligence (AI). From the very beginning of work in this field it was understood that the technology of automating logical inference could have great potential for solving problems and drawing conclusions from facts. Ron Brachman described first-order logic (FOL) as the metric against which all AI knowledge-representation formalisms should be evaluated. There is no more general or powerful known method for describing and analyzing information than FOL. The reason FOL is simply not used as a computer language is that it is in fact too expressive, in the sense that FOL can easily express statements that no computer, regardless of its power, could ever solve. For this reason, every form of knowledge representation is in a certain sense a compromise between expressiveness and computability. The more expressive the language, the closer it is to FOL, the more likely it is to be slower and prone to infinite loops.
For example, the IF-THEN rules used in expert systems correspond to a very limited subset of FOL. Instead of arbitrary formulas with the full set of logical operators, the starting point is simply what logicians call modus ponens. As a result, rule-based systems can support high-performance computing, especially if they take advantage of optimization and compilation algorithms.
Another important area of research in logical theory has been software engineering. Research projects such as the Knowledge Based Software Assistant and the Programmer's Apprentice programs applied logical theory to verify the correctness of software specifications. They also used it to transform specifications into efficient code on various platforms and to prove the equivalence of an implementation and a specification. [10] This formal, transformation-based approach often requires much more effort than traditional software development. However, in certain domains with appropriate formalisms and reusable patterns, this approach has proven viable for commercial products. Suitable domains are usually those such as weapons systems, safety systems and real-time financial systems, where a system failure has excessively high human or financial costs. An example of such a domain is very-large-scale integration (VLSI) design—the process of designing the chips used for processors and other important components of digital devices. An error in a chip is a catastrophe. Unlike software, chips cannot be patched or updated. As a result, there is a commercial justification for using formal methods to prove that an implementation conforms to a specification.
Another important application of logic in computer technology has been in the field of frame languages and automatic classifiers. Frame languages such as KL-ONE have rigid semantics. Definitions in KL-ONE can be directly mapped to set theory and the predicate calculus. This allows specialized theorem provers called classifiers to analyze various declarations among sets, subsets and relations in a given model. In this way the model can be verified and any inconsistent definitions flagged. The classifier can also infer new information, for example define new sets based on existing information and change the definition of existing sets based on new data. This level of flexibility is ideal for working in the constantly changing world of the Internet. Classifier technology is built on top of languages such as the Web Ontology Language to provide a logical semantic layer over the existing Internet. This layer is called the Semantic Web.
Temporal logic is used for reasoning about concurrent systems.
The following main applications are included:
Unlike the natural sciences, computer science has received a great stimulus from broad and continuous interaction with logic. A special role in computer science is played by proof-based methods for developing algorithms and programs together with proofs of their correctness.
Testing programs can detect the presence of errors in programs, but cannot guarantee their absence. Guarantees of the absence of errors in algorithms and programs can be provided only by proofs of their correctness. An algorithm contains no errors if it produces correct solutions for all admissible data.
A serious problem for computer science and informatics is the presence of errors in algorithms and programs published in textbooks and study guides, as well as the inability of computer science instructors and teachers to detect and correct errors in the algorithms and programs written by their students.
The only way to overcome these problems is to study systematic methods of composing algorithms and programs while simultaneously analyzing their correctness within the framework of proof-based programming, from the very start of teaching the fundamentals of algorithm design and programming.
The difficulty for instructors and programmers is that they must be able to write not only algorithms and programs, but also proofs of the correctness of their algorithms and programs. Unfortunately, at present neither mathematicians nor programmers are able to do this.
As a result, programmers write programs with a large number of errors that they can neither detect nor correct. Massive program testing brings programmers undoubted benefit, but does not guarantee the complete elimination of errors.
The practice of applying and studying proof-based methods of programming has shown that this technology is quite accessible to students of mathematics faculties, who are quite capable of writing proofs of the correctness of algorithms, after checking and testing the programs on a computer.
The greatest effect in mastering proof-based programming technologies is observed in computer science and programming olympiads, where the winners and prize-holders are those students who have mastered the technique of testing programs and composing algorithms and programs without errors.
Computer science as a discipline began to take shape together with the creation and rapid development of computing technology. Its formation and the definition of its subject matter continue to the present day. Computer science is the science of storing, processing and transmitting information with the help of computers. It comprises large sections that study the algorithmic, software and hardware means of storing, processing and transmitting information. Mathematical logic turned out to be the only mathematical science whose methods have become powerful instruments of knowledge in all sections of computer science. Therefore, any at all serious study of computer science is inconceivable without mastering the foundations of mathematical logic.
For a computer to work, it must be equipped with software, that is, with a set of programs that direct the computer toward solving problems of one class or another. The word «program» is of Greek origin and means «announcement», «instruction». The very concept of a computer program, which provides for a precise algorithmic prescription to the computer about the order and nature of actions, already implies the penetration into the program, as well as into the process of its assembly (into programming), of the theory of algorithms.
But upon closer examination, the process of the penetration of logic into programs and programming turns out to be much deeper and more organic. Not only does a single section of the theory of algorithms operate here, but the very essence of mathematical logic—its language, its axiomatic theories, the inferences and theorems within them, the properties of these theories—proves to be exceptionally effective.
The theory of algorithms and mathematical logic are the fundamental basis of programming. In the 1830s the English mathematician Charles Babbage first put forward the idea of a computing machine. And only a hundred years later logicians developed four mathematically equivalent models of the concept of an algorithm. It was precisely in the theory of algorithms that the basic concepts were foreseen which formed the basis of the principles of constructing and operating a program-controlled computing machine and the principles of creating programming languages. The idea of such a computing machine was first realized by the Bulgarian scientist J. Atanasoff in 1940 and the German scientist K. Zuse in 1942. The four principal models of the algorithm gave rise to different directions in programming.
Mathematical logic began to develop rapidly at the beginning of the 20th century on the ground of the seemingly extremely application-remote problem of the foundations of mathematics. But it was precisely this research that laid the beginning of a rigorous definition of algorithmic languages, revealed their colossal possibilities and fundamental limitations, and developed the technique of formalization. Therefore, when it was realized in programming that every program is a formalization, the mathematical problems that arose here fell on ground carefully prepared by mathematical logic.
The first attempts to apply developed logical calculi and formalization methods in programming were made by the American logician H. B. Curry. In 1952 he delivered a report titled «The logic of program composition», whose ideas were ahead of their time by at least a quarter of a century. Curry regarded the task of programming as the task of composing large programs from ready-made pieces. Two basic systems of constructs were introduced: the first—sequential execution, branching and loop; the second—sequential execution and conditional jump. He characterized the logical means that can be used to compose programs from subprograms in each of these cases.
As is well known, the computer is a kind of «ideal bureaucrat»: it will not accept a program written in a not fully formalized language, and will begin work only after everything has been expressed in full accordance with detailed instructions. Therefore in the 1960s the tasks of precisely defining formal languages of a sufficiently complex structure came to the fore. Mathematical logic, supported by the ideas of programming, successfully coped with them and developed a description of the syntax of complex formal languages rich in expressive means.
In the mid-1960s a number of pioneering works in the field of describing the conditions that a program satisfies appeared practically simultaneously. The Soviet mathematician V. M. Glushkov in 1965 introduced the concept of an algorithmic algebra, which served as a prototype of algorithmic logics. E. Engeler in 1967 proposed using languages with infinitely long formulas in order to express the infinite set of possibilities arising during various executions of a program. But the greatest fame was gained by the languages of algorithmic logics. These languages were invented practically simultaneously by the American logicians R. W. Floyd (1967) and C. A. R. Hoare (1969) and by scientists of the Polish logical school, for example A. Salwicki (1970) and others.
Algorithmic logic (also dynamic logic, or program logic, or Hoare logic) is a branch of theoretical programming within which axiomatic systems are studied that provide means for specifying the syntax and semantics of programming languages, as well as for synthesizing computer programs and their verification (checking the correctness of their operation). The languages of algorithmic logics are based on first-order predicate logic and include statements of the form {A} S {B}, read as follows: «If before the execution of operator S the condition A held, then after it B will hold». Here A is called the precondition, B the postcondition, or promise of S. In this language, logical descriptions are given of the assignment and conditional-jump operators, branching, and the loop.
Alongside first-order dynamic logic, propositional dynamic logic and its generalizations are considered—the so-called process logic, which expresses certain properties of a program that depend on the process of its execution. Various dynamic logics are obtained by varying the programming language means used in programs. These means include arrays and other data structures, recursive procedures, loop constructs, as well as means for specifying nondeterministic programs.
Dynamic logic is one of the types of logical systems used for the logical synthesis of computer programs. Logical synthesis—one of the ways of moving from a program specification to a realizing algorithm—takes the form of precise reasoning in some logical system. In dynamic logic the specification of a problem is given in the form of two predicate-calculus formulas—the precondition and the postcondition—while the axioms of the logical system are schemes of preconditions and postconditions linked by one or another programming language construct. The synthesized program emerges in the form of an assertion derived in dynamic logic, which states that if the arguments of the problem satisfy the given precondition, then the result of executing the synthesized program satisfies the given postcondition.
In theoretical works on dynamic logics, questions of the consistency and completeness of axiomatic systems, algorithmically complex properties of sets of true formulas, and the comparison of the expressive power of dynamic-logic languages are investigated.
A fundamentally different way of defining the semantics of programs, suitable rather for describing an entire algorithmic language than specific programs, was proposed in 1970 by the American logician D. Scott. He constructed a mathematical model of the λ-calculus and showed how to translate a functional description of a structured programming language into the λ-calculus and how to define a mathematical model of an algorithmic language through the model of the λ-calculus. This so-called denotational semantics of algorithmic languages became a practical tool for building reliable translators from complex algorithmic languages. Thus yet another abstract area of mathematical logic found direct practical applications.
Programming is the process of composing a program, a plan of action. It has been noted that classical logic is poorly suited for describing this process, if only because it is generally poorly suited for describing any process in mathematics. Already at the beginning of the 20th century it became clear that in mathematics the concepts of «to exist» and «to be constructed», which since ancient times had been treated as synonyms, had long diverged. The so-called mathematical objects—«ghosts» (sets, functions, numbers)—were discovered, whose existence has been proved but which cannot be constructed. The cause of their appearance was the effect of combining classical logic with Gödel's theorem on the incompleteness of formal arithmetic. One of the fundamental laws of classical logic—the law of the excluded middle (P ∨ ¬P)—in a certain loose interpretation in effect means that we know. This postulate can of course by no means be called realistic: we know very little, and the more we learn, the better we understand this. The Dutch mathematician L. E. J. Brouwer identified the logical roots of the «phantoms», even before the discovery of Gödel's theorem, in 1908, and began the construction of the so-called intuitionistic mathematics, which does not accept the law (P ∨ ¬P) as universal. In 1930–1932 another Dutchman, A. Heyting, rigorously formulated the logic that was used in intuitionistic mathematics—intuitionistic logic. Its mathematical interpretation, set forth by the Soviet mathematician A. N. Kolmogorov, has retained its significance to this day.
A. N. Kolmogorov regarded logic as a calculus of problems. Each formula of the algebra of propositions is regarded not merely as a formula, but as a requirement to solve a problem, that is, to construct an object satisfying certain conditions. This is the so-called constructive interpretation of propositional logic. Logical connectives are understood as means for constructing formulations of more complex problems from simpler ones, axioms as problems whose solution is given, and inference rules as ways of transforming solutions of some problems into solutions of others. Note that the solution of a problem is not only the sought object itself, but also a proof that it satisfies the requirements imposed. For example, the formula A∧B is understood in the Kolmogorov interpretation as the problem consisting in constructing a solution of problem A and a solution of problem B; the inference rule A, B / A∧B as the transformation which, from an object a, a solution of problem A, and an object b, a solution of problem B, produces the pair (a, b), a solution of problem A∧B. An object a that solves the problem associated with the formula A is called a realization of A. This fact is denoted a R A. The central point of the constructive understanding of logical formulas is the interpretation of implication. The constructive implication A → B is understood as the requirement to construct an effective transformation f, applied to all realizations of formula A and mapping them into realizations of formula B.
The fuzzy Kolmogorov formulation of logic as a calculus of problems gave rise to numerous different concretizations, yielding a whole system of precise mathematical definitions. This formulation found application not only in intuitionistic logic, for which it was created, but also in other logical systems. Rigorous mathematical semantics based on Kolmogorov's idea are usually called realizability semantics (in contrast to other kinds of logical semantics based on systems of truth values). The first realizability was constructed by the American logician S. C. Kleene in 1940 for arithmetic with intuitionistic logic. In the 1960s–1980s dozens of notions of realizability appeared, both for systems based on intuitionistic logic and for other logics. The Soviet logician A. A. Voronkov in 1985 derived conditions under which classical logic can be regarded as constructive. From them it follows, in particular, that a necessary (but not sufficient) condition for the constructivity of a classical theory is its completeness, that is, the derivability in it, for each closed formula F, of either F itself or its negation ¬F. This once again confirmed Brouwer's insight into the logical roots of nonconstructivity. Note that examples of classical theories that have a constructive interpretation are elementary geometry and the algebraic theory of real numbers.
The description of programming with the help of logic is based on a certain analogy between the derivation of a formula in some logical calculus and a program for solving the problem corresponding to that formula under the constructive interpretation of logic. The logical theory corresponding to structural schemes of programs appeared in the mid-1980s. Structural schemes matched an emerging new type of logic—the logic of program schemes, which a programmer uses to create complex, multivariant, iterative plans of action.
The wide use of computers in various spheres of human activity raises the question of the reliability of computer software. As is well known, the correctness of a created program is usually checked on a number of so-called test cases, on initial data for which the result is known or can be predicted. It is not hard to understand that such a check is capable only of revealing the presence of errors in a program, but not of proving their absence.
Therefore the task of rigorously proving the correctness of programs is exceptionally important, and it was precisely for this purpose that program and dynamic logics began to be developed.
From an intuitive point of view, a program will be correct if, as a result of its execution, the result is achieved for the purpose of obtaining which the program was written. Proving the correctness of a program consists in presenting such a chain of arguments as convincingly testify that this is indeed so, that is, that the program actually solves the posed problem.
Let us now formulate a precise definition of the concept of program correctness. Let α be a program, P an assertion relating to the input data that must be true before the execution of program α (it is called the precondition of program α), Q an assertion that must be true after the execution of program α (it is called the postcondition of program α). Two kinds of program correctness are distinguished: partial and total (full). A program α is called partially correct with respect to precondition P and postcondition Q if, each time that before the execution of α the precondition P is true for the input values of the variables, and α terminates, the postcondition Q will also be true for the output values of the variables. In this case we shall use the notation P [α] Q. A program α is called totally correct with respect to P and Q if it is partially correct with respect to P and Q, and α necessarily terminates its work for input values of the variables satisfying condition P. In this case we write P [α!] Q.
Let us note that the concept of the correctness of a program α is formulated with respect to the corresponding assertions (conditions) P and Q. Therefore, from the truth of the assertion P [α] Q (or P [α!] Q respectively) the truth of an assertion about the correctness of the program under other preconditions and postconditions does not necessarily follow. Similarly, replacing in P [α] Q (or P [α!] Q) the program α by a program β generally does not preserve the truth value of the assertion about correctness. Nor should one think that under given conditions P and Q there exists only one program α for which the statement P [α] Q (or P [α!] Q) is true.
To speak of the correctness of a program in itself is meaningless. A program is written for the purpose of solving one or another specific problem. Every properly posed problem includes a condition (that which is given) and questions to which an answer must be given. When composing a program, the condition of the problem turns into a precondition, and the question turns into a postcondition, which already has the form not of a question but of an assertion that must be true whenever the answer to the problem's question is correct.
From the definitions it follows that every totally correct program is partially correct under the same preconditions and postconditions. The converse is of course untrue. It is clear that total correctness is «better» than partial, although proving the total correctness of a program is perhaps harder than the partial.
To prove the partial correctness of operator programs, various modifications of Floyd's method are usually used, which consists in the following. On the scheme of the program, control points are chosen so that any cyclic path passes through at least one point. With each control point a special condition (an inductive assertion or loop invariant) is associated, true at each passage through that point. With the entry and exit of the scheme, pre- and postconditions are also associated. Then to each path of the program between two neighboring control points a so-called correctness condition is assigned. The satisfiability of all correctness conditions guarantees the partial correctness of the program.
One of the ways of proving the termination of a program consists in introducing into the program additional counters for each loop and proving their boundedness in the process of proving the partial correctness of the program.
One of the modifications of Floyd's method consists in constructing a finite axiomatic system (the so-called «Hoare logic»), consisting of axiom schemes and inference rules, in which, as theorems, assertions about the partial correctness of programs are derived, in particular in the Pascal programming language. Such a system is also used to specify the axiomatic semantics of the Pascal language. Axiomatic systems related to Hoare logic have been developed for other algorithmic programming languages as well.
To prove the correctness of recursive programs, the method of mathematical induction is used, connected with the definition of the least fixed point, and for programs with complex data structures (for example, graphs, trees)—induction over the data structure. In doing so, theoretical investigations of Hoare logic consider the usual properties of axiomatizations in logic—their consistency and completeness.
Prescriptive (computational) algorithms can be represented by an informal description in the form of flowcharts. In these forms algorithms lend themselves more easily to analysis and verification.
Checking the correctness of an informal algorithm can be based on a logical model of the algorithm, the investigation of which can be carried out by formal logical methods.
In the program, control points are chosen, to which predicates are assigned that denote the state of the program.
A logical description of the semantics of a program:
1) if i and j — are the entry and exit of an operator vertex, then the transition from i to j — is an arc,
which is determined by the implication Qi(t1, t2, tn) —> Q;(l1,l2, ..ln), where li = f(t1 ..., tn) — is the designation of the corresponding transforma
tion performed by the operator;
For integer multiplication, an obvious simple algorithm of repeated summation is used 
.
To describe the algorithm a flowchart is used, in which A, B — are integers; A — the multiplicand; B — the multiplier; S — the product, which is computed by the indicated formula (fig. 5.2).
Fig. 5.2. Scheme of the algorithm for example 5.3
The formulas describing the scheme of the algorithm, in which the machine-state control points Qq, ..., Q6) are singled out:
The control invariant formulas in the algorithm:
Interpreting the formulas for specific initial data is equivalent to executing the program.
The task of analyzing the program is the following: to prove that, with bounded initial data, the program terminates in the state
Q6(A, B, S) && (B = 0), i.e.
Executing the program consists of the following steps:
1) substitution (interpretation) of the values of the variables after data input into the formula:
Symbolic testing and partial evaluation are used
for not fully defined data with the purpose of testing the algorithm. As a result of interpretation with partially defined data, a formula will be obtained that coincides with the original definition of the computation method.
Let us take the multiplicand A = a and the multiplier B = 3.
Interpretation of the algorithm in predicate logic:
The execution of the formula S = a • 3 = Σ= a + a + a is confirmed.
In traditional programming, control formulas are used, in which the state of the data is checked at specific points of the program. In programming languages such as C++ the assert operator is used (a logical formula with predicates); when this formula is interpreted, a flag (F or T) is formed that makes it possible to monitor possible errors in the input data and computations.
Comments