NEW ISSUE: (3621) Formal semantics

Title -
         Formal semantics

Description -
         Much of the language of the framework specification talks as if
WS-Policy is a logic (e.g., reason about, logical construct, etc.)  
and yet the
semantics are specified informally, and in no concentrated place.  
Furthermore,
certain aspects of the semantics seem unspecified (e.g., the precise  
meaning of
exactlyOne; first order exclusive disjunction, that + some sort of  
close world
assumption, etc.).

Justification -
         Clarity and completeness of a specification are always  
critical.
Formalization does not *always* help clarity, at least for a wide  
audience, but
WS-Policy is simple enough that the semantics should be reasonably  
accessible
to anyone who understands truth tables.

         Secondly, if the semantics are as I believe (roughly  
propositional
logic or a very simple description logic) then we gain access to the  
wealth of
tools and algorithms available for these logics. SAT solvers and DL  
reasoners
are highly optimized and used in all sorts of industrial settings.

         Thirdly, various sorts of analysis become easier if we have  
a clear
semantics. On this page:
                 <http://www.mindswap.org/2005/services-policies/>
are some papers and presentations showing how to discover policy  
containment,
equivalence, disjointness, and incoherence.

         Furthermore, certain behaviors of the operators are specified
individually (e.g., commutativity, etc.) that would follow from a normal
semantics for the operators (e.g., logical and is commutative, etc.)  
I think
this would simplify the spec.

Target -
         framework

Proposal -
         Let's consider normal form only for the moment.

         I will do it only propositionally at the moment.

         Policy assertions correspond to propositional variables,  
aka, atomic
sentences. There are an infinite number of them.

                 <all>P1...Pj</all> is true just in case for i = 1 to  
j, Pi is
true.
                 <exactlyOne>A1...Ak</exactlyOne> is true just in  
case for some
i=1 to k, Ai is true and for an m != i, Am is false.

         (Now, when we introduce a policy subject, the propositional  
letters
become one place predicates, but that is easily handled.)

         Clearly this isn't a lot of text, though there are  
additional details.
I just wanted to give a flavor.

         For example, it's easy to show that <all> is communtative, and
associative (the truth conditions are independent of order or grouping)

Received on Friday, 25 August 2006 11:17:39 UTC