Re: Understanding some issues on the denotational semantics

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

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

[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