Oracle FAQ | Your Portal to the Oracle Knowledge Grid |
Home -> Community -> Usenet -> comp.databases.theory -> Re: completeness of the relational lattice
On 26 jun, 19:55, Vadim Tropashko <vadimtro_inva..._at_yahoo.com> wrote:
> On Jun 26, 12:53 am, Jan Hidders <hidd..._at_gmail.com> wrote:
>
> > On Jun 26, 12:29 am, Vadim Tropashko <vadimtro_inva..._at_yahoo.com>
> > > So you have axiom schemas, instead of a single axiom system? I don't
> > > challenge this approach, but think that a single axiom system is
> > > workable as well (see below).
>
> > It's a schema anyway because you still have relation variables.
> > Although I agree that I need two types of variables, or three if you
> > count the singleton attributes, and you have one (or two if you have
> > special ones for singleton sets, as you suggest later). On the other
> > hand, I only have equations, and you need propositional formulas over
> > equation.
>
> I'm not sure I understand. I see "if" all over the place in your axiom
> system -- you must have propositions there as well. I had a quantifier
> in one place where I wanted to introduce atomic attribute, but this
> can be avoided (see below).
Ok. There may be some fundamental misunderstanding here, so before I'm going to reply to you remarks I'm going to try to clear that. Maybe I'm telling you stuff that you already thoroughly understood, but I just want to make sure there is no misunderstanding. The concepts I'll discuss are not defined the same by everybody, but I'll give you my version which AFAIK is how most CS researchers define it.
What is an inference system? In the wider meaning of the word it is an
algorithm that takes as input a finite set of formulas or formula
schemas describing axioms and tries to enumerate all formulas that
logically follow from them. The specification of such a system
consists of:
1. The language that describes all formulas
2. If the axioms are given as axiom schemas then an algorithm must me
given that given a schema enumerates the set of formulas it defines.
Usually the schemas are simply formulas with open variables like "P or
not(P)" where P may be replaced with arbitrary formulas, thus giving
all formulas.
3. The inference rules in general consist of a set of premisses and a
conclusion. The premises are usually formulas, formulas scemas and
some conditions over them that can be checked if the formulas are
known, and the conclusoin is also a formula or a formula schema. The
meaning is that if the system can derive formulas that match the
premises then it also derives the conclusion. The standard example is
the Modus Ponens which states that "if we can derive 'P' and 'P->Q'
then we can derive 'Q'". Another is "if we can derive 'P' and x is a
free variable in 'P' then we derive 'forall x : P'".
The set of inferred propositions is then simply defined with induction such that in step 0 we derive all formulas defined by the axiom schemas, and in step i + 1 we derive all formulas were already derive in step i plus the formulas that the inference rules allow us to derive from those in one step. The set of all derived formulas is then the union of all formulas that can be derived in a finite number of steps.
Ok. So what is now an algebraic axiomatization? In that case (1) all formulas are equations between expresssions and (2) there is only one inference rule, namely the rule that says "if we can derive 'e1 = e2' and there is an axiom 'e3 = e4" and e3 occurs somewhere in e2 then we derive 'e1 = e5' where e5 is e2 but with that occurrence of e3 replaced with e4".
So why is my axiomatizatoin algebraic and your's not? Look at for exampe at this rule:
(32b) W + [x] = <x> with x a single attribute
This is actually a schema which generates
"W + [a] = <a>", "W + [b] = <b>", ...
Another example:
(9) r + (s * t) = (r + s) * (r + t) if A(s) * A(t) <= A(r)
This schema generates:
"R(a) + (([a,b] + S(b)) * (W + [a])) = (R(a) + ([a,b] + S(b))) *
(R(a) + (W + [a]))", ...
As you can see, there is a condition involved, but this disappears in the generated formula which is simply an equation. Now consider one of your rules:
(R/\00) \/ (S/\00) <= Q/\00
and (R/\00) \/ (Q/\00) <= S/\00
implies (R /\ S) \/ (R /\ Q) = R /\ (S \/ Q)
If you replace the variables you do not get an equation but a formula of the form "A and B implies C" with A, B and C equations. There is a simple way of solving this, namely promoting this axiom to the status of inference rule. As you probably know something similiar happened for regular expressions and it was in fact proven that without such an extra inference rule you cannot axiomatize regular expressions. But by doing this you are no longer giving an algebraic axiomatization in the strict meaning of the term. Notably this makes the structures of proofs more complicated. In the strict approach these are lists of expressions connected by the axioms that were used for each rewrite. If you add new inference rules like this your proof actually becomes a tree because there can be multiple equations that had to be proven before you could apply a rule.
Note that in such a system the premises still have to be conjunctions of equalities and conditions over the involved formulas. It is not clear what it means if you have a rule "if we derive not(W = R) then ..." because the inference mechanism only derives equalities and not inequalities. Of course you could incorporate something like that by extending the set of formulas from equations to propositional formulas over equations and then such a rule would have meaning. But then you als have to add the inference rules that are required for propositional calculus, which makes that the inference mechanism becomes more complex and cannot by any means be called purely algebraic anymore.
Did this make sense sofar? Is it clear to you why I would like to keep the axiomatization purely algebraic even if that means having axiom schemas that seem redundant at first sight?