[Prev][Next][Index][Thread]

typed eta reduction



   Date: Thu, 9 Jun 88 08:03:11 PDT
   From: coraki!pratt@Sun.COM (Vaughan Pratt)

   The analogue of the eta reduction

           \x:tau. fx   >     f
                         eta

   in dynamic logic would be the equivalence

           [p?]q = q

   This is unsound in dynamic logic.  Why should it be sound in a typed
   lambda calculus?
   -v

I don't understand the analogy; or rather, I don't understand why the analogy
between dynamic logic and typed lambda calculus should be any more plausible
than between DL and untyped lambda calculus, where eta is sound.

Do you have some equivalence between some dynamic logic and some typed lambda
calculus in mind?  Do you have a reference for it?

-- Bard