# Reversible computations; Proof nets and Hilbert space



Two papers by Danos and Regnier are now accessible, either by anonymous ftp on
lmd.univ-mrs.fr in the directory /pub/regnier, or by mosaic in the URL's

http://boole.logique.jussieu.fr/www.danos/experience.html
ftp://lmd.univ-mrs.fr/pub/regnier/Papers.html

________________

revirrev.[dvi, ps].[Z, gz]: Danos & Regnier
Reversible  &  Irreversible Computations  (GOI  & Environment
Machines).

We present a sequential {\it reversible\/} computation scheme
for $\lambda$-calculus coming from the {\em geometry of
interaction\/}.  The computation consists in pushing a token
(a finite list of symbols) along the term (adequately
represented as a net), each traversal of a node acting
reversibly (i.e., one-one'ly) on that token.

Then we define an optimization of that scheme taking
advantage of its call/return'' symmetry that was recently
discovered (see the {\em legality} condition of Asperti and
Laneve). Moves in this case are no longer reversible and
correspond exactly to the transitions of a simple environment
machine.

This result provides a clearcut correspondence between
reversible \& irreversible means  of computation (and it is
fun also to  know that 	GOI gives a simpler account of
computations than environment machines).

pnh.[dvi, ps].[Z, gz]: Danos & Regnier
Proof-nets and the Hilbert space,
to appear in the Proceedings of the Linear Logic Workshop
Cornell, 1993.

Girard's execution formula is a decomposition of usual
$\beta$-reduction (or cut-elimination) in reversible, local
and asynchronous elementary moves.  It can easily be
presented, when applied to a $\lambda$-term or a net, as the
sum of maximal paths on the $\lambda$-term/net that are not
cancelled by the algebra $\LS$ (as was done in Danos and
Regnier's theses).

It is then natural to ask for a characterization of those
paths, that would be only of geometric nature. We prove here
that they are exactly those paths that have residuals in any
reduct of the $\lambda$-term/net. Remarkably, the proof puts
to use for the first time the interpretation of
$\lambda$-terms/nets as operators on the Hilbert space.