preliminary analysis of shape expressions proposal

-----BEGIN PGP SIGNED MESSAGE-----
Hash: SHA256

I spent some time yesterday and today looking over the Core SHACL Semantics
document http://w3c.github.io/data-shapes/semantics/

This is a new formal basis for a shapes/constraint language.

The language (in Section 2) is quite limited.  It includes closed shape
expressions and open shape expressions.  It has disjunction and a construct
called grouping.  It has cardinality ranges.  It has values and node kinds
and datatyping and facets.  It has inverse properties (which are not handled
in the semantics).  That's it.  In particular there is no conjunction of
shape expressions, and adding this conjunction would break a property of the
semantics.

The basic technical idea of the semantics is that nodes in a graph are
assigned zero or more shape labels and then the elements of these
assignments have to be backed up with local derivations that cover all the
outgoing edges from a node and are consonant with the shape labels assigned
to neighbouring nodes.  This gets around problems with ill-foundedness of
recursive shapes.


There are some minor problems with the proposal.

The language (Section 2) is very ambiguous.  The productions for
disjunction and grouping need to be modified to require them to be
disjunctions or groupings, respectively.

The abstract syntax used in Section 5 is different from that in Section 2.


There are some broken parts of the proposal.

There is a claim that disjunctive shape expressions are similar to logical
disjunction.  However disjunctive shape expressions here end up being quite
different from logical disjunction.  See below for more on this.


There are some serious problems with the proposal

There is no connection between how shapes are associated with data (Section
4) and the main part of the semantics (Section 5).

The semantics in Section 5 does not cover the full language from Section 2.
It is missing inverse triple constraints.  Adding inverse triple constraints
to the semantics appears to be problematic.

The semantics depends on witness mappings.  The definition of witness
mappings talks about triples appearing in the conclusion of applications of
the rule for the empty shape expression.  However, applications of this rule
do not include any triples at all.  I think that there is a simple
fix---using the rule for triple constraints instead---but that remains to be
verified.



Disjunctive shape expressions

Disjunctive shape expressions work differently from what one might expect.

For example, there is no valid typing for the shape expression schema
 S open { p , q } p E [1;1] | q E [1;1]
 E open { } empty
on the graph
 a p b .
 a q c .
that includes S in the shapes of a.


Open shape expressions

Open shape expressions work differently from what one might expect.

For example, there is a valid typing for the shape expression schema
 S open { p } p { b } [1;1]
on the graph
 a p b .
 a p c .
that includes S in the shapes for a.  However, there is no such valid typing
for either the shape expression schema
 S open { p } p { b , c } [1;1]
or the shape expression schema
 S open { p } p E [1;1]
 E open { } empty
-----BEGIN PGP SIGNATURE-----
Version: GnuPG v2

iQEcBAEBCAAGBQJVQ3vvAAoJECjN6+QThfjzOiYIAM+LjmGgimUKwucHkHjjKTfS
qw1gw9kVBiv1Gcdnyk1G7RY6JbQ5eHEJn8XyNIsTFhW68SSAZ5BggqwgoXgdaD/y
6VuS6yh1gWL2lQgliBDOaqUIhRU96Au+RBaLMnz+NNkGtW788qx0j8RhC+QktVmk
sAKV3g72l+8iNmxZrm6I4kcBSwfKuiVegSWztYS7AS6zkY8YjdqOf4MUNSd/9yFo
mNjwWSmLnIsv8r82A20HQZaHY/fFeNqlptTXlAgZCEcKns9oVaUyUMUncgk8ih24
GwmuNQL6OCYjeHAFE24hVwFl4JUctKTC66yVAvq/vQ6Nvf/GzOzeKfzZOKoBBWA=
=o8K5
-----END PGP SIGNATURE-----

Received on Friday, 1 May 2015 13:13:51 UTC