{
"cells": [
{
"cell_type": "markdown",
"id": "24fd8b94",
"metadata": {},
"source": [
"# Algebraic Specification\n",
"\n",
"Next let's tackle a bigger challenge: proving the correctness of a data\n",
"structure, such as a stack, queue, or set.\n",
"\n",
"Correctness proofs always need specifications. In proving the correctness of\n",
"iterative factorial, we used recursive factorial as a specification. By analogy,\n",
"we could provide two implementations of a data structure---one simple, the other\n",
"complex and efficient---and prove that the two are equivalent. That would\n",
"require us to introduce ways to translate between the two implementations. For\n",
"example, we could prove the correctness of a map implemented with an efficient\n",
"balanced binary search tree relative to an implementation as an inefficient\n",
"association list, by defining functions to convert trees to lists. Such an\n",
"approach is certainly valid, but it doesn't lead to new ideas about verification\n",
"for us to study.\n",
"\n",
"Instead, we will pursue a different approach based on *equational\n",
"specifications*, aka *algebraic specifications*. The idea with these is to\n",
"\n",
"- define the types of the data structure operations, and\n",
"\n",
"- to write a set of equations that define how the operations interact with one\n",
" another.\n",
"\n",
"The reason the word \"algebra\" shows up here is (in part) that this\n",
"type-and-equation based approach is something we learned in high-school algebra.\n",
"For example, here is a specification for some operators:\n",
"\n",
"```ocaml\n",
"0 : int\n",
"1 : int\n",
"- : int -> int\n",
"+ : int -> int -> int\n",
"* : int -> int -> int\n",
"\n",
"(a + b) + c = a + (b + c)\n",
"a + b = b + a\n",
"a + 0 = a\n",
"a + (-a) = 0\n",
"(a * b) * c = a * (b * c)\n",
"a * b = b * a\n",
"a * 1 = a\n",
"a * 0 = 0\n",
"a * (b + c) = a * b + a * c\n",
"```\n",
"\n",
"The types of those operators, and the associated equations, are facts learned\n",
"when studying algebra.\n",
"\n",
"Our goal is now to write similar specifications for data structures, and use\n",
"them to reason about the correctness of implementations.\n",
"\n",
"## Example: Stacks\n",
"\n",
"{{ video_embed | replace(\"%%VID%%\", \"Pyz2xEzD2cY\")}}\n",
"\n",
"Here are a few familiar operations on stacks along with their types."
]
},
{
"cell_type": "code",
"execution_count": 1,
"id": "5b2ba652",
"metadata": {
"tags": [
"hide-output"
]
},
"outputs": [
{
"data": {
"text/plain": [
"module type Stack =\n",
" sig\n",
" type 'a t\n",
" val empty : 'a t\n",
" val is_empty : 'a t -> bool\n",
" val peek : 'a t -> 'a\n",
" val push : 'a -> 'a t -> 'a t\n",
" val pop : 'a t -> 'a t\n",
" end\n"
]
},
"execution_count": 1,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"module type Stack = sig\n",
" type 'a t\n",
" val empty : 'a t\n",
" val is_empty : 'a t -> bool\n",
" val peek : 'a t -> 'a\n",
" val push : 'a -> 'a t -> 'a t\n",
" val pop : 'a t -> 'a t\n",
"end"
]
},