Důkaz korektnosti Dijkstry

Po skončení má pro každý vrchol $v$ platit $l(v) = \mathrm{dist}(v)$, kde $\mathrm{dist}(v)$ je skutečná délka nejkratší cesty $s \to v$ (a $l(v) = \infty$ právě pro nedosažitelné vrcholy). Vektor $p$ má navíc kódovat strom nejkratších cest.

Přímo „po skončení“ se to ale dokazuje špatně. Trik (a jediná nová věc téhle lekce): dokážeme silnější průběžné tvrzení — invariant, který platí po celou dobu běhu. Silnější tvrzení se indukcí často dokazuje snáz, protože máš silnější indukční předpoklad.

Prázdná cesta z $s$ do $s$ má délku $0$, takže $\mathrm{dist}(s) \le 0$. A kratší to být nemůže, protože všechny váhy jsou nezáporné — každý sled má délku $\ge 0$. Tady poprvé (a zatím nenápadně) vstupuje předpoklad $c : E(G) \to \mathbb{R}^+_0$: kdyby přes $s$ vedl záporný cyklus, bylo by „$\mathrm{dist}(s) = -\infty$“ a báze by spadla hned [L2.1].

Konečná značka vzniká jedině relaxací: někdy dříve se uzavíral nějaký vrchol $x \in R$ a vnitřní smyčka nastavila $D(v) := D(x) + c(x,v)$, $p(v) := x$. Po řetízku předchůdců $p$ zpátky až do $s$ to znamená, že $D(v)$ je délka skutečného existujícího sledu $s \to \cdots \to x \to v$ [L2.3]. Nejkratší cesta nemůže být delší než nějaký konkrétní sled, tedy $\mathrm{dist}(v) \le D(v)$.

(Okrajový případ $D(v) = \infty$: pak mají $\infty$ všechny vrcholy mimo $R$. Všechny hrany vedoucí z $R$ ven už ale relaxovány byly — kdyby nějaká existovala, její konec by měl konečnou značku. Žádná tedy neexistuje, vrcholy mimo $R$ jsou nedosažitelné a $\mathrm{dist} = \infty = D$ sedí. Banka i slidy tento případ přecházejí mlčky; u písemky stačí věta v závorce.)

$P$ musí někde poprvé opustit množinu $R$. Označme $y$ první vrchol na $P$, který neleží v $R$, a $x$ jeho předchůdce na $P$. Z definice „první“ plyne $x \in R$ — a na $x$ se proto vztahuje indukční předpoklad: $D(x) = \mathrm{dist}(x)$. (Klidně může být $y = v$, pokud $P$ vede až do $v$ celou dobu uvnitř $R$ — argument níže funguje beze změny.)

Když byl $x$ přidán do $R$, vnitřní smyčka otestovala všechny jeho odchozí hrany do neuzavřených vrcholů — tedy i hranu $(x,y)$. Po této relaxaci platí (a značky už nikdy nerostou, takže platí pořád):

kde $P[s,x]$ je úsek cesty $P$ od $s$ do $x$. Prostřední nerovnost: $P[s,x]$ je nějaká $s$–$x$ cesta, takže není kratší než $\mathrm{dist}(x)$. Slovy: značka prvního vrcholu za hranicí $R$ není horší než délka $P$ až k němu.

Zbytek cesty $P$ od $y$ do $v$ se skládá z hran s váhami $c \ge 0$, takže má délku $\ge 0$ a

To je celé — jediné místo důkazu, kde nezápornost vstupuje, a přesně to místo, které záporná hrana zboří (viz níže). Složením řetízku:

Cesta $P$ má $|P| = 0 < 1 = D(a)$, takže podle důkazu by měl existovat spor. Projdi řetízek: první vrchol mimo $R = \{s\}$ na $P$ je $y = b$, předchůdce $x = s$. Odhad značky funguje: $D(b) \le \mathrm{dist}(s) + c(s,b) = 2 = |P[s,b]|$. Jenže další krok

Zbytek cesty ($b \to a$ s váhou $-2$) má zápornou délku, takže prefix je delší než celá cesta. Spor se nekoná, $D(b) = 2$ je klidně větší než $D(a) = 1$, Dijkstra s čistým svědomím uzavře $a$ se špatnou hodnotou — a hranu $(b,a)$ už nikdy neotestuje, protože vnitřní smyčka jede jen přes $w \notin R$ [L2.4].

Je to tentýž argument v jiném kabátě. Případ „$k \in R$“ = naše relaxace hrany $(x,y)$ na hranici (všechny hrany z $R$ ven byly otestovány — proto víme $D(y) \le \mathrm{dist}(x) + c(x,y)$). Případ „$k \notin R$“ = naše nezápornost + minimalita $v$ (cesta procházející vrcholem mimo $R$ nese už aspoň $l(v)$ a nezáporné hrany nic neslevují — přesně řetízek $D(y) \le |P| < D(v)$ obrácený do sporu). U zkoušky si vyber jednu verzi a doveď ji do konce; verze sporem z banky je vzorové řešení a hůř se v ní něco zamlčí.