Adjoint Rewriting and Eta-Expansions
Summary
Extensional equality for the lambda calculus requires eta-conversion,
whose interpretation as a rewrite rule has traditionally been as a
contraction. Unfortunately eta-contractions suffer from a number of
problems, eg they behave badly when combined with other rewrite rules
and do not generalise well to other type constructors.
Categorical models of reduction in the lambda-calculus interpret
introduction and elimination rules as being adjoint, with the
associated unit and counit forming an expansionary eta-
and contractive beta-rewrite rule. Not only can eta-expansions be
applied to complex type systems, but they also generalise to a wide
variety of type constructors , preserve key properties such as
confluence when combined with other well behaved rewrite relations and
normalise to the important long beta-eta normal forms.
Journal Papers
- The Virtues of Eta-Expansion . C.B.Jay and N.Ghani. In
Journal of Functional Programming , Volume 5(2), April 1995, pages 135-154. CUP 1995.
Conference Papers
- Beta-Eta Equality for
Coproducts . N.Ghani. Published in proceedings of
Typed Lambda-Calculus and Applications 1995 , number 902 in Lecture
Notes in Computer Science, pages 171 - 185. Springer-Verlag 1995. Here
is a longer version submitted to
Mathematical Structures in Computer Science .
- Adjoint
Rewriting . N. Ghani. Ph.D. Thesis, University of
Edinburgh. Graduation November 1995.
- Eta Expansions in System
F . N.Ghani. Published as technical report LIENS-96-10,
LIENS-DMI, Ecole Normale Superieure.
- Eta-Expansions in Fw
. N.Ghani. Published in proceedings of Computer
Science and Logic 1996 , number 1258 in Lecture Notes in
Computer Science, pages 182 - 197. Springer-Verlag 1997.
- Eta-Expansions in
Dependent Type Theory - The Calculus of Constructions .
N. Ghani. Published in Typed Lambda-Calculus and Applications
, number 1210 in Lecture Notes in Computer Science, pages 164 -
180. Springer-Verlag 1997.
-
On modular properties of higher order extensional lambda calculi .
R. Di Cosmo and N.Ghani. Published in proceedings of ICALP'97 , number 1256 in Lecture Notes in Computer Science,
pages 237 - 247. Springer-Verlag 1997.
-
Adjoint Rewriting and the !-Type Constructor .
N.Ghani. Draft Version - Comments Welcome.
Open Problems
Here's a couple of questions whose solution I would be interested in
- So far the techniques of adjoint rewriting have been applied to
several type constructors including the !-from linear logic. What
about modal constructors such as diamond and box? Recursive types?
Impredicative forms of quantification?
- My thesis contains a suggested eta-expansion for the natural
numbers object. Does the associated equational theory give a strong or
weak natural numbers object?
Author: Neil Ghani
Email: ng13@mcs.le.ac.uk
Tel: 44 (0)116 252 3807
Last Update: June 22 2000
The opinions expressed in this page are the authors' and not those of
the University.
Back to the homepage.