Re: ShEx semantics ill-founded

Dear all,

I've answered the issue pointed out by Peter in another mail earlier today, which unfortunately was not posted to the list immediately because of sender's mail mismatch (I didn't send it with the right e-mail address).

Peter, the "solution" that you propose here is precisely what I explained to you in private mails earlier this week, and that is what will be made explicit in the spec shortly, as I promised in my other mail to the public-shex list.

Anyways, thank you for your careful reading of the ShEx spec.
I will let you know when the fix is done and will be happy to have your comments on it.

Best regards,
Iovka

 
 
Le Vendredi 23 Mars 2018 13:51 CET, "Peter F. Patel-Schneider" <peter.patel-schneider@nuance.com> a écrit: 
 
> The ShEx semantics in http://shex.io/shex-semantics/ is ill-founded.  There
> are many simple cases of recursive shapes where the semantics gets into an
> infinite loop trying to determine values for satisfies.  This is a serious,
> fundamental flaw in the semantics.
> 
> The simplest case is just
>   S = :s @:s
>   G = { :x :p :x }
>   m = { ( :x, :s ) }
> where determining whether G conforms with S with m requires (from Section
> 5.6.1) checking satisfies(:x,:s,G,m) but the portion of the definition of
> satisfies in Section 5.3.2 says that this is defined as
> satisfies(:x,:s,G,m), which is ill-founded.
> 
> There are also simple ill-founded cases where the recursion is through a
> triple constraint, such as
>   S = :s { :p @:s }
>   G = { :x :p :x }
>   m = { ( :x, :s ) }
> Here there is an added step of checking out the triple constraint, whose
> semantics is given in Section 5.5.2, but here again satisfies(:x,:s,G,m)
> depends on satisfies(:x,:s,G,m), which is ill-founded.
> 
> The obvious solution to this problem is to have the semantics of
> shapeExprRef use the shape map, i.e., change the bit of Section 5.3.2 from
> "Se is a shapeExprRef and there exists in the schema a shape expression se2
> with that id and satisfies(n, se2, G, m)" to "Se is a shapeExprRef to shape
> id and m(n,id)".  The fact that currently the last argument of satisfies is
> not currently used also strongly points to this as being the obvious way to
> fix the semantics.
> 
> This change makes the above two example valid.  It also gives an intuitive
> meaning to negation, making the following valid
>   S = :s { :p @:s }
>       :t NOT @:s
>   G = { :x :p :x }
>   m = { ( :x, :t ) }
> 
> 
> 
> peter
>

Received on Friday, 23 March 2018 16:16:55 UTC