{
"cells": [
{
"cell_type": "markdown",
"id": "c255eafb",
"metadata": {},
"source": [
"# Structural Induction\n",
"\n",
"So far we've proved the correctness of recursive functions on natural numbers.\n",
"We can do correctness proofs about recursive functions on variant types, too.\n",
"That requires us to figure out how induction works on variants. We'll do that,\n",
"next, starting with a variant type for representing natural numbers, then\n",
"generalizing to lists, trees, and other variants. This inductive proof technique\n",
"is sometimes known as *structural induction* instead of *mathematical\n",
"induction*. But that's just a piece of vocabulary; don't get hung up on it. The\n",
"core idea is completely the same.\n",
"\n",
"## Induction on Naturals\n",
"\n",
"{{ video_embed | replace(\"%%VID%%\", \"Lkb-eTUrHTs\")}}\n",
"\n",
"We used OCaml's `int` type as a representation of the naturals. Of course, that\n",
"type is somewhat of a mismatch: negative `int` values don't represent naturals,\n",
"and there is an upper bound to what natural numbers we can represent with `int`.\n",
"\n",
"Let's fix those problems by defining our own variant to represent natural\n",
"numbers:"
]
},
{
"cell_type": "code",
"execution_count": 1,
"id": "c20c2956",
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"type nat = Z | S of nat\n"
]
},
"execution_count": 1,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"type nat = Z | S of nat"
]
},
{
"cell_type": "markdown",
"id": "e3296b14",
"metadata": {},
"source": [
"The constructor `Z` represents zero; and the constructor `S` represents the\n",
"successor of another natural number. So,\n",
"\n",
"- 0 is represented by `Z`,\n",
"- 1 by `S Z`,\n",
"- 2 by `S (S Z)`,\n",
"- 3 by `S (S (S Z))`,\n",
"\n",
"and so forth. This variant is thus a *unary* (as opposed to binary or decimal)\n",
"representation of the natural numbers: the number of times `S` occurs in a value\n",
"`n : nat` is the natural number that `n` represents.\n",
"\n",
"We can define addition on natural numbers with the following function:"
]
},
{
"cell_type": "code",
"execution_count": 2,
"id": "4075e65c",
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"val plus : nat -> nat -> nat = \n"
]
},
"execution_count": 2,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"let rec plus a b =\n",
" match a with\n",
" | Z -> b\n",
" | S k -> S (plus k b)"
]
},