Back
Close

Functional Modelling System

IngmarDasseville
5,122 views

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
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
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
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
s :: subset of {1..10}.
count s = 4.
sum s = 16.
XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX
Create your playground on Tech.io
This playground was created on Tech.io, our hands-on, knowledge-sharing platform for developers.
Go to tech.io
codingame x discord
Join the CodinGame community on Discord to chat about puzzle contributions, challenges, streams, blog articles - all that good stuff!
JOIN US ON DISCORD
Online Participants