From: Jim Pryor Date: Fri, 17 Sep 2010 20:37:40 +0000 (-0400) Subject: tweak week2 X-Git-Url: http://lambda.jimpryor.net/git/gitweb.cgi?p=lambda.git;a=commitdiff_plain;h=c359efaee71b34e8db4e7527c75766fde6c0e8fa tweak week2 Signed-off-by: Jim Pryor --- 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.