Tekst źródłowy strony Relacja silnie konfluentna

'''Relacja silnie konfluentna''' (lub po prostu relacja konfluentna) – [[Relacja (matematyka)|relacja]] taka, że jeśli istnieje [[Ciąg (matematyka)|ciąg]] elementów będących w stosunku do siebie kolejno w relacji prowadzący od <math>a</math> do <math>b</math> oraz ciąg od <math>a</math> do <math>c</math> o tej samej własności, to istnieje takie <math>d,</math> że istnieją ciągi elementów będących kolejno względem siebie w relacji z <math>b</math> do <math>d</math> oraz z <math>c</math> do <math>d.</math> Mówiąc językiem [[teoria grafów|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 <math>a</math> 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 [[relacja słabo konfluentna|słabo konfluentna]].

== Systemy obliczeń ==
Konfluencja jest pojęciem w [[teoria obliczeń|teorii obliczeń]] – jeśli system dokonywania obliczeń jest silnie konfluentny, to niezależnie od kolejności wykonywania obliczeń zawsze 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 [[rachunek lambda|rachunku lambda]] jest silnie konfluentny ([[twierdzenie Churcha-Rossera]]).

== Postać normalna ==
Drugą właściwością systemów silnie konfluentnych jest unikalność [[Postać normalna (matematyka)|postaci normalnych]]. Postać normalna to element, którego nie da się zredukować. Element <math>a</math> ma postać normalną <math>b,</math> jeśli istnieje ciąg redukcji z <math>a</math> do <math>b.</math> 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 +.

== Bibliografia ==
* Handbook of automated reasoning, Volume 1 By John Alan Robinson, Andreĭ Voronkov, strona 561. {{ISBN|9780444829498}}.
* Handbook of Formal Languages: Beyond words By Grzegorz Rozenberg, Arto Salomaa, strona 281. {{ISBN|9783540606499}}.

{{Relacje matematyczne}}

[[Kategoria:Własności relacji dwuczłonowych]]
[[en:Confluence (abstract rewriting)#Strong confluence]]