AN EQUIVALENCE RELATIONSHIP BETWEEN LAMBDA-TERMS

In this paper an equivalence relation between lambda-terms is defined which identifies terms only differing by permutation of radices: the sigma-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 sigma-equivalent terms. Finally, the sigma-equivalence is used for proving a generalisation of the perpetual strategy theorem.