Syntax highlighting of Archiv/Formální základy databázové technologie/TransitiveClosure

Binární relace <math>R</math> je '''tranzitivní''', jestliže <math>∀ (a,b)∈R</math> a <math>(b,c)∈R</math> také <math>(a,c)∈R</math>.

'''Tranzitivní uzávěr <math>R^+</math>''' relace <math>R</math>, je nejmenší tranzitivní relace obsahující <math>R</math>.
* v praxi užitečný – např. hledání spojení s přestupy v dopravě, nebo hledání nejkratší cesty v grafu, apod.
{{theorem 
  | Pro schéma binární relace <math>R</math> v <math>A_R</math> neexistuje výraz, který ∀ relaci <math>R</math> počítá její tranzitivní uzávěr <math>R^+</math>.
  | o tranzitivním uzávěru relace
}} 

{{TODO|důkaz}}

;Dk (sporem a indukcí přes počet operací v hypotetickém výrazu pro výpočet tranzitivního uzávěru RA):
'''Pozn:''' 💡 Nestačí ani rozšíření o aritmetické výrazy, agregační fce a ano/ne dotazy, částečné řešení poskytuje Datalog
* uvažujme binární relaci <math>R_s=\{a_1a_2, a_2a_3, ..., a_{s-1}a_s\}</math> 
:⇔ <math>a_1→a_2→a_3…</math> ⇒ jejím tranzitivním uzávěrem je <math>R^+_s=\{a_ia_j: i < j\}</math>
* ukážeme, že ∄ výraz <math>E(R_s) = R^+_s</math>, pro všechna s
'''Lemma:''' výraz relační algebry <math>E(R_s) ≅ \{b_1b_2: Γ(b_1,b_2)\}</math> (pro dost.velké <math>s</math>), kde <math>Γ</math> je v DNF
: lze se na to dívat tak, že: 
:: <math>E(R_s) = \{(a_i,a_j):</math> 
::: <math>(a_i,a_j) \in R_s \or</math> 
::: <math>(a_i,x) \in R_s \and (x, aj) \in R_s \or</math>
::: <math>(a_i,x) \in R_s \and (x, y) \in R_s \and (y, aj) \in R_s \or</math>
:: <math>...\}</math>
* tohle Lemma se dokazuje indukcí dle počtu operátorů v E
* sporem, nechť takové <math>E</math> existuje (je konečné), pak dokážu zvýšit s natolik, že <math>(a_1,a_s)</math> nebude <math>E(R_s)</math>

