{
"cells": [
{
"cell_type": "markdown",
"id": "f2a915b1",
"metadata": {},
"source": [
"# Proving Correctness\n",
"\n",
"{{ video_embed | replace(\"%%VID%%\", \"48GBq4koKPs\")}}\n",
"\n",
"Testing provides evidence of correctness, but not full assurance. Even after\n",
"extensive black-box and glass-box testing, maybe there's still some test case\n",
"the programmer failed to invent, and that test case would reveal a fault in the\n",
"program.\n",
"\n",
"```{epigraph}\n",
"Program testing can be used to show the presence of bugs, but never to show their absence.\n",
"\n",
"-- Edsger W. Dijkstra\n",
"```\n",
"\n",
"The point is not that testing is useless! It can be quite effective. But it is a\n",
"kind of *inductive reasoning*, in which evidence (i.e., passing tests)\n",
"accumulates in support of a conclusion (i.e., correctness of the program)\n",
"without absolutely guaranteeing the validity of that conclusion. (Note that the\n",
"word \"inductive\" here is being used in a different sense than the proof\n",
"technique known as induction.) To get that guarantee, we turn to *deductive\n",
"reasoning*, in which we proceed from premises and rules about logic to a valid\n",
"conclusion. In other words, we prove the correctness of the program. Our goal,\n",
"next, is to learn some techniques for such correctness proofs. These techniques\n",
"are known as *formal methods* because of their use of logical formalism.\n",
"\n",
"*Correctness* here means that the program produces the right output\n",
"according to a *specification*. Specifications are usually provided in the\n",
"documentation of a function (hence the name \"specification comment\"): they\n",
"describe the program's precondition and postcondition. Postconditions, as we\n",
"have been writing them, have the form `[f x] is \"...a description of the output\n",
"in terms of the input [x]...\"`. For example, the specification of a factorial\n",
"function could be:\n",
"\n",
"```ocaml\n",
"(** [fact n] is [n!]. Requires: [n >= 0]. *)\n",
"let rec fact n = ...\n",
"```\n",
"\n",
"The postcondition is asserting an equality between the output of the function\n",
"and some English description of a computation on the input. *Formal\n",
"verification* is the task for proving that the implementation of the function\n",
"satisfies its specification.\n",
"\n",
"Equalities are one of the fundamental ways we think about correctness of\n",
"functional programs. The absence of mutable state makes it possible to reason\n",
"straightforwardly about whether two expressions are equal. It's difficult to do\n",
"that in an imperative language, because those expressions might have side\n",
"effects that change the state.\n",
"\n",
"## Equality\n",
"\n",
"{{ video_embed | replace(\"%%VID%%\", \"zjDUrMdVC5U\")}}\n",
"\n",
"When are two expressions equal? Two possible answers are:\n",
"\n",
"- When they are syntactically identical.\n",
"\n",
"- When they are semantically equivalent: they produce the same value.\n",
"\n",
"For example, are `42` and `41+1` equal? The syntactic answer would say they are\n",
"not, because they involve different tokens. The semantic answer would say they\n",
"are: they both produce the value `42`.\n",
"\n",
"What about functions: are `fun x -> x` and `fun y -> y` equal? Syntactically\n",
"they are different. But semantically, they both produce a value that is the\n",
"identity function: when they are applied to an input, they will both produce the\n",
"same output. That is, `(fun x -> x) z = z`, and `(fun y -> y) z = z`. If it is\n",
"the case that for all inputs two functions produce the same output, we will\n",
"consider the functions to be equal:\n",
"\n",
"```text\n",
"if (forall x, f x = g x), then f = g.\n",
"```\n",
"\n",
"That definition of equality for functions is known as the *Axiom of\n",
"Extensionality* in some branches of mathematics; henceforth we'll refer to it\n",
"simply as \"extensionality\".\n",
"\n",
"Here we will adopt the semantic approach. If `e1` and `e2` evaluate to the same\n",
"value `v`, then we write `e1 = e2`. We are using `=` here in a mathematical\n",
"sense of equality, not as the OCaml polymorphic equality operator. For example,\n",
"we allow `(fun x -> x) = (fun y -> y)`, even though OCaml's operator would raise\n",
"an exception and refuse to compare functions.\n",
"\n",
"We're also going to restrict ourselves to expressions that are well typed, pure\n",
"(meaning they have no side effects), and total (meaning they don't have\n",
"exceptions or infinite loops).\n",
"\n",
"## Equational Reasoning\n",
"\n",
"{{ video_embed | replace(\"%%VID%%\", \"MjpZJA1jIqU\")}}\n",
"\n",
"Consider these functions:"
]
},