# Comments on "normal form" of policy expressions

From: David Hull <dmh@tibco.com>
Date: Tue, 01 May 2007 01:13:29 -0400
Message-ID: <4636CC79.7050501@tibco.com>

```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.
```
Received on Tuesday, 1 May 2007 05:13:45 UTC

This archive was generated by hypermail 2.3.1 : Tuesday, 6 January 2015 20:38:34 UTC