typed eta reduction

• To: coraki!pratt@Sun.COM
• Subject: typed eta reduction
• From: Bard Bloom <bard@THEORY.LCS.MIT.EDU>
• Date: Thu, 9 Jun 88 11:10:12 edt
• Cc: types@theory.lcs.mit.edu
• In-Reply-To: Vaughan Pratt's message of Thu, 9 Jun 88 08:03:11 PDT <8806091503.AA05893@>

   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

• Prev: Re: specification logic and call by name
• Next: typed eta reduction
• Index(es):
  • Main
  • Thread