From b2e828b6395e29f0e2f1811ae48ac24567d8cd9a Mon Sep 17 00:00:00 2001
From: Michael Leuschel <leuschel@cs.uni-duesseldorf.de>
Date: Wed, 6 Jun 2018 09:50:35 +0100
Subject: [PATCH] add FP notebook
---
.../Functional_Programming_in_B.ipynb | 337 ++++++++++++++++++
1 file changed, 337 insertions(+)
create mode 100644 notebooks/tutorials/Functional_Programming_in_B.ipynb
diff --git a/notebooks/tutorials/Functional_Programming_in_B.ipynb b/notebooks/tutorials/Functional_Programming_in_B.ipynb
new file mode 100644
index 0000000..9d48341
--- /dev/null
+++ b/notebooks/tutorials/Functional_Programming_in_B.ipynb
@@ -0,0 +1,337 @@
+{
+ "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
+}
--
GitLab