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



revirrev.[dvi, ps].[Z, gz]: Danos & Regnier
        Reversible  &  Irreversible Computations  (GOI  & Environment
	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

	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.