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

A Asperti; V. Danos; C. Laneve; L. Regnier

doi:10.1109/LICS.1994.316048

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

A Asperti, V. Danos, C. Laneve, L. Regnier

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

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

Original language	English
Title of host publication	Logic in Computer Science, 1994. LICS '94. Proceedings., Symposium on
Publisher	Institute of Electrical and Electronics Engineers (IEEE)
Pages	426-436
Number of pages	11
ISBN (Print)	0-8186-6310-3
DOIs	https://doi.org/10.1109/LICS.1994.316048
Publication status	Published - Jul 1994

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

Access to Document

10.1109/LICS.1994.316048

http://ieeexplore.ieee.org/xpl/articleDetails.jsp?arnumber=316048

Cite this

@inproceedings{ea67d895e0154d1b8de6ca03bc507b38,

title = "Paths in the lambda-calculus. Three years of communications without understanding",

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",

author = "A Asperti and V. Danos and C. Laneve and L. Regnier",

year = "1994",

month = jul,

doi = "10.1109/LICS.1994.316048",

language = "English",

isbn = "0-8186-6310-3 ",

pages = "426--436",

booktitle = "Logic in Computer Science, 1994. LICS '94. Proceedings., Symposium on",

publisher = "Institute of Electrical and Electronics Engineers (IEEE)",

address = "United States",

}

TY - GEN

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

AU - Asperti, A

AU - Danos, V.

AU - Laneve, C.

AU - Regnier, L.

PY - 1994/7

Y1 - 1994/7

N2 - 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

AB - 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

KW - computational geometry

KW - graph theory

KW - lambda calculus

KW - β-reduction

KW - consistent paths

KW - graph-reduction algorithm

KW - interaction geometry

KW - labeled reductions

KW - lambda-calculus

KW - legal paths

KW - redex families

KW - regular paths

KW - Algorithm design and analysis

KW - Displays

KW - Geometry

KW - Joining processes

KW - Law

KW - Legal factors

KW - Logic devices

U2 - 10.1109/LICS.1994.316048

DO - 10.1109/LICS.1994.316048

M3 - Conference contribution

SN - 0-8186-6310-3

SP - 426

EP - 436

BT - Logic in Computer Science, 1994. LICS '94. Proceedings., Symposium on

PB - Institute of Electrical and Electronics Engineers (IEEE)

ER -

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

Abstract

Keywords

Access to Document

Fingerprint

Cite this