Relacja silnie konfluentna: Różnice pomiędzy wersjami
| [wersja nieprzejrzana] | [wersja nieprzejrzana] |
Usunięta treść Dodana treść
wersja 1 |
drobne |
||
Linia 1:
'''Relacja silnie konfluentna''' (lub po prostu relacja konfluentna) to [[relacja]] taka, że jeśli istnieje ciąg elementów będących do siebie kolejno w relacji z <math>a</math> do <math>b</math> oraz z <math>a</math> do <math>c</math>, to istnieje takie <math>d</math>, że istnieją ciąg elementów będących kolejno do 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ę też zejść.
Każda [[relacja symetryczna]] jest silnie konfluentna - możemy wrócić do <math>a</math> tą samą drogą jaką tam się znaleźliśmy.
Dlatego też konfluencja jest "interesująca" tylko w przypadku relacji które nie są symetryczne.
Każda relacja silnie konfluentna jest też [[relacja słabo konfluentna|słabo konfluentna]].
=== Systemy obliczeń ===
Konfluencja jest bardzo ważnym pojęciem w [[teoria obliczeń|teorii obliczeń]] - jeśli system dokonywania obliczeń jest
silnie konfluentny to niezależnie od kolejności wykonywania obliczeń zawsz dojdziemy do tego samego wyniku.
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]]).▼
Np. 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:
Linia 15 ⟶ 19:
Nie wyklucza to jednak sytuacji w której obliczenia jedną metodą dadzą wynik a 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ą ważną właściwością systemów silnie konfluentnych jest unikalność [[postać normalna|postaci normalnych]].
| |||