Hi,
In the concept proposal(s), what struck me as the most interesting
part was axioms. Unfortunately (to me), they were devoted least
attention in presentations and examples. Looking at different fora, I
can see I am not the only one who is missing information about axioms.
I tried to collect all information available in the web and provide a
digest. Here is the link:

       http://kojot.sggw.waw.pl/~akrzemi1/cpp/axioms/axioms_index.html

It might interest some people. Also, it is likely that my
understanding of axioms is incorrect; I would appreciate feedback.

Regards,
&rzej


--
[ comp.std.c++ is moderated.  To submit articles, try posting with your ]
[ newsreader.  If that fails, use mailto:std-cpp-submit@vandevoorde.com ]
[              --- Please see the FAQ before posting. ---               ]
[ FAQ: http://www.comeaucomputing.com/csc/faq.html                      ]

On Thu, 10 Mar 2011 at 07:22:02, in comp.std.c++, restor wrote:
>
>Hi,
>In the concept proposal(s), what struck me as the most interesting
>part was axioms. Unfortunately (to me), they were devoted least
>attention in presentations and examples. Looking at different fora, I
>can see I am not the only one who is missing information about axioms.
>I tried to collect all information available in the web and provide a
>digest. Here is the link:
>
>       http://kojot.sggw.waw.pl/~akrzemi1/cpp/axioms/axioms_index.html
>
>It might interest some people. Also, it is likely that my
>understanding of axioms is incorrect; I would appreciate feedback.

Is it really necessary to use the symbol  <=>  to mean equivalent in
value ?  It's too easily confused with equivalent meaning if and only
if.

In ordinary text,  f(a,a) <=> false  is more simply written as  =E6=9F=8F=
(a,a).

 John
--
John Harris


[ comp.std.c++ is moderated.  To submit articles, try posting with your ]
[ newsreader.  If that fails, use mailto:std-cpp-submit@vandevoorde.com ]
[              --- Please see the FAQ before posting. ---               ]
[ FAQ: http://www.comeaucomputing.com/csc/faq.html                      ]

On Thu, 10 Mar 2011 at 12:43:27, in comp.std.c++, John G Harris wrote:
>
>On Thu, 10 Mar 2011 at 07:22:02, in comp.std.c++, restor wrote:
>>
>>Hi,
>>In the concept proposal(s), what struck me as the most interesting
>>part was axioms. Unfortunately (to me), they were devoted least
>>attention in presentations and examples. Looking at different fora, I
>>can see I am not the only one who is missing information about axioms.
>>I tried to collect all information available in the web and provide a
>>digest. Here is the link:
>>
>>       http://kojot.sggw.waw.pl/~akrzemi1/cpp/axioms/axioms_index.html
>>
>>It might interest some people. Also, it is likely that my
>>understanding of axioms is incorrect; I would appreciate feedback.
>
>Is it really necessary to use the symbol  <=>  to mean equivalent in
>value ?  It's too easily confused with equivalent meaning if and only
>if.

If it can't be changed then one of your web pages should give the
meaning of the symbols that may be unfamiliar to some people.


>In ordinary text,  f(a,a) <=> false  is more simply written as  =E6=9F=8F=
>(a,a).

It seems that the keyboard's NOT symbol can survive e-mail but not
always news. Oh well.

   John
--
John Harris


[ comp.std.c++ is moderated.  To submit articles, try posting with your ]
[ newsreader.  If that fails, use mailto:std-cpp-submit@vandevoorde.com ]
[              --- Please see the FAQ before posting. ---               ]
[ FAQ: http://www.comeaucomputing.com/csc/faq.html                      ]

> Is it really necessary to use the symbol  <=>  to mean equivalent in
> value ?  It's too easily confused with equivalent meaning if and only
> if.

According to N2887, symbol <=> denotes "equivalence of expressions"
rather than equivalence of values, so, for example, the following
states a valid equivalence:

   cont.clear() <=> cont.erase( cont.begin(), cont.end() );

even though neither side is really a value (their return type is
void).

> In ordinary text,  f(a,a) <=> false  is more simply written as  =E6=9F=8F=
> (a,a).

Due to some text encoding I could not read the entire sentence. I
guess, the simpler you mention version read  !f(a, a). If so, it
should be noticed that according to N2887, the two assertions mean two
different, although related, things: "!f(a, a)" only says about the
value returned by the expression.  "f(a,a) <=> false" also says about
"f" itself, namely that it is "sort of" pure (or referentially
transparent).

If you say that this is wrong to expect of the programmers to
understand the subtle difference, then I guess you are right. I would
say this is a consequence of using a construct that looks like logic
algebra expressions in imperative language.

Regards,
&rzej


--
[ comp.std.c++ is moderated.  To submit articles, try posting with your ]
[ newsreader.  If that fails, use mailto:std-cpp-submit@vandevoorde.com ]
[              --- Please see the FAQ before posting. ---               ]
[ FAQ: http://www.comeaucomputing.com/csc/faq.html                      ]

Is there any place where I could find more about axioms? An axiom
syntactically looks like a function (block of statements):

concept C< typename T1, typename T2 >
{
  bool fun( T1, T2 );

  axiom A( T1 t, T2 u ) {
    fun(t, u);
  }
}

but it means something "for all t's in T1 and all u's in T2". Am I
correct?
This is clear as long as all the operations in the axiom have no side
effects, but what if they do? Consider:

axiom Ax( T t, U u ) {
   ++t = fun(++t); // assignment instead of comparison (will convert
to bool)
   (new T(u)) != nullptr; //
}

Is it a valid axiom? (at least syntactically). If so, how are side
effects treated?

Thanks,
&rzej

---
[ comp.std.c++ is moderated.  To submit articles, try just posting with ]
[ your news-reader.  If that fails, use mailto:std-c++@ncar.ucar.edu    ]
[              --- Please see the FAQ before posting. ---               ]
[ FAQ: http://www.comeaucomputing.com/csc/faq.html                      ]

Could anyone explain to me the practical value of axioms that come
with concepts?
Are they suppose to represent concept invariants that the
implementation is not required to check?
Can I lie in the axioms I define? E.g.:

concept SequentialContainer<typename T> {
    // size, begin, end, [], ...
    axiom Untrue(T cont) {
        cont.size() == 0;
    }
}

Is it going to be checked anywhere, or simply change someone else's
code to:

for( auto i = 0 ; i < 0 ; ++i ) // intended i < cont.size() but axiom
'optimized'
    cout << cont[i];


&rzej

---
[ comp.std.c++ is moderated.  To submit articles, try just posting with ]
[ your news-reader.  If that fails, use mailto:std-c++@ncar.ucar.edu    ]
[              --- Please see the FAQ before posting. ---               ]
[ FAQ: http://www.comeaucomputing.com/csc/faq.html                      ]

On Mar 28, 10:54 pm, "restor" <akrze...@interia.pl> wrote:
> Could anyone explain to me the practical value of axioms that come
> with concepts?

They allow one to express the semantic properties of concepts (and,
thus, the types that are intended to meet the requirements of the
concept), and allow verification and optimization tools to make use of
these properties.

> Are they suppose to represent concept invariants that the
> implementation is not required to check?

Yes.

> Can I lie in the axioms I define?

You lie to the compiler at your own peril, just like your example
below shows.

> E.g.:
>
> concept SequentialContainer<typename T> {
>     // size, begin, end, [], ...
>     axiom Untrue(T cont) {
>         cont.size() == 0;
>     }
>
> }
>
> Is it going to be checked anywhere, or simply change someone else's
> code to:
>
> for( auto i = 0 ; i < 0 ; ++i ) // intended i < cont.size() but axiom
> 'optimized'
>     cout << cont[i];

Compilers aren't required to do anything with axioms other than parse
them. The compiler could complain about your axiom being wrong, or it
could "optimize" the code as above, or both, or nothing.
Axioms are a way to pass on semantic information that only the author
of the concept can know ("extrinsic" semantic properties) to the
compiler, optimizer, and other software development tools. Use it
where it helps, abuse it at your peril.

  Cheers,
  Doug

---
[ comp.std.c++ is moderated.  To submit articles, try just posting with ]
[ your news-reader.  If that fails, use mailto:std-c++@ncar.ucar.edu    ]
[              --- Please see the FAQ before posting. ---               ]
[ FAQ: http://www.comeaucomputing.com/csc/faq.html                      ]

Can axioms be freely used with auto concepts?
I would see an auto peril in such cases. If we make a Semigroup from
the proposed concept text an auto concept:

  auto concept Semigroup<typename Op, typename T> {
      T operator()(Op, T, T);
      axiom Associativity(Op op, T x, T y, T z) {
          op(x, op(y, z)) == op(op(x, y), z);
      }
  }

We risk any function object taking two same arguments inadvertently
becoming a Semigroup and very likely violating the axiom.

&rzej

---
[ comp.std.c++ is moderated.  To submit articles, try just posting with ]
[ your news-reader.  If that fails, use mailto:std-c++@ncar.ucar.edu    ]
[              --- Please see the FAQ before posting. ---               ]
[ FAQ: http://www.comeaucomputing.com/csc/faq.html                      ]

On Mar 30, 1:08 am, "restor" <akrze...@interia.pl> wrote:
> Can axioms be freely used with auto concepts?
> I would see an auto peril in such cases. If we make a Semigroup from
> the proposed concept text an auto concept:
>
>   auto concept Semigroup<typename Op, typename T> {
>       T operator()(Op, T, T);
>       axiom Associativity(Op op, T x, T y, T z) {
>           op(x, op(y, z)) == op(op(x, y), z);
>       }
>   }

The problem here is that you should NOT let Semigroup be an auto
concept in the first place. So the question of whether the axiom here
could be problematic becomes irrelevant.

>
> We risk any function object taking two same arguments inadvertently
> becoming a Semigroup and very likely violating the axiom.

---
[ comp.std.c++ is moderated.  To submit articles, try just posting with ]
[ your news-reader.  If that fails, use mailto:std-c++@ncar.ucar.edu    ]
[              --- Please see the FAQ before posting. ---               ]
[ FAQ: http://www.comeaucomputing.com/csc/faq.html                      ]