共 7 条
- [1] BARENDREGT H, 1978, LAMBDA CALCULUS
- [2] DANOS V, 1990, THESIS U PARIS 7
- [3] DEVRIJER R, 1987, CR ACAD SCI HOLL DEC
- [5] Krivine J.-L., 1990, LAMBDA CALCUL TYPES
- [6] REGNIER L, 1992, THESIS U PARIS 7, V6
- [7] VIDAL D, 1989, THESIS U NANCY 1
AN EQUIVALENCE RELATIONSHIP BETWEEN LAMBDA-TERMS
被引：50
作者：
REGNIER, L
机构：
[1] Laboratoire de Mathématiques Discrètes, UPR 9016 du CNRS, 13288 Marseille Cedex 9
关键词：
D O I：
10.1016/0304-3975(94)90012-4
中图分类号：
TP301 [理论、方法];
学科分类号：
081202 ;
摘要：
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.
引用
收藏
页码：281 / 292
页数：12
相关论文