We investigate the possibility and meaning of giving a computational
interpretation of an involutive negation in classical natural
deduction. We first show why this cannot be simply achieved by adding
"not not A = A" to typed lambda-calculus: the main obstacle is that an
involutive negation cannot be a particular case of implication at the
computational level. It means that one has to go out typed
lambda-calculus in order to have a safe computational interpretation of
an involutive negation.
We then show that, in contrary, lambda-mu-calculus can be equiped in a
natural way with an involutive negation. The abstraction and
application associated to negation are simply the operators mu and []
from lambda-mu-calculus. The resulting system, called symetric
lambda-mu-calculus, enjoys strong normalisation and has natural
confluent subsystems.
Finally we give a translation of symetric lambda-mu-calculus in
symetric lambda-mu-calculus, which doesn't make use of the rule of
mu-reduction of lambda-mu-calculus (which is precisely the rule which
makes the difference between classical and intuitionistic proofs in
the context of lambda-mu-calculus). This seems to indicate that an
involutive negation generates an original way of computing. Because
symetric lambda-mu-calculus contains both ways, it should be a good
framework for further investigations.
