There are two redexes in this term; we've marked the operative lambdas
with a star. If we reduce the leftmost redex first, the term reduces
There are two redexes in this term; we've marked the operative lambdas
with a star. If we reduce the leftmost redex first, the term reduces
redex instead, the "reduced" form is `(\x.I)Ω` again, and we are in
danger of entering an infinite loop.
redex instead, the "reduced" form is `(\x.I)Ω` again, and we are in
danger of entering an infinite loop.
One thing we'll see is that it is all too easy for the evaluation
order properties of an evaluator to depend on the evaluation order
One thing we'll see is that it is all too easy for the evaluation
order properties of an evaluator to depend on the evaluation order