Re: Questions on normal forms

First, note that the third form you give is identical to the initial
form.  How do we know not to loop around again?

In any case, I don't see how the distributive rule applies where you say
it does.  If it does apply, why is the result what you give? Why would
it be that and not, say

<wsp:ExactlyOne><!-- Distribute All over ExactlyOne and leave the other child alone -->
  <wsp:All>
   <A/>
  <wsp:All>
  <B/>
</wsp:ExactlyOne>

This brings up broader concerns about the distributive rule, which I was
going to mention separately since as far as I could tell that rule
didn't apply here.  But that's the problem: how do you tell?

The section on the distributive rule makes two apparently normative
statements, one very vague:

    * |wsp:All| distributes over |wsp:ExactlyOne|
    * Distributing |wsp:All| over an empty |wsp:ExactlyOne| is
      equivalent to no alternatives

There are also several examples.  In all examples the surrounding All
element contains only ExactlyOne children, as one would expect from the
first statement.  There is nothing to suggest that the rule would apply
in the case of an All with (for example) one child an assertion and one
ExactlyOne.

Examples are generally non-normative anyway.  It's hard to see how these
particular ones could be normative.  Read literally they might say "All
containing ExactlyOne containing two arbitrarily named alternatives is
equivalent to ExactlyOne containing All containing the same two
alternatives," and so forth, but this is clearly not what is meant.

Read more intuitively, they suggest a general Cartesian product rule, by
which (informally speaking) the general form

<All>
  <ExactlyOne>expr-1-1 expr1-1-2 ... expr-1-n1</ExactlyOne> <!-- n1 >= 0 -->
  <ExactlyOne>expr-2-1 expr1-2-2 ... expr-1-n2</ExactlyOne> <!-- n2 >= 0 -->
  ...
  <ExactlyOne>expr-m-1 expr-m-2 ... expr-m-nm</ExactlyOne> <!-- m >= 1,
nm >= 0 -->
</All>

is equivalent to

<ExactlyOne>
  <All>expr-1-1 expr2-1 ... expr-m-1</All>
  <All>expr-1-2 expr2-1 ... expr-m-1</All>
  ...
  <All>expr-1-n1 expr2-1 ... expr-m-1</All>
  ...
  <All>expr-1-1 expr2-2 ... expr-m-1</All>
  <All>expr-1-2 expr2-2 ... expr-m-1</All>
  ...
  <All>expr-1-n1 expr2-2 ... expr-m-1</All>
  ...
  <All>expr-1-1 expr2-1 ... expr-m-nm</All>
  <All>expr-1-2 expr2-1 ... expr-m-nm</All>
  ...
  <All>expr-1-n1 expr2-1 ... expr-m-nm</All>
</ExactlyOne>

(The text suggests that this is generally the result of "repeatedly
distributing", but what are the intermediate forms and how would the
rule produce them?)

This is a specification, and indeed one that takes the unusually formal
approach of defining a set of axioms.  One should not have to infer
rules from examples.  One should certainly not have to refer to existing
implementations to clarify rules.  The whole point is to capture
abstractly the behavior of existing or future implementations.

I would strongly suggest formalizing the examples given into a normative
rule using the term "Cartesian product", limiting its applicability to
cases matching the form given above (i.e, All containing only ExactlyOne
children) and adding a "Promotion" rule (or whatever the WG wants to
call it) for bringing loose assertions into the fold.

As I understand it, this would

    * Be specific where the existing text is vague.
    * Cover (in conjunction with the other rules) all combinations of
      All, ExactlyOne and loose assertions.  It would even be possible
      to prove this by the usual case analysis.
    * Capture the de facto standard behavior.



Asir Vedamuthu wrote:
> Let's look at your second example. The second example with the Policy wrapper is:
>
> <wsp:Policy>
>  <wsp:All>
>   <wsp:ExactlyOne>
>    <A/>
>   </wsp:ExactlyOne>
>   <B/>
>  </wsp:All>
> </wsp:Policy>
>
> Policy is equivalent to All. That is,
>
> <wsp:All>
>  <wsp:All>
>   <wsp:ExactlyOne>
>    <A/>
>   </wsp:ExactlyOne>
>   <B/>
>  </wsp:All>
> </wsp:All>
>
> Applying the idempotent rule,
>
> <wsp:All>
>  <wsp:ExactlyOne>
>   <A/>
>  </wsp:ExactlyOne>
>  <B/>
> </wsp:All>
>
> Applying the distributive rule,
>
> <wsp:ExactlyOne>
>   <wsp:All>
>    <A/>
>    <B/>
>   <wsp:All>
> </wsp:ExactlyOne>
>
> We checked with a few online policy tools and our command line tool. They all consistently produced the above result. We hope this helps.
>
> Regards,
>
> Asir S Vedamuthu
> Microsoft Corporation
>
>
>
>
> From: public-ws-policy-request@w3.org [mailto:public-ws-policy-request@w3.org] On Behalf Of David Hull
> Sent: Tuesday, May 29, 2007 12:52 PM
> To: public-ws-policy@w3.org
> Subject: Questions on normal forms
>
> As far as I can tell, the following are valid compact expressions.
> 1. What are their normal forms?
> 2. By what rules are those normal forms computed?
> <wsp:ExactlyOne>
>   <wsp:All><A/></wsp:All>
>   <B/>
> </wsp:ExactlyOne>
>
> <wsp:All>
>   <wsp:ExactlyOne><A/></wsp:ExactlyOne>
>   <B/>
> </wsp:All>
>