Confluence Results

  • Roberto Di Cosmo
Part of the Progress in Theoretical Computer Science book series (PTCS)


In the λ-calculus there are plenty of programs (or λ-terms) where it is pos­sible to apply the reduction rule β, introduced in 1.3.4, in more than one position. The λ-calculus does not specify a unique evaluation order, or reduction strategy, that associates to each program or term a unique position where the reduction will proceed.


Normal Form Equational Theory Reduction Rule Critical Pair Type Isomorphism 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

Copyright information

© Birkhäuser Boston 1995

Authors and Affiliations

  • Roberto Di Cosmo
    • 1
  1. 1.Ecole Normale SupérieureLIENS-DMIParis Cedex 05France

Personalised recommendations