
{
"cell_type": "code",
"execution_count": 1,
"id": "43df651d",
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"val twice : ('a -> 'a) -> 'a -> 'a = \n"
]
},
"execution_count": 1,
"metadata": {},
"output_type": "execute_result"
},
{
"data": {
"text/plain": [
"val compose : ('a -> 'b) -> ('c -> 'a) -> 'c -> 'b = \n"
]
},
"execution_count": 1,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"let twice f x = f (f x)\n",
"let compose f g x = f (g x)"
]
},
{
"cell_type": "markdown",
"id": "e0023963",
"metadata": {},
"source": [
"We know from the rules of OCaml evaluation that `twice h x = h (h x)`, and\n",
"likewise, `compose h h x = h (h x)`. Thus we have:\n",
"\n",
"```ocaml\n",
"twice h x = h (h x) = compose h h x\n",
"```\n",
"\n",
"Therefore can conclude that `twice h x = compose h h x`. And by extensionality\n",
"we can simplify that equality: Since `twice h x = compose h h x` holds for all\n",
"`x`, we can conclude `twice h = compose h h`.\n",
"\n",
"As another example, suppose we define an infix operator for function\n",
"composition:\n",
"\n",
"```ocaml\n",
"let ( << ) = compose\n",
"```\n",
"\n",
"Then we can prove that composition is associative, using equational reasoning:\n",
"\n",
"```text\n",
"Theorem: (f << g) << h = f << (g << h)\n",
"\n",
"Proof: By extensionality, we need to show\n",
" ((f << g) << h) x = (f << (g << h)) x\n",
"for an arbitrary x.\n",
"\n",
" ((f << g) << h) x\n",
"= (f << g) (h x)\n",
"= f (g (h x))\n",
"\n",
"and\n",
"\n",
" (f << (g << h)) x\n",
"= f ((g << h) x)\n",
"= f (g (h x))\n",
"\n",
"So ((f << g) << h) x = f (g (h x)) = (f << (g << h)) x.\n",
"\n",
"QED\n",
"```\n",
"\n",
"All of the steps in the equational proof above follow from evaluation.\n",
"Another format for writing the proof would provide hints as to why\n",
"each step is valid:\n",
"\n",
"```text\n",
" ((f << g) << h) x\n",
"= { evaluation of << }\n",
" (f << g) (h x)\n",
"= { evaluation of << }\n",
" f (g (h x))\n",
"\n",
"and\n",
"\n",
" (f << (g << h)) x\n",
"= { evaluation of << }\n",
" f ((g << h) x)\n",
"= { evaluation of << }\n",
" f (g (h x))\n",
"```\n",
"\n",
"## Induction on Natural Numbers\n",
"\n",
"{{ video_embed | replace(\"%%VID%%\", \"By4VSmpzuHw\")}}\n",
"\n",
"The following function sums the non-negative integers up to `n`:"
]
},
{
"cell_type": "code",
"execution_count": 2,
"id": "c5be4697",
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"val sumto : int -> int = \n"
]
},
"execution_count": 2,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"let rec sumto n =\n",
" if n = 0 then 0 else n + sumto (n - 1)"
]
},