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 |
Pages | 426-436 |
Number of pages | 11 |
ISBN (Print) | 0-8186-6310-3 |
DOIs | |
Publication status | Published - Jul 1994 |
Keywords / Materials (for Non-textual outputs)
- 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