Re: [Core] new definition of safeness

From: Jos de Bruijn <debruijn@inf.unibz.it>
Date: Mon, 04 May 2009 18:37:33 +0200
Message-ID: <49FF19CD.4040305@inf.unibz.it>
To: Sandro Hawke <sandro@w3.org>
CC: RIF <public-rif-wg@w3.org>
```

Sandro Hawke wrote:
>> I also finished the definition of strong safeness:
>> http://www.w3.org/2005/rules/wiki/Core#Strong_Safeness
>>
>
>
>
>> ...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
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

```
Received on Monday, 4 May 2009 16:38:26 GMT

This archive was generated by hypermail 2.2.0+W3C-0.50 : Tuesday, 2 June 2009 18:34:08 GMT