Caractérisation des équivalences invisibles par des règles de réécriture confluentes

14

En réponse à une autre question, Extensions de la théorie bêta du calcul lambda , Evgenij a offert la réponse:

bêta + la règle {s = t | s et t sont des termes insolubles fermés}

où un terme M est résoluble si nous pouvons trouver une séquence de termes tels que M la demande de leur est égal à moi .

La réponse d'Evgenij donne une théorie équationnelle sur le calcul lambda, mais pas une caractérisée par un système de réduction, c'est-à-dire un ensemble de règles de réécriture confluentes et récursives.

Appelons une équivalence invisible par rapport à une théorie du calcul lambda, un système de réduction qui équivaut à un ensemble non trivial de termes lambda fermés insolubles, mais n'ajoute aucune nouvelle équation impliquant des termes résolubles.

Existe-t-il des équivalences invisibles par rapport à la théorie bêta du calcul lambda?

Postscript Un exemple qui caractérise une équivalence invisible, mais n'est pas confluent. Soit M = (λx.xx) et N = (λx.xxx) , deux termes insolubles. L'ajout de la règle de réécriture de NN à MM induit une équivalence invisible contenant MM = NN , mais a la mauvaise paire critique où NN se réduit à MM et MMN , chacun ayant une réécriture disponible, qui se réécrit pour lui-même.

pl.programming-languages lambda-calculus lo.logic Charles Stewart
la source
La notion d' équivalence invisible est liée à la notion d' extension conservatrice . Une extension conservatrice d'une théorie est un ensemble de termes et d'équations supplémentaires à la théorie qui n'ajoutent pas de nouvelles équations entre les termes de la théorie d'origine.
Dave Clarke
@supercooldave: Les termes insolubles sont des termes normaux de la théorie, tels que (λx.xx) (λx.xx) , et sont réductibles à d'autres termes (insolubles), font donc partie de la théorie normale du lambda-calcul. Le fait est qu'ils sont orthogonaux à la sémantique du calcul lambda que nous obtenons du théorème de Böhm.
Charles Stewart
λβ
@Evgenij: Oui. Il est crucial que les nouvelles règles soient confluentes et, bien sûr, triviales pour trouver des exemples si elles ne le sont pas. J'ajouterai un exemple pour montrer le problème.
Charles Stewart

Réponses:

6

Oui. Avec M = (λx.xx) par question, considérons la réécriture ζ qui prend MM p en MM .

Il est confluent et caractérise ainsi un système de réduction par rapport au calcul lambda. Esquisse d'argument pour la confluence: puisque MM est fermé, il suffit de considérer les paires critiques de la forme MMN 1 ... N k . Ces problèmes peuvent être résolus.

C'est une équivalence invisible, car les termes de la forme MMI ... I (avec zéro ou plus I s) sont des termes fermés insolubles qui ne se réduisent qu'à eux-mêmes dans le calcul lambda de base, sont donc distincts, et donc l'ensemble infini de ceux-ci termes est non trivial, et est évidemment égalé par ζ.

Je n'aime pas accepter ma réponse à ma question, donc j'accepterai une réponse de quelqu'un qui fournit un argument de confluence moins absurdement incomplet.

Charles Stewart
la source