Completeness of Relational Algebra via Cylindric Algebra

Titel: Volledigheid van Relationale Algebra via Cilindrische Algebra

1. Probleemstelling

Relationele algebra (RA) vormt de procedurele basis voor het opvragen van relationele databases. Een centrale vraag in de theorie van databases is de volledigheid (completeness) van deze algebra ten opzichte van de eerste-orde logica (FOL).

• Het probleem: Niet elke eerste-orde formule heeft een semantisch equivalente relationele expressie. Bijvoorbeeld, formules met vrije variabelen die niet gebonden zijn aan een actieve domein (zoals $\neg r(x)$) of formules die afhankelijk zijn van het domein, kunnen niet worden vertaald naar RA.
• De beperking: Om een equivalentie te garanderen, moet men zich beperken tot een specifieke subset van formules, de zogenaamde toegelaten formules (allowed formulas).
• Bestaande oplossingen: Een eerdere bewijsvoering en conversie-algoritme werden gepresenteerd in [VGT91]. Deze benadering behandelde negatie echter vaak als een secundaire constructie en vereiste soms het elimineren van gelijkheid voordat verwerking kon plaatsvinden.
• Het doel van dit artikel: Het presenteren van een alternatief bewijs van de volledigheidstheorema en een nieuw conversie-algoritme. De hoofdmotivatie is het creëren van een bewijstechniek die geschikt is voor generalisatie naar relationele modellen die werken met onvolledige of vage informatie, waar standaard relationele algebra tekortschiet.

2. Methodologie

De auteur kiest voor een algebraïsche benadering in plaats van een puur syntactische of model-theoretische aanpak. De kern van de methodologie bestaat uit drie pijlers:

1. Embedding in Cilindrische Algebra:
   De relatie tussen relationele algebra en eerste-orde logica wordt geanalyseerd via cilindrische algebra (Cylindric Algebra, CA), een algebraïsche structuur geïntroduceerd door Tarski voor de algebraïsche formalisering van FOL. De auteur maakt gebruik van de bekende embedding van relationele algebra in CA (zoals beschreven door Imieliński en Lipski). Hierdoor kunnen semantische equivalenties worden bewezen binnen de strakke axioma's van CA.

2. Definitie van Toegelaten Formules:
   De paper definieert "toegelaten formules" op basis van de structuur van de formule en de vrijheid van variabelen. Hiervoor worden nieuwe concepten geïntroduceerd:

   • Gelijkheid (eq) en Ongelijkheid (coeq): Equivalences op variabelen die worden afgeleid uit de structuur van de formule.
   • Generatoren en Co-generatoren: Mappings gen(φ) en cogen(φ) die de "actieve" variabelen en de beperkingen van de formule vastleggen. Een formule is "toegestaan" als de verzameling vrije variabelen overeenkomt met de generator en elke existentiële kwantificatie binnen de generator valt.

3. Normalisatie-algoritme:
   Het artikel presenteert een tweestaps-algoritme om een toegelaten formule om te zetten in een relationele expressie:

   • Stap 1: Normalisatie. De invoerformule wordt getransformeerd naar een genormaliseerde formule. Deze stap behoudt de structuur van de invoer en behandelt negatie als een volwaardig logisch connectief. Gelijkheid wordt expliciet gehanteerd zonder voorafgaande eliminatie.
   • Stap 2: Conversie. De genormaliseerde formule wordt rechtstreeks vertaald naar een relationele expressie (met operaties zoals projectie, selectie, join, en verschil) via een recursieve definitie (expr(φ)).

3. Belangrijkste Bijdragen

• Alternatief Bewijs van Volledigheid:
  Het artikel levert een nieuw bewijs dat elke toegelaten formule semantisch equivalent is aan een relationele expressie, en vice versa. Dit bewijs is "algebraïsch" omdat het werkt binnen de structuur van een cilindrische algebra, wat het mogelijk maakt om de bewijstechniek te generaliseren naar complexere databasemodellen (bijv. met onvolledige informatie).

• Verbeterde Behandeling van Negatie en Gelijkheid:
  In tegenstelling tot eerdere werken (zoals [VGT91]), behandelt deze methode negatie als een primaire operator en behoudt gelijkheid (≈) in de formules tijdens de verwerking. Dit maakt de definitie van toegelaten formules duidelijker en het algoritme robuuster.

• Het Normalisatie-algoritme:
  De auteur introduceert een specifiek algoritme (norm(φ, ψ)) dat een formule normaliseert ten opzichte van een "generator". Dit algoritme zorgt ervoor dat de geconverteerde relationele expressie correct werkt binnen het actieve domein van de database.

• Generaliseerbaarheid:
  De belangrijkste theoretische bijdrage is dat de bewijstechniek gebaseerd is op eigenschappen van cilindrische algebra's. Omdat deze algebra's kunnen worden uitgebreid om onzekerheid of vage waarden te modelleren, biedt deze aanpak een pad naar volledigheidstheorema's voor geavanceerde databasemodellen die buiten het bereik van traditionele relationele algebra vallen.

4. Resultaten

• Theorema 6.8: Elke toegelaten formule is semantisch equivalent aan zijn genormaliseerde vorm.
• Theorema 6.9: Alle toegelaten formules zijn domein-onafhankelijk (domain independent). Dit betekent dat hun betekenis niet afhangt van het specifieke domein van de database, maar alleen van de actieve waarden.
• Correctheid van het Algoritme: Het artikel bewijst dat het voorgestelde algoritme (expr toegepast op de genormaliseerde formule) een relationele expressie produceert die semantisch equivalent is aan de oorspronkelijke toegelaten formule.
• Voorbeeld: Het artikel demonstreert het algoritme aan de hand van de relationele deling (relational division), een complexe operatie die vaak moeilijk is om direct uit logica af te leiden. Het algoritme converteert de logica van deling succesvol naar de standaard relationele deling-expressie.

5. Betekenis en Impact

De betekenis van dit werk ligt voornamelijk in de methodologische verschuiving:

1. Van Syntaxis naar Algebra: Door de brug te slaan tussen relationele algebra en cilindrische algebra, biedt de auteur een krachtigere toolset voor het analyseren van query-vertalingen.
2. Toekomstgericht: De motivatie voor dit werk is niet alleen het verbeteren van bestaande theorieën, maar het voorbereiden van de grondslag voor relationele modellen met onvolledige of vage informatie. Traditionele relationele algebra faalt vaak bij het modelleren van onzekerheid; door de bewijstechniek te baseren op CA, kan deze techniek worden uitgebreid naar "generalized relational models" (zoals vermeld in de introductie, verwijzend naar werk over incomplete informatie).
3. Praktische Toepassing: Hoewel het artikel theoretisch van aard is, biedt het een gestructureerd algoritme voor het compileren van declaratieve queries (FOL) naar uitvoerbare query's (RA), wat essentieel is voor database-ontwerpers en query-optimizers.

Kortom, het artikel levert een robuust, algebraïsch onderbouwd bewijs voor de volledigheid van relationele algebra voor een specifieke, maar cruciale subset van logica, en opent de deur voor de toepassing van deze principes op complexere, minder strikte databasemodellen.