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

J. Richard Kennaway, Zurab Khasidashvili, Adolfo Piperno

Research output: Chapter in Book/Report/Conference proceedingChapter

1 Citation (Scopus)


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 languageEnglish
Title of host publicationRewriting Techniques and Applications
EditorsSophie Tison
PublisherSpringer Berlin / Heidelberg
Number of pages15
ISBN (Print)978-3-540-43916-5
Publication statusPublished - 2002
Event13th International Conference, RTA - Copenhagen, Denmark
Duration: 22 Jul 200224 Jul 2002

Publication series

NameLecture Notes in Computer Science
PublisherSpringer Berlin / Heidelberg


Conference13th International Conference, RTA

Cite this