{{Collapse|Dk (sporem a indukcí přes počet operací v hypotetickém výrazu pro výpočet tranzitivního uzávěru RA)|
# Nechť <math>\sum_s = \{a_1,a_2,...,a_s\}, s \geq 1</math>, je množina konstant, na které neexistuje uspořádání a
#: <math>R_s =\{a1a2, a2a3,...,as-1as\}</math>
#: Pz.: Rs grafu a1  a2 as, tj. transitivita je definovaná pomocí konektivity v orientovaném grafu.
#: Pz.: je-li na sdefinováno uspořádání , pak
#:: <math>Rs+(Rs 1Rs )(1  2)</math>
# Ukážeme, že pro libovolný výraz E(R) existuje s takové, že E(R_s) Rs+.
# Lemma: Je-li <math>E</math> výraz relační algebry, pak pro dostatečně velké s
#:: <math>E(R_s) b1,...,bk |(b1,...,bk)</math>,
#: kde k 1 a  je formule v disjunktivní normální formě.
#: Atomické formule v mají speciální tvar:
#:: <math>bi = aj, bi aj</math>,
#:: <math>bi = bj + c</math> nebo <math>bi bj + c</math>, kde c je (ne nutně kladná) konstanta, přičemž
#:: bj + c je zkratka pro “takové am, pro které bj = am-c“
#: Doména interpretace pro ohodnocení proměnných bj je s.
#: Pz.: <math>bi = bj + c bi</math> je za bj ve vzdálenosti c uzlů.
# '''Dk(sporem):'''
#* existuje E tak, že <math>E(R) = R+</math> a jakoukoliv relaci R, tj. i <math>E(Rs) =Rs+</math> pro dostatečně velká s
#* dle lemmatu, <math>Rs+ b1,b2 |(b1,b2)</math>
#: Nastávají dva případy:
## každá klauzule z obsahuje atom tvaru
##: <math>b1=ai, b2=ai</math> nebo <math>b1=b2+ c (b=b1- c)</math>
##: Nechť <math>b1b2 =amam+d</math> ,
##: kde m  libovolné i a d libovolné c
##: <math>b1=am</math> a <math>b2 =am+d</math> nevyhovuje žádné klauzuli z .
##: spor (amam+d Rs+ )
## v existuje klauzule s atomy obsahujícími jen 
##: Nechť b1b2 =am+dam , kde ani bi am ani bi  am+d
##: není obsaženo v  a d 0 je větší než libovolné c
##: v b1b2+ c nebo b2 b1+ c v (viz konstrukce )
##: am+d am E(Rs) pro postačující s, ale Rs+ spor
##: Tedy: Pro jakýkoliv výraz E vždy existuje s pro něž
##: E(Rs) Rs+
# '''Dk lemmatu(indukcí dle počtu operátorů v E):'''
## operátorů E Rs nebo E je relační konstanta stupně 1
##: <math>E b1,b2 | b2=b1 + 1,</math>resp.
##: <math>E b1 | b1 = c1 b1=c2b1 = cm,</math>
## 
### E E1 E2, E1-E2, E1  E2
#:: <math>E1b1,...,bk | 1(b1,...,bk)</math>
#:: <math>E2 b1,...,bm | 2(b1,...,bm)</math>
#:: pro a - je k=m a tedy
#:: <math>E b1,...,bk | 1(b1,...,bk) (b1,...,bk)</math>, resp. ,
#:: <math>E b1,...,bk | 1(b1,...,bk)  2(b1,...,bk)</math>,
#:: pro
#:: <math>E b1,...,bk bk+1,...,bk+m | 1(b1,...,bk) 2( bk+1,...,bk+m)</math>
#:: !! pak následuje transformace do DNF.
### E E1() a obsahuje buď <math>=</math> nebo 
#:: <math>E b1,...,bk |1(b1,...,bk) (b1,...,bk)</math>
### E E1S
#:: Budeme uvažovat projekci odstraňující jeden atribut
#:: jde o posloupnost permutací proměnných a eliminaci poslední komponenty
#:: eliminace bk vede k
#:: <math>b1,...,bk-1|  bk (b1,...,bk)</math>,kde  je v DNF
#:: podle a) ..
#:: <math>i=1..mb1,...,bk-1 |bki(b1,...,bk)</math>
#:: budeme eliminovat  z jednoho konjunktu
##* v i není bk=ai, bi =bk +c, bk=bi +c
##: b1,...,bk-1 i(b1,...,bk-1)
##: kde i neobsahuje bkai , bi bk +c, bk bi +c
##* v i je buď bk=ai, bi =bk +c, bk=bi +c
##: provedou se substituce za bk
##: výsledky se upraví na TRUE
##: nebo FALSE
##: nebo <math>bt=bj +g</math>
##: a přidají se: bi aj pro s-c  j s, resp.
##: bi aj pro 1  j c
}}
{{Zdroje|
* Zdroj (znění a důkaz věty):
** Věta: For an arbitrary binary relation R, there is no expression E(R) in relational algebra equivalent to R+, the transitive closure of R.

** Článek: Alfred V. Aho and Jeffrey D. Ullman: Universality of data retrieval languages. In POPL '79: Proceedings of the 6th ACM SIGACT-SIGPLAN symposium on  Principles of programming languages, San Antonio, Texas, 1979, strany 110--119
** [http://db.cs.berkeley.edu/cs286sp07/aho-ullman.pdf link]

V češtině u Prof. Pokorného na [http://ksi.ms.mff.cuni.cz/~pokorny/vyuka/pokorny.dj/ slajdech].

A pokud to někdo náhodou stále nechápe, tak jako já, tak doporučuji materiály z jedné nizozemské univerzity, kde je dopodrobna rozebrán jak důkaz lemmatu, tak hlavního teorému:
[http://wwwis.win.tue.nl/~tcalders/teaching/advancedDB08/ex/tc.pdf Lemma1]
[http://wwwis.win.tue.nl/~tcalders/teaching/advancedDB09/notes/lecture02.pdf MainTheorem]
}}