Dandl: Initial creation from TTM post

2017-09-24T14:29:59Z

Initial creation from TTM post

New page

This is a verbatim copy of text posted by Philip to the TTM mailing list, lightly edited for continuity and formatting.

Hopefully Philip will improve it, but (of course) he may just delete it. Over to Philip.

== PREAMBLE ==

Below is an edited message that quoted others with some RM semantics, my 'tutorial' & my 'quiz'.

I have sent many messages about RM query meanings. The recent intro/tutorial/quiz that this is from is not intended
to be an ideal presentation.
If one bumped up against not understanding something in reading an example or not knowing something in answering the quiz,
presumably one would ask a question or point out a contradiction.

== INTRODUCTION ==

Each relvar name has a dba-given predicate and each operator has a Codd-given transformation on predicates.
Each query subexpression (relation or wff) has a predicate built from its mentioned relvar names and operators.
This is in fact how we actually know what queries mean.

Every relvar has a predicate (parameterized statement about the
world), with attributes the free variables. Every relation operator
has a corresponding predicate transform, eg JOIN/AND. So every
relation expression has a corresponding predicate, and vice versa. The
design of the relation operators is such that IF the relvars' values are their predicates'
extensions THEN an expression's value is its predicate's extension.
The value of a relvar after an assignment is the value of the query
evaluated before the assignment. Which means the extension of the
relvar predicate in the new state is the extension of the expression predicate in the old state.
When I say that is all you need to know, THAT IS ALL YOU NEED TO KNOW.

The predicate of a relation expression that is a name of a relation
variable or constant is its predicate. The predicate of a relation
expression that is a JOIN is the AND of the predicates its operands;
of a UNION is the OR; of a MINUS is the AND NOT; of a RESTRICT X=Y or
of an ADD X AS Y is the AND X=Y; and of a PROJECTALLBUT X is the
EXISTS X.

RE: delete-through-restrict - logical basis

query wff predicate:
n n(x,y) 'x likes y'
m m(z) 'i like z'
n where y=3 n(x,y) and y=3 'x likes y and y=3'
(n where y=3){allbut y} exists y [n(x,y) and y=3] 'x likes 3'
(n where y=3){allbut y} n(x, 3) 'x likes 3'
m rename z to x m(x) 'i like x'
(n where y=3) join (m rename z to x) n(x, y) and y=3 and m(x)
'x likes y and y=3 and i like x' ie 'x likes 3 and y=3 and i like x'
(n where y=3){allbut y} join (m rename z to x) n(x, 3) and m(x)
'x likes 3 and i like x'

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

The value of every subexpression is the extension of its predicate.
I append (a) an excerpt tracing and justifying an illustrating example and (b) a self-quiz excerpt.

== TUTORIAL ==

Here is how a relational database works.

type T={a, b}
relvar r RELATION{X T} "i like X"
Relvar predicate for relvar r is "i like X".
r:=RELATION{TUPLE{X a}} // i like a and i don't like b.
Relvar r value, relvar r (and database) proposition is "i like a and i don't like b".
r:=RELATION{TUPLE{X a},TUPLE{X b}} // now i like a and i like b.
Relvar r value, relvar r (and database) proposition is "i like a and i like b".

hmm... if i assume that a relvar holds those tuples that make its predicate true
(in which case, for each present tuple, that tuple put into the
predicate is true, and in which case, for each absent tuple, that
tuple put into the predicate is false) then a certain conjunction mapped from its tuples is true.

Namely:
(AND for t in r of the predicate of r applied to t)
AND (AND for t not in r of NOT(the predicate of r applied to t))
or if you prefer:
(FORALL t in r : the predicate of r applied to t)
AND (FORALL t not in r : NOT (the predicate of r applied to t))

So if i assume that a relvar value is the extension of its predicate then it seems to state what i expect!

