add FP notebook

notebooks/tutorials/Functional_Programming_in_B.ipynb

+{
+ "cells": [
+  {
+   "cell_type": "markdown",
+   "metadata": {},
+   "source": [
+    "# Functional Programming in B #"
+   ]
+  },
+  {
+   "cell_type": "markdown",
+   "metadata": {},
+   "source": [
+    "Some functions are automatically detected as infinite by ProB, are kept symbolic but can be applied in several ways:\n",
+    "For example, you can apply the function and compute the relational image:\n"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 6,
+   "metadata": {},
+   "outputs": [
+    {
+     "data": {
+      "text/plain": [
+       "TRUE\n",
+       "\n",
+       "Solution:\n",
+       "\tr2 = {1,4,9,16,25,36,49,64,81,100}\n",
+       "\tf = λx·(x ∈ INTEGER∣x ∗ x)\n",
+       "\tr1 = 10000000000"
+      ]
+     },
+     "execution_count": 6,
+     "metadata": {},
+     "output_type": "execute_result"
+    }
+   ],
+   "source": [
+    "f = %x.(x:INTEGER|x*x) &\n",
+    "r1 = f(100000) &\n",
+    "r2 = f[1..10] "
+   ]
+  },
+  {
+   "cell_type": "markdown",
+   "metadata": {},
+   "source": [
+    "You can map the function over a sequence using the relational composition:"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 7,
+   "metadata": {},
+   "outputs": [
+    {
+     "data": {
+      "text/plain": [
+       "TRUE\n",
+       "\n",
+       "Solution:\n",
+       "\tr3 = [4,9,25,49,121]\n",
+       "\tf = λx·(x ∈ INTEGER∣x ∗ x)"
+      ]
+     },
+     "execution_count": 7,
+     "metadata": {},
+     "output_type": "execute_result"
+    }
+   ],
+   "source": [
+    "f = %x.(x:INTEGER|x*x) &\n",
+    "r3 = ([2,3,5,7,11] ; f)"
+   ]
+  },
+  {
+   "cell_type": "markdown",
+   "metadata": {},
+   "source": [
+    "You can iterate the function using the iterate construct:"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 8,
+   "metadata": {},
+   "outputs": [
+    {
+     "data": {
+      "text/plain": [
+       "TRUE\n",
+       "\n",
+       "Solution:\n",
+       "\tr4 = 256\n",
+       "\tf = λx·(x ∈ INTEGER∣x ∗ x)"
+      ]
+     },
+     "execution_count": 8,
+     "metadata": {},
+     "output_type": "execute_result"
+    }
+   ],
+   "source": [
+    "f = %x.(x:INTEGER|x*x) &\n",
+    "r4 = iterate(f,3)(2)"
+   ]
+  },
+  {
+   "cell_type": "markdown",
+   "metadata": {},
+   "source": [
+    "You can even use the function for constraint solving:"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 9,
+   "metadata": {},
+   "outputs": [
+    {
+     "data": {
+      "text/plain": [
+       "TRUE\n",
+       "\n",
+       "Solution:\n",
+       "\tsqrt = 10\n",
+       "\tf = λx·(x ∈ INTEGER∣x ∗ x)"
+      ]
+     },
+     "execution_count": 9,
+     "metadata": {},
+     "output_type": "execute_result"
+    }
+   ],
+   "source": [
+    "f = %x.(x:INTEGER|x*x) &\n",
+    "f(sqrt) = 100"
+   ]
+  },
+  {
+   "cell_type": "markdown",
+   "metadata": {},
+   "source": [
+    "Let us use a more complicated function which is not obviously infinite:"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 10,
+   "metadata": {},
+   "outputs": [
+    {
+     "name": "stdout",
+     "output_type": "stream",
+     "text": [
+      "[2018-06-06 09:48:30,643, T+626136] \"ProB Output Logger for instance 23eee4b8\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] VIRTUAL TIME-OUT caused by: ### Warning: enumerating NATURAL(1) : NATURAL(1) : 1:sup ---> 1:3\u001b[0m\n"
+     ]
+    },
+    {
+     "data": {
+      "text/plain": [
+       "TRUE\n",
+       "\n",
+       "Solution:\n",
+       "\tf = {x,y∣x ∈ NATURAL ∧ y × 2 ≥ x ∧ (y − 1) × 2 < x}\n",
+       "\tr1 = 317"
+      ]
+     },
+     "execution_count": 10,
+     "metadata": {},
+     "output_type": "execute_result"
+    }
+   ],
+   "source": [
+    "f = {x,y|x:NATURAL & y**2 >= x & (y-1)**2 <x } & // integer square root function\n",
+    "r1 = f(100000) "
+   ]
+  },
+  {
+   "cell_type": "markdown",
+   "metadata": {},
+   "source": [
+    "You can use the symbolic pragma so that ProB does not try to expand the function:"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 13,
+   "metadata": {},
+   "outputs": [
+    {
+     "data": {
+      "text/plain": [
+       "TRUE\n",
+       "\n",
+       "Solution:\n",
+       "\tr2 = {1,2,3,4}\n",
+       "\tr3 = [2,2,3,3,4]\n",
+       "\tr4 = 2\n",
+       "\tsqr = 9802\n",
+       "\tf = {x,y∣x ∈ NATURAL ∧ y × 2 ≥ x ∧ (y − 1) × 2 < x}\n",
+       "\tr1 = 317"
+      ]
+     },
+     "execution_count": 13,
+     "metadata": {},
+     "output_type": "execute_result"
+    }
+   ],
+   "source": [
+    "f = /*@symbolic*/ {x,y|x:NATURAL & y**2 >= x & (y-1)**2 <x } & // integer square root function\n",
+    "r1 = f(100000) &\n",
+    "r2 = f[1..10] &\n",
+    "r3 = ([2,3,5,7,11] ; f) &\n",
+    "r4 = iterate(f,3)(2) &\n",
+    "f(sqr) = 100"
+   ]
+  },
+  {
+   "cell_type": "markdown",
+   "metadata": {},
+   "source": [
+    "We can also use the transitive closure of the function and apply it:"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 12,
+   "metadata": {},
+   "outputs": [
+    {
+     "data": {
+      "text/plain": [
+       "TRUE\n",
+       "\n",
+       "Solution:\n",
+       "\tr5 = {2,4,10,100}\n",
+       "\tf = {x,y∣x ∈ NATURAL ∧ y × 2 ≥ x ∧ (y − 1) × 2 < x}"
+      ]
+     },
+     "execution_count": 12,
+     "metadata": {},
+     "output_type": "execute_result"
+    }
+   ],
+   "source": [
+    "f = /*@symbolic*/ {x,y|x:NATURAL & y**2 >= x & (y-1)**2 <x } & // integer square root function\n",
+    "r5 = closure1(f)[{10000}]"
+   ]
+  },
+  {
+   "cell_type": "markdown",
+   "metadata": {},
+   "source": [
+    "We can visualize the result of the function for some values:"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 5,
+   "metadata": {},
+   "outputs": [
+    {
+     "data": {
+      "text/markdown": [
+       "|Nr|x|isqrt|\n",
+       "|---|---|---|\n",
+       "|1|1|1|\n",
+       "|2|2|2|\n",
+       "|3|3|2|\n",
+       "|4|4|2|\n",
+       "|5|5|3|\n",
+       "|6|6|3|\n",
+       "|7|7|3|\n",
+       "|8|8|3|\n",
+       "|9|9|3|\n",
+       "|10|10|4|\n",
+       "|11|11|4|\n",
+       "|12|12|4|\n",
+       "|13|13|4|\n",
+       "|14|14|4|\n",
+       "|15|15|4|\n",
+       "|16|16|4|\n"
+      ],
+      "text/plain": [
+       "Nr\tx\tisqrt\n",
+       "1\t1\t1\n",
+       "2\t2\t2\n",
+       "3\t3\t2\n",
+       "4\t4\t2\n",
+       "5\t5\t3\n",
+       "6\t6\t3\n",
+       "7\t7\t3\n",
+       "8\t8\t3\n",
+       "9\t9\t3\n",
+       "10\t10\t4\n",
+       "11\t11\t4\n",
+       "12\t12\t4\n",
+       "13\t13\t4\n",
+       "14\t14\t4\n",
+       "15\t15\t4\n",
+       "16\t16\t4\n"
+      ]
+     },
+     "execution_count": 5,
+     "metadata": {},
+     "output_type": "execute_result"
+    }
+   ],
+   "source": [
+    ":table {x,isqrt|x:1..16 & isqrt**2 >= x & (isqrt-1)**2 <x }"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": null,
+   "metadata": {},
+   "outputs": [],
+   "source": []
+  }
+ ],
+ "metadata": {
+  "kernelspec": {
+   "display_name": "ProB 2",
+   "language": "prob",
+   "name": "prob2"
+  },
+  "language_info": {
+   "file_extension": ".prob",
+   "mimetype": "text/x-prob",
+   "name": "prob"
+  }
+ },
+ "nbformat": 4,
+ "nbformat_minor": 2
+}