[TYPES] Encoding of negation
Carter Tazio Schonwald
carter.schonwald at yale.edu
Tue Aug 21 12:36:46 EDT 2007
I believe that this paper
http://www.cs.bham.ac.uk/~hxt/research/effects.pdf
by Hayo Thielecke studies this style of translation and its use in the
presence of effects
cheers,
-Carter
Philip Wadler wrote:
> [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
>
> One possible encoding of negation, closely related to the CPS
> translation, is the following:
>
> A* = all Z. A+
>
> X+ = X
> (A -> B)+ = A+ -> B+
> (not A)+ = A+ -> Z
>
> where Z is a fresh type variable that does not appear free in A. I
> conjecture that
>
> A1, ..., An |- B
>
> holds in classical logic iff
>
> A1*, ..., An* |- B*
>
> holds in intuitionistic logic.
>
> Has anyone explored this translation? As an example of its interest,
> I conjecture that A* and (not (not A))* are isomorphic in the
> presence of parametricity; this is certainly true if A contains no
> negations.
>
> Many thanks for any responses. Cheers, -- P
>
>
>
>
>
More information about the Types-list
mailing list