Abstract: 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 form reduction loops, but strong normalisation (to the long beta-eta-normal forms) can be recovered by ``cutting'' the loops.
This paper will be published in the Journal of Functional Programming.
Previous | Index | Next An error occured whilst processing this directive