COMP 317: Semantics of Programming Languages

Logic and Computation

These notes introduce Hoare Logic as a way of specifying an axiomatic semantics of imperative programs. Axiomatic semantics is concerned with logical properties of programs: Hoare Logic describes the meaning of programs (more indirectly than either operational or denotational semantics) by saying what can be said about the states before and after a program is executed. Hoare Logic is an example of a formal logic; in order to explain formal logics in general, and Hoare logic in particular, we begin with a historical review of logic, biased towards a view of formal logics as games that have nothing whatsoever to do with Truth. This gap (even: antithesis) between formality and truth is best illustrated by examining the origins of formality in logic as a process that begins with the use of formality to help explain truth, and ends with an abortive attempt to capture or constrain truth within a formal system. The story begins in ancient Greece.

Aristotle

Aristotle
The formal study of logic begins with Aristotle, in Athens in the 4th century BC. At this time, the modern Western political and intellectual world was being invented, and active participation in the democratic institutions of government was seen as the duty of all citizens. Because power lay in public institutions, an individual's own interests could be served by swaying public opinion; so oratory and rhetoric were important elements of this fledgeling democracy. Speech-making and argumentation formed an important part of the education of young Athenian men (democracy didn't extend to females). And if you weren't skilled in these arts, you could always hire someone who was, to present your arguments for you. Around this time, there arose a school of rhetorical philosophers called sophists, who emphasised the skills of oratory in the presentation of subtle arguments (often emphasising rhetoric and subtlety at the expense of truth or reasonableness - the term "sophistry" still has negative connotations to this day).

Aristotle was concerned with argumentation that paid more than lip service to truth, and developed what we now call "deductive logic". He developed formal ways of deducing true statements from other true statements, in the form of syllogisms. An example of a syllogism is:
 

All men are mortal.
Socrates is a man.
Therefore: Socrates is mortal.

 
The first two sentences are called the premises; the third is called the conclusion. This is a rule of deduction: given the premises, we can deduce the conclusion. Aristotle identified about sixteen different forms of syllogism that allowed valid argumentation: "valid" in the sense that the conclusion is true if the premises are. The great contribution that Aristotle made with syllogisms, the reason why we can say that these are the beginning of formal logic, is that they explicitly identify the syntactic form of sentences. A schematic form of the above syllogism is:
 
All P are Q.
X is P.
Therefore: X is Q.

 
Aristotle formulated his syllogisms in this sort of schematic form; the advantage of this is that it clearly emphasises the nature of deduction in a way that abstracts from the actual content of the argument. These syllogisms represent valid forms of reasoning: the conclusion follows from the premises, regardless of what the individual sentences say. For example, one or both of the premises may be false, in which case the conclusion may or may not be true; however, if the premises are true, then so too is the conclusion.

In summary, Aristotle's syllogisms give schematic, syntactic rules for constructing valid arguments. These syllogisms prefigure the rules of deduction in modern formal logics. In the ancient Greek world, the deductive method was further developed by Euclid and others in the field of geometry. Euclid's Elements of Geometry presents a rigorous, if not entirely formal, account of plane geometry using a deductive style: from postulates (or "axioms", such as: parallel lines do not intersect) and constructions (the "ruler and compass" constructions of using two points to determine a line or circle), true statements of geometry are deduced; moreover, once these theorems have been proved they can be used in proving further true statements.

Leibniz

The great advances in logic made by the ancient Greeks were not matched for two thousand years. Aristotle's syllogisms were certainly influential, but became almost fossilised: in the scholastic period, undergraduates at Oxford University could be fined for arguments that contravened the valid syllogisms. Given that mathematics and philosophy continued to advance without the benefit of formal, syntactic methods, it might have seemed as though formalism was a dead-end: arid, irrelevant and unproductive. Nevertheless, formal approaches promised great pay-offs. In the seventeenth century, Gottfried Leibniz envisioned a formal language, a calculus, that would capture and embody all truth and valid reasoning. He called this the characteristica universalis:

