Re: Proving an Upgrade is Possible

Kenneth Downs wrote:
> Jan Hidders wrote:

>>
>>Ok, so I suspect are you asking the following:
>>
>>"Given the old database schema and a few updates to its constraints (but
>>not its structure) is it possible to algorithmically decide (or
>>mathematically prove) whether all instances of the old schema are also
>>instances of the new schema?"
>>
>>I leave it to you whether it is "algorithmically decide" or
>>"mathematically prove".

What do you mean by "constraints are included"? Those were already included in my formulation. Since you only care about whether instances are valid or not, automation can in this case be regarded as a special case of constraints. Default values are completely irrelevant for your question because they do not change the set of allowed valid instances.

Or do you want to also consider updates that change the structure of the schema, because in that case my formulation would be completely off track.

> Another way to state the question is: "What structure of meta-data allows
> us to specify completely a database of arbitrary complexity and also allows
> us to demonstrate by analysis that any given change in the meta data is
> valid or not valid".

And when exactly is a change to the meta-data "valid"? What does the specification of the meta-data look like? What do you mean by "arbitrary complexity"? What do you mean by "demonstrate by analysis"?

> Methinks the structure of the meta-data would reduce the truth to a data
> validity issue (an invalid transform would fail a validitity check in the
> meta data), which is closer to an algorithm than to a mathematical proof.
> Yet, I have the strong intuitive sense that a before-hand mathematical
> proof could lead to the table structure.

Whoah, wait right there! You want to derive the table structure? That's a completely different question! Since you are still a bit sloppy with your terminology and still have not really given a mathematically exact definition of the theorem (which is mathematical in nature) that you want to discuss, I suggest that we first keep things simple and start with the case where the structure of the tables is fixed. Note that I'm not even talking about the answer of the problem here, just about formulating the problem. That's always the first problem you need to solve. :-)

• Jan Hidders