Re: SHACL abstract syntax or functional specification

On Sun, Mar 15, 2015 at 8:53 PM, Arthur Ryman <arthur.ryman@gmail.com>
wrote:

> Jose,
>
> Sorry for the delayed response. Thanks for taking a stab at a
> semantics document. I scanned your spec at
> http://labra.github.io/Haws/shacl/


Thank you very much for reviewing it.

I have started an updated version of that document based on Eric's SHACL
language proposal. The new version is here:

http://w3c.github.io/data-shapes/semantics/Axiomatic

1. The spec says:
>
> Schema ::= Label Shape * // Schema associates a Label with a Shape
>
> You are using a some informal syntax. I assume a Schema is actually a
> mapping that associates each Label in some set with some Shape. If so,
> then should't the grammar be:
>
> Schema ::= (Label Shape) *           // Schema associates a Label with a
> Shape
>
> You'd also need a constraint that no Label is associated with more
> than one Shape.
>

You are right.  I changed the abstract syntax according to your suggestion.

2. Your syntax does not make it apparent the difference between
> terminal and non-terminal symbols. I assume Empty, And, Or, Arc,
> InvArc are terminal symbols.
>

Yes, they are.

3. Your formal semantics is defined as interpreting a Schema as a
> mapping from the nodes of a graph to types, where I believe you are
> calling the Label's types?


Yes. They could also be called "Shapes" but I though types was better.

I don't think this is a very natural
> semantics. It's more like XML post-schema validation.


Indeed, it could also be used to generate some kind of post-schema
validation data structure.

The natural
> semantics is as constraints. Given a node in a graph and a shape, the
> node either satisfies the shape or not.
>

Well, in fact, that's what it means. The rule succeeds if the node matches
the shape, but it also returns the shape typings, the checked triples and
the remaining triples.

Those 3 data structures are needed during the matching process but they
could optionally be avoided if the user is only interested in a yes/no
answer.

>
> 4. The operation removeTriple(ts) does not match its description. Are
> you missing an argument, i.e. removeTriple(t, ts)?
>

No, the operation takes a set of triples ts as argument and returns a pair
(t,ts') where t is the triple removed and ts' the rest of triples.


> 5. My preference is to use a real formal specification language that
> can be machine-checked, e.g. Z, if you want to claim formality.


Yes, I also prefer a more formal approach. The axiomatic semantics has been
implemented in Haskell and partly in Prolog. These days, I am starting to
port it to Coq (although it may take some more time given my current
teaching duties). But anyway, I would not object to use also Z as the
specification language.

Many
> of the errors I identified would be caught immediately by a
> type-checker like fuzz.
>

Sure, and I would appreciate if you report me those errors. The main
problem is that the axioms are manually HTMLized and it is quite possible
that I introduce some errors in that process.

The axiomatic semantics proposal is a first attempt and I assume that it
may not be perfect. However, I really think the best way to go is to
identify the core language constructs be means of an abstract syntax and to
define them in a formal way.

Best regards, Jose Labra


> -- Arthur
>
>
>
> On Mon, Mar 2, 2015 at 12:14 AM, Jose Emilio Labra Gayo
> <jelabra@gmail.com> wrote:
> > One of the already approved requirements is that SHACL should be a higher
> > level language.
> >
> >
> > To do that, my understanding is that we have to define an abstract
> syntax or
> > functional specification which describes the main constructs of the
> > language.
> >
> >
> > Most language specifications are defined based on that abstract syntax.
> For
> > example:
> >
> >
> > RDF Abstract Syntax and concepts (http://www.w3.org/TR/rdf11-concepts/)
> >
> > SPARQL (http://www.w3.org/TR/sparql11-query/#sparqlDefinition)
> >
> > OWL (http://www.w3.org/TR/2012/REC-owl2-syntax-20121211/)
> >
> >
> > I proposed an abstract syntax for SHACL here:
> >
> >
> > http://labra.github.io/Haws/shacl/
> >
> >
> > which is of course open to comments/feedback.
> >
> >
> > There are multiple advantages of defining an abstract syntax for
> describing
> > a language like separation of concerns, allowing the language designers
> to
> > concentrate on the language concepts instead of syntactic details,
> > identification of possible redundant constructs, etc.
> >
> >
> > I also proposed that the Shacl spec should have a section about the
> abstract
> > syntax.
> >
> >
> > However, I found this answer from Holger:
> >
> >
> > “I don't think any Abstract Syntax is needed or helpful. SHACL is already
> > self-contained using SPARQL.”
> >
> >
> > I start this as a separate thread to remark that this is for me a very
> > important topic. I really don’t understand why having an abstract Syntax
> is
> > not needed for Shacl or why it will be unhelpful.
> >
> >
> > If the reason is that SHACL is self-contained using SPARQL, then my
> > understanding is that we are not defining a higher level language at all.
> >
> >
> > --
> >
> > -- Jose Labra
> >
>



-- 
-- Jose Labra