[Prev][Next][Index][Thread]
Long beta/eta normal forms
Date: Mon, 11 Feb 91 14:14:49 gmt
The presentation of eta-rules for exponentials and pairing in the
simply typed lambda calculus as contractions
lambda x.fx ==> f
<p1(c),p2(c)> ==> c
(pi is the ith projection) leads to a number of difficulties. Notably,
confluence only holds when the only terms of type 1 which appear are
instances of the constant *:1. One solution to this problem is to
perform the reuction in two stages: first beta-reduce as much as
possible and then perform some eta-expansions
f ==> lambda x.fx
c ==> <p1(c),p2(c)>
The question here is "Why are there two reduction systems in play?"
I came to this problem while trying to create a semantics for the
lambda calculus in which these reductions appear as 2-cells, or an
ordering, between the morphisms of a category. In order to have a
satisfying notion of adjunction in this setting (a local adjunction)
the local unit of the adjunctions must be given by eta-expansions. The
local triangle laws become
fa ==> (lambda x.fx)a ==> fa
lambda x.fx ==> lambda y.(lambda x.fx)y ==> lambda y.fy
pi(c) ==> pi<p1(c),p2(c)> ==> pi(c)
<a,b> ==> <p1<a,b>,p2<a,b>> ==> <a,b>
Now these loops make for good mathematics, and ensure easy confluence
of the rewrite system without any restrictions on terms of type 1, but
of course they destroy the termination properties. Fortunately the
obvious solution works. Simply banning any reduction which enters
one of the four loops above suffices to guarantee strong normalisation,
to the usual long beta/eta normal forms. Although this now means that
reduction on subterms is constrained, it is a purely syntactic
restriction, and also allows the usual "beta then eta" style.
Further details can be found in my abstract
"Long beta/eta normal forms in confluent categories"
available on request.
Barry Jay