
{
"cell_type": "markdown",
"id": "8e5d5181",
"metadata": {},
"source": [
"As usual, there is a design choice to be made with `peek` etc. about what to do\n",
"with empty stacks. Here we have not used `option`, which suggests that `peek`\n",
"will raise an exception on the empty stack. So we are cautiously relaxing our\n",
"prohibition on exceptions.\n",
"\n",
"In the past we've given these operations specifications in English, e.g.,\n",
"\n",
"```ocaml\n",
" (** [push x s] is the stack [s] with [x] pushed on the top. *)\n",
" val push : 'a -> 'a stack -> 'a stack\n",
"```\n",
"\n",
"But now, we'll write some equations to describe how the operations work:\n",
"\n",
"```text\n",
"1. is_empty empty = true\n",
"2. is_empty (push x s) = false\n",
"3. peek (push x s) = x\n",
"4. pop (push x s) = s\n",
"```\n",
"\n",
"(Later we'll return to the question of *how* to design such equations.) The\n",
"variables appearing in these equations are implicitly universally quantified.\n",
"Here's how to read each equation:\n",
"\n",
"1. `is_empty empty = true`. The empty stack is empty.\n",
"\n",
"2. `is_empty (push x s) = false`. A stack that has just been pushed is\n",
" non-empty.\n",
"\n",
"3. `peek (push x s) = x`. Pushing then immediately peeking yields whatever\n",
" value was pushed.\n",
"\n",
"4. `pop (push x s) = s`. Pushing then immediately popping yields the original\n",
" stack.\n",
"\n",
"Just with these equations alone, we already can deduce a lot about how any\n",
"sequence of stack operations must work. For example,\n",
"\n",
"```text\n",
" peek (pop (push 1 (push 2 empty)))\n",
"= { equation 4 }\n",
" peek (push 2 empty)\n",
"= { equation 3 }\n",
" 2\n",
"```\n",
"\n",
"And `peek empty` doesn't equal any value according to the equations, since there\n",
"is no equation of the form `peek empty = ...`. All that is true regardless of\n",
"the stack implementation that is chosen: any correct implementation must cause\n",
"the equations to hold.\n",
"\n",
"Suppose we implemented stacks as lists, as follows:"
]
},
{
"cell_type": "code",
"execution_count": 2,
"id": "1ef08345",
"metadata": {
"tags": [
"hide-output"
]
},
"outputs": [
{
"data": {
"text/plain": [
"module ListStack :\n",
" sig\n",
" type 'a t = 'a list\n",
" val empty : 'a list\n",
" val is_empty : 'a list -> bool\n",
" val peek : 'a list -> 'a\n",
" val push : 'a -> 'a list -> 'a list\n",
" val pop : 'a list -> 'a list\n",
" end\n"
]
},
"execution_count": 2,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"module ListStack = struct\n",
" type 'a t = 'a list\n",
" let empty = []\n",
" let is_empty = function [] -> true | _ -> false\n",
" let peek = List.hd\n",
" let push = List.cons\n",
" let pop = List.tl\n",
"end"
]
},
{
"cell_type": "markdown",
"id": "a0d71441",
"metadata": {},
"source": [
"Next we could *prove* that each equation holds of the implementation. All these\n",
"proofs are quite easy by now, and proceed entirely by evaluation. For example,\n",
"here's a proof of equation 3:\n",
"\n",
"```text\n",
" peek (push x s)\n",
"= { evaluation }\n",
" peek (x :: s)\n",
"= { evaluation }\n",
" x\n",
"```\n",
"\n",
"## Example: Queues\n",
"\n",
"{{ video_embed | replace(\"%%VID%%\", \"lAJz6ZnsbNI\")}}\n",
"\n",
"Stacks were easy. How about queues? Here is the specification:"
]
},
{
"cell_type": "code",
"execution_count": 3,
"id": "9560f0a8",
"metadata": {
"tags": [
"hide-output"
]
},
"outputs": [
{
"data": {
"text/plain": [
"module type Queue =\n",
" sig\n",
" type 'a t\n",
" val empty : 'a t\n",
" val is_empty : 'a t -> bool\n",
" val front : 'a t -> 'a\n",
" val enq : 'a -> 'a t -> 'a t\n",
" val deq : 'a t -> 'a t\n",
" end\n"
]
},
"execution_count": 3,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"module type Queue = sig\n",
" type 'a t\n",
" val empty : 'a t\n",
" val is_empty : 'a t -> bool\n",
" val front : 'a t -> 'a\n",
" val enq : 'a -> 'a t -> 'a t\n",
" val deq : 'a t -> 'a t\n",
"end"
]
},