Formální sémantika SQL dotazování

Elina HazaranZuzana Vytisková

6.11. 2012

podle M. Negri, G. Pelagatti, L. Sbattela, 1991

● Základní pojmy

● Formální logický model

● Pravidla pro překlad SQL dotazů do tohoto modelu

● Dokazování ekvivalence SQL dotazů

Formální model:

● ROZŠÍŘENÁ TŘÍHODNOTOVÁ PREDIKÁTOVÁ LOGIKA(Extended three-value predicate calculus = E3VPC)○ true, false, unknown

● založena na "vícedruhové" nebo "vícesortové" logice (Many-sorted logic)○ termy různého druhu

● umožňujě pokrýt všechny dotazy

SQL -> E3VPC

Pravidla umožňují převést libovolný dotaz v SQL do E3VPC formy

(Zpracována podle ANSI normy, tedy 1986)

Jsou relativně jednoduchá (je jich jen 33)

Ekvivalence dotazů

● pravidla pro převedení z E3VPC do tvaru, se kterým je možno zacházet postupy základní dvouhodnotové logiky

● situace, kdy nefunguje dobře

E3VPC - rozšíření

Symboly, které se nevyskytují v dvouhodnotové logice, ale jsou nutné pro definici SQL sémantiky:-kompaktní formy-agregační funkce-tříhodnotová logika-interpretační operátor-operátor na porovnání NULL hodnot - externí referenční operátor ↑

Struktura E3VPC výrazu

{t(v1,. . .,vn) :||P(v1,. . .,vn||α }

cílový seznam

n-tice proměnných predikátová

formule

interpretační operátor

nabývá hodnot: T(true), F(false)

Cílový seznam

- Má tvar

v1 in R1, . . ., vn in Rn

-Lze chápat jako definiční obor, nad kterým bude výhodnocen predikát-SELECT c.id FROM CLIENTS c odpovídá

c in CLIENTS

Predikátová formule

Je definována rekurzivně pomocí termů a porovnávacích operátorů:1) Term

- konstanta- vl.Al a vl↑.Al - f(A)S

2) Porovnávací operátory- = , ≠ , > , < , . . . -

Predikátová formule - pravidla

1) Atomické predikáty- t1 θ t2- T, F, U- || P ||α

2) Atomický predikát je predikátovou formulí3) ¬P, P ∨ Q, P ∧ Q 4) kvantifikator (kompaktní forma) ∀/ ∃{t(v1,...,vn):||P(v1,...,vn)||

α}Q(v1,...,vn). . . a nic jiného

Interpretace E3VPC výrazu - interpretační operátor

1) Pravdivě interpretovaný (notace || ||T)P(x) = T ⇒ Q(x) = TP(x) = F ⇒ Q(x) = FP(x) = U ⇒ Q(x) = T

2) Nepravdivě interpretovaný (notace || ||F)P(x) = T ⇒ Q(x) = TP(x) = F ⇒ Q(x) = FP(x) = U ⇒ Q(x) = F

Interpretace E3VPC výrazů - termy

Externí referenční operátorindikuje, že proměnnou nepočítáme v

daném oboru (in R), ale patří do nejbližšího vnějšího

oboru (in S)

{v in R: P(v, v ↑)}

{v in S:∀{v in R:||v.A1=v↑.B1||α}. . .}

Interpretace E3VPC výrazů - termy

Agregační funkce-dostává n-tice na vstup, výstupem je jednahodnota-pokud je daná množina prazdná vrátí NULL (kromě COUNT a COUNTD vracejí 0)-vynechají NULL hodnoty (kromě COUNT)-COUNTD, SUMD, AVGD nezapočítávají duplicitní hodnoty

Interpretace E3VPC výrazu - kvantifikátory a kompaktní formy

∀{x in R:||W(x)||α}P(x)=T prázdná množina, nebo pro všechny elementy platí P(x)=F množina není prázdná, je alespoň jeden element pro který P(x) neplatí=U jinak

∃{x in R:||W(x)||α}P(x)=F prázdná množina, nebo pro všechny elementy neplatí P(x)=T množina není prázdná, je alespoň jeden element pro který P(x) platí=U jinak

SQL syntax a tranformační pravidla

SQL SYNTAXPravidla - "generující gramatika" očíslovaná (1..50)ve formátu <QUERY> = SELECT[ALL|DISTINCT]<SELECTLIST><FRCLAUSE>[<WHCLAUSE>][<GBCLAUSE>][<HCLAUSE>]<WHCLAUSE> = WHERE <WHERE SEARCH CONDITION><SIMPLEPRED>=<COL OR VAL> <comp op> <COL OR VAL>

KEYWORDS - tučněUPPERCASE - neterminálylowercase - terminály

