123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133134135136137138139140141142143144145146147148149150151152153154155156157158159160161162163164165166167168169170171172173174175176177178179180181182183184185186187188189190191192193194195196197198199200201202203204205206207208209210211212213214215216217218219220221222223224225226227228229230231232233234235236237238239240241242243244245246247248249250251252253254255256257258259260261262263264265266267268269270271272273274275276277278279280281282283284285286287288289290291292293294295296297298299300301302303304305306307308309310311312313314315316317318319320321322323324325326327328329330331332333334335336337338339340341342343344345346347348349350351352353354355356357358359360361362363364365366367368369370371372373374375376377378379380381382383384385386387388389390391392393394395396397398399400401402403404405406407408409410411412413414415416417418419420421422423424425426427428429430431432433434435436437438439440441442443444445446447448449450451452453454455456457458459460461462463464465466467468469470471472473474475476477478479480481482483484485486487488489490491492493494495496497498499500501502503504505506507508509510511512513514515516517518519520521522523524525526527528529530531532533534535536537538539540541542543544545546547548549550551552553554555556557558559560561562563564565566567568569570571572573574575576577578579580581582583584585586587588589590591592593594595596597598599600601602603604605606607608609610611612613614615616617618619620621622623624625626627628629630631632633634635636637638639640641642643644645646647648649650651652653654655656657658659660661662663664665666667668669670671672673674675676677678679680681682683684685686687688689690691692693694695696697698699700701702703704705706707708709710711712713714715716717718719720721722723724725726727728729730731732733734735736737738739740741742743744745746747748749750751752753754755756757758759760 |
- [/
- Copyright (c) 2008-2009 Joachim Faulhaber
- Distributed under the Boost Software License, Version 1.0.
- (See accompanying file LICENSE_1_0.txt or copy at
- http://www.boost.org/LICENSE_1_0.txt)
- ]
- [section Semantics]
- ["Beauty is the ultimate defense against complexity] -- [/David Gelernter]
- [@http://en.wikipedia.org/wiki/David_Gelernter David Gelernter]
- In the *icl* 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 *icl*. For sake of simplicity
- we will use pseudocode here.
- The laws that describe the semantics of the *icl'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 *icl* 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/.
- [section Orderings and Equivalences]
- [h4 Lexicographical Ordering and Equality]
- On all set and map containers of the icl, there is an `operator <`
- that implements a
- [@http://www.sgi.com/tech/stl/StrictWeakOrdering.html strict weak ordering].
- [/ (see also [@http://en.wikipedia.org/wiki/Strict_weak_ordering here]).]
- The semantics of `operator <` is the same as for an stl's
- [@http://www.sgi.com/tech/stl/SortedAssociativeContainer.html SortedAssociativeContainer],
- specifically
- [@http://www.sgi.com/tech/stl/set.html stl::set]
- and
- [@http://www.sgi.com/tech/stl/map.html 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 icl::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 icl::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 __bi_iterative__ 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.
- [h4 Subset Ordering and Element Equality]
- On the __conceptual__ 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
- icl::containers implements a
- [@http://en.wikipedia.org/wiki/Partially_ordered_set partial order]
- on icl::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 icl::container a,b
- a.contained_in(b) && b.contained_in(a) implies is_element_equal(a, b);
- ``
- [endsect][/ Orderings and Equivalences]
- [section Sets]
- For all set types `S` that are models concept `Set`
- (__icl_set__, __itv_set__, __sep_itv_set__ and __spl_itv_set__)
- most of the well known mathematical
- [@http://en.wikipedia.org/wiki/Algebra_of_sets laws on sets]
- were successfully checked via LaBatea. The next tables
- are giving an overview over the checked laws ordered by
- operations. If possible, the laws are formulated with
- the stronger lexicographical equality (`operator ==`)
- which implies the law's validity for the weaker
- element equality `is_element_equal`. Throughout this
- chapter we will denote element equality as `=e=` instead
- of `is_element_equal` where a short notation is advantageous.
- [h5 Laws on set union]
- For the operation ['*set union*] available as
- `operator +, +=, |, |=` and the neutral element
- `identity_element<S>::value()` which is the empty set `S()`
- these laws hold:
- ``
- Associativity<S,+,== >: S a,b,c; a+(b+c) == (a+b)+c
- Neutrality<S,+,== > : S a; a+S() == a
- Commutativity<S,+,== >: S a,b; a+b == b+a
- ``
- [h5 Laws on set intersection]
- For the operation ['*set intersection*] available as
- `operator &, &=` these laws were validated:
- ``
- Associativity<S,&,== >: S a,b,c; a&(b&c) == (a&b)&c
- Commutativity<S,&,== >: S a,b; a&b == b&a
- ``
- [/ FYI
- Neutrality has *not* been validated to avoid
- additional requirements on the sets template
- parameters.]
- [h5 Laws on set difference]
- For set difference there are only these laws. It is
- not associative and not commutative. It's neutrality
- is non symmetrical.
- ``
- RightNeutrality<S,-,== > : S a; a-S() == a
- Inversion<S,-,== >: S a; a - a == S()
- ``
- Summarized in the next table are laws that use `+`, `&` and `-`
- as a single operation. For all validated laws,
- the left and right hand sides of the equations
- are lexicographically equal, as denoted by `==` in the cells
- of the table.
- ``
- + & -
- Associativity == ==
- Neutrality == ==
- Commutativity == ==
- Inversion ==
- ``
- [h5 Distributivity Laws]
- Laws, like distributivity, that use more than one operation can
- sometimes be instantiated for different sequences of operators
- as can be seen below. In the two instantiations of the distributivity
- laws operators `+` and `&` are swapped. So we can have small operator
- signatures like `+,&` and `&,+` to describe such instantiations,
- which will be used below.
- Not all instances of distributivity laws hold for lexicographical equality.
- Therefore they are denoted using a /variable/ equality `=v=` below.
- ``
- Distributivity<S,+,&,=v= > : S a,b,c; a + (b & c) =v= (a + b) & (a + c)
- Distributivity<S,&,+,=v= > : S a,b,c; a & (b + c) =v= (a & b) + (a & c)
- RightDistributivity<S,+,-,=v= > : S a,b,c; (a + b) - c =v= (a - c) + (b - c)
- RightDistributivity<S,&,-,=v= > : S a,b,c; (a & b) - c =v= (a - c) & (b - c)
- ``
- The next table shows the relationship between
- law instances,
- [link boost_icl.introduction.interval_combining_styles interval combining style]
- and the
- used equality relation.
- ``
- +,& &,+
- Distributivity joining == ==
- separating == ==
- splitting =e= =e=
-
- +,- &,-
- RightDistributivity joining == ==
- separating == ==
- splitting =e= ==
- ``
- The table gives an overview over 12 instantiations of
- the four distributivity laws and shows the equalities
- which the instantiations holds for. For instance
- `RightDistributivity` with operator signature `+,-`
- instantiated for __spl_itv_sets__ holds only for
- element equality (denoted as `=e=`):
- ``
- RightDistributivity<S,+,-,=e= > : S a,b,c; (a + b) - c =e= (a - c) + (b - c)
- ``
- The remaining five instantiations of `RightDistributivity`
- are valid for lexicographical equality (demoted as `==`) as well.
- [link boost_icl.introduction.interval_combining_styles Interval combining styles]
- correspond to containers according to
- ``
- style set
- joining interval_set
- separating separate_interval_set
- splitting split_interval_set
- ``
- Finally there are two laws that combine all three major set operations:
- De Mogans Law and Symmetric Difference.
- [h5 DeMorgan's Law]
- De Morgans Law is better known in an incarnation where the unary
- complement operation `~` is used. `~(a+b) == ~a * ~b`. The version
- below is an adaption for the binary set difference `-`, which is
- also called ['*relative complement*].
- ``
- DeMorgan<S,+,&,=v= > : S a,b,c; a - (b + c) =v= (a - b) & (a - c)
- DeMorgan<S,&,+,=v= > : S a,b,c; a - (b & c) =v= (a - b) + (a - c)
- ``
- ``
- +,& &,+
- DeMorgan joining == ==
- separating == =e=
- splitting == =e=
- ``
- Again not all law instances are valid for lexicographical equality.
- The second instantiations only holds for element equality, if
- the interval sets are non joining.
- [h5 Symmetric Difference]
- ``
- SymmetricDifference<S,== > : S a,b,c; (a + b) - (a & b) == (a - b) + (b - a)
- ``
- Finally Symmetric Difference holds for all of icl set types and
- lexicographical equality.
- [/ pushout laws]
- [endsect][/ Sets]
- [section Maps]
- By definition a map is set of pairs. So we would expect maps to
- obey the same laws that are valid for sets. Yet
- the semantics of the *icl's* maps may be a different one, because
- of it's aggregating facilities, where the aggregating combiner
- operations are passed to combine the map's associated values.
- It turns out, that the aggregation on overlap principle
- induces semantic properties to icl maps in such a way,
- that the set of equations that are valid will depend on
- the semantics of the type `CodomainT` of the map's associated
- values.
- This is less magical as it might seem at first glance.
- If, for instance, we instantiate an __itv_map__ to
- collect and concatenate
- `std::strings` associated to intervals,
- ``
- interval_map<int,std::string> cat_map;
- cat_map += make_pair(interval<int>::rightopen(1,5),std::string("Hello"));
- cat_map += make_pair(interval<int>::rightopen(3,7),std::string(" World"));
- cout << "cat_map: " << cat_map << endl;
- ``
- we won't be able to apply `operator -=`
- ``
- // This will not compile because string::operator -= is missing.
- cat_map -= make_pair(interval<int>::rightopen(3,7),std::string(" World"));
- ``
- because, as std::sting does not implement `-=` itself, this won't compile.
- So all *laws*, that rely on `operator -=` or `-` not only will not be valid they
- can not even be stated.
- This reduces the set of laws that can be valid for a richer `CodomainT`
- type to a smaller set of laws and thus to a less restricted semantics.
- Currently we have investigated and validated two major instantiations
- of icl::Maps,
- * ['*Maps of Sets*] that will be called ['*Collectors*] and
- * ['*Maps of Numbers*] which will be called ['*Quantifiers*]
- both of which seem to have many interesting use cases for practical
- applications. The semantics associated with the term /Numbers/
- is a
- [@http://en.wikipedia.org/wiki/Monoid commutative monoid]
- for unsigned numbers
- and a
- [@http://en.wikipedia.org/wiki/Abelian_group commutative or abelian group]
- for signed numbers.
- From a practical point of view we can think
- of numbers as counting or quantifying the key values
- of the map.
- Icl ['*Maps of Sets*] or ['*Collectors*]
- are models of concept `Set`. This implies that all laws that have been
- stated as a semantics for `icl::Sets` in the previous chapter also hold for
- `Maps of Sets`.
- Icl ['*Maps of Numbers*] or ['*Quantifiers*] on the contrary are not models
- of concept `Set`.
- But there is a substantial intersection of laws that apply both for
- `Collectors` and `Quantifiers`.
- [table
- [[Kind of Map] [Alias] [Behavior] ]
- [[Maps of Sets] [Collector] [Collects items *for* key values] ]
- [[Maps of Numbers][Quantifier][Counts or quantifies *the* key values]]
- ]
- In the next two sections the law based semantics of ['*Collectors*]
- and ['*Quantifiers*] will be described in more detail.
- [endsect][/ Maps]
- [section Collectors: Maps of Sets]
- Icl `Collectors`, behave like `Sets`.
- This can be understood easily, if we consider, that
- every map of sets can be transformed to an equivalent
- set of pairs.
- For instance in the pseudocode below map `m`
- ``
- icl::map<int,set<int> > m = {(1->{1,2}), (2->{1})};
- ``
- is equivalent to set `s`
- ``
- icl::set<pair<int,int> > s = {(1,1),(1,2), //representing 1->{1,2}
- (2,1) }; //representing 2->{1}
- ``
- Also the results of add, subtract and other operations on `map m` and `set s`
- preserves the equivalence of the containers ['*almost*] perfectly:
- ``
- m += (1,3);
- m == {(1->{1,2,3}), (2->{1})}; //aggregated on collision of key value 1
- s += (1,3);
- s == {(1,1),(1,2),(1,3), //representing 1->{1,2,3}
- (2,1) }; //representing 2->{1}
- ``
- The equivalence of `m` and `s` is only violated if an
- empty set occurres in `m` by subtraction of a value pair:
- ``
- m -= (2,1);
- m == {(1->{1,2,3}), (2->{})}; //aggregated on collision of key value 2
- s -= (2,1);
- s == {(1,1),(1,2),(1,3) //representing 1->{1,2,3}
- }; //2->{} is not represented in s
- ``
- This problem can be dealt with in two ways.
- # Deleting value pairs form the Collector, if it's associated value
- becomes a neutral value or `identity_element`.
- # Using a different equality, called distinct equality in the laws
- to validate. Distinct equality only
- accounts for value pairs that that carry values unequal to the `identity_element`.
- Solution (1) led to the introduction of map traits, particularly trait
- ['*partial_absorber*], which is the default setting in all icl's map
- templates.
- Solution (2), is applied to check the semantics of icl::Maps for the
- partial_enricher trait that does not delete value pairs that carry
- identity elements. Distinct equality is implemented by a non member function
- called `is_distinct_equal`. Throughout this chapter
- distinct equality in pseudocode and law denotations is denoted
- as `=d=` operator.
- The validity of the sets of laws that make up `Set` semantics
- should now be quite evident. So the following text shows the
- laws that are validated for all `Collector` types `C`. Which are
- __icl_map__`<D,S,T>`, __itv_map__`<D,S,T>` and __spl_itv_map__`<D,S,T>`
- where `CodomainT` type `S` is a model of `Set` and `Trait` type `T` is either
- __pabsorber__ or __penricher__.
- [h5 Laws on set union, set intersection and set difference]
- ``
- Associativity<C,+,== >: C a,b,c; a+(b+c) == (a+b)+c
- Neutrality<C,+,== > : C a; a+C() == a
- Commutativity<C,+,== >: C a,b; a+b == b+a
- Associativity<C,&,== >: C a,b,c; a&(b&c) ==(a&b)&c
- Commutativity<C,&,== >: C a,b; a&b == b&a
- RightNeutrality<C,-,== >: C a; a-C() == a
- Inversion<C,-,=v= > : C a; a - a =v= C()
- ``
- All the fundamental laws could be validated for all
- icl Maps in their instantiation as Maps of Sets or Collectors.
- As expected, Inversion only holds for distinct equality,
- if the map is not a `partial_absorber`.
- ``
- + & -
- Associativity == ==
- Neutrality == ==
- Commutativity == ==
- Inversion partial_absorber ==
- partial_enricher =d=
- ``
- [h5 Distributivity Laws]
- ``
- Distributivity<C,+,&,=v= > : C a,b,c; a + (b & c) =v= (a + b) & (a + c)
- Distributivity<C,&,+,=v= > : C a,b,c; a & (b + c) =v= (a & b) + (a & c)
- RightDistributivity<C,+,-,=v= > : C a,b,c; (a + b) - c =v= (a - c) + (b - c)
- RightDistributivity<C,&,-,=v= > : C a,b,c; (a & b) - c =v= (a - c) & (b - c)
- ``
- Results for the distributivity laws are almost identical to
- the validation of sets except that
- for a `partial_enricher map` the law `(a & b) - c == (a - c) & (b - c)`
- holds for lexicographical equality.
- ``
- +,& &,+
- Distributivity joining == ==
- splitting partial_absorber =e= =e=
- partial_enricher =e= ==
-
- +,- &,-
- RightDistributivity joining == ==
- splitting =e= ==
- ``
- [h5 DeMorgan's Law and Symmetric Difference]
- ``
- DeMorgan<C,+,&,=v= > : C a,b,c; a - (b + c) =v= (a - b) & (a - c)
- DeMorgan<C,&,+,=v= > : C a,b,c; a - (b & c) =v= (a - b) + (a - c)
- ``
- ``
- +,& &,+
- DeMorgan joining == ==
- splitting == =e=
- ``
- ``
- SymmetricDifference<C,== > : C a,b,c; (a + b) - (a * b) == (a - b) + (b - a)
- ``
- Reviewing the validity tables above shows, that the sets of valid laws for
- `icl Sets` and `icl Maps of Sets` that are /identity absorbing/ are exactly the same.
- As expected, only for Maps of Sets that represent empty sets as associated values,
- called /identity enrichers/, there are marginal semantic differences.
- [endsect][/ Collectors]
- [section Quantifiers: Maps of Numbers]
- [h5 Subtraction on Quantifiers]
- With `Sets` and `Collectors` the semantics of
- `operator -` is
- that of /set difference/ which means, that you can
- only subtract what has been put into the container before.
- With `Quantifiers` that ['*count*] or ['*quantify*]
- their key values in some way,
- the semantics of `operator -` may be different.
- The question is how subtraction should be defined here?
- ``
- //Pseudocode:
- icl::map<int,some_number> q = {(1->1)};
- q -= (2->1);
- ``
- If type `some_number` is `unsigned` a /set difference/ kind of
- subtraction make sense
- ``
- icl::map<int,some_number> q = {(1->1)};
- q -= (2->1); // key 2 is not in the map so
- q == {(1->1)}; // q is unchanged by 'aggregate on collision'
- ``
- If `some_number` is a `signed` numerical type
- the result can also be this
- ``
- icl::map<int,some_number> q = {(1->1)};
- q -= (2->1); // subtracting works like
- q == {(1->1), (2-> -1)}; // adding the inverse element
- ``
- As commented in the example, subtraction of a key value
- pair `(k,v)` can obviously be defined as adding the ['*inverse element*]
- for that key `(k,-v)`, if the key is not yet stored in the map.
- [h4 Partial and Total Quantifiers and Infinite Vectors]
- Another concept, that we can think of, is that in a `Quantifier`
- every `key_value` is initially quantified `0`-times, where `0` stands
- for the neutral element of the numeric `CodomainT` type.
- Such a `Quantifier` would be totally defined on all values of
- it's `DomainT` type and can be
- conceived as an `InfiniteVector`.
- To create an infinite vector
- that is totally defined on it's domain we can set
- the map's `Trait` parameter to the value __tabsorber__.
- The __tabsorber__ trait fits specifically well with
- a `Quantifier` if it's `CodomainT` has an inverse
- element, like all signed numerical type have.
- As we can see later in this section this kind of
- a total `Quantifier` has the basic properties that
- elements of a
- [@http://en.wikipedia.org/wiki/Vector_space vector space]
- do provide.
- [h5 Intersection on Quantifiers]
- Another difference between `Collectors` and `Quantifiers`
- is the semantics of `operator &`, that has the meaning of
- set intersection for `Collectors`.
- For the /aggregate on overlap principle/ the operation `&`
- has to be passed to combine associated values on overlap
- of intervals or collision of keys. This can not be done
- for `Quantifiers`, since numeric types do not implement
- intersection.
- For `CodomainT` types that are not models of `Sets`
- `operator & ` is defined as ['aggregation on the intersection
- of the domains]. Instead of the `codomain_intersect` functor
- `codomain_combine` is used as aggregation operation:
- ``
- //Pseudocode example for partial Quantifiers p, q:
- interval_map<int,int> p, q;
- p = {[1 3)->1 };
- q = { ([2 4)->1};
- p & q =={ [2 3)->2 };
- ``
- So an addition or aggregation of associated values is
- done like for `operator +` but value pairs that have
- no common keys are not added to the result.
- For a `Quantifier` that is a model of an `InfiniteVector`
- and which is therefore defined for every key value of
- the `DomainT` type, this definition of `operator &`
- degenerates to the same sematics that `operaotor +`
- implements:
- ``
- //Pseudocode example for total Quantifiers p, q:
- interval_map<int,int> p, q;
- p = {[min 1)[1 3)[3 max]};
- ->0 ->1 ->0
- q = {[min 2)[2 4)[4 max]};
- ->0 ->1 ->0
- p&q =={[min 1)[1 2)[2 3)[3 4)[4 max]};
- ->0 ->1 ->2 ->1 ->0
- ``
- [h4 Laws for Quantifiers of unsigned Numbers]
- The semantics of icl Maps of Numbers is different
- for unsigned or signed numbers. So the sets of
- laws that are valid for Quantifiers will be different
- depending on the instantiation of an unsigned or
- a signed number type as `CodomainT` parameter.
- Again, we are presenting the investigated sets of laws, this time for
- `Quantifier` types `Q` which are
- __icl_map__`<D,N,T>`, __itv_map__`<D,N,T>` and __spl_itv_map__`<D,N,T>`
- where `CodomainT` type `N` is a `Number` and `Trait` type `T` is one of
- the icl's map traits.
- ``
- Associativity<Q,+,== >: Q a,b,c; a+(b+c) == (a+b)+c
- Neutrality<Q,+,== > : Q a; a+Q() == a
- Commutativity<Q,+,== >: Q a,b; a+b == b+a
- Associativity<Q,&,== >: Q a,b,c; a&(b&c) ==(a&b)&c
- Commutativity<Q,&,== >: Q a,b; a&b == b&a
- RightNeutrality<Q,-,== >: Q a; a-Q() == a
- Inversion<Q,-,=v= > : Q a; a - a =v= Q()
- ``
- For an `unsigned Quantifier`, an icl Map of `unsigned numbers`,
- the same basic laws apply that are
- valid for `Collectors`:
- ``
- + & -
- Associativity == ==
- Neutrality == ==
- Commutativity == ==
- Inversion absorbs_identities ==
- enriches_identities =d=
- ``
- The subset of laws, that relates to `operator +` and the neutral
- element `Q()` is that of a commutative monoid. This is the same
- concept, that applies for the `CodomainT` type. This gives
- rise to the assumption that an icl `Map` over a `CommutativeModoid`
- is again a `CommutativeModoid`.
- Other laws that were valid for `Collectors` are not valid
- for an `unsigned Quantifier`.
-
- [h4 Laws for Quantifiers of signed Numbers]
- For `Quantifiers` of signed numbers, or
- `signed Quantifiers`, the pattern of valid
- laws is somewhat different:
- ``
- + & -
- Associativity =v= =v=
- Neutrality == ==
- Commutativity == ==
- Inversion absorbs_identities ==
- enriches_identities =d=
- ``
- The differences are tagged as `=v=` indicating, that
- the associativity law is not uniquely valid for a single
- equality relation `==` as this was the case for
- `Collector` and `unsigned Quntifier` maps.
- The differences are these:
- ``
- +
- Associativity icl::map ==
- interval_map ==
- split_interval_map =e=
- ``
- For `operator +` the associativity on __spl_itv_maps__ is only valid
- with element equality `=e=`, which is not a big constrained, because
- only element equality is required.
- For `operator &` the associativity is broken for all maps
- that are partial absorbers. For total absorbers associativity
- is valid for element equality. All maps having the /identity enricher/
- Trait are associative wrt. lexicographical equality `==`.
- ``
- Associativity &
- absorbs_identities && !is_total false
- absorbs_identities && is_total =e=
- enriches_identities ==
- ``
- Note, that all laws that establish a commutative
- monoid for `operator +` and identity element `Q()` are valid
- for `signed Quantifiers`.
- In addition symmetric difference that does not
- hold for `unsigned Qunatifiers` is valid
- for `signed Qunatifiers`.
- ``
- SymmetricDifference<Q,== > : Q a,b,c; (a + b) - (a & b) == (a - b) + (b - a)
- ``
- For a `signed TotalQuantifier` `Qt` symmetrical difference degenerates to
- a trivial form since `operator &` and `operator +` become identical
- ``
- SymmetricDifference<Qt,== > : Qt a,b,c; (a + b) - (a + b) == (a - b) + (b - a) == Qt()
- ``
- [h5 Existence of an Inverse]
- By now `signed Quantifiers` `Q` are
- commutative monoids
- with respect to the
- `operator +` and the neutral element `Q()`.
- If the Quantifier's `CodomainT` type has an /inverse element/
- like e.g. `signed numbers` do,
- the `CodomainT` type is a
- ['*commutative*] or ['*abelian group*].
- In this case a `signed Quantifier` that is also ['*total*]
- has an ['*inverse*] and the following law holds:
- ``
- InverseElement<Qt,== > : Qt a; (0 - a) + a == 0
- ``
- Which means that each `TotalQuantifier` over an
- abelian group is an
- abelian group
- itself.
- This also implies that a `Quantifier` of `Quantifiers`
- is again a `Quantifiers` and a
- `TotalQuantifier` of `TotalQuantifiers`
- is also a `TotalQuantifier`.
- `TotalQuantifiers` resemble the notion of a
- vector space partially.
- The concept could be completed to a vector space,
- if a scalar multiplication was added.
- [endsect][/ Quantifiers]
- [section Concept Induction]
- Obviously we can observe the induction of semantics
- from the `CodomainT` parameter into the instantiations
- of icl maps.
- [table
- [[] [is model of] [if] [example]]
- [[`Map<D,Monoid>`] [`Modoid`] [] [`interval_map<int,string>`]]
- [[`Map<D,Set,Trait>`] [`Set`] [`Trait::absorbs_identities`][`interval_map<int,std::set<int> >`]]
- [[`Map<D,CommutativeMonoid>`][`CommutativeMonoid`][] [`interval_map<int,unsigned int>`]]
- [[`Map<D,CommutativeGroup>`] [`CommutativeGroup`] [`Trait::is_total`] [`interval_map<int,int,total_absorber>`]]
- ]
- [endsect][/ Concept Induction]
- [endsect][/ Semantics]
|