Re: Understanding some issues on the denotational semantics

Hi Ivan,

first of all, thank you for the comments.

On Thu, 2011-02-17 at 13:45 +0100, Ivan Herman wrote:
> Hi Alex,
> 
> On Feb 16, 2011, at 20:26 , Alexandre Bertails wrote:
> 
> [snip]
> 
> > I suggest you follow [2] instead of what you found in the current draft.
> > This is an updated version (far simpler and much more complete) and I'll
> > be happy to help you going through it.
> > 
> > Alexandre Bertails.
> > 
> > [2] http://www.w3.org/2011/02/16-DM-denotational-rdf-semantics
> 
> I went through the text and found some issues in reading the text. They may come from my own non-understanding, though... See them below. There some undefined things at the 'bottom', so to say, but these can be completed easily, like the definition of url_encode. But, overall, it looks fairly complete to me and  is certainly (in my view) publishing ready and worthwhile...
> 
> Of course, what I did until now is to read through the stuff and, I think, I understand it. Next I should take some specific cases and run a mental program to see if it does what I think it does:-). Actually, the nice thing would be if somebody did _another_ implementation (hm, possibly not in scala:-) to prove that the definition is complete. No, I will not do this, I do not think I would have the time now:-)
> 
> A specific technical question and this probably shows my lack of sql knowledge. The DM document talks about primary keys as possibly a multi-column primary keys (eg, section 2.2). Your description says
> 
> primaryKey : Table → {s:Set(CandidateKey) | size(s) ≤ 1}

No, this is actually perfectly correct. I will of course explain that in
an introduction but here is a quick explanation of what this dependent
type [1] means.

The general form of a dependent type is { a:A | P(a) } where P is a
predicate on a. It's read "the set of a of type A such that P(a)".

If you want to understand the basic meaning, start by removing the
dependent part and you obtain:
primaryKey : Table → Set(CandidateKey)

So primaryKey is a function giving you a set of CandidateKey from a
Table, potentially empty. But we *know* we want to restrict this type to
a set with at most 1 element (there is 0 or only 1 primary key). This is
where the dependent type gives you the information. First you bind the
Set to s, then you can use it with a predicate constraining the size,
expecting than the function "size" is part of the accessors associated
with the commonly known Set ADT.

> 
> ie, a specific primary key for a table cannot be multi-column, right? There seems to be a discrepancy.
> 
> 
> 
> Small comments
> ==============
> 
> There is a superfluous '(' in
> 
> value : ({r:Row} → {a:ColumnName  |  a ∈ r} → CellValue

Fixed.

> -------------
> 
> There is no definition for LexicalValue in 
> 
> CellValue ::= LexicalValue  |  NULL

Known, ericP is supposed to give me the pointer to the definition.

> 
> and that also backfires in the definition of:
> 
> lexicals : {r:Row} → List({a:ColumnName  |  a ∈ r}) → List(LexicalValue)

Fixed. I actually curried this function, that explains some forgotten
parenthesis :-)

> -------------
> 
> I understand the intention, but I am not sure I fully understand the mathematical formalism in, say, 
> 
> references : {t:Table} → {r:Row  |  r ∈ t} → Set(ForeignKey)
> 
> The formalism you use for accessor functions like
> 
> bla : {a:Set1} → {b:Set2}
> 
> seems to indicate that this is a function so that bla(a) yields b. But I am not sure what the value of references(t) is... Shouldn't it be
> 
> references : {t:Table} → {r:Row | r ∈ t} → { f:Set(ForeignKey) | (cn,v) ∈ r | (cn,t1,c1) ∈ r}
> 
> or something like that?
> 
> (The same issue with 'lexicals' and 'scalars'.)

Each time you '{' '}' in a type, be sure it *is* a dependent type.

That's known as type-as-specification. We say that the function is fully
specified. Here, it's really mandatory because I need some information
that binds Table and Row, the later needing to be part of the body of
the table. That exactly what the type means.

Again, first remove all the dependent-types and try to understand what
kind of constraints you need:

references : Table → Row → Set(ForeignKey)

> 
> ---------------
> 
> It is a notational thing, but the usage of '+' is a bit strange to me in ⟦r⟧ row φ. Instead of +, wouldn't it be cleaner to use a set union for
> 
> {(s, rdf:type, ue(tablename(table(r))))} 

I'm ok with that, I updated this part.

> 
> ---------------
> 
> In the definition of ⟦r, fk⟧ ref φ you refer to the function 'dereference', but that is not defined anywhere else. I did not spend time to try to reproduce the definition...

Added. It's a tough one.

> 
> IN the same function you also refer to 
> 
> let p = ⟦table(r), pk⟧col
> 
> but what is 'pk' here?

That's a type: s/pk/fk/

I also applied s/tuple/row/ . The document is updated.

Thanks again Ivan!

Alexandre.

[1] http://en.wikipedia.org/wiki/Dependent_type



> 
> ----
> Ivan Herman, W3C Semantic Web Activity Lead
> Home: http://www.w3.org/People/Ivan/
> mobile: +31-641044153
> PGP Key: http://www.ivan-herman.net/pgpkey.html
> FOAF: http://www.ivan-herman.net/foaf.rdf
> 
> 
> 
> 
>

Received on Thursday, 17 February 2011 14:28:32 UTC