[TYPES] Encoding of negation

[Peter Selinger]

Dear Vladimir,

I missed your post when it first appeared, so sorry for the relatively
late reply. Although I love to be cited, I should point out that I was
mis-cited in this case, in terms of both credit and content.

First, let me clarify that the CPS translation you are refering to is
not at all due to me; as I stated in the cited paper, this particular
translation is due to Hofmann and Streicher (1997) and Streicher and
Reus (1996), and is a variant of the original call-by-name CPS
translation of Plotkin (1975). [The variant arises because the
translation makes use of products in the target language, whereas
Plotkin's translation used only "->"]

Also, you actually copied the rules incorrectly; see below. 

Vladimir Komendantsky 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.
> >
> 
> 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.

In case anybody wondered why these rules don't make any sense (and
Phil Wadler has already wondered publicly): the reason is that these
are actually *not* the rules that appear in Section 6.1 of my
paper. For reference, the correct call-by-name rules (in the case
above) are:

A* = A+ -> R
X+ = X
(A->B)+ = (A+ -> R) x B+
(not A)+ = A+ -> R

Note the different translation of implication. This translation has
the following properties, up to intuitionistic type isomorphism:

(A -> B)*  ~~  A* -> B*   (1)
(not A)*   ~~  not A*     (2)

Soundness of the translation is therefore not extremely surprising.
The only thing this translation does (for this fragment) is to replace
each variable by a negated variable; this makes Peirce's law valid and
therefore also gives soundness for classical logic.

For the sake of completeness, here are the translations of "and" and
"or":

(A x B)+ = (A+) + (B+)
(A + B)+ = (A+) x (B+)

Note that the analog of (1) and (2) holds for "and":

(A x B)*   ~~  A* x B*    (3)

However, the corresponding property for "or" fails; we only have

(not not A + not not B)*  ~~  not not (A* + B*)  (4)

We also have

A* + B* |- (A + B)*   (4'),

but not the opposite implication. This is at the heart of why this
translation is sound from classical to intuitionistic logic. It is
slightly tighter than Goedel's double negation translation, which uses
(up to type isomorphism) (A + B)* = not not (A* + B*).

> So, for example, the law of double negation elimination
> 
> (not (not A)) |- A
> 
> is translated as
> 
> ((A+ -> R) -> R) -> R |- A+ -> R.
> 
> Since this translation is call-by-name, it is not directly related to
> Hayo Thieleke's CPS translation, which is call-by-value. The idea behind
> the call-by-name CPS translation stems back to Goedel's double negation
> translation. The variants of the CPS call-by-value translation 
> correspond (sometimes loosely) to Kolmogorov's double negation
> translation. As noted by Hayo Thieleke, in the absence of control types
> (which is exactly the case) one has universal quantification, "all Z",
> instread of just the free variable R.
> 
> >I conjecture that
> >
> >   A1, ..., An |- B
> >
> >holds in classical logic iff
> >
> >   A1*, ..., An* |- B*
> >
> >holds in intuitionistic logic.
> >
> >  
> >
> For Peter Selinger's translation above this holds if we rewrite R with
> _|_. 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.

This last statement is false, as was already pointed out by Phil
Wadler. Of course (all Z. (A+ -> Z) -> Z)) implies (A+ -> A+) -> A+),
and therefore A+, and therefore (all Z. A+), in the case where Z does
not occur in A+.

-- Peter