[L7] ================================================ AMAST Links 02 02

                    Two papers by Danos and Regnier 

  These papers are available on the WWW at
URL: http://boole.logique.jussieu.fr/www.danos/experience.html
and _also_ at
URL: ftp://lmd.univ-mrs.fr/pub/regnier/Papers.html
or by _anonymous ftp_ from the directory at
URL: ftp://lmd.univ-mrs.fr/pub/regnier/
  The file revirrev.[dvi, ps].[Z, gz] is the paper
   Reversible and Irreversible Computations
   (GOI & Environment Machines)
  We present a sequential _reversible_ computation scheme for
lambda-calculus coming from the _geometry of interaction_.  The
computation consists in pushing a token (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 _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 and 
irreversible means  of computation (and it is fun also to  know that 
GOI gives a simpler account of computations than environment machines).
  The file pnh.[dvi, ps].[Z, gz] is the paper
   Proof-nets and the Hilbert space
  to appear in 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.