Relacja silnie konfluentna

Z Wikipedii

Relacja silnie konfluentna (lub po prostu relacja konfluentna) to relacja taka, że jeśli istnieje ciąg elementów będących w stosunku do siebie kolejno w relacji prowadzący od $a$ do $b$ oraz ciąg od $a$ do $c$ o tej samej własności, to istnieje takie $d$ , że istnieją ciągi elementów będących kolejno względem siebie w relacji z $b$ do $d$ oraz z $c$ do $d$ . Mówiąc językiem teorii grafów, jeśli się rozejdziemy, zawsze potrafimy się ponownie zejść.

Każda relacja symetryczna jest silnie konfluentna - możemy bowiem wrócić do $a$ tą samą drogą jaką tam się znaleźliśmy. Dlatego też własność konfluencji jest "interesująca" tylko w przypadku relacji, które nie są symetryczne. Każda relacja silnie konfluentna jest słabo konfluentna.

[edytuj] Systemy obliczeń

Konfluencja jest bardzo ważnym pojęciem w teorii obliczeń - jeśli system dokonywania obliczeń jest silnie konfluentny, to niezależnie od kolejności wykonywania obliczeń zawsz dojdziemy do tego samego wyniku.

Na przykład system złożony z liczb całkowitych, symbolu +, oraz reguły redukcji zastępującej parę liczb po obu stronach symbolu + ich sumą jest silnie konfluentny. Rozpatrzmy dwie redukcje:

2 + 3 + 4 + 5 + 6 → 2 + 3 + 4 + 11
2 + 3 + 4 + 5 + 6 → 5 + 4 + 5 + 6

Można je doprowadzić do tego samego wyniku:

2 + 3 + 4 + 11 → 2 + 3 + 15 → 2 + 18 → 20
5 + 4 + 5 + 6 → 9 + 5 + 6 → 14 + 6 → 20

Nie wyklucza to jednak sytuacji, w której obliczenia jedną metodą dadzą wynik, zaś drugą będą działać "w nieskończoność". Jednak jeśli zaczynamy stosując strategię, która działałaby "w nieskończoność", w każdym momencie możemy dojść do wyniku, jeśli zmienimy zdanie i to, do czego ta strategia doszła, zaczniemy redukować w inny sposób.

Do ważniejszych twierdzeń rachunku lambda należy to, że zbiór redukcji α i β w rachunku lambda jest silnie konfluentny (twierdzenie Churcha-Rossera).

[edytuj] Postać normalna

Drugą ważną właściwością systemów silnie konfluentnych jest unikalność postaci normalnych. Postać normalna to element, którego nie da się zredukować. Element $a$ ma postać normalną $b$ , jeśli istnieje ciąg redukcji z $a$ do $b$ . Element nie może mieć dwóch postaci normalnych, ponieważ musiałyby one redukować się do wspólnego wyrażenia, zaś postać normalna jest z definicji nieredukowalna. W dalszym ciągu element ten może jednak nie mieć żadnej postaci normalnej. W przedstawionym powyżej systemie postaciami normalnymi są samodzielne liczby bez żadnych znaków +.