Re: Comments on "normal form" of policy expressions

I'm a bit confused by this reply.

I've never advocated formalizing policy expression normalization in Z,
UML, OWL or any other such notation.  I'm not even sure how one would
use, say, UML to formalize it.  I advocate /getting rid/ of the section
on normalizing expressions and replacing it with a much shorter section
showing how to find the policy that a given policy expression
expresses.  I also point out that with this done, the section on
normalizing policy expressions could be moved into, say, the primer,
since the normalization rules would follow from the fact that equivalent
expressions express the same policies.  Assuming that anyone wants to
normalize expressions.

Put another way: WSP defines two main concepts: Policies and policy
expressions.  It does not clearly answer the question: What policy does
a given policy expression express?  It should, of course, and if it does
there is no great need for a section on normalizing expressions.

As to actionable issues, I'm sure you're aware I've submitted several. 
So far these have been aimed mainly at answering some simple questions
about policies themselves.  For example, exactly what is the meaning of
policy intersection (4553) and in what ways is it and is it not
extensible (4554).  There is also the overall question of whether
policies and alternatives are sets or bags.

Once these are nailed down, it should be simple to define a mapping from
policy expressions to policies.  As far as I can tell it would require
three statements of the form "The expression
<ExactlyOne>...</ExactlyOne> represents the policy ...".  The rule for
<All> would be the longest, as it has to talk about distribution, but
even this doesn't seem onerous.   The sketch I gave below takes about a
dozen lines.

I suppose this could be formalized further using Z or some other such
notation, but I would certainly not insist on such an approach.

Paul Cotton wrote:
>
> >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 2^nd 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/(/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.
>