Re: A good book
Date: Sat, 08 Jul 2006 02:48:39 GMT
Message-ID: <b2Frg.7720$pu3.171926_at_ursa-nb00s0.nbnet.nb.ca>
>> Bob Badour <bbadour_at_pei.sympatico.ca> wrote: >> >>> Chris Smith wrote: >>> >>>> I'm suggesting that you've yet to establish the connection between: >>>> >>>> (a) predicate calculus and elegant code >>>> (b) databases and predicate calculus >>> >>> Relational calculus = 1st order predicate calculus >>> >>> Am I missing something? >> >> >> No, you're almost certainly not missing something. Nevertheless, what >> I'm asking for ought to be relatively simple, so I'll try to explain >> it another way. >> >> As is pointed out here several times every five minutes (okay, not >> that often...), database design and programming is rather frequently >> and unfortnuately performed from very little theoretical basis at >> all. At the same time, it's frequently stated that relational >> databases operate on a solid mathematical foundation. That's a useful >> statement if and only if that mathematical foundation provides tools >> that are useful in practice for reasoning about behavior, >> transformations, correctness, etc. of the code written in relational >> languages. If this connection is not made, then all this talk about >> predicate calculus is pointless. I am looking for the sources that >> explain how this connection is made. Are there theorems of relational >> theory that suggest certain program transformations, or certain >> criteria for correctness? You made a comment in another thread that >> suggested that features added to relational databases can be traced >> back to the mathematical model; where's a source that explains how? >> Although it's not a specialty of mine, I have a pretty solid layman's >> knowledge of systems of logic, including predicate calculus, but it's >> entirely non-obvious to me how this would effect my use of or >> implementation of a database system. This is what I'm asking for. Or >> at least, that's the theoretical part of what I'm asking for, which I >> called (b). The practical part is (a), but I imagine it will largely >> follow from the theoretical understanding. >> >>> Life is too short to go digging for it, but one EWD stands out in >>> regard to elegance where EWD provided a proof without iteration for >>> something previously proved using iteration. He used it as an example >>> of greater elegance. >> >> Hopefully, I've explained why this isn't what I want.
>
> I know nobody asked me but can't resist. What we want isn't always what
> we get. First, what we get from the RT is the certainty (with a
> faithful implementation) that results of the relops are logically
> correct, just like how we can depend on certain mathematical results
> when we know they are based on mathematical theory. When it comes to
> products, this is a far cry from anything that went before, eg. the
> network model, where as far as I can recall, for example, I could get
> different answers depending on whether I put a 'secondary' index on an
> IMS db, as well as anything since, where for example, results from an OO
> db depend on what the implementer thinks OO is. There are a few other
> things too, like normalization theory, which if ever an IT technique
> offered 'elegance', an 'ingenious and simple' way of arranging data to
> avoid redundancy as well as misleading conclusions, certainly qualifies.
> Codd got both of these ideas rolling.
>
> The criteria you want such as transformations and correctness are
> already possible (correctness as above and certainly transformations
> too), at least at a statement level, depending on what means by
> 'statement'. When you mention 'program correctness' that depends on
> what a program is defined to be and I'd agree that it is an open area,
> just as it seems to be when I read what people say about non RT db's.
What's particularly astounding about his repeat of the question is predicate calculus is exactly the tool one uses to prove correctness of program transformations. When using the RM, it is up to the 'programmer' to deliver the proof, and it is up to the dbms to deliver the program.
> One big value of RT, I suspect a big part of its original motivation has
> to do with persistence and since then other notions such as transactions
> have been attached to RT, but I think they are not an intrinsic part of it.
The concern for concurrency, while important and somewhat related to correctness, is a separate concern from the concern for correctness. A dbms must deliver a number of separate concerns: concurrency, correctness, efficiency, recovery, security etc. That the RM enables one to consider each of these concerns separately should speak volumes to anyone familiar with Dijkstra's writings.
> There is so much baggage involved with commercial IT that isn't directly
> part of RT that asking for 'one book' is a somewhat naive question. For
> myself, I don't think RT is complete yet (as an aside, it is still
> beyond me why no modern cpu has an instruction to 'join' two sets of
> tuples - I think it was around 1954 that Gene Amdahl was trying to put
> very complex instructions into the IBM processors of the day and
> personally, I think the notion of equality of two relations with
> different types is actually a possibility given finite domains). And it
> all depends on what one's immediate purpose is. Eg., if it's a handout
> book for a one-week course in db, you wouldn't have many happy students
> if you gave them TTM. Same would go for Date's (massive) Intro,
> although many people like me who are missing much of the historical
> theory background find its comprehensive references extremely useful.
> Besides Codd's first two papers which can be found here and there, there
> are many ACM papers by people such as Ron Fagin, Ullman et cetera on the
> theory. At an application level and possibly for implementation
> purposes, the dbdebunk papers and the site itself have been illuminating
> for me as they have given me a glimpse into the motivating thinking of
> some of the big names in the field. (Personally, I'm interested in
> implementations that are very low-level, as close to the bare metal as
> possible, so I like the free chapter 13 of the latest TTM edition which
> is at the thethirdmanifesto.com site.)
>
> p
Received on Sat Jul 08 2006 - 04:48:39 CEST