
{
"cell_type": "markdown",
"id": "e5aa4da7",
"metadata": {},
"source": [
"Immediately we can prove the following rather trivial claim:\n",
"\n",
"```text\n",
"Claim: plus Z n = n\n",
"\n",
"Proof:\n",
"\n",
" plus Z n\n",
"= { evaluation }\n",
" n\n",
"\n",
"QED\n",
"```\n",
"\n",
"But suppose we want to prove this also trivial-seeming claim:\n",
"\n",
"```text\n",
"Claim: plus n Z = n\n",
"\n",
"Proof:\n",
"\n",
" plus n Z\n",
"=\n",
" ???\n",
"```\n",
"\n",
"We can't just evaluate `plus n Z`, because `plus` matches against its first\n",
"argument, not second. One possibility would be to do a case analysis: what if\n",
"`n` is `Z`, vs. `S k` for some `k`? Let's attempt that.\n",
"\n",
"```text\n",
"Proof:\n",
"\n",
"By case analysis on n, which must be either Z or S k.\n",
"\n",
"Case: n = Z\n",
"\n",
" plus Z Z\n",
"= { evaluation }\n",
" Z\n",
"\n",
"Case: n = S k\n",
"\n",
" plus (S k) Z\n",
"= { evaluation }\n",
" S (plus k Z)\n",
"=\n",
" ???\n",
"```\n",
"\n",
"We are again stuck, and for the same reason: once more `plus` can't be evaluated\n",
"any further.\n",
"\n",
"When you find yourself needing to solve the same subproblem in programming, you\n",
"use recursion. When it happens in a proof, you use induction!\n",
"\n",
"We'll need an induction principle for `nat`. Here it is:\n",
"\n",
"```text\n",
"forall properties P,\n",
" if P(Z),\n",
" and if forall k, P(k) implies P(S k),\n",
" then forall n, P(n)\n",
"```\n",
"\n",
"Compare that to the induction principle we used for natural numbers before,\n",
"when we were using `int` in place of natural numbers:\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",
"There's no essential difference between the two: we just use `Z` in place of\n",
"`0`, and `S k` in place of `k + 1`.\n",
"\n",
"Using that induction principle, we can carry out the proof:\n",
"\n",
"```text\n",
"Claim: plus n Z = n\n",
"\n",
"Proof: by induction on n.\n",
"P(n) = plus n Z = n\n",
"\n",
"Base case: n = Z\n",
"Show: plus Z Z = Z\n",
"\n",
" plus Z Z\n",
"= { evaluation }\n",
" Z\n",
"\n",
"Inductive case: n = S k\n",
"IH: plus k Z = k\n",
"Show: plus (S k) Z = S k\n",
"\n",
" plus (S k) Z\n",
"= { evaluation }\n",
" S (plus k Z)\n",
"= { IH }\n",
" S k\n",
"\n",
"QED\n",
"```\n",
"\n",
"## Induction on Lists\n",
"\n",
"{{ video_embed | replace(\"%%VID%%\", \"Xo3rW_dTqEg\")}}\n",
"\n",
"It turns out that natural numbers and lists are quite similar, when viewed\n",
"as data types. Here are the definitions of both, aligned for comparison:\n",
"\n",
"```ocaml\n",
"type nat = Z | S of nat\n",
"type 'a list = [] | ( :: ) of 'a * 'a list\n",
"```\n",
"\n",
"Both types have a constructor representing a concept of \"nothing\". Both types\n",
"also have a constructor representing \"one more\" than another value of the type:\n",
"`S n` is one more than `n`, and `h :: t` is a list with one more element than\n",
"`t`.\n",
"\n",
"The induction principle for lists is likewise quite similar to the induction\n",
"principle for natural numbers. Here is the principle for lists:\n",
"\n",
"```text\n",
"forall properties P,\n",
" if P([]),\n",
" and if forall h t, P(t) implies P(h :: t),\n",
" then forall lst, P(lst)\n",
"```\n",
"\n",
"An inductive proof for lists therefore has the following structure:\n",
"\n",
"```text\n",
"Proof: by induction on lst.\n",
"P(lst) = ...\n",
"\n",
"Base case: lst = []\n",
"Show: P([])\n",
"\n",
"Inductive case: lst = h :: t\n",
"IH: P(t)\n",
"Show: P(h :: t)\n",
"```\n",
"\n",
"Let's try an example of this kind of proof. Recall the definition of the append\n",
"operator:"
]
},
{
"cell_type": "code",
"execution_count": 3,
"id": "13ae8453",
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"val append : 'a list -> 'a list -> 'a list = \n"
]
},
"execution_count": 3,
"metadata": {},
"output_type": "execute_result"
},
{
"data": {
"text/plain": [
"val ( @ ) : 'a list -> 'a list -> 'a list = \n"
]
},
"execution_count": 3,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"let rec append lst1 lst2 =\n",
" match lst1 with\n",
" | [] -> lst2\n",
" | h :: t -> h :: append t lst2\n",
"\n",
"let ( @ ) = append"
]
},