notes on DDRTNFATJ - Ch 5

For a while I've been trying to read Database Design & Relational Theory: Normal Forms & All That Jazz by CJ Date (no relation). I have a bad habit of picking up new books and reading only the first 3 or 4 chapters before moving on to another book, which is unfortunate for this book because it really starts in earnest at Chapter 5.

i'ma keep some notes here–for my own sake. Before I get to that, I'd like to file a complaint about the level of formality used in this book, but hold on it's not what you think.

Date drops a couple unambiguous warnings in Chapter 5 about how the level of formality is about to soar:

“...it’ll certainly be more formal. For that reason, I don’t want you to look at this chapter at all until you’ve absorbed everything in the previous one.

If that wasn't clear enough*:

“In this section I simply give definitions, with little by way of further elaboration [...] definitions that are rather more precise than the ones typically found in the literature (as well as being more precise, in some cases, than ones given earlier in this book).”

That's a solid burn on the database literature out there. But here's the thing: I wish it was more formal.

To me, formal is Practical Foundations for Programming Languages; it is The Mechanization of Standard ML; it is Homotopy Type Theory. I want to see a database design and relational theory text reach for this level of formality. Let me say that again for dramatic effect:

I want to see a database design and relational theory text as rigorous and formal as contemporary type-theoretic publications.

The world needs this. Now onto notes and outlines...

Warning: I'm rephrasing these into my own words and am probably turning some into wrong definitions in doing so. Any errors are my own.

• heading – a set. The elements represent attribute names.
• tuple with heading H – set of pairs $$<A, v>$$ pairing each attribute $$A \in H$$ with some corresponding value $$v$$
• tuple projection – a subset of a tuple with heading H
• relation – an ordered pair comprising a heading $$H$$ and a set of tuples $$h$$ all having heading $$H$$. The components of $$H$$ and $$h$$ all lift into the relation.
• relational projection – like tuple projection but lifted into a relation
• joinable – relations where attributes having the same name have the same type†
• join – a relation whose heading is the union of all given headings and tuples are the union of all given tuples
• relation variable (relvar) – a relation lifted into a variable

More to come as I find time.

* Some online reviewers out there really lambaste the excessive formality, despite Date's own warning that formality is imminent. To each his own, I guess. I still wish it was more formal.

† Whoa, see what I mean about the lack of formality? the same type, what does that mean? Before we can say anything about type equality we need to define syntax, judgments, induction, and, oh, types–basically Parts I-IV of PFPL.