Namely that if a tuple is in a relvar then it asserts the relvar
predicate applied to it and that if a tuple is not in a relvar then it
asserts the negation of the relvar predicate applied to it.
(Informally, present tuples are true and absent tuples are false.)

print r // RELATION{TUPLE{X a},TUPLE{X b}}

hmm... this is the extension of the predicate of r.

hmm... a query expression that is a relvar name seems to be the
extension of a predicate that is the relvar's predicate.

print RELATION{TUPLE{X b}} // RELATION{TUPLE{X b}}

hmm... this is the extension of X=b.

hmm... a relation expression RELATION{TUPLE{A1 v1, ...}, ...} seems
to be the extension of a predicate (A1=v1 AND ...) OR ....

Or if it's clearer: (A1=v11 AND A2=v12 AND...) OR (A1=v21 AND A2=v22
AND...) OR .... Ie the disjunction of the conjunction of the equalites
of attributes names and values.

print r PROJECT ALL BUT X // RELATION{TUPLE{}}

hmm... relation expression e PROJECT ALL BUT A seems to be the
extension of (EXISTS A: the predicate of e).

print r UNION RELATION{TUPLE{X b}} // RELATION{TUPLE{X a},TUPLE{X b}}

hmm... relation expression e UNION f seems to be the extension of
(the predicate of e OR the predicate of f).

print (r UNION RELATION{TUPLE{X b}}) MINUS RELATION{TUPLE{X a}} // RELATION{TUPLE{X b}}

hmm... relation expression (e UNION f) MINUS g
seems to be the extension of ((the predicate of e OR the predicate of
f) AND NOT the predicate of g)

hmm... relation expression e MINUS f
seems to be the extension of (the predicate of e AND NOT the
predicate of f).

hmm... every relation seems to be the extension of a certain
transformation of its arguments' predicates.

hmm... seems that a query expression that is a relvar name has as
value the extension of the relvar predicate and that a query
expression that is a literal has as value the extension of the
disjunction-conjunction-equality from its tuples and that a query
expression that is an operator call has as value the extension of a
certain transformation of its arguments' predicates, and that
(consequently) an arbitrary query expression has as value the
extension of a thus-built predicate.

So if i assume that a query expression predicate is thus-built then
the query is the extension of its predicate!
And so the query tuples are the ones that make a certain predicate true!

Namely the thus-built query expression predicate.
And so a certain conjunction mapped from its tuples is true!

Namely the same proposition as expressed twice above, but for the
query instead of the relvar:
(AND for t in value of query of the predicate of query applied to t)
AND (AND for t not in value of query of NOT(the predicate of query applied to t))
or if you prefer:
(FORALL t in value of query : the predicate of query applied to t)
AND (FORALL t not in value of query : NOT (the predicate of query applied to t))

So if i assume that a query value is the extension of its predicate
then it seems to state what i expect

Namely that if a tuple is in a query then it asserts the query
predicate applied to it and that if a tuple is not in a query then it
asserts the negation of the query predicate applied to it.
(Informally, present tuples are true and absent tuples are false.)
(Note that if missing tuples are not false, then you can't use
MINUS/NOTMATCHING.)

b. QUIZ

* What are the names of your relation variables and constants?
* What is the characteristic predicate (parameterized statement about the world) for each?
* What is the formal wff for each? Why?
* What are the attributes for each? Why?
* What is your (example) query relation expression?
* What is the characteristic predicate of its result? Why?
* What are the (example) values of your relation variables?
* What statement does each make about the world? Why?
* What statement does the database make about the world? Why?
* What is the value of your query relation expression? Why?
* What statement does this value make about the world in the context of this query relation expression? Why?
* What statement does a query result make about the world regardless of its query relation expression? Why?

The most important things to understand are that:

# each relation expression corresponds to a certain wff and
# equivalent relation expressions correspond to equivalent wffs

The relational algebra is just another syntax for FOPL.

PhilipTutorial - Revision history

Dandl: Initial creation from TTM post