[TYPES] [Fwd: Re: Encoding of negation]
Philip Wadler
wadler at inf.ed.ac.uk
Sat Aug 25 05:59:54 EDT 2007
> 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
More information about the Types-list
mailing list