docs/tutorials/notebooks/Semigroups,_Monoids_and_Groups.ipynb

{
  "cells": [
    {
      "attachments": {},
      "cell_type": "markdown",
      "metadata": {
        "colab_type": "text",
        "id": "view-in-github"
      },
      "source": [
        "<a href=\"https://colab.research.google.com/github/sasha704/conjure/blob/semigroups/docs/tutorials/notebooks/Semigroups%2C_Monoids_and_Groups.ipynb\" target=\"_parent\"><img src=\"https://colab.research.google.com/assets/colab-badge.svg\" alt=\"Open In Colab\"/></a>"
      ]
    },
    {
      "attachments": {},
      "cell_type": "markdown",
      "metadata": {
        "id": "tlwA1gWxaq7u"
      },
      "source": [
        "# Semigroups, Monoids and Groups"
      ]
    },
    {
      "attachments": {},
      "cell_type": "markdown",
      "metadata": {
        "id": "3kKmC_37a2uo"
      },
      "source": [
        "Original [Semigroups, Monoids and Groups](https://conjure.readthedocs.io/en/latest/tutorials/Groups.html) by Chris Jefferson and Alice Lynch. Adapted by Alex Gallagher."
      ]
    },
    {
      "attachments": {},
      "cell_type": "markdown",
      "metadata": {
        "id": "Tly_igpYbNYM"
      },
      "source": [
        "This tutorial discusses how to model semigroups, monoids and groups in Essence."
      ]
    },
    {
      "cell_type": "code",
      "execution_count": null,
      "metadata": {
        "colab": {
          "base_uri": "https://localhost:8080/",
          "height": 173
        },
        "id": "0RYHwN9UcZ0A",
        "outputId": "a740cb25-36a7-4a06-95bd-9a546aa001ea"
      },
      "outputs": [
        {
          "name": "stdout",
          "output_type": "stream",
          "text": [
            "  % Total    % Received % Xferd  Average Speed   Time    Time     Time  Current\n",
            "                                 Dload  Upload   Total   Spent    Left  Speed\n",
            "\r  0     0    0     0    0     0      0      0 --:--:-- --:--:-- --:--:--     0\r100   697  100   697    0     0   4329      0 --:--:-- --:--:-- --:--:--  4329\n",
            "Installing Conjure...\n",
            "Conjure: The Automated Constraint Modelling Tool\n",
            "Release version 2.4.0\n",
            "Repository version a7382e3d9 (2022-11-21 10:41:03 +0000)\n"
          ]
        },
        {
          "data": {
            "application/javascript": "\"use strict\";\n\nCodeMirror.defineMode(\"text/conjure\", function (config) {\n\n    var isOperatorChar = /[+\\-*=<>%^\\/]/;\n\n    var keywords = {\n        \"forall\": true,\n        \"allDifferent\": true,\n        \"allDiff\": true,\n        \"alldifferent_except\": true,\n        \"dim\": true,\n        \"toSet\": true,\n        \"toMSet\": true,\n        \"toRelation\": true,\n        \"maximising\": true,\n        \"minimising\": true,\n        \"forAll\": true,\n        \"exists\": true,\n        \"toInt\": true,\n        \"sum\": true,\n        \"be\": true,\n        \"bijective\": true,\n        \"bool\": true,\n        \"by\": true,\n        \"complete\": true,\n        \"defined\": true,\n        \"domain\": true,\n        \"in\": true,\n        \"or\": true,\n        \"and\": true,\n        \"false\": true,\n        \"find\": true,\n        \"from\": true,\n        \"function\": true,\n        \"given\": true,\n        \"image\": true,\n        \"indexed\": true,\n        \"injective\": true,\n        \"int\": true,\n        \"intersect\": true,\n        \"freq\": true,\n        \"lambda\": true,\n        \"language\": true,\n        \"letting\": true,\n        \"matrix\": true,\n        \"maxNumParts\": true,\n        \"maxOccur\": true,\n        \"maxPartSize\": true,\n        \"maxSize\": true,\n        \"minNumParts\": true,\n        \"minOccur\": true,\n        \"minPartSize\": true,\n        \"minSize\": true,\n        \"mset\": true,\n        \"numParts\": true,\n        \"of\": true,\n        \"partial\": true,\n        \"partition\": true,\n        \"partSize\": true,\n        \"preImage\": true,\n        \"quantifier\": true,\n        \"range\": true,\n        \"regular\": true,\n        \"relation\": true,\n        \"representation\": true,\n        \"set\": true,\n        \"size\": true,\n        \"subset\": true,\n        \"subsetEq\": true,\n        \"such\": true,\n        \"supset\": true,\n        \"supsetEq\": true,\n        \"surjective\": true,\n        \"that\": true,\n        \"together\": true,\n        \"enum\": true,\n        \"total\": true,\n        \"true\": true,\n        \"new\": true,\n        \"type\": true,\n        \"tuple\": true,\n        \"union\": true,\n        \"where\": true,\n        \"branching\": true,\n        \"on\": true\n    };  \n    var punc = \":;,.(){}[]\";\n\n    function tokenBase(stream, state) {\n        var ch = stream.next();\n        if (ch == '\"') {\n            state.tokenize.push(tokenString);\n            return tokenString(stream, state);\n        }\n        if (/[\\d\\.]/.test(ch)) {\n            if (ch == \".\") {\n                stream.match(/^[0-9]+([eE][\\-+]?[0-9]+)?/);\n            } else if (ch == \"0\") {\n                stream.match(/^[xX][0-9a-fA-F]+/) || stream.match(/^0[0-7]+/);\n            } else {\n                stream.match(/^[0-9]*\\.?[0-9]*([eE][\\-+]?[0-9]+)?/);\n            }\n            return \"number\";\n        }\n        if (ch == \"/\") {\n            if (stream.eat(\"*\")) {\n                state.tokenize.push(tokenComment);\n                return tokenComment(stream, state);\n            }\n        }\n        if (ch == \"$\") {\n            stream.skipToEnd();\n            return \"comment\";\n        }\n        if (isOperatorChar.test(ch)) {\n            stream.eatWhile(isOperatorChar);\n            return \"operator\";\n        }\n        if (punc.indexOf(ch) > -1) {\n            return \"punctuation\";\n        }\n        stream.eatWhile(/[\\w\\$_\\xa1-\\uffff]/);\n        var cur = stream.current();\n        \n        if (keywords.propertyIsEnumerable(cur)) {\n            return \"keyword\";\n        }\n        return \"variable\";\n    }\n\n    function tokenComment(stream, state) {\n        var maybeEnd = false, ch;\n        while (ch = stream.next()) {\n            if (ch == \"/\" && maybeEnd) {\n                state.tokenize.pop();\n                break;\n            }\n            maybeEnd = (ch == \"*\");\n        }\n        return \"comment\";\n    }\n\n    function tokenUntilClosingParen() {\n        var depth = 0;\n        return function (stream, state, prev) {\n            var inner = tokenBase(stream, state, prev);\n            console.log(\"untilClosing\", inner, stream.current());\n            if (inner == \"punctuation\") {\n                if (stream.current() == \"(\") {\n                    ++depth;\n                } else if (stream.current() == \")\") {\n                    if (depth == 0) {\n                        stream.backUp(1)\n                        state.tokenize.pop()\n                        return state.tokenize[state.tokenize.length - 1](stream, state)\n                    } else {\n                        --depth;\n                    }\n                }\n            }\n            return inner;\n        }\n    }\n\n    function tokenString(stream, state) {\n        var escaped = false, next, end = false;\n        while ((next = stream.next()) != null) {\n            if (next == '(' && escaped) {\n                state.tokenize.push(tokenUntilClosingParen());\n                return \"string\";\n            }\n            if (next == '\"' && !escaped) { end = true; break; }\n            escaped = !escaped && next == \"\\\\\";\n        }\n        if (end || !escaped)\n            state.tokenize.pop();\n        return \"string\";\n    }\n\n    return {\n        startState: function (basecolumn) {\n            return {\n                tokenize: []\n            };\n        },\n\n        token: function (stream, state) {\n            if (stream.eatSpace()) return null;\n            var style = (state.tokenize[state.tokenize.length - 1] || tokenBase)(stream, state);\n            console.log(\"token\", style);\n            return style;\n        },\n\n        blockCommentStart: \"/*\",\n        blockCommentEnd: \"*/\",\n        lineComment: \"$\"\n    };\n});\n\n\nCodeMirror.defineMIME(\"text/conjure\", \"text/conjure\");\n\nrequire(['notebook/js/codecell'], function (codecell) {\n    codecell.CodeCell.options_default.highlight_modes['magic_text/conjure'] = { 'reg': [/%?%conjure/] };\n    Jupyter.notebook.events.one('kernel_ready.Kernel', function () {\n        Jupyter.notebook.get_cells().map(function (cell) {\n            if (cell.cell_type == 'code') { cell.auto_highlight(); }\n        });\n    });\n});\n\n",
            "text/plain": [
              "<IPython.core.display.Javascript object>"
            ]
          },
          "metadata": {},
          "output_type": "display_data"
        },
        {
          "name": "stdout",
          "output_type": "stream",
          "text": [
            "Conjure extension is loaded.\n",
            "For usage help run: %conjure_help\n"
          ]
        }
      ],
      "source": [
        "!source <(curl -s https://raw.githubusercontent.com/conjure-cp/conjure-notebook/v0.0.2/scripts/install-colab.sh)\n",
        "%load_ext conjure"
      ]
    },
    {
      "attachments": {},
      "cell_type": "markdown",
      "metadata": {
        "id": "IIXm6aerbQEv"
      },
      "source": [
        "## The Problem"
      ]
    },
    {
      "attachments": {},
      "cell_type": "markdown",
      "metadata": {
        "id": "8_84KDprbpLq"
      },
      "source": [
        "Semigroups, monoids and groups are all examples of binary operations, with added conditions.\n",
        "\n",
        "\n",
        "We will begin by building a binary operation. A binary relation `R` on a domain `S` is a two-argument function which maps two elements of `S` to a third element of `S`. We will make `S` be the integers from `1` to `n`, for some given `n`."
      ]
    },
    {
      "attachments": {},
      "cell_type": "markdown",
      "metadata": {
        "id": "aP09RDjCc03v"
      },
      "source": [
        "We make a new type of size `n` to represent the set the operation is defined on. We then define a function from `(S,S)` to `S`. Technically, this function doesn’t take two arguments - it takes a single argument which is a pair of values from `S`. This is mathematically the same, but will change how we use `R`.\n",
        "\n",
        "\n",
        "We will begin by creating a solution to this, for `n = 4`."
      ]
    },
    {
      "cell_type": "code",
      "execution_count": null,
      "metadata": {
        "id": "WutDydBpcrlm"
      },
      "outputs": [],
      "source": [
        "n = 4"
      ]
    },
    {
      "cell_type": "code",
      "execution_count": null,
      "metadata": {
        "colab": {
          "base_uri": "https://localhost:8080/"
        },
        "id": "ruoE-Rc-b-eP",
        "outputId": "2404a163-69b6-466e-86a0-ef24f370ba85"
      },
      "outputs": [
        {
          "data": {
            "text/plain": [
              "{'R': [[[1, 1], 1],\n",
              "  [[1, 2], 1],\n",
              "  [[1, 3], 1],\n",
              "  [[1, 4], 1],\n",
              "  [[2, 1], 1],\n",
              "  [[2, 2], 1],\n",
              "  [[2, 3], 1],\n",
              "  [[2, 4], 1],\n",
              "  [[3, 1], 1],\n",
              "  [[3, 2], 1],\n",
              "  [[3, 3], 1],\n",
              "  [[3, 4], 1],\n",
              "  [[4, 1], 1],\n",
              "  [[4, 2], 1],\n",
              "  [[4, 3], 1],\n",
              "  [[4, 4], 1]]}"
            ]
          },
          "execution_count": 4,
          "metadata": {},
          "output_type": "execute_result"
        }
      ],
      "source": [
        "%%conjure\n",
        "given n : int\n",
        "letting S be domain int(1..n)\n",
        "\n",
        "find R : function(total) (S,S) --> S"
      ]
    },
    {
      "attachments": {},
      "cell_type": "markdown",
      "metadata": {
        "id": "d6aN2lyydSpa"
      },
      "source": [
        "At the moment this is quite boring, as the function can take any value at all! Asking Conjure how many solutions this problem has is unreasonable, but we can figure it out with maths:\n",
        "\n",
        "4<sup>16</sup> = 4,294,967,296\n",
        "\n",
        "Let’s try adding some constraints."
      ]
    },
    {
      "attachments": {},
      "cell_type": "markdown",
      "metadata": {
        "id": "7fJvxGbLd3Rp"
      },
      "source": [
        "## Semigroups"
      ]
    },
    {
      "attachments": {},
      "cell_type": "markdown",
      "metadata": {
        "id": "s7QuRhtUd52X"
      },
      "source": [
        "The simplest object we will consider is a **semigroup**. A semigroup adds one constraint to our binary operation, **associativity**. A binary operation is associative if for all i,j and k in S, R(i,R(j,k)) = R((R(i,j),k). This might look very abstract, but it is true of many binary operations, for example given integers i,j and k, (i+j)+k = i+(j+k), and (i * j) * k = i * (j * k)."
      ]
    },
    {
      "attachments": {},
      "cell_type": "markdown",
      "metadata": {
        "id": "0gWAIm26eGVv"
      },
      "source": [
        "We begin by saying we want to check `forAll i,j,k: S`. The strangest bit is all of the brackets seem doubled. Your vision isn’t failing, this is because `M` is a one argument function (and we use `M(x)` to apply `M` to `x`), but `M` takes a tuple as its argument (which we write as `(i,j)`), so to apply `M` to `i` and `j` we write `M((i,j))`."
      ]
    },
    {
      "cell_type": "code",
      "execution_count": null,
      "metadata": {
        "colab": {
          "base_uri": "https://localhost:8080/"
        },
        "id": "E5hy8Xe7ebsM",
        "outputId": "e878e0f2-d253-46eb-c723-7eed146e726d"
      },
      "outputs": [
        {
          "data": {
            "text/plain": [
              "{'R': [[[1, 1], 1],\n",
              "  [[1, 2], 1],\n",
              "  [[1, 3], 1],\n",
              "  [[1, 4], 1],\n",
              "  [[2, 1], 1],\n",
              "  [[2, 2], 1],\n",
              "  [[2, 3], 1],\n",
              "  [[2, 4], 1],\n",
              "  [[3, 1], 1],\n",
              "  [[3, 2], 1],\n",
              "  [[3, 3], 1],\n",
              "  [[3, 4], 1],\n",
              "  [[4, 1], 1],\n",
              "  [[4, 2], 1],\n",
              "  [[4, 3], 1],\n",
              "  [[4, 4], 1]]}"
            ]
          },
          "execution_count": 6,
          "metadata": {},
          "output_type": "execute_result"
        }
      ],
      "source": [
        "%%conjure\n",
        "letting S be domain int(1..n)\n",
        "\n",
        "find R : function(total) (S,S) --> S\n",
        "\n",
        "such that\n",
        "\n",
        "forAll i,j,k: S. R((i,R((j,k)))) = R((R((i,j)),k))"
      ]
    },
    {
      "attachments": {},
      "cell_type": "markdown",
      "metadata": {
        "id": "uQBnwZarenjL"
      },
      "source": [
        "The first result is still the same, but there are fewer solutions to be found now - only 3,492. Is this correct? It’s always good to check. This number was first published in 1955, by George E. Forsythe, in his paper “SWAC Computes 126 Distinct Semigroups of Order 4”. Where does the number 126 come from? This small number comes from ignoring cases where the semigroup is the same except for rearranging the numbers 1,2,3,4. The number we found, 3,492, is found in the paper."
      ]
    },
    {
      "attachments": {},
      "cell_type": "markdown",
      "metadata": {
        "id": "Kxr07DIuex8m"
      },
      "source": [
        "## Monoids"
      ]
    },
    {
      "attachments": {},
      "cell_type": "markdown",
      "metadata": {
        "id": "kHVypWgQe6Fr"
      },
      "source": [
        "Let’s move further to monoids. A monoid is a semigroup with an extra condition, there has to exist some element of the semigroup, which we will call *e*, which acts as an **identity**. An **identity** is an element such that for all `i` in `S`, `R(e,i) = R(i,e) = e`.\n",
        "\n",
        "Firstly we will add a variable to store the value of this `e`, and then add the extra constraint which makes it an identity:"
      ]
    },
    {
      "cell_type": "code",
      "execution_count": null,
      "metadata": {
        "colab": {
          "base_uri": "https://localhost:8080/"
        },
        "id": "6d9Bng1hfpEm",
        "outputId": "e95c22bf-cd3f-4d3e-f37a-70ea909351b6"
      },
      "outputs": [
        {
          "data": {
            "text/plain": [
              "{'R': [[[1, 1], 1],\n",
              "  [[1, 2], 2],\n",
              "  [[1, 3], 3],\n",
              "  [[1, 4], 4],\n",
              "  [[2, 1], 2],\n",
              "  [[2, 2], 1],\n",
              "  [[2, 3], 4],\n",
              "  [[2, 4], 3],\n",
              "  [[3, 1], 3],\n",
              "  [[3, 2], 4],\n",
              "  [[3, 3], 1],\n",
              "  [[3, 4], 2],\n",
              "  [[4, 1], 4],\n",
              "  [[4, 2], 3],\n",
              "  [[4, 3], 2],\n",
              "  [[4, 4], 1]],\n",
              " 'e': 1,\n",
              " 'inv': {'1': 1, '2': 2, '3': 3, '4': 4}}"
            ]
          },
          "execution_count": 12,
          "metadata": {},
          "output_type": "execute_result"
        }
      ],
      "source": [
        "%%conjure\n",
        "\n",
        "letting S be domain int(1..n)\n",
        "\n",
        "find R : function (total) (S,S) --> S\n",
        "\n",
        "find e : S\n",
        "\n",
        "such that\n",
        "\n",
        "forAll i,j,k: S. R((i,R((j,k)))) = R((R((i,j)),k)),\n",
        "forAll i : S. R((e,i)) = i /\\ R((i,e)) = i,"
      ]
    },
    {
      "attachments": {},
      "cell_type": "markdown",
      "metadata": {
        "id": "8UUknSEagk34"
      },
      "source": [
        "We now have only 624 solutions! We can check this by looking at the amazing online encyclopedia of integer sequences https://oeis.org/A058153 , which tells us there are indeed 624 “labelled monoids” of order n."
      ]
    },
    {
      "attachments": {},
      "cell_type": "markdown",
      "metadata": {
        "id": "2gudg9KYgp6R"
      },
      "source": [
        "## Groups"
      ]
    },
    {
      "attachments": {},
      "cell_type": "markdown",
      "metadata": {
        "id": "eWHVoUvPgrbh"
      },
      "source": [
        "Finally, let us move to groups. Groups add one important requirement, the concept of an inverse. Given some `i` in `S`, `j` is an inverse of `i` if `R((i,j)) = R((j,i)) = e`, where `e` is our already existing identity.\n",
        "\n",
        "We will store the inverses as an extra array, and then add this final constraint:"
      ]
    },
    {
      "cell_type": "code",
      "execution_count": null,
      "metadata": {
        "colab": {
          "base_uri": "https://localhost:8080/"
        },
        "id": "kjnJufr6g7RP",
        "outputId": "d612e8b4-54a2-4c5a-8651-1dd386771596"
      },
      "outputs": [
        {
          "data": {
            "text/plain": [
              "{'R': [[[1, 1], 1],\n",
              "  [[1, 2], 2],\n",
              "  [[1, 3], 3],\n",
              "  [[1, 4], 4],\n",
              "  [[2, 1], 2],\n",
              "  [[2, 2], 1],\n",
              "  [[2, 3], 4],\n",
              "  [[2, 4], 3],\n",
              "  [[3, 1], 3],\n",
              "  [[3, 2], 4],\n",
              "  [[3, 3], 1],\n",
              "  [[3, 4], 2],\n",
              "  [[4, 1], 4],\n",
              "  [[4, 2], 3],\n",
              "  [[4, 3], 2],\n",
              "  [[4, 4], 1]],\n",
              " 'e': 1,\n",
              " 'inv': {'1': 1, '2': 2, '3': 3, '4': 4}}"
            ]
          },
          "execution_count": 9,
          "metadata": {},
          "output_type": "execute_result"
        }
      ],
      "source": [
        "%%conjure\n",
        "letting S be domain int(1..n)\n",
        "\n",
        "find R : function (total) (S,S) --> S\n",
        "\n",
        "find e : S\n",
        "\n",
        "find inv: function S --> S\n",
        "\n",
        "such that\n",
        "\n",
        "forAll i,j,k: S. R((i,R((j,k)))) = R((R((i,j)),k)),\n",
        "forAll i : S. R((e,i)) = i /\\ R((i,e)) = i,\n",
        "\n",
        "forAll i : S. R((i,inv(i))) = e /\\ R((inv(i),i)) = e"
      ]
    },
    {
      "attachments": {},
      "cell_type": "markdown",
      "metadata": {
        "id": "HAdxspUohyta"
      },
      "source": [
        "This solution has much more going on than our previous ones! For example, each row and column contains the numbers from `1` to `4`, in some order. This (and many, many other results) are true for all groups (but we won’t prove this here!). This problem only has 16 solutions, and once we removed the groups which are made by just swapping around 1,2,3 and 4, we would find there was only 2 groups! The extra structure means there are only a small number of groups for each size, compared to the number of semigroups and monoids.\n",
        "\n",
        "There are many special types of groups; we will consider just one here, abelian groups. A group is abelian if for all `i` and `j` in `S`, `R((i,j)) = R((j,i))`. Let’s add this condition!"
      ]
    },
    {
      "cell_type": "code",
      "execution_count": null,
      "metadata": {
        "colab": {
          "base_uri": "https://localhost:8080/"
        },
        "id": "Kunrbz0-iXhY",
        "outputId": "2a1b5af6-f56e-4ba4-fc1e-c6f55b8be553"
      },
      "outputs": [
        {
          "data": {
            "text/plain": [
              "{'R': [[[1, 1], 1],\n",
              "  [[1, 2], 2],\n",
              "  [[1, 3], 3],\n",
              "  [[1, 4], 4],\n",
              "  [[2, 1], 2],\n",
              "  [[2, 2], 1],\n",
              "  [[2, 3], 4],\n",
              "  [[2, 4], 3],\n",
              "  [[3, 1], 3],\n",
              "  [[3, 2], 4],\n",
              "  [[3, 3], 1],\n",
              "  [[3, 4], 2],\n",
              "  [[4, 1], 4],\n",
              "  [[4, 2], 3],\n",
              "  [[4, 3], 2],\n",
              "  [[4, 4], 1]],\n",
              " 'e': 1,\n",
              " 'inv': {'1': 1, '2': 2, '3': 3, '4': 4}}"
            ]
          },
          "execution_count": 11,
          "metadata": {},
          "output_type": "execute_result"
        }
      ],
      "source": [
        "%%conjure\n",
        "letting S be domain int(1..n)\n",
        "\n",
        "find R : function (total) (S,S) --> S\n",
        "\n",
        "find e : S\n",
        "\n",
        "find inv: function S --> S\n",
        "\n",
        "such that\n",
        "\n",
        "forAll i,j,k: S. R((i,R((j,k)))) = R((R((i,j)),k)),\n",
        "forAll i : S. R((e,i)) = i /\\ R((i,e)) = i,\n",
        "forAll i : S. R((i,inv(i))) = e /\\ R((inv(i),i)) = e,\n",
        "forAll i,j : S. R((i,j)) = R((j,i))"
      ]
    },
    {
      "attachments": {},
      "cell_type": "markdown",
      "metadata": {
        "id": "yZDLJ0G6ifkn"
      },
      "source": [
        "This gives us the same first solution. In fact, there is the same number of solutions (16) to this problem as the previous one, proving that all groups of size 4 are abelian! In fact, the smallest non-abelian group is size 60, and that is beyond the size of problems we can find all solutions to with our current, simple model."
      ]
    }
  ],
  "metadata": {
    "colab": {
      "authorship_tag": "ABX9TyNmwuGfH/vOYeP0Tj5vUcu/",
      "include_colab_link": true,
      "provenance": []
    },
    "kernelspec": {
      "display_name": "Python 3",
      "name": "python3"
    },
    "language_info": {
      "name": "python"
    }
  },
  "nbformat": 4,
  "nbformat_minor": 0
}