
{
"cell_type": "markdown",
"id": "461cdae1",
"metadata": {},
"source": [
"You might recall that the same summation can be expressed in closed form as\n",
"`n * (n + 1) / 2`. To prove that `forall n >= 0, sumto n = n * (n + 1) / 2`, we\n",
"will need *mathematical induction*.\n",
"\n",
"Recall that induction on the natural numbers (i.e., the non-negative integers)\n",
"is formulated as follows:\n",
"\n",
"```text\n",
"forall properties P,\n",
" if P(0),\n",
" and if forall k, P(k) implies P(k + 1),\n",
" then forall n, P(n)\n",
"```\n",
"\n",
"That is called the *induction principle* for natural numbers. The *base case* is\n",
"to prove `P(0)`, and the *inductive case* is to prove that `P(k + 1)` holds\n",
"under the assumption of the *inductive hypothesis* `P(k)`.\n",
"\n",
"{{ video_embed | replace(\"%%VID%%\", \"JRNxlQYOLyw\")}}\n",
"\n",
"Let's use induction to prove the correctness of `sumto`.\n",
"\n",
"```text\n",
"Claim: sumto n = n * (n + 1) / 2\n",
"\n",
"Proof: by induction on n.\n",
"P(n) = sumto n = n * (n + 1) / 2\n",
"\n",
"Base case: n = 0\n",
"Show: sumto 0 = 0 * (0 + 1) / 2\n",
"\n",
" sumto 0\n",
"= { evaluation }\n",
" 0\n",
"= { algebra }\n",
" 0 * (0 + 1) / 2\n",
"\n",
"Inductive case: n = k + 1\n",
"Show: sumto (k + 1) = (k + 1) * ((k + 1) + 1) / 2\n",
"IH: sumto k = k * (k + 1) / 2\n",
"\n",
" sumto (k + 1)\n",
"= { evaluation }\n",
" k + 1 + sumto k\n",
"= { IH }\n",
" k + 1 + k * (k + 1) / 2\n",
"= { algebra }\n",
" (k + 1) * (k + 2) / 2\n",
"\n",
"QED\n",
"```\n",
"\n",
"Note that we have been careful in each of the cases to write out what we need to\n",
"show, as well as to write down the inductive hypothesis. It is important to show\n",
"all this work.\n",
"\n",
"Suppose we now define:"
]
},
{
"cell_type": "code",
"execution_count": 3,
"id": "1361d8fe",
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"val sumto_closed : int -> int = \n"
]
},
"execution_count": 3,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"let sumto_closed n = n * (n + 1) / 2"
]
},
{
"cell_type": "markdown",
"id": "014cb2a6",
"metadata": {},
"source": [
"Then as a corollary to our previous claim, by extensionality we can conclude\n",
"\n",
"```text\n",
"sumto_closed = sumto\n",
"```\n",
"\n",
"Technically that equality holds only inputs that are natural numbers. But since\n",
"all our examples henceforth will be for naturals, not integers per se, we will\n",
"elide stating any preconditions or restrictions regarding natural numbers.\n",
"\n",
"## Programs as Specifications\n",
"\n",
"We have just proved the correctness of an efficient implementation relative to\n",
"an inefficient implementation. The inefficient implementation, `sumto`, serves\n",
"as a specification for the efficient implementation, `sumto_closed`.\n",
"\n",
"That technique is common in verifying functional programs: write an obviously\n",
"correct implementation that is lacking in some desired property, such as\n",
"efficiency, then prove that a better implementation is equal to the original.\n",
"\n",
"Let's do another example of this kind of verification. This time, well use the\n",
"factorial function.\n",
"\n",
"{{ video_embed | replace(\"%%VID%%\", \"htMNllWnLzg\")}}\n",
"\n",
"The simple, obviously correct implementation of factorial would be:"
]
},
{
"cell_type": "code",
"execution_count": 4,
"id": "4c02741d",
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"val fact : int -> int = \n"
]
},
"execution_count": 4,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"let rec fact n =\n",
" if n = 0 then 1 else n * fact (n - 1)"
]
},
{
"cell_type": "markdown",
"id": "95feb158",
"metadata": {},
"source": [
"A tail-recursive implementation would be more efficient about stack space:"
]
},