[Prev][Next][Index][Thread]
paper annoucement
An extended abstract of the paper "Relating paths in lambda-calculus" by
A. Asperti, V. Danos, C. Laneve and L. Regnier is available by anonymous ftp on
the machine lmd.univ-mrs.fr. The file is in compressed postcript format and is
named /pub/regnier/rpilc.ps.Z. In order to give an insight of the content, the
introduction of the paper is reproduced hereafter.
Laurent Regnier
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\section{Introduction}
Let us first survey the three different notions of paths which we want to
prove are equivalent.
L\'evy took hold in~\cite{Le78} of the difficult notion of two redexes being
created in the ``same'' way during a reduction (in which case they were said
to belong to the same ``family''). Then he labeled terms and made beta
reductions act on labels so that two redexes were in the same family iff they
had the same labels.
Labels then slept fifteen years before the awakening in~\cite{ALrta93} where
they were identified with {\em legal paths}. More precisely: 1) labels of
redexes in any reduct $N$ of $M$ denote paths in $M$; 2) those paths are
legal; 3) conversely, any legal path in $M$ denotes a label of a redex to
appear somewhere in the set of reducts of $M$. Legality is a simple and
effective condition that intuitively asks for enough symmetry in the path so
that the reduction may unfold it into a redex.
In the meantime, people were seeking for a shared reduction faithfully
implementing the notion of families, i.e., a reduction where families could be
said to be reduced in one step. Such a reduction was discovered by Lamping
in~\cite{Lam90}, and also by Kathail in~\cite{Ka90} (important subsequent
simplifications were given in~\cite{GAL92p} and~\cite{As91}). The invariants
which were used to prove the correctness of Lamping's implementation were {\em
consistent paths}.
Finally Girard unveiled in~\cite{Gi88} an interpretation of the
cut-elimination procedure for linear logic. Again the alternative computation
could be defined as the computation of a particular set of paths on proofs,
namely {\em regular paths} which were defined through an algebraic and
computational device the {\em dynamic algebra}\/ (see \cite{Dan90, Reg92} where
this is also extended to pure lambda-calculus).
A fact to marvel at, is that none of the three conditions above seems to bear
any relation with beta-reduction. There is yet another equivalent definition
which may be the most natural one, but which is also the most uneffective one:
{\em persistent paths}. Call a path persistent if its residuals through any
reductions are still connected. In~\cite{goirecol} this fourth condition
is shown to be equivalent to regularity hence to all the three with which we
deal in this paper.
Apart from the satisfaction gained in knowing that there is essentially one
notion of paths in lambda-calculus, we also expect these studies to yield some
new insights about the (implementation of) beta-reduction based on the
unification of the different perspectives.
A word about linear logic. This paper could have been written entirely in the
framework of proof-nets. Actually, since proof-nets are a graphical syntax
based on a duality (the linear negation) and have a nice geometrical structure
given by their correctness condition (the trips), they are much more appealing
for working out these investigations on paths. We choose to stick to
lambda-calculus because two of the three related works were done for it.
However the results presented here may be transposed to linear logic and
proof-nets without any difficulty. This point is important since other calculi
may be encoded in proof-nets; for instance lambda-calculus-like systems for
classical logic such as the $\lambda\mu$-calculus of Parigot~\cite{Par92}.