
{
"cell_type": "markdown",
"id": "9c01138b",
"metadata": {},
"source": [
"```text\n",
"1. is_empty empty = true\n",
"2. is_empty (enq x q) = false\n",
"3a. front (enq x q) = x if is_empty q = true\n",
"3b. front (enq x q) = front q if is_empty q = false\n",
"4a. deq (enq x q) = empty if is_empty q = true\n",
"4b. deq (enq x q) = enq x (deq q) if is_empty q = false\n",
"```\n",
"\n",
"The types of the queue operations are actually identical to the types\n",
"of the stack operations. Here they are, side-by-side for comparison:\n",
"```ocaml\n",
"module type Stack = sig module type Queue = sig\n",
" type 'a t type 'a t\n",
" val empty : 'a t val empty : 'a t\n",
" val is_empty : 'a t -> bool val is_empty : 'a t -> bool\n",
" val peek : 'a t -> 'a val front : 'a t -> 'a\n",
" val push : 'a -> 'a t -> 'a t val enq : 'a -> 'a t -> 'a t\n",
" val pop : 'a t -> 'a t val deq : 'a t -> 'a t\n",
"end end\n",
"```\n",
"Look at each line: though the operation may have a different name, its type\n",
"is the same. Obviously, the types alone don't tell us enough about the\n",
"operations. But the equations do! Here's how to read each equation:\n",
"\n",
"1. The empty queue is empty.\n",
"\n",
"2. Enqueueing makes a queue non-empty.\n",
"\n",
"3. Enqueueing `x` on an empty queue makes `x` the front element.\n",
" But if the queue isn't empty, enqueueing doesn't change the front element.\n",
"\n",
"4. Enqueueing then dequeueing on an empty queue leaves the queue empty.\n",
" But if the queue isn't empty, the enqueue and dequeue operations can\n",
" be swapped.\n",
"\n",
"For example,\n",
"\n",
"```text\n",
" front (deq (enq 1 (enq 2 empty)))\n",
"= { equation 4b }\n",
" front (enq 1 (deq (enq 2 empty)))\n",
"= { equation 4a }\n",
" front (enq 1 empty)\n",
"= { equation 3a }\n",
" 1\n",
"```\n",
"\n",
"And `front empty` doesn't equal any value according to the equations.\n",
"\n",
"Implementing a queue as a list results in an implementation that is easy to\n",
"verify just with evaluation."
]
},
{
"cell_type": "code",
"execution_count": 4,
"id": "5491f404",
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"module ListQueue : Queue\n"
]
},
"execution_count": 4,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"module ListQueue : Queue = struct\n",
" type 'a t = 'a list\n",
" let empty = []\n",
" let is_empty q = q = []\n",
" let front = List.hd\n",
" let enq x q = q @ [x]\n",
" let deq = List.tl\n",
"end"
]
},
{
"cell_type": "markdown",
"id": "efa5de71",
"metadata": {},
"source": [
"For example, 4a can be verified as follows:\n",
"\n",
"```text\n",
" deq (enq x empty)\n",
"= { evaluation of empty and enq}\n",
" deq ([] @ [x])\n",
"= { evaluation of @ }\n",
" deq [x]\n",
"= { evaluation of deq }\n",
" []\n",
"= { evaluation of empty }\n",
" empty\n",
"```\n",
"\n",
"And 4b, as follows:\n",
"```text\n",
" deq (enq x q)\n",
"= { evaluation of enq and deq }\n",
" List.tl (q @ [x])\n",
"= { lemma, below, and q <> [] }\n",
" (List.tl q) @ [x]\n",
"\n",
" enq x (deq q)\n",
"= { evaluation }\n",
" (List.tl q) @ [x]\n",
"```\n",
"\n",
"Here is the lemma:\n",
"\n",
"```text\n",
"Lemma: if xs <> [], then List.tl (xs @ ys) = (List.tl xs) @ ys.\n",
"Proof: if xs <> [], then xs = h :: t for some h and t.\n",
"\n",
" List.tl ((h :: t) @ ys)\n",
"= { evaluation of @ }\n",
" List.tl (h :: (t @ ys))\n",
"= { evaluation of tl }\n",
" t @ ys\n",
"\n",
" (List.tl (h :: t)) @ ys\n",
"= { evaluation of tl }\n",
" t @ ys\n",
"\n",
"QED\n",
"```\n",
"\n",
"Note how the precondition in 3b and 4b of `q` not being empty ensures that we\n",
"never have to deal with an exception being raised in the equational proofs.\n",
"\n",
"## Example: Batched Queues\n",
"\n",
"Recall that batched queues represent a queue with two lists:"
]
},