Převáděcí pravidlaNěkterým pravidlům SQL syntaxe odpovídá přepis do formy E3VPC.Přepisuje se neterminál X z levé strany TR <X>na zřetězení přepisů TR<Y1>... TR<Yn> doplněné o další symboly E3VPCkde <Yi> je terminál nebo neterminál podle pravé strany pravidla, případně "zděděný" neterminál X.

<TABLE REFERENCE>=<table name><correlation name>-> <correlation name> in <table name>

Specifické vlastnosti překladu (1)

● nepovinné prvky se převedou na prázdný výraz

● implicitní pravidlo převádí zřetězení prvků na zřetězení jejich překladů

● terminály se nepřekládají - stávají se z nich jména proměných

● <COL OR VAL> je v SQL neterminál, převádí se na terminál

● SQL pravidla typu "booleovská hodnota" <P> se převedou na "booleovská hodnota" TR <P>

Specifické vlastnosti překladu (2)

● Dvojice TR1 a TR2 se překládá přímo○ TR1 <FUNC SPEC> se překládá rovnou na jméno

funkce + proměnná.atribut○ TR2 <FUNSPEC> se překládá rovnou jako 0

respektive NULL - vždy se vyskytují pohromadě, první vede na vyhodnocení agregační funkce, druhá dodává hodnotu pro případ prázdné množiny

● obecně odpovídá jednomu syntaktickému pravidlu jedno převáděcí ->stejná čísla

● vnější SELECTLIST se nepřevádí (slouží v SQL jen pro vypsání výsledku; nemá vliv)

Kompletní tabulky

tabulky vedle sebe (gif)

tabulky vedle sebe (png)

Stručné zdůvodnění pravidel- základní struktura (1)

● Základem každého dotazu/poddotazu je formule ve tvaru{ TR <FRCLAUSE> : || TR <WHCLAUSE> ∧ TR <HCLAUSE> ||F } která definuje množinu ntic vracenou dotazem

● SELECT je zpracováván v FALSE-intepretaci, což odpovídá tomu, že prvky s hodnotou UNKNOWN nesplňují podmínku "vyber takové, pro které platí"

Stručné zdůvodnění pravidel - základní stuktura (2)

● GROUP BY nepatří do základního tvaru - neovlivňuje výslednou množinu

● Předpokládá se, že každá ntice obsahuje unikátní identifikátor; nejsou řešeny duplicity (pokud není implicitně řečeno) - odpovídá ALL

● SELECTLIST poddotazů je převáděn kompletně (výběr sloupce, agregace) - má vliv na výsledek vnější funkce

Stručné zdůvodnění pravidel- složené predikáty

= takové, které zahrnují poddotaz● pravidla 20 a 38 jsou symetrická - stejné

zpracování v sekci WHERE <COMPLEXPRED> i HAVING <HACOMPLEXPRED>

● oddělená pravidla pro jednoduché poddotazy (výstupem je celý list) <SUBQ> a pro poddotazy, kde výstupní seznam obsahuje funkci <AFSUBQ>

● všechny čtyři kombinace jsou převáděny strukturou TR1.... TR2

Stručné zdůvodnění pravidel-klíčové slovo DISTINCT

● Po agregačních funkcích - je zahrnuto do zpracování funkce

● Ve výsledku poddotazu - není potřeba samostatně, je vyřešeno přítomností kvantifikátoru v pravidlech pro poddotazy

Stručné zdůvodnění pravidel- prázdné množiny

● Prázdné množiny jako výsledek poddotazu○ pro ∀ je výsledek TR1 TRUE○ pro ∃ je výsledek TR1 FALSE○ jednoduché funkce fungují díky TR2 přímo○ funkce <AFSUBQ> typu obsahují v příslušných

pravidlech speciální term TR3● Pravidla pro práci se složenými

porovnávacími predikáty obsahují speciální term pro korektní zpracování prázdných množin

Příklad

SELECT d.managerFROM DEPT dWHERE d.location = ALL

SELECT e.residenceFROM EMP eWHERE e.d# = d.d#

GROUP BY d.managerHAVING AVG(d.nofemp) >500

Řešení● 1-15:

● <WHERE..>

● TR1

● TR2

● <WHERE..>

Řešení - dokončení

● <HAVING..>

● <GB..>

● =>

Ekvivalence SQL dotazů

Postup:● převod obecného E3VPC výrazu do

kanonického tvaru● porovnání pomocí dvouhodnotové

predikátové logiky

. . . použití třihodnotové predikátové logiky ukazuje, že i když dva dotazy jsou ekvivalentní v dvouhodnotové interpretaci, můžou se lišit v reálném SQL

Kanonický E3VPC výraz

