Functional Modelling System

IngmarDasseville
3,155 views

Open Source Your Knowledge, Become a Contributor

Technology knowledge has to be shared and made accessible for free. Join the movement.

Create Content

Sets

The set constructs are the last fundamental part of the language. Up to now we have only encountered enumerations like {"a","c"} and ranges like {1..5}.

IDP4 supports more advanced set expressions. In a set you can write down a double pipe || and after that you can write a number of different things:

  • a <- s, picks a new variable a out of a set. This variable can then be used in the members of the set. It behaves a lot like a for-loop. {2*a || a <- s} contains the double of all the elements of a set s.
  • a < 5, any Boolean expression is seen as a guard that limits the content of the set. {a || a <- s, a < 5} is the set containing of all numbers in s which are smaller than 5.
  • a := 8, behaves like a local let expression, {a || a := 8} is the singleton set of 8.
Sets
1
2
3
4
5
6
7
8
9
10
11
12
s1 := {1,2,3,5}.
//Applying a function to every element of a set
s2 := {x*2 || x <- s1}.
//Filtering only the elements which satisfy a certain property
s3 := {x || x <- s2, x < 5}.
//Defining an intermediate symbol s.
s4 := {y, y + 100 || x <- s3, y := x + 2}.
relevant {s1, s2, s3, s4}.
XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX

Note that these expressions are order dependent, as you can use the variables introduced in one expression in the next one. Look for at example at a definition of union

Sets
1
2
3
4
5
6
7
8
9
s1 := {1,2,3}.
s2 := {3,4,5}.
myUnion # noprint.
myUnion a b := {x || s <- {a,b}, x <- s}.
s3 := myUnion s1 s2.
relevant {s1,s2,s3}.
XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX

When you take the union of 2 sets a and b this can be done through first selecting a set s out of the two. And then taking all elements x in this set.

Builtins

There are a few builtins over sets predefined.

  • quantifiers: forall (!) and exists (?)
  • member: membership test
  • count: returns the cardinality of a set
  • sum : returns the sum of the members of a set
  • sumBy : returns the sum of the members of a set based on the result of a function
  • min: returns the minimum of the members of a set
  • max: returns the maximum of the members of a set
Set Builtins
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
s := {1,2,3}.
//is true iff 2 is an element of s
memberTest1 := member 2 s.
//is true iff 5 is an element of s
memberTest2 := member 5 s.
//is true iff all elements of s are smaller than 4
memberTest3 := ! s (\x -> x < 4).
//is true iff any element of s is larger than 2
memberTest4 := ? s (\x -> x > 2).
three := count s.
six := sum s.
//for every element of s, add a 3 true to the sum
nine := sumBy (\x -> 3) s.
mini := min s.
maxi := max s.
relevant {memberTest1, memberTest2, memberTest3, memberTest4}.
relevant {three, six, nine, mini, maxi}.
XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX

The other way around

Just like element of you can declare a symbol subset of and let IDP4 search for a set.

Uninterpreted Set
1
2
3
4
s :: subset of {1..10}.
count s = 4.
sum s = 16.
XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX
Open Source Your Knowledge: become a Contributor and help others learn. Create New Content