Static Analysis of Modularity of β-Reduction in the Hyperbalanced λ-Calculus

J. Richard Kennaway; Zurab Khasidashvili; Adolfo Piperno

doi:10.1007/3-540-45610-4_5

Static Analysis of Modularity of β-Reduction in the Hyperbalanced λ-Calculus

J. Richard Kennaway, Zurab Khasidashvili, Adolfo Piperno

School of Computing Sciences

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

1 Citation (Scopus)

Abstract

We investigate the degree of parallelism (or modularity) in the hyperbalanced ?-calculus, ?H, a subcalculus of ?-calculus containing all simply typable terms (up to a restricted ?-expansion). In technical terms, we study the family relation on redexes in ?H, and the contribution relation on redex-families, and show that the latter is a forest (as a partial order). This means that hyperbalanced ?-terms allow for maximal possible parallelism in computation. To prove our results, we use and further refine, for the case of hyperbalanced terms, some well known results concerning paths, which allow for static analysis of many fundamental properties of ß-reduction.

Original language	English
Title of host publication	Rewriting Techniques and Applications
Editors	Sophie Tison
Publisher	Springer Berlin / Heidelberg
Pages	51-65
Number of pages	15
Volume	2378
ISBN (Print)	978-3-540-43916-5
DOIs	https://doi.org/10.1007/3-540-45610-4_5
Publication status	Published - 2002
Event	13th International Conference, RTA - Copenhagen, Denmark Duration: 22 Jul 2002 → 24 Jul 2002

Publication series

Name	Lecture Notes in Computer Science
Publisher	Springer Berlin / Heidelberg

Conference

Conference	13th International Conference, RTA
Country/Territory	Denmark
City	Copenhagen
Period	22/07/02 → 24/07/02

Access to Document

10.1007/3-540-45610-4_5

Cite this

@inbook{ae6e6c85de2d4a08919816335e37357f,

title = "Static Analysis of Modularity of β-Reduction in the Hyperbalanced λ-Calculus",

abstract = "We investigate the degree of parallelism (or modularity) in the hyperbalanced ?-calculus, ?H, a subcalculus of ?-calculus containing all simply typable terms (up to a restricted ?-expansion). In technical terms, we study the family relation on redexes in ?H, and the contribution relation on redex-families, and show that the latter is a forest (as a partial order). This means that hyperbalanced ?-terms allow for maximal possible parallelism in computation. To prove our results, we use and further refine, for the case of hyperbalanced terms, some well known results concerning paths, which allow for static analysis of many fundamental properties of {\ss}-reduction.",

author = "Kennaway, {J. Richard} and Zurab Khasidashvili and Adolfo Piperno",

year = "2002",

doi = "10.1007/3-540-45610-4_5",

language = "English",

isbn = "978-3-540-43916-5",

volume = "2378",

series = "Lecture Notes in Computer Science",

publisher = "Springer Berlin / Heidelberg",

pages = "51--65",

editor = "Sophie Tison",

booktitle = "Rewriting Techniques and Applications",

note = "13th International Conference, RTA ; Conference date: 22-07-2002 Through 24-07-2002",

}

Kennaway, JR, Khasidashvili, Z & Piperno, A 2002, Static Analysis of Modularity of β-Reduction in the Hyperbalanced λ-Calculus. in S Tison (ed.), Rewriting Techniques and Applications. vol. 2378, Lecture Notes in Computer Science, Springer Berlin / Heidelberg, pp. 51-65, 13th International Conference, RTA, Copenhagen, Denmark, 22/07/02. https://doi.org/10.1007/3-540-45610-4_5

TY - CHAP

T1 - Static Analysis of Modularity of β-Reduction in the Hyperbalanced λ-Calculus

AU - Kennaway, J. Richard

AU - Khasidashvili, Zurab

AU - Piperno, Adolfo

PY - 2002

Y1 - 2002

N2 - We investigate the degree of parallelism (or modularity) in the hyperbalanced ?-calculus, ?H, a subcalculus of ?-calculus containing all simply typable terms (up to a restricted ?-expansion). In technical terms, we study the family relation on redexes in ?H, and the contribution relation on redex-families, and show that the latter is a forest (as a partial order). This means that hyperbalanced ?-terms allow for maximal possible parallelism in computation. To prove our results, we use and further refine, for the case of hyperbalanced terms, some well known results concerning paths, which allow for static analysis of many fundamental properties of ß-reduction.

AB - We investigate the degree of parallelism (or modularity) in the hyperbalanced ?-calculus, ?H, a subcalculus of ?-calculus containing all simply typable terms (up to a restricted ?-expansion). In technical terms, we study the family relation on redexes in ?H, and the contribution relation on redex-families, and show that the latter is a forest (as a partial order). This means that hyperbalanced ?-terms allow for maximal possible parallelism in computation. To prove our results, we use and further refine, for the case of hyperbalanced terms, some well known results concerning paths, which allow for static analysis of many fundamental properties of ß-reduction.

U2 - 10.1007/3-540-45610-4_5

DO - 10.1007/3-540-45610-4_5

M3 - Chapter

SN - 978-3-540-43916-5

VL - 2378

T3 - Lecture Notes in Computer Science

SP - 51

EP - 65

BT - Rewriting Techniques and Applications

A2 - Tison, Sophie

PB - Springer Berlin / Heidelberg

T2 - 13th International Conference, RTA

Y2 - 22 July 2002 through 24 July 2002

ER -