Co to jest równoważność beta?

W skrypcie, który obecnie czytam na rachunku lambda, równoważność beta jest zdefiniowana następująco:

$\beta$ -equivalence $\equiv_\beta$ jest najmniejszym równoważności, który zawiera $\rightarrow_\beta$ .

Nie mam pojęcia co to znaczy. Czy ktoś może to wyjaśnić w prostszy sposób? Może z przykładem?

Potrzebuję go do lematu wynikającego z twierdzenia Church-Russer, mówiąc:

$\equiv_\beta$↠ $\twoheadrightarrow_\beta$$\twoheadrightarrow_\beta$

$\to_\beta$ to jednoetapowa relacja między terminami w -calculus. Ta relacja nie jest ani zwrotna, symetryczna ani przechodnia. Relacja równoważności jest zwrotnym, symetrycznym, przechodnim zamknięciem . To znaczy≡ β → $\lambda$$\equiv_\beta$$\to_\beta$

1. Jeśli to . M ≡ β M $M\to_\beta M'$$M\equiv_\beta M'$
2. Dla wszystkich warunków , .M ≡ β$M$$M\equiv_\beta M$
3. Jeśli'a .M ′ ≡ β$M\equiv_\beta M'$$M'\equiv_\beta M$
4. Jeśli i , to .$M\equiv_\beta M'$$M'\equiv_\beta M''$$M\equiv_\beta M''$
5. $\equiv_\beta$ jest najmniejszą relacją spełniającą warunki 1-4.

Mówiąc bardziej konstruktywnie, najpierw stosuj reguły 1 i 2, a następnie powtarzaj reguły i w kółko, dopóki nie dodadzą nowych elementów do relacji.$3$$4$

To tak naprawdę podstawowa teoria mnogości. Wiesz, czym jest relacja zwrotna, czym jest relacja symetryczna, a co relacja przechodnia, prawda? Relacja równoważności to taka, która spełnia wszystkie trzy z tych właściwości.

Prawdopodobnie słyszałeś o „przejściowym zamknięciu” relacji ? Cóż, to jest nic, ale przynajmniej przechodnia relacja który zawiera . To właśnie oznacza termin „zamknięcie”. Podobnie można mówić o „symetrycznym zamknięciu” relacji , „refleksyjnym zamknięciu” relacji i „równoważnym zamknięciu” relacji w dokładnie ten sam sposób.R R R $R$$R$$R$$R$$R$

Po namyśle możesz przekonać się, że przechodnie przejście to . Symetryczne zamknięcie to . Zamknięcie zwrotne to (gdzie to relacja tożsamości). R ∪ R 2 ∪ R 3 ∪ … R ∪ R - 1 R ∪ I $R$$R \cup R^2 \cup R^3 \cup \ldots$$R \cup R^{-1}$$R \cup I$$I$

Używamy notacji dla . To zwrotny przechodni zamknięcie z . Zauważ teraz, że jeśli jest symetryczny, każda relacja , , , , ... jest symetryczna. Zatem będzie również symetryczny. I ∪ R ∪ R 2 ∪ … R R I R R 2 R 3 R $R^*$$I \cup R \cup R^2 \cup \ldots$$R$$R$$I$$R$$R^2$$R^3$$R^*$

Zatem równoważne zamknięcie jest przejściowym zamknięciem jego symetrycznego zamknięcia, tj. . To reprezentuje sekwencję kroków, z których niektóre są krokami do przodu ( ) i niektóre krokami do tyłu ( ).( R ∪ R - 1 ) ∗ R R - $R$$(R \cup R^{-1})^*$$R$$R^{-1}$

Mówi się, że relacja ma właściwość Church-Rosser, jeśli zamknięcie równoważności jest takie samo jak relacja złożona . Jest to sekwencja kroków, w której wszystkie kroki do przodu są pierwsze, a następnie wszystkie kroki do tyłu. Tak więc właściwość Church-Rosser mówi, że wszelkie przeplatanie kroków do przodu i do tyłu można w równoważny sposób wykonać, wykonując kroki do przodu, a kroki do tyłu później.R ∗ ( R - 1 ) $R$$R^* (R^{-1})^*$