
{
"cell_type": "markdown",
"id": "55dff643",
"metadata": {},
"source": [
"We'll prove that append is associative.\n",
"\n",
"```text\n",
"Theorem: forall xs ys zs, xs @ (ys @ zs) = (xs @ ys) @ zs\n",
"\n",
"Proof: by induction on xs.\n",
"P(xs) = forall ys zs, xs @ (ys @ zs) = (xs @ ys) @ zs\n",
"\n",
"Base case: xs = []\n",
"Show: forall ys zs, [] @ (ys @ zs) = ([] @ ys) @ zs\n",
"\n",
" [] @ (ys @ zs)\n",
"= { evaluation }\n",
" ys @ zs\n",
"= { evaluation }\n",
" ([] @ ys) @ zs\n",
"\n",
"Inductive case: xs = h :: t\n",
"IH: forall ys zs, t @ (ys @ zs) = (t @ ys) @ zs\n",
"Show: forall ys zs, (h :: t) @ (ys @ zs) = ((h :: t) @ ys) @ zs\n",
"\n",
" (h :: t) @ (ys @ zs)\n",
"= { evaluation }\n",
" h :: (t @ (ys @ zs))\n",
"= { IH }\n",
" h :: ((t @ ys) @ zs)\n",
"\n",
" ((h :: t) @ ys) @ zs\n",
"= { evaluation of inner @ }\n",
" (h :: (t @ ys)) @ zs\n",
"= { evaluation of outer @ }\n",
" h :: ((t @ ys) @ zs)\n",
"\n",
"QED\n",
"```\n",
"\n",
"{{ video_embed | replace(\"%%VID%%\", \"4B2jF2zHSCs\")}}\n",
"\n",
"\n",
"## A Theorem about Folding\n",
"\n",
"When we studied `List.fold_left` and `List.fold_right`, we discussed how they\n",
"sometimes compute the same function, but in general do not. For example,\n",
"\n",
"```\n",
" List.fold_left ( + ) 0 [1; 2; 3]\n",
"= (((0 + 1) + 2) + 3\n",
"= 6\n",
"= 1 + (2 + (3 + 0))\n",
"= List.fold_right ( + ) lst [1; 2; 3]\n",
"```\n",
"\n",
"but\n",
"\n",
"```\n",
" List.fold_left ( - ) 0 [1; 2; 3]\n",
"= (((0 - 1) - 2) - 3\n",
"= -6\n",
"<> 2\n",
"= 1 - (2 - (3 - 0))\n",
"= List.fold_right ( - ) lst [1; 2; 3]\n",
"```\n",
"\n",
"Based on the equations above, it looks like the fact that `+` is commutative and\n",
"associative, whereas `-` is not, explains this difference between when the two\n",
"fold functions get the same answer. Let's prove it!\n",
"\n",
"First, recall the definitions of the fold functions:"
]
},
{
"cell_type": "code",
"execution_count": 4,
"id": "29fc93f9",
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"val fold_left : ('a -> 'b -> 'a) -> 'a -> 'b list -> 'a = \n"
]
},
"execution_count": 4,
"metadata": {},
"output_type": "execute_result"
},
{
"data": {
"text/plain": [
"val fold_right : ('a -> 'b -> 'b) -> 'a list -> 'b -> 'b = \n"
]
},
"execution_count": 4,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"let rec fold_left f acc lst =\n",
" match lst with\n",
" | [] -> acc\n",
" | h :: t -> fold_left f (f acc h) t\n",
"\n",
"let rec fold_right f lst acc =\n",
" match lst with\n",
" | [] -> acc\n",
" | h :: t -> f h (fold_right f t acc)"
]
},