Paths in the lambda-calculus. Three years of communications without understanding

Since the rebirth of λ-calculus in the late 1960s, three major theoretical investigations of β-reduction have been undertaken: (1) Levy´s (1978) analysis of families of redexes (and the associated concept of labeled reductions); (2) Lamping´s (1990) graph-reduction algorithm; and (3) Girard´s (1988) geometry of interaction. All three studies happened to make crucial (if not always explicit) use of the notion of a path, namely and respectively: legal paths, consistent paths and regular paths. We prove that these are equivalent to each other