Subject: [Boost-commit] svn:boost r50551 - in sandbox/itl/libs: itl/doc validate/example/labat_single
From: afojgo_at_[hidden]
Date: 2009-01-12 05:45:09
Author: jofaber
Date: 2009-01-12 05:45:08 EST (Mon, 12 Jan 2009)
New Revision: 50551
URL: http://svn.boost.org/trac/boost/changeset/50551
Log:
Added documentation. Semantics: Concept Induction. Stable {msvc-9.0, partly congcc-4.3-a7}
Text files modified:
sandbox/itl/libs/itl/doc/semantics.qbk | 126 +++++++++++++++++++++++++++------------
sandbox/itl/libs/validate/example/labat_single/labat_single.cpp | 8 +-
2 files changed, 90 insertions(+), 44 deletions(-)
Modified: sandbox/itl/libs/itl/doc/semantics.qbk
==============================================================================
--- sandbox/itl/libs/itl/doc/semantics.qbk (original)
+++ sandbox/itl/libs/itl/doc/semantics.qbk 2009-01-12 05:45:08 EST (Mon, 12 Jan 2009)
@@ -14,8 +14,8 @@
instantiation of the variables contained in the law. The following
pseudocode gives a shorthand notation of such a law.
``
-Commutativity<typename T>
-T a, b: a + b == b + a;
+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
@@ -141,9 +141,9 @@
`neutron<S>::value()` which is the empty set `T()`
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
+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]
@@ -152,8 +152,8 @@
`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
+Associativity<S,*,== >: S a,b,c; a*(b*c) == (a*b)*c
+Commutativity<S,*,== >: S a,b; a*b == b*a
``
Neutrality has *not* been validated to avoid
@@ -167,8 +167,8 @@
is non symmetrical.
``
-RightNeutrality<S,-,== > : S a: a-S() == a
-SelfRemovability<S,-,== >: S a: a - a == S()
+RightNeutrality<S,-,== > : S a; a-S() == a
+SelfRemovability<S,-,== >: S a; a - a == S()
``
Summarized in the next table are laws that use `+`, `*` and `-`
@@ -197,10 +197,10 @@
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)
+ 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
@@ -254,8 +254,8 @@
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<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)
``
``
@@ -272,7 +272,7 @@
[h5 Symmetric Difference]
``
-SymmetricDifference<S,== > : S a,b,c: (a + b) - (a * b) == (a - b) + (b - a)
+SymmetricDifference<S,== > : S a,b,c; (a + b) - (a * b) == (a - b) + (b - a)
``
Finally Symmetrical Difference holds for all of itl set types and
@@ -425,15 +425,15 @@
[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
+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
+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
-SelfRemovability<C,-,=v= >: C a: a - a =v= C()
+RightNeutrality<C,-,== > : C a; a-C() == a
+SelfRemovability<C,-,=v= >: C a; a - a =v= C()
``
All the fundamental laws could be validated for all
@@ -453,10 +453,10 @@
[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)
+ 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
@@ -478,8 +478,8 @@
[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<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)
``
``
@@ -489,7 +489,7 @@
``
``
-SymmetricDifference<C,== > : C a,b,c: (a + b) - (a * b) == (a - b) + (b - a)
+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
@@ -554,7 +554,7 @@
As we can see later in this section this kind of
a total `Quantifier` has the basic properties that
elements of a
-vector space
+[@http://en.wikipedia.org/wiki/Vector_space vector space]
do provide.
We will use the terms `TotalQuantifier` and
@@ -620,15 +620,15 @@
``
-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
+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
+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
-SelfRemovability<Q,-,=v= >: Q a: a - a =v= Q()
+RightNeutrality<Q,-,== > : Q a; a-Q() == a
+SelfRemovability<Q,-,=v= >: Q a; a - a =v= Q()
``
For a `Quantifier` the same basic laws apply that are
@@ -647,16 +647,62 @@
`Qunatifiers` and the
modified `operator *`.
``
-SymmetricDifference<Q,== > : Q a,b,c: (a + b) - (a * b) == (a - b) + (b - a)
+SymmetricDifference<Q,== > : Q a,b,c; (a + b) - (a * b) == (a - b) + (b - a)
``
For a `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) == 0
+SymmetricDifference<Qt,== > : Qt a,b,c; (a + b) - (a + b) == (a - b) + (b - a) == 0
``
+[h5 Existence of an Inverse]
+By now Quantifiers `Q` are
+commutative monoids
+with respect to the
+operation `+` and the neutral element Q().
+If the Quantifiers `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 `TotalQuantifier` also 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 itl maps.
+
+[table
+[[] [is model of] [if] [example]]
+[[`Map<D,Monoid>`] [`Modoid`] [] [`interval_map<int,string>`]]
+[[`Map<D,Set,Trait>`] [`Set`] [`Trait::absorbs_neutrons`][`interval_map<int,itl::set<int> >`]]
+[[`Map<D,CommutativeMonoid>`][`CommutativeMonoid`][] [`interval_map<int,unsigned int>`]]
+[[`Map<D,CommutativeGroup>`] [`CommutativeGroup`] [`Trait::emits_neutrons`] [`interval_map<int,int,neutron_emitter>`]]
+]
+
+[endsect][/ Concept Induction]
+
[endsect][/ Semantics]
Modified: sandbox/itl/libs/validate/example/labat_single/labat_single.cpp
==============================================================================
--- sandbox/itl/libs/validate/example/labat_single/labat_single.cpp (original)
+++ sandbox/itl/libs/validate/example/labat_single/labat_single.cpp 2009-01-12 05:45:08 EST (Mon, 12 Jan 2009)
@@ -79,10 +79,10 @@
//LawValidater<TestLawT, RandomGentor> test_law;
//test_law.setTrialsCount(1000);
- //typedef InplaceInverseRemovability
- // <split_interval_map<int, int, neutron_enricher>, inplace_plus> TestLawT;
- //LawValidater<TestLawT, RandomGentor> test_law;
- //test_law.setTrialsCount(1000);
+ typedef InplaceInverseRemovability
+ <split_interval_map<int, int, neutron_emitter>, inplace_plus> TestLawT;
+ LawValidater<TestLawT, RandomGentor> test_law;
+ test_law.setTrialsCount(1000);
std::cout << "Start\n";
ptime start(microsec_clock::local_time());