DocumentCode :
1995849
Title :
Paths in the lambda-calculus. Three years of communications without understanding
Author :
Asperti, Andrea ; Danos, Vincent ; Laneve, Cosimo ; Regnier, Laurent
Author_Institution :
Bologna Univ., Italy
fYear :
1994
fDate :
4-7 Jul 1994
Firstpage :
426
Lastpage :
436
Abstract :
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
Keywords :
computational geometry; graph theory; lambda calculus; β-reduction; consistent paths; graph-reduction algorithm; interaction geometry; labeled reductions; lambda-calculus; legal paths; redex families; regular paths; Algorithm design and analysis; Displays; Geometry; Joining processes; Law; Legal factors; Logic devices;
fLanguage :
English
Publisher :
ieee
Conference_Titel :
Logic in Computer Science, 1994. LICS '94. Proceedings., Symposium on
Conference_Location :
Paris
Print_ISBN :
0-8186-6310-3
Type :
conf
DOI :
10.1109/LICS.1994.316048
Filename :
316048
Link To Document :
بازگشت