{
"cells": [
{
"cell_type": "markdown",
"id": "1ccbfd56",
"metadata": {},
"source": [
"# The Curry-Howard Correspondence\n",
"\n",
"```{note}\n",
"A *lagniappe* is a small and unexpected gift — a little \"something extra\".\n",
"Please enjoy this little chapter, which contains one of the most beautiful\n",
"results in the entire book. It is based on the paper\n",
"[Propositions as Types][pat] by Philip Wadler. You can watch an entertaining\n",
"[recorded lecture][pat-lambda-days] by Prof. Wadler on it, in addition\n",
"to our lecture below.\n",
"```\n",
"\n",
"{{ video_embed | replace(\"%%VID%%\", \"GdcOy6zVFC4\")}}\n",
"\n",
"As we observed long ago, OCaml is a language in the ML family, and ML was\n",
"originally designed as the __m__eta __l__anguage for a theorem\n",
"prover—that is, a computer program designed to help prove and check the\n",
"proofs of logical formulas. When constructing proofs, it's desirable to make\n",
"sure that you can only prove true formulas, to make sure that you don't make\n",
"incorrect arguments, etc.\n",
"\n",
"The dream would be to have a computer program that can determine the truth or\n",
"falsity of any logical formula. For some formulas, that is possible. But, one of\n",
"the groundbreaking results in the early 20th century was that it is *not*\n",
"possible, in general, for a computer program to do this. Alonzo Church and Alan\n",
"Turing independently showed this in 1936. Church used the *lambda calculus* as a\n",
"model for computers; Turing used what we now call *Turing machines*. The\n",
"*Church-Turing thesis* is a hypothesis that says the lambda calculus and Turing\n",
"machines both formalize what \"computation\" informally means.\n",
"\n",
"Instead of focusing on that impossible task, we're going to focus on the\n",
"relationship between proofs and programs. It turns out the two are deeply\n",
"connected in a surprising way.\n",
"\n",
"## Computing with Evidence\n",
"\n",
"We're accustomed to OCaml programs that manipulate data, such as integers and\n",
"variants and functions. Those data values are always typed: at compile time,\n",
"OCaml infers (or the programmer annotates) the types of expressions. For\n",
"example, `3110 : int`, and `[] : 'a list`. We long ago learned to read those as\n",
"\"`3110` has type `int`\", and \"`[]` has type `'a list`\".\n",
"\n",
"Let's try a different reading now. Instead of \"has type\", let's read \"is\n",
"evidence for\". So, `3110` is evidence for `int`. What does that mean? Think of a\n",
"type as a set of values. So, `3110` is evidence that type is not empty.\n",
"Likewise, `[]` is evidence that the type `'a list` is not empty. We say that the\n",
"type is *inhabited* if it is not empty.\n",
"\n",
"Are there empty types? There actually is one in OCaml, though we've never had\n",
"reason to mention it before. It's possible to define a variant type that has no\n",
"constructors:"
]
},
{
"cell_type": "code",
"execution_count": 1,
"id": "a0b7095c",
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"type empty = |\n"
]
},
"execution_count": 1,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"type empty = |"
]
},
{
"cell_type": "markdown",
"id": "bf70fc17",
"metadata": {},
"source": [
"We could have called that type anything we wanted instead of `empty`; the\n",
"special syntax there is just writing `|` instead of actual constructors. (Note,\n",
"that syntax might give some editors some trouble. You might need to put\n",
"double-semicolon after it to get the formatting right.) It is impossible to\n",
"construct a value of type `empty`, exactly because it has no constructors. So,\n",
"`empty` is not inhabited.\n",
"\n",
"Under our new reading based on evidence, we could think about functions as ways\n",
"to manipulate and transform evidence—just as we are already accustomed to\n",
"thinking about functions as ways to manipulate and transform data. For example,\n",
"the following functions construct and destruct pairs:"
]
},
{
"cell_type": "code",
"execution_count": 2,
"id": "00705398",
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"val pair : 'a -> 'b -> 'a * 'b = \n"
]
},
"execution_count": 2,
"metadata": {},
"output_type": "execute_result"
},
{
"data": {
"text/plain": [
"val fst : 'a * 'b -> 'a = \n"
]
},
"execution_count": 2,
"metadata": {},
"output_type": "execute_result"
},
{
"data": {
"text/plain": [
"val snd : 'a * 'b -> 'b = \n"
]
},
"execution_count": 2,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"let pair x y = (x, y)\n",
"let fst (x, y) = x\n",
"let snd (x, y) = y"
]
},