Re: Understanding some issues on the denotational semantics

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}

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
-------------

There is no definition for LexicalValue in 

CellValue ::= LexicalValue  |  NULL

and that also backfires in the definition of:

lexicals : {r:Row} → List({a:ColumnName  |  a ∈ r}) → List(LexicalValue)
-------------

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'.)

---------------

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))))} 

---------------

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...

IN the same function you also refer to 

let p = ⟦table(r), pk⟧col

but what is 'pk' here?

----
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