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 -