
{
"cell_type": "markdown",
"id": "a005fee1",
"metadata": {},
"source": [
"We could think of `pair` as a function that takes in evidence for `'a` and\n",
"evidence for `'b`, and gives us back evidence for `'a * 'b`. That latter piece\n",
"of evidence is the the pair `(x, y)` containing the individual pieces of\n",
"evidence, `x` and `y`. Similarly, `fst` and `snd` extract the individual pieces\n",
"of evidence from the pair. Thus,\n",
"\n",
"- If you have evidence for `'a` and evidence for `'b`, you can produce evidence\n",
" for `'a` and `'b`.\n",
"- If you have evidence for `'a` and `'b`, then you can produce evidence for\n",
" `'a`.\n",
"- If you have evidence for `'a` and `'b`, then you can produce evidence for\n",
" `'b`.\n",
"\n",
"In learning to do proofs (say, in a discrete mathematics class), you will\n",
"have learned that in order to prove two statements hold, you individually\n",
"have to prove that each holds. That is, to prove the conjunction of A and B,\n",
"you must prove A as well as prove B. Likewise, if you have a proof of the\n",
"conjunction of A and B, then you can conclude A holds, and you can conclude B\n",
"holds. We can write those patterns of reasoning as logical formulas, using\n",
"`/\\` to denote conjunction and `->` to denote implication:\n",
"\n",
"```text\n",
"A -> B -> A /\\ B\n",
"A /\\ B -> A\n",
"A /\\ B -> B\n",
"```\n",
"\n",
"Proofs are a form of evidence: they are logical arguments about the truth\n",
"of a statement. So another reading of those formulas would be:\n",
"\n",
"- If you have evidence for A and evidence for B, you can produce evidence\n",
" for A and B.\n",
"- If you have evidence for A and B, then you can produce evidence for A.\n",
"- If you have evidence for A and B, then you can produce evidence for B.\n",
"\n",
"Notice how we now have given the same reading for programs and for proofs. They\n",
"are both ways of manipulating and transforming evidence. In fact, take a close\n",
"look at the types for `pair`, `fst`, and `snd` compared to the logical formulas\n",
"that describe valid patterns of reasoning:\n",
"\n",
"```text\n",
"val pair : 'a -> 'b -> 'a * 'b A -> B -> A /\\ B\n",
"val fst : 'a * 'b -> 'a A /\\ B -> A\n",
"val snd : 'a * 'b -> 'b A /\\ B -> B\n",
"```\n",
"\n",
"If you replace `'a` with A, and `'b` with B, and `*` with `/\\`, **the types of\n",
"the programs are identical to the formulas!**\n",
"\n",
"## The Correspondence\n",
"\n",
"What we have just discovered is that computing with evidence corresponds to\n",
"constructing valid logical proofs. This correspondence is not just an accident\n",
"that occurs with these three specific programs. Rather, it is a deep phenomenon\n",
"that links the fields of programming and logic. Aspects of it have been\n",
"discovered by many people working in many areas. So, it goes by many names. One\n",
"common name is *the Curry-Howard correspondence*, named for logicians Haskell\n",
"Curry (for whom the functional programming language Haskell is named) and\n",
"William Howard. This correspondence links ideas from programming to ideas from\n",
"logic:\n",
"\n",
"- Types correspond to logical formulas (aka *propositions*).\n",
"- Programs correspond to logical proofs.\n",
"- Evaluation corresponds to simplification of proofs.\n",
"\n",
"We've already seen the first two of those correspondences. The types of our\n",
"three little programs corresponded to formulas, and the programs themselves\n",
"corresponded to the reasoning done in proofs involving conjunctions. We haven't\n",
"seen the third yet; we will later.\n",
"\n",
"Let's dig into each of the correspondences to appreciate them more fully.\n",
"\n",
"## Types Correspond to Propositions\n",
"\n",
"In *propositional logic*, formulas are created with atomic propositions,\n",
"negation, conjunction, disjunction, and implication. The following BNF describes\n",
"propositional logic formulas:\n",
"\n",
"```text\n",
"p ::= atom\n",
" | ~ p (* negation *)\n",
" | p /\\ p (* conjunction *)\n",
" | p \\/ p (* disjunction *)\n",
" | p -> p (* implication *)\n",
"\n",
"atom ::= \n",
"```\n",
"\n",
"For example, `raining /\\ snowing /\\ cold` is a proposition stating that it is\n",
"simultaneously raining and snowing and cold (a weather condition known as\n",
"[*Ithacating*][ithacating]). An atomic proposition might hold of the world, or\n",
"not. There are two distinguished atomic propositions, written `true` and\n",
"`false`, which are always hold and never hold, respectively.\n",
"\n",
"[ithacating]: https://www.urbandictionary.com/define.php?term=Ithacating\n",
"\n",
"All these *connectives* (so-called because they connect formulas together) have\n",
"correspondences in the types of functional programs.\n",
"\n",
"**Conjunction.** We have already seen that the `/\\` connective corresponds to\n",
"the `*` type constructor. Proposition `A /\\ B` asserts the truth of both `A` and\n",
"`B`. An OCaml value of type `a * b` contains values both of type `a` and `b`.\n",
"Both `/\\` and `*` thus correspond to the idea of pairing or products.\n",
"\n",
"**Implication.** The implication connective `->` corresponds to the function\n",
"type constructor `->`. Proposition `A -> B` asserts that if you can show that\n",
"`A` holds, then you can show that `B` holds. In other words, by assuming `A`,\n",
"you can conclude `B`. In a sense, that means you can transform `A` into `B`. An\n",
"OCaml value of type `a -> b` expresses that idea even more clearly. Such a value\n",
"is a function that transforms a value of type `a` into a value of type `b`.\n",
"Thus, if you can show that `a` is inhabited (by exhibiting a value of that\n",
"type), you can show that `b` is inhabited (by applying the function of type\n",
"`a -> b` to it). So, `->` corresponds to the idea of transformation.\n",
"\n",
"**Disjunction.** The disjunction connective `\\/` corresponds to something a\n",
"little more difficult to express concisely in OCaml. Proposition `A \\/ B`\n",
"asserts that either you can show `A` holds or `B` holds. Let's strengthen that\n",
"to further assert that in addition to showing *one* of them holds, you have to\n",
"specify *which one* you are showing. Why would that matter?\n",
"\n",
"Suppose we were working on a proof of the *twin prime conjecture*, an unsolved\n",
"problem that states there are infinitely many twin primes (primes of the form\n",
"$n$ and $n+2$, such as 3 and 5, or 5 and 7). Let the atomic proposition `TP`\n",
"denote that there are infinitely many twin primes. Then the proposition\n",
"`TP \\/ ~ TP` seems reasonable: either there are infinitely many twin primes, or\n",
"there aren't. We wouldn't even have to figure out how to prove the conjecture!\n",
"But if we strengthen the meaning of `\\/` to be that we have to state *which one*\n",
"of the sides, left or right, holds, then we would either have to give a proof or\n",
"disproof of the conjecture. No one knows how to do that currently. So we could\n",
"not prove `TP \\/ ~ TP`.\n",
"\n",
"Henceforth we will use `\\/` in that stronger sense of having to identify whether\n",
"we are giving a proof of the left or the right side proposition. Thus, we can't\n",
"necessarily conclude `p \\/ ~ p` for any proposition `p`: it will matter whether\n",
"we can prove `p` or `~ p` on their own. Technically, this makes our\n",
"propositional logic *constructive* rather than *classical*. In constructive\n",
"logic we must construct the proof of the individual propositions. Classical\n",
"logic (the traditional way `\\/` is understood) does not require that.\n",
"\n",
"Returning to the correspondence between disjunction and variants, consider this\n",
"variant type:"
]
},