Lemat Newmana

W matematyce , w teorii systemów przepisywania , lemat Newmana , powszechnie nazywany lematem diamentu , stwierdza, że kończący (lub silnie normalizujący) abstrakcyjny system przepisywania (ARS), to znaczy taki, w którym nie ma nieskończonych sekwencji redukcji, jest zlewający się , jeśli jest lokalnie zlewający się . W rzeczywistości kończący ARS jest konfluentny dokładnie wtedy, gdy jest lokalnie konfluentny.

Równoważnie, dla każdej relacji binarnej bez malejących nieskończonych łańcuchów i spełniającej słabą wersję własności diamentu, istnieje unikalny element minimalny w każdym spójnym elemencie relacji rozpatrywanej jako graf .

Dziś jest to postrzegane jako czysto kombinatoryczny wynik oparty na solidności wynikającej z dowodu Gérarda Hueta w 1980 r. Oryginalny dowód Newmana był znacznie bardziej skomplikowany.

Diamentowy lemat

Pomysł dowodu (linie proste i linie faliste oznaczające odpowiednio → i ): Biorąc pod uwagę t ₁ t t ₂ , wykonaj indukcję na długości wyprowadzenia. Uzyskaj t ′ z lokalnego zbiegu, a t ′ z hipotezy indukcyjnej ; podobnie dla t ′ ′ .

Ogólnie rzecz biorąc, lemat Newmana można postrzegać jako kombinatoryczny wynik dotyczący relacji binarnych → na zbiorze A (zapisanym od tyłu, tak że a → b oznacza, że b jest poniżej a ) o następujących dwóch właściwościach:

→ jest dobrze uzasadnioną relacją : każdy niepusty podzbiór X z A ma element minimalny (element a z X taki, że a → b dla żadnego b w X ). Równoważnie, nie ma nieskończonego łańcucha $0 a \to a 1 \to a 2 \to a 3 \to ...$ . W terminologii systemów przepisujących → kończy się.
Każde pokrycie jest ograniczone poniżej. To znaczy, jeśli element a w A obejmuje elementy b i c w A w tym sensie, że $a \to b$ i $a \to c$ , to istnieje element d w A taki, że $b * \to d$ i $c * \to d$ , gdzie ∗ → oznacza zwrotne domknięcie przechodnie z →. W terminologii systemów przepisywania → jest lokalnie zlewający się.

Lemat stwierdza, że jeśli powyższe dwa warunki są spełnione, to → jest zbieżne: ilekroć $a * \to b$ i $a * \to c$ , istnieje element d taki, że $b * \to d$ i $c * \to d$ . Ze względu na zakończenie → oznacza to, że każdy spójny składnik → jako wykresu zawiera unikalny minimalny element a , ponadto $b * \to a$ dla każdego elementu b komponentu.

Notatki

MHA Newmana . O teoriach z kombinatoryczną definicją „równoważności” . Annals of Mathematics, 43, nr 2, strony 223–243, 1942.
Paterson, Michael S. (1990). Automaty, języki i programowanie: XVII międzynarodowe kolokwium . Notatki z wykładów z informatyki. Tom. 443. Warwick University, Anglia: Springer. ISBN 978-3-540-52826-5 .

Podręczniki

Term Rewriting Systems , Terese, Cambridge Tracts in Theoretical Computer Science, 2003. (link do książki)
Przepisywanie terminów i wszystko inne , Franz Baader i Tobias Nipkow, Cambridge University Press, 1998 (link do książki)
John Harrison, Handbook of Practical Logic and Automated Reasoning , Cambridge University Press, 2009, ISBN 978-0-521-89957-4 , rozdział 4 „Równość”.

Linki zewnętrzne

Diamentowy lemat w PlanetMath .
„Newman's Proof of Newman's Lemma”, plik PDF na temat oryginalnego dowodu , zarchiwizowany 6 lipca 2017 r. W Wayback Machine