Hey, On Fri, Nov 02, 2007 at 04:02:12PM -0400, Jeff Polakow wrote:
Hello,
I think you mean
!U -o U
is a theorem. The converse is not provable.
Oops... I should read more carefully before hitting send.
No, you were right, I was wrong :) I get confused about the syntax sometimes :) Anyway, !U -o U is indeed a theorem of linear logic (with the interpretation I gave in my previous email), and we certainly do not want to allow this theorem in a uniqueness type system. The main point I wanted to make is that in uniqueness typing, it may seem that we can allow the converse of this theorem (and allow to treat terms with a unique type as having a non-unique type), but that it is dangerous to do so unless you take the elements in function closures into account. Edsko