Re: typed eta reduction
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
In the untyped case the analogy should be with "true&q = q",
which again is unproblematical.