Skip to content
Snippets Groups Projects
Commit 267b3908 authored by Michael Leuschel's avatar Michael Leuschel
Browse files

update notebook

parent f65443f6
Branches
Tags
No related merge requests found
%% Cell type:markdown id: tags:
# Functional Programming in B #
%% Cell type:markdown id: tags:
Some functions are automatically detected as infinite by ProB, are kept symbolic but can be applied in several ways:
For example, you can apply the function and compute the relational image:
%% Cell type:code id: tags:
``` prob
f = %x.(x:INTEGER|x*x) &
r1 = f(100000) &
r2 = f[1..10]
```
%% Output
$TRUE$
**Solution:**
* $r2 = \{1,4,9,16,25,36,49,64,81,100\}$
* $f = \lambdax\qdot(x \in INTEGER\midx * x)$
* $r1 = 10000000000$
TRUE
Solution:
r2 = {1,4,9,16,25,36,49,64,81,100}
f = λx·(x ∈ INTEGER∣x ∗ x)
r1 = 10000000000
%% Cell type:markdown id: tags:
You can map the function over a sequence using the relational composition:
%% Cell type:code id: tags:
``` prob
f = %x.(x:INTEGER|x*x) &
r3 = ([2,3,5,7,11] ; f)
```
%% Output
$TRUE$
**Solution:**
* $r3 = [4,9,25,49,121]$
* $f = \lambdax\qdot(x \in INTEGER\midx * x)$
TRUE
Solution:
r3 = [4,9,25,49,121]
f = λx·(x ∈ INTEGER∣x ∗ x)
%% Cell type:markdown id: tags:
You can iterate the function using the iterate construct:
%% Cell type:code id: tags:
``` prob
f = %x.(x:INTEGER|x*x) &
r4 = iterate(f,3)(2)
```
%% Output
$TRUE$
**Solution:**
* $r4 = 256$
* $f = \lambdax\qdot(x \in INTEGER\midx * x)$
TRUE
Solution:
r4 = 256
f = λx·(x ∈ INTEGER∣x ∗ x)
%% Cell type:markdown id: tags:
You can even use the function for constraint solving:
%% Cell type:code id: tags:
``` prob
f = %x.(x:INTEGER|x*x) &
f(sqrt) = 100
```
%% Output
$TRUE$
**Solution:**
* $sqrt = 10$
* $f = \lambdax\qdot(x \in INTEGER\midx * x)$
TRUE
Solution:
sqrt = 10
f = λx·(x ∈ INTEGER∣x ∗ x)
%% Cell type:markdown id: tags:
Let us use a more complicated function which is not obviously infinite:
%% Cell type:code id: tags:
``` prob
f = {x,y|x:NATURAL & y**2 >= x & (y-1)**2 <x } & // integer square root function
r1 = f(100000)
```
%% Output
$TRUE$
**Solution:**
* $f = \{x,y\midx \in NATURAL \land y \cprod 2 \geq x \land (y - 1) \cprod 2 < x\}$
* $r1 = 317$
TRUE
Solution:
f = {x,y∣x ∈ NATURAL ∧ y × 2 ≥ x ∧ (y − 1) × 2 < x}
r1 = 317
%% Cell type:markdown id: tags:
You can use the symbolic pragma so that ProB does not try to expand the function:
%% Cell type:code id: tags:
``` prob
f = /*@symbolic*/ {x,y|x:NATURAL & y**2 >= x & (y-1)**2 <x } & // integer square root function
r1 = f(100000) &
r2 = f[1..10] &
r3 = ([2,3,5,7,11] ; f) &
r4 = iterate(f,3)(2) &
f(sqr) = 100
```
%% Output
$TRUE$
**Solution:**
* $r2 = \{1,2,3,4\}$
* $r3 = [2,2,3,3,4]$
* $r4 = 2$
* $sqr = 9802$
* $f = \{x,y\midx \in NATURAL \land y \cprod 2 \geq x \land (y - 1) \cprod 2 < x\}$
* $r1 = 317$
TRUE
Solution:
r2 = {1,2,3,4}
r3 = [2,2,3,3,4]
r4 = 2
sqr = 9802
f = {x,y∣x ∈ NATURAL ∧ y × 2 ≥ x ∧ (y − 1) × 2 < x}
r1 = 317
%% Cell type:markdown id: tags:
We can also use the transitive closure of the function and apply it:
%% Cell type:code id: tags:
``` prob
f = /*@symbolic*/ {x,y|x:NATURAL & y**2 >= x & (y-1)**2 <x } & // integer square root function
r5 = closure1(f)[{10000}]
```
%% Output
$TRUE$
**Solution:**
* $r5 = \{2,4,10,100\}$
* $f = \{x,y\midx \in NATURAL \land y \cprod 2 \geq x \land (y - 1) \cprod 2 < x\}$
TRUE
Solution:
r5 = {2,4,10,100}
f = {x,y∣x ∈ NATURAL ∧ y × 2 ≥ x ∧ (y − 1) × 2 < x}
%% Cell type:markdown id: tags:
We can visualize the result of the function for some values:
%% Cell type:code id: tags:
``` prob
:table {x,isqrt|x:1..16 & isqrt**2 >= x & (isqrt-1)**2 <x }
```
%% Output
|Nr|x|isqrt|
|---|---|---|
|1|1|1|
|2|2|2|
|3|3|2|
|4|4|2|
|5|5|3|
|6|6|3|
|7|7|3|
|8|8|3|
|9|9|3|
|10|10|4|
|11|11|4|
|12|12|4|
|13|13|4|
|14|14|4|
|15|15|4|
|16|16|4|
Nr x isqrt
1 1 1
2 2 2
3 3 2
4 4 2
5 5 3
6 6 3
7 7 3
8 8 3
9 9 3
10 10 4
11 11 4
12 12 4
13 13 4
14 14 4
15 15 4
16 16 4
%% Cell type:code id: tags:
``` prob
:prettyprint f = %x.(x:INTEGER|x*x) &
r1 = f(100000) &
r2 = f[1..10]
```
%% Output
$\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]$
f = λx.(x ∈ ℤ|x * x) ∧ r1 = f(100000) ∧ r2 = f[1 ‥ 10]
%% Cell type:code id: tags:
``` prob
```
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment