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
in dynamic logic would be the equivalence
[p?]q = q
This is unsound in dynamic logic. Why should it be sound in a typed
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?