[Prev][Next][Index][Thread]
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.