 Home Libraries People FAQ More

## Semantics

Orderings and Equivalences
Sets
Maps
Collectors: Maps of Sets
Quantifiers: Maps of Numbers
Concept Induction

Beauty is the ultimate defense against complexity” -- David Gelernter

In the itl we follow the notion, that the semantics of a concept or abstract data type can be expressed by laws. We formulate laws over interval containers that can be evaluated for a given instantiation of the variables contained in the law. The following pseudocode gives a shorthand notation of such a law.

```Commutativity<T,+>:
T a, b; a + b == b + a;
```

This can of course be coded as a proper c++ class template which has been done for the validation of the itl. For sake of simplicity we will use pseudocode here.

The laws that describe the semantics of the itl's class templates were validated using the Law based Test Automaton LaBatea, a tool that generates instances for the law's variables and then tests it's validity. Since the itl deals with sets, maps and relations, that are well known objects from mathematics, the laws that we are using are mostly recycled ones. Also some of those laws are grouped in notions like e.g. orderings or algebras.

### Orderings and Equivalences

##### Lexicographical Ordering and Equality

On all set and map containers of the itl, there is an ```operator <``` that implements a strict weak ordering.

The semantics of `operator <` is the same as for an stl's SortedAssociativeContainer, specifically stl::set and stl::map:

```Irreflexivity<T,< > : T a;     !(a<a)
Asymmetry<T,< >     : T a,b;   a<b implies !(b<a)
Transitivity<T,< >  : T a,b,c; a<b && b<c implies a<c
```

`Operator <` depends on the itl::container's template parameter `Compare` that implements a strict weak ordering for the container's `domain_type`. For a given `Compare` ordering, `operator <` implements a lexicographical comparison on itl::containers, that uses the `Compare` order to establish a unique sequence of values in the container.

The induced equivalence of ```operator <``` is lexicographical equality which is implemented as `operator ==`.

```//equivalence induced by strict weak ordering <
!(a<b) && !(b<a) implies a == b;
```

Again this follows the semantics of the stl. Lexicographical equality is stronger than the equality of elements. Two containers that contain the same elements can be lexicographically unequal, if their elements are differently sorted. Lexicographical comparison belongs to the segmental aspect. Of all the different sequences that are valid for unordered sets and maps, one such sequence is selected by the `Compare` order of elements. Based on this selection a unique iteration is possible.

##### Subset Ordering and Element Equality

On the fundamental aspect only membership of elements matters, not their sequence. So there are functions `contained_in` and `element_equal` that implement the subset relation and the equality on elements. Yet, `contained_in` and `is_element_equal` functions are not really working on the level of elements. They also work on the basis of the containers templates `Compare` parameter. In practical terms we need to distinguish between lexicographical equality `operator ==` and equality of elements `is_element_equal`, if we work with interval splitting interval containers:

```split_interval_set<time> w1, w2; //Pseudocode
w1 = {[Mon       ..       Sun)}; //split_interval_set containing a week
w2 = {[Mon .. Fri)[Sat .. Sun)}; //Same week split in work and week end parts.
w1 == w2;                        //false: Different segmentation
is_element_equal(w1,w2);         //true:  Same elements contained
```

For a constant `Compare` order on key elements, member function `contained_in` that is defined for all itl::containers implements a partial order on itl::containers.

```with <= for contained_in,
=e= for is_element_equal:
Reflexivity<T,<= >     : T a;     a <= a
Antisymmetry<T,<=,=e=> : T a,b;   a <= b && b <= a implies a =e= b
Transitivity<T,<= >    : T a,b,c; a <= b && b <= c implies a <= c
```

The induced equivalence is the equality of elements that is implemented via function `is_element_equal`.

```//equivalence induced by the partial ordering contained_in on itl::container a,b
a.contained_in(b) && b.contained_in(a) implies is_element_equal(a, b);
```