Traduction des Combinatory Reduction Systems en Rho-Calcul

Overview & Synopsis

Les "Combinatory Reduction Systems" sont des systèmes de réécriture d'ordre supérieur étendant les systèmes de réécriture du premier ordre par un mécanisme de liaison de variables. D'un autre côté, la réécriture et le lambda-calcul ont été généralisés dans le calcul de réécriture et il est donc naturel de se demander quelle est la relation entre les deux formalismes : les systèmes de réécriture d'ordre supérieur et le rho-calcul. Nous avons analysé cette correspondance et nous présentons une fonction de traduction entre les termes CRS et les termes du rho-calcul. Nous montrons que cette traduction permet d'exprimer les réduction des termes CRS dans le rho-calcul. || The higher order rewrite systems known as Combinatory Reduction systems (CRS), introduced by J.W.Klop, are an extension of first order rewrite systems by a mechanism allowing the binding of variables. On the other side, first order rewriting and lambda c