Information AboutCurry-howard Isomorphism |
| CATEGORIES ABOUT CURRY–HOWARD | |
| proof theory | |
| logic in computer science | |
| type theory | |
|
The ''correspondence'' can be seen at two levels, firstly, that of an Analogy , which states that the assertion of the type of value computed by a function is analogous to a logical theorem, and that the program to compute that value is analogous to a proof of that theorem. In theoretical Computer Science , this is an important underlying principle connecting the adjacent areas of Lambda Calculus and Type Theory . It is often stated in the form ''proofs are programs''. An alternate formulation is '''''propositions as types'''''. Secondly, and more formally, it specifies a formal isomorphism between two mathematical domains, that of Natural Deduction formalised in a particular manner, and of the Simply Typed Lambda Calculus , where there is a Bijection between, in the first place proofs and terms, and in the second, proof reduction steps and beta reductions. There are a number of ways to think about the Curry–Howard correspondence. In one direction, it operates on the level ''compile proofs into programs''. Here ''proof'' was, originally, limited to proofs in Constructive Logic — typically in a system of Intuitionistic Logic . And ''program'' meant ''in the sense of conventional Functional Programming ''; from the point of view of Syntax such programs are expressed in some kind of Lambda Calculus . Therefore one concrete realisation of the Curry-Howard isomorphism is to study in detail how proofs from intuitionistic logic should be written into lambda terms. (Which is Howard's contribution; Curry being committed to the Combinator , which is more like writing everything in a machine language for which the lambda calculus is a high-level language.) More recently, extensions of the Curry-Howard correspondence have been formulated which handle Classical Logic as well, by relating classically valid rules such as Double Negation Elimination and Peirce's Law to the types of terms which explicitly deal with continuations, such as Call/cc . There is a converse direction, relating to the possibility of ''proof extraction'', given the Correctness of a program. This is only feasible in a quite rich Type Theory environment. In fact the development of very rich typed functional programming languages, by theoreticians, has been partly motivated by the wish to bring the Curry-Howard correspondence to a more 'manifest' status. TYPES Following the Lambda Calculus , we will use λ''x''.''E'' to denote the function with formal parameter ''x'' and body ''E''. When applied to an argument, say ''a'', this function yields ''E'', with every Free appearance of ''x'' replaced with ''a''. Valid λ-calculus expressions have one of these forms: # ''v'' (where ''v'' is a variable) # λ''v''.''E'' (where ''v'' is a variable and ''E'' is a λ-calculus expression) # (''E'' ''F'') (where ''E'' and ''F'' are λ-calculus expressions) As is usual, we will abbreviate ((''A'' ''B'') ''C'') as (''A'' ''B'' ''C'') and λ''a''.λ''b''.''E'' as λ''ab''.''E''. An expression is said to be ''closed'' if it contains no Free Variable s. Types can depend on ''type variables'', which will be denoted by lowercase Greek letters α, β, and so on. In our notation type variables are implicitly Universally Quantified , i.e. if a value is of a type that includes type variables, it must be consistent with all possible instantiations of the type variables. We can define the type of an arbitrary expression as follows: a variable, say ''x'', can have any type. If variable ''x'' has type α, and expression ''E'' has type β, then λ''x''.''E'' has a type denoted as α → β; that is, it is a function which takes values of type α to values of type β. In the expression (''E'' ''F''), if ''F'' has type α, then ''E'' must have type α → β (that is, it must be a function that expects an argument of type α) and the entire expression has type β. For example, consider the function K = λ''a''.λ''b''.''a''. Suppose that ''a'' has type α and ''b'' has type β. Then λ''b''.''a'' has type β → α, and λ''a''.λ''b''.''a'' has type α → (β → α). We adopt the convention that → associates to the right, so that the type can also be written as α → β → α. This means that the K function takes an argument of type α and returns a function, which, given an argument of type β, returns a value of type α. Similarly, consider the function B = λ''a''.λ''b''.λ''c''. (''a'' (''b'' ''c'')). Suppose that ''c'' has type γ. Then ''b'' must have some type of the form γ → β, and the expression (''b'' ''c'') has the type β. ''a'' must have some type of the form β → α, and the expression (''a'' (''b'' ''c'')) has the type α. Then λ''c''. (''a'' (''b'' ''c'')) has the type γ → α; λ''b''.λ''c''. (''a'' (''b'' ''c'')) has the type (γ → β) → γ → α, and λ''a''.λ''b''.λ''c''. (''a'' (''b'' ''c'')) has the type (β → α) → (γ → β) → γ → α. One can interpret this as meaning that the B function takes an argument of type (β → α) and an argument of type (γ → β) and returns a function, which, given an argument of type γ, returns a result of type α. THE TYPE INHABITATION PROBLEM It's clear that λ-expressions can have quite complicated types. One might ask whether there is a λ-expression with any given type. The problem of finding a λ-expression with a particular type is called the Type Inhabitation Problem . The answer turns out to be remarkable: There is a closed λ-expression with a particular type only if the type corresponds to a theorem of logic, when the → symbols are re-interpreted as meaning logical implication. For example, consider the identity function, λ''x''.''x'', which takes an argument of type ξ and returns a result of type ξ, and so has type ξ → ξ. ξ → ξ is certainly a theorem of logic: given a formula ξ, one may conclude ξ. The type of the K function, α → β → α, is also a theorem. If α is known to be true, then one can conclude that if β were true, one would be able to deduce α. This is sometimes known as the Reiteration Rule . The type of B is (β → α) → (γ → β) → γ → α. One can interpret this similarly as a logical Tautology ; if (β → α) were known to be true, then if (γ → β) were known to be true, then one could deduce that γ would imply α. On the other hand, consider α → β, which is not a theorem. Clearly there is no λ-term which has this type; it would have to be a function which would take an argument of type α and which would return a result of some completely unrelated and unconstrained type. This is impossible, because you can't get something out of such a function unless you put it in somewhere else. Although there is a function of type β → (α → α) (for example, λ''b''.λ''a''.''a'', which takes an argument ''b'', ignores the argument, and returns the identity function), there is no function of type (α → α) → β, which, if it existed, would be a function for transforming the identity function into an arbitrary value. INTUITIONISTIC LOGIC Although it is true that all inhabited types correspond to theorems of logic, the converse is not true. Even if we restrict our attention to logical formulas that contain only the → operator, the so-called ''implicational fragment'' of logic, not every classically valid logical formula is an inhabited type. For example, the type ((α → β) → α) → α is uninhabited, even though the corresponding logical formula, known as Peirce's Law , is a tautology. Intuitionistic logic is a weaker system than classical logic. Whereas classical logic concerns itself with formulas that are 'true' in an abstract, Platonic sense, a formula of intuitionistic logic is considered true only if a proof can be constructed for it. The formula α ∨ ¬α exemplifies the difference; it is a theorem of classical logic but not of intuitionistic logic. Although it is 'true' classically, in intuitionistic logic this formula asserts that we can either ''prove'' α or we can prove ¬α. Since it isn't always the case that we can do one of these things, this ''isn't'' a theorem of intuitionistic logic. The correspondence between inhabited types and valid logical formulas is exact in both directions if we restrict our attention to theorems of the implicational fragment of Intuitionistic Logic (this is called a Hilbert Algebra ). HILBERT-STYLE PROOFS One simple way to formally characterize intuitionistic logic is as follows. It has two axiom schemas. All formulas of the form : α → β → α are axioms, as are all formulas of the form : (α → β → γ) → (α → β) → α → γ The only deduction rule is Modus Ponens , which states that if we have proved two theorems, one of the form α → β and one of the form α, we may conclude that β is also a theorem. The set of formulas that can be deduced in this fashion is precisely the set of formulas of intuitionistic logic. In particular, Peirce's law is ''not'' deducible in this way. (For a proof that Peirce's law is not deducible in this way, see the article on Heyting Algebra s.) If we add Peirce's law as a third axiom schema, the system above becomes capable of proving all the theorems in the implicational fragment of classical logic. PROGRAMS ARE PROOFS A second aspect of the Curry–Howard isomorphism is that a program whose type corresponds to a logical formula is itself analogous to a proof of that formula. Consider the two following functions of λ-calculus: : K: λ''xy''.''x'' : S: λ''xyz''. (''x'' ''z'' (''y'' ''z'')) It can be shown that any function can be created by suitable applications of K and '''S''' to each other. (See the Combinatory Logic article for a proof.) For example, the function '''B''' defined above is equivalent to (S ('''K''' S) '''K'''). If a function, such as B, can be expressed as a composition of '''S''' and '''K''', the expression can be converted directly into a proof that the type of B, interpreted as a logical formula, is a theorem of intuitionistic logic. Essentially, appearances of K correspond to uses of the first axiom schema, appearances of S correspond to uses of the second axiom schema, and function applications correspond to uses of the modus ponens deduction rule. The first axiom schema is α → β → α, and this is precisely the type of the K function; similarly the second axiom schema, (α → β → γ) → (α → β) → α → γ, is the type of the S function. Modus ponens says that if we have two expressions, one of type α → β (that is, a function that takes a value of type α and returns a value of type β) and the other of type α (that is, a value of type α) then we should be able to find a value of type β; clearly, we can do this by applying the function to the value; the result will have type β. Proof of α → α As a simple example, we will construct a proof of the theorem α → α. This is the type of the identity function I = λ''x''.''x''. The function ((S '''K''') '''K''') is also equivalent to the identity function. As a description of a proof, this says that we need to first apply S to '''K'''. We do this as follows: : α → β → α : (α → β → γ) → (α → β) → α → γ If we let γ = α in S, we get: : (α → β → α) → (α → β) → α → α Since the antecedent of this formula (α → β → α) is a known theorem, and is in fact precisely K, we can apply modus ponens and deduce the consequent: : (α → β) → α → α This is the type of the function (S '''K'''). Now we need to apply this function to K. Again, we manipulate the formula so that the antecedent looks like K, this time by substituting (β → α) for β: : (α → β → α) → α → α Once again we can use modus ponens to detach the consequent: : α → α and we are done. In general, the procedure is that whenever the program contains an application of the form (''P'' ''Q''), we should first prove theorems corresponding to the types of ''P'' and ''Q''. Since ''P'' is being applied to ''Q'', the type of ''P'' must have the form α → β and the type of ''Q'' must have the form α for some α and β. We can then detach the conclusion, β, via the modus ponens rule. Proof of (β → α) → (γ → β) → γ → α As a more complicated example, let's look at the theorem that corresponds to the B function. The type of B is (β → α) → (γ → β) → γ → α. B is equivalent to ('''S''' ('''K''' '''S''') K). This is our roadmap for the proof of the theorem (β → α) → (γ → β) → γ → α. First we need to construct (K '''S'''). We make the antecedent of the K axiom look like the '''S''' axiom by setting α equal to (α → β → γ) → (α → β) → α → γ, and β equal to δ: : α → β → α : ((α → β → γ) → (α → β) → α → γ) → δ → (α → β → γ) → (α → β) → α → γ Since the antecedent here is just S, we can detach the consequent: : δ → (α → β → γ) → (α → β) → α → γ This is the theorem that corresponds to the type of (K '''S'''). We now apply S to this expression. Taking S : (α → β → γ) → (α → β) → α → γ we put α = δ, β = (α → β → γ), and γ = ((α → β) → α → γ), yielding : (δ → (α → β → γ) → (α → β) → α → γ) → (δ → (α → β → γ)) → δ → (α → β) → α → γ and we then detach the consequent: : (δ → α → β → γ) → δ → (α → β) → α → γ This is the formula for the type of (S ('''K''' S)). A special case of this theorem has δ = (β → γ): : ((β → γ) → α → β → γ) → (β → γ) → (α → β) → α → γ We need to apply this last formula to K. Again, we specialize K, this time by replacing α with (β → γ) and β with α: : α → β → α : (β → γ) → α → (β → γ) This is the same as the antecedent of the prior formula, so we detach the consequent: : (β → γ) → (α → β) → α → γ Switching the names of the variables α and γ gives us : (β → α) → (γ → β) → γ → α which was what we had to prove. SEQUENT CALCULUS Hilbert-style proofs can be difficult to construct. A more intuitive way to prove theorems of logic is Gentzen 's ' Sequent Calculus '. Sequent calculus proofs correspond to λ-calculus programs in the same way that Hilbert-style proofs correspond to combinator expressions. The sequent calculus rules for the implicational fragment of intuitionistic logic are:
|