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)

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 languageEnglish
Title of host publicationRewriting Techniques and Applications
EditorsSophie Tison
PublisherSpringer Berlin / Heidelberg
Pages51-65
Number of pages15
Volume2378
ISBN (Print)978-3-540-43916-5
DOIs
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

Conference

Conference13th International Conference, RTA
CountryDenmark
CityCopenhagen
Period22/07/0224/07/02

Cite this