
{
"cell_type": "code",
"execution_count": 3,
"id": "3a3b055e",
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"type ('a, 'b) disj = Left of 'a | Right of 'b\n"
]
},
"execution_count": 3,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"type ('a, 'b) disj = Left of 'a | Right of 'b"
]
},
{
"cell_type": "markdown",
"id": "728a7ed9",
"metadata": {},
"source": [
"A value `v` of that type is either `Left a`, where `a : 'a`; or `Right b`, where\n",
"`b : 'b`. That is, `v` identifies (i) whether it is tagged with the left\n",
"constructor or the right constructor, and (ii) carries within it exactly one\n",
"sub-value of type either `'a` or `'b`—not two subvalues of both types,\n",
"which is what `'a * 'b` would be.\n",
"\n",
"Thus, the (constructive) disjunction connective `\\/` corresponds to the `disj`\n",
"type constructor. Proposition `A \\/ B` asserts that either `A` or `B` holds as\n",
"well as which one, left or right, it is. An OCaml value of type `('a, 'b) disj`\n",
"similarly contains a value of type either `'a` or `'b` as well as identifying\n",
"(with the `Left` or `Right` constructor) which one it is. Both `\\/` and `disj`\n",
"therefore correspond to the idea of unions.\n",
"\n",
"**Truth and Falsity** The atomic proposition `true` is the only proposition that\n",
"is guaranteed to always hold. There are many types in OCaml that are always\n",
"inhabited, but the simplest of all of them is `unit`: there is one value `()` of\n",
"type `unit`. So the proposition `true` (best) corresponds to the type `unit`.\n",
"\n",
"Likewise, the atomic proposition `false` is the only proposition that is\n",
"guaranteed to never hold. That corresponds to the `empty` type we introduced\n",
"earlier, which has no constructors. (Other names for that type could include\n",
"`zero` or `void`, but we'll stick with `empty`.)\n",
"\n",
"There is a subtlety with `empty` that we should address. The type has no\n",
"constructors, but it is nonetheless possible to write expressions that have type\n",
"`empty`. Here is one way:"
]
},