
{
"cell_type": "code",
"execution_count": 5,
"id": "b3c9e53d",
"metadata": {
"tags": [
"hide-output"
]
},
"outputs": [
{
"data": {
"text/plain": [
"module BatchedQueue :\n",
" sig\n",
" type 'a t = 'a list * 'a list\n",
" val empty : 'a list * 'b list\n",
" val is_empty : 'a list * 'b -> bool\n",
" val enq : 'a -> 'a list * 'a list -> 'a list * 'a list\n",
" val front : 'a list * 'b -> 'a\n",
" val deq : 'a list * 'a list -> 'a list * 'a list\n",
" end\n"
]
},
"execution_count": 5,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"module BatchedQueue = struct\n",
" (* AF: [(o, i)] represents the queue [o @ (List.rev i)].\n",
" RI: if [o] is empty then [i] is empty. *)\n",
" type 'a t = 'a list * 'a list\n",
"\n",
" let empty = ([], [])\n",
"\n",
" let is_empty (o, i) = if o = [] then true else false\n",
"\n",
" let enq x (o, i) = if o = [] then ([x], []) else (o, x :: i)\n",
"\n",
" let front (o, _) = List.hd o\n",
"\n",
" let deq (o, i) =\n",
" match List.tl o with\n",
" | [] -> (List.rev i, [])\n",
" | t -> (t, i)\n",
"end"
]
},