
{
"cell_type": "code",
"execution_count": 5,
"id": "ef73b280",
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"val facti : int -> int -> int = \n"
]
},
"execution_count": 5,
"metadata": {},
"output_type": "execute_result"
},
{
"data": {
"text/plain": [
"val fact_tr : int -> int = \n"
]
},
"execution_count": 5,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"let rec facti acc n =\n",
" if n = 0 then acc else facti (acc * n) (n - 1)\n",
"\n",
"let fact_tr n = facti 1 n"
]
},
{
"cell_type": "markdown",
"id": "73ed93a2",
"metadata": {},
"source": [
"The `i` in the name `facti` stands for *iterative*. We call this an iterative\n",
"implementation because it strongly resembles how the same computation would be\n",
"expressed using a loop (that is, an iteration construct) in an imperative\n",
"language. For example, in Java we might write:\n",
"\n",
"```java\n",
"int facti (int n) {\n",
" int acc = 1;\n",
" while (n != 0) {\n",
" acc *= n;\n",
" n--;\n",
" }\n",
" return acc;\n",
"}\n",
"```\n",
"\n",
"Both the OCaml and Java implementation of `facti` share these features:\n",
"\n",
"- they start `acc` at `1`\n",
"- they check whether `n` is `0`\n",
"- they multiply `acc` by `n`\n",
"- they decrement `n`\n",
"- they return the accumulator, `acc`\n",
"\n",
"Let's try to prove that `fact_tr` correctly implements the same computation as\n",
"`fact`.\n",
"\n",
"```text\n",
"Claim: forall n, fact n = fact_tr n\n",
"\n",
"Since fact_tr n = facti 1 n, it suffices to show fact n = facti 1 n.\n",
"\n",
"Proof: by induction on n.\n",
"P(n) = fact n = facti 1 n\n",
"\n",
"Base case: n = 0\n",
"Show: fact 0 = facti 1 0\n",
"\n",
" fact 0\n",
"= { evaluation }\n",
" 1\n",
"= { evaluation }\n",
" facti 1 0\n",
"\n",
"Inductive case: n = k + 1\n",
"Show: fact (k + 1) = facti 1 (k + 1)\n",
"IH: fact k = facti 1 k\n",
"\n",
" fact (k + 1)\n",
"= { evaluation }\n",
" (k + 1) * fact k\n",
"= { IH }\n",
" (k + 1) * facti 1 k\n",
"\n",
" facti 1 (k + 1)\n",
"= { evaluation }\n",
" facti (1 * (k + 1)) k\n",
"= { evaluation }\n",
" facti (k + 1) k\n",
"\n",
"Unfortunately, we're stuck. Neither side of what we want to show\n",
"can be manipulated any further.\n",
"\n",
"ABORT\n",
"```\n",
"\n",
"We know that `facti (k + 1) k` and `(k + 1) * facti 1 k` should yield the same\n",
"value. But the IH allows us only to use `1` as the second argument to `facti`,\n",
"instead of a bigger argument like `k + 1`. So our proof went astray the moment\n",
"we used the IH. We need a stronger inductive hypothesis!\n",
"\n",
"So let's strengthen the claim we are making. Instead of showing that\n",
"`fact n = facti 1 n`, we'll try to show `forall p, p * fact n = facti p n`. That\n",
"generalizes the `k + 1` we were stuck on to an arbitrary quantity `p`.\n",
"\n",
"```text\n",
"Claim: forall n, forall p . p * fact n = facti p n\n",
"\n",
"Proof: by induction on n.\n",
"P(n) = forall p, p * fact n = facti p n\n",
"\n",
"Base case: n = 0\n",
"Show: forall p, p * fact 0 = facti p 0\n",
"\n",
" p * fact 0\n",
"= { evaluation and algebra }\n",
" p\n",
"= { evaluation }\n",
" facti p 0\n",
"\n",
"Inductive case: n = k + 1\n",
"Show: forall p, p * fact (k + 1) = facti p (k + 1)\n",
"IH: forall p, p * fact k = facti p k\n",
"\n",
" p * fact (k + 1)\n",
"= { evaluation }\n",
" p * (k + 1) * fact k\n",
"= { IH, instantiating its p as p * (k + 1) }\n",
" facti (p * (k + 1)) k\n",
"\n",
" facti p (k + 1)\n",
"= { evaluation }\n",
" facti (p * (k + 1)) k\n",
"\n",
"QED\n",
"\n",
"Claim: forall n, fact n = fact_tr n\n",
"\n",
"Proof:\n",
"\n",
" fact n\n",
"= { algebra }\n",
" 1 * fact n\n",
"= { previous claim }\n",
" facti 1 n\n",
"= { evaluation }\n",
" fact_tr n\n",
"\n",
"QED\n",
"```\n",
"\n",
"That finishes our proof that the efficient, tail-recursive function `fact_tr` is\n",
"equivalent to the simple, recursive function `fact`. In essence, we have proved\n",
"the correctness of `fact_tr` using `fact` as its specification.\n",
"\n",
"## Recursion vs. Iteration\n",
"\n",
"We added an accumulator as an extra argument to make the factorial function be\n",
"tail recursive. That's a trick we've seen before. Let's abstract and see how to\n",
"do it in general.\n",
"\n",
"Suppose we have a recursive function over integers:\n",
"\n",
"```ocaml\n",
"let rec f_r n =\n",
" if n = 0 then i else op n (f_r (n - 1))\n",
"```\n",
"\n",
"Here, the `r` in `f_r` is meant to suggest that `f_r` is a recursive function.\n",
"The `i` and `op` are pieces of the function that are meant to be replaced by\n",
"some concrete value `i` and operator `op`. For example, with the factorial\n",
"function, we have:\n",
"\n",
"```ocaml\n",
"f_r = fact\n",
"i = 1\n",
"op = ( * )\n",
"```\n",
"\n",
"Such a function can be made tail recursive by rewriting it as follows:\n",
"\n",
"```ocaml\n",
"let rec f_i acc n =\n",
" if n = 0 then acc\n",
" else f_i (op acc n) (n - 1)\n",
"\n",
"let f_tr = f_i i\n",
"```\n",
"\n",
"Here, the `i` in `f_i` is meant to suggest that `f_i` is an iterative function,\n",
"and `i` and `op` are the same as in the recursive version of the function. For\n",
"example, with factorial we have:\n",
"\n",
"```ocaml\n",
"f_i = fact_i\n",
"i = 1\n",
"op = ( * )\n",
"f_tr = fact_tr\n",
"```\n",
"\n",
"We can prove that `f_r` and `f_tr` compute the same function. During the proof,\n",
"next, we will discover certain conditions that must hold of `i` and `op` to make\n",
"the transformation to tail recursion be correct.\n",
"\n",
"```text\n",
"Theorem: f_r = f_tr\n",
"\n",
"Proof: By extensionality, it suffices to show that forall n, f_r n = f_tr n.\n",
"\n",
"As in the previous proof for fact, we will need a strengthened induction\n",
"hypothesis. So we first prove this lemma, which quantifies over all accumulators\n",
"that could be input to f_i, rather than only i:\n",
"\n",
" Lemma: forall n, forall acc, op acc (f_r n) = f_i acc n\n",
"\n",
" Proof of Lemma: by induction on n.\n",
" P(n) = forall acc, op acc (f_r n) = f_i acc n\n",
"\n",
" Base: n = 0\n",
" Show: forall acc, op acc (f_r 0) = f_i acc 0\n",
"\n",
" op acc (f_r 0)\n",
" = { evaluation }\n",
" op acc i\n",
" = { if we assume forall x, op x i = x }\n",
" acc\n",
"\n",
" f_i acc 0\n",
" = { evaluation }\n",
" acc\n",
"\n",
" Inductive case: n = k + 1\n",
" Show: forall acc, op acc (f_r (k + 1)) = f_i acc (k + 1)\n",
" IH: forall acc, op acc (f_r k) = f_i acc k\n",
"\n",
" op acc (f_r (k + 1))\n",
" = { evaluation }\n",
" op acc (op (k + 1) (f_r k))\n",
" = { if we assume forall x y z, op x (op y z) = op (op x y) z }\n",
" op (op acc (k + 1)) (f_r k)\n",
"\n",
" f_i acc (k + 1)\n",
" = { evaluation }\n",
" f_i (op acc (k + 1)) k\n",
" = { IH, instantiating acc as op acc (k + 1)}\n",
" op (op acc (k + 1)) (f_r k)\n",
"\n",
" QED\n",
"\n",
"The proof then follows almost immediately from the lemma:\n",
"\n",
" f_r n\n",
"= { if we assume forall x, op i x = x }\n",
" op i (f_r n)\n",
"= { lemma, instantiating acc as i }\n",
" f_i i n\n",
"= { evaluation }\n",
" f_tr n\n",
"\n",
"QED\n",
"```\n",
"\n",
"Along the way we made three assumptions about i and op:\n",
"\n",
"1. `forall x, op x i = x`\n",
"2. `op x (op y z) = op (op x y) z`\n",
"3. `forall x, op i x = x`\n",
"\n",
"The first and third say that `i` is an *identity* of `op`: using it on the left\n",
"or right side leaves the other argument `x` unchanged. The second says that `op`\n",
"is *associative*. Both those assumptions held for the values we used in the\n",
"factorial functions:\n",
"\n",
"- `op` is multiplication, which is associative.\n",
"- `i` is `1`, which is an identity of multiplication: multiplication by 1 leaves\n",
" the other argument unchanged.\n",
"\n",
"So our transformation from a recursive to a tail-recursive function is valid as\n",
"long as the operator applied in the recursive call is associative, and the value\n",
"returned in the base case is an identity of that operator.\n",
"\n",
"Returning to the `sumto` function, we can apply the theorem we just proved to\n",
"immediately get a tail-recursive version:"
]
},