User Tools

Site Tools


cookbook:folding

Folding in lists (and sets)

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

Folding

Adding

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 +.

Multiplying

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.

Max and min

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.

Concatenation

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)
 ; ...
]|

Sets

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