Une équivalence sur les lambda- termes

Dans ce papier on définit une relation d'équivalence sur les lambda-termes, identifiant les termes qui ne diffèrent que par des permutations de radicaux: la σ-équivalence. On démontre qu'aucun des critères opérationnels standards de classification du lambda-calcul (e. g. la longueur de la plus longue normalisation) ne permet de distinguer deux termes σ-équivalents. Enfin, la σ-équivalence est utilisée pour démontrer une généralisation du théorème de la stratégie perpétuelle. In this paper an equivalence relation between lambda-terms is defined which identifies terms only differing by permutation of radices: the σ-equivalence. It is shown that none of the standard operational classification criteria on lambda-calculus (e. g. the length of the longest reduction) can separate two σ-equivalent terms. Finally, the σ-equivalence is used for proving a generalisation of the perpetual strategy theorem.

Authors

• Laurent Regnier

Keywords

No keywords are indexed for this paper.