From 267b390813b09ad1f79f154d107f174ea2c5bb07 Mon Sep 17 00:00:00 2001
From: Michael Leuschel <leuschel@cs.uni-duesseldorf.de>
Date: Mon, 16 Jul 2018 10:00:38 +0200
Subject: [PATCH] update notebook
---
.../Functional_Programming_in_B.ipynb | 90 ++++++++++++++++++-
1 file changed, 88 insertions(+), 2 deletions(-)
diff --git a/notebooks/tutorials/Functional_Programming_in_B.ipynb b/notebooks/tutorials/Functional_Programming_in_B.ipynb
index c225131..c21b7f7 100644
--- a/notebooks/tutorials/Functional_Programming_in_B.ipynb
+++ b/notebooks/tutorials/Functional_Programming_in_B.ipynb
@@ -22,6 +22,14 @@
"outputs": [
{
"data": {
+ "text/markdown": [
+ "$TRUE$\n",
+ "\n",
+ "**Solution:**\n",
+ "* $r2 = \\{1,4,9,16,25,36,49,64,81,100\\}$\n",
+ "* $f = \\lambdax\\qdot(x \\in INTEGER\\midx * x)$\n",
+ "* $r1 = 10000000000$"
+ ],
"text/plain": [
"TRUE\n",
"\n",
@@ -56,6 +64,13 @@
"outputs": [
{
"data": {
+ "text/markdown": [
+ "$TRUE$\n",
+ "\n",
+ "**Solution:**\n",
+ "* $r3 = [4,9,25,49,121]$\n",
+ "* $f = \\lambdax\\qdot(x \\in INTEGER\\midx * x)$"
+ ],
"text/plain": [
"TRUE\n",
"\n",
@@ -88,6 +103,13 @@
"outputs": [
{
"data": {
+ "text/markdown": [
+ "$TRUE$\n",
+ "\n",
+ "**Solution:**\n",
+ "* $r4 = 256$\n",
+ "* $f = \\lambdax\\qdot(x \\in INTEGER\\midx * x)$"
+ ],
"text/plain": [
"TRUE\n",
"\n",
@@ -120,6 +142,13 @@
"outputs": [
{
"data": {
+ "text/markdown": [
+ "$TRUE$\n",
+ "\n",
+ "**Solution:**\n",
+ "* $sqrt = 10$\n",
+ "* $f = \\lambdax\\qdot(x \\in INTEGER\\midx * x)$"
+ ],
"text/plain": [
"TRUE\n",
"\n",
@@ -152,6 +181,13 @@
"outputs": [
{
"data": {
+ "text/markdown": [
+ "$TRUE$\n",
+ "\n",
+ "**Solution:**\n",
+ "* $f = \\{x,y\\midx \\in NATURAL \\land y \\cprod 2 \\geq x \\land (y - 1) \\cprod 2 < x\\}$\n",
+ "* $r1 = 317$"
+ ],
"text/plain": [
"TRUE\n",
"\n",
@@ -184,6 +220,17 @@
"outputs": [
{
"data": {
+ "text/markdown": [
+ "$TRUE$\n",
+ "\n",
+ "**Solution:**\n",
+ "* $r2 = \\{1,2,3,4\\}$\n",
+ "* $r3 = [2,2,3,3,4]$\n",
+ "* $r4 = 2$\n",
+ "* $sqr = 9802$\n",
+ "* $f = \\{x,y\\midx \\in NATURAL \\land y \\cprod 2 \\geq x \\land (y - 1) \\cprod 2 < x\\}$\n",
+ "* $r1 = 317$"
+ ],
"text/plain": [
"TRUE\n",
"\n",
@@ -224,6 +271,13 @@
"outputs": [
{
"data": {
+ "text/markdown": [
+ "$TRUE$\n",
+ "\n",
+ "**Solution:**\n",
+ "* $r5 = \\{2,4,10,100\\}$\n",
+ "* $f = \\{x,y\\midx \\in NATURAL \\land y \\cprod 2 \\geq x \\land (y - 1) \\cprod 2 < x\\}$"
+ ],
"text/plain": [
"TRUE\n",
"\n",
@@ -251,7 +305,7 @@
},
{
"cell_type": "code",
- "execution_count": 8,
+ "execution_count": 9,
"metadata": {},
"outputs": [
{
@@ -296,7 +350,7 @@
"16\t16\t4\n"
]
},
- "execution_count": 8,
+ "execution_count": 9,
"metadata": {},
"output_type": "execute_result"
}
@@ -304,6 +358,38 @@
"source": [
":table {x,isqrt|x:1..16 & isqrt**2 >= x & (isqrt-1)**2 <x }"
]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 10,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/latex": [
+ "$\\mathit{f} = \\lambda \\mathit{x}.(\\mathit{x} \\in \\mathbb Z \\mid \\mathit{x} * \\mathit{x}) \\wedge \\mathit{r1} = \\mathit{f}(100000) \\wedge \\mathit{r2} = \\mathit{f}[1 .. 10]$"
+ ],
+ "text/plain": [
+ "f = λx.(x ∈ ℤ|x * x) ∧ r1 = f(100000) ∧ r2 = f[1 ‥ 10]"
+ ]
+ },
+ "execution_count": 10,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":prettyprint f = %x.(x:INTEGER|x*x) &\n",
+ "r1 = f(100000) &\n",
+ "r2 = f[1..10] "
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": null,
+ "metadata": {},
+ "outputs": [],
+ "source": []
}
],
"metadata": {
--
GitLab