Relational lattice completeness
Mikito Harakiri
> Jan Hidders wrote:
> > I'm asking the question for a specific model, not in general as you
> > did. For example, boolean algebra for boolean value *is* complete.
>
> According to Matt all that I have to do to prove incompleteness is to
> find 2 nonisomorphic relational lattices with the same cardinality...
... and here they are:
#1
----------------------------
`xy` = 10
`x`
`y`
00
{(x=1,y=a)} = 11
{(x=1)}
{(y=a)}
01
#2
----------------------------
`x` = 10
00
{(x=1)}
{(x=1), (x=2)}
{(x=1), (x=2), (x=3)}
{(x=1), (x=2), (x=3), (x=4)}
{(x=1), (x=2), (x=3), (x=4), (x=5)} = 11
01
Jan Hidders
Mikito Harakiri wrote:
> Mikito Harakiri wrote:
> > Jan Hidders wrote:
> > > I'm asking the question for a specific model, not in general as you
> > > did. For example, boolean algebra for boolean value *is* complete.
> >
> > According to Matt all that I have to do to prove incompleteness is to
> > find 2 nonisomorphic relational lattices with the same cardinality...
That is under the assumption you are asking whether you are complete
for all models of that cardinality. But here we only have *one* model,
namely the (infinite) lattice over all relations as defined by the two
operations. So, since there is only one, all the models you are
considering are isomorphic.
Sorry for asking such hard questions.
-- Jan Hidders
Mikito Harakiri
Jan Hidders wrote:
> That is under the assumption you are asking whether you are complete
> for all models of that cardinality. But here we only have *one* model,
> namely the (infinite) lattice over all relations as defined by the two
> operations. So, since there is only one, all the models you are
> considering are isomorphic.
>
> Sorry for asking such hard questions.
AFIR you mentioned long time ago that there is some kind of
incompleteness result for RA. Do you have any reference? (Then it would
be clear for me what kind of completeness you have in mind.)
Jan Hidders
I'm not sure I said that, but there is a strongly related result about
the undecidability of equivalence of two relational algebra
expressions. But I suspect that is not going to help you much. I
already gave an almost formal description of the problem in sci.math so
I'm not sure what more there is to explain. I will elaborate that a
bit:
We are talking about expressions as described by the following syntax
(where R is assumed to be the set of relation variables):
E ::= R | (E /\ E) | (E \/ E)
We define a database as a tuple D = (S, f) where S is called the schema
of D and a finite set of relation variables and f a function that maps
each element in R to a relation. Clearly if an expression e contains
only variables from S then it defines a query over D and its result is
denoted as e(D).
Now we define two expressions e1 and e2 as query equivalent if (1) they
contain the same set of relation variables, denoted as S, and (2) for
every database D with schema S it holds that e1(D) = e2(D). We denote
this fact as e1 =q= e2.
I think it is also clear that a set of algebraic identities of the form
e1 == e2 defines an equivalence relationship over expressions as
defined above by defining two expressions as equivalent iff we can
rewrite one to the other with these identities. By rewriting I mean
simply that if we apply e1 == e2 to e3 then we try to match e1 with a
subexpression in e3 and replace it with e2 while replacing in e2 the
variables with the subexpressions to wich they were mapped in e3 when
matching e1. We denote this equivalence relation as e1 =a= e2.
We now call a set of algebraic identities *complete* if ifor all two
expressions e1 and e2 that contain the same set of relation variables
it holds that e1 =q= e2 iff e1 =a= e2.
If this holds then you can be sure that you have all the rewrite rules
you need to do query optimization. That's why this is an interesting
question. It would also establish that your set of operations is really
interesting as it describes a large class of queries but allows to do
something that is not possble for the full relational algebra.
Does that clear some things up?
-- Jan Hidders
vc
I am still not entirely sure what 'completeness' you have in mind.
Simplifying a bit, the relational calculus/algebra are a FOL dialect.
As such, it is complete in the context of the Godel completeness
theorem and trivially incomplete in the context of the Godel first
incompleteness theorem, if treated as a theory with an empty axiom
set. The 'completeness' terminology is unfortunate but that's life.
Now, using Codd's classification of what 'complete' means in the
context of query languages, the RA/RC are 'complete' by Codd's
definition (as far as I remember) as a standard agains which other
query languages should be measured (despite the well-known facts about
inexpressibility of certain questions).
Speaking of the OP question, is he trying to show that his query
language is as expressive/'complete' as RA/RC, more
expressive/'complete', or his question is about something completely
different ?
What's confusing, to me at least, is that in another thread you said
that the question was about complete theories, that is about
completeness in the context of the first incompleteness theorem.
Mikito Harakiri
> Speaking of the OP question, is he trying to show that his query
> language is as expressive/'complete' as RA/RC, more
> expressive/'complete', or his question is about something completely
> different ?
It's not clear who you assume the Delphi is. Jan asked about the
completeness first. After the round of exchanges I once again think
that speaking about completeness of axiom system is premature until we
establish the axiom system in the first place
http://www.phil.cam.ac.uk/research_fellows/leng/b_theories3_02.pdf
For relational lattice we know the interpretation. Can we speak of the
completeness of a theory by just knowing the set of interpretations?
As for Jan's equality expression derivation rule, does the Spight
criteria (which is an implication in meta language) fit there?
Jan Hidders
vc wrote:
>
> I am still not entirely sure what 'completeness' you have in mind.
I gave a full formal definition of what I meant, so, just to be sure,
did you understand this definition of completeness that I gave? Or is
it that you don't see what it intuitively means?
Roughly, you can summarize it as saying that you have all the algebraic
identities that hold, either directly, or indirectly in the sense that
that they can be derived from the given list by applying them to each
other.
> Simplifying a bit, the relational calculus/algebra are a FOL dialect.
> As such, it is complete in the context of the Godel completeness
> theorem and trivially incomplete in the context of the Godel first
> incompleteness theorem, if treated as a theory with an empty axiom
> set. The 'completeness' terminology is unfortunate but that's life.
Indeed.
> Now, using Codd's classification of what 'complete' means in the
> context of query languages, the RA/RC are 'complete' by Codd's
> definition (as far as I remember) as a standard agains which other
> query languages should be measured (despite the well-known facts about
> inexpressibility of certain questions).
Yes, but that is not the kind of completeness we are talking about
here.
> Speaking of the OP question, is he trying to show that his query
> language is as expressive/'complete' as RA/RC, more
> expressive/'complete', or his question is about something completely
> different ?
Since this was originally my question and the OP indicated that he not
yet fully understands what I meant, I'm going to answer this for my
question: it is about something completely different.
> What's confusing, to me at least, is that in another thread you said
> that the question was about complete theories, that is about
> completeness in the context of the first incompleteness theorem.
It is. Because we talking about a system where we have a semantical
notion of truth for algebraic identities and a syntactical one
(derivation from the set of given algebraic identies by applying them
to each other) and the question is if these two are the same.
-- Jan Hidders
Mikito Harakiri
> It is. Because we talking about a system where we have a semantical
> notion of truth for algebraic identities and a syntactical one
> (derivation from the set of given algebraic identies by applying them
> to each other) and the question is if these two are the same.
What makes your question hard is that the idea of formal derivation of
algebraic identities is not mature enough yet.
Consider the chain of rewritings for push-select-through-project on
page 7. On step 8 the Spight criteria is applied. It's highly informal.
We looked on the set of attributes of the each relation, check that
they meet the condition, then apply the distributivity law. This step
is highly informal. It has to be be broken down to a series of smaller
steps which are simple applications of aximoatic equalities.
Next, consider the step #13 in push-cross-through-project rewritings on
page 8. Informally, it is obvious that
`x` /\ B(z) = `xz`
(cross product of the empty relation `x` with the other relation is
empty)
but what axiom identity were appied on this step exactly?
vc
Mikito Harakiri wrote:
> vc wrote:
> > Speaking of the OP question, is he trying to show that his query
> > language is as expressive/'complete' as RA/RC, more
> > expressive/'complete', or his question is about something completely
> > different ?
>
> It's not clear who you assume the Delphi is. Jan asked about the
> completeness first.
Which completeness did he ask about ?
>After the round of exchanges I once again think
> that speaking about completeness of axiom system is premature until we
> establish the axiom system in the first place
That seems like a reasonable suggestion.
>
> http://www.phil.cam.ac.uk/research_fellows/leng/b_theories3_02.pdf
It would be prudent not to read the reference.
>
> For relational lattice we know the interpretation. Can we speak of the
> completeness of a theory by just knowing the set of interpretations?
Theory completeness in the sense of the fisrt Goedel theorem is a
syntactic notion. There is no need to talk about interpretations.
>
> As for Jan's equality expression derivation rule, does the Spight
> criteria (which is an implication in meta language) fit there?
I would not know until you elaborate.
Vadim Tropashko
> Next, consider the step #13 in push-cross-through-project rewritings on
> page 8. Informally, it is obvious that
>
> `x` /\ B(z) = `xz`
>
> (cross product of the empty relation `x` with the other relation is
> empty)
> but what axiom identity were appied on this step exactly?
This step may indeed require some formal clarification, which might be
helpful in identifying additional axiom identities. There is no
complexity here from the RDBMS implementation perspective however. This
is supposed to be a step in query optimization phase. Let me put query
optimization into the bigger perspective of query evaluation, which
consists of the two phases: static analysis (aka query compilation, aka
query optimization) and dynamic execution. On step #13 the optimizer
notices that there is a special identity that one of the relations in
the expression `x` /\ B(z) meet
`x` /\ 00 = `x`
In this situation the optimizer is allowed to perform full evaluation
of the expression `x` /\ B(z). (The general principle is that we can do
full evaluation of static compilation phase if we guarantee that the
dynamic execution of the query is fast). The query evaluation results
in the empty relation `xz`.
vc
Jan Hidders wrote:
> vc wrote:
> >
> > I am still not entirely sure what 'completeness' you have in mind.
>
> I gave a full formal definition of what I meant, so, just to be sure,
> did you understand this definition of completeness that I gave? Or is
> it that you don't see what it intuitively means?
No, I was not sure what kind of completeness we were talking about
since the word is abused so much. Intuitive meaning would be helpful
for sure.
>
> Roughly, you can summarize it as saying that you have all the algebraic
> identities that hold, either directly, or indirectly in the sense that
> that they can be derived from the given list by applying them to each
> other.
OK.
[...]
> the RA/RC are 'complete' by Codd's
> > definition (as far as I remember) as a standard agains which other
> > query languages should be measured (despite the well-known facts about
> > inexpressibility of certain questions).
>
> Yes, but that is not the kind of completeness we are talking about
> here.
OK.
>
> > Speaking of the OP question, is he trying to show that his query
> > language is as expressive/'complete' as RA/RC, more
> > expressive/'complete', or his question is about something completely
> > different ?
>
> Since this was originally my question
I apologize for the misattribution.
> and the OP indicated that he not
> yet fully understands what I meant, I'm going to answer this for my
> question: it is about something completely different.
>
> > What's confusing, to me at least, is that in another thread you said
> > that the question was about complete theories, that is about
> > completeness in the context of the first incompleteness theorem.
>
> It is. Because we talking about a system where we have a semantical
> notion of truth for algebraic identities and a syntactical one
> (derivation from the set of given algebraic identies by applying them
> to each other) and the question is if these two are the same.
They would be the same for a complete (in the sense of the first
incompletenes theorem) system so finding out whether this is the case
would amount to showing if the system in question is complete or not.
However, I am not sure why that may be practically important.
Arithmetic incompleteness does not prevent anyone from balancing one's
checkbook.
>
> -- Jan Hidders
Mikito Harakiri
> Arithmetic incompleteness does not prevent anyone from balancing one's
> checkbook.
I'll add that before arithmetics axiomatization questions were asked,
there was a wealth of results in different direction. Negative,
rational, algebraic, real and complex were discovered -- these are
several centuries of accumulated results, as opposed to metamathematics
which is only a century old. How about "extraordinary relations"?
vc
Mikito Harakiri wrote:
> vc wrote:
> > Arithmetic incompleteness does not prevent anyone from balancing one's
> > checkbook.
>
> I'll add that before arithmetics axiomatization questions were asked,
> there was a wealth of results in different direction. Negative,
> rational, algebraic, real and complex were discovered -- these are
> several centuries of accumulated results, as opposed to metamathematics
> which is only a century old.
What do you mean by metamathematics ?
>How about "extraordinary relations"?
What about them ?
Mikito Harakiri
>
> What do you mean by metamathematics ?
http://en.wikipedia.org/wiki/Metamathematics
> >How about "extraordinary relations"?
>
> What about them ?
They are introduced in the link supplied.
> > http://citeseer.ist.psu.edu/hehner97relational.html
Tarski relation algebra appears not to have the union operator. Perhaps
this may explain why the emphasis is on the relational division and
"rational" aka "extraordinary" relations. One part which seems
obviously missing is the introduction of negative relations. The
equation with union operator
P \/ X = Q
has solutions only if P <= Q. Unlike equations in integers there has to
be a second equation that would guarantee uniqueness of the solution
P \/ X = Q
P /\ X = 01
...
vc
Mikito Harakiri wrote:
> vc wrote:
> >
> > What do you mean by metamathematics ?
>
> http://en.wikipedia.org/wiki/Metamathematics
How is the link relevant to theory completeness ?
>
> > >How about "extraordinary relations"?
> >
> > What about them ?
>
> They are introduced in the link supplied.
I wonder why you think the article is interesting. What important
insight does it offer ?
Jan Hidders
Mikito Harakiri wrote:
> Jan Hidders wrote:
> > It is. Because we talking about a system where we have a semantical
> > notion of truth for algebraic identities and a syntactical one
> > (derivation from the set of given algebraic identies by applying them
> > to each other) and the question is if these two are the same.
>
> What makes your question hard is that the idea of formal derivation of
> algebraic identities is not mature enough yet.
I gave a nearly formal definition of what I meant with that term. I
don't see how it can get more mature.
> Consider the chain of rewritings for push-select-through-project on
> page 7. On step 8 the Spight criteria is applied.
For the fragment that I asked about (look at the definition expression)
the Spight rule is irrelevant.
-- Jan Hidders
Jan Hidders
Not necessarily because the syntactical notion of truth is not the
usual one. It's related but not the same.
> However, I am not sure why that may be practically important.
> Arithmetic incompleteness does not prevent anyone from balancing one's
> checkbook.
Having a full and simple axiomatization makes it possible to write
query optimizers that do a more thorough search of the "optimization
space", and if you know you are complete then you are sure that you
need not look further for any other rules.
-- Jan Hidders
Jan Hidders
Mikito Harakiri wrote:
>
> Tarski relation algebra appears not to have the union operator.
AFAIK both the cylindrical set algebra and the relation algebra by
Tarski have both the union operator. See e.g.
http://citeseer.ist.psu.edu/vandenbussche01applications.html
-- Jan Hidders
vc
> vc wrote:
> > Jan Hidders wrote:
> > > vc wrote:
> > > >
> > > > What's confusing, to me at least, is that in another thread you said
> > > > that the question was about complete theories, that is about
> > > > completeness in the context of the first incompleteness theorem.
> > >
> > > It is. Because we talking about a system where we have a semantical
> > > notion of truth for algebraic identities and a syntactical one
> > > (derivation from the set of given algebraic identies by applying them
> > > to each other) and the question is if these two are the same.
> >
> > They would be the same for a complete (in the sense of the first
> > incompletenes theorem) system so finding out whether this is the case
> > would amount to showing if the system in question is complete or not.
>
> Not necessarily because the syntactical notion of truth is not the
> usual one. It's related but not the same.
I let it slip the first time because I thought you'd used the
expression metaphorically, but now I am curious as to what exactly you
meant. The 1st incompleteness theorem talks about provability, not
truth. The notion of truth is not used in either the formulation or
proof.
Let's assume that by 'syntactical notion of truth; you've meant in fact
derivation. If so, what did you mean by " because the syntactical
notion of truth is not the usual one. It's related but not the same" ?
>
> > However, I am not sure why that may be practically important.
> > Arithmetic incompleteness does not prevent anyone from balancing one's
> > checkbook.
>
> Having a full and simple axiomatization makes it possible to write
> query optimizers that do a more thorough search of the "optimization
> space", and if you know you are complete then you are sure that you
> need not look further for any other rules.
If you have a bunch of axioms/derivation rules, you can transform an
expression to your heart content regardless of whether the theory is
complete or not. It's highly unlikely that you will all of a sudden
come up with a formula which turns out to be unprovable in your
hypothetical incomplete theory -- such formula is underivable from the
theory axioms (unless the formula somehow magically appears in your
mind). So I am puzzled by your thinking that a theory completeness in
the sense of the 1st incompletness theorem may have any practical
implications for the query language.
>
> -- Jan Hidders
Jan Hidders
vc wrote:
> Jan Hidders wrote:
> > vc wrote:
> > > Jan Hidders wrote:
> > > > vc wrote:
> > > > >
> > > > > What's confusing, to me at least, is that in another thread you said
> > > > > that the question was about complete theories, that is about
> > > > > completeness in the context of the first incompleteness theorem.
> > > >
> > > > It is. Because we talking about a system where we have a semantical
> > > > notion of truth for algebraic identities and a syntactical one
> > > > (derivation from the set of given algebraic identies by applying them
> > > > to each other) and the question is if these two are the same.
> > >
> > > They would be the same for a complete (in the sense of the first
> > > incompletenes theorem) system so finding out whether this is the case
> > > would amount to showing if the system in question is complete or not.
> >
> > Not necessarily because the syntactical notion of truth is not the
> > usual one. It's related but not the same.
>
> I let it slip the first time because I thought you'd used the
> expression metaphorically, but now I am curious as to what exactly you
> meant. The 1st incompleteness theorem talks about provability, not
> truth. The notion of truth is not used in either the formulation or
> proof.
It also doesn't mention completeness, so I thought you meant the notion
of completeness that it is usually assumed to say something about. But
this is all detracting form the main point. I gave an exact and, I
think, very simple definition in:
http://groups.google.be/group/comp.databases.theory/msg/a1c140fbe76681e8?hl=en&
What did you not understand about it?
> Let's assume that by 'syntactical notion of truth; you've meant in fact
> derivation. If so, what did you mean by " because the syntactical
> notion of truth is not the usual one. It's related but not the same" ?
We have different derivation rules.
> > Having a full and simple axiomatization makes it possible to write
> > query optimizers that do a more thorough search of the "optimization
> > space", and if you know you are complete then you are sure that you
> > need not look further for any other rules.
>
> If you have a bunch of axioms/derivation rules, you can transform an
> expression to your heart content regardless of whether the theory is
> complete or not.
But you are not sure that you can find all possible query evaluation
plans, so you migh miss an optimization opportunity.
-- Jan Hidders
vc
Jan Hidders wrote:
[...]
> > > Having a full and simple axiomatization makes it possible to write
> > > query optimizers that do a more thorough search of the "optimization
> > > space", and if you know you are complete then you are sure that you
> > > need not look further for any other rules.
> >
> > If you have a bunch of axioms/derivation rules, you can transform an
> > expression to your heart content regardless of whether the theory is
> > complete or not.
>
> But you are not sure that you can find all possible query evaluation
> plans, so you migh miss an optimization opportunity.
The set of transformation rules ('algebraic identities') defines the
optimization space also called 'algebraic space' which is enormous in a
general case even with reltive simple queries. None of the existing
relational database optimizers traverses the entire algebraic space
because of the combinatorial explosion and therefore none is capable of
producing an otimal query, only a good enough one. Various heuristics
are used in order to prune the algebraic space and manual query
rewriting and tuning is a fact of life.
In light of the above, the axiom completenes issue is really a
non-issue.
>
> -- Jan Hidders
Jan Hidders
Of course.
> In light of the above, the axiom completenes issue is really a
> non-issue.
That conclusion is far too hasty. If you have a better grasp on what
the total optimization-landscape is and looks like you might possibly
be able to come up with better heuristics. Moreover, we are looking
here at a small subset of the queries that can be expressed with
relational algebra, and an algebra that is in some respects more
"algebra friendly" so things might be simpeler here. In some sense that
is the whole raison d'etre of Vadim's algebra, so such a result would
seriously strengthen his case. Until we have actually looked, it is
simply too early to tell. Finally, trying to prove completeness is
simply a good way of checking if there are no obvious algebraic
identities still missing.
-- Jan Hidders
Marshall Spight
> Finally, trying to prove completeness is
> simply a good way of checking if there are no obvious algebraic
> identities still missing.
It seems a very interesting question. But I haven't been able to come
up with an idea of how to approach it. I was thinking I'd try to
understand
some simpler cases first. For example, one can construct every possible
boolean function with only NAND (or NOR), but the only proof of this
I'm aware of is simply one by demonstration. There are only 16 possible
boolean functions, so it's quite to simply build them all with NAND and
there's your proof.
So, how would one go about proving that any boolean expression
with the grammar
E :== v
| E && E
| E || E
could be transformed into any equivalent expression, using only
some fixed set of transformations. (That is the basic idea,
right?) What is the smallest set of transformations necessary?
Any pointers to further reading appreciated; I'm completely
uninformed on this topic.
Marshall
Jan Hidders
>
> So, how would one go about proving that any boolean expression
> with the grammar
>
> | E && E
> | E || E
>
> could be transformed into any equivalent expression, using only
> some fixed set of transformations. (That is the basic idea,
> right?) What is the smallest set of transformations necessary?
Often it is shown that you can use the rewrite rules to rewrite the
expression to some normal form and then it is shown that for this
normal form it holds that expressions are sementically equivalent iff
they are syntactically equivalent. I'll give the example for the
boolean case you presented.
You need to show that if you have two equivalent expressions you can
rewrite one to the other. What is often a good idea for showing
equivalence is to rewrite them to some normal form. For the disjunctive
normal form you need:
(1) (v1 || v2) && v3 == (v1 && v3) || (v2 && v3)
(1') v1 && (v2 || v3) == (v1 && v2) || (v1 && v3)
Note that this is enough to get you into DNF, which means here an
expresssion of the following syntax:
E1 ::= E2 | E1 || E1
E2 ::= V | E2 && E2
We have the usual idempotency, commutativity and associativity rules:
(2) (v1 || v1) == v1
(3) (v1 && v1) == v1
(4) (v1 || v2) == (v2 || v1)
(5) (v1 && v2) == (v2 && v1)
(6) (v1 || v2) || v3 == v1 || (v2 || v3)
(7) (v1 && v2) && v3 == v1 && (v2 && v3)
Which essentially means that we can view the expression as a set of
sets of variables, e.g., (v1 || (v2 && v3)) || ((v2 && v4) && v5) can
be thought of as { {v1}, {v2, v3}, {v2, v4, v5} }. I will call this a
set representation of a DNF expression.
Note that we can now also drop rule (1') because it follows from (1),
(4) and (5).
If we add the following rule
(8) (v1 && v2) || v2 == v1 && v2
then we can always rewrite to a DNF such that it holds for its set
version {C1, ..., Cn} that there are no Ci and Cj such that Ci is a
subset of Cj. I will call set-representations with that property
subset-free.
We now set out to show that if two expressions e1 and e2 are rewritten
to DNF expressions with subset-free set-representions s1 and s2,
respectively, and e1 and e2 are semantically equivalent then s1 = s2.
We proof this by contradiction:
We begin with assuming that two expressions e1 and e2 are rewritten to
DNF expressions with subset-free set-representations s1 and s2,
respectively, and e1 and e2 are semantically equivalent. Let us now
also assume that s1 <> s2. Let s1 = {B1, ..., Bn} and s2 = {C1, ...,
Cm}. Now there is some Bi that is not a superset of any of C1, ..., Cm
or there is a Cj that is not a superset of any of B1, ..., Bn. Note
that this is true because s1 and s2 are different, finite and
subset-free. (Proof of that is left to the reader as an exercise.) Let
us assume that such a Bi exists. (The case for Cj is symmetric.) Let
M(Bi) be the model that assigns all variables in Bi to TRUE and all
other variables to FALSE. Then clearly M(B_i) is a model for which e1
evaluates to TRUE, but e2 evaluates to FALSE, since none of C1, ..., Cm
is a subset of Bi. It follows that e1 and e2 are semantically
different, which contradicts the assumption that e1 and e2 are
semantically equivalent.
So we know that if two expressions e1 and e2 are semantically
equivalent then there is a a subset-free set-representation s' such
that both e1 and e2 can be rewritten to e1' and e2' with s' as their
set-version. Clearly since e1' and e2' have the same set-representation
they can be rewritten to each other, and so we can rewrite e1 to e1' to
e2' to e2.
QED
So the conclusion is that the set of rules (1), ..., (8) are indeed
complete in the sense that we talked about. Note that the dual of (1),
i.e.,
(v1 && v2) || v3 == (v1 || v3) && (v2 || v3)
is missing but that indeed we can prove it from the other rules by
algebraic rewriting. That's also left to the reader as an exercise.
:-)
Hope this helps,
-- Jan Hidders
Jan Hidders
Oops. That should of course read:
(8) (v1 && v2) || v2 == v2
-- Jan Hidders
Marshall Spight
>
> Hope this helps,
Wonderful! Thanks very much for the effort.
Marshall
Marshall Spight
> Mikito Harakiri wrote:
> >
> > incompleteness result for RA. Do you have any reference? (Then it would
> > be clear for me what kind of completeness you have in mind.)
>
> I'm not sure I said that, but there is a strongly related result about
> the undecidability of equivalence of two relational algebra
> expressions. But I suspect that is not going to help you much.
I would like to second Mikito's request for a citation for this.
For one thing, I now have this idea in my head that the
equivalence of two RA expressions is undecidable, but
no actual way to back that idea up. For another, it's a
significant part of the motivation to work towards a proof that
it *is* decidable for the Tropashko algebra.
Marshall
Jan Hidders
Marshall Spight wrote:
> Jan Hidders wrote:
> > Mikito Harakiri wrote:
> > >
> > > AFIR you mentioned long time ago that there is some kind of
> > > incompleteness result for RA. Do you have any reference? (Then it would
> > > be clear for me what kind of completeness you have in mind.)
> >
> > I'm not sure I said that, but there is a strongly related result about
> > the undecidability of equivalence of two relational algebra
> > expressions. But I suspect that is not going to help you much.
>
> I would like to second Mikito's request for a citation for this.
> For one thing, I now have this idea in my head that the
> equivalence of two RA expressions is undecidable, but
> no actual way to back that idea up.
It's a direct consequence of the fact that the satisfiability of a
first-order logic formula over finite structures is undecidable. Just
ask if it is not clear to you why this is a consequence. The usual
references for the FOL result may not be what you wanted but I'll give
them anyway:
W. Craig. Incompletability, with respect to validity in every finite
nonempty domain, of first order functional calculus. In Proceedings
of the International Congress of
Mathematicians, page 721, Cambridge, Mass., 1950.
B.A. Trakhtenbrot. The impossibility of an algorithm for the decision
problem for
finite models. Dokl. Akad. Nauk SSSR, 70:596--572, 1950. English
translation in:
AMS Transl. Ser. 2, vol.23 (1063), 1--6.
-- Jan Hidders