
{
"cell_type": "markdown",
"id": "59e44888",
"metadata": {},
"source": [
"Second, recall what it means for a function `f : 'a -> 'a` to be commutative and\n",
"associative:\n",
"\n",
"```text\n",
"Commutative: forall x y, f x y = f y x\n",
"Associative: forall x y z, f x (f y z) = f (f x y) z\n",
"```\n",
"\n",
"Those might look a little different than the normal formulations of those\n",
"properties, because we are using `f` as a prefix operator. If we were to write\n",
"`f` instead as an infix operator `op`, they would look more familiar:\n",
"\n",
"```text\n",
"Commutative: forall x y, x op y = y op x\n",
"Associative: forall x y z, x op (y op z) = (x op y) op z\n",
"```\n",
"\n",
"When `f` is both commutative and associative we have this little interchange\n",
"lemma that lets us swap two arguments around:\n",
"\n",
"```\n",
"Lemma (interchange): f x (f y z) = f y (f x z)\n",
"\n",
"Proof:\n",
"\n",
" f x (f y z)\n",
"= { associativity }\n",
" f (f x y) z\n",
"= { commutativity }\n",
" f (f y x) z\n",
"= { associativity }\n",
" f y (f z x)\n",
"\n",
"QED\n",
"```\n",
"\n",
"Now we're ready to state and prove the theorem.\n",
"\n",
"```text\n",
"Theorem: If f is commutative and associative, then\n",
" forall lst acc,\n",
" fold_left f acc lst = fold_right f lst acc.\n",
"\n",
"Proof: by induction on lst.\n",
"P(lst) = forall acc,\n",
" fold_left f acc lst = fold_right f lst acc\n",
"\n",
"Base case: lst = []\n",
"Show: forall acc,\n",
" fold_left f acc [] = fold_right f [] acc\n",
"\n",
" fold_left f acc []\n",
"= { evaluation }\n",
" acc\n",
"= { evaluation }\n",
" fold_right f [] acc\n",
"\n",
"Inductive case: lst = h :: t\n",
"IH: forall acc,\n",
" fold_left f acc t = fold_right f t acc\n",
"Show: forall acc,\n",
" fold_left f acc (h :: t) = fold_right f (h :: t) acc\n",
"\n",
" fold_left f acc (h :: t)\n",
"= { evaluation }\n",
" fold_left f (f acc h) t\n",
"= { IH with acc := f acc h }\n",
" fold_right f t (f acc h)\n",
"\n",
" fold_right f (h :: t) acc\n",
"= { evaluation }\n",
" f h (fold_right f t acc)\n",
"```\n",
"\n",
"Now, it might seem as though we are stuck: the left and right sides of the\n",
"equality we want to show have failed to \"meet in the middle.\" But we're actually\n",
"in a similar situation to when we proved the correctness of `facti` earlier:\n",
"there's something (applying `f` to `h` and another argument) that we want to\n",
"push into the accumulator of that last line (so that we have `f acc h`).\n",
"\n",
"Let's try proving that with its own lemma:\n",
"\n",
"```text\n",
"Lemma: forall lst acc x,\n",
" f x (fold_right f lst acc) = fold_right f lst (f acc x)\n",
"\n",
"Proof: by induction on lst.\n",
"P(lst) = forall acc x,\n",
" f x (fold_right f lst acc) = fold_right f lst (f acc x)\n",
"\n",
"Base case: lst = []\n",
"Show: forall acc x,\n",
" f x (fold_right f [] acc) = fold_right f [] (f acc x)\n",
"\n",
" f x (fold_right f [] acc)\n",
"= { evaluation }\n",
" f x acc\n",
"\n",
" fold_right f [] (f acc x)\n",
"= { evaluation }\n",
" f acc x\n",
"= { commutativity of f }\n",
" f x acc\n",
"\n",
"Inductive case: lst = h :: t\n",
"IH: forall acc x,\n",
" f x (fold_right f t acc) = fold_right f t (f acc x)\n",
"Show: forall acc x,\n",
" f x (fold_right f (h :: t) acc) = fold_right f (h :: t) (f acc x)\n",
"\n",
" f x (fold_right f (h :: t) acc)\n",
"= { evaluation }\n",
" f x (f h (fold_right f t acc))\n",
"= { interchange lemma }\n",
" f h (f x (fold_right f t acc))\n",
"= { IH }\n",
" f h (fold_right f t (f acc x))\n",
"\n",
" fold_right f (h :: t) (f acc x)\n",
"= { evaluation }\n",
" f h (fold_right f t (f acc x))\n",
"\n",
"QED\n",
"```\n",
"\n",
"Now that the lemma is completed, we can resume the proof of the theorem. We'll\n",
"restart at the beginning of the inductive case:\n",
"\n",
"```text\n",
"Inductive case: lst = h :: t\n",
"IH: forall acc,\n",
" fold_left f acc t = fold_right f t acc\n",
"Show: forall acc,\n",
" fold_left f acc (h :: t) = fold_right f (h :: t) acc\n",
"\n",
" fold_left f acc (h :: t)\n",
"= { evaluation }\n",
" fold_left f (f acc h) t\n",
"= { IH with acc := f acc h }\n",
" fold_right f t (f acc h)\n",
"\n",
" fold_right f (h :: t) acc\n",
"= { evaluation }\n",
" f h (fold_right f t acc)\n",
"= { lemma with x := h and lst := t }\n",
" fold_right f t (f acc h)\n",
"\n",
"QED\n",
"```\n",
"\n",
"It took two inductions to prove the theorem, but we succeeded! Now we know that\n",
"the behavior we observed with `+` wasn't a fluke: any commutative and\n",
"associative operator causes `fold_left` and `fold_right` to get the same answer.\n",
"\n",
"## Induction on Trees\n",
"\n",
"{{ video_embed | replace(\"%%VID%%\", \"UJyE8ylHFA0\")}}\n",
"\n",
"Lists and binary trees are similar when viewed as data types. Here are the\n",
"definitions of both, aligned for comparison:"
]
},
{
"cell_type": "code",
"execution_count": 5,
"id": "b1b53768",
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"type 'a list = [] | (::) of 'a * 'a list\n"
]
},
"execution_count": 5,
"metadata": {},
"output_type": "execute_result"
},
{
"data": {
"text/plain": [
"type 'a tree = Leaf | Node of 'a tree * 'a * 'a tree\n"
]
},
"execution_count": 5,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"type 'a list = [] | ( :: ) of 'a * 'a list\n",
"type 'a tree = Leaf | Node of 'a tree * 'a * 'a tree"
]
},