All our reasoning is nothing but the joining and substituting of characters, whether these characters be words or symbols or pictures.... If we could find characters or signs appropriate for expressing all our thoughts as definitely and as exactly as arithmetic expresses numbers ... we could in all subjects in so far as they are amenable to reasoning accomplish what is done in arithmetic and geometry. For all inquiries that depend on reasoning would be performed by the transposition of characters and by a kind of calculus.... And if someone would doubt my results, I should say to him: `let us calculate, Sir,' and thus by taking to pen and ink, we should soon settle the question.
 

Leibniz was not concerned merely with a language for formal reasoning in mathematics. Anticipating by more than three hundred years the kind of predictions that earned Artificial Intelligence a reputation for hyperbole, Leibniz wrote:

I believe that a number of chosen men can complete the task within five years; within two years they will exhibit the common doctrines of life, that is, metaphysics and morals, in an irrefutable calculus.

The advantages of formal logic are clearly set out here: certainty, irrefutability, and the possibility of mechanical verification. Although Leibniz worked on the characteristica universalis, he was not able - obviously - to bring his ideas to fruition.

Boole

George Boole laid the foundations of what we now call the Propositional Calculus in a small book rather ambitiously entitled An Inquiry into the Laws of Thought .... This book concentrated on the algebraic properties of the logical connectives (and, or, implies, not), and their relationships to other familiar mathematical operations, such as set-theoretic union and intersection. For example, logical conjunction (and) corresponds to intersection and logicals disjunction (or) to union: thus any object x is an element of the union of sets
 


 
if and only if x is an element of A or x is n element of B. Moreover, intersection and union have the same algebraic properties as conjunction and disjunction (for example, A and A is the same as A, just as the intersection of a set A with itself is just A. Boole's contribution to Computing Science lay in the discovery that the logical connectives shared the same algebraic properties as arithmetic modulo 2 (where the only numbers are 0 and 1, and 1+1=0), which meant that logic could be carried out with the binary logic familiar from courses in circuit design: the logical conectives are implemented by gates (and-gates, or-gates, etc.). Again, the insight is that the logical connectives share the same algebraic properties as addition, multiplication, etc., when carried out modulo 2. In this case, the relationship allows us to define the logical connectives by means of their truth tables. The following tables use "0" for false and "1" for true:
 

 
Here we see that, modulo 2, conjunction acts like multiplication, negation like adding 1, disjunction like maximum ("exclusive or" is like addition), while implication is just strange ("A implies B" is the largest number n such that A times n is less than or equal to B, modulo 2 of course).

The great contribution of Boole's Laws of Thought is that it identifies the logical connectives as sharing the same algebraic properties as other mathematical operations. This furthers a formal approach to logic, where the validity of an argument is abstracted from its content: in this case, validity is just a result of the algebraic properties of the logical connectives. Structures that have the algebraic properties of the logical connectives are nowadays called Boolean Algebras, and play an important role in so-called "Intuitionistic" logics (where, generally, sentences can be true, false, or somewhere inbetween).

Hilbert

David Hilbert
David Hilbert was one of the foremost mathematicians at the turn of the nineteenth century. At the Second International Congress of Mathematicians in 1900, Hilbert set out what he saw as the most important open problems of the time. Among these was the development of a formal logical basis for mathematics. At the time, Cantor and others were developing set theory, which promised a formal account of basic mathematical objects and constructions, but the early stages of its development were plagued with various paradoxical results. It was clearly desirable to have a formal basis for the fundamental notion of set, since mathematical objects such as integer and real numbers could be represented by sets. Moreover, a formal logical approach to set theory would provide a formal touchstone for the truth or validity of mathematical reasoning. Formal proofs would be, like the Leibniz's characteristica universalis, mechanically verifiable, and the validity of a sufficiently detailed mathematical argument would therefore be transparent.

Peano

Giuseppe Peano

Russell and Whitehead

Bertrand Russell sought to provide a solution to Hilbert's open problem.

Gödel

Kurt Gödel
Kurt Gödel did provide a solution to Hilbert's problem: a negative solution.

Après Lui, La Déluge: local language games


The Propositional Calculus:

A logic that says nothing at all about anything


The Predicate Calculus


Hoare Logic

See this summary of the rules of Hoare Logic.

The example proof from Thursday's lecture:
 


 
See also some slides (PDF) from the lecture illustrating the construction of the proof.

When we looked at operational and denotational semantics, we saw that the compositional nature of those semantics allowed us to easily add new syntactic forms to the programming language and then extend the semantics to those new forms. Is it possible to do the same thing with Hoare Logic? To a certain extent, it is. Consider, for example, if-then programs of the form
 

if b then c .
 
From the operational or denotational semantics of these programs, we could show that programs of the above form are equivalent to:
 
if b then c else skip .
 
We can use this equivalence to derive a rule of inference in Hoare Logic as follows. Suppose we want to conclude something of the following form:
 
{ A } if b then c { B } .
 
From the equivalence given, we can conclude this iff we know:
 
{ A } if b then c else skip { B } .
 
We might then build up a partial proof tree, using the rules of Hoare Logic as far as we can:
 

 
Although this is an incomplete, and schematic, proof-tree, we know that if the leaves of this tree are true, then so is the root, because we built the tree using the rules of inference of Hoare Logic. In other words, the conclusion is valid if we take the leaves as premises; so we have derived the following rule of inference for if-then programs:

Grant Malcolm
Last modified: Sun Nov 3 23:27:00 GMT 2002