
{
"cell_type": "markdown",
"id": "92365da5",
"metadata": {},
"source": [
"This implementation is superficially different from the earlier implementation\n",
"we gave, in that it uses pairs instead of records, and it raises the built-in\n",
"exception `Failure` instead of a custom exception `Empty`.\n",
"\n",
"Is this implementation correct? We need only verify the equations to find out.\n",
"\n",
"First, a lemma:\n",
"\n",
"```text\n",
"Lemma: if is_empty q = true, then q = empty.\n",
"Proof: Since is_empty q = true, it must be that q = (f, b) and f = [].\n",
"By the RI, it must also be that b = []. Thus q = ([], []) = empty.\n",
"QED\n",
"```\n",
"\n",
"Verifying equation 1:\n",
"\n",
"```text\n",
" is_empty empty\n",
"= { eval empty }\n",
" is_empty ([], [])\n",
"= { eval is_empty }\n",
" [] = []\n",
"= { eval = }\n",
" true\n",
"```\n",
"\n",
"Verifying equation 2:\n",
"\n",
"```text\n",
" is_empty (enq x q) = false\n",
"= { eval enq }\n",
" is_empty (if f = [] then [x], [] else f, x :: b)\n",
"\n",
"case analysis: f = []\n",
"\n",
" is_empty (if f = [] then [x], [] else f, x :: b)\n",
"= { eval if, f = [] }\n",
" is_empty ([x], [])\n",
"= { eval is_empty }\n",
" [x] = []\n",
"= { eval = }\n",
" false\n",
"\n",
"case analysis: f = h :: t\n",
"\n",
" is_empty (if f = [] then [x], [] else f, x :: b)\n",
"= { eval if, f = h :: t }\n",
" is_empty (h :: t, x :: b)\n",
"= { eval is_empty }\n",
" h :: t = []\n",
"= { eval = }\n",
" false\n",
"```\n",
"\n",
"Verifying equation 3a:\n",
"\n",
"```text\n",
" front (enq x q) = x\n",
"= { emptiness lemma }\n",
" front (enq x ([], []))\n",
"= { eval enq }\n",
" front ([x], [])\n",
"= { eval front }\n",
" x\n",
"```\n",
"\n",
"Verifying equation 3b:\n",
"\n",
"```text\n",
" front (enq x q)\n",
"= { rewrite q as (h :: t, b), because q is not empty }\n",
" front (enq x (h :: t, b))\n",
"= { eval enq }\n",
" front (h :: t, x :: b)\n",
"= { eval front }\n",
" h\n",
"\n",
" front q\n",
"= { rewrite q as (h :: t, b), because q is not empty }\n",
" front (h :: t, b)\n",
"= { eval front }\n",
" h\n",
"```\n",
"\n",
"Verifying equation 4a:\n",
"\n",
"```text\n",
" deq (enq x q)\n",
"= { emptiness lemma }\n",
" deq (enq x ([], []))\n",
"= { eval enq }\n",
" deq ([x], [])\n",
"= { eval deq }\n",
" List.rev [], []\n",
"= { eval rev }\n",
" [], []\n",
"= { eval empty }\n",
" empty\n",
"```\n",
"\n",
"Verifying equation 4b:\n",
"\n",
"```text\n",
"Show: deq (enq x q) = enq x (deq q) assuming is_empty q = false.\n",
"Proof: Since is_empty q = false, q must be (h :: t, b).\n",
"\n",
"Case analysis: t = [], b = []\n",
"\n",
" deq (enq x q)\n",
"= { rewriting q as ([h], []) }\n",
" deq (enq x ([h], []))\n",
"= { eval enq }\n",
" deq ([h], [x])\n",
"= { eval deq }\n",
" List.rev [x], []\n",
"= { eval rev }\n",
" [x], []\n",
"\n",
" enq x (deq q)\n",
"= { rewriting q as ([h], []) }\n",
" enq x (deq ([h], []))\n",
"= { eval deq }\n",
" enq x (List.rev [], [])\n",
"= { eval rev }\n",
" enq x ([], [])\n",
"= { eval enq }\n",
" [x], []\n",
"\n",
"Case analysis: t = [], b = h' :: t'\n",
"\n",
" deq (enq x q)\n",
"= { rewriting q as ([h], h' :: t') }\n",
" deq (enq x ([h], h' :: t'))\n",
"= { eval enq }\n",
" deq ([h], x :: h' :: t')\n",
"= { eval deq }\n",
" (List.rev (x :: h' :: t'), [])\n",
"\n",
" enq x (deq q)\n",
"= { rewriting q as ([h], h' :: t') }\n",
" enq x (deq ([h], h' :: t'))\n",
"= { eval deq }\n",
" enq x (List.rev (h' :: t'), [])\n",
"= { eval enq }\n",
" (List.rev (h' :: t'), [x])\n",
"\n",
"STUCK\n",
"```\n",
"\n",
"Wait, we just got stuck! `(List.rev (x :: h' :: t'), [])` and\n",
"`(List.rev (h' :: t'), [x])` are different. But, abstractly, they do\n",
"represent the same queue: `(List.rev t') @ [h'; x]`.\n",
"\n",
"To solve this problem, we will adopt the following equation for representation\n",
"types:\n",
"\n",
"```text\n",
"e = e' if AF(e) = AF(e')\n",
"```\n",
"\n",
"That equation allows us to conclude that the two differing expressions are\n",
"equal:\n",
"\n",
"```text\n",
" AF((List.rev (h' :: t'), [x]))\n",
"= { apply AF } \n",
" List.rev (h' :: t') @ List.rev [x]\n",
"= { rev distributes over @, an exercise in the previous lecture }\n",
" List.rev ([x] @ (h' :: t'))\n",
"= { eval @ }\n",
" List.rev (x :: h' :: t')\n",
" \n",
" AF((List.rev (x :: h' :: t'), []))\n",
"= { apply AF }\n",
" List.rev (x :: h' :: t') @ List.rev []\n",
"= { eval rev }\n",
" List.rev (x :: h' :: t') @ []\n",
"= { eval @ }\n",
" List.rev (x :: h' :: t')\n",
"```\n",
"\n",
"Now we are unstuck:\n",
"\n",
"```text\n",
" (List.rev (h' :: t'), [x])\n",
"= { AF equation }\n",
" (List.rev (x :: h' :: t'), [])\n",
"```\n",
"\n",
"There is one more case analysis remaining to finish the proof:\n",
" \n",
"```text\n",
"Case analysis: t = h' :: t'\n",
"\n",
" deq (enq x q)\n",
"= { rewriting q as (h :: h' :: t', b) }\n",
" deq (enq x (h :: h' :: t', b))\n",
"= { eval enq }\n",
" deq (h :: h' :: t, x :: b)\n",
"= { eval deq }\n",
" h' :: t, x :: b\n",
"\n",
" enq x (deq q)\n",
"= { rewriting q as (h :: h' :: t', b) }\n",
" enq x (deq (h :: h' :: t', b))\n",
"= { eval deq }\n",
" enq x (h' :: t', b)\n",
"= { eval enq }\n",
" h' :: t', x :: b\n",
"\n",
"QED\n",
"```\n",
"\n",
"That concludes our verification of the batched queue. Note that we had to add\n",
"the extra equation involving the abstraction function to get the proofs to go\n",
"through:\n",
"\n",
"```text\n",
"e = e' if AF(e) = AF(e')\n",
"```\n",
"\n",
"and that we made use of the RI during the proof. The AF and RI really are\n",
"important!\n",
"\n",
"## Designing Algebraic Specifications\n",
"\n",
"{{ video_embed | replace(\"%%VID%%\", \"8uJmKmsiF2I\")}}\n",
"\n",
"For both stacks and queues we provided some equations as the specification.\n",
"Designing those equations is, in part, a matter of thinking hard about the data\n",
"structure. But there's more to it than that.\n",
"\n",
"Every value of the data structure is constructed with some operations. For a\n",
"stack, those operations are `empty` and `push`. There might be some `pop`\n",
"operations involved, but those can be eliminated. For example, `pop (push 1\n",
"(push 2 empty))` is really the same stack as `push 2 empty`. The latter is the\n",
"*canonical form* of that stack: there are many other ways to construct it, but\n",
"that is the simplest. Indeed, every possible stack value can be constructed just\n",
"with `empty` and `push`. Similarly, every possible queue value can be\n",
"constructed just with `empty` and `enq`: if there are `deq` operations involved,\n",
"those can be eliminated.\n",
"\n",
"Let's categorize the operations of a data structure as follows:\n",
"\n",
"- **Generators** are those operations involved in creating a canonical form.\n",
" They return a value of the data structure type. For example, `empty`, `push`,\n",
" `enq`.\n",
"\n",
"- **Manipulators** are operations that create a value of the data structure\n",
" type, but are not needed to create canonical forms. For example, `pop`, `deq`.\n",
"\n",
"- **Queries** do not return a value of the data structure type. For example,\n",
" `is_empty`, `peek`, `front`.\n",
"\n",
"Given such a categorization, we can design the equational specification of a\n",
"data structure by applying non-generators to generators. For example: What does\n",
"`is_empty` return on `empty`? on `push`? What does `front` return on `enq`? What\n",
"does `deq` return on `enq`? etc.\n",
"\n",
"So if there are `n` generators and `m` non-generators of a data structure, we\n",
"would begin by trying to create `n*m` equations, one for each pair of a\n",
"generator and non-generator. Each equation would show how to simplify an\n",
"expression. In some cases we might need a couple equations, depending on the\n",
"result of some comparison. For example, in the queue specification, we have the\n",
"following equations:\n",
"\n",
"1. `is_empty empty = true`: this is a non-generator `is_empty` applied to a\n",
" generator `empty`. It reduces just to a Boolean value, which doesn't involve\n",
" the data structure type (queues) at all.\n",
"\n",
"2. `is_empty (enq x q) = false`: a non-generator `is_empty` applied to a\n",
" generator `enq`. Again it reduces simply to a Boolean value.\n",
"\n",
"3. There are two subcases.\n",
"\n",
" - `front (enq x q) = x`, if `is_empty q = true`. A non-generator `front`\n",
" applied to a generator `enq`. It reduces to `x`, which is a smaller\n",
" expression than the original `front (enq x q)`.\n",
"\n",
" - `front (enq x q) = front q`, `if is_empty q = false`. This similarly\n",
" reduces to a smaller expression.\n",
"\n",
"4. Again, there are two subcases.\n",
"\n",
" - `deq (enq x q) = empty`, if `is_empty q = true`. This simplifies the\n",
" original expression by reducing it to `empty`.\n",
"\n",
" - `deq (enq x q) = enq x (deq q)`, if `is_empty q = false`. This simplifies\n",
" the original expression by reducing it to an generator applied to a smaller\n",
" argument, `deq q` instead of `deq (enq x q)`.\n",
"\n",
"We don't usually design equations involving pairs of non-generators. Sometimes\n",
"pairs of generators are needed, though, as we will see in the next example.\n",
"\n",
"**Example: Sets.** Here is a small interface for sets:"
]
},