
{
"cell_type": "markdown",
"id": "c1590c22",
"metadata": {},
"source": [
"Both have a constructor that represents \"empty\", and both have a constructor\n",
"that combines a value of type `'a` together with another instance of the\n",
"data type. The only real difference is that `( :: )` takes just *one* list,\n",
"whereas `Node` takes *two* trees.\n",
"\n",
"The induction principle for binary trees is therefore very similar to the\n",
"induction principle for lists, except that with binary trees we get\n",
"*two* inductive hypotheses, one for each subtree:\n",
"\n",
"```text\n",
"forall properties P,\n",
" if P(Leaf),\n",
" and if forall l v r, (P(l) and P(r)) implies P(Node (l, v, r)),\n",
" then forall t, P(t)\n",
"```\n",
"\n",
"An inductive proof for binary trees therefore has the following structure:\n",
"\n",
"```text\n",
"Proof: by induction on t.\n",
"P(t) = ...\n",
"\n",
"Base case: t = Leaf\n",
"Show: P(Leaf)\n",
"\n",
"Inductive case: t = Node (l, v, r)\n",
"IH1: P(l)\n",
"IH2: P(r)\n",
"Show: P(Node (l, v, r))\n",
"```\n",
"\n",
"Let's try an example of this kind of proof. Here is a function that creates the\n",
"mirror image of a tree, swapping its left and right subtrees at all levels:"
]
},
{
"cell_type": "code",
"execution_count": 6,
"id": "b21deab3",
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"val reflect : 'a tree -> 'a tree = \n"
]
},
"execution_count": 6,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"let rec reflect = function\n",
" | Leaf -> Leaf\n",
" | Node (l, v, r) -> Node (reflect r, v, reflect l)"
]
},
{
"cell_type": "markdown",
"id": "06d290d7",
"metadata": {},
"source": [
"For example, these two trees are reflections of each other:\n",
"\n",
"```text\n",
" 1 1\n",
" / \\ / \\\n",
" 2 3 3 2\n",
" / \\ / \\ / \\ / \\\n",
"4 5 6 7 7 6 5 4\n",
"```\n",
"\n",
"If you take the mirror image of a mirror image, you should get the original\n",
"back. That means reflection is an *involution*, which is any function `f` such\n",
"that `f (f x) = x`. Another example of an involution is multiplication by\n",
"negative one on the integers.\n",
"\n",
"Let's prove that `reflect` is an involution.\n",
"\n",
"```text\n",
"Claim: forall t, reflect (reflect t) = t\n",
"\n",
"Proof: by induction on t.\n",
"P(t) = reflect (reflect t) = t\n",
"\n",
"Base case: t = Leaf\n",
"Show: reflect (reflect Leaf) = Leaf\n",
"\n",
" reflect (reflect Leaf)\n",
"= { evaluation }\n",
" reflect Leaf\n",
"= { evaluation }\n",
" Leaf\n",
"\n",
"Inductive case: t = Node (l, v, r)\n",
"IH1: reflect (reflect l) = l\n",
"IH2: reflect (reflect r) = r\n",
"Show: reflect (reflect (Node (l, v, r))) = Node (l, v, r)\n",
"\n",
" reflect (reflect (Node (l, v, r)))\n",
"= { evaluation }\n",
" reflect (Node (reflect r, v, reflect l))\n",
"= { evaluation }\n",
" Node (reflect (reflect l), v, reflect (reflect r))\n",
"= { IH1 }\n",
" Node (l, v, reflect (reflect r))\n",
"= { IH2 }\n",
" Node (l, v, r)\n",
"\n",
"QED\n",
"```\n",
"\n",
"Induction on trees is really no more difficult than induction on lists or\n",
"natural numbers. Just keep track of the inductive hypotheses, using our stylized\n",
"proof notation, and it isn't hard at all.\n",
"\n",
"{{ video_embed | replace(\"%%VID%%\", \"aiJDQeWL2G0\")}}\n",
"\n",
"## Induction Principles for All Variants\n",
"\n",
"We've now seen induction principles for `nat`, `list`, and `tree`. Generalizing\n",
"from what we've seen, each constructor of a variant either generates a base case\n",
"for the inductive proof, or an inductive case. And, if a constructor itself\n",
"carries values of that data type, each of those values generates an inductive\n",
"hypothesis. For example:\n",
"\n",
"- `Z`, `[]`, and `Leaf` all generated base cases.\n",
"\n",
"- `S`, `::`, and `Node` all generated inductive cases.\n",
"\n",
"- `S` and `::` each generated one IH, because each carries one value of the\n",
" data type.\n",
"\n",
"- `Node` generated two IHs, because it carries two values of the data type.\n",
"\n",
"As an example of an induction principle for a more complicated type, let's\n",
"consider a type that represents the syntax of a mathematical expression. You\n",
"might recall from an earlier data structures course that trees can be used for\n",
"that purpose.\n",
"\n",
"Suppose we have the following `expr` type, which is a kind of tree, to represent\n",
"expressions with integers, Booleans, unary operators, and binary operators:"
]
},