The virtues of eta-expansion. (English) Zbl 0833.68072

Summary: Interpreting \(\eta\)-conversion as an expansion rule in the simply-typed \(\lambda\)-calculus maintains the confluence of reduction in a richer type structure. This use of expansions is supported by categorical models of reduction, where \(\beta\)-contraction, as the local counit, and \(\eta\)- expansion, as the local unit, are linked by local triangle laws. The latter from reduction loops, but strong normalization (to the long \(\beta\eta\)-normal forms) can be recovered by ‘cutting’ the loops.


68Q42 Grammars and rewriting systems
68W30 Symbolic computation and algebraic computation
Full Text: DOI


[1] Barendregt, The Lambda Calculus Its Syntax and Semantics (Revised Ed.). Studies in Logic and the Foundations of Mathematics 103 (1984) · Zbl 0551.03007
[2] Curien, Proc. ICALP: Lecture Notes in Computer Science 510 pp 291– (1991)
[3] Seely, Proc. Second Annual Symposium on Logic in Computer Science (1987)
[4] Rydeheard, Category Theory and Computer Science: Lecture Notes in Computer Science 283 pp 114– (1987)
[5] Prawitz, Proc. 2nd Scandinavian Logic Symposium pp 235– (1971)
[6] Lambek, Introduction to higher order categorical logic (1986) · Zbl 0596.03002
[7] Kasangian, Cahiers de Topologie et Géometrie Différentielle 24 pp 23– (1983)
[8] Jay, Proc. Durham Symposium on Applications of Categories in Computer Science 177 pp 143– (1992)
[9] Jay, IV Higher Order Workshop, Banff, 1990 pp 151– (1991)
[10] DOI: 10.1016/0022-4049(88)90124-7 · Zbl 0673.18006
[11] Huet, Résolution d’équations dans des langages d’ordre 1,2,...,{\(\omega\)} (1976)
[12] Hoare, Pre-adjunctions in Order Enriched Categories (1989) · Zbl 0755.18003
[13] J.W. Gray J. W., Formal category theory: Adjointness for 2-categories: Lecture Notes in Mathematics 391 (1974) · Zbl 0285.18006
[14] Girard, Proofs and Types (1989)
[15] D., Rewriting Techniques and Applications: Lecture Notes in Computer Science 690 pp 137– (1993)
[16] Di Cosmo, Proc. ICALP: Lecture Notes in Computer Science 700 (1993)
[17] Akama, On Mints’ Reduction for ccc-Calculus. Lecture Notes in Computer Science Vol. 664 pp 1– (1993)
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.