
{
"cell_type": "code",
"execution_count": 6,
"id": "a698d103",
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"val sumto_r : int -> int = \n"
]
},
"execution_count": 6,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"let rec sumto_r n =\n",
" if n = 0 then 0 else n + sumto_r (n - 1)"
]
},
{
"cell_type": "markdown",
"id": "7fda6118",
"metadata": {},
"source": [
"Here, the operator is addition, which is associative; and the base case is zero,\n",
"which is an identity of addition. Therefore our theorem applies, and we can use\n",
"it to produce the tail-recursive version without even having to think about it:"
]
},
{
"cell_type": "code",
"execution_count": 7,
"id": "4543748d",
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"val sumto_i : int -> int -> int = \n"
]
},
"execution_count": 7,
"metadata": {},
"output_type": "execute_result"
},
{
"data": {
"text/plain": [
"val sumto_tr : int -> int = \n"
]
},
"execution_count": 7,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"let rec sumto_i acc n =\n",
" if n = 0 then acc else sumto_i (acc + n) (n - 1)\n",
"\n",
"let sumto_tr = sumto_i 0"
]
},
{
"cell_type": "markdown",
"id": "d38ae8de",
"metadata": {},
"source": [
"We already know that `sumto_tr` is correct, thanks to our theorem.\n",
"\n",
"## Termination\n",
"\n",
"{{ video_embed | replace(\"%%VID%%\", \"Xy7GTfEfIK4\")}}\n",
"\n",
"Sometimes correctness of programs is further divided into:\n",
"\n",
"- **partial correctness**: meaning that *if* a program terminates, then its\n",
" output is correct; and\n",
"\n",
"- **total correctness**: meaning that a program *does* terminate, *and* its\n",
" output is correct.\n",
"\n",
"Total correctness is therefore the conjunction of partial correctness and\n",
"termination. Thus far, we have been proving partial correctness.\n",
"\n",
"To prove that a program terminates is difficult. Indeed, it is impossible in\n",
"general for an algorithm to do so: a computer can't precisely decide whether a\n",
"program will terminate. (Look up the \"halting problem\" for more details.) But, a\n",
"smart human sometimes can do so.\n",
"\n",
"There is a simple heuristic that can be used to show that a recursive function\n",
"terminates:\n",
"\n",
"- All recursive calls are on a \"smaller\" input, and\n",
"- all base cases are terminating.\n",
"\n",
"For example, consider the factorial function:"
]
},