Paths in the lambda-calculus
Andrea Asperti, Vincent Danos, Cosimo Laneve, Laurent Régnier · Logic in Computer Science · 1994
Since the rebirth of X-calculus in the late sixties, three major theoretical investigations of r 2) Lumping’s graph-reduction algorithm; 3) Girard’s geometry of interaction. All these three studies happened to make crucial (if not always explicit) use of a notion of path. Namely and respectively: legal, consistent and regzllar paths. We prove they are equivalent.