recursive shapes (and negation)

-----BEGIN PGP SIGNED MESSAGE-----
Hash: SHA1

On 03/15/2015 07:07 PM, Eric Prud'hommeaux wrote:
>>>> The specification appears to be ill-founded on recursive shapes
>>>> over data loops.  I can't tell for sure because there is no formal
>>>> basis.
>>> 
>>> We can add a set visited:([node,shape]) to the shape matches function
>>> to provide an opperational strategy for eliminating infinite
>>> recursion. Is that useful in the this semantics?
>> 
>> Well something is needed.  Otherwise it is not possible to determine
>> what should be happening.
> 
> Fair enough. I'll cook some text up tomorrow. It would be nice to work 
> out in advance some form strategy for negation e.g. stratification. Do 
> you have an approach that yields a reasonably intuitive behavior for:
> 
> <Sh1> { !:p1 @<Sh1> }
> 
> ? Can you cook up a realistic example to check the intuition?

I don't think that stratification is very helpful.  Your example above is
not stratified, and I think that it is an example of the most common
interaction between recursion and negation.


One way of handling recursive shapes is via a model theory.  The model
theory just says that needs to be, not what needs to happen, so it can
escape from having to terminate a potentially unending computation.  In a
model theory, recursive shapes (as well as definitions) can be handled in
several ways.  One way is to do nothing - recursive shapes work just like
everything else.  However, here recursive shapes generally generate multiple
models.  Another way is to maximize or minimize recursive shapes.  If there
is no negation, then there is generally unique maximum and minimum, which is
good.  However, in the presence of negation, there can be multiple maxima
and minima, i.e., multiple models, which may not be tolerable.


There are multiple simple examples that show the problems.  Consider
  <Sh1> { !:p1 @<Sh1> }
with the graph
  ex:a :p1 ex:b .

What belongs to <Sh1>?  There are two different possibilities.  Either ex:a
belongs to <Sh1> or ex:b belongs to <Sh1>.  However, they both can't belong
to <Sh1> and similarly they can't both not belong to <Sh1>, at least not
without violating the intuitive meaning of <Sh1>.

Now you could pop up a level and say that all this means that neither ex:a
nor ex:b belongs to <Sh1> because there are setups where ex:a does not
belong to <Sh1> and there are setups where ex:b does not belong to <Sh1>.
So far, so good, but note that there is a reasoning-by-cases being done
here, which can be very computationally expensive.


So what should be done for recursive shapes, particularly if you can't step
back from procedural specifications into something like a model theory?
Well, that's the task of whoever is producing the specification for SHACL,
but any specification for SHACL is only going to succeed if it has a story
for recursive shapes.

By the way, my story for recursive shapes is that they should not be allowed
in SHACL at all.

peter
-----BEGIN PGP SIGNATURE-----
Version: GnuPG v1

iQEcBAEBAgAGBQJVBt49AAoJECjN6+QThfjzveAIAJUZ2KQS4S6j1Cy3jzD8PyH1
OMcmf2n/B45zd+xxO9nudyydQJgyfbUbidIgg9pV3939qlVAgPp+RwdeqLLjKnrL
MrThr0AlutbtSgQ1eOVt5uTE6TWVAHXyw3p0FNKamGkEAxt0WnCnvbNQk5cVPP1h
N6T+6crzIgyBzeaJXByXx+ZxMSxQ+rItt3+An3hrTjx5rGhUrtunAf4gMuqD9WJ9
PBeV/a3maO4VIwtNs5zx+dPTWyqy/hOiAjai6rG/DiuzDhSktlf4hjykIFMBybZJ
E5dHAsp3iXK3biSmbUms47HNQiAvrKqN78Oqr7THasQngYKJqrwovzOug667880=
=ziWH
-----END PGP SIGNATURE-----

Received on Monday, 16 March 2015 13:44:59 UTC