[TYPES] [Fwd: Re: Encoding of negation]

[Philip Wadler]

> A closely related call-by-name CPS translation was described, e.g.,  
> in Peter Selinger's
> "Control categories and duality: on the categorical semantics of  
> the lambda-mu calculus" (2001),
> http://www.mscs.dal.ca/~selinger/papers/control.pdf
>
> There, in Section 6.1, he gives the CPS translation which, if we  
> content ourselves with the case above, gives the following rules  
> for translation of types:
>
> A* = A+ -> R
> X+ = X
> (A->B)+ = A+ -> B+
> (not A)+ = A+ -> R
>
> where R is a free fixed type variable (the type of responses). The  
> difference is in A* which now has an occurrence of R in it.

So you are suggesting that my conjecture may hold if we modify it as  
follows:

A* = all Z. A+ -> Z

A+ as before

This in effect adds a negation, so I would no longer expect
that A1,...,An |- B classically iff A1*,...,An* |-  B*  
intuitionistically,
although I might expect that A |- B classically iff B* |- A*  
intuitionistically.
Is that what you had in mind?

> But if we let
>
> A* = all Z. A+
>
> (and don't rewrite response variables) we obtain the following  
> translation of the double negation elimination:
>
> all Z. (A+ -> Z) -> Z) |- all Z. A+
>
> This is not provable already in classical logic (otherwise (A\/B)- 
> >A would be provable). In this sence the above conjecture does not  
> hold.

Why do you claim that if the above is provable then (A\/B)->A is  
provable?  Note that in the case where A does not contain negation,  
all Z. (A+ -> Z) -> Z is isomorphic to A, in the presence of  
parametricity.

Cheers,  -- P