● s každým atomickým predikátem je asociován interpretační operátor

● výraz neobsahuje žadné další interpretační operátory

● výraz neobsahuje kompaktní formy

s kanonickým výrazem můžeme dál pracovat pomocí dvouhodnotové logiky (důvod: každý atomický predikát má interpretační operátor, a interpretována třihodnotová logika je dvouhodnotová, jak již bylo ukázáno)

Transformace E3VPC výrazu do kanonické formy

1. ||P(x) ∨ Q(x)||α ⇔ ||P(x)||α ∨ ||Q(x)||α

2. ||P(x) ∧ Q(x)||α ⇔ ||P(x)||α ∧ ||Q(x)||α

3. ||¬P(x)||α ⇔¬||P(x)||¬α

4. || ||P(x)||α||β ⇔ ||P(x)||α

5. ||∃ x in R: P(x)||α ⇔ ∃ x in R: ||P(x)||α

6. ||∀ x in R: P(x)||α ⇔ ∀ x in R: ||P(x)||α

Neplatí:P ∨ ¬P ⇔ 1 a P ∧ ¬P ⇔ 0nedefinují jak posunout interpretační operátor z podvýrazu do každého atomického predikátu, takže je nepotřebujeme

Eliminace kompaktních forem

Věta 1.

||∃{x in R: ||P(x)||α}Q(x)||β ⇔ ∃ x in R: ||P(x)||α ∧ ||Q(x)||β

Věta 2.

||∀{x in R: ||P(x)||α}Q(x)||β ⇔ ∀ x in R: ||¬P(x)||¬α ∨ ||Q(x)||β

Ekvivalence SQL dotazů - tříhodnotová logika

Problém: Interpretace unknown: dva dotazy, které se v kanonickém tvaru liší jen o typ interpretace (T nebo F)

TR<Q1> = {x in R: ||P(x)||F}

TR<Q2> = {x in R: ||P(x)||T}

. . . jsou ekvivalentní?

Ekvivalence SQL dotazů - množina kritické ekvivalence

-SQL dotazy, u kterých se může výše uvedený problém projevit, tvoří množinu kritické ekvivalence (critical equivalence set).-Nastává při převodu E3VPC výrazu na kanonický tvar (kvůli pravidlům 3 a 4)

Jaké typy dotazů v SQL tam patří?

Množina kritické ekvivalence - jednoduchý dotaz

NE Pravidlo 3:TR<Q1> = {x in R: ||¬P(x)||F}

TR<Q2> = {x in R:¬||P(x)||F} ⇒ {x in R:||¬P(x)||T}

Pravidlo 4:TR<Q1> = {x in R: ||P(x)||F}

TR<Q2> = {x in R: || ||P(x)||T||F} ⇒{x in R: ||P(x)||T}...ale v SQL neexistuje dotaz jako Q2

Množina kritické ekvivalence - univerzální kvantifikace

ANO

Q1: SELECT * FROM R x WHERE NOT EXISTS SELECT * FROM S y WHERE x.Ai = y.Bi ∧ y.Bj ≠ 'P'Q2: SELECT * FROM R x WHERE NOT x.Ai IN SELECT y.Bi FROM S y WHERE x.Bj ≠ 'P'

Množina kritické ekvivalence - univerzální kvantifikace

E3VPC:1) ||¬∃ {y in S: ||Q(x,y) ∧ P(y)||α}||β

2) ||¬∃ {y in S: || P(y)||α}Q(x,y)||β

Kanonický tvar:1)∀ y in S: ||¬Q(x,y)||¬α ∨ ||¬P(y)||¬α

2)∀ y in S: ||¬Q(x,y)||β ∨ ||¬P(y)||¬α

Jsou ekvivalentní právě když β = ¬α, což obecně nemusí platit (a neplatí v uvedeném příkladu, kde β = α = F)

Množina kritické ekvivalence - existenční kvantifikace

ANOE3VPC:1) ||∃{y in S:||Q(x,y) ∧ P(y)α}||β

2) ||∃{y in S:||P(y)||α}Q(x,y)||β

Kanonický tvar:1) ∃ y in S: ||Q(x,y)||α ∧ ||P(y)||α

2) ∃ y in S: ||Q(x,y)||β ∧ ||P(y)||α

Jsou ekvivalentní právě když α = β (α je vždy F, β může být T pokud predikát je části univerzálně kvantifikovaného predikátu)

Ekvivalence SQL dotazů - závěr

(1) SQL dotazy, které neobsahují univerzální kvantifikátor nikdy nepatří do množiny kritické ekvivalence(2) SQL dotazy, které obsahují univerzální kvantifikátor vždy patří do množiny kritické ekvivalence

Děkujeme za pozornost