diff --git a/mathematical/TransitiveClosure.ipynb b/mathematical/TransitiveClosure.ipynb
new file mode 100644
index 0000000000000000000000000000000000000000..b22706d8b6f5bb66300dc9669fb30167ebbc2688
--- /dev/null
+++ b/mathematical/TransitiveClosure.ipynb
@@ -0,0 +1,520 @@
+{
+ "cells": [
+ {
+ "cell_type": "code",
+ "execution_count": null,
+ "id": "d4a6c748",
+ "metadata": {
+ "vscode": {
+ "languageId": "plaintext"
+ }
+ },
+ "outputs": [],
+ "source": [
+ "# Modeling transitive closure in B/Event-B\n",
+ "\n",
+ "Also discussions about first-order and higher-order aspects of B."
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 4,
+ "id": "964d8a32-2743-4f52-ab27-78dcfe798e11",
+ "metadata": {
+ "vscode": {
+ "languageId": "classicalb"
+ }
+ },
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Loaded machine: StateGraph"
+ ]
+ },
+ "execution_count": 4,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "::load\n",
+ "MACHINE StateGraph\n",
+ "SETS States = {s1,s2,s3}\n",
+ "CONSTANTS next\n",
+ "PROPERTIES\n",
+ " next = {s1|->s2, s2|->s1, s3|->s3}\n",
+ "END"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 6,
+ "id": "0b8c470d",
+ "metadata": {
+ "vscode": {
+ "languageId": "plaintext"
+ }
+ },
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Machine constants were not set up yet. Automatically set up constants using arbitrary transition: SETUP_CONSTANTS()\n",
+ "Executed operation: INITIALISATION()"
+ ]
+ },
+ "execution_count": 6,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":init"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 7,
+ "id": "949c9b64",
+ "metadata": {
+ "vscode": {
+ "languageId": "plaintext"
+ }
+ },
+ "outputs": [
+ {
+ "data": {
+ "image/svg+xml": "<?xml version=\"1.0\" encoding=\"UTF-8\" standalone=\"no\"?>\n<!DOCTYPE svg PUBLIC \"-//W3C//DTD SVG 1.1//EN\"\n \"http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd\">\n<!-- Generated by graphviz version 6.0.1 (20220911.1526)\n -->\n<!-- Title: state Pages: 1 -->\n<svg width=\"208pt\" height=\"184pt\"\n viewBox=\"0.00 0.00 208.00 184.00\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n<g id=\"graph0\" class=\"graph\" transform=\"scale(1 1) rotate(0) translate(4 180)\">\n<title>state</title>\n<polygon fill=\"white\" stroke=\"none\" points=\"-4,4 -4,-180 204,-180 204,4 -4,4\"/>\n<g id=\"clust1\" class=\"cluster\">\n<title>cluster_States</title>\n<polygon fill=\"lightgrey\" stroke=\"lightgrey\" points=\"8,-8 8,-168 192,-168 192,-8 8,-8\"/>\n<text text-anchor=\"middle\" x=\"100\" y=\"-154.4\" font-family=\"Times,serif\" font-size=\"12.00\">States</text>\n</g>\n<!-- s3 -->\n<g id=\"node1\" class=\"node\">\n<title>s3</title>\n<polygon fill=\"#efdf84\" stroke=\"#efdf84\" points=\"142,-139 88,-139 88,-103 142,-103 142,-139\"/>\n<text text-anchor=\"middle\" x=\"115\" y=\"-117.3\" font-family=\"Times,serif\" font-size=\"14.00\">s3</text>\n</g>\n<!-- s3->s3 -->\n<g id=\"edge1\" class=\"edge\">\n<title>s3->s3</title>\n<path fill=\"none\" stroke=\"firebrick\" d=\"M142.24,-129.15C152.02,-129.32 160,-126.61 160,-121 160,-117.58 157.04,-115.24 152.51,-113.97\"/>\n<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"152.56,-110.45 142.24,-112.85 151.8,-117.41 152.56,-110.45\"/>\n<text text-anchor=\"middle\" x=\"172\" y=\"-117.3\" font-family=\"Times,serif\" font-size=\"14.00\">next</text>\n</g>\n<!-- s2 -->\n<g id=\"node2\" class=\"node\">\n<title>s2</title>\n<polygon fill=\"#efdf84\" stroke=\"#efdf84\" points=\"70,-139 16,-139 16,-103 70,-103 70,-139\"/>\n<text text-anchor=\"middle\" x=\"43\" y=\"-117.3\" font-family=\"Times,serif\" font-size=\"14.00\">s2</text>\n</g>\n<!-- s1 -->\n<g id=\"node3\" class=\"node\">\n<title>s1</title>\n<polygon fill=\"#efdf84\" stroke=\"#efdf84\" points=\"91,-52 37,-52 37,-16 91,-16 91,-52\"/>\n<text text-anchor=\"middle\" x=\"64\" y=\"-30.3\" font-family=\"Times,serif\" font-size=\"14.00\">s1</text>\n</g>\n<!-- s2->s1 -->\n<g id=\"edge2\" class=\"edge\">\n<title>s2->s1</title>\n<path fill=\"none\" stroke=\"firebrick\" d=\"M38.45,-102.96C36.6,-93.11 35.6,-80.61 39,-70 40,-66.87 41.4,-63.78 43.02,-60.82\"/>\n<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"46,-62.66 48.42,-52.35 40.09,-58.9 46,-62.66\"/>\n<text text-anchor=\"middle\" x=\"51\" y=\"-73.8\" font-family=\"Times,serif\" font-size=\"14.00\">next</text>\n</g>\n<!-- s1->s2 -->\n<g id=\"edge3\" class=\"edge\">\n<title>s1->s2</title>\n<path fill=\"none\" stroke=\"firebrick\" d=\"M65.74,-52.43C66.2,-62.18 65.91,-74.46 63,-85 62.17,-88.01 61.02,-91.03 59.69,-93.96\"/>\n<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"56.53,-92.47 55,-102.95 62.73,-95.71 56.53,-92.47\"/>\n<text text-anchor=\"middle\" x=\"77\" y=\"-73.8\" font-family=\"Times,serif\" font-size=\"14.00\">next</text>\n</g>\n</g>\n</svg>\n",
+ "text/plain": [
+ "<Dot visualization: expr_as_graph [next]>"
+ ]
+ },
+ "execution_count": 7,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":dot expr_as_graph next"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "id": "ce973fde",
+ "metadata": {},
+ "source": [
+ "How do we obtain the transitive closure of this relation? In classical B there is the operator ```closure1``` for this:"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 8,
+ "id": "31e1b59d",
+ "metadata": {
+ "vscode": {
+ "languageId": "plaintext"
+ }
+ },
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$\\{(\\mathit{s1}\\mapsto\\mathit{s1}),(\\mathit{s1}\\mapsto\\mathit{s2}),(\\mathit{s2}\\mapsto\\mathit{s1}),(\\mathit{s2}\\mapsto\\mathit{s2}),(\\mathit{s3}\\mapsto\\mathit{s3})\\}$"
+ ],
+ "text/plain": [
+ "{(s1↦s1),(s1↦s2),(s2↦s1),(s2↦s2),(s3↦s3)}"
+ ]
+ },
+ "execution_count": 8,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "closure1(next)"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 12,
+ "id": "006bae98",
+ "metadata": {
+ "vscode": {
+ "languageId": "plaintext"
+ }
+ },
+ "outputs": [
+ {
+ "data": {
+ "image/svg+xml": "<?xml version=\"1.0\" encoding=\"UTF-8\" standalone=\"no\"?>\n<!DOCTYPE svg PUBLIC \"-//W3C//DTD SVG 1.1//EN\"\n \"http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd\">\n<!-- Generated by graphviz version 6.0.1 (20220911.1526)\n -->\n<!-- Title: state Pages: 1 -->\n<svg width=\"246pt\" height=\"184pt\"\n viewBox=\"0.00 0.00 246.00 184.00\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n<g id=\"graph0\" class=\"graph\" transform=\"scale(1 1) rotate(0) translate(4 180)\">\n<title>state</title>\n<polygon fill=\"white\" stroke=\"none\" points=\"-4,4 -4,-180 242,-180 242,4 -4,4\"/>\n<g id=\"clust1\" class=\"cluster\">\n<title>cluster_States</title>\n<polygon fill=\"lightgrey\" stroke=\"lightgrey\" points=\"8,-8 8,-168 230,-168 230,-8 8,-8\"/>\n<text text-anchor=\"middle\" x=\"119\" y=\"-154.4\" font-family=\"Times,serif\" font-size=\"12.00\">States</text>\n</g>\n<!-- s3 -->\n<g id=\"node1\" class=\"node\">\n<title>s3</title>\n<polygon fill=\"#efdf84\" stroke=\"#efdf84\" points=\"182,-139 128,-139 128,-103 182,-103 182,-139\"/>\n<text text-anchor=\"middle\" x=\"155\" y=\"-117.3\" font-family=\"Times,serif\" font-size=\"14.00\">s3</text>\n</g>\n<!-- s3->s3 -->\n<g id=\"edge1\" class=\"edge\">\n<title>s3->s3</title>\n<path fill=\"none\" stroke=\"firebrick\" d=\"M182.24,-129.15C192.02,-129.32 200,-126.61 200,-121 200,-117.58 197.04,-115.24 192.51,-113.97\"/>\n<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"192.56,-110.45 182.24,-112.85 191.8,-117.41 192.56,-110.45\"/>\n<text text-anchor=\"middle\" x=\"211\" y=\"-117.3\" font-family=\"Times,serif\" font-size=\"14.00\">cls1</text>\n</g>\n<!-- s2 -->\n<g id=\"node2\" class=\"node\">\n<title>s2</title>\n<polygon fill=\"#efdf84\" stroke=\"#efdf84\" points=\"70,-139 16,-139 16,-103 70,-103 70,-139\"/>\n<text text-anchor=\"middle\" x=\"43\" y=\"-117.3\" font-family=\"Times,serif\" font-size=\"14.00\">s2</text>\n</g>\n<!-- s2->s2 -->\n<g id=\"edge2\" class=\"edge\">\n<title>s2->s2</title>\n<path fill=\"none\" stroke=\"firebrick\" d=\"M70.24,-129.15C80.02,-129.32 88,-126.61 88,-121 88,-117.58 85.04,-115.24 80.51,-113.97\"/>\n<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"80.56,-110.45 70.24,-112.85 79.8,-117.41 80.56,-110.45\"/>\n<text text-anchor=\"middle\" x=\"99\" y=\"-117.3\" font-family=\"Times,serif\" font-size=\"14.00\">cls1</text>\n</g>\n<!-- s1 -->\n<g id=\"node3\" class=\"node\">\n<title>s1</title>\n<polygon fill=\"#efdf84\" stroke=\"#efdf84\" points=\"90,-52 36,-52 36,-16 90,-16 90,-52\"/>\n<text text-anchor=\"middle\" x=\"63\" y=\"-30.3\" font-family=\"Times,serif\" font-size=\"14.00\">s1</text>\n</g>\n<!-- s2->s1 -->\n<g id=\"edge3\" class=\"edge\">\n<title>s2->s1</title>\n<path fill=\"none\" stroke=\"firebrick\" d=\"M38.53,-102.99C36.7,-93.15 35.7,-80.65 39,-70 39.98,-66.83 41.36,-63.7 42.96,-60.68\"/>\n<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"46,-62.42 48.29,-52.07 40.05,-58.74 46,-62.42\"/>\n<text text-anchor=\"middle\" x=\"50\" y=\"-73.8\" font-family=\"Times,serif\" font-size=\"14.00\">cls1</text>\n</g>\n<!-- s1->s2 -->\n<g id=\"edge4\" class=\"edge\">\n<title>s1->s2</title>\n<path fill=\"none\" stroke=\"firebrick\" d=\"M64.13,-52.4C64.32,-62.14 63.79,-74.41 61,-85 60.25,-87.85 59.24,-90.73 58.08,-93.56\"/>\n<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"54.83,-92.26 53.73,-102.8 61.16,-95.24 54.83,-92.26\"/>\n<text text-anchor=\"middle\" x=\"74\" y=\"-73.8\" font-family=\"Times,serif\" font-size=\"14.00\">cls1</text>\n</g>\n<!-- s1->s1 -->\n<g id=\"edge5\" class=\"edge\">\n<title>s1->s1</title>\n<path fill=\"none\" stroke=\"firebrick\" d=\"M90.24,-42.15C100.02,-42.32 108,-39.61 108,-34 108,-30.58 105.04,-28.24 100.51,-26.97\"/>\n<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"100.56,-23.45 90.24,-25.85 99.8,-30.41 100.56,-23.45\"/>\n<text text-anchor=\"middle\" x=\"119\" y=\"-30.3\" font-family=\"Times,serif\" font-size=\"14.00\">cls1</text>\n</g>\n</g>\n</svg>\n",
+ "text/plain": [
+ "<Dot visualization: expr_as_graph [(\"cls1\",closure1(next))]>"
+ ]
+ },
+ "execution_count": 12,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":dot expr_as_graph (\"cls1\",closure1(next))"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "id": "6dd0ca64",
+ "metadata": {},
+ "source": [
+ "In Event-B this operator is not available in the core language; one can import a theory for it though.\n",
+ "Let us, however, try and axiomatise this ourselves:"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 16,
+ "id": "44c560e2",
+ "metadata": {
+ "vscode": {
+ "languageId": "plaintext"
+ }
+ },
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$\\mathit{TRUE}$\n",
+ "\n",
+ "**Solution:**\n",
+ "* $\\mathit{cls1} = \\{(\\mathit{s2}\\mapsto\\mathit{s1}),(\\mathit{s1}\\mapsto\\mathit{s2}),(\\mathit{s3}\\mapsto\\mathit{s3}),(\\mathit{s1}\\mapsto\\mathit{s1}),(\\mathit{s1}\\mapsto\\mathit{s3}),(\\mathit{s2}\\mapsto\\mathit{s2})\\}$"
+ ],
+ "text/plain": [
+ "TRUE\n",
+ "\n",
+ "Solution:\n",
+ "\tcls1 = {(s2↦s1),(s1↦s2),(s3↦s3),(s1↦s1),(s1↦s3),(s2↦s2)}"
+ ]
+ },
+ "execution_count": 16,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "next <: cls1 & // the next relation is included in the transitive closure\n",
+ "!s.(s:States => next[cls1[{s}]] <: cls1[{s}] ) // all successors are also included"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "id": "1259680a",
+ "metadata": {},
+ "source": [
+ "As you can see this solution is maybe not what you expected, it contains an edge between s1 and s3.\n",
+ "But it satisfies our conditions."
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 19,
+ "id": "90d84935",
+ "metadata": {
+ "vscode": {
+ "languageId": "plaintext"
+ }
+ },
+ "outputs": [
+ {
+ "data": {
+ "image/svg+xml": "<?xml version=\"1.0\" encoding=\"UTF-8\" standalone=\"no\"?>\n<!DOCTYPE svg PUBLIC \"-//W3C//DTD SVG 1.1//EN\"\n \"http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd\">\n<!-- Generated by graphviz version 6.0.1 (20220911.1526)\n -->\n<!-- Title: state Pages: 1 -->\n<svg width=\"246pt\" height=\"184pt\"\n viewBox=\"0.00 0.00 246.00 184.00\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n<g id=\"graph0\" class=\"graph\" transform=\"scale(1 1) rotate(0) translate(4 180)\">\n<title>state</title>\n<polygon fill=\"white\" stroke=\"none\" points=\"-4,4 -4,-180 242,-180 242,4 -4,4\"/>\n<g id=\"clust1\" class=\"cluster\">\n<title>cluster_States</title>\n<polygon fill=\"lightgrey\" stroke=\"lightgrey\" points=\"8,-8 8,-168 230,-168 230,-8 8,-8\"/>\n<text text-anchor=\"middle\" x=\"119\" y=\"-154.4\" font-family=\"Times,serif\" font-size=\"12.00\">States</text>\n</g>\n<!-- s3 -->\n<g id=\"node1\" class=\"node\">\n<title>s3</title>\n<polygon fill=\"#efdf84\" stroke=\"#efdf84\" points=\"182,-52 128,-52 128,-16 182,-16 182,-52\"/>\n<text text-anchor=\"middle\" x=\"155\" y=\"-30.3\" font-family=\"Times,serif\" font-size=\"14.00\">s3</text>\n</g>\n<!-- s3->s3 -->\n<g id=\"edge1\" class=\"edge\">\n<title>s3->s3</title>\n<path fill=\"none\" stroke=\"firebrick\" d=\"M182.24,-42.15C192.02,-42.32 200,-39.61 200,-34 200,-30.58 197.04,-28.24 192.51,-26.97\"/>\n<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"192.56,-23.45 182.24,-25.85 191.8,-30.41 192.56,-23.45\"/>\n<text text-anchor=\"middle\" x=\"211\" y=\"-30.3\" font-family=\"Times,serif\" font-size=\"14.00\">cls1</text>\n</g>\n<!-- s2 -->\n<g id=\"node2\" class=\"node\">\n<title>s2</title>\n<polygon fill=\"#efdf84\" stroke=\"#efdf84\" points=\"70,-52 16,-52 16,-16 70,-16 70,-52\"/>\n<text text-anchor=\"middle\" x=\"43\" y=\"-30.3\" font-family=\"Times,serif\" font-size=\"14.00\">s2</text>\n</g>\n<!-- s2->s2 -->\n<g id=\"edge2\" class=\"edge\">\n<title>s2->s2</title>\n<path fill=\"none\" stroke=\"firebrick\" d=\"M70.24,-42.15C80.02,-42.32 88,-39.61 88,-34 88,-30.58 85.04,-28.24 80.51,-26.97\"/>\n<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"80.56,-23.45 70.24,-25.85 79.8,-30.41 80.56,-23.45\"/>\n<text text-anchor=\"middle\" x=\"99\" y=\"-30.3\" font-family=\"Times,serif\" font-size=\"14.00\">cls1</text>\n</g>\n<!-- s1 -->\n<g id=\"node3\" class=\"node\">\n<title>s1</title>\n<polygon fill=\"#efdf84\" stroke=\"#efdf84\" points=\"115,-139 61,-139 61,-103 115,-103 115,-139\"/>\n<text text-anchor=\"middle\" x=\"88\" y=\"-117.3\" font-family=\"Times,serif\" font-size=\"14.00\">s1</text>\n</g>\n<!-- s2->s1 -->\n<g id=\"edge3\" class=\"edge\">\n<title>s2->s1</title>\n<path fill=\"none\" stroke=\"firebrick\" d=\"M55.05,-52.09C58.77,-57.68 62.74,-64 66,-70 70.08,-77.5 74.01,-85.9 77.39,-93.65\"/>\n<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"74.22,-95.16 81.35,-103 80.67,-92.43 74.22,-95.16\"/>\n<text text-anchor=\"middle\" x=\"84\" y=\"-73.8\" font-family=\"Times,serif\" font-size=\"14.00\">cls1</text>\n</g>\n<!-- s1->s3 -->\n<g id=\"edge4\" class=\"edge\">\n<title>s1->s3</title>\n<path fill=\"none\" stroke=\"firebrick\" d=\"M101.56,-102.8C111.18,-90.59 124.27,-73.99 135.08,-60.28\"/>\n<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"138.02,-62.2 141.46,-52.18 132.52,-57.86 138.02,-62.2\"/>\n<text text-anchor=\"middle\" x=\"136\" y=\"-73.8\" font-family=\"Times,serif\" font-size=\"14.00\">cls1</text>\n</g>\n<!-- s1->s2 -->\n<g id=\"edge5\" class=\"edge\">\n<title>s1->s2</title>\n<path fill=\"none\" stroke=\"firebrick\" d=\"M60.95,-106.76C52.69,-101.25 44.58,-94.01 40,-85 36.48,-78.07 35.78,-69.89 36.36,-62.17\"/>\n<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"39.85,-62.49 37.81,-52.09 32.93,-61.49 39.85,-62.49\"/>\n<text text-anchor=\"middle\" x=\"51\" y=\"-73.8\" font-family=\"Times,serif\" font-size=\"14.00\">cls1</text>\n</g>\n<!-- s1->s1 -->\n<g id=\"edge6\" class=\"edge\">\n<title>s1->s1</title>\n<path fill=\"none\" stroke=\"firebrick\" d=\"M115.24,-129.15C125.02,-129.32 133,-126.61 133,-121 133,-117.58 130.04,-115.24 125.51,-113.97\"/>\n<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"125.56,-110.45 115.24,-112.85 124.8,-117.41 125.56,-110.45\"/>\n<text text-anchor=\"middle\" x=\"144\" y=\"-117.3\" font-family=\"Times,serif\" font-size=\"14.00\">cls1</text>\n</g>\n</g>\n</svg>\n",
+ "text/plain": [
+ "<Dot visualization: expr_as_graph [(\"cls1\", {(s2↦s1),(s1↦s2),(s3↦s3),(s1↦s1),(s1↦s3),(s2↦s2)})]>"
+ ]
+ },
+ "execution_count": 19,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":dot expr_as_graph (\"cls1\", {(s2↦s1),(s1↦s2),(s3↦s3),(s1↦s1),(s1↦s3),(s2↦s2)})"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "id": "77992532",
+ "metadata": {},
+ "source": [
+ "As you can see there are eight solutions to this \"axiomatisation\" of transitive closure for this graph:"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 17,
+ "id": "28d0f48e",
+ "metadata": {
+ "vscode": {
+ "languageId": "plaintext"
+ }
+ },
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "|cls1|\n",
+ "|---|\n",
+ "|{(s1↦s1),(s1↦s2),(s1↦s3),(s2↦s1),(s2↦s2),(s3↦s3)}|\n",
+ "|{(s1↦s1),(s1↦s2),(s2↦s1),(s2↦s2),(s3↦s3)}|\n",
+ "|{(s1↦s1),(s1↦s2),(s2↦s1),(s2↦s2),(s2↦s3),(s3↦s3)}|\n",
+ "|{(s1↦s1),(s1↦s2),(s1↦s3),(s2↦s1),(s2↦s2),(s2↦s3),(s3↦s3)}|\n",
+ "|{(s1↦s1),(s1↦s2),(s1↦s3),(s2↦s1),(s2↦s2),(s3↦s1),(s3↦s2),(s3↦s3)}|\n",
+ "|{(s1↦s1),(s1↦s2),(s2↦s1),(s2↦s2),(s3↦s1),(s3↦s2),(s3↦s3)}|\n",
+ "|{(s1↦s1),(s1↦s2),(s1↦s3),(s2↦s1),(s2↦s2),(s2↦s3),(s3↦s1),(s3↦s2),(s3↦s3)}|\n",
+ "|{(s1↦s1),(s1↦s2),(s2↦s1),(s2↦s2),(s2↦s3),(s3↦s1),(s3↦s2),(s3↦s3)}|\n"
+ ],
+ "text/plain": [
+ "cls1\n",
+ "{(s1|->s1),(s1|->s2),(s1|->s3),(s2|->s1),(s2|->s2),(s3|->s3)}\n",
+ "{(s1|->s1),(s1|->s2),(s2|->s1),(s2|->s2),(s3|->s3)}\n",
+ "{(s1|->s1),(s1|->s2),(s2|->s1),(s2|->s2),(s2|->s3),(s3|->s3)}\n",
+ "{(s1|->s1),(s1|->s2),(s1|->s3),(s2|->s1),(s2|->s2),(s2|->s3),(s3|->s3)}\n",
+ "{(s1|->s1),(s1|->s2),(s1|->s3),(s2|->s1),(s2|->s2),(s3|->s1),(s3|->s2),(s3|->s3)}\n",
+ "{(s1|->s1),(s1|->s2),(s2|->s1),(s2|->s2),(s3|->s1),(s3|->s2),(s3|->s3)}\n",
+ "{(s1|->s1),(s1|->s2),(s1|->s3),(s2|->s1),(s2|->s2),(s2|->s3),(s3|->s1),(s3|->s2),(s3|->s3)}\n",
+ "{(s1|->s1),(s1|->s2),(s2|->s1),(s2|->s2),(s2|->s3),(s3|->s1),(s3|->s2),(s3|->s3)}\n"
+ ]
+ },
+ "execution_count": 17,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":table {cls1 | next <: cls1 & !s.(s:States => next[cls1[{s}]] <: cls1[{s}] )}"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "id": "c6f8db6c",
+ "metadata": {},
+ "source": [
+ "Can we encode transitive closure in B?\n",
+ "\n",
+ "What we want is the smallest relation satisfying our axioms. In higher-oder logic we can quantify over predicates, and\n",
+ "for example ask that we want the smallest solution.\n",
+ "\n",
+ "Transitive closure can actually not be axiomatised in first-order logic.\n",
+ "As B is based on first-order logic, can we do this without resorting to the built-in operator ```closure1```?\n",
+ "The answer is yes, becase B has higher-order values and we can arbitrarily quantify over sets and relation values."
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 24,
+ "id": "4d178ab1",
+ "metadata": {
+ "vscode": {
+ "languageId": "plaintext"
+ }
+ },
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "|cls1|\n",
+ "|---|\n",
+ "|{(s1↦s1),(s1↦s2),(s2↦s1),(s2↦s2),(s3↦s3)}|\n"
+ ],
+ "text/plain": [
+ "cls1\n",
+ "{(s1|->s1),(s1|->s2),(s2|->s1),(s2|->s2),(s3|->s3)}\n"
+ ]
+ },
+ "execution_count": 24,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":table {cls1 | \n",
+ " next <: cls1 & !s.(s:States => next[cls1[{s}]] <: cls1[{s}]) // we satisfy our axioms\n",
+ " &\n",
+ " !other.(other <<: cls1 & next <: other => \n",
+ " not ( !s.(s:States => next[other[{s}]] <: other[{s}]) )\n",
+ " )\n",
+ " }"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 25,
+ "id": "c7c935b3",
+ "metadata": {
+ "vscode": {
+ "languageId": "plaintext"
+ }
+ },
+ "outputs": [
+ {
+ "data": {
+ "image/svg+xml": "<?xml version=\"1.0\" encoding=\"UTF-8\" standalone=\"no\"?>\n<!DOCTYPE svg PUBLIC \"-//W3C//DTD SVG 1.1//EN\"\n \"http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd\">\n<!-- Generated by graphviz version 6.0.1 (20220911.1526)\n -->\n<!-- Title: state Pages: 1 -->\n<svg width=\"246pt\" height=\"184pt\"\n viewBox=\"0.00 0.00 246.00 184.00\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n<g id=\"graph0\" class=\"graph\" transform=\"scale(1 1) rotate(0) translate(4 180)\">\n<title>state</title>\n<polygon fill=\"white\" stroke=\"none\" points=\"-4,4 -4,-180 242,-180 242,4 -4,4\"/>\n<g id=\"clust1\" class=\"cluster\">\n<title>cluster_States</title>\n<polygon fill=\"lightgrey\" stroke=\"lightgrey\" points=\"8,-8 8,-168 230,-168 230,-8 8,-8\"/>\n<text text-anchor=\"middle\" x=\"119\" y=\"-154.4\" font-family=\"Times,serif\" font-size=\"12.00\">States</text>\n</g>\n<!-- s3 -->\n<g id=\"node1\" class=\"node\">\n<title>s3</title>\n<polygon fill=\"#efdf84\" stroke=\"#efdf84\" points=\"182,-139 128,-139 128,-103 182,-103 182,-139\"/>\n<text text-anchor=\"middle\" x=\"155\" y=\"-117.3\" font-family=\"Times,serif\" font-size=\"14.00\">s3</text>\n</g>\n<!-- s3->s3 -->\n<g id=\"edge1\" class=\"edge\">\n<title>s3->s3</title>\n<path fill=\"none\" stroke=\"firebrick\" d=\"M182.24,-129.15C192.02,-129.32 200,-126.61 200,-121 200,-117.58 197.04,-115.24 192.51,-113.97\"/>\n<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"192.56,-110.45 182.24,-112.85 191.8,-117.41 192.56,-110.45\"/>\n<text text-anchor=\"middle\" x=\"211\" y=\"-117.3\" font-family=\"Times,serif\" font-size=\"14.00\">cls1</text>\n</g>\n<!-- s2 -->\n<g id=\"node2\" class=\"node\">\n<title>s2</title>\n<polygon fill=\"#efdf84\" stroke=\"#efdf84\" points=\"70,-139 16,-139 16,-103 70,-103 70,-139\"/>\n<text text-anchor=\"middle\" x=\"43\" y=\"-117.3\" font-family=\"Times,serif\" font-size=\"14.00\">s2</text>\n</g>\n<!-- s2->s2 -->\n<g id=\"edge2\" class=\"edge\">\n<title>s2->s2</title>\n<path fill=\"none\" stroke=\"firebrick\" d=\"M70.24,-129.15C80.02,-129.32 88,-126.61 88,-121 88,-117.58 85.04,-115.24 80.51,-113.97\"/>\n<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"80.56,-110.45 70.24,-112.85 79.8,-117.41 80.56,-110.45\"/>\n<text text-anchor=\"middle\" x=\"99\" y=\"-117.3\" font-family=\"Times,serif\" font-size=\"14.00\">cls1</text>\n</g>\n<!-- s1 -->\n<g id=\"node3\" class=\"node\">\n<title>s1</title>\n<polygon fill=\"#efdf84\" stroke=\"#efdf84\" points=\"90,-52 36,-52 36,-16 90,-16 90,-52\"/>\n<text text-anchor=\"middle\" x=\"63\" y=\"-30.3\" font-family=\"Times,serif\" font-size=\"14.00\">s1</text>\n</g>\n<!-- s2->s1 -->\n<g id=\"edge3\" class=\"edge\">\n<title>s2->s1</title>\n<path fill=\"none\" stroke=\"firebrick\" d=\"M38.53,-102.99C36.7,-93.15 35.7,-80.65 39,-70 39.98,-66.83 41.36,-63.7 42.96,-60.68\"/>\n<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"46,-62.42 48.29,-52.07 40.05,-58.74 46,-62.42\"/>\n<text text-anchor=\"middle\" x=\"50\" y=\"-73.8\" font-family=\"Times,serif\" font-size=\"14.00\">cls1</text>\n</g>\n<!-- s1->s2 -->\n<g id=\"edge4\" class=\"edge\">\n<title>s1->s2</title>\n<path fill=\"none\" stroke=\"firebrick\" d=\"M64.13,-52.4C64.32,-62.14 63.79,-74.41 61,-85 60.25,-87.85 59.24,-90.73 58.08,-93.56\"/>\n<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"54.83,-92.26 53.73,-102.8 61.16,-95.24 54.83,-92.26\"/>\n<text text-anchor=\"middle\" x=\"74\" y=\"-73.8\" font-family=\"Times,serif\" font-size=\"14.00\">cls1</text>\n</g>\n<!-- s1->s1 -->\n<g id=\"edge5\" class=\"edge\">\n<title>s1->s1</title>\n<path fill=\"none\" stroke=\"firebrick\" d=\"M90.24,-42.15C100.02,-42.32 108,-39.61 108,-34 108,-30.58 105.04,-28.24 100.51,-26.97\"/>\n<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"100.56,-23.45 90.24,-25.85 99.8,-30.41 100.56,-23.45\"/>\n<text text-anchor=\"middle\" x=\"119\" y=\"-30.3\" font-family=\"Times,serif\" font-size=\"14.00\">cls1</text>\n</g>\n</g>\n</svg>\n",
+ "text/plain": [
+ "<Dot visualization: expr_as_graph [(\"cls1\", {(s1↦s1),(s1↦s2),(s2↦s1),(s2↦s2),(s3↦s3)})]>"
+ ]
+ },
+ "execution_count": 25,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":dot expr_as_graph (\"cls1\", {(s1↦s1),(s1↦s2),(s2↦s1),(s2↦s2),(s3↦s3)})"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "id": "6142e45d",
+ "metadata": {},
+ "source": [
+ "In Prolog we can encode transitive closure as this:\n",
+ "```\n",
+ "cls1(A,B) :- next(A,B).\n",
+ "cls1(A,B) :- next(A,C), cls1(C,B).\n",
+ "```\n",
+ "So even though Prolog is built on top of first-order logic, it has a \"minimization\" built-in: the semantics of the above Prolog program are not <b>all</b> models satisfying the clauses, but the minimal Herbrand model, which here encodes exactly the transitive closure.\n",
+ "\n",
+ "Note that the Clark completion is an attempt at modelling the semantics of Prolog programs in first-order logic.\n",
+ "The Clark completion translates the implications of the two clauses above into a single equivalence formula of the form:"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 27,
+ "id": "73cc5e59",
+ "metadata": {
+ "vscode": {
+ "languageId": "plaintext"
+ }
+ },
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$\\mathit{TRUE}$\n",
+ "\n",
+ "**Solution:**\n",
+ "* $\\mathit{cls1} = \\{(\\mathit{s1}\\mapsto\\mathit{s2}),(\\mathit{s2}\\mapsto\\mathit{s1}),(\\mathit{s1}\\mapsto\\mathit{s1}),(\\mathit{s2}\\mapsto\\mathit{s2}),(\\mathit{s3}\\mapsto\\mathit{s3})\\}$"
+ ],
+ "text/plain": [
+ "TRUE\n",
+ "\n",
+ "Solution:\n",
+ "\tcls1 = {(s1↦s2),(s2↦s1),(s1↦s1),(s2↦s2),(s3↦s3)}"
+ ]
+ },
+ "execution_count": 27,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "!(A,B).( A:States & B:States =>\n",
+ " (A|->B : cls1 \n",
+ " <=>\n",
+ " (A|->B : next \n",
+ " or\n",
+ " #C.(C:States & A|->C:next & C|->B:cls1)\n",
+ " ) \n",
+ " ))"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "id": "8c683280",
+ "metadata": {},
+ "source": [
+ "As our initial attempt at axiomatising the transitive closure, this encoding admits eightmany solutions:"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 29,
+ "id": "1dcb6a9d",
+ "metadata": {
+ "vscode": {
+ "languageId": "plaintext"
+ }
+ },
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "|cls1|\n",
+ "|---|\n",
+ "|{(s1↦s1),(s1↦s2),(s2↦s1),(s2↦s2),(s3↦s3)}|\n",
+ "|{(s1↦s1),(s1↦s2),(s2↦s1),(s2↦s2),(s3↦s1),(s3↦s3)}|\n",
+ "|{(s1↦s1),(s1↦s2),(s2↦s1),(s2↦s2),(s3↦s2),(s3↦s3)}|\n",
+ "|{(s1↦s1),(s1↦s2),(s1↦s3),(s2↦s1),(s2↦s2),(s2↦s3),(s3↦s3)}|\n",
+ "|{(s1↦s1),(s1↦s2),(s1↦s3),(s2↦s1),(s2↦s2),(s2↦s3),(s3↦s1),(s3↦s3)}|\n",
+ "|{(s1↦s1),(s1↦s2),(s1↦s3),(s2↦s1),(s2↦s2),(s2↦s3),(s3↦s2),(s3↦s3)}|\n",
+ "|{(s1↦s1),(s1↦s2),(s2↦s1),(s2↦s2),(s3↦s1),(s3↦s2),(s3↦s3)}|\n",
+ "|{(s1↦s1),(s1↦s2),(s1↦s3),(s2↦s1),(s2↦s2),(s2↦s3),(s3↦s1),(s3↦s2),(s3↦s3)}|\n"
+ ],
+ "text/plain": [
+ "cls1\n",
+ "{(s1|->s1),(s1|->s2),(s2|->s1),(s2|->s2),(s3|->s3)}\n",
+ "{(s1|->s1),(s1|->s2),(s2|->s1),(s2|->s2),(s3|->s1),(s3|->s3)}\n",
+ "{(s1|->s1),(s1|->s2),(s2|->s1),(s2|->s2),(s3|->s2),(s3|->s3)}\n",
+ "{(s1|->s1),(s1|->s2),(s1|->s3),(s2|->s1),(s2|->s2),(s2|->s3),(s3|->s3)}\n",
+ "{(s1|->s1),(s1|->s2),(s1|->s3),(s2|->s1),(s2|->s2),(s2|->s3),(s3|->s1),(s3|->s3)}\n",
+ "{(s1|->s1),(s1|->s2),(s1|->s3),(s2|->s1),(s2|->s2),(s2|->s3),(s3|->s2),(s3|->s3)}\n",
+ "{(s1|->s1),(s1|->s2),(s2|->s1),(s2|->s2),(s3|->s1),(s3|->s2),(s3|->s3)}\n",
+ "{(s1|->s1),(s1|->s2),(s1|->s3),(s2|->s1),(s2|->s2),(s2|->s3),(s3|->s1),(s3|->s2),(s3|->s3)}\n"
+ ]
+ },
+ "execution_count": 29,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":table {cls1|\n",
+ " !(A,B).( A:States & B:States =>\n",
+ " (A|->B : cls1 \n",
+ " <=>\n",
+ " (A|->B : next \n",
+ " or\n",
+ " #C.(C:States & A|->C:next & C|->B:cls1)\n",
+ " ) \n",
+ " ))}"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": null,
+ "id": "8e13128d",
+ "metadata": {
+ "vscode": {
+ "languageId": "plaintext"
+ }
+ },
+ "outputs": [],
+ "source": []
+ }
+ ],
+ "metadata": {
+ "kernelspec": {
+ "display_name": "ProB 2",
+ "language": "prob",
+ "name": "prob2"
+ },
+ "language_info": {
+ "codemirror_mode": "prob2_jupyter_repl",
+ "file_extension": ".prob",
+ "mimetype": "text/x-prob2-jupyter-repl",
+ "name": "prob"
+ }
+ },
+ "nbformat": 4,
+ "nbformat_minor": 5
+}