Re: [Core] new definition of safeness

Sandro Hawke wrote:
>> I also finished the definition of strong safeness:
>> http://www.w3.org/2005/rules/wiki/Core#Strong_Safeness
>>
>> please have a look.
> 
> 
> 
>> ...and membership formulas a#b and ternary, respectively binary
>> predicate symbols, and so (->,3),(#,2) ...
> 
> I think you mean:
> 
>    ...and membership formulas a#b, respectively, as ternary and binary
>    predicate symbols (->,3) and (#2) ...

Right

> 
> That was about as far as I got.  Well, actually, I got as far as
> "(?V,?V') ∈ E and {f1, ..., fn} ∈ L'((?V,?V'))" before I gave up.
> Personally, I'd prefer pseudocode, but if others in the group can
> actually read this definition and be confident it's correct, then I can
> live with that.

Let's hope more people will try to read it.
Well, what's written there is nearly pseudocode.  Basically, you first
check all the equality atoms for ?V (first bullet of first list), for
every variable ?V' that appears in the term on the other side of the
equality you add an edge, and you label that edge with the set of
function symbols in which ?V' appears.  For example, if you have
add(subtract(?V',divide(?X,?Y)),?Z), ?V' appears in add and subtract.
Then, you check whether ?V appears in a possibly unbound position in an
external atomic formula, and, if so, you similarly add edges and label
them.  Now, it may happen that you labeled the same edge more than once,
e.g., because ?V appears in two different externals.  What you do then
is take the smallest label, and if there are several smallest labels,
you take their union.

I think the dependency graph of a set of implications should be easier
to construct.


> 
> Also, as I understand
>   http://www.w3.org/2005/rules/wg/meeting/2009-04-16#resolution_2 
> this shouldn't be at risk, and should be labeled as "informative" (or
> "non-normative"), although I guess that ACTION-749 was on Axel.

Right. Done.


Best, Jos

> 
>       -- Sandro
> 
> 

-- 
+43 1 58801 18470        debruijn@inf.unibz.it

Jos de Bruijn,        http://www.debruijn.net/
----------------------------------------------
Many would be cowards if they had courage
enough.
  - Thomas Fuller