X-Git-Url: http://lambda.jimpryor.net/git/gitweb.cgi?p=lambda.git;a=blobdiff_plain;f=week2.mdwn;h=77459bfda891dc264e5619162878263015ef5706;hp=992c8c8975efd62467f72b8e7c6458460f004135;hb=94621f911e8647cb12c1eb0a759ef2c3ffdb3f53;hpb=600b9e54be61643b0d85021bfbfbd575f47b0d17 diff --git a/week2.mdwn b/week2.mdwn index 992c8c89..77459bfd 100644 --- a/week2.mdwn +++ b/week2.mdwn @@ -161,7 +161,8 @@ One important advantage of normal-order evaluation in particular is that it can Indeed, it's provable that if there's *any* reduction path that delivers a value for a given expression, the normal-order evalutation strategy will terminate with that value. -An expression is said to be in **normal form** when it's not possible to perform any more reductions. (EVEN INSIDE ABSTRACTS?) There's a sense in which you *can't get anything more out of* ω ω, but it's not in normal form because it still has the form of a redex. +An expression is said to be in **normal form** when it's not possible to perform any more reductions (not even inside abstracts). +There's a sense in which you *can't get anything more out of* ω ω, but it's not in normal form because it still has the form of a redex. A computational system is said to be **confluent**, or to have the **Church-Rosser** or **diamond** property, if, whenever there are multiple possible evaluation paths, those that terminate always terminate in the same value. In such a system, the choice of which sub-expressions to evaluate first will only matter if some of them but not others might lead down a non-terminating path.