Comments on "normal form" of policy expressions

Hello WSP-ers,

I'm sending this at the urging of the WSA group, with the understanding
that with WSP in CR, there is a limit to what, if anything can be done.

A large portion of section 4 of WS-P concerns the "normal form" of a
policy expression.  There are several points to be made here.  In what
follows, in order to compare more easily to more conventional notation
(and, frankly, to save typing) I will write /a*b*c .../ for
<All><A/><B/><C/></All> and /a+b+c/ for the case of ExactlyOne, with
parentheses for grouping.  I'll use (*a) for <All><A/></All>, (*) for
<All/> (if it comes up) and likewise for (+a) and (+) if they come up.

    * When describing a normal form, one typically speaks of
      /reductions/ (or /expansions/), not of equivalences.  The spec
      takes  a somewhat less direct approach, saying "this is what a
      normal form looks like" and "the following kinds of expressions
      are equivalent".  It is /implied/ that any given expression is
      equivalent to at least one expression in normal form, and examples
      are given that can be taken to indicate reductions, but no proof
      is given that every expression has a normal form.  Such a proof
      would be provide reassurance that no corner cases had been missed,
      and would be much easier if the rules followed the grammar of
      policy expressions (i.e., separate cases for assertions, All and
      ExactlyOne). But see below.
    * It is not immediately clear to what extent terms such as
      "associative" are used in their usual senses.  The usual
      mathematical definition of associativity (of a /binary/ operator)
      is /a*(b*c) = (a*b)*c./  When an operator is associative,
      parentheses may be dropped with the understanding that /a*b*c/ is
      shorthand for the equivalence class {/a*(b*c), (a*b)*c/}.  Here we
      are told that /a*(*b) = a*b/ ("for example").  We can reasonably
      infer that /a*(b*c) = a*b*c./  Is /(a*b)*c/ also equivalent to
      /a*b*c/?  This is not a spurious question, as the distinction
      between /left associativity/ and /right/ /associativity/ matters
      in parsing in general.  As it happens, it doesn't matter here,
      since /(a*b)*c = c*(a*b) = c*a*b = a*b*c/, applying the examples
      we already have or have inferred but I seriously doubt that such
      manipulation was the intent of the committee in invoking
      "associative" and "commutative".
    * It is even less clear /why/ such prominence is given to these
      terms.  The implication is that there is some important
      commonality being captured, but do I really expect to spend time
      going through, say, a WSDL file and rewriting /a+b/ as /b+a/?  As
      it is, organizing the exposition around these terms serves more to
      distract than to inform.

Assuming we have defined a normal form, what is its purpose?  The
"expanded" form of a "compact" expression can quickly grow unwieldy,
thanks to distribution.  It seems clear that such a form is not meant to
be the sole representation used by real processors.  The spec says it
SHOULD be used where feasible, for simplicity and interoperability,
though it's not clear to what extent those are promoted when there is no
guarantee of normality.  Rather, normal form seems most useful in
specifying semantics, in particular, which policy expressions are
equivalent.

But the meaning of an expression is (or at least ought to be) exactly
the policy that it denotes.  Expressions are equivalent iff they denote
the same meaning, in this case the same policy.  Given that policies are
"the truth" and policy expressions are just their realization in angle
brackets, the spec will need to define the mapping from policy
expressions to policies.  Yet this does not seem to be done.  There is
instead the implication that policy expressions in normal form map to
actual policies in the intuitive way (only the reverse mapping is given,
and that informally), and that every policy expression is equivalent to
some normal form, and thus to some policy.

If we /did/ have such a semantic map from policy expressions to
policies, there would be no obvious need for a normal form for
expressions.  If there were such a need, an expression could always be
canonicalized by computing the policy it denotes and then producing the
angle brackets as described at the top of section 4.

How does one compute the policy an expression denotes?  Leaving nested
assertions as an exercise and using square brackets to denote
collections, I believe the mapping is essentially

    * [[/a/]] if the expression is an assertion /a/.  That is, a policy
      consisting of a single alternative containing /a/.  This form
      won't appear on its own, but will appear in recursively processing
      the other two forms.
    * /distrib/(/p_1 , p_2 ... p_n )/ if the expression is
      <All>/pexpr/_/1/ /// pexpr/_/2/ / ... pexpr/_/n/ </All>, where
      expression /pexpr/_/i/ denotes policy /p/_/i/ and /distrib/ takes
      the one-from-column-a-one-from-column-b Cartesian product
      described under "distributive".
    * [[/a/_/1/ ][/a/_/2/ ]...[/a/_/k/ ]] if the expression is
      <ExactlyOne>/pexpr/_/1/ / pexpr/_/2/ / ... pexpr/_/n/
      </ExactlyOne> and the /a/_/j/ are the alternatives of the policies
      the /pexpr/_/i / denote.  That is, make a policy of all the
      alternatives found in all the child expressions.

I may well have missed some subtleties, but this approach appears to
produce the same results as the spec.  One could also take a more
strongly-typed approach of mapping assertion elements to assertions,
<All/> elements to alternatives and <ExactlyOne/> elements to policies. 
The overall case analysis remains the same either way.  In such an
analysis, it's easy to check whether all possible expressions are
covered.  There is no need to worry about commuting and associating or
idempotence.  Just go by induction as usual.