In the λ-calculus there are plenty of programs (or λ-terms) where it is possible 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.
KeywordsNormal Form Equational Theory Reduction Rule Critical Pair Type Isomorphism
Unable to display preview. Download preview PDF.