Propriété de normalisation (réécriture abstraite) - Normalization property (abstract rewriting)

En logique mathématique et en informatique théorique , un système de réécriture a la propriété de normalisation ( forte ) ou se termine si chaque terme est fortement normalisant ; c'est-à-dire si chaque séquence de réécritures se termine finalement par un terme irréductible , également appelé forme normale . Un système de réécriture peut également avoir la propriété de normalisation faible , ce qui signifie que pour chaque terme, il existe au moins une séquence particulière de réécritures qui donne finalement une forme normale, c'est-à-dire un terme irréductible.

Calcul lambda

Calcul lambda non typé

Le lambda calcul pur non typé ne satisfait pas la propriété de normalisation forte, ni même la propriété de normalisation faible. Considérez le terme . Il a la règle de réécriture suivante : Pour tout terme , ${\style d'affichage \lambda x.xxx}$${\style d'affichage t}$

${\displaystyle (\mathbf {\lambda } x.xxx)t\rightarrow ttt}$

Mais considérez ce qui se passe lorsque nous nous appliquons à lui-même : ${\style d'affichage \lambda x.xxx}$

${\displaystyle {\begin{aligned}(\mathbf {\lambda } x.xxx)(\lambda x.xxx)&\rightarrow (\mathbf {\lambda } x.xxx)(\lambda x.xxx)(\ lambda x.xxx)\\&\rightarrow (\mathbf {\lambda } x.xxx)(\lambda x.xxx)(\lambda x.xxx)(\lambda x.xxx)\\&\rightarrow (\mathbf {\lambda } x.xxx)(\lambda x.xxx)(\lambda x.xxx)(\lambda x.xxx)(\lambda x.xxx)\\&\rightarrow \ \ldots \,\end{aligned }}}$

Par conséquent, le terme n'est ni fortement ni faiblement normalisant. ${\style d'affichage (\lambda x.xxx)(\lambda x.xxx)}$

Calcul lambda typé

Divers systèmes de typé lambda - calcul , y compris le lambda - calcul simplement typé , Jean-Yves Girard « s système F , et Thierry Coquand » s calcul des constructions sont fortement normalisant.

Un système de calcul lambda avec la propriété de normalisation peut être considéré comme un langage de programmation avec la propriété que chaque programme se termine . Bien que ce soit une propriété très utile, elle a un inconvénient : un langage de programmation avec la propriété de normalisation ne peut pas être Turing complete , sinon on pourrait résoudre le problème d'arrêt en voyant si le programme effectue une vérification de type. Cela signifie qu'il y a des fonctions calculables qui ne peuvent pas être définies dans le calcul lambda simplement typé (et de même il y a des fonctions calculables qui ne peuvent pas être calculées dans le calcul des constructions ou System F ).

Auto-interprétation dans le calcul lambda typé

A titre d'exemple, il est impossible de définir un auto-interprète dans aucun des calculs cités ci-dessus.

Ici, par "auto-interprète", nous entendons un programme qui prend une représentation de terme source dans un format simple (comme une chaîne de caractères) et renvoie une représentation du terme normalisé correspondant. Ce résultat d'impossibilité ne vaut pas pour les autres définitions de « auto-interprète ». Par exemple, certains auteurs ont qualifié les fonctions de type d'auto-interprètes, où est le type de représentation des termes -typés. Pour éviter toute confusion, nous appellerons ces fonctions auto-reconnaissances . Brown et Palsberg ont montré que l' auto-définies pourraient être de reconnaissance en plusieurs langues fortement normalisant, y compris système F et le système F _ω . Cela s'est avéré possible parce que les types de termes codés reflétés dans les types de leurs représentations empêchent de construire un argument diagonal . Dans leur article, Brown et Palsberg prétendent réfuter la "sagesse conventionnelle" selon laquelle l'auto-interprétation est impossible (et ils se réfèrent à cette même page Wikipédia comme un exemple de la sagesse conventionnelle), mais ce qu'ils réfutent en fait, c'est l'impossibilité de s'auto-interpréter. reconnaissances, un concept complètement différent. Dans leur travail de suivi, ils basculent vers la terminologie plus spécifique d'« auto-reconnaissance » que nous utilisons ici, en les distinguant notamment des « auto-évaluateurs », de type . Ils reconnaissent également que la mise en œuvre de l'auto-évaluation semble plus difficile que l'auto-reconnaissance, et laissent la mise en œuvre de la première dans un langage fortement normalisant comme un problème ouvert. ${\displaystyle \pi \,\tau \to \tau }$${\style d'affichage \pi \,\tau }$${\style d'affichage \tau }$${\displaystyle \pi \,\tau \to \pi \,\tau }$

Voir également

• Calcul lambda typé
• Réécriture
• Programmation fonctionnelle totale
• Conjecture de Barendregt–Geuvers–Klop
• Lemme de Newman
• Normalisation par évaluation

Remarques

Les références

• Baader, Franz ; Nipkow, Tobias (1999). Réécriture de termes et tout ça . La presse de l'Universite de Cambridge. ISBN 0-521-77920-0. 316 pages.