
{
"cell_type": "code",
"execution_count": 4,
"id": "2db31928",
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"val loop : 'a -> 'b = \n"
]
},
"execution_count": 4,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"let rec loop x = loop x"
]
},
{
"cell_type": "markdown",
"id": "09222345",
"metadata": {},
"source": [
"Now if you enter this code in utop you will get no response:\n",
"\n",
"```ocaml\n",
"let e : empty = loop ()\n",
"```\n",
"\n",
"That expression type checks successfully, then enters an infinite loop. So,\n",
"there is never any value of type `empty` that is produced, even though the\n",
"expression has that type.\n",
"\n",
"Here is another way:"
]
},
{
"cell_type": "code",
"execution_count": 5,
"id": "46541058",
"metadata": {
"tags": [
"raises-exception"
]
},
"outputs": [
{
"ename": "error",
"evalue": "runtime_error",
"output_type": "error",
"traceback": [
"\u001b[31mException: Failure \"\".\nRaised at Stdlib.failwith in file \"stdlib.ml\", line 29, characters 17-33\nCalled from unknown location\nCalled from Stdlib__Fun.protect in file \"fun.ml\", line 33, characters 8-15\nRe-raised at Stdlib__Fun.protect in file \"fun.ml\", line 38, characters 6-52\nCalled from Topeval.load_lambda in file \"toplevel/byte/topeval.ml\", line 89, characters 4-150\n\u001b[0m"
]
}
],
"source": [
"let e : empty = failwith \"\""
]
},