learntlaplus.ipynb

{
 "cells": [
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "# Introduction\n",
    "\n",
    "This notebook provides an interactive environment to work out the exercises from https://learntla.com/. \n",
    "\n",
    "You can use it like this:\n",
    "1. Read a section in https://learntla.com/tla/\n",
    "2. For each exercise edit the cell and look at the output until you think you have the correct solution\n",
    "3. Look at the solution\n",
    "\n",
    "Selected cells can be run with `Ctrl + Enter`."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "# Operators"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "https://learntla.com/tla/operators/\n",
    "\n",
    "Write an operator that tests if two numbers are not equal."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "solution2": "hidden",
    "solution2_first": true
   },
   "outputs": [],
   "source": [
    "LET \n",
    "  Neq(a, b) == FALSE\n",
    "IN\n",
    "  Neq(1,2)\n",
    "  \\* TRUE"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "solution2": "hidden"
   },
   "outputs": [],
   "source": [
    "LET \n",
    "  Neq(a,b) == a /= b \n",
    "IN\n",
    "  /\\ Neq(1,2) = TRUE\n",
    "  /\\ Neq(1,1) = FALSE"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## Higher-Order Operators"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Write an operator that determines whether a second operator is commutative over two given numbers. An operator is commutative if `f(a,b) = f(b,a)`."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "solution2": "hidden",
    "solution2_first": true
   },
   "outputs": [],
   "source": [
    "LET\n",
    "  Sum(a, b) == a + b\n",
    "  Sub(a, b) == a - b\n",
    "\n",
    "  IsCommutative(op(_,_), a, b) == FALSE\n",
    "IN\n",
    "  IsCommutative(Sum, 2, 4)\n",
    "  \\* TRUE"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "solution2": "hidden"
   },
   "outputs": [],
   "source": [
    "LET\n",
    "  Sum(a, b) == a + b\n",
    "  Sub(a, b) == a - b\n",
    "\n",
    "  IsCommutative(op(_, _), a, b) == op(a, b) = op(b, a)\n",
    "IN\n",
    "  /\\ IsCommutative(Sum, 2, 4) = TRUE\n",
    "  /\\ IsCommutative(Sub, 4, 2) = FALSE"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "# Tuples and Structures\n",
    "https://learntla.com/tla/tuples/\n",
    "## Tuples"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Write an operator that takes a tuple and, if the tuple is length two, returns the reversed tuple, and otherwise returns the original tuple."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "solution2": "hidden",
    "solution2_first": true
   },
   "outputs": [],
   "source": [
    "LET\n",
    "  Reverse(T) == <<1, 1>>\n",
    "IN\n",
    "  Reverse(<<1, 2>>)\n",
    "  \\* <<2, 1>>"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "solution2": "hidden"
   },
   "outputs": [],
   "source": [
    "LET\n",
    "  Reverse(T) == IF Len(T) = 2 THEN <<T[2], T[1]>> ELSE T\n",
    "IN\n",
    "  /\\ Reverse(<<1, 2>>) = <<2, 1>>\n",
    "  /\\ Reverse(<<1, 2, 3>>) = <<1, 2, 3>>"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "# Sets\n",
    "https://learntla.com/tla/sets/\n",
    "## Mapping"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Given DOMAIN Tuple is the set of numbers Tuple is defined over, write an operator that gives you the values of the Tuple, ie the range."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "solution2": "hidden",
    "solution2_first": true
   },
   "outputs": [],
   "source": [
    "LET\n",
    "  Range(T) == {1}\n",
    "IN\n",
    "  Range(<<1, 3, 5>>)\n",
    "  \\* {1, 3, 5}"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "solution2": "hidden"
   },
   "outputs": [],
   "source": [
    "LET\n",
    "  Range(T) == { T[x] : x \\in DOMAIN T }\n",
    "IN\n",
    "  /\\ Range(<<1, 3, 5>>) = {1, 3, 5}\n",
    "  /\\ Range(<<100, 200, 300>>) = {100, 200, 300}"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## Set Operators"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Write an operator that takes two sets S1 and S2 and determines if the double of every element in S1 is an element of S2."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "solution2": "hidden",
    "solution2_first": true
   },
   "outputs": [],
   "source": [
    "LET\n",
    "  IsDoubleSubset(S1, S2) == FALSE\n",
    "IN\n",
    "  IsDoubleSubset({3,5,20}, {6,10,40,1})\n",
    "  \\* TRUE"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "solution2": "hidden"
   },
   "outputs": [],
   "source": [
    "LET\n",
    "  IsDoubleSubset(S1, S2) == {x * 2 : x \\in S1} \\subseteq S2\n",
    "IN\n",
    "  /\\ IsDoubleSubset({3,5,20}, {6,10,40,1}) = TRUE\n",
    "  /\\ IsDoubleSubset({1,3,5,20}, {6,10,40,1}) = FALSE"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Given a sequence of sets, write an operator that determines if a given element is found in any of the sequence’s sets. IE\n",
    "```\n",
    "InSeqSets(\"a\", <<{\"b\", \"c\"}, {\"a\", \"c\"}>>) = TRUE\n",
    "```."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "solution2": "hidden",
    "solution2_first": true
   },
   "outputs": [],
   "source": [
    "LET\n",
    "  Range(T) == { T[x] : x \\in DOMAIN T }\n",
    "\n",
    "  InSeqSets(element, tupleOfSets) == FALSE\n",
    "IN \n",
    "  InSeqSets(\"a\", <<{\"b\", \"c\"}, {\"a\", \"c\"}>>)\n",
    "  \\* TRUE"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "solution2": "hidden"
   },
   "outputs": [],
   "source": [
    "LET\n",
    "  Range(T) == { T[x] : x \\in DOMAIN T }\n",
    "\n",
    "  InSeqSets(element, tupleOfSets) == element \\in UNION Range(tupleOfSets)\n",
    "IN \n",
    "  /\\ InSeqSets(\"a\", <<{\"b\", \"c\"}, {\"a\", \"c\"}>>) = TRUE\n",
    "  /\\ InSeqSets(\"d\", <<{\"b\", \"c\"}, {\"a\", \"c\"}>>) = FALSE"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Given a set, write an operator that returns all subsets of length two. IE\n",
    "```\n",
    "Op(1..3) == {{1, 2}, {1, 3}, {2, 3}}.\n",
    "```"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "solution2": "hidden",
    "solution2_first": true
   },
   "outputs": [],
   "source": [
    "LET\n",
    "  Op(S) == {{1, 1}}\n",
    "IN\n",
    "  Op(1..3)\n",
    "  \\* {1, 2}, {1, 3}, {2, 3}}"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "solution2": "hidden"
   },
   "outputs": [],
   "source": [
    "LET\n",
    "  Op(S) == { subset \\in SUBSET S : Cardinality(subset) = 2 }\n",
    "IN\n",
    "  Op(1..3) = {{1, 2}, {1, 3}, {2, 3}}"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "# Logic\n",
    "https://learntla.com/tla/logic/\n",
    "## \\E"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Assuming Sum(S) returns the sum of the elements of S, write an operator that, for a given set of integers S and integer N, returns `TRUE` if there are N elements in S that sum to 0. eg\n",
    "```TLA\n",
    "SumsToZero({1, 2, -7, 4, 11}, 2) = FALSE\n",
    "SumsToZero({1, 2, -7, 4, 11}, 4) = TRUE\n",
    "SumsToZero({1, 2, -7, 4, 11}, 5) = FALSE\n",
    "```"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "solution2": "hidden",
    "solution2_first": true
   },
   "outputs": [],
   "source": [
    "LET\n",
    "  ReduceSet(op(_, _), set, acc) ==\n",
    "    LET f[s \\in SUBSET set] ==\n",
    "      IF s = {} THEN acc\n",
    "      ELSE LET x == CHOOSE x \\in s: TRUE\n",
    "           IN op(x, f[s \\ {x}])\n",
    "    IN f[set]\n",
    "  Sum(set) == ReduceSet(LAMBDA x, y: x + y, set, 0)\n",
    "\n",
    "  SumsToZero(S, N) == FALSE\n",
    "IN\n",
    "  SumsToZero({1, 2, -7, 4, 11}, 4)\n",
    "  \\* TRUE"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "solution2": "hidden"
   },
   "outputs": [],
   "source": [
    "LET\n",
    "  ReduceSet(op(_, _), set, acc) ==\n",
    "    LET f[s \\in SUBSET set] ==\n",
    "      IF s = {} THEN acc\n",
    "      ELSE LET x == CHOOSE x \\in s: TRUE\n",
    "           IN op(x, f[s \\ {x}])\n",
    "    IN f[set]\n",
    "  Sum(set) == ReduceSet(LAMBDA x, y: x + y, set, 0)\n",
    "\n",
    "  SumsToZero(S, N) == \\E s \\in SUBSET S:\n",
    "                      /\\ Cardinality(s) = N\n",
    "                      /\\ Sum(s) = 0\n",
    "IN\n",
    "  /\\ SumsToZero({1, 2, -7, 4, 11}, 2) = FALSE\n",
    "  /\\ SumsToZero({1, 2, -7, 4, 11}, 4) = TRUE\n",
    "  /\\ SumsToZero({1, 2, -7, 4, 11}, 5) = FALSE"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## \\A"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Given a set and an operator, determine whether the operator is commutative over all elements in the set."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "solution2": "hidden",
    "solution2_first": true
   },
   "outputs": [],
   "source": [
    "LET\n",
    "  Sum(a, b) == a + b\n",
    "  Sub(a, b) == a - b\n",
    "  \n",
    "  IsCommutative(S, op(_,_)) == FALSE\n",
    "IN\n",
    "  IsCommutative({23,4,56,2}, Sum)\n",
    "  \\* TRUE"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "solution2": "hidden"
   },
   "outputs": [],
   "source": [
    "LET\n",
    "  Sum(a, b) == a + b\n",
    "  Sub(a, b) == a - b\n",
    "\n",
    "  IsCommutative(S, op(_,_)) == \\A x \\in S :\n",
    "                               \\A y \\in S : op(x,y) = op(y,x)\n",
    "IN\n",
    "  /\\ IsCommutative({23,4,56,2}, Sum) = TRUE\n",
    "  /\\ IsCommutative({23,4,56,2}, Sub) = FALSE"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## CHOOSE"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Without looking back at the introduction, write an operator that returns the maximum number of a set."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "solution2": "hidden",
    "solution2_first": true
   },
   "outputs": [],
   "source": [
    "LET\n",
    "  Max(S) == 1\n",
    "IN\n",
    "  Max({1,3,7,4})\n",
    "  \\* 7"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "solution2": "hidden"
   },
   "outputs": [],
   "source": [
    "LET\n",
    "  Max(S) == CHOOSE x \\in S : \\A y \\in S : y <= x\n",
    "IN\n",
    "  Max({1,3,7,4}) = 7"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "A prime number p is a twin prime if p-2 is prime or p+2 is prime. Find the largest twin prime in S."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "solution2": "hidden",
    "solution2_first": true
   },
   "outputs": [],
   "source": [
    "LET\n",
    "  IsPrime(x) == x > 1 /\\ ~\\E d \\in 2..(x-1) : x % d = 0\n",
    "\n",
    "  LargestTwinPrime(S) == 1\n",
    "IN\n",
    "  LargestTwinPrime({10, 50, 41, 43, 45})\n",
    "  \\* 43"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "solution2": "hidden"
   },
   "outputs": [],
   "source": [
    "LET\n",
    "  IsPrime(x) == x > 1 /\\ ~\\E d \\in 2..(x-1) : x % d = 0\n",
    "  IsTwinPrime(x) == /\\ IsPrime(x)\n",
    "                    /\\ \\/ IsPrime(x + 2)\n",
    "                       \\/ IsPrime(x - 2)\n",
    "  \n",
    "  \n",
    "  LargestTwinPrime(S) == CHOOSE x \\in S:\n",
    "                      /\\ IsTwinPrime(x)\n",
    "                      /\\ \\A y \\in S: IsTwinPrime(y) => y <= x\n",
    "                      \\* or y > x => ~ IsTwinPrime(y)\n",
    "  \\* or\n",
    "  \\* LargestTwinPrime(S) == Max({x \\in S : IsTwinPrime(x)})\n",
    "IN\n",
    "  /\\ LargestTwinPrime({10, 50, 41, 43, 45}) = 43\n",
    "  /\\ LargestTwinPrime({3, 5, 13}) = 13"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Now return the largest pair of twin primes, ordered by value. Assume that S may be missing numbers and, if one of the twin primes is missing, the pair is invalid. For example, the largest pair in {3, 5, 13} is <<3, 5>>, not <<5, 13>>."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "solution2": "hidden",
    "solution2_first": true
   },
   "outputs": [],
   "source": [
    "LET\n",
    "  IsPrime(x) == x > 1 /\\ ~\\E d \\in 2..(x-1) : x % d = 0\n",
    "\n",
    "  LargestTwinPair(S) == <<1, 2>>\n",
    "IN\n",
    "  LargestTwinPair({3, 5, 11, 13, 41})\n",
    "  \\* <<11, 13>>"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "solution2": "hidden"
   },
   "outputs": [],
   "source": [
    "LET\n",
    "  IsPrime(x) == x > 1 /\\ ~\\E d \\in 2..(x-1) : x % d = 0\n",
    "\n",
    "  LargestTwinPair(S) == CHOOSE <<x, y>> \\in S \\X S:\n",
    "                           /\\ IsPrime(x)\n",
    "                           /\\ IsPrime(y)\n",
    "                           /\\ x = y - 2\n",
    "                           /\\ \\A <<w, z>> \\in S \\X S:\n",
    "                              /\\ IsPrime(z)\n",
    "                              /\\ IsPrime(w)\n",
    "                              /\\ w = z - 2\n",
    "                              => z <= y\n",
    "IN\n",
    "  /\\ LargestTwinPair({3, 5, 13}) = <<3, 5>>\n",
    "  /\\ LargestTwinPair({3, 5, 11, 13, 41}) = <<11, 13>>"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Given stockprices is a tuple of positive integers representing the value of a stock at a given time of day, write an operator that determines the maximum profit you could make by buying and selling a single stock. Assume for this problem that you cannot short; you must buy before you sell."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "solution2": "hidden",
    "solution2_first": true
   },
   "outputs": [],
   "source": [
    "LET\n",
    "  MaxProfit(stockprices) == 1\n",
    "IN\n",
    "  MaxProfit(<<100, 5, 1, 10, 20>>)\n",
    "  \\* 19"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "solution2": "hidden"
   },
   "outputs": [],
   "source": [
    "LET\n",
    "  MaxProfit(stockprices) ==\n",
    "    LET\n",
    "      Time == 1..Len(stockprices)\n",
    "      TimePair == { <<t1, t2>> \\in Time \\X Time : t1 < t2 }\n",
    "      Profits == { stockprices[t2] - stockprices[t1] : <<t1, t2>> \\in TimePair }\n",
    "    IN\n",
    "      CHOOSE max \\in Profits : \\A p \\in Profits : p <= max\n",
    "IN\n",
    "  MaxProfit(<<100, 5, 1, 10, 20>>) = 19\n",
    "\n",
    "\\* Note this will crash if there is no possible pair, which is preferrable\n",
    "\\* to paying trading fees twice on a zero-dollar profit."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "# Functions\n",
    "https://learntla.com/tla/functions/"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Write an operator that takes a string (tuple of characters, here) and returns the number of occurrences of each string token."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "solution2": "hidden",
    "solution2_first": true
   },
   "outputs": [],
   "source": [
    "LET\n",
    "  Range(T) == { T[x] : x \\in DOMAIN T }\n",
    "\n",
    "  Counter(str) == [a |-> 1]\n",
    "\n",
    "IN\n",
    "  Counter(<<\"t\", \"e\", \"s\", \"t\">>)\n",
    "  \\* [s |-> 1, t |-> 2, e |-> 1]"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "solution2": "hidden"
   },
   "outputs": [],
   "source": [
    "LET\n",
    "  Range(T) == { T[x] : x \\in DOMAIN T }\n",
    "\n",
    "  Counter(str) == [c \\in Range(str) |-> Cardinality({n \\in 1..Len(str) : str[n] = c})]\n",
    "IN\n",
    "  Counter(<<\"t\", \"e\", \"s\", \"t\">>) = [s |-> 1, t |-> 2, e |-> 1]"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## Function Sets"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "For a given p in People and a in Animals, p either “like”s them, “hate”s them, or are “neutral”. What is the set of all possible relationships between people, animals, and preferences?"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "solution2": "hidden",
    "solution2_first": true
   },
   "outputs": [],
   "source": [
    "LET\n",
    "  People == {\"alice\", \"bob\"}\n",
    "  Animals == {\"dog\", \"cat\", \"alligator\"}\n",
    "  Relationships == {\"like\", \"hate\", \"neutral\"}\n",
    "\n",
    "  Prefs == {\"alice\"}\n",
    "IN\n",
    "  Prefs\n",
    "  \\* Cardinality(Prefs) = 729"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "solution2": "hidden"
   },
   "outputs": [],
   "source": [
    "LET\n",
    "  People == {\"alice\", \"bob\"}\n",
    "  Animals == {\"dog\", \"cat\", \"alligator\"}\n",
    "  Relationships == {\"like\", \"hate\", \"neutral\"}\n",
    "\n",
    "  \\* There’s a few ways to do this. First, we could chain two function sets.\n",
    "  \\* Pref == [People -> [Animals -> Relationships]]\n",
    "  \\* For pref \\in Pref, we would call it with pref[p][a].\n",
    "  \n",
    "  \\* We could also use a set of structures:\n",
    "  \\* Pref == [[person: People, animal: Animals] -> Relationships]\n",
    "  \\* This tends to be very awkward, as we end up having to call that with pref[[person: p, animal: a]].\n",
    "  \n",
    "  \\* Finally, we could use a tuple:\n",
    "  Pref == [People \\X Animals -> Relationships]\n",
    "  \\* We would call pref with pref[<<p, a>>].\n",
    "  \\* I’ve personally found this to be the least cumbersome, and its the way\n",
    "  \\* we’ll be writing multivariable functions going forward.\n",
    "IN\n",
    "  Cardinality(Pref) = 729"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "`EXTENDS Sequences` gives you the `Seq(S)` operator, which gives you the set of all sequences with a range in S. Unfortunately, you can’t actually use this operator, since it will crash TLC. So let’s make some better versions. First, write an operator that returns a tuple of N copies of a set. For example\n",
    "```\n",
    "Op(S, 3) == S \\X S \\X S\n",
    "```"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "solution2": "hidden",
    "solution2_first": true
   },
   "outputs": [],
   "source": [
    "LET\n",
    "  Tup(S, n) == {1}\n",
    "IN\n",
    "  Tup({\"a\", \"b\"}, 2)\n",
    "  \\* {<<\"a\", \"a\">>, <<\"a\", \"b\">>, <<\"b\", \"a\">>, <<\"b\", \"b\">>}"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "solution2": "hidden"
   },
   "outputs": [],
   "source": [
    "LET\n",
    "  Tup(S, n) == [1..n -> S]\n",
    "IN\n",
    "  Tup({1,2}, 3) = {1,2} \\X {1,2} \\X {1,2}"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Now write an operator that returns all sequences with a range in S of length n or less."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "solution2": "hidden",
    "solution2_first": true
   },
   "outputs": [],
   "source": [
    "LET\n",
    "  Sequ(S, n) == {1}\n",
    "IN\n",
    "  Sequ({\"a\", \"b\"}, 2)\n",
    "  \\* {<<\"a\">>, <<\"b\">>, <<\"a\", \"a\">>, <<\"a\", \"b\">>, <<\"b\", \"a\">>, <<\"b\", \"b\">>}"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "solution2": "hidden"
   },
   "outputs": [],
   "source": [
    "LET\n",
    "  Sequ(S, n) == UNION {[1..m -> S] : m \\in 1..n}\n",
    "IN\n",
    "  Sequ({1,2}, 2) = {1,2} \\X {1,2} \\union {<<1>>, <<2>>}"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## Using Functions"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "The TLC module provides a “Sort” operator, which takes a sequence of numbers and returns, surprisingly enough, the sorted sequence. This is done in the implementation layer, though, because sorting with the TLA tools is surprisingly tricky.\n",
    "\n",
    "First, write an operator that determines if a sequence is sorted or not."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "solution2": "hidden",
    "solution2_first": true
   },
   "outputs": [],
   "source": [
    "LET\n",
    "  IsSorted(T) == FALSE\n",
    "IN\n",
    "  IsSorted(<<1, 5, 7>>)\n",
    "  \\* TRUE"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "solution2": "hidden"
   },
   "outputs": [],
   "source": [
    "LET\n",
    "  IsSorted(T) == \\A x \\in 1..Len(T):\n",
    "                   \\A y \\in x..Len(T):\n",
    "                     T[x] <= T[y]  \n",
    "IN\n",
    "  /\\ IsSorted(<<1,2>>) = TRUE\n",
    "  /\\ IsSorted(<<1,1>>) = TRUE\n",
    "  /\\ IsSorted(<<1,5,7,5>>) = FALSE\n",
    "  /\\ IsSorted(<<2,1>>) = FALSE\n",
    "  /\\ IsSorted(<<1,5,7>>) = TRUE"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Next, we’ll need a concept of permuting a sequence. The easiest way to that is to first create a permutation of its domain, and then map that over the original sequence. Start by writing an operator that takes some number n and returns all permutations of `<<1, 2, ..., n>>`."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "solution2": "hidden",
    "solution2_first": true
   },
   "outputs": [],
   "source": [
    "LET\n",
    "  Range(T) == { T[x] : x \\in DOMAIN T }\n",
    "\n",
    "  PermutationKey(n) == {<<1, 2>>}\n",
    "IN\n",
    "  PermutationKey(2)\n",
    "  \\* {<<1, 2>>, <<2, 1>>}"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "solution2": "hidden"
   },
   "outputs": [],
   "source": [
    "LET\n",
    "  Range(T) == { T[x] : x \\in DOMAIN T }\n",
    "\n",
    "  PermutationKey(n) == {key \\in [1..n -> 1..n] : Range(key) = 1..n}\n",
    "IN\n",
    "  /\\ PermutationKey(2) = {<<1, 2>>, <<2, 1>>}\n",
    "  /\\ PermutationKey(5) = Permutations(1..5)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Next, write an operator that takes a sequence and returns the corresponding permuted sequences."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "solution2": "hidden",
    "solution2_first": true
   },
   "outputs": [],
   "source": [
    "LET\n",
    "  Range(T) == { T[x] : x \\in DOMAIN T }\n",
    "\n",
    "  PermutationsOf(T) == {<<\"a\", \"b\">>}\n",
    "IN\n",
    "  PermutationsOf(<<\"a\", \"b\">>)\n",
    "  \\* {<<\"a\", \"b\">>, <<\"b\", \"a\">>}"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "solution2": "hidden"
   },
   "outputs": [],
   "source": [
    "LET\n",
    "  Range(T) == { T[x] : x \\in DOMAIN T }\n",
    "  PermutationKey(n) == {key \\in [1..n -> 1..n] : Range(key) = 1..n}\n",
    "\n",
    "  PermutationsOf(T) == { [x \\in 1..Len(T) |-> T[P[x]]] : P \\in PermutationKey(Len(T))}\n",
    "IN\n",
    "  PermutationsOf(<<\"a\",\"b\">>) = {<<\"a\", \"b\">>, <<\"b\", \"a\">>}"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Now write an operator that takes a sequence and returns the sorted sequence."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "solution2": "hidden",
    "solution2_first": true
   },
   "outputs": [],
   "source": [
    "LET\n",
    "  Sort(T) == <<1, 2, 3>>\n",
    "IN\n",
    "  Sort(<<1, 5, 7, 5>>)\n",
    "  \\* <<1, 5, 5, 7>>"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "solution2": "hidden"
   },
   "outputs": [],
   "source": [
    "LET\n",
    "  Range(T) == { T[x] : x \\in DOMAIN T }\n",
    "  IsSorted(T) == \\A x \\in 1..Len(T):\n",
    "                   \\A y \\in x..Len(T):\n",
    "                     T[x] <= T[y]  \n",
    "  PermutationKey(n) == {key \\in [1..n -> 1..n] : Range(key) = 1..n}\n",
    "  PermutationsOf(T) == { [x \\in 1..Len(T) |-> T[P[x]]] : P \\in PermutationKey(Len(T))}\n",
    "  Sort(T) == CHOOSE sorted_tuple \\in PermutationsOf(T) : IsSorted(sorted_tuple)\n",
    "IN\n",
    "  Sort(<<1,5,7,5>>) = <<1, 5, 5, 7>>"
   ]
  }
 ],
 "metadata": {
  "celltoolbar": "Hide code",
  "kernelspec": {
   "display_name": "TLA⁺",
   "language": "tla",
   "name": "tlaplus_jupyter"
  },
  "language_info": {
   "codemirror_mode": "tlaplus",
   "file_extension": ".tla",
   "mimetype": "text/x-tlaplus",
   "name": "tlaplus"
  }
 },
 "nbformat": 4,
 "nbformat_minor": 4
}