RE: Comments on "normal form" of policy expressions

>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

The WG considered your mail on May 2nd 2007 conference call and decided not to take any action [1].

Last September, the WG considered a similar request (3621 [2]) to describe policy normalization using a formal methodology. The WG didn't express any interest and didn't find any value added by such an exercise [3].

To be successful, formalization has to be a work item that the whole WG should take on. Please note that there isn't a formal methodology that is common to all the participants in the WG. There are n-ways to formalize - such as Z, UML, OWL and custom notations.

Participants and reviewers may use their favorite formal methodologies. When they indulge in such exercises, they might discover issues in the underlying algorithm or data model. The most important part is to convert these discoveries into actionable issues for the WG. We encourage you to do the same.

/paulc

[1] http://www.w3.org/2006/09/14-ws-policy-minutes.html#item02
[2] http://www.w3.org/Bugs/Public/show_bug.cgi?id=3621
[3] http://www.w3.org/2007/05/02-ws-policy-minutes.html#item12

Paul Cotton, Microsoft Canada
17 Eleanor Drive, Ottawa, Ontario K2E 6A3
Tel: (613) 225-5445 Fax: (425) 936-7329
mailto:Paul.Cotton@microsoft.com




________________________________
From: public-ws-policy-request@w3.org [mailto:public-ws-policy-request@w3.org] On Behalf Of David Hull
Sent: May 1, 2007 1:13 AM
To: public-ws-policy@w3.org
Subject: 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(p1, p2 ... pn) if the expression is <All>pexpr1 pexpr2 ... pexprn</All>, where expression pexpri denotes policy pi and distrib takes the one-from-column-a-one-from-column-b Cartesian product described under "distributive".
 *   [[a1][a2]...[ak]] if the expression is <ExactlyOne>pexpr1 pexpr2 ... pexprn</ExactlyOne> and the aj are the alternatives of the policies the pexpri 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.