Re: Understanding some issues on the denotational semantics

On Thu, 2011-02-17 at 15:47 +0100, Ivan Herman wrote:
> Alex,
> 
> 
> On Feb 17, 2011, at 15:28 , Alexandre Bertails wrote:
> [snip]
> >> 
> >> 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.
> > 
> 
> You misunderstood me. I understand the formalism, I guess. 

Sorry, I did not understand your comment this way as I think that the
type is already correct.

> But does that specification means that for every table t, primaryKey(t) will give me a set s=primaryKey(t) where size(s)<=1? Ie, that, for every table, the primaryKey is either empty or restricted to one single column? That is the discrepancy with section 2.2 that explicitly speaks about multi-column primary keys...

>From you comment:
s/the primaryKey is either empty or restricted to one single column/the primaryKey is either empty or restricted to one single CandidateKey/

So primaryKey's type tells you that primaryKey gives you either 0 or 1
CandidateKey. The definition for CandidateKey is
[[
CandidateKey ::= List(ColumnName)
]]

So you do have multi-columns for a Primary Key (if there is one).

Am I getting it right? I may be not introducing this one the right way.

> 
> [snip]
> 
> > 
> >> -------------
> >> 
> >> 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)
> 
> 
> Yes. But isn't it correct that for the result you _do_ need constraints, something that I tried to capture in my row? The way you say does not tell me what kinds of constraints you need to impose on the 'results'...

You are absolutely right. I modified references accordingly.

[[
references:{t:Table} → {r:Row  |  r ∈ t} → Set({fk:ForeignKey  |  fk ∈ references(table(r), r)})
]]

And I have to do the same for the other functions.

Alexandre.

> 
> [snip]
> > 
> > I also applied s/tuple/row/ . The document is updated.
> > 
> 
> I will look at it... later:-)
> 
> Cheers
> 
> Ivan
> 
> 
> > 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
> >> 
> >> 
> >> 
> >> 
> >> 
> > 
> > 
> 
> 
> ----
> 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 15:18:15 UTC