
{
"cell_type": "markdown",
"id": "a8c4e8f2",
"metadata": {},
"source": [
"Again, the expression type checks, but it never produces an actual value of type\n",
"`empty`. Instead, this time an exception is produced.\n",
"\n",
"So the type `empty` is not inhabited, even though there are some expressions of\n",
"that type. But, **if we require programs to be total**, we can rule out those\n",
"expressions. That means eliminating programs that raise exceptions or go into an\n",
"infinite loop. We did in fact make that requirement when we started discussing\n",
"formal methods, and we will continue to assume it.\n",
"\n",
"**Negation.** This connective is the trickiest. Let's consider negation to\n",
"actually be syntactic sugar. In particular, let's say that the propositional\n",
"formula `~ p` actually means this formula instead: `p -> false`. Why? The\n",
"formula `~ p` should mean that `p` does not hold. So if `p` *did* hold, then it\n",
"would lead to a contradiction. Thus, given `p`, we could conclude `false`. This\n",
"is the standard way of understanding negation in constructive logic.\n",
"\n",
"Given that syntactic sugar, `~ p` therefore corresponds to a function type whose\n",
"return type is `empty`. Such a function could never actually return. Given our\n",
"ongoing assumption that programs are total, that must mean it's impossible to\n",
"even call that function. So, it must be impossible to construct a value of the\n",
"function's input type. Negation therefore corresponds to the idea of\n",
"impossibility, or contradiction.\n",
"\n",
"**Propositions as types.** We have now created the following correspondence that\n",
"enables us to read propositions as types:\n",
"\n",
"- `/\\` and `*`\n",
"- `->` and `->`\n",
"- `\\/` and `disj`\n",
"- `true` and `unit`\n",
"- `false` and `empty`\n",
"- `~` and `... -> false`\n",
"\n",
"But that is only the first level of the Curry-Howard correspondence. It goes\n",
"deeper...\n",
"\n",
"## Programs Correspond to Proofs\n",
"\n",
"We have seen that programs and proofs are both ways to manipulate and transform\n",
"evidence. In fact, every program **is** a proof that the type of the program is\n",
"inhabited, since the type checker must verify that the program is well typed.\n",
"\n",
"The details of type checking, though, lead to an even more compelling\n",
"correspondence between programs and proofs. Let's restrict our attention to\n",
"programs and proofs involving just conjunction and implication, or equivalently,\n",
"pairs and functions. (The other propositional connectives could be included as\n",
"well, but require additional work.)\n",
"\n",
"**Type checking rules.** For type checking, we gave many *rules* to define when\n",
"a program is well typed. Here are rules for variables, functions, and pairs:\n",
"\n",
"```text\n",
"{x : t, ...} |- x : t\n",
"```\n",
"A variable has whatever type the environment says it has.\n",
"\n",
"```text\n",
"env |- fun x -> e : t -> t'\n",
"if env[x -> t] |- e : t'\n",
"```\n",
"\n",
"An anonymous function `fun x -> e` has type `t -> t'` if `e` has type `t'` in a\n",
"static environment extended to bind `x` to type `t`.\n",
"\n",
"```text\n",
"env |- e1 e2 : t'\n",
"if env |- e1 : t -> t'\n",
"and env |- e2 : t\n",
"```\n",
"\n",
"An application `e1 e2` has type `t'` if `e1` has type `t -> t'` and `e2` has\n",
"type `t`.\n",
"\n",
"```text\n",
"env |- (e1, e2) : t1 * t2\n",
"if env |- e1 : t1\n",
"and env |- e2 : t2\n",
"```\n",
"\n",
"The pair `(e1, e2)` has type `t1 * t2` if `e1` has type `t1` and `e2` has\n",
"type `t2`.\n",
"\n",
"```text\n",
"env |- fst e : t1\n",
"if env |- e : t1 * t2\n",
"\n",
"env |- snd e : t2\n",
"if env |- e : t1 * t2\n",
"```\n",
"\n",
"If `e` has type `t1 * t2`, then `fst e` has type `t1`, and `snd e` has type\n",
"`t2`.\n",
"\n",
"**Proof trees.** Another way of expressing those rules would be to draw *proof\n",
"trees* that show the recursive application of rules. Here are those proof trees:\n",
"\n",
"```text\n",
"\n",
"---------------------\n",
"{x : t, ...} |- x : t\n",
"\n",
"\n",
" env[x -> t1] |- e2 : t2\n",
"-----------------------------\n",
"env |- fun x -> e2 : t1 -> t2\n",
"\n",
"\n",
"env |- fun x -> e2 : t1 -> t2 env |- e1 : t1\n",
"---------------------------------------------------\n",
" env |- (fun x -> e2) e1 : t2\n",
"\n",
"\n",
"env |- e1 : t1 env |- e2 : t2\n",
"-------------------------------------\n",
" env |- (e1, e2) : t1 * t2\n",
"\n",
"\n",
" env |- e : t1 * t2\n",
"--------------------\n",
" env |- fst e : t1\n",
"\n",
"\n",
" env |- e : t1 * t2\n",
"--------------------\n",
" env |- snd e : t2\n",
"```\n",
"\n",
"**Proof trees, logically.** Let's rewrite each of those proof trees to eliminate\n",
"the programs, leaving only the types. At the same time, let's use the\n",
"propositions-as-types correspondence to re-write the types as propositions:\n",
"\n",
"```text\n",
"\n",
"--------\n",
" p |- p\n",
"\n",
"\n",
" env, p1 |- p2\n",
"-------------------\n",
" env |- p1 -> p2\n",
"\n",
"\n",
"env |- p1 -> p2 env |- p1\n",
"-----------------------------\n",
" env |- p2\n",
"\n",
"\n",
"env |- p1 env |- p2\n",
"------------------------\n",
" env |- p1 /\\ p2\n",
"\n",
"\n",
"env |- p1 /\\ p2\n",
"---------------\n",
" env |- p1\n",
"\n",
"\n",
"env |- p1 /\\ p2\n",
"---------------\n",
" env |- p2\n",
"```\n",
"\n",
"Each rule can now be read as a valid form of logical reasoning. Whenever we\n",
"write `env |- t`, it means that \"from the assumptions in `env`, we can conclude\n",
"`p` holds\". A rule, as usual, means that from all the premisses above the line,\n",
"the conclusion below the line holds.\n",
"\n",
"**Proofs and programs.** Now consider the following proof tree, showing the\n",
"derivation of the type of a program:\n",
"\n",
"```text\n",
"------------------------ ------------------------\n",
"{p : a * b} |- p : a * b {p : a * b} |- p : a * b\n",
"------------------------ ------------------------\n",
"{p : a * b} |- snd p : b {p : a * b} |- fst p : a\n",
"-----------------------------------------------------------\n",
" {p : a * b} |- (snd p, fst p) : b * a\n",
" ----------------------------------------------\n",
" {} |- fun p -> (snd p, fst p) : a * b -> b * a\n",
"```\n",
"\n",
"That program shows that you can swap the components of a pair, thus\n",
"swapping the types involved.\n",
"\n",
"If we erase the program, leaving only the types, and re-write those\n",
"as propositions, we get this proof tree:\n",
"\n",
"```text\n",
"---------------- ----------------\n",
"a /\\ b |- a /\\ b a /\\ b |- a /\\ b\n",
"---------------- -----------------\n",
" a /\\ b |- b a /\\ b |- a\n",
"--------------------------------------------\n",
" a /\\ b |- b /\\ a\n",
" ------------------------\n",
" {} |- a /\\ b -> b /\\ a\n",
"```\n",
"\n",
"And that is a valid proof tree for propositional logic. It shows that you can\n",
"swap the sides of a conjunction.\n",
"\n",
"What we see from those two proof trees is: **a program is a proof**. A\n",
"well-typed program corresponds to the proof of a logical proposition. It shows\n",
"how to compute with evidence, in this case transforming a proof of `a /\\ b` into\n",
"a proof of `b /\\ a`.\n",
"\n",
"**Programs are proofs.** We have now created the following correspondence that\n",
"enables us to read programs as proofs:\n",
"\n",
"- A program `e : t` corresponds to a proof of the logical formula to which `t`\n",
" itself corresponds.\n",
"- The proof tree of `|- t` corresponds to the proof tree of `{} |- e : t`.\n",
"- The proof rules for typing a program correspond to the rules for proving a\n",
" proposition.\n",
"\n",
"But that is only the second level of the Curry-Howard correspondence. It goes\n",
"deeper...\n",
"\n",
"## Evaluation Corresponds to Simplification\n",
"\n",
"We will treat this part of the correspondence only briefly. Consider the\n",
"following program:\n",
"\n",
"```ocaml\n",
"fst (a, b)\n",
"```\n",
"\n",
"That program would of course evaluate to `a`.\n",
"\n",
"Next, consider the typing derivation of that program. The variables `a` and\n",
"`b` must be bound to some types in the static environment for the program\n",
"to type check.\n",
"\n",
"```text\n",
"------------------------ -------------------------\n",
"{a : t, b : t'} |- a : t {a : t, b : t'} |- b : t'\n",
"---------------------------------------------------------\n",
" {a : t, b : t'} |- (a, b) : t * t'\n",
" ----------------------------------\n",
" {a : t, b : t'} |- fst (a, b) : t\n",
"```\n",
"\n",
"Erasing that proof tree to just the propositions, per the proofs-as-programs\n",
"correspondence, we get this proof tree:\n",
"```\n",
"----------- -----------\n",
"t, t' |- t t, t' |- t'\n",
"----------------------------------\n",
" t, t' |- t /\\ t'\n",
" ----------------\n",
" t, t' |- t\n",
"```\n",
"\n",
"However, there is a much simpler proof tree with the same conclusion:\n",
"\n",
"```text\n",
" ------------\n",
" t, t' |- t\n",
"```\n",
"\n",
"In other words, we don't need the detour through proving `t /\\ t'` to prove `t`,\n",
"if `t` is already an assumption. We can instead just directly conclude `t`.\n",
"\n",
"Likewise, there is a simpler typing derivation corresponding to that same\n",
"simpler proof:\n",
"\n",
"```text\n",
"------------------------\n",
"{a : t, b : t'} |- a : t\n",
"```\n",
"\n",
"Note that typing derivation is for the program `a`, which is exactly what the\n",
"bigger program `fst (a, b)` evaluates to.\n",
"\n",
"Thus evaluation of the program causes the proof tree to simplify, and the\n",
"simplified proof tree is actually (through the proofs-as programs\n",
"correspondence) a simpler proof of the same proposition. **Evaluation therefore\n",
"corresponds to proof simplification.** And that is the final level of the\n",
"Curry-Howard correspondence.\n",
"\n",
"## What It All Means\n",
"\n",
"Logic is a fundamental aspect of human inquiry. It guides us in reasoning about\n",
"the world, in drawing valid inferences, in deducing what must be true vs. what\n",
"must be false. Training in logic and argumentation—in various fields and\n",
"disciplines—is one of the most important parts of a higher education.\n",
"\n",
"The Curry-Howard correspondence shows that logic and computation are\n",
"fundamentally linked in a deep and maybe even mysterious way. The basic building\n",
"blocks of logic (propositions, proofs) turn out to correspond to the basic\n",
"building blocks of computation (types, functional programs). Computation itself,\n",
"the evaluation or simplification of expressions, turns out to correspond to\n",
"simplification of proofs. The very task that computers do therefore is the same\n",
"task that humans do in trying to present a proof in the best possible way.\n",
"\n",
"Computation is thus intrinsically linked to reasoning. And functional\n",
"programming is a fundamental part of human inquiry.\n",
"\n",
"Could there *be* a better reason to study functional programming?\n",
"\n",
"[pat]: http://homepages.inf.ed.ac.uk/wadler/papers/propositions-as-types/propositions-as-types.pdf\n",
"[pat-lambda-days]: https://www.youtube.com/watch?v=aeRVdYN6fE8\n",
"\n",
"## Exercises\n",
"\n",
"{{ solutions }}\n",
"\n",
"\n",
"{{ ex2 | replace(\"%%NAME%%\", \"propositions as types\")}}\n",
"\n",
"For each of the following propositions, write its corresponding type\n",
"in OCaml.\n",
"\n",
"- `true -> p`\n",
"- `p /\\ (q /\\ r)`\n",
"- `(p \\/ q) \\/ r`\n",
"- `false -> p`\n",
"\n",
"\n",
"{{ ex3 | replace(\"%%NAME%%\", \"programs as proofs\")}}\n",
"\n",
"For each of the following propositions, determine its corresponding type in\n",
"OCaml, then write an OCaml `let` definition to give a program of that type. Your\n",
"program proves that the type is *inhabited*, which means there is a value of\n",
"that type. It also proves the proposition holds.\n",
"\n",
"- `p /\\ q -> q /\\ p`\n",
"- `p \\/ q -> q \\/ p`\n",
"\n",
"\n",
"{{ ex3 | replace(\"%%NAME%%\", \"evaluation as simplification\")}}\n",
"\n",
"Consider the following OCaml program:\n",
"\n",
"```ocaml\n",
"let f x = snd ((fun x -> x, x) (fst x))\n",
"```\n",
"\n",
"- What is the type of that program?\n",
"- What is the proposition corresponding to that type?\n",
"- How would `f (1,2)` evaluate in the small-step semantics?\n",
"- What simplified implementation of `f` does that evaluation suggest? (or\n",
" perhaps there are several, though one is probably the simplest?)\n",
"- Does your simplified `f` still have the same type as the original? (It\n",
" should.)\n",
"\n",
"Your simplified `f` and the original `f` are both proofs of the same\n",
"proposition, but evaluation has helped you to produce a simpler proof."
]
}
],
"metadata": {
"jupytext": {
"cell_metadata_filter": "-all",
"formats": "md:myst",
"text_representation": {
"extension": ".md",
"format_name": "myst",
"format_version": 0.13,
"jupytext_version": "1.10.3"
}
},
"kernelspec": {
"display_name": "OCaml",
"language": "OCaml",
"name": "ocaml-jupyter"
},
"language_info": {
"codemirror_mode": "text/x-ocaml",
"file_extension": ".ml",
"mimetype": "text/x-ocaml",
"name": "OCaml",
"nbconverter_exporter": null,
"pygments_lexer": "OCaml",
"version": "4.14.0"
},
"source_map": [
14,
67,
69,
83,
87,
231,
233,
262,
264,
278,
281
]
},
"nbformat": 4,
"nbformat_minor": 5
}