| Both sides previous revision Previous revision Next revision | Previous revision |
| using:standard_lib [2024/10/09 12:55] – fponzi | using:standard_lib [2024/10/10 16:42] (current) – fponzi |
|---|
| The Sequences module defines operations on finite sequences. We represent a finite sequence as a tuple, so the sequence of three numbers 3, 2, 1 is the triple <<3, 2, 1>>. The Sequences module defines the following operators on sequences: | The Sequences module defines operations on finite sequences. We represent a finite sequence as a tuple, so the sequence of three numbers 3, 2, 1 is the triple <<3, 2, 1>>. The Sequences module defines the following operators on sequences: |
| * ''s \o t'': The sequence obtained by concatenating the sequences s and t. | * ''s \o t'': The sequence obtained by concatenating the sequences s and t. |
| * Example: ''<<3, 7>> \o <<3>>'' equals ''<<3, 7, 3>>''. | * Example: ''<<3, 7>> \o <<3>>'' is equal to ''<<3, 7, 3>>''. |
| * ''Head'' | * ''Head(s)'': The first element of the sequence s. |
| * ''SelectSeq'' | * Example: ''Head(<<3,2,1>>)'' is equal to ''3'' |
| * ''SubSeq'' | * ''SelectSeq(s, Test)'': The subsequence of s consisting of the elements s[i] such that Test(s[i]) equals true. |
| * ''Append'' | * Example: <code latex>PosSubSeq(s) == LET IsPos(n) == n > 0 |
| * ''Len'' | in SelectSeq(s, IsPos)</code> defines ''PosSubSeq(<<0, 3, −2, 5>>)'' to be equal to ''<<3, 5>>'' |
| * ''Seq'' | * ''SubSeq(s, m, n)'': The subsequence ''<<s[m], s[m + 1], . . . , s[n]>>'' consisting of the mth through nth elements of s. It is undefined if ''m < 1'' or ''n > Len(s)'', except that it equals the empty sequence if ''m > n''. |
| * ''Tail'' | * ''Append(s, e)'': The sequence obtained by appending element e to the tail of sequence s. |
| | * Example: ''Append(<<3, 7>>, 3)'' equals ''<<3, 7, 3>>''. |
| | * ''Len(s)'': The length of sequence s. |
| | * Example: ''Len(<<1,2,3>>)'' is equal to ''3''. |
| | * ''Seq(S)'': The set of all sequences of elements of the set S . |
| | * Example: ''Seq({3,7})'' is equal to ''<<3, 7>>''. |
| | * ''Tail(s)'': The tail of sequence ''s'', which consists of ''s'' with its head element removed. |
| | * Example: ''Tail(<<3, 7>>)'' equals ''<<7>>''. |
| |
| ===== Module ''FiniteSets'' ===== | ===== Module ''FiniteSets'' ===== |
| |
| * ''IsFiniteSet'' | * ''IsFiniteSet(s)'': A set is finite iff there is a finite sequence containing all its elements. |
| * ''Cardinality'' | * Example: ''IsFiniteSet({1,2,3})'' is equal to ''TRUE'' |
| | * ''Cardinality(s)'': The number of elements in the set s. It's only defined for finite sets. |
| | * Example: ''Cardinality({1,2})'' is equal to 2. |
| |
| ===== Module ''Bags'' ===== | ===== Module ''Bags'' ===== |
fponzi