Re: First steps on SPARQL Update formal model

Hi,

On 30 Aug 2010, at 22:08, Andy Seaborne wrote:

> 
> 
> On 30/08/10 17:33, Alexandre Passant wrote:
>> Hi all,
>> 
>> I've committed first steps of the SPARQL Update formal model in CVS.
>> It's available at http://www.w3.org/2009/sparql/docs/update-1.1/Overview.xml#sec_formalmodel for comments.
>> 
>> So far it covers only the general definitions (GraphStore, GraphStoreState and UpdateOperation) and operations dealing with graph management (CreateOperation and DropOperation).
>> Before going further, I'd like to get comments / feedback of the group, especially Andy + Steve to be sure it fits with definition of SPARQL Query, and Chimezie re. definitions in the Update document - while I checked both when doing that formal model, but feedback is welcome.
>> 
>> Best
>> 
>> Alex.
>> 
> 
> Hi Alex,
> 
> Makes sense to me.
> 
> [[
> Definition: GraphStore
> 
> A GraphStore GS is a mutable container of RDF graphs.
> It has one unnamed (default) slot and zero or more named slots identified by an IRI <i>.
> Each slot holds an RDF graph.
> 
> GS = (<DG>, {(<i>, <G_i>)})
> ]]
> 
> Typographical: (don't want <> around - it's not an IRI)
> <DG>  ==> DG
> <G_i> ==> G_i
> 

Fixed

> [[
> Definition: CreateOperation
> 
> A CreateOperation OpC is an UpdateOperation in which (1) a new named slot <j> and (2) a new graph are created in the GraphStore. The new graph is held in the new slot. Other slots and graphs are not affected.
> 
> OpC(GSS(GS, t)) = (S(DG, t), {(<i>, S(G_i, t)}, (<j>, S(G_j, t+1))
> ]]
> 
> I think OpC needs to take some argument so we can talk about them on the RHS.

Makes sense, I've added the following the the update operation definition:

""It can accept some arguments""

>  (As an side-effect or writing like that, I don't think the t is needed at all but I've left them in below)

> 
> Something like:
> 
> OpC(<IRI>, silent, (S(DG, t+1), {(<i>, S(G_i, t+1)})) =

If keeping the timestamp, I'd rather use t on the left side, and got t+1 as a result on the right side
So OpC(<IRI>, silent, GSS(GS, t)) = something_at_t+1
But t might indeed be not needed anymore
 
> 
>  if <IRI> is one of <i> for some <i> in GS
>    if !silent then error else ;
>  if <IRI> is not one of <i> for any <i> in GS
>    (S(DG, t), {<i>, (G_i, t)} union {(<IRI>, {}, t+1))
> 
> that is, union a new pair into the named graph state of the graph store (this is the non-error, non-silent case).

Should silent be in the formal model ?
To me, it's more from the implementation pov, as it having it or not does not make any change to the graph state after the operation.

OpC(<IRI>, silent, GSS(GS, t)) = GSS(GS, t) UNION (<IRI>, {}_t+1)

W/o timestamp, that will be

OpC(<IRI>, silent, GSS(GS)) = GSS(GS) UNION (<IRI>, {})

Might be indeed clearer

> 
> It'll have to OpCreate, not OpC as we have OpClear as well.

Fixed

> 
> For OpDrop:

(checking as well w/o timestamp, do they make sense ?)

> 
> OpD(<IRI>, silent, (S(DG, t+1), {(<i>, S(G_i, t+1)})) = ...

OpD(<URI>, silent, GSS(GS)) = (S(DG), {(<i-1>, S(G_i-1))}

> 
> OpD(DEFAULT, silent, (S(DG, t+1), NG) = (S({}, t+1), NG)

OpD(DEFAULT, silent, GSS(GS)) = ({}, {(<i>, S(G_i))}

> 
> OpD(NAMED, silent, (S(DG, t+1), {(<i>, S(G_i, t+1)})) = S(DG, t, {})
> 

OpD(NAMED, silent, GSS(GS)) = (S(DG), {()})

> OpD(ALL, silent, GS) =
>  OpD(DEFAULT, silent, OpD(NAMED, silent, GS))
> or just
> (S({},t+1), {})
> 
> Writing GSS out as it's definition on the LHS, gives the names for the RHS as well.
> 
> --------------------
> From this:
> 
> Do we want SILENT on
> 
> DROP NAMED / DROP ALL / DROP DEFAULT
> CLEAR NAMED / CLEAR ALL / CLEAR DEFAULT
> 
> I think could move the SILENT to only apply for GRAPH <iri>

What will be the default behavior for DROP NAMED if there's no named graphs and if we remove SILENT ?
I'd rather keeping it for all for consistency, even if in practice, X SILENT DEFAULT will not be useful as DEFAULT graph always exists.

Alex.

> 
> At the moment, the grammar has:
> 
> Clear	:= <CLEAR> ( <SILENT> )? GraphRefAll
> Drop	:= <DROP> ( <SILENT> )? GraphRefAll
> GraphRefAll :=	( GraphRef | <DFT> | <NAMED> | <ALL> )?
> 
> Welcome to wonders of typesetting definitions in HTML.
> 
> 	Andy

--
Dr. Alexandre Passant
Digital Enterprise Research Institute
National University of Ireland, Galway
:me owl:sameAs <http://apassant.net/alex> .

Received on Tuesday, 31 August 2010 11:40:09 UTC