[/ 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 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 [@https://boost.org/sgi/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 [@https://boost.org/sgi/stl/SortedAssociativeContainer.html SortedAssociativeContainer], specifically [@https://boost.org/sgi/stl/set.html stl::set] and [@https://boost.org/sgi/stl/Map.html stl::map]: `` Irreflexivity : T a; !(a : T a,b; a : T a,b,c; a 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 a; a <= a Antisymmetry : T a,b; a <= b && b <= a implies a =e= b Transitivity : 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::value()` which is the empty set `S()` these laws hold: `` Associativity: S a,b,c; a+(b+c) == (a+b)+c Neutrality : S a; a+S() == a Commutativity: 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 a,b,c; a&(b&c) == (a&b)&c Commutativity: 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 a; a-S() == a Inversion: 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 a,b,c; a + (b & c) =v= (a + b) & (a + c) Distributivity : S a,b,c; a & (b + c) =v= (a & b) + (a & c) RightDistributivity : S a,b,c; (a + b) - c =v= (a - c) + (b - c) RightDistributivity : 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 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 a,b,c; a - (b + c) =v= (a - b) & (a - c) DeMorgan : 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 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 cat_map; cat_map += make_pair(interval::rightopen(1,5),std::string("Hello")); cat_map += make_pair(interval::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::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 > m = {(1->{1,2}), (2->{1})}; `` is equivalent to set `s` `` icl::set > 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__``, __itv_map__`` and __spl_itv_map__`` 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 a,b,c; a+(b+c) == (a+b)+c Neutrality : C a; a+C() == a Commutativity: C a,b; a+b == b+a Associativity: C a,b,c; a&(b&c) ==(a&b)&c Commutativity: C a,b; a&b == b&a RightNeutrality: C a; a-C() == a Inversion : 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 a,b,c; a + (b & c) =v= (a + b) & (a + c) Distributivity : C a,b,c; a & (b + c) =v= (a & b) + (a & c) RightDistributivity : C a,b,c; (a + b) - c =v= (a - c) + (b - c) RightDistributivity : 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 a,b,c; a - (b + c) =v= (a - b) & (a - c) DeMorgan : C a,b,c; a - (b & c) =v= (a - b) + (a - c) `` `` +,& &,+ DeMorgan joining == == splitting == =e= `` `` SymmetricDifference : 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 q = {(1->1)}; q -= (2->1); `` If type `some_number` is `unsigned` a /set difference/ kind of subtraction make sense `` icl::map 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 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 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 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__``, __itv_map__`` and __spl_itv_map__`` where `CodomainT` type `N` is a `Number` and `Trait` type `T` is one of the icl's map traits. `` Associativity: Q a,b,c; a+(b+c) == (a+b)+c Neutrality : Q a; a+Q() == a Commutativity: Q a,b; a+b == b+a Associativity: Q a,b,c; a&(b&c) ==(a&b)&c Commutativity: Q a,b; a&b == b&a RightNeutrality: Q a; a-Q() == a Inversion : 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 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 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 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`] [`Modoid`] [] [`interval_map`]] [[`Map`] [`Set`] [`Trait::absorbs_identities`][`interval_map >`]] [[`Map`][`CommutativeMonoid`][] [`interval_map`]] [[`Map`] [`CommutativeGroup`] [`Trait::is_total`] [`interval_map`]] ] [endsect][/ Concept Induction] [endsect][/ Semantics]