=0pt omitted tabular environment
which puts propositions and types on a par. This is sometimes called the Curry-Howard isomorphism, as William Howard (1968) identified it in Haskell Curry's work (1958), although Nikolas de Bruijn, Joachim Lambek, Hans Läuchli and Bill Lawvere also deserve credit for it in the late 1960s. The idea was developed by Dana Scott to give substance to Brouwer's intuition, and rather more extensively by Per Martin-Löf.
Formulae correspond to types and their deductions to terms. Crudely, a type gives rise to the proposition that the type has an element, and a proposition to the type whose elements are its proofs.
Indeed, as soon as we take some care over it, we have no alternative but to treat the hypothesis for Þ alongside the generic value of " and the bound variable of l. Similarly Sections 4.3 and 5.3 show that midconditions go with program-variables. Other analogies with types versus terms are games versus strategies, problems versus solutions and specifications versus implementations of programs.
Calling the analogy an isomorphism overstates the case. Terms may or may not satisfy equations, but proofs are anonymous: we do not usually bother either to equate or to distinguish between them. The difference between propositions and types is that the former are much simpler; we exploit this by treating them first, in Chapters I and III. Posets and induction concern propositions, categories and recursion are about types. (Some authors say proof-irrelevance instead of anonymity.)
The propositions as types analogy ought not to be confused with the earlier but superficial one between predicates and classes, which merely states the axiom of comprehension (Definition 2.2.3) in a fixed domain of discourse, and has no algorithmic content. Far more striking is Jan Lukasiewicz's re-evaluation of the history of logic in 1934 (in which he condemned earlier historians for their ignorance of the modern study of the subject): he attributed the identity on propositions ( f\vdashf) to the Stoics and that on terms (x:X\vdash x:X) to Aristotle.
EXAMPLE 2.4.1 The proofs of the proposition a® (a® a)® a may be characterised up to bh-equivalence by a number, viz the number of times modus ponens (® E ) is used.
These proofs correspond to the l-terms 0 = lx f.x, 1 = lx f.fx and 2 = lx f.f(fx), called the Church numerals (Exercise 2.44ff).
|
EXAMPLE 2.4.2 The Schönfinkel combinators are 1 #1 =2pt
omitted eqnarray* environment
These types are the axioms of implicational logic (Remark 1.6.10): I is the identity, K corresponds to weakening, S to contraction, T to exchange and Z to cut. Exercise 2.26 shows how to express any l-term using S and K alone; for example I = SKK and Z = S(KS)K. Proposition 2.8.6 gives further examples of the relationship between proofs and terms.
The correspondence What is the content of a proof?
REMARK 2.4.3 Arend Heyting and Andrei Kolmogorov independently gave this interpretation of intuitionistic logic in 1934. To prove
These may be read off from the rules of Sections 1.4, 1.5 and 2.3.
REMARK 2.4.4 In particular, the direct logical rules correspond to the operation-symbols of simple type theory:
Direct deductions are, then, sequences of declarations, ie assignments to intermediate variables of expressions which involve previously declared variables. The utility of the proof box method as a way of composing proofs lies in its similarity, under this correspondence, to the declarative style of programming, which we shall discuss in Section 4.3.=0pt
I I (a,b) E0(f) E1(f) I0(a) I1(b) E (f,a) a,b _0(f) _1(f) _0(a) _1(b) ev(f,a).
REMARK 2.4.5 The indirect rules correspond to l-abstraction, in which the bound variable is
In particular, the box lying above the (Þ Á )-rule is a program which transforms a given proof x of f into a proof p(x) of y, the proof of fÞ y being the abstraction lx.p(x). Conversely, the (Þ E )-rule applies the proof f of fÞ y to the proof a of f to yield a proof fa of y. If f was in fact lx.p then there is a b-reduction of (lx.p)a into p[x: = a], which is obtained by removing the box around p and replacing its hypothesis x with the given proof a (Remark 1.5.10).
WARNING 2.4.6 The l-calculus variables introduced in this translation of indirect rules denote proofs, not propositions. They do not occur in terms or predicates and can only be bound by l, not by " or $ . They should not be confused with the variables which denote elements of the object-language, occur free in predicates and are bound by first order quantifiers.
Programs out of proofs It is sometimes claimed that, as a corollary of the analogy, programs may be extracted from proofs. Indeed [GLT89 , chapter 15] shows that any function which can be proved to be total in second order logic is definable in Girard's System F. Unfortunately, to achieve this in practice it currently appears to be necessary to add so much detail to a proof that it would be easier to write the program in the first place. Maybe in the future it will be possible to automate the process of filling in this detail.
The constructive existential quantifier The logical symbol for which the type-theoretic version involves the most extra detail compared to its propositional form is the existential quantifier or dependent sum. Here, then, is where the isomorphism has its strongest consequences: in particular Choice is a theorem. So conversely this is where it is perhaps the most overstated: the existential quantifier, as understood by ordinary mathematicians, does not provide a particular witness, so is weaker than a dependent sum. So judicious consideration leads us to ask where the principle is to be followed, and where it is essentially inapplicable.
REMARK 2.4.7 We observed that the extended use of the notation for set-comprehension (Remark 2.2.7) hides an existential quantifier. Some of the footnotes in the next chapter point out other disguised quantifiers resulting from our blindness to why one thing is ``less than'' another; this is the abstract version of only considering prov ability. Inequalities, structures ``generated'' by a set, and any words which end in ``-able'' or ``-ible'' probably all conceal similar secrets. Chapter IV provides ways of accounting for the unstated reasons.
EXAMPLE 2.4.8 Square roots, on the other hand, can manifestly be exhibited, but the extreme constructivist would seem, like Buridan's ass, to be unable to make a choice of them.
=0.35mm omitted picture environment =70mm Figure
The diagram illustrates the squaring function on the unit circle in the complex plane. It is well known that there is no continuous choice of square roots which can be made all the way around the circle, but there are, according to Brouwer, no real- (or complex-) valued functions apart from continuous ones (Remark 1.8.6). We seem to be unable to say that squaring is a surjective function, "x.$y.x = y2.
One answer which a constructivist type-theorist might give falls back on the Cauchy sequences (Definition 2.1.2) used to define the real and complex numbers. Using only the first approximation \arga0 Î Q[i] to x, we make an arbitrary selection of \argb0 such that \argb02 » \arga0; this is admissible since Q has decidable equality. Subsequent approximants \argbn are chosen to be nearer to \argb0 than to -\argb0. The resulting square root ``function'' does not preserve the equality relation on its nominal source S1. So tokens for mathematical objects (the actual terms of Cauchy sequences in this case), rather than the objects themselves, must be used to give the witnesses of existential quantifiers. A similar idea will emerge from constructions of algebras using generators and relations in Section 7.4.
I have to say that I am not convinced, and feel that the Example shows that the unwitnessed existential quantifier is important in mathematics. This and the dependent sum should be seen as two cases (in some sense the extremes) of a single more general concept, and we shall treat them as such in Section 9.3. To rely on coding is certainly not conceptual mathematics, even if Per Martin-Löf regards this as constructive.
Another reason for wanting to ignore the witnesses is that, in the study of systems, we need to be able to discard as much information as we can about the lower levels in order to comprehend the higher ones.
Example 6.6.7 considers how many square roots there are.
The existence and disjunction properties Classical logic asserts (and thereby gives a trivial proof of the fact) that fÚ\lnot f is true, without necessarily giving a proof of either f or \lnot f.
REMARK 2.4.9 The normalisation theorem for the sum type (which we shall prove in Section 7.7) says that any proof \vdash c:fÚy is either of the form n0(a) with \vdash a:f or of the form n1(b) with \vdash b:y. So the identification of Ú with + means that the only way to prove fÚy is by first proving one of the disjuncts. This is known as the disjunction property of intuitionistic logic.
Similarly, if $x.f[x] is provable then there is some a - which may be found by examination of the given proof - for which f[a] is also provable (the existence property). This is what justifies the uniform proofs in Fact 1.7.1. The classical inter-definability of " and $ via negation breaks down because " has no analogous property. For example, let f[n] be the statement that n is not the code of a valid proof in Peano arithmetic whose conclusion is that 0 = 1. Then f[n] has a proof for each n, but Kurt Gödel (1931) showed that "x.f[x] has no proof in the same system (Theorem 9.6.2).
Classical logic The failure of the disjunction property in classical logic seems to mean that it has no constructive interpretation.
REMARK 2.4.10 Peirce's law (which, with y = ^, is excluded middle),
|
|
The sequent above has been called the restart rule because it is invoked when we have failed to prove the local goal: it is sufficient to prove any pending goal from an enclosing box. Note that this is a valid classical proof of the main goal q, but not necessarily of the sub-goal fÞ y.
=10pt omitted proofbox environment
This idiom seems a little less bizarre if we imagine, not a proof, but a program such as a compiler with a recursive structure tied closely to that of the user's input. The easiest way of dealing with potential errors in the input is to abandon the structure, ie to jump directly out of scope. Recently, methods have been developed for compiling higher order programs into very efficient continuation-passing object code. Nevertheless , such idioms are notoriously difficult to understand: the verification must take account of the fact that there are two ways of getting to line restart goal.
Returning to logic, suppose we have a classical proof which doesn't use (^E ). Harvey Friedman (1978) observed that the symbol ^ (and its implicit use for negation) may validly be replaced throughout such a proof by any formula - such as the one to be proved (Remark 1.4.4). Peirce's law serves for excluded middle in this translation; this explains why box proofs that involve negation or classical logic are very difficult to find. Hence any proposition of the form "n.$m.f[n,m] with a classical proof also has an intuitionistic one, so long as f is primitive recursive, and in particular decidable. This result does not extend to more complex formulae, for example $m."n.f(m) £ f(n) is provable in classical Peano arithmetic, for any f:N® N, but (using Gödel again) "n.f(m0) £ f(n) need not be provable in the same system for any m0.
See [Coq97] for a survey of the constructive interpretations which can be given to classical logic.
Although we do not exploit such interpretations in this book, continuations do feature throughout, in the background. The open-ended ($E )- box and the commuting conversion rule for sums (Remarks 1.6.5 and 2.3.13ff) were our first encounter with them, and we shall always write them as the symbol z. They will arise in more interesting ways in our treatments of lists and while programs.
Term and type assignment Another difference between propositions and types apparent in the simpler examples of symbolic reasoning is that algebra, the l-calculus and programming typically involve many terms but few distinct types, whereas in logic we mention many propositions, but the identity of their proofs is unimportant and usually left implicit.
REMARK 2.4.11 The uninteresting information therefore gets elided, and we might expect development tools to recover it automatically:
The \Clone notation We shall exploit the analogy between propositions as types, deliberately confusing algebra, logic and type theory.
|