[TYPES] Encoding of negation

[Burak Emir]

Krivine has written about this translation [1] and the mentioned result
appears as theorem 3.2 (without proof). He calls it Goedel's translation and
the paper is about storage operators that are specific to a data type and
serve the purpose of simulating call-by-value in call-by-name.

[1] Jean-Louis Krivine, Operateurs de mise en memoire et traduction de
Goedel, Arch. Math. Logic (1990) 30:241--267, Springer
http://www.springerlink.com/content/t420j01286833044/


Could this be what you were looking for?

cheers,
Burak

On 8/21/07, Philip Wadler <wadler at inf.ed.ac.uk> 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
>
>
>


-- 
Burak Emir
Research Assistant / PhD Candidate
Programming Methods Group
EPFL, 1015 Lausanne, Switzerland
http://lamp.epfl.ch/~emir