Forme bêta normale

En calcul lambda , un terme est sous forme normale bêta si aucune réduction bêta n'est possible. Un terme est sous forme normale bêta-êta si ni une réduction bêta ni une réduction êta n'est possible. Un terme est sous forme normale de tête s'il n'y a pas de bêta-redex en position de tête . La forme normale d'un terme, s'il en existe une, est unique (corollaire du théorème de Church-Rosser ). Cependant, un terme peut avoir plus d'une forme normale de tête.

Dans le calcul lambda, un bêta redex est un terme de la forme :

Un redex est en position de tête dans un terme , s'il a la forme suivante (notez que l'application a une priorité plus élevée que l'abstraction, et que la formule ci-dessous est censée être une abstraction lambda, pas une application) :

Une réduction bêta est une application de la règle de réécriture suivante à une redex bêta contenue dans un terme :

où est le résultat de la substitution du terme à la variable dans le terme .

Une réduction bêta de la tête est une réduction bêta appliquée en position de la tête, c'est-à-dire de la forme suivante :

Toute autre réduction est une réduction bêta interne .

Une forme normale est un terme qui ne contient pas de bêta redex, c'est-à -dire qui ne peut pas être réduit davantage. Une forme normale de tête est un terme qui ne contient pas de bêta redex en position de tête, c'est-à-dire qui ne peut pas être réduit davantage par une réduction de tête. Lorsque l'on considère le calcul lambda simple (c'est-à-dire sans l'ajout de symboles constants ou de fonctions, destinés à être réduits par une règle delta supplémentaire), les formes normales de tête sont les termes de la forme suivante :

Une forme normale de tête n'est pas toujours une forme normale, car les arguments appliqués ne doivent pas nécessairement être normaux. Cependant, l'inverse est vrai : toute forme normale est également une forme normale de tête. En fait, les formes normales sont exactement les formes normales de tête dans lesquelles les sous-termes sont eux-mêmes des formes normales. Cela donne une description syntaxique inductive des formes normales.

Il existe également la notion de forme normale de tête faible : un terme en forme normale de tête faible est soit un terme en forme normale de tête, soit une abstraction lambda. Cela signifie qu'un redex peut apparaître à l'intérieur d'un corps lambda.

En général, un terme donné peut contenir plusieurs redex, et donc plusieurs réductions bêta différentes peuvent être appliquées. Nous pouvons spécifier une stratégie pour choisir quel redex réduire.

• La réduction d'ordre normal est la stratégie dans laquelle on applique continuellement la règle de réduction bêta en position de tête jusqu'à ce qu'aucune réduction de ce type ne soit plus possible. À ce stade, le terme résultant est sous forme normale de tête. On continue ensuite à appliquer la réduction de tête dans les sous-termes , de gauche à droite. En d'autres termes, la réduction d'ordre normal est la stratégie qui réduit toujours le redex le plus à gauche en premier.
• En revanche, dans la réduction d'ordre applicatif , on applique d'abord les réductions internes, puis on applique seulement la réduction de la tête lorsqu'aucune autre réduction interne n'est possible.

La réduction d'ordre normal est complète, dans le sens où si un terme a une forme normale de tête, alors la réduction d'ordre normal l'atteindra finalement. D'après la description syntaxique des formes normales ci-dessus, cela implique la même déclaration pour une forme normale « entièrement » (c'est le théorème de normalisation). En revanche, la réduction d'ordre applicatif peut ne pas se terminer, même lorsque le terme a une forme normale. Par exemple, en utilisant la réduction d'ordre applicatif, la séquence de réductions suivante est possible :

Mais en utilisant la réduction d'ordre normal, le même point de départ se réduit rapidement à la forme normale :

Les chaînes de directeur de Sinot sont une méthode par laquelle la complexité de calcul de la réduction bêta peut être optimisée.