
{
"cell_type": "code",
"execution_count": 8,
"id": "11efa058",
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"val fact : int -> int = \n"
]
},
"execution_count": 8,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"let rec fact n =\n",
" if n = 0 then 1\n",
" else n * fact (n - 1)"
]
},
{
"cell_type": "markdown",
"id": "ec4eab34",
"metadata": {},
"source": [
"The base case, `1`, obviously terminates. The recursive call is on `n - 1`,\n",
"which is a smaller input than the original `n`. So `fact` always terminates (as\n",
"long as its input is a natural number).\n",
"\n",
"The same reasoning applies to all the other functions we've discussed above.\n",
"\n",
"To make this more precise, we need a notion of what it means to be smaller.\n",
"Suppose we have a binary relation `<` on inputs. Despite the notation, this\n",
"relation need not be the less-than relation on integers---although that will\n",
"work for `fact`. Also suppose that it is never possible to create an infinite\n",
"sequence `x0 > x1 > x2 > x3 ...` of elements using this relation. (Where of\n",
"course `a > b` iff `b < a`.) That is, there are no infinite descending chains of\n",
"elements: once you pick a starting element `x0`, there can be only a finite\n",
"number of \"descents\" according to the `<` relation before you bottom out and hit\n",
"a base case. This property of `<` makes it a *well-founded relation*.\n",
"\n",
"So, a recursive function terminates if all its recursive calls are on elements\n",
"that are smaller according to `<`. Why? Because there can be only a finite\n",
"number of calls before a base case is reached, and base cases must terminate.\n",
"\n",
"The usual `<` relation is well-founded on the natural numbers, because\n",
"eventually any chain must reach the base case of 0. But it is not well-founded\n",
"on the integers, which can get just keep getting smaller: `-1 > -2 > -3 > ...`.\n",
"\n",
"Here's an interesting function for which the usual `<` relation doesn't suffice\n",
"to prove termination:"
]
},