
{
"cell_type": "code",
"execution_count": 6,
"id": "814a72c7",
"metadata": {
"tags": [
"hide-output"
]
},
"outputs": [
{
"data": {
"text/plain": [
"module type Set =\n",
" sig\n",
" type 'a t\n",
" val empty : 'a t\n",
" val is_empty : 'a t -> bool\n",
" val add : 'a -> 'a t -> 'a t\n",
" val mem : 'a -> 'a t -> bool\n",
" val remove : 'a -> 'a t -> 'a t\n",
" end\n"
]
},
"execution_count": 6,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"module type Set = sig\n",
" type 'a t\n",
" val empty : 'a t\n",
" val is_empty : 'a t -> bool\n",
" val add : 'a -> 'a t -> 'a t\n",
" val mem : 'a -> 'a t -> bool\n",
" val remove : 'a -> 'a t -> 'a t\n",
"end"
]
},
{
"cell_type": "markdown",
"id": "43c9f51a",
"metadata": {},
"source": [
"The generators are `empty` and `add`. The only manipulator is `remove`. Finally,\n",
"`is_empty` and `mem` are queries. So we should expect at least 2 * 3 = 6\n",
"equations, one for each pair of generator and non-generator. Here is an\n",
"equational specification:\n",
"\n",
"```text\n",
"1. is_empty empty = true\n",
"2. is_empty (add x s) = false\n",
"3. mem x empty = false\n",
"4a. mem y (add x s) = true if x = y\n",
"4b. mem y (add x s) = mem y s if x <> y\n",
"5. remove x empty = empty\n",
"6a. remove y (add x s) = remove y s if x = y\n",
"6b. remove y (add x s) = add x (remove y s) if x <> y\n",
"```\n",
"\n",
"Consider, though, these two sets:\n",
"\n",
"- `add 0 (add 1 empty)`\n",
"- `add 1 (add 0 empty)`\n",
"\n",
"They both intuitively represent the set {0,1}. Yet, we cannot prove that those\n",
"two sets are equal using the above specification. We are missing an equation\n",
"involving two generators:\n",
"\n",
"```\n",
"7. add x (add y s) = add y (add x s)\n",
"```"
]
}
],
"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,
74,
85,
140,
150,
170,
180,
235,
244,
299,
319,
618,
628
]
},
"nbformat": 4,
"nbformat_minor": 5
}