
{
"cell_type": "code",
"execution_count": 7,
"id": "1c069bc8",
"metadata": {
"tags": [
"hide-output"
]
},
"outputs": [
{
"data": {
"text/plain": [
"type uop = UMinus\n"
]
},
"execution_count": 7,
"metadata": {},
"output_type": "execute_result"
},
{
"data": {
"text/plain": [
"type bop = BPlus | BMinus | BLeq\n"
]
},
"execution_count": 7,
"metadata": {},
"output_type": "execute_result"
},
{
"data": {
"text/plain": [
"type expr =\n",
" Int of int\n",
" | Bool of bool\n",
" | Unop of uop * expr\n",
" | Binop of expr * bop * expr\n"
]
},
"execution_count": 7,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"type uop =\n",
" | UMinus\n",
"\n",
"type bop =\n",
" | BPlus\n",
" | BMinus\n",
" | BLeq\n",
"\n",
"type expr =\n",
" | Int of int\n",
" | Bool of bool\n",
" | Unop of uop * expr\n",
" | Binop of expr * bop * expr"
]
},
{
"cell_type": "markdown",
"id": "8c63fd18",
"metadata": {},
"source": [
"For example, the expression `5 < 6` would be represented as\n",
"`Binop (Int 5, BLeq, Int 6)`. We'll see more examples of this kind of\n",
"representation later in the book when we study interpreters.\n",
"\n",
"The induction principle for `expr` is:\n",
"\n",
"```text\n",
"forall properties P,\n",
" if forall i, P(Int i)\n",
" and forall b, P(Bool b)\n",
" and forall u e, P(e) implies P(Unop (u, e))\n",
" and forall b e1 e2, (P(e1) and P(e2)) implies P(Binop (e1, b, e2))\n",
" then forall e, P(e)\n",
"```\n",
"\n",
"There are two base cases, corresponding to the two constructors that don't carry\n",
"an `expr`. There are two inductive cases, corresponding to the two constructors\n",
"that do carry `expr`s. `Unop` gets one IH, whereas `Binop` gets two IHs, because\n",
"of the number of `expr`s that each carries.\n",
"\n",
"## Induction and Recursion\n",
"\n",
"{{ video_embed | replace(\"%%VID%%\", \"J-x9hcNqRhY\")}}\n",
"\n",
"Inductive proofs and recursive programs bear a striking similarity. In a sense,\n",
"an inductive proof *is* a recursive program that shows how to construct evidence\n",
"for a theorem involving an algebraic data type (ADT). The **structure** of an ADT determines the structure of proofs and programs:\n",
"\n",
"- The **constructors** of an ADT are the organizational principle of both proofs\n",
" and programs. In a proof, we have a base or inductive case for each\n",
" constructor. In a program, we have a pattern-matching case for each\n",
" constructor.\n",
"\n",
"- The use of **recursive types** in an ADT determine where recursion occurs in\n",
" both proofs and programs. By \"recursive type\", we mean the occurrence of the\n",
" type in its own definition, such as the second `'a list` in\n",
" `type 'a list = [] | ( :: ) 'a * 'a list`. Such occurrences lead to \"smaller\"\n",
" values of a type occurring inside larger values. In a proof, we apply the\n",
" inductive hypothesis upon reaching such a smaller value. In a program, we\n",
" recurse on the smaller value."
]
}
],
"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,
38,
40,
56,
61,
213,
220,
291,
301,
464,
467,
503,
507,
590,
605
]
},
"nbformat": 4,
"nbformat_minor": 5
}