
{
"cell_type": "code",
"execution_count": 9,
"id": "dc413ed8",
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"val ack : int * int -> int = \n"
]
},
"execution_count": 9,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"let rec ack = function\n",
" | (0, n) -> n + 1\n",
" | (m, 0) -> ack (m - 1, 1)\n",
" | (m, n) -> ack (m - 1, ack (m, n - 1))"
]
},
{
"cell_type": "markdown",
"id": "9c570b63",
"metadata": {},
"source": [
"This is known as *Ackermann's function*. It grows faster than any exponential\n",
"function. Try running `ack (1, 1)`, `ack (2, 1)`, `ack (3, 1)`, then `ack (4,\n",
"1)` to get a sense of that. It also is a famous example of a function that can\n",
"be implemented with `while` loops but not with `for` loops. Nonetheless, it does\n",
"terminate.\n",
"\n",
"To show that, the base case is easy: when the input is `(0, _)`, the function\n",
"terminates. But in other cases, it makes a recursive call, and we need to define\n",
"an appropriate `<` relation. It turns out *lexicographic ordering* on pairs\n",
"works. Define `(a, b) < (c, d)` if:\n",
"\n",
"- `a < c`, or\n",
"- `a = c` and `b < d`.\n",
"\n",
"The `<` order in those two cases is the usual `<` on natural numbers.\n",
"\n",
"In the first recursive call, `(m - 1, 1) < (m, 0)` by the first case of the\n",
"definition of `<`, because `m - 1 < m`. In the nested recursive call\n",
"`ack (m - 1, ack (m, n - 1))`, both cases are needed:\n",
"\n",
"- `(m, n - 1) < (m, n)` because `m = m` and `n - 1 < n`\n",
"- `(m - 1, _) < (m, n)` because `m - 1 < m`."
]
}
],
"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,
111,
114,
184,
187,
247,
249,
278,
281,
285,
290,
546,
549,
555,
560,
592,
596,
625,
630
]
},
"nbformat": 4,
"nbformat_minor": 5
}