ShEx semantics ill-founded

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 12:52:21 UTC