Re: typed eta reduction

To: Bard Bloom <bard@THEORY.LCS.MIT.EDU>
Subject: Re: typed eta reduction
From: coraki!pratt@Sun.COM (Vaughan Pratt)
Date: Thu, 9 Jun 88 11:17:33 PDT
Cc: types@theory.lcs.mit.edu
In-Reply-To: message of Thu, 9 Jun 88 11:10:12 edt. <8806091510.AA04660@TOUCAN.LCS.MIT.EDU>

The analogy depended on reading \x:t.fx as cutting down the domain of f
to t.  For f with domain other than t this is the only reading I've
been able to assign.  I was hoping that my question might bring to
light some other reading that would give more general circumstances
than dom(f)=t under which eta reduction could be trusted.

On second thought I think <p?>q is more appropriate for the analogy
than [p?]q; the latter does not so much cut down the domain of q as
bypass q when p is false.  In that case the analogy is with "<p?>q =
q", which of course is just "p&q = q".

When f has domain t the analogy is with "p&p = p", which I have no
problem with.

In the untyped case the analogy should be with "true&q = q",
which again is unproblematical.
-v