Twierdzenie Churcha-Rossera

W rachunku lambda twierdzenie Churcha -Rossera stwierdza, że ​​​​stosując reguły redukcji do warunków , kolejność, w jakiej wybierane są redukcje, nie ma wpływu na ostateczny wynik.

Dokładniej, jeśli istnieją dwie różne redukcje lub sekwencje redukcji, które można zastosować do tego samego składnika, to istnieje składnik, który jest osiągalny z obu wyników, stosując (być może puste) sekwencje dodatkowych redukcji. Twierdzenie zostało udowodnione w 1936 roku przez Alonzo Churcha i J. Barkleya Rossera , od którego pochodzi jego nazwa.

Twierdzenie jest symbolizowane przez sąsiedni diagram: Jeśli składnik a można zredukować zarówno do b , jak i c , to musi istnieć dodatkowy składnik d (prawdopodobnie równy b lub c ), do którego można zredukować zarówno b, jak i c . Postrzegając rachunek lambda jako abstrakcyjny system przepisywania , twierdzenie Churcha-Rossera stwierdza, że ​​​​reguły redukcji rachunku lambda są zbieżne . W konsekwencji twierdzenia, termin w rachunku lambda ma co najwyżej jedną postać normalną , co uzasadnia odniesienie do „ postaci normalnej” danego terminu normalizowalnego.

Historia

W 1936 roku Alonzo Church i J. Barkley Rosser udowodnili, że twierdzenie to obowiązuje dla β-redukcji w rachunku λI (w którym każda wyabstrahowana zmienna musi występować w treści wyrazu). Metoda dowodu jest znana jako „skończoność rozwoju” i ma dodatkowe konsekwencje, takie jak twierdzenie o standaryzacji, które odnosi się do metody, w której redukcje można przeprowadzać od lewej do prawej, aby osiągnąć postać normalną (jeśli taka istnieje). Wynik dla czystego, nieokreślonego rachunku lambda został udowodniony przez DE Shroera w 1965 roku.

Czysty, nietypowany rachunek lambda

Jednym z rodzajów redukcji w czystym, nieokreślonym rachunku lambda, do którego ma zastosowanie twierdzenie Churcha-Rossera, jest redukcja β, w której termin podrzędny postaci jest skracany przez ${\ Displaystyle (\ lambda xt) s}$ podstawienie ${\ Displaystyle t [x: = s]}$ . Jeśli β-redukcja jest oznaczona przez ${\ displaystyle \ rightarrow _ {\ beta}},$ a jej zwrotne, przechodnie zamknięcie przez ${\ displaystyle \ twoheadrightarrow _ {\ beta}},$ to twierdzenie Churcha-Rossera jest takie, że:

${\ Displaystyle \ forall M, N_ {1 },N_{2}\in \Lambda :{\text{if}}\ M\twoheadrightarrow _{\beta }N_{1}\ {\text{and}}\ M\twoheadrightarrow _{\beta }N_{ 2}\ {\text{wtedy}}\ \istnieje X\in \Lambda :N_{1}\twoheadrightarrow _{\beta }X\ {\text{i}}\ N_{2}\twoheadrightarrow _{\beta }X}$

Konsekwencją tej właściwości jest to, że dwa terminy równe w muszą sprowadzić się do wspólnego terminu: ${\ displaystyle \ lambda \ beta}$

${\ Displaystyle \ forall M, N \ in \ Lambda: {\ tekst {jeśli}} \ \ lambda \beta \vdash M=N\ {\text{wtedy}}\ \exists X:M\twoheadrightarrow _{\beta }X\ {\text{i}}\ N\twoheadrightarrow _{\beta }X}$

Twierdzenie dotyczy również redukcji η, w której podczłon ${\ Displaystyle \ lambda x.Sx}$ zastępuje się ${\ Displaystyle S}$ . Dotyczy to również redukcji βη, połączenia dwóch reguł redukcji.

Dowód

W przypadku redukcji β jedna metoda dowodowa pochodzi od Williama W. Taita i Pera Martina-Löfa . Powiedzmy, $:$ relacja binarna spełnia właściwość diamentu, jeśli

${\ Displaystyle \ forall M, N_ {1}, N_ { 2}\in \Lambda :{\text{if}}\ M\rightarrow N_{1}\ {\text{and}}\ M\rightarrow N_{2}\ {\text{wtedy}}\ \exists X \in \Lambda :N_{1}\rightarrow X\ {\text{i}}\ N_{2}\rightarrow X}$

$Rossera$ jest stwierdzeniem, że właściwość diamentu. Wprowadzamy nową redukcję $i która spełnia$ której zwrotnym domknięciem przechodnim jest ${\ displaystyle \ twoheadrightarrow _ {\ beta}}$ diamentu. Z $indukcji$ liczby kroków w redukcji wynika zatem, że diamentu.

Relacja ${\ displaystyle \ rightarrow _ {\|}}$ ma reguły tworzenia:

• ${\ Displaystyle M \ rightarrow _ {\|} M}$
• Jeśli ${\ Displaystyle M \ rightarrow _ {\|} M '}$ i ${\ Displaystyle N \ rightarrow _ {\|} N'}$ to $i$ ( $_$ _ ${\ Displaystyle (\ lambda xM) N \ strzałka w prawo _ {\|} M'[x: = N']}$

Reguła redukcji η może być bezpośrednio udowodniona przez Churcha-Rossera. Następnie można udowodnić, że β-redukcja i η-redukcja komutują się w tym sensie, że:

Jeśli ${\ Displaystyle M \ rightarrow _ {\ beta} N_ {1}}$ i ${\ Displaystyle M \ rightarrow _ {\ eta} N_ {2}}$ to istnieje termin ${\ Displaystyle X}$ takie, że ${\ Displaystyle N_ {1} \ rightarrow _ {\ eta} X}$ i ${\ Displaystyle N_ {2} \ rightarrow _ {\ beta} X}$ .

Stąd możemy wywnioskować, że βη-redukcja jest metodą Churcha-Rossera.

Normalizacja

Reguła redukcji, która spełnia własność Churcha-Rossera, ma tę właściwość, że każdy termin M może mieć co najwyżej jedną odrębną postać normalną, jak następuje: jeśli X i Y są normalnymi formami M , to zgodnie z własnością Churcha-Rossera oba redukują się do równy wyraz Z . Oba terminy są już normalnymi formami, więc ${\ Displaystyle X = Z = Y}$ .

Jeśli redukcja jest silnie normalizująca (nie ma nieskończonych ścieżek redukcji), to słaba postać własności Churcha-Rossera implikuje pełną własność (patrz lemat Newmana ). Słaba właściwość dla relacji to: ${\ displaystyle \ rightarrow}$

$_$ _ $_$ _ ${\ Displaystyle M \ rightarrow N_ {2}}$ wtedy istnieje termin ${\ Displaystyle X}$ taki, że ${\ Displaystyle N_ {1} \ twoheadrightarrow X}$ i ${\ styl wyświetlania N_{2}\twoheadrightarrow X}$ .

Warianty

Twierdzenie Churcha-Rossera dotyczy również wielu wariantów rachunku lambda, takich jak rachunek lambda z prostym typem , wiele rachunków z zaawansowanymi systemami typów i rachunek wartości beta Gordona Plotkina . Plotkin użył również twierdzenia Churcha-Rossera, aby udowodnić, że ocena programów funkcjonalnych (zarówno dla oceny leniwej , jak i chętnej ) jest funkcją od programów do wartości ( podzbiór warunków lambda).

W starszych artykułach badawczych mówi się, że system przepisywania to Church-Rosser lub ma właściwość Church-Rosser, gdy jest zbieżny .

Notatki

• Alam, Jesse (2017). Zalta, Edward N. (red.). The Stanford Encyclopedia of Philosophy (wyd. Jesień 2017). Laboratorium Badań Metafizycznych Uniwersytetu Stanforda.
•   Kościół, Alonzo ; Rosser, J. Barkley (maj 1936), „Niektóre właściwości konwersji” (PDF) , Transactions of the American Mathematical Society , 39 (3): 472–482, doi : 10.2307/1989762 , JSTOR 1989762 .
•   Barendregt, Hendrik Pieter (1984), Rachunek lambda: jego składnia i semantyka , Studies in Logic and the Foundations of Mathematics, tom. 103 (wydanie poprawione), North Holland, Amsterdam, ISBN 0-444-87508-5 , zarchiwizowane z oryginału w dniu 2004-08-23 . Errata .