1[/ 2 Copyright (c) 2008-2009 Joachim Faulhaber 3 4 Distributed under the Boost Software License, Version 1.0. 5 (See accompanying file LICENSE_1_0.txt or copy at 6 http://www.boost.org/LICENSE_1_0.txt) 7] 8 9[section Semantics] 10 11["Beauty is the ultimate defense against complexity] -- [/David Gelernter] 12[@http://en.wikipedia.org/wiki/David_Gelernter David Gelernter] 13 14In the *icl* we follow the notion, that the semantics of a ['*concept*] or 15['*abstract data type*] can be expressed by ['*laws*]. We formulate 16laws over interval containers that can be evaluated for a given 17instantiation of the variables contained in the law. The following 18pseudocode gives a shorthand notation of such a law. 19`` 20Commutativity<T,+>: 21T a, b; a + b == b + a; 22`` 23This can of course be coded as a proper c++ class template which has 24been done for the validation of the *icl*. For sake of simplicity 25we will use pseudocode here. 26 27The laws that describe the semantics of the *icl's* class templates 28were validated using the Law based Test Automaton ['*LaBatea*], 29a tool that generates instances for the law's variables and then 30tests it's validity. 31Since the *icl* deals with sets, maps and relations, that are 32well known objects from mathematics, the laws that we are 33using are mostly /recycled/ ones. Also some of those laws are grouped 34in notions like e.g. /orderings/ or /algebras/. 35 36[section Orderings and Equivalences] 37 38[h4 Lexicographical Ordering and Equality] 39 40On all set and map containers of the icl, there is an `operator <` 41that implements a 42[@https://boost.org/sgi/stl/StrictWeakOrdering.html strict weak ordering]. 43[/ (see also [@http://en.wikipedia.org/wiki/Strict_weak_ordering here]).] 44The semantics of `operator <` is the same as for an stl's 45[@https://boost.org/sgi/stl/SortedAssociativeContainer.html SortedAssociativeContainer], 46specifically 47[@https://boost.org/sgi/stl/set.html stl::set] 48and 49[@https://boost.org/sgi/stl/Map.html stl::map]: 50`` 51Irreflexivity<T,< > : T a; !(a<a) 52Asymmetry<T,< > : T a,b; a<b implies !(b<a) 53Transitivity<T,< > : T a,b,c; a<b && b<c implies a<c 54`` 55 56`Operator <` depends on the icl::container's template parameter 57`Compare` that implements a ['strict weak ordering] for the container's 58`domain_type`. 59For a given `Compare` ordering, `operator <` implements a 60lexicographical comparison on icl::containers, that uses the 61`Compare` order to establish a unique sequence of values in 62the container. 63 64The induced equivalence of `operator <` is 65lexicographical equality 66which is implemented as `operator ==`. 67`` 68//equivalence induced by strict weak ordering < 69!(a<b) && !(b<a) implies a == b; 70`` 71Again this 72follows the semantics of the *stl*. 73Lexicographical equality is stronger than the equality 74of elements. Two containers that contain the same elements 75can be lexicographically unequal, if their elements are 76differently sorted. Lexicographical comparison belongs to 77the __bi_iterative__ aspect. Of all the different sequences that are valid 78for unordered sets and maps, one such sequence is 79selected by the `Compare` order of elements. Based on 80this selection a unique iteration is possible. 81 82[h4 Subset Ordering and Element Equality] 83 84On the __conceptual__ aspect only membership of elements 85matters, not their sequence. So there are functions 86`contained_in` and `element_equal` that implement 87the subset relation and the equality on elements. 88Yet, `contained_in` and `is_element_equal` functions are not 89really working on the level of elements. They also 90work on the basis of the containers templates 91`Compare` parameter. In practical terms we need to 92distinguish between lexicographical equality 93`operator ==` and equality of elements `is_element_equal`, 94if we work with interval splitting interval containers: 95`` 96split_interval_set<time> w1, w2; //Pseudocode 97w1 = {[Mon .. Sun)}; //split_interval_set containing a week 98w2 = {[Mon .. Fri)[Sat .. Sun)}; //Same week split in work and week end parts. 99w1 == w2; //false: Different segmentation 100is_element_equal(w1,w2); //true: Same elements contained 101`` 102 103For a constant `Compare` order on key elements, 104member function `contained_in` that is defined for all 105icl::containers implements a 106[@http://en.wikipedia.org/wiki/Partially_ordered_set partial order] 107on icl::containers. 108 109`` 110with <= for contained_in, 111 =e= for is_element_equal: 112Reflexivity<T,<= > : T a; a <= a 113Antisymmetry<T,<=,=e=> : T a,b; a <= b && b <= a implies a =e= b 114Transitivity<T,<= > : T a,b,c; a <= b && b <= c implies a <= c 115`` 116 117The induced equivalence is the equality of elements that 118is implemented via function `is_element_equal`. 119`` 120//equivalence induced by the partial ordering contained_in on icl::container a,b 121a.contained_in(b) && b.contained_in(a) implies is_element_equal(a, b); 122`` 123 124[endsect][/ Orderings and Equivalences] 125 126[section Sets] 127 128For all set types `S` that are models concept `Set` 129(__icl_set__, __itv_set__, __sep_itv_set__ and __spl_itv_set__) 130most of the well known mathematical 131[@http://en.wikipedia.org/wiki/Algebra_of_sets laws on sets] 132were successfully checked via LaBatea. The next tables 133are giving an overview over the checked laws ordered by 134operations. If possible, the laws are formulated with 135the stronger lexicographical equality (`operator ==`) 136which implies the law's validity for the weaker 137element equality `is_element_equal`. Throughout this 138chapter we will denote element equality as `=e=` instead 139of `is_element_equal` where a short notation is advantageous. 140 141[h5 Laws on set union] 142 143For the operation ['*set union*] available as 144`operator +, +=, |, |=` and the neutral element 145`identity_element<S>::value()` which is the empty set `S()` 146these laws hold: 147`` 148Associativity<S,+,== >: S a,b,c; a+(b+c) == (a+b)+c 149Neutrality<S,+,== > : S a; a+S() == a 150Commutativity<S,+,== >: S a,b; a+b == b+a 151`` 152 153[h5 Laws on set intersection] 154 155For the operation ['*set intersection*] available as 156`operator &, &=` these laws were validated: 157 158`` 159Associativity<S,&,== >: S a,b,c; a&(b&c) == (a&b)&c 160Commutativity<S,&,== >: S a,b; a&b == b&a 161`` 162 163[/ FYI 164Neutrality has *not* been validated to avoid 165additional requirements on the sets template 166parameters.] 167 168[h5 Laws on set difference] 169 170For set difference there are only these laws. It is 171not associative and not commutative. It's neutrality 172is non symmetrical. 173 174`` 175RightNeutrality<S,-,== > : S a; a-S() == a 176Inversion<S,-,== >: S a; a - a == S() 177`` 178 179Summarized in the next table are laws that use `+`, `&` and `-` 180as a single operation. For all validated laws, 181the left and right hand sides of the equations 182are lexicographically equal, as denoted by `==` in the cells 183of the table. 184 185`` 186 + & - 187Associativity == == 188Neutrality == == 189Commutativity == == 190Inversion == 191`` 192 193[h5 Distributivity Laws] 194 195Laws, like distributivity, that use more than one operation can 196sometimes be instantiated for different sequences of operators 197as can be seen below. In the two instantiations of the distributivity 198laws operators `+` and `&` are swapped. So we can have small operator 199signatures like `+,&` and `&,+` to describe such instantiations, 200which will be used below. 201Not all instances of distributivity laws hold for lexicographical equality. 202Therefore they are denoted using a /variable/ equality `=v=` below. 203 204`` 205 Distributivity<S,+,&,=v= > : S a,b,c; a + (b & c) =v= (a + b) & (a + c) 206 Distributivity<S,&,+,=v= > : S a,b,c; a & (b + c) =v= (a & b) + (a & c) 207RightDistributivity<S,+,-,=v= > : S a,b,c; (a + b) - c =v= (a - c) + (b - c) 208RightDistributivity<S,&,-,=v= > : S a,b,c; (a & b) - c =v= (a - c) & (b - c) 209`` 210 211The next table shows the relationship between 212law instances, 213[link boost_icl.introduction.interval_combining_styles interval combining style] 214and the 215used equality relation. 216 217`` 218 +,& &,+ 219 Distributivity joining == == 220 separating == == 221 splitting =e= =e= 222 223 +,- &,- 224RightDistributivity joining == == 225 separating == == 226 splitting =e= == 227`` 228 229The table gives an overview over 12 instantiations of 230the four distributivity laws and shows the equalities 231which the instantiations holds for. For instance 232`RightDistributivity` with operator signature `+,-` 233instantiated for __spl_itv_sets__ holds only for 234element equality (denoted as `=e=`): 235`` 236RightDistributivity<S,+,-,=e= > : S a,b,c; (a + b) - c =e= (a - c) + (b - c) 237`` 238The remaining five instantiations of `RightDistributivity` 239are valid for lexicographical equality (demoted as `==`) as well. 240 241[link boost_icl.introduction.interval_combining_styles Interval combining styles] 242correspond to containers according to 243`` 244style set 245joining interval_set 246separating separate_interval_set 247splitting split_interval_set 248`` 249 250 251Finally there are two laws that combine all three major set operations: 252De Mogans Law and Symmetric Difference. 253 254[h5 DeMorgan's Law] 255 256De Morgans Law is better known in an incarnation where the unary 257complement operation `~` is used. `~(a+b) == ~a * ~b`. The version 258below is an adaption for the binary set difference `-`, which is 259also called ['*relative complement*]. 260`` 261DeMorgan<S,+,&,=v= > : S a,b,c; a - (b + c) =v= (a - b) & (a - c) 262DeMorgan<S,&,+,=v= > : S a,b,c; a - (b & c) =v= (a - b) + (a - c) 263`` 264 265`` 266 +,& &,+ 267DeMorgan joining == == 268 separating == =e= 269 splitting == =e= 270`` 271 272Again not all law instances are valid for lexicographical equality. 273The second instantiations only holds for element equality, if 274the interval sets are non joining. 275 276[h5 Symmetric Difference] 277 278`` 279SymmetricDifference<S,== > : S a,b,c; (a + b) - (a & b) == (a - b) + (b - a) 280`` 281 282Finally Symmetric Difference holds for all of icl set types and 283lexicographical equality. 284 285[/ pushout laws] 286 287[endsect][/ Sets] 288 289[section Maps] 290 291By definition a map is set of pairs. So we would expect maps to 292obey the same laws that are valid for sets. Yet 293the semantics of the *icl's* maps may be a different one, because 294of it's aggregating facilities, where the aggregating combiner 295operations are passed to combine the map's associated values. 296It turns out, that the aggregation on overlap principle 297induces semantic properties to icl maps in such a way, 298that the set of equations that are valid will depend on 299the semantics of the type `CodomainT` of the map's associated 300values. 301 302This is less magical as it might seem at first glance. 303If, for instance, we instantiate an __itv_map__ to 304collect and concatenate 305`std::strings` associated to intervals, 306 307`` 308interval_map<int,std::string> cat_map; 309cat_map += make_pair(interval<int>::rightopen(1,5),std::string("Hello")); 310cat_map += make_pair(interval<int>::rightopen(3,7),std::string(" World")); 311cout << "cat_map: " << cat_map << endl; 312`` 313 314we won't be able to apply `operator -=` 315`` 316// This will not compile because string::operator -= is missing. 317cat_map -= make_pair(interval<int>::rightopen(3,7),std::string(" World")); 318`` 319because, as std::sting does not implement `-=` itself, this won't compile. 320So all *laws*, that rely on `operator -=` or `-` not only will not be valid they 321can not even be stated. 322This reduces the set of laws that can be valid for a richer `CodomainT` 323type to a smaller set of laws and thus to a less restricted semantics. 324 325Currently we have investigated and validated two major instantiations 326of icl::Maps, 327 328* ['*Maps of Sets*] that will be called ['*Collectors*] and 329* ['*Maps of Numbers*] which will be called ['*Quantifiers*] 330 331both of which seem to have many interesting use cases for practical 332applications. The semantics associated with the term /Numbers/ 333is a 334[@http://en.wikipedia.org/wiki/Monoid commutative monoid] 335for unsigned numbers 336and a 337[@http://en.wikipedia.org/wiki/Abelian_group commutative or abelian group] 338for signed numbers. 339From a practical point of view we can think 340of numbers as counting or quantifying the key values 341of the map. 342 343Icl ['*Maps of Sets*] or ['*Collectors*] 344are models of concept `Set`. This implies that all laws that have been 345stated as a semantics for `icl::Sets` in the previous chapter also hold for 346`Maps of Sets`. 347Icl ['*Maps of Numbers*] or ['*Quantifiers*] on the contrary are not models 348of concept `Set`. 349But there is a substantial intersection of laws that apply both for 350`Collectors` and `Quantifiers`. 351 352[table 353[[Kind of Map] [Alias] [Behavior] ] 354[[Maps of Sets] [Collector] [Collects items *for* key values] ] 355[[Maps of Numbers][Quantifier][Counts or quantifies *the* key values]] 356] 357 358In the next two sections the law based semantics of ['*Collectors*] 359and ['*Quantifiers*] will be described in more detail. 360 361[endsect][/ Maps] 362 363[section Collectors: Maps of Sets] 364 365Icl `Collectors`, behave like `Sets`. 366This can be understood easily, if we consider, that 367every map of sets can be transformed to an equivalent 368set of pairs. 369For instance in the pseudocode below map `m` 370`` 371icl::map<int,set<int> > m = {(1->{1,2}), (2->{1})}; 372`` 373is equivalent to set `s` 374`` 375icl::set<pair<int,int> > s = {(1,1),(1,2), //representing 1->{1,2} 376 (2,1) }; //representing 2->{1} 377`` 378 379Also the results of add, subtract and other operations on `map m` and `set s` 380preserves the equivalence of the containers ['*almost*] perfectly: 381`` 382m += (1,3); 383m == {(1->{1,2,3}), (2->{1})}; //aggregated on collision of key value 1 384s += (1,3); 385s == {(1,1),(1,2),(1,3), //representing 1->{1,2,3} 386 (2,1) }; //representing 2->{1} 387`` 388 389The equivalence of `m` and `s` is only violated if an 390empty set occurres in `m` by subtraction of a value pair: 391`` 392m -= (2,1); 393m == {(1->{1,2,3}), (2->{})}; //aggregated on collision of key value 2 394s -= (2,1); 395s == {(1,1),(1,2),(1,3) //representing 1->{1,2,3} 396 }; //2->{} is not represented in s 397`` 398 399This problem can be dealt with in two ways. 400 401# Deleting value pairs form the Collector, if it's associated value 402 becomes a neutral value or `identity_element`. 403# Using a different equality, called distinct equality in the laws 404 to validate. Distinct equality only 405 accounts for value pairs that that carry values unequal to the `identity_element`. 406 407Solution (1) led to the introduction of map traits, particularly trait 408['*partial_absorber*], which is the default setting in all icl's map 409templates. 410 411Solution (2), is applied to check the semantics of icl::Maps for the 412partial_enricher trait that does not delete value pairs that carry 413identity elements. Distinct equality is implemented by a non member function 414called `is_distinct_equal`. Throughout this chapter 415distinct equality in pseudocode and law denotations is denoted 416as `=d=` operator. 417 418The validity of the sets of laws that make up `Set` semantics 419should now be quite evident. So the following text shows the 420laws that are validated for all `Collector` types `C`. Which are 421__icl_map__`<D,S,T>`, __itv_map__`<D,S,T>` and __spl_itv_map__`<D,S,T>` 422where `CodomainT` type `S` is a model of `Set` and `Trait` type `T` is either 423__pabsorber__ or __penricher__. 424 425 426[h5 Laws on set union, set intersection and set difference] 427 428`` 429Associativity<C,+,== >: C a,b,c; a+(b+c) == (a+b)+c 430Neutrality<C,+,== > : C a; a+C() == a 431Commutativity<C,+,== >: C a,b; a+b == b+a 432 433Associativity<C,&,== >: C a,b,c; a&(b&c) ==(a&b)&c 434Commutativity<C,&,== >: C a,b; a&b == b&a 435 436RightNeutrality<C,-,== >: C a; a-C() == a 437Inversion<C,-,=v= > : C a; a - a =v= C() 438`` 439 440All the fundamental laws could be validated for all 441icl Maps in their instantiation as Maps of Sets or Collectors. 442As expected, Inversion only holds for distinct equality, 443if the map is not a `partial_absorber`. 444 445`` 446 + & - 447Associativity == == 448Neutrality == == 449Commutativity == == 450Inversion partial_absorber == 451 partial_enricher =d= 452`` 453 454[h5 Distributivity Laws] 455 456`` 457 Distributivity<C,+,&,=v= > : C a,b,c; a + (b & c) =v= (a + b) & (a + c) 458 Distributivity<C,&,+,=v= > : C a,b,c; a & (b + c) =v= (a & b) + (a & c) 459RightDistributivity<C,+,-,=v= > : C a,b,c; (a + b) - c =v= (a - c) + (b - c) 460RightDistributivity<C,&,-,=v= > : C a,b,c; (a & b) - c =v= (a - c) & (b - c) 461`` 462 463Results for the distributivity laws are almost identical to 464the validation of sets except that 465for a `partial_enricher map` the law `(a & b) - c == (a - c) & (b - c)` 466holds for lexicographical equality. 467 468`` 469 +,& &,+ 470 Distributivity joining == == 471 splitting partial_absorber =e= =e= 472 partial_enricher =e= == 473 474 +,- &,- 475RightDistributivity joining == == 476 splitting =e= == 477`` 478 479[h5 DeMorgan's Law and Symmetric Difference] 480 481`` 482DeMorgan<C,+,&,=v= > : C a,b,c; a - (b + c) =v= (a - b) & (a - c) 483DeMorgan<C,&,+,=v= > : C a,b,c; a - (b & c) =v= (a - b) + (a - c) 484`` 485 486`` 487 +,& &,+ 488DeMorgan joining == == 489 splitting == =e= 490`` 491 492`` 493SymmetricDifference<C,== > : C a,b,c; (a + b) - (a * b) == (a - b) + (b - a) 494`` 495 496Reviewing the validity tables above shows, that the sets of valid laws for 497`icl Sets` and `icl Maps of Sets` that are /identity absorbing/ are exactly the same. 498As expected, only for Maps of Sets that represent empty sets as associated values, 499called /identity enrichers/, there are marginal semantic differences. 500 501[endsect][/ Collectors] 502 503[section Quantifiers: Maps of Numbers] 504 505[h5 Subtraction on Quantifiers] 506 507With `Sets` and `Collectors` the semantics of 508`operator -` is 509that of /set difference/ which means, that you can 510only subtract what has been put into the container before. 511With `Quantifiers` that ['*count*] or ['*quantify*] 512their key values in some way, 513the semantics of `operator -` may be different. 514 515The question is how subtraction should be defined here? 516`` 517//Pseudocode: 518icl::map<int,some_number> q = {(1->1)}; 519q -= (2->1); 520`` 521If type `some_number` is `unsigned` a /set difference/ kind of 522subtraction make sense 523`` 524icl::map<int,some_number> q = {(1->1)}; 525q -= (2->1); // key 2 is not in the map so 526q == {(1->1)}; // q is unchanged by 'aggregate on collision' 527`` 528If `some_number` is a `signed` numerical type 529the result can also be this 530`` 531icl::map<int,some_number> q = {(1->1)}; 532q -= (2->1); // subtracting works like 533q == {(1->1), (2-> -1)}; // adding the inverse element 534`` 535As commented in the example, subtraction of a key value 536pair `(k,v)` can obviously be defined as adding the ['*inverse element*] 537for that key `(k,-v)`, if the key is not yet stored in the map. 538 539[h4 Partial and Total Quantifiers and Infinite Vectors] 540 541Another concept, that we can think of, is that in a `Quantifier` 542every `key_value` is initially quantified `0`-times, where `0` stands 543for the neutral element of the numeric `CodomainT` type. 544Such a `Quantifier` would be totally defined on all values of 545it's `DomainT` type and can be 546conceived as an `InfiniteVector`. 547 548To create an infinite vector 549that is totally defined on it's domain we can set 550the map's `Trait` parameter to the value __tabsorber__. 551The __tabsorber__ trait fits specifically well with 552a `Quantifier` if it's `CodomainT` has an inverse 553element, like all signed numerical type have. 554As we can see later in this section this kind of 555a total `Quantifier` has the basic properties that 556elements of a 557[@http://en.wikipedia.org/wiki/Vector_space vector space] 558do provide. 559 560 561[h5 Intersection on Quantifiers] 562 563Another difference between `Collectors` and `Quantifiers` 564is the semantics of `operator &`, that has the meaning of 565set intersection for `Collectors`. 566 567For the /aggregate on overlap principle/ the operation `&` 568has to be passed to combine associated values on overlap 569of intervals or collision of keys. This can not be done 570for `Quantifiers`, since numeric types do not implement 571intersection. 572 573For `CodomainT` types that are not models of `Sets` 574`operator & ` is defined as ['aggregation on the intersection 575of the domains]. Instead of the `codomain_intersect` functor 576`codomain_combine` is used as aggregation operation: 577`` 578//Pseudocode example for partial Quantifiers p, q: 579interval_map<int,int> p, q; 580p = {[1 3)->1 }; 581q = { ([2 4)->1}; 582p & q =={ [2 3)->2 }; 583`` 584So an addition or aggregation of associated values is 585done like for `operator +` but value pairs that have 586no common keys are not added to the result. 587 588For a `Quantifier` that is a model of an `InfiniteVector` 589and which is therefore defined for every key value of 590the `DomainT` type, this definition of `operator &` 591degenerates to the same sematics that `operaotor +` 592implements: 593`` 594//Pseudocode example for total Quantifiers p, q: 595interval_map<int,int> p, q; 596p = {[min 1)[1 3)[3 max]}; 597 ->0 ->1 ->0 598q = {[min 2)[2 4)[4 max]}; 599 ->0 ->1 ->0 600p&q =={[min 1)[1 2)[2 3)[3 4)[4 max]}; 601 ->0 ->1 ->2 ->1 ->0 602`` 603 604[h4 Laws for Quantifiers of unsigned Numbers] 605 606The semantics of icl Maps of Numbers is different 607for unsigned or signed numbers. So the sets of 608laws that are valid for Quantifiers will be different 609depending on the instantiation of an unsigned or 610a signed number type as `CodomainT` parameter. 611 612Again, we are presenting the investigated sets of laws, this time for 613`Quantifier` types `Q` which are 614__icl_map__`<D,N,T>`, __itv_map__`<D,N,T>` and __spl_itv_map__`<D,N,T>` 615where `CodomainT` type `N` is a `Number` and `Trait` type `T` is one of 616the icl's map traits. 617 618`` 619Associativity<Q,+,== >: Q a,b,c; a+(b+c) == (a+b)+c 620Neutrality<Q,+,== > : Q a; a+Q() == a 621Commutativity<Q,+,== >: Q a,b; a+b == b+a 622 623Associativity<Q,&,== >: Q a,b,c; a&(b&c) ==(a&b)&c 624Commutativity<Q,&,== >: Q a,b; a&b == b&a 625 626RightNeutrality<Q,-,== >: Q a; a-Q() == a 627Inversion<Q,-,=v= > : Q a; a - a =v= Q() 628`` 629 630For an `unsigned Quantifier`, an icl Map of `unsigned numbers`, 631the same basic laws apply that are 632valid for `Collectors`: 633 634`` 635 + & - 636Associativity == == 637Neutrality == == 638Commutativity == == 639Inversion absorbs_identities == 640 enriches_identities =d= 641`` 642 643The subset of laws, that relates to `operator +` and the neutral 644element `Q()` is that of a commutative monoid. This is the same 645concept, that applies for the `CodomainT` type. This gives 646rise to the assumption that an icl `Map` over a `CommutativeModoid` 647is again a `CommutativeModoid`. 648 649Other laws that were valid for `Collectors` are not valid 650for an `unsigned Quantifier`. 651 652 653[h4 Laws for Quantifiers of signed Numbers] 654 655For `Quantifiers` of signed numbers, or 656`signed Quantifiers`, the pattern of valid 657laws is somewhat different: 658`` 659 + & - 660Associativity =v= =v= 661Neutrality == == 662Commutativity == == 663Inversion absorbs_identities == 664 enriches_identities =d= 665`` 666 667The differences are tagged as `=v=` indicating, that 668the associativity law is not uniquely valid for a single 669equality relation `==` as this was the case for 670`Collector` and `unsigned Quntifier` maps. 671 672The differences are these: 673`` 674 + 675Associativity icl::map == 676 interval_map == 677 split_interval_map =e= 678`` 679For `operator +` the associativity on __spl_itv_maps__ is only valid 680with element equality `=e=`, which is not a big constrained, because 681only element equality is required. 682 683For `operator &` the associativity is broken for all maps 684that are partial absorbers. For total absorbers associativity 685is valid for element equality. All maps having the /identity enricher/ 686Trait are associative wrt. lexicographical equality `==`. 687`` 688Associativity & 689 absorbs_identities && !is_total false 690 absorbs_identities && is_total =e= 691 enriches_identities == 692`` 693 694Note, that all laws that establish a commutative 695monoid for `operator +` and identity element `Q()` are valid 696for `signed Quantifiers`. 697In addition symmetric difference that does not 698hold for `unsigned Qunatifiers` is valid 699for `signed Qunatifiers`. 700 701`` 702SymmetricDifference<Q,== > : Q a,b,c; (a + b) - (a & b) == (a - b) + (b - a) 703`` 704For a `signed TotalQuantifier` `Qt` symmetrical difference degenerates to 705a trivial form since `operator &` and `operator +` become identical 706`` 707SymmetricDifference<Qt,== > : Qt a,b,c; (a + b) - (a + b) == (a - b) + (b - a) == Qt() 708`` 709 710[h5 Existence of an Inverse] 711 712By now `signed Quantifiers` `Q` are 713commutative monoids 714with respect to the 715`operator +` and the neutral element `Q()`. 716If the Quantifier's `CodomainT` type has an /inverse element/ 717like e.g. `signed numbers` do, 718the `CodomainT` type is a 719['*commutative*] or ['*abelian group*]. 720In this case a `signed Quantifier` that is also ['*total*] 721has an ['*inverse*] and the following law holds: 722 723`` 724InverseElement<Qt,== > : Qt a; (0 - a) + a == 0 725`` 726 727Which means that each `TotalQuantifier` over an 728abelian group is an 729abelian group 730itself. 731 732This also implies that a `Quantifier` of `Quantifiers` 733is again a `Quantifiers` and a 734`TotalQuantifier` of `TotalQuantifiers` 735is also a `TotalQuantifier`. 736 737`TotalQuantifiers` resemble the notion of a 738vector space partially. 739The concept could be completed to a vector space, 740if a scalar multiplication was added. 741[endsect][/ Quantifiers] 742 743 744[section Concept Induction] 745 746Obviously we can observe the induction of semantics 747from the `CodomainT` parameter into the instantiations 748of icl maps. 749 750[table 751[[] [is model of] [if] [example]] 752[[`Map<D,Monoid>`] [`Modoid`] [] [`interval_map<int,string>`]] 753[[`Map<D,Set,Trait>`] [`Set`] [`Trait::absorbs_identities`][`interval_map<int,std::set<int> >`]] 754[[`Map<D,CommutativeMonoid>`][`CommutativeMonoid`][] [`interval_map<int,unsigned int>`]] 755[[`Map<D,CommutativeGroup>`] [`CommutativeGroup`] [`Trait::is_total`] [`interval_map<int,int,total_absorber>`]] 756] 757 758[endsect][/ Concept Induction] 759 760[endsect][/ Semantics] 761