cookbook:folding

We have the list `xs = [ 1,3,2 ]`

.
We are interested in the sum of these list elements.
A solution for this problem is the following function:

func sum(val xs: [nat]) -> nat = |[ var s: nat = 0 :: len(xs) > 0 *> ( s:= s + hd(xs); xs:= tl(xs) ) ; ret s ]|

Initially the sum `s`

equals zero.
As long as the list contains an element, we perform the addition
of the sum until so far and the head of the list.
We update the list by removing the head of the list, and we start the loop.

We can use this function in the following process fragment:

|[ var xs: [nat] = [ 1,3,2 ], s: nat, ... :: ... ; s:= sum(xs) // the result will be 6 ; ... ]|

The above specification of function `sum`

is a so called iterative
solution of the problem. Another way of specification is in a recursive way:

func sum(val xs: [nat]) -> nat = |[ var s: nat = 0 :: ( len(xs) = 0 -> ret 0 | len(xs) > 0 -> ret hd(xs) + sum(tl(xs)) ) ]|

Again the result will be 6. A snapshot of the execution of the specification is:

sum([1,3,2]) = 1 + sum([3,2]) = 1 + 3 + sum([2]) = 1 + 3 + 2 + sum([]) = 1 + 3 + 2 + 0 = 6

And still another way is by folding:

|[ var xs: [nat] = [1,3,2], s: nat, ... :: ... ; s:= ( +, x <- xs, x) ; ... ]|

The pronunciation of this fragment is:
“add elements `x`

, whereby `x`

is drawn from list `xs`

”.
The elements 1,3,2 are drawn form the list `xs`

.
The elements are added by the plus (`+`

) operator.
The final result will be 6.

Another example of folding is the following.
We are interested in the sum of all odd elements of list `xs`

.
The specification is:

|[ var xs: [nat] = [1,3,2], s: nat, ... :: ... ; s:= ( +, x <- xs, x mod 2 > 0, x) ; ... ]|

The result will be 4, as 1 and 3 are odd elements.
In this case we are using a filter `x mod 2 > 0`

to consider only those elements that fulfill the condition.

Another example delivers the sum of the square numbers of the list `xs`

.
We have:

|[ var xs: [nat] = [1,3,2], s: nat, ... :: ... ; s:= ( +, x <- xs, x * x) ; ... ]|

Another way of writing is by using a function `f`

.
This function maps the variable on the value:

func f(val x: nat) -> nat = |[ ret x * x ]|

We have for the last example the following fragment:

|[ var xs: [nat] = [1,3,2], s: nat, ... :: ... ; s:= ( +, x <- xs, f(x)) ; ... ]|

So far examples based on the operator `+`

.

It is also possible to use a multiply operator.
As an example we want to calculate the factorial (`n!`

) of a number.
The factorial of a number is
`fac(n) = n(n -1)(n - 2) … 1`

.
So:
`fac(3) = 3 . 2 . 1 = 6`

, and
`fac(5) = 5 . 4 . 3 . 2 . 1 = 120`

.
In a traditional manner we have the following function:

function fac(val n: nat) -> nat = |[ var k: nat = n, p: nat = n :: k > 1 *> ( k:= k - 1; p:= p * k ) ; ret p ]|

Or in an recursive manner:

function fac(val n: nat) -> nat = |[ ( n > 1 -> ret n * fac(n - 1) | n = 1 -> ret 1 ) ]|

Or using folding:

function fac(val n: nat) -> nat = |[ ret ( * , m <- 1 .. n, m) ]|

Note we use the construct `1..n`

to generate the numbers 1,2, …, n.

It is also possible to use max operator `max`

or
min operator `min`

. An example:

|[ var xs: [nat] = [1,3,2], s,t: nat, ... :: ... ; s:= ( max, x <- xs, x * x) ; t:= ( min, x <- xs, x) ; ... ]|

in this case the result of `s`

will become 9,
and `t`

will become 1.

We have the concatenation operator. This operator adds (glues) elements into one new list. An example:

|[ var xs: [nat] = [1,3,2], ys: [nat], ... :: ... ; ys:= ( ++ , x <- xs, [ 2 * x ]) ; ... ]|

Every element of `xs`

is multiplied by two, and glued into a new list
`ys`

. In this case the value of `ys`

will become `[2,6,4]`

.

We assume that `xs`

is a list with tuple elements of type
`(nat,nat)`

. The first elements is the identifier, the second
number is the number of parcel of an item.
And we are interested in the total number of parcel of the even item numbers.
We find:

|[ var xs: [(nat,nat)] = [(1,10),(2,12),(3,16),(6,17)], s: nat, ... :: ... ; s:= ( + , x < xs, x.0 mod 2 = 0, x.1) ; ... ]|

Folding in sets

As an example we have the set {1,3,2}. The sum of these three set elements can be obtained by:

|[ var xr: {nat} = {1,3,2}, s: nat, ... :: ... ; s:= ( +, x <- xr, x ) ; ... ]|

Folding in sets is similar to folding in lists.
In general we use suffix `r`

to denote sets (and suffix `s`

to denote lists), so we have `xr`

and `xs`

.

cookbook/folding.txt · Last modified: Thursday, 12 February 2009 : 09:50:10 by hvrooy

Except where otherwise noted, content on this wiki is licensed under the following license: CC Attribution-Noncommercial-Share Alike 4.0 International