Qu'est-ce que l'équivalence bêta?

Dans le script que je lis actuellement sur le calcul lambda, l'équivalence bêta est définie comme suit:

L' équivalence est la plus petite équivalence qui contient .$\beta$$\equiv_\beta$$\rightarrow_\beta$

Je n'ai aucune idée de ce que ça veut dire. Quelqu'un peut-il l'expliquer en termes plus simples? Peut-être avec un exemple?

J'en ai besoin pour un lemme suivant le théorème de Church-Russer, disant

Si M N alors il y a un L avec M L et N \ twoheadrightarrow_ \ beta L.$\equiv_\beta$$\twoheadrightarrow_\beta$$\twoheadrightarrow_\beta$

$\to_\beta$ est la relation en une étape entre les termes du $\lambda$ -calculus. Cette relation n'est ni réflexive, ni symétrique, ni transitive. La relation d'équivalence $\equiv_\beta$ est la fermeture réflexive, symétrique et transitive de $\to_\beta$ . Ça signifie

1. Si $M\to_\beta M'$ alors $M\equiv_\beta M'$ .
2. Pour tous les termes $M$ , $M\equiv_\beta M$ est valable.
3. Si $M\equiv_\beta M'$'alors $M'\equiv_\beta M$ .
4. Si $M\equiv_\beta M'$ et $M'\equiv_\beta M''$ , alors $M\equiv_\beta M''$ .
5. $\equiv_\beta$ est la plus petite relation satisfaisant aux conditions 1-4.

De manière plus constructive, appliquez d'abord les règles 1 et 2, puis répétez les règles et encore et encore jusqu'à ce qu'elles n'ajoutent aucun nouvel élément à la relation.$3$$4$

C'est vraiment de la théorie des ensembles élémentaires. Vous savez ce qu'est une relation réflexive, qu'est-ce qu'une relation symétrique et qu'est-ce qu'une relation transitive, n'est-ce pas? Une relation d'équivalence est une relation qui satisfait à ces trois propriétés.

Vous avez probablement entendu parler de la "fermeture transitive" d'une relation ? Eh bien, il n'y a rien , mais la moindre relation transitive qui comprend . C'est ce que signifie le terme «fermeture». De même, on peut parler de la "fermeture symétrique" d'une relation , de la "fermeture réflexive" d'une relation et de la "fermeture d'équivalence" d'une relation exactement de la même manière.$R$$R$$R$$R$$R$

Avec un peu de réflexion, vous pouvez vous convaincre que la fermeture transitive de est . La fermeture symétrique est . La fermeture réflexive est (où est la relation d'identité). $R$$R \cup R^2 \cup R^3 \cup \ldots$$R \cup R^{-1}$$R \cup I$$I$

Nous utilisons la notation pour . Ceci est la fermeture réflexive et transitive de . Remarquez maintenant que si est symétrique, chacune des relations , , , , ... est symétrique. Par conséquent, sera également symétrique.$R^*$$I \cup R \cup R^2 \cup \ldots$$R$$R$$I$$R$$R^2$$R^3$$R^*$

La fermeture d'équivalence de est donc la fermeture transitive de sa fermeture symétrique, c'est-à-dire . Cela représente une séquence d'étapes, dont certaines sont des étapes avant ( ) et des étapes arrière ( ).$R$$(R \cup R^{-1})^*$$R$$R^{-1}$

On dit que la relation a la propriété de Church-Rosser si la fermeture d'équivalence est la même que la relation composite . Cela représente une séquence d'étapes dans laquelle toutes les étapes avant viennent en premier, suivies de toutes les étapes arrière. Ainsi, la propriété Church-Rosser indique que tout entrelacement des étapes avant et arrière peut être effectué de manière équivalente en effectuant des étapes avant d'abord et des étapes